Lambda Calculus Cheat SheetCS 68April 3, 20111 Lambda calculus syntaxLambda calculus terms are variables, function applications, or function defini-tions:M ::= v | (M M) | λv. Mwhere “v” represents a variable symbol.Computation takes place by substituting in actual parameters for free occur-rences of formal parameters, which are defined by induction on the structure oflambda calculus terms as follows:Definition 1.1 If M is a term, then FV(M), the collection of free variables ofM, is defined as follows:1. FV(x) = { x }2. FV(M N) = FV(M) ∪ FV(N) Lambe3. FV(λv. M) = FV(M) - { v }Definition 1.2 We write [N/x] M to denote the result of replacing all free oc-currences of identifier x by N in expression M.1. [N/x] x∆= N,2. [N/x] y∆= y, if y 6= x,3. [N/x] (L M)∆= ([N/x] L) ([N/x] M),4. [N/x] (λy. M)∆= λy. ([N/x] M), if y 6= x and y 6∈ FV(N),5. [N/x] (λx. M)∆=λx. M.12 Rules of ComputationDefinition 2.1 The reduction rules for the lambda calculus are given by:(α) λx. Mα→→ λ y. ([y/x] M), if y 6∈ FV(M).(β) (λx. M) Nβ→→ [N/x] M.(η) λx. (M x)η→→
View Full Document