lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

index.md (1698B)

      1 +++
      2 title = "Lambda terms"
      3 +++
      4 
      5 # Lambda terms
      6 ## abstraction
      7 πœ†.M is function mapping of x to M
      8 πœ†x.square x is function mapping of x to square x
      9 
     10 ## application
     11 F M is application of function F to argument M
     12 
     13 ## terms as trees
     14 ![screenshot.png](6b229883cf977b73b10c370d2cf2bca9.png)
     15 ![screenshot.png](b06d6359ad899d2f43b675ff8530866d.png)
     16 
     17 ## parentheses
     18 application is associative to the left
     19 `(M N P) β€”> ((M N) P)`
     20 
     21 outermost parentheses are omitted
     22 `M N P β€”> (M N P)`
     23 
     24 lambda extends to the right as far as possible
     25 `πœ†x.M N β€”> πœ†x.(M N)`
     26 
     27 combining lambdas is possible
     28 `πœ†xy.M β€”> πœ†x.πœ†y.M`
     29 
     30 start with most nested lambda
     31 `(πœ†x.πœ†y.M) β€”> πœ†x.(πœ†y.M))`
     32 
     33 ## currying
     34 reduces function with several arguments to functions with single arguments
     35 
     36 f: x => x+x β€”> πœ†x.x+x
     37 g: (x,y) => x+y β€”> πœ†x.πœ†y.x+y
     38 
     39 ## free/bound variables
     40 x is bound by the first πœ†x above it in the term tree (underlined)
     41 
     42 - πœ†x.<u>x</u>
     43 - πœ†x.<u>x x</u>
     44 - (πœ†x.<u>x</u>)x
     45 - πœ†x.yΒ <u>x</u>
     46 
     47 variables that aren’t bound are free (such as y in the last example)
     48 
     49 ## substitution
     50 M[x := N] means: result of replacing all free *x*Β in M by N
     51 
     52 - x[x := N] = N
     53 - a[x := N] = a
     54 - (P Q)[x := N] = (P[x := N]) (Q[x := N])
     55 - (πœ†x.P)[x := N] = πœ†x.P
     56 - (πœ†y.P)[x := N] = πœ†y.(P[y := N]) if x β‰  y
     57 
     58 ## alpha conversion
     59 renaming bound variables (in case of possible name clashes)
     60 - πœ†x.x =Β πœ†y.y
     61 - (πœ†x.y)[y := x] =Β πœ†z.x
     62 
     63 P = Ξ±Q only if Q can be obtained from P by finitely many changes of bound variables in context
     64 
     65 ## beta-reduction (dynamic):
     66 (πœ†x.x)y β€”> By
     67 (πœ†x.x)y β€”> By
     68 (πœ†x.xz)y β€”> Byz
     69 (πœ†x.z)y β€”> Bz
     70 
     71 In general: (πœ†x.M)N β€”> BM[x := N]