Lambda Calculus
                     Prof. Tobias Nipkow
                      August 2, 2012
                  Contents
                  1 Untyped Lambda Calculus                                                                                3
                     1.1   Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      3
                           1.1.1    Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      3
                           1.1.2    Currying (Sch¨onfinkeln) . . . . . . . . . . . . . . . . . . . . . . . . . . . .        4
                           1.1.3    Static binding and substitution . . . . . . . . . . . . . . . . . . . . . . . .        5
                           1.1.4    α-conversion    . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .    6
                     1.2   β-reduction (contraction)      . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .    7
                           1.2.1    Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .        9
                     1.3   η-reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      11
                     1.4   λ-calculus as an equational theory       . . . . . . . . . . . . . . . . . . . . . . . . . .   13
                           1.4.1    β-conversion    . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .   13
                           1.4.2    η-conversion and extensionality . . . . . . . . . . . . . . . . . . . . . . . .       14
                     1.5   Reduction strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .       14
                     1.6   Labeled terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      15
                     1.7   Lambda calculus as a programming language . . . . . . . . . . . . . . . . . . . .              16
                           1.7.1    Data types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      16
                           1.7.2    Recursive functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .     18
                           1.7.3    Computable functions on IN: . . . . . . . . . . . . . . . . . . . . . . . . .         19
                  2 Typed Lambda Calculi                                                                                 21
                     2.1   Simply typed λ-calculus (λ→) . . . . . . . . . . . . . . . . . . . . . . . . . . . . .         22
                           2.1.1    Type checking for explicitly typed terms . . . . . . . . . . . . . . . . . . .        22
                     2.2   Termination of →β . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .        24
                     2.3   Type inference for λ→ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .        26
                     2.4   let-polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .         26
                  3 The Curry-Howard Isomorphismus                                                                       29
                  A Relational Basics                                                                                    33
                     A.1 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .       33
                     A.2 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .          33
                     A.3 Commuting relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .          36
                                                                      1
       2                                   CONTENTS
               Chapter 1
               Untyped Lambda Calculus
               1.1     Syntax
               1.1.1    Terms
               Definition 1.1.1 In lambda calculus the set of terms are defined as follows:
                                          t   ::=   c  |  x | (t t ) | (λx.t)
                                                                  1 2
               (t t ) is called application and represents the application of a function t to an argument t .
                 1 2                                                                   1                 2
               (λx.t) is called abstraction and represents the function with formal parameter x and body t;
               x is bound in t.
               Convention:
                      x,y,z            variables
                      c,d,f,g,h        constants
                      a,b              atoms = variables ∪ constants
                      r,s,t,u,v,w      terms
               In lambda calculus there is one computation rule called β-reduction: ((λx.s) t) can be reduced
               to s[t/x], the result of replacing the arguments t for the formal parameter x in s. Examples:
                                       ((λx.((f x)x))5)         →            ((f 5)5)
                                                                  β
                                        ((λx.x)(λx.x))          →            (λx.x)
                                                                  β
                                             (x(λy.y))   cannot be reduced
               The precise definition of s[t/x] needs some work.
               Notation:
                   • Variables are listed after λ: λx ...x .s ≡ λx ....λx .s
                                                   1     n       1       n
                   • Application associates to the left: (t1 ...tn) ≡ (((t1 t2)t3)...tn)
                   • λ binds to the right as far as possible.
                     Example:    λx.x x ≡ λx.(x x) 6≡ (λx.x) x
                   • Outermost parentheses are omitted: t1...tn ≡ (t1...tn)
                                                             3