Why we can not define factorial in lambda calculus

Question

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.

Answer 1

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.

Answer 2

$\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).