From: Jim Date: Sat, 21 Feb 2015 14:15:57 +0000 (-0500) Subject: Merge branch 'working' X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=6694165ac4d6edab602b3ad3651d0a5931b36a0e;hp=12b94057358619fd5ae7a48f685fedba8ce4d082 Merge branch 'working' * working: replace tattoo image --- diff --git a/content.mdwn b/content.mdwn index a546e9d8..b6f23c0b 100644 --- a/content.mdwn +++ b/content.mdwn @@ -80,4 +80,4 @@ Week 4: * [[Fixed point combinators|topics/week4_fixed_point_combinators]] * [[More about fixed point combinators|topics/week4_more_about_fixed_point_combinators]] * Towards types (in progress) - +* [[Homework for week 4|exercises/assignment4]] diff --git a/exercises/_assignment4.mdwn b/exercises/_assignment4.mdwn deleted file mode 100644 index 7df06052..00000000 --- a/exercises/_assignment4.mdwn +++ /dev/null @@ -1,146 +0,0 @@ -## Recursion ## - -## Basic fixed points ## - -1. Recall that `ω := \f.ff`, and ```Ω := -ω ω```. Is `Ω` a fixed point for -`ω`? Find a fixed point for `ω`, -and prove that it is a fixed point. - -2. Consider `Ω X` for an arbitrary term `X`. -Ω is so busy reducing itself (the eternal solipsist) that it -never gets around to noticing whether it has an argument, let alone -doing anything with that argument. If so, how could Ω have a -fixed point? That is, how could there be an `X` such that -`Ω X <~~> Ω(Ω X)`? To answer this -question, begin by constructing `YΩ`. Prove that -`YΩ` is a fixed point for Ω. - -3. Find two different terms that have the same fixed point. That is, -find terms `F`, `G`, and `X` such that `F(X) <~~> F(F(X))` and `G(X) -<~~> G(G(X))`. (If you need a hint, reread the notes on fixed -points.) - -## Writing recursive functions ## - -4. Helping yourself to the functions given just below, -write a recursive function caled `fac` that computes the factorial. -The factorial `n! = n * (n - 1) * (n - 2) * ... * 3 * 2 * 1`. -For instance, `fac 0 ~~> 1`, `fac 1 ~~> 1`, `fac 2 ~~> 2`, `fac 3 ~~> -6`, and `fac 4 ~~> 24`. - - let true = \then else. then in - let false = \then else. else in - let iszero = \n. n (\x. false) true in - let pred = \n f z. n (\u v. v (u f)) (K z) I in - let succ = \n f z. f (n f z) in - let add = \n m .n succ m in - let mult = \n m.n(add m)0 in - let Y = \h . (\f . h (f f)) (\f . h (f f)) in - - let fac = ... in - - fac 4 - -## Arithmetic infinity? ## - -The next few questions involve reasoning about Church arithmetic and -infinity. Let's choose some arithmetic functions: - - succ = \nfz.f(nfz) - add = \m n. m succ n in - mult = \m n. m (add n) 0 in - exp = \m n . m (mult n) 1 in - -There is a pleasing pattern here: addition is defined in terms of -the successor function, multiplication is defined in terms of -addition, and exponentiation is defined in terms of multiplication. - -1. Find a fixed point `X` for the succ function. Prove it's a fixed -point, i.e., demonstrate that `succ X <~~> succ (succ X)`. - -We've had surprising success embedding normal arithmetic in the lambda -calculus, modeling the natural numbers, addition, multiplication, and -so on. But one thing that some versions of arithmetic supply is a -notion of infinity, which we'll write as `inf`. This object usually -satisfies the following constraints, for any (finite) natural number `n`: - - n + inf == inf - n * inf == inf - n ^ inf == inf - n leq inf == True - -2. Prove that `add 1 X <~~> X`, where `X` is the fixed -point you found in (1). What about `add 2 X <~~> X`? - -Comment: a fixed point for the succ function is an object such that it -is unchanged after adding 1 to it. It make a certain amount of sense -to use this object to model arithmetic infinity. For instance, -depending on implementation details, it might happen that `leq n X` is -true for all (finite) natural numbers `n`. However, the fixed point -you found for succ is unlikely to be a fixed point for `mult n` or for -`exp n`. - - -#Mutually-recursive functions# - -
-
1. (Challenging.) One way to define the function `even` is to have it hand off -part of the work to another function `odd`: - - let even = \x. iszero x - ; if x == 0 then result is - true - ; else result turns on whether x's pred is odd - (odd (pred x)) - -At the same tme, though, it's natural to define `odd` in such a way that it -hands off part of the work to `even`: - - let odd = \x. iszero x - ; if x == 0 then result is - false - ; else result turns on whether x's pred is even - (even (pred x)) - -Such a definition of `even` and `odd` is called **mutually recursive**. If you -trace through the evaluation of some sample numerical arguments, you can see -that eventually we'll always reach a base step. So the recursion should be -perfectly well-grounded: - - even 3 - ~~> iszero 3 true (odd (pred 3)) - ~~> odd 2 - ~~> iszero 2 false (even (pred 2)) - ~~> even 1 - ~~> iszero 1 true (odd (pred 1)) - ~~> odd 0 - ~~> iszero 0 false (even (pred 0)) - ~~> false - -But we don't yet know how to implement this kind of recursion in the lambda -calculus. - -The fixed point operators we've been working with so far worked like this: - - let X = Y T in - X <~~> T X - -Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on -a *pair* of functions `T1` and `T2`, as follows: - - let X1 = Y1 T1 T2 in - let X2 = Y2 T1 T2 in - X1 <~~> T1 X1 X2 and - X2 <~~> T2 X1 X2 - -If we gave you such a `Y1` and `Y2`, how would you implement the above -definitions of `even` and `odd`? - - -