Go backward to Partial Functions Go up to Top Go forward to Functional and Fixed Point |
fac0 = lambda n. _|_
faci+1 = lambda n. n equals zero -> one
[] n times faci(n minus one)
Recursive specification can be understood in terms of a family of non-recursive ones.
"Functional" F
F: (Nat -> Nat_|_) -> (Nat -> Nat_|_)
F = lambda f. lambda n. n equals zero -> one
[] n times f(n minus one)
Each subfunction is an instance of the functional!