Go backward to Recursive Specifications Go up to Top Go forward to Double Recursion |
F = lambda f. lambda n. n equals zero -> one
[] n times (f(n minus one))
Simplification rule
fix F = F(fix F)
(fix F)(three)
= (F (fix F))(three)
= (lambda f. lambda n. n equals zero -> one
[] n times (f(n minus one))(fix F))(three)
= (lambda n. n equals zero -> one
[] n times (fix F)(n minus one))(three)
= three equals zero -> one
[] three times (fix F)(three minus one)
= three times (fix F)(two)
= three times (F (fix F))(two)
= ...
= three times (two times (fix F)(two))
Fixed point property justifies rec. unfolding!