176x Filetype PDF File size 0.31 MB Source: www2.imm.dtu.dk
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
no reviews yet
Please Login to review.