02157
                                                                                                                                                     Functional
                                                                                                                                                      Program-
                                                                                                                                                        ming
             02157 Functional Programming                                                                                                           MichaelR.Hansen
             Abrief introduction to Lambda calculus                                                                                                 Lambda
                                                                                                                                                    calculus
                                                                                                                                                     Background
                                                                                                                                                     Syntax
                                                                                                                                                     reductions
             Michael R. Hansen                                                                                                                       Lambda
                                                                                                                                                     terms as
                                                                                                                                                     programs
                                                                                                                                                     Church
                                                                                                                                                     numerals
                                                                                                                                                     Fixpoint
                                                                                                                                                     combinators
 1       DTUInformatics,Technical University of Denmark                                           Abrief introduction to Lambda calculus       MRH25/10/2012
    Purpose
                                                                                                                                                       02157
                                                                                                                                                     Functional
                                                                                                                                                      Program-
                                                                                                                                                        ming
                                                                                                                                                    MichaelR.Hansen
             Thetheoreticalunderpinningof functional languagesis λ-calculus.                                                                        Lambda
                                                                                                                                                    calculus
                                                                                                                                                     Background
             Thepurposeisto hint on this underpinningand to introduce                                                                                Syntax
                                                                                                                                                     reductions
             concepts of functional languages.                                                                                                       Lambda
                                                                                                                                                     terms as
                                                                                                                                                     programs
                 • Informal introduction to λ-calculus                                                                                               Church
                                                                                                                                                     numerals
                          • computations of lambda-calculus and functional languages                                                                 Fixpoint
                                                                                                                                                     combinators
             Todayyouwill be introduced to basic concepts of λ-calculus and you
             will get a feeling for the theoretical power of these concepts by the
             construction of an interpreter for a λ-calculus based language .
 2       DTUInformatics,Technical University of Denmark                                           Abrief introduction to Lambda calculus       MRH25/10/2012
    Lambdacalculus: background
                                                                                                                                                       02157
                                                                                                                                                     Functional
                                                                                                                                                      Program-
                                                                                                                                                        ming
                                                                                                                                                    MichaelR.Hansen
                 • Invented in the 1930’s by the logician Alonzo Church in logical                                                                  Lambda
                     studies and in investigations of function definition and                                                                        calculus
                                                                                                                                                     Background
                     application, and recursion.                                                                                                     Syntax
                                                                                                                                                     reductions
                 • Comprisefull computability.                                                                                                       Lambda
                                                                                                                                                     terms as
                                                                                                                                                     programs
                 • First uncomputability results were discovered using λ-calculus.                                                                   Church
                                                                                                                                                     numerals
             Somequestions                                                                                                                           Fixpoint
                                                                                                                                                     combinators
                 • Doesthemathematicalexpressionx −y denotea function,say
                     f, of x or a function, say g, of y, or :::?
                 • Doesthenotationh(z) mean a function h or h applied to z
 3       DTUInformatics,Technical University of Denmark                                           Abrief introduction to Lambda calculus       MRH25/10/2012
    Lambdacalculus: informal ideas
                                                                                                                                                       02157
                                                                                                                                                     Functional
                                                                                                                                                      Program-
                                                                                                                                                        ming
                 • λx:e denotes the anonymousfunction of x which e is.                                                                              MichaelR.Hansen
             Examplesoffunction definitions:                                                                                                         Lambda
                                                                                                                                                    calculus
                                                                                                                                                     Background
                 • Let f be λx:x − y                                                                                                                 Syntax
                     Theexpressionx −y consideredas a function f : Z → Z of x                                                                        reductions
                                                                                                                                                     Lambda
                 • g = λy:x −y                                                                                                                       terms as
                                                                                                                                                     programs
                     Theexpressionx −y consideredas a function g : Z → Z of y                                                                        Church
                                                                                                                                                     numerals
                                                                                                                                                     Fixpoint
                 • h = λx:λy:x −y                                                                                                                    combinators
                     Theexpressionx −y consideredas a higher-orderfunction
                     h : Z → (Z → Z)
             Examplesoffunction applications:
                 • f(1) = 1−y andg(1) = x −1
                 • h(2) = λy:2 −y and h(2)(5) = 2−5 = −3
 4       DTUInformatics,Technical University of Denmark                                           Abrief introduction to Lambda calculus       MRH25/10/2012