If you asked Landin to convert the imperative program Fact to declarative form he would write:
function Fact(n) {
function L(k, m) {
return (k==n) ? m : L(k+1,(k+1)*m)
}
return L(1, 1)
}
Notice that we have defined an auxiliary function L, inside Fact, which references the parameter n.
This doesn’t look like the declarative program Factorial we discussed, but now that it has a declarative form, it can be proven to be the same function as Factorial.
To prove Fact(n) == Factorial(n) we’ll first prove
Lemma: For a fixed n>0 and k>0,
L(k, Factorial(k)) == Factorial(n)
Proof: (by a backwards induction from n to 1)
Basis Step: k==n
L(n, Factorial(n))==(n==n) ? Factorial(n) : …
by the definition of L
== Factorial(n)
Induction Step: Assume for all i, n≥i>k, L(k,Factorial(k))==Factorial(n) (IH)
L(k,Factorial(k))
==L(k+1,(k+1)*Factorial(k))
by the definition of L
== L(k+1, Factorial(k+1))
by the definition of Factorial
== Factorial(n) by IH
QED
Theorem: Fact(n) == Factorial(n)
Proof:
Fact(n)== L(1,1) == Factorial(n) by the Lemma
QED