previous up next
Go backward to Double Recursion
Go up to Top
Go forward to While Loops
RISC-Linz logo

Simultaneous Definitions

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)


Author: Wolfgang Schreiner
Last Modification: November 5, 1997

previous up next