Something wrong with this definition of factorial with structural recursion? [closed]

In The Algebra of Programming page 5, the authors defined structural recursion foldn (c, h) over natural numbers:

f  0    = c
f (n+1) = h (f n)


They then went on to defin factorial as follows:

fact = outr . foldn ((0, 1), f)
outr (m, n) = n
f (m, n) = (m + 1, (m + 1) * n)


This doesn't seem right, first of all, foldn ((0, 1), f) does not comply to its definition, secondly, this fold will never terminate, will it?

• 1. Questions about code are normally off-topic for CS.SE (but might be on-topic for StackOverflow if you describe what you've tried to resolve this on your own). See our help center. 2. What have you tried? We expect you to put in a significant effort to solve the question on your own before asking. In this particular example, have you tried running it on a few examples? Seems like you should be able to very quickly resolve your own question by just running the code in a suitable interpreter on a few inputs and see whether it terminates or not and whether it produces the right answer. – D.W. Mar 5 '15 at 23:57
• These are not code, the are math equations. – qed Mar 5 '15 at 23:59
• @qed It is code, it's a (functional) program to compute the factorial function. Equations neither terminate nor fail to terminate, they are not expressions of computation. – Luke Mathieson Mar 6 '15 at 6:43

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 )
*Main> fact 0
1
*Main> fact 1
1
*Main> fact 2
2
*Main> fact 3
6
*Main> fact 4
24
*Main> fact 5
120


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)


so

fact 0 = (outr . foldn ((0, 1), f)) 0
= outr (foldn ((0, 1), f) 0)
= outr (0, 1)
= 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)
= 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.