Cheat sheet – λ-calculus
                   BNFgrammar                                       Parenthesis
                                              • application is left-associative: T T T = T (T T )
           T ::= x       (variable)                                            1 2 3    1  2 3
                | (TT)   (application)        • λ-abstraction is right-associative:
                                                 λx:λy:T = λx:(λy:T) and λx:T T = λx:(T T )
                | (λx:T) (λ-abstraction)                                      1 2        1 2
                                              • (T T ) = T T
                                                   1 2     1 2
                                               Well-known terms
                                                                          λ
                         λ                                              x
           • I = λx:x                                                          λ
                       x     x
                                             • S = λx:λy:λz:((xz)(yz))       y     λ
                             λ
           • K=λx:λy:x                                                           z     @
                           x     λ
                                y                                                    @       @
                                      x
                                                                                   x     z y    z
                                        Free variables vs bound variables
                            Free variable                           bound variable
                        defined outside a term                     intern to the term
                name is essential (cannot be modified)  name is not important (can be modified)
                                                           
                                                           FV(x)       ={x}
                   Inductive definition of Free Variables FV:  FV(T T ) = FV(T )∪FV(T )
                                                                  1 2          1         2
                                                           FV(λx:T)=FV(T)n{x}
                                                  Substitution
               [x 7→T ]T is the term defined by replacing all free occurrences of x within T by T
                      1 2                                                               2     1
                                       (1) [x 7→T]x = T
               Inductive definition of  (2) [x 7→T]y = y                     if x 6= y
                substitution on Λ :    (3) [x 7→T]T T = [x 7→T]T [x 7→T]T
                                X                  1 2           1         2
                                       (4) [x 7→T]λy:T′ = λy:[x 7→T]T′      if x 6= y and y∈/ FV (T)
                                     α-conversion or α-equivalence (renaming)
                     renaming a defining occurrence and all its depending bound occurrences
                                      λx:T = λy:[x 7→y]T if y ∈/ FV(T)
                                             α
                                      e.g.: λx:x =α λy:y but λx:y 6=α λx:z
                                                  β-reduction
                 λx:T T →[x7→T ]T                           can be applied anywhere in a term
                     1 2          2  1