# Why we can not define factorial in lambda calculus

I came across factorial semantics using lambda calculus:

$$fact = \lambda n. if(iszero~n) (1) (mult~n(fact(pred~n)))$$

I am not sure why the above does not make sense. Why we just can not keep substituting $$fact$$ please?

Other semanticss of $$if, iszero, mult, pred$$ are defined as follows:

\begin{align*} if = (\lambda n.n)\\ iszero = if~n==0~~then~~return~~True~~else~~return~~False~~end\\ mult = \lambda n.\lambda m. m (add~n) 0\\ add = \lambda n.\lambda m.\lambda f. \lambda x. nf(mfx)\\ pred~0 = 1 \end{align*}

Edit: it does not make sense as we can not use the function itself in its definition.

• Please edit your question to reveal precisely which portion does not make sense to you. The definition of factorial that you provided is functually/factually correct. You should provide the definition of factorial that you propose so that we can critique where it goes awry. Commented Feb 17, 2022 at 0:46
• @AndreasZUERCHER. Thank you. The teacher said, "you can not use the function itself in its definition". For me, I don't see why we can not do that?
– Avv
Commented Feb 17, 2022 at 1:32
• there exist 2 interpretations of what your teacher intended: 1) Your teacher was capriciously prohibiting all forms of recursion, especially tail recursion (which would be bizarre in this topic) or 2) Your teacher simply meant that you are prohibited from ricocheting off to invoke a preexisting library's factorial function. I suspect that your teacher meant #2 there, because the interpretation that you are taking (‘Your teacher is saying that it is factually incorrect to ever re-invoke the function in its definition.’) is likely not a lifelong lesson that your teacher was intending to teach. Commented Feb 17, 2022 at 1:43

The language doesn't really allow definitions of the form $$\text{name}=\textit{expr}$$. That's just a shorthand for readability. All of these definitions have to be eliminated by substitution to get a real λ-calculus term.

You can substitute the definition of $$\text{fact}$$ into itself, but the result will still have an occurence of $$\text{fact}$$ in it. No matter how many times you substitute, you can't get rid of the self-reference.

You can't substitute it infinitely many times to get an infinite term with "turtles all the way down". Terms have to be of finite length.

The usual solution is to introduce a fixed-point combinator to eliminate the self-reference. That's probably what your teacher will do next.

$$\lambda$$-calculus has a very restricted set of symbols. You can't refer to a variable by a variable name. You can't refer to something by itself in the definition because there is no way to "refer" to anything. There is only $$\lambda$$, $$.$$, well-balanced parentheses $$(,)$$ and a countably infinite number of variables (e.g. $$x,y,x_0,x_1,...$$). There is nowhere you can refer to another $$\lambda$$-term, let alone the term itself.

$$iszero = if~n==0~~then~~return~~True~~else~~return~~False~~end$$ is not the language of $$\lambda$$-calculus. It is a shorthand outside the language of $$\lambda$$-calculus for the $$\lambda$$-calculus term found by a certain composition of $$\lambda$$-calculus terms: $$True$$ is $$\lambda xy.x$$, $$False$$ is $$\lambda xy.y$$, etc.

If $$\text{fact}$$ was a $$\lambda$$-calculus term with length $$k$$ then $$\lambda n. if(iszero~n) (1) (mult~n(fact(pred~n)))$$ would have length $$>k$$, so the two could not possibly be the same set of symbols (they cannot be equal under $$\alpha$$-conversion). So, the $$=$$ in the equation must indicate equality under $$\beta$$-conversion (or even $$\beta\eta$$-conversion), and you have not defined a term in the $$\lambda$$-calculus if you have just specified its $$\beta$$ properties, not its literal symbolic definition (up to $$\alpha$$-conversion). Specifying what properties you want it to have is not acceptable, otherwise you could specify paradoxical properties.

You say in a comment that $$Y\equiv(\lambda x. \lambda y. y(xxy))(\lambda x. \lambda y. y(xxy))$$ "is calling itself twice", but no such thing is true. The RHS makes no reference to the variable $$Y$$. That it is the application of two identical $$\lambda$$-terms is not really relevant: it is a string that can be obtained by repeated applications of the variable rule ($$x,y$$ are $$\lambda$$-terms), application rule ($$xx,xxy,y(xxy),...$$ are $$\lambda$$-terms) and abstraction rule $$\lambda y.y(xxy),...$$ are $$\lambda$$-terms).