Lambda Calculus
      
      
      General Notice
      
        - 
           Exam:  The oral exam will be held on February 8, 2018. 
 
        - 
          This course overlaps with the second half of the course
          Equational Logic and Lambda Calculus (IN2048). Only one of the two courses can be credited towards your degree.
        
 
        - There will be weekly homework sheets, which will be graded. Students who achieve 50% of the homework points will
          receive a bonus mark of 0.3, provided that they also pass the final exam.
        
 
      
      Excercises
      
      Contents
      
        Lambda Calculus
        
          - Untyped Lambda calculus
 
          - 
            
              - Syntax
 
              - 
                Terms, notational conventions, Currying, static binding, free and bound variables, substitution, alpha-conversion.
 
              - Beta-reduction
 
              - Definition of beta-reduction. Definition of parallel reduction >. Proof that > has the diamond property. Because
                >
                  * = →
                  β
                  *
                 this implies that β-reduction is confluent. (See confluence proof for orthogonal TRS)
 
              - Eta-reduction
 
              - Motivation, definition and basic properties: termination and (local) confluence. No proofs.
 
              - Reduction strategies
 
              - Without proof: contraction of leftmost β-redexes leads to a normal form if one exists.
 
              - Lambda calculus as a programming language
 
              - Booleans, pairs, Church numerals, fixed-point combinators.
 
            
           
          - Typed Lambda calculus
 
          - 
            
              - Simply typed lambda calculus
 
              - Simple types. Implicitly and explicitly typed terms. Type checking rules. Properties: 1. beta-reduction preserves
                types ("subject reduction") (w/o proof). 2. beta-reduction terminates on type-correct terms (w/o proof).
                Thus beta-equivalence is decidable for type-correct terms (but has non-elementary complexity).
                Corollary The simply-typed lambda-calculus can only represent total functions.
                Thm Every computable functions is representable as a closed type-correct lambda-term whose only contants
                are additional fixed-point combinators (proof only sketched).
 
              - Type inference
 
              - The rules. Type-correct terms no longer have a unique type but still a most general type. Proof by a concrete
                Prolog-like interpretation of the typing rules as backward computation rules.
 
              - Let-polymorphism
 
              - Universally quantified type schemas. Typing rules for "let" and for type schemas. Syntax-directed typing rules
                with built-in quantifier handling.
 
              - Curry-Howard isomorphism
 
              - Types = formulas, lambda-terms = proofs, beta-reduction = proof-reduction. Proof of the subterm property of
                proofs in normal form. Proof of decidability of intuitionistic propositional logic via proofs in normal form.
 
            
           
        
       
      
        Literature
        Primary:
        
        Additional:
        
          - 
            Hendrik Pieter Barendregt.
              The Lambda Calculus, its Syntax and Semantics, North-Holland, 2nd edition, 1984
          
 
          - 
            Jean-Yves Girard, Yves Lafont, and Paul Taylor.
              
                Proofs and Types
              , Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989
          
 
          - 
            Chris Hankin.
              An Introduction to Lambda Calculi for Computer Scientists, King's College Publications, 2004
          
 
          - 
            J. Roger Hindley and Jonathan P. Seldin.
              Introduction to Combinators and Lambda Calculus, Cambridge University Press, 1986
          
 
          - 
            J. Roger Hindley and Jonathan P. Seldin.
              Lambda-Calculus and Combinators: An Introduction, Cambridge University Press, 2008