From 4b58f050598948e1345d1a5734257c656adb9002 Mon Sep 17 00:00:00 2001 From: Chris Date: Wed, 18 Feb 2015 14:55:13 -0500 Subject: [PATCH] added draft of assignment4 --- exercises/_assignment4.mdwn | 110 ++++++++++++++++++++++++++++++++++++ exercises/_assignment4_answers.mdwn | 27 +++++++++ 2 files changed, 137 insertions(+) create mode 100644 exercises/_assignment4.mdwn create mode 100644 exercises/_assignment4_answers.mdwn diff --git a/exercises/_assignment4.mdwn b/exercises/_assignment4.mdwn new file mode 100644 index 00000000..bb67eb40 --- /dev/null +++ b/exercises/_assignment4.mdwn @@ -0,0 +1,110 @@ +## 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. + +## 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`? + + +
  2. (More challenging.) Using our derivation of Y from the [Week3 +notes](/week3/#index4h2) as a model, construct a pair `Y1` and `Y2` that behave +in the way described. + +(See [[hints/Assignment 4 hint 3]] if you need some hints.) + diff --git a/exercises/_assignment4_answers.mdwn b/exercises/_assignment4_answers.mdwn new file mode 100644 index 00000000..ac1ab6eb --- /dev/null +++ b/exercises/_assignment4_answers.mdwn @@ -0,0 +1,27 @@ +1. Find a fixed point `X` for the succ function: + + H := \f.succ(ff) + X := HH + == (\f.succ(ff)) H + ~~> succ(HH) + +So `succ(HH) <~~> succ(succ(HH))`. + +2. Prove that `add 1 X <~~> X`: + + add 1 X == (\mn.m succ n) 1 X + ~~> 1 succ X + == (\fz.fz) succ X + ~~> succ X + +What about `add 2 X`? + + add 2 X == (\mn.m succ n) 2 X + ~~> 2 succ X + == (\fz.f(fz)) succ X + ~~> succ (succ X) + +So `add n X <~~> X` for all (finite) natural numbers `n`. + + + -- 2.11.0