projects
/
lambda.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
history
|
raw
|
HEAD
Merge branch 'working'
[lambda.git]
/
exercises
/
_assignment4_answers.mdwn
1
1. Find a fixed point `X` for the succ function:
2
3
H := \f.succ(ff)
4
X := HH
5
== (\f.succ(ff)) H
6
~~> succ(HH)
7
8
So `succ(HH) <~~> succ(succ(HH))`.
9
10
2. Prove that `add 1 X <~~> X`:
11
12
add 1 X == (\mn.m succ n) 1 X
13
~~> 1 succ X
14
== (\fz.fz) succ X
15
~~> succ X
16
17
What about `add 2 X`?
18
19
add 2 X == (\mn.m succ n) 2 X
20
~~> 2 succ X
21
== (\fz.f(fz)) succ X
22
~~> succ (succ X)
23
24
So `add n X <~~> X` for all (finite) natural numbers `n`.
25
26
27