-
Notifications
You must be signed in to change notification settings - Fork 18
Expand file tree
/
Copy pathLessons-Lesson14.html
More file actions
34 lines (34 loc) · 17.8 KB
/
Lessons-Lesson14.html
File metadata and controls
34 lines (34 loc) · 17.8 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /><title>Lessons.Lesson14</title><link href="linuwial.css" rel="stylesheet" type="text/css" title="Linuwial" /><link rel="stylesheet" type="text/css" href="quick-jump.css" /><link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=PT+Sans:400,400i,700" /><script src="haddock-bundle.min.js" async="async" type="text/javascript"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { processClass: "mathjax", ignoreClass: ".*" } });</script><script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></head><body><div id="package-header"><span class="caption empty"> </span><ul class="links" id="page-menu"><li><a href="src/Lessons.Lesson14.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>Safe-Inferred</td></tr></table><p class="caption">Lessons.Lesson14</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Notes taken by Jonas Grybė</p><p>VARIABLE BINDING PROBLEM:
When substituting in lambda calculus, we must change only FREE variables, not BOUND ones.
Example: (λx.λy.x(xy)) - x and y are bound, we can't just replace them.</p><p>TWO SOLUTIONS:
1. Barendregt Convention: All variables must be unique (eliminates name conflicts).
2. De Bruijn Indices: Don't use names - use numbers indicating distance to binding lambda.
Examples: λx.x → λ.0 | λx.λy.x(xy) → λ.λ.1(10) | λx.λy.b(yx) → λ.λ.2(01)</p><p>EVALUATION STRATEGIES:
- Full Beta Reduction: Reduce anywhere (messy, can use function or argument first)
- Call by Value: Evaluate arguments before passing (Java, C#, C)
- Call by Name: No reduction inside abstractions (Haskell)</p></div></div><div id="synopsis"><details id="syn"><summary>Synopsis</summary><ul class="details-toggle" data-details-id="syn"><li class="src short"><span class="keyword">data</span> <a href="#t:Term">Term</a><ul class="subs"><li>= <a href="#v:Var">Var</a> String</li><li>| <a href="#v:Abs">Abs</a> String <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li><li>| <a href="#v:App">App</a> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li></ul></li><li class="src short"><a href="#v:tru">tru</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li><li class="src short"><a href="#v:fls">fls</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li><li class="src short"><a href="#v:c0">c0</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li><li class="src short"><a href="#v:c2">c2</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li><li class="src short"><a href="#v:apps">apps</a> :: [<a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a>] -> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li><li class="src short"><a href="#v:land">land</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li><li class="src short"><a href="#v:expr">expr</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:ITerm">ITerm</a><ul class="subs"><li>= <a href="#v:IVar">IVar</a> Int</li><li>| <a href="#v:IAbs">IAbs</a> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></li><li>| <a href="#v:IApp">IApp</a> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></li></ul></li><li class="src short"><a href="#v:deBruijnIndices">deBruijnIndices</a> :: [String] -> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></li><li class="src short"><a href="#v:termShift">termShift</a> :: Int -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></li><li class="src short"><a href="#v:termSubst">termSubst</a> :: Int -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></li><li class="src short"><a href="#v:termSubstTop">termSubstTop</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></li><li class="src short"><a href="#v:isVal">isVal</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> Bool</li><li class="src short"><a href="#v:eval">eval</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></li></ul></details></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:Term" class="def">Term</a> <a href="src/Lessons.Lesson14.html#Term" class="link">Source</a> <a href="#t:Term" class="selflink">#</a></p><div class="doc"><p>Named lambda calculus representation. Grammar: term = x | λx.t | tt</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:Var" class="def">Var</a> String</td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:Abs" class="def">Abs</a> String <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:App" class="def">App</a> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><h4 class="instances details-toggle-control details-toggle" data-details-id="i:Term">Instances</h4><details id="i:Term" open="open"><summary class="hide-when-js-enabled">Instances details</summary><table><tr><td class="src clearfix"><span class="inst-left"><span class="instance details-toggle-control details-toggle" data-details-id="i:id:Term:Show:1"></span> Show <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a></span> <a href="src/Lessons.Lesson14.html#line-25" class="link">Source</a> <a href="#t:Term" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><details id="i:id:Term:Show:1"><summary class="hide-when-js-enabled">Instance details</summary><p>Defined in <a href="Lessons-Lesson14.html">Lessons.Lesson14</a></p> <div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: Int -> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> -> ShowS</p><p class="src"><a href="#v:show">show</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> -> String</p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a>] -> ShowS</p></div></details></td></tr></table></details></div></div><div class="top"><p class="src"><a id="v:tru" class="def">tru</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="src/Lessons.Lesson14.html#tru" class="link">Source</a> <a href="#v:tru" class="selflink">#</a></p><div class="doc"><p>Church boolean TRUE: λt.λf.t (returns first argument)
>>> show tru
"(<em>|t.(</em>|f.t))"</p></div></div><div class="top"><p class="src"><a id="v:fls" class="def">fls</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="src/Lessons.Lesson14.html#fls" class="link">Source</a> <a href="#v:fls" class="selflink">#</a></p><div class="doc"><p>Church boolean FALSE: λt.λf.f (returns second argument)
>>> show fls
"(<em>|t.(</em>|f.f))"</p></div></div><div class="top"><p class="src"><a id="v:c0" class="def">c0</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="src/Lessons.Lesson14.html#c0" class="link">Source</a> <a href="#v:c0" class="selflink">#</a></p><div class="doc"><p>Church numeral ZERO: λs.λz.z (successor applied 0 times)
Based on Peano numbers: z=zero, s=successor function.
>>> show c0
"(<em>|s.(</em>|z.z))"</p></div></div><div class="top"><p class="src"><a id="v:c2" class="def">c2</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="src/Lessons.Lesson14.html#c2" class="link">Source</a> <a href="#v:c2" class="selflink">#</a></p><div class="doc"><p>Church numeral TWO: λs.λz.s(s z) (successor applied 2 times)
>>> show c2
"(<em>|s.(</em>|z.(s (s z))))"</p></div></div><div class="top"><p class="src"><a id="v:apps" class="def">apps</a> :: [<a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a>] -> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="src/Lessons.Lesson14.html#apps" class="link">Source</a> <a href="#v:apps" class="selflink">#</a></p><div class="doc"><p>Builds left-associative applications from a list of terms.
Allows us to write expression over expression, building complex applications.
Takes multiple terms and combines them: apps [t1, t2, t3] = ((t1 t2) t3)</p></div></div><div class="top"><p class="src"><a id="v:land" class="def">land</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="src/Lessons.Lesson14.html#land" class="link">Source</a> <a href="#v:land" class="selflink">#</a></p><div class="doc"><p>Logical AND for Church booleans: λb.λc.b c false
>>> show land
"(<em>|b.(</em>|c.((b c) (<em>|t.(</em>|f.f)))))"</p></div></div><div class="top"><p class="src"><a id="v:expr" class="def">expr</a> :: <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> <a href="src/Lessons.Lesson14.html#expr" class="link">Source</a> <a href="#v:expr" class="selflink">#</a></p><div class="doc"><p>Example expression: (land true true)
>>> show expr
"(((<em>|b.(</em>|c.((b c) (<em>|t.(</em>|f.f))))) (<em>|t.(</em>|f.t))) (<em>|t.(</em>|f.t)))"</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:ITerm" class="def">ITerm</a> <a href="src/Lessons.Lesson14.html#ITerm" class="link">Source</a> <a href="#t:ITerm" class="selflink">#</a></p><div class="doc"><p>Nameless lambda terms using De Bruijn indices (no variable names, just numbers).</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:IVar" class="def">IVar</a> Int</td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:IAbs" class="def">IAbs</a> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:IApp" class="def">IApp</a> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><h4 class="instances details-toggle-control details-toggle" data-details-id="i:ITerm">Instances</h4><details id="i:ITerm" open="open"><summary class="hide-when-js-enabled">Instances details</summary><table><tr><td class="src clearfix"><span class="inst-left"><span class="instance details-toggle-control details-toggle" data-details-id="i:id:ITerm:Show:1"></span> Show <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></span> <a href="src/Lessons.Lesson14.html#line-89" class="link">Source</a> <a href="#t:ITerm" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><details id="i:id:ITerm:Show:1"><summary class="hide-when-js-enabled">Instance details</summary><p>Defined in <a href="Lessons-Lesson14.html">Lessons.Lesson14</a></p> <div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: Int -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> ShowS</p><p class="src"><a href="#v:show">show</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> String</p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a>] -> ShowS</p></div></details></td></tr><tr><td class="src clearfix"><span class="inst-left"><span class="instance details-toggle-control details-toggle" data-details-id="i:id:ITerm:Eq:2"></span> Eq <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a></span> <a href="src/Lessons.Lesson14.html#line-87" class="link">Source</a> <a href="#t:ITerm" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><details id="i:id:ITerm:Eq:2"><summary class="hide-when-js-enabled">Instance details</summary><p>Defined in <a href="Lessons-Lesson14.html">Lessons.Lesson14</a></p> <div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:-61--61-">(==)</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> Bool</p><p class="src"><a href="#v:-47--61-">(/=)</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> Bool</p></div></details></td></tr></table></details></div></div><div class="top"><p class="src"><a id="v:deBruijnIndices" class="def">deBruijnIndices</a> :: [String] -> <a href="Lessons-Lesson14.html#t:Term" title="Lessons.Lesson14">Term</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> <a href="src/Lessons.Lesson14.html#deBruijnIndices" class="link">Source</a> <a href="#v:deBruijnIndices" class="selflink">#</a></p><div class="doc"><p>Converts named terms to De Bruijn indices.
ctx: free variable names (context) - not bound within the term.
Walk the term with empty stack initially. When numbering, we go from inside to inside,
stacking variable names as we enter abstractions (n : stack).
findInd checks stack first (bound vars), then context (free vars).
For context variables: take context position + length of stack to renumber properly.</p></div></div><div class="top"><p class="src"><a id="v:termShift" class="def">termShift</a> :: Int -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> <a href="src/Lessons.Lesson14.html#termShift" class="link">Source</a> <a href="#v:termShift" class="selflink">#</a></p><div class="doc"><p>Shifts free variables by d. Cutoff c tracks binding depth.
Variables with index >= c are free and get shifted.</p></div></div><div class="top"><p class="src"><a id="v:termSubst" class="def">termSubst</a> :: Int -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> <a href="src/Lessons.Lesson14.html#termSubst" class="link">Source</a> <a href="#v:termSubst" class="selflink">#</a></p><div class="doc"><p>Substitutes term s for variable j. Core operation for beta reduction.
When x == j+c, replace with s (shifted by c for binders).</p></div></div><div class="top"><p class="src"><a id="v:termSubstTop" class="def">termSubstTop</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> <a href="src/Lessons.Lesson14.html#termSubstTop" class="link">Source</a> <a href="#v:termSubstTop" class="selflink">#</a></p><div class="doc"><p>Top-level substitution for beta reduction: (λ.t) s → [s/0]t
Shift s up, substitute, shift result down.</p></div></div><div class="top"><p class="src"><a id="v:isVal" class="def">isVal</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> Bool <a href="src/Lessons.Lesson14.html#isVal" class="link">Source</a> <a href="#v:isVal" class="selflink">#</a></p><div class="doc"><p>Only abstractions are values in call-by-name.</p></div></div><div class="top"><p class="src"><a id="v:eval" class="def">eval</a> :: <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> -> <a href="Lessons-Lesson14.html#t:ITerm" title="Lessons.Lesson14">ITerm</a> <a href="src/Lessons.Lesson14.html#eval" class="link">Source</a> <a href="#v:eval" class="selflink">#</a></p><div class="doc"><p>Single-step evaluator (call-by-name, like Haskell).
From Pierce's "Types and Programming Languages".
Each eval call returns a shorter expression.</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.29.2</p></div></body></html>