CIS 500Software FoundationsFall 2006September 27Programming in theLambda-Calculus, ContinuedTesting booleansRecall:tru = λt. λf. tfls =λt. λf. fWe showed last time that, if b is a boolean (i.e., it behaves likeeither tru or fls), then, for any values v and w, eitherb v w −→∗v(if b behaves like tru) orb v w −→∗w(if b behaves like fls).Testing booleansBut what if we apply a boolean to terms that are not values?E.g., what is the result of evaluatingtru c0 omega ?Not what we want!Testing booleansBut what if we apply a boolean to terms that are not values?E.g., what is the result of evaluatingtru c0 omega ?Not what we want!A better wayA dummy “unit value,” for forcing evaluation of thunks:unit = λx. xA “conditional function”:test = λb. λt. λf. b t f unitIfb is a boolean (i.e., it behaves like either tru or fls), then, forarbitrary terms s and t, eitherb (λdummy. s) (λdummy. t) −→∗s(if b behaves like tru) orb (λdummy. s) (λdummy. t) −→∗t(if b behaves like fls).Review: The Z OperatorIn the last lecture, we defined an operator Z that calculates the“fixed point” of a function it is applied to:z=λf. λy. (λx. f (λy. x x y)) (λx. f (λy. x x y)) yThat is, z f v −→∗f (z f) v.(N.b.: I’m writing it with a lower-case z today so that codesnippet s in the lecture notes can literally be typed into thefulluntyped interpreter, which expects identifiers to begin withlowercase letters.)FactorialAs an example, we defined the factorial function inlambda-calculus as follows:fact = z ( λfct.λn.if n=0 then 1else n * (fct (pred n)) )For the sake of the example, we used “regular” booleans, numbers,etc.I c laimed that all this could be translated “straightforwardly” intothe pure lambda-calculus.Let’s do this.Factorialbadfact =z (λfct.λn.iszro nc1(times n (fct (prd n))))Why is this not what we want?(Hint: What happens when we evaluate badfact c0?)Factorialbadfact =z (λfct.λn.iszro nc1(times n (fct (prd n))))Why is this not what we want?(Hint: What happens when we evaluate badfact c0?)FactorialA better version:fact =fix (λfct.λn.test (iszro n)(λdummy. c1)(λdummy. (times n (fct (prd n)))))Displaying numbersfact c6 −→∗(λs. λz.s ((λs. λz.s ((λs. λz.s ((λs. λz.s ((λs. λz.s ((λs. λz.s ((λs. λz.z)s z))s z))s z))s z))s z))s z))Ugh!Displaying numbersfact c6 −→∗(λs. λz.s ((λs. λz.s ((λs. λz.s ((λs. λz.s ((λs. λz.s ((λs. λz.s ((λs. λz.z)s z))s z))s z))s z))s z))s z))Ugh!Displaying numbersIf we enrich the pure lambda-calculus with “regular numb ers,” wecan display church numerals by converting them to regularnumbe rs:realnat = λn. n (λm. succ m) 0Now:realnat (times c2 c2)−→∗succ (succ (succ (succ zero))).Displaying numbersAlternatively, we can convert a few specific numbers to the formwe want like this:whack =λn. (equal n c0) c0((equal n c1) c1((equal n c2) c2((equal n c3) c3((equal n c4) c4((equal n c5) c5((equal n c6) c6n))))))Now:whack (fact c3)−→∗λs. λz. s (s (s (s (s (s z)))))A Larger ExampleIn the second homework assignment, we saw how to encode aninfinite st ream as a thunk yielding a pair of a head element andanother thunk representing the rest of the stream. The sameenco ding also works in the lambda-calculus.Head and tail functions for streams:streamhd = λs. fst (s unit)streamtl =λs. snd (s unit)A stre am of increasing numbers:upfrom =fix(λr.λn.λdummy.pair n (r (scc n)))Some tests:whack (streamhd (upfrom c0))−→∗c0whack (streamhd (streamtl (upfrom c0)))−→∗c2whack (streamhd (streamtl (streamtl (upfrom c0))))−→∗c4Mapping over streams:streammap =fix(λsm.λf.λs.λdummy.pair (f (streamhd s)) (sm f (streamtl s)))Some tests:evens = streammap double (upfrom c0);whack (streamhd evens);/* yields c0 */whack (streamhd (streamtl evens));/* yields c2 */whack (streamhd (streamtl (streamtl evens)));/* yields c4 */Equivalence of Lambda TermsRepresenting NumbersWe have seen how certain terms in the lambda-calculus can beused t o represent natural numbers.c0= λs. λz. zc1= λs. λz. s zc2= λs. λz. s (s z)c3= λs. λz. s (s (s z))Other lambda-terms represent common operations on numbers:scc = λn. λs. λz. s (n s z)In what sense can we say this representation is “correct”?In particular, on what basis can we argue that scc on churchnumerals corresponds to ordinary successor on numbers?Representing NumbersWe have seen how certain terms in the lambda-calculus can beused t o represent natural numbers.c0= λs. λz. zc1= λs. λz. s zc2= λs. λz. s (s z)c3= λs. λz. s (s (s z))Other lambda-terms represent common operations on numbers:scc = λn. λs. λz. s (n s z)In what sense can we say this representation is “correct”?In particular, on what basis can we argue that scc on churchnumerals corresponds to ordinary successor on numbers?The naive approach... doesn’t workOne possibility:For each n, the term scc cnevaluates t o cn+1.Unfortunately, this is false.E.g.:scc c2= (λn. λs. λz. s (n s z)) (λs. λz. s (s z))−→ λs. λz. s ((λs. λz. s (s z)) s z)6= λs. λz. s (s (s z))= c3The naive approach... doesn’t workOne possibility:For each n, the term scc cnevaluates t o cn+1.Unfortunately, this is false.E.g.:scc c2= (λn. λs. λz. s (n s z)) (λs. λz. s (s z))−→ λs. λz. s ((λs. λz. s (s z)) s z)6= λs. λz. s (s (s z))= c3A better approachRecall t he intuition behind the church numeral representation:Ia number n is represented as a term that “does something ntimes to something else”Iscc takes a term that “does something n times to somethingelse” and returns a term that “does something n + 1 times tosomething else”I.e., what we really care about is that scc c2be haves the same asc3when applied to two arguments.scc c2v w = (λn. λs. λz. s (n s z)) (λs. λz. s (s z)) v w−→(λs. λz. s ((λs. λz. s (s z)) s z)) v w−→(λz. v ((λs. λz. s (s z)) v z)) w−→v ((λs. λz. s (s z)) v w)−→v ((λz. v (v z)) w)−→v (v (v w))c3v w = (λs. λz. s (s (s z))) v w−→(λz. v (v (v z))) w−→v (v (v w)))A general questionWe have argued that, although scc c2and c3do not evaluate tothe same thing, they are nevertheless “behaviorally equivalent.”What, precisely, does behavioral equivalence mean?IntuitionRoughly,“terms s and t are behaviorally equivalent”should mean:“there is no ‘test’ that distinguishes s and t — i.e., no way toput them in the same context and observe different results.”To make this precise,