This definition is correct. The syntax is almost Haskell code, so you can run it in a Haskell interpreter:
foldn (c, h) = g where
g 0 = c
g n = h (g (n - 1))
fact = outr . foldn ((0, 1), f)
outr (m, n) = n
f (m, n) = (m + 1, (m + 1) * n)
Usage in ghci:
Prelude> :load fact.hs
[1 of 1] Compiling Main ( fact.hs, interpreted )
Ok, modules loaded: Main.
*Main> fact 0
*Main> fact 1
*Main> fact 2
*Main> fact 3
*Main> fact 4
*Main> fact 5
I don't know what you mean by “
foldn ((0, 1), f) does not comply to its definition. If you mean that it's missing an argument, then this is not a problem. It's a function waiting to be applied.
foldn is a curried function: it takes an argument and returns a function, which itself takes an argument and returns something; this makes
foldn look like a function that takes two arguments (the first of which is a pair).
You can't evaluate
foldn ((0, 1), f) any further (except to replace it by an anonymous function for which there is no source syntax) because its definition is by case on its argument: there's no way to know which one of
g 0 = … or
g (n+1) = … to use until you know whether the argument is 0.
Once you pass an argument, you can evaluate the call.
foldn ((0, 1), f) 0 = (0, 1)
fact 0 = (outr . foldn ((0, 1), f)) 0
= outr (foldn ((0, 1), f) 0)
= outr (0, 1)
fact 1 = (outr . foldn ((0, 1), f)) 1
= outr (foldn ((0, 1), f) 1)
= outr (f (foldn ((0, 1), f) 0))
= outr (f (0, 1))
= outr (0 + 1, (0 + 1) * 1)
= outr (1, 1)
I'll let you work out other values by yourself.
The computation always terminates, regardless of the function
h (assuming only that
h terminates), by a simple induction argument: each nested call to
foldn is applied to a smaller integer. For any nonnegative parameter, eventually the argument will be 0 which does not involve recursion.