141x Filetype PDF File size 0.24 MB Source: is.muni.cz
IA014: Advanced Functional Programming 2. Untyped Lambda Calculus Jan Obdržálek obdrzalek@fi.muni.cz Faculty of Informatics, Masaryk University, Brno IA014 2. Untyped Lambda Calculus 1 Formal development IA014 2. Untyped Lambda Calculus 2 Syntax Theset of λ-terms is defined by the following BNF grammar: M::= x variable | MM′ application | λx.M abstraction • where x,y,z,... are variables from a countable set Var • weuseuppercaseletters M,N,... to denote λ-terms • (,) are used whenever the meaning is not clear examples I ≡ λx.x K≡λx.(λy.x) ω≡λx.(xx) S≡λx.(λy.(λz.((x z)(y z)))) Ω≡ωω≡(λx.(xx))(λx.(xx)) IA014 2. Untyped Lambda Calculus 3 Syntactic conventions • λx x ...x .M means λx .(λx .(...(λx .M)...)) 1 2 n 1 2 n • M M M ...M means(...((M M )M )...) 1 2 3 n 1 2 3 application associates to the left • λx.x y means λx.(x y) function application takes precedence • spaces have no meaning Examples simplified λx.(x y z) λx.x y z (λx.x) y (λx.x) y λx.(λy.x) λxy.x λx.(λy.(λz.((x z) (y z))) λxyz.(x z) (y z) IA014 2. Untyped Lambda Calculus 4
no reviews yet
Please Login to review.