Go backward to Double Recursion Go up to Top Go forward to While Loops |
f, g: Nat -> Nat_|_
f = lambda x. x equals zero -> g(zero)
[] f(g(x minus one)) plus two
g = lambda y. y equals zero -> zero
[] y times f(y minus one)
T = Nat -> Nat_|_
F: (T × T) -> (T × T)
F = lambda (f,g).(..., ...)
F0(_|_) = ({}, {})
F1(_|_) = ({}, {(zero, zero)})
F2(_|_) = ({(zero,zero)}, {(zero, zero)})
...
F5(_|_) = ({(zero,zero), (one, two), (two, two)},
{(zero, zero), (one, zero),
(two, four), (three, six)})
Fi(_|_) = F5(_|_), i>5
fix(F) = (f,g)