From 1557d471b7e1c4c8723ab78f0fa6492f59554ba1 Mon Sep 17 00:00:00 2001 From: Chris Date: Thu, 19 Feb 2015 09:14:39 -0500 Subject: [PATCH] added exercises --- exercises/_assignment4.mdwn | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/exercises/_assignment4.mdwn b/exercises/_assignment4.mdwn index 6c92b54a..0ff4b2c3 100644 --- a/exercises/_assignment4.mdwn +++ b/exercises/_assignment4.mdwn @@ -7,6 +7,41 @@ ω? 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 <~~> &Omegea;(Ω 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 -- 2.11.0