Pure vs. Impure Lambda CalculusChurch's NumeralsChurch's Numerals --- LC {succ}Church's Numerals --- LC {succ}ldots Church's Numerals --- LC {add}Church's Numerals --- LC {add}ldots Church's Numerals --- LC {mult}PairsPairsldots Pairsldots Pairsldots Pairsldots Church's BooleansChurch's Booleansldots Church's Booleansldots Church's Booleansldots RecursionRecursive FunctionsFixed PointsFixed Points --- ExamplesFixed Points --- Examplesldots Fixed Point CombinatorsFixed Point Combinatorsldots Fixed Point Combinatorsldots Fixed Point Combinatorsldots Fixed Point Combinatorsldots Fixed Point Combinators --- ExampleFixed Point Combinators --- Exampleldots Fixed Point Combinators --- Exampleldots Fixed Point Combinators --- Exampleldots Fixed Point Combinators --- Exampleldots Fixed Point Functions in HaskellFixed Point Functions in Haskellldots Readings and ReferencesAcknowledgments520—Spring 2005—23CSc 520Principles of ProgrammingLanguages23: Lambda Calculus — PureChristian [email protected] of Computer ScienceUniversity of ArizonaCopyrightc 2005 Christian Collberg[1]520—Spring 2005—23Pure vs. Impure Lambda CalculusThe version of lambda calculus we have looked at so farhas been impure — it has contained constants such ash1, 2, 3, · · ·i and add, sqr, etc.Church’s Thesis says that lambda calculus can defineevery computable function.If we’re going to believe Church’s Thesis we are goingto have to define the natural numbers, arithmeticoperations, booleans, pairs, conditional expressionsand recursion, directly in the calculus.A lambda calculus so defined contains no constants,and is said to be pure.[2]520—Spring 2005—23Church’s NumeralsWe can encode a natural number as the number oftimes a function parameter is applied:0 ≡ (λf.(λx.x))1 ≡ (λf.(λx.(f x)))2 ≡ (λf.(λx.(f (f x))))3 ≡ (λf.(λx.(f (f (f x)))))We can now define arithmetic operations:succ ≡ (λn.(λf.(λx.(f ((n f) x)))))add ≡ (λm.(λn.(λf.(λx.((m f) ((n f) x))))))[3]520—Spring 2005—23Church’s Numerals — succsucc’s first argument is n, the number to be incremented.succ just adds one more application of the f function (itssecond argument). The third argument (x) is the “basecase”, that is, zero.2 ≡ (λg.(λy.(g (g y))))succ ≡ (λn.(λf.(λx.(f ((n f) x)))))(succ 2) ⇒((λn.(λf.(λx.(f ((n f ) x))))) (λg.(λy.(g (g y)))))...[4]520—Spring 2005—23Church’s Numerals — succ...succ ≡ (λn.(λf.(λx.(f ((n f) x)))))2 ≡ (λg.(λy.(g (g y))))3 ≡ (λf.(λx.(f (f (f x)))))(succ 2) ⇒((λn.(λf.(λx.(f ((n f ) x))))) (λg.(λy.(g (g y))))) ⇒β(λf.(λx.(f (((λg.(λy.(g (g y)))) f ) x)))) ⇒β(λf.(λx.(f ((λy.(f (f y))) x)))) ⇒β(λf.(λx.(f (f (f x))))) ≡ 3[5]520—Spring 2005—23Church’s Numerals — addadd takes two numbers n and m as arguments.(m f) simply plugs in f as the function used torepresent numbers in the expression form, (n f) doesthe same for the second number.(add f(f(x)) g(g(g(x)))) (representing 2 + 3) constructs anew functionh(h(h(h(h(x))))) (representing 5).2 ≡ (λg.(λy.(g (g y))))3 ≡ (λh.(λz.(h (h (h z)))))add ≡ (λm.(λn.(λf.(λx.((m f ) ((n f) x))))))(add 2 3) ⇒(((λm.(λn.(λf.(λx.((m f) ((n f) x)))))) (λg.(λy.(g (g y))))) 3)[6]520—Spring 2005—23Church’s Numerals — add...2 ≡ (λg.(λy.(g (g y))))3 ≡ (λh.(λz.(h (h (h z)))))add ≡ (λm.(λn.(λf.(λx.((m f ) ((n f ) x))))))(add 2 3) ⇒(((λm.(λn.(λf.(λx.((m f) ((n f) x)))))) (λg.(λy.(g (g y))))) 3) ⇒β((λn.(λf.(λx.((λy.(f (f y))) ((n f ) x))))) 3) ⇒β((λn.(λf.(λx.((λy.(f (f y))) ((n f ) x))))) (λh.(λz.(h (h (h z)))))) ⇒β(λf.(λx.((λy.(f (f y))) (((λh.(λz.(h (h (h z))))) f) x)))) ⇒β(λf.(λx.((λy.(f (f y))) ((λz.(f (f (f z)))) x)))) ⇒β(λf.(λx.((λy.(f (f y))) (f (f (f x)))))) ⇒β(λf.(λx.(f (f (f (f (f x))))))) = 5[7]520—Spring 2005—23Church’s Numerals — multMultiplying m ∗ n is like adding m copies of n together:add ≡ (λm.(λn.(λf.(λx.((m f ) ((n f) x))))))mult ≡ (λm.(λn.(m ((plus n) zero))))[8]520—Spring 2005—23PairsJust like in Scheme, we can define pairs — these allowus to construct data structures such as lists and trees.The definition of Pair below is similar to a dotted pairnotation (or cons) in Scheme.Head and Tail correspond to car and cdr, Nil is aspecial constant.Pair ≡ (λa.(λb.(λf.((f a) b))))Head ≡ (λg.(g (λa.(λb.a))))Tail ≡ (λg.(g (λa.(λb.b))))Nil ≡ (λx.(λa.(λb.a)))[9]520—Spring 2005—23Pairs...We can construct a pair (p, q) (or (p.q) in Schemenotation) like this:Pair ≡ (λa.(λb.(λf.((f a) b))))((Pair p) q) =(((λa.(λb.(λf.((f a) b)))) p) q) ⇒β((λb.(λf.((f p) b))) q) ⇒β(λf.((f p) q))[10]520—Spring 2005—23Pairs...We can construct the list [2] like this:Pair ≡ (λa.(λb.(λf.((f a) b))))Nil ≡ (λx.(λa.(λb.a)))((Pair 2) Nil) =(((λa.(λb.(λf.((f a) b)))) 2) Nil) ⇒β((λb.(λf.((f 2) b))) Nil) ⇒β(λf.((f 2) Nil)) = (λf.((f 2) (λx.(λa.(λb.a)))))We can go even further and substitute in the definitionof 2.[11]520—Spring 2005—23Pairs...We can construct the list [1, 2] like this:Pair ≡ (λa.(λb.(λf.((f a) b))))Nil ≡ (λx.(λa.(λb.a)))((Pair 1) ((Pair 2) Nil)) =((Pair 1) (λf.((f 2) Nil))) =(((λa.(λb.(λf.((f a) b)))) 1) (λg.((g 2) Nil))) ⇒β((λb.(λf.((f 1) b))) (λg.((g 2) Nil))) ⇒β(λf.((f 1) (λg.((g 2) Nil))))[12]520—Spring 2005—23Pairs...We can verify that Head works as specified:Pair ≡ (λa.(λb.(λf.((f a) b))))Head ≡ (λg.(g (λa.(λb.a))))((Pair p) q) = (((λa.(λb.(λf.((f a) b)))) p) q) ⇒β((λb.(λf.((f p) b))) q) ⇒β(λf.((f p) q))(Head ((Pair p) q)) = (Head (λf.((f p) q))) =((λg.(g (λa.(λb.a)))) (λf.((f p) q))) ⇒β((λf.((f p) q)) (λa.(λb.a))) ⇒β(((λa.(λb.a)) p) q) ⇒∗βp[13]520—Spring 2005—23Church’s BooleansWe define two constants for true and false, and a functionif for selection:true ≡ (λt.(λf.t))false ≡ (λt.(λf.f))if ≡ (λl.(λm.(λn.((l m) n))))We can now write programs with control flow![14]520—Spring 2005—23Church’s Booleans...We can verify that if works as expected:true ≡ (λt.(λf.t))if ≡ (λl.(λm.(λn.((l m) n))))(((if true) v) w) = ((((λl.(λm.(λn.((l m) n)))) true) v) w) ⇒β(((λm.(λn.((true m) n))) v) w) =(((λm.(λn.(((λt.(λf.t)) m) n))) v) w) ⇒β(((λm.(λn.((λf.m) n))) v) w) ⇒β(((λm.(λn.m)) v) w) ⇒β((λn.v) w) ⇒βv[15]520—Spring 2005—23Church’s Booleans...and can
View Full Document
Unlocking...