CSc 520Principles of Programming Languages23: Lambda Calculus — PureChristian CollbergDepartment of Computer ScienceUniversity of [email protected] 2005 Christian CollbergApril 22, 20051 Pure vs. Impure Lambda Calculus• The version of lambda calculus we have looked at so far has been impure — it has contained constantssuch as h1, 2, 3, · · ·i and add, sqr, etc.• Church’s Thesis says that lambda calculus can define every computable function.• If we’re going to believe Church’s Thesis we are going to have to define the natural numbers, arithmeticoperations, booleans, pairs, conditional expressions and recursion, directly in the calculus.• A lambda calculus so defined contains no constants, and is said to be pure.2 Church’s Numerals• We can encode a natural number as the number of times 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))))))13 Church’s Numerals — succ• succ’s first argument is n, the number to be incremented. succ just adds one more application of thef function (its second argument). The third argument (x) is the “base case”, 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 Church’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))))) ≡ 35 Church’s Numerals — add• add takes two numbers n and m as arguments.• (m f) simply plugs in f as the function used to represent numbers in the expression for m, (n f ) doesthe same for the second number.• (add f (f (x)) g(g(g(x)))) (representing 2 + 3) constructs a new function h(h(h(h(h(x))))) (representing5).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)26 Church’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))))))) = 57 Church’s Numerals — mult• Multiplying 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 Pairs• Just like in Scheme, we can define pairs — these allow us to construct data structures such as lists andtrees.• The definition of Pair below is similar to a dotted pair notation (or cons) in Scheme.• Head and Tail correspond to car and cdr, Nil is a special 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 Pairs. . .• We can construct a pair (p, q) (or (p.q) in Scheme notation) 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))310 Pairs. . .• 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 definition of 2.11 Pairs. . .• 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 Pairs. . .• We can verify that Head works as specified:4Pair ≡ (λ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) ⇒∗βp13 Church’s Booleans• We define two constants for true and false, and a function if 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 Church’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) ⇒βv15 Church’s Booleans. . .• and can be defined like this:5false ≡ (λt.(λf.f))if ≡ (λl.(λm.(λn.((l m) n))))and ≡ (λa.(λb.(((if a) b) false))) =(λa.(λb.((((λl.(λm.(λn.((l m) n)))) a) b) false))) ⇒∗β(λa.(λb.((a b) false)))16 Church’s Booleans. . .• iszero can be defined like this:false ≡ (λt.(λf.f))if ≡ (λl.(λm.(λn.((l m) n))))iszero ≡ (λm.((m (λx.false)) true))Recursion17 Recursive Functions• If lambda calculus is going to allow us to compute any function, we need for it to handle recursion.• Example:fact ≡ (λn.if (zero n) 1 (mult n (fact (pred n))))• Unfortunately, the name fact appears in the expression itself. Remember that we defined ≡ -operatoras macro-expansion, and recursive macros make no sense.• Recursion is defined in normal programming languages, but not in lambda calculus.18 Fixed Points• A fixed point is a value x in the domain of a function that is the same in the range f (x).• In other words, a fixed point of a function is a value left fixed by that function; for example, 0 and 1are fixed points of the squaring function.• Formally, a value x is a
View Full Document
Unlocking...