previous up next
Go backward to Recursive Specifications
Go up to Top
Go forward to Double Recursion
RISC-Linz logo

Factorial Function

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!


Author: Wolfgang Schreiner
Last Modification: November 5, 1997

previous up next