Self-application in Church's untyped lambda calculus

Question

In "Proposition as Types" by Philip Wadler mentions the weaknesses of untyped lambda calculus and "Russell's logic" concerning self-application.

Whereas self-application in Russell’s logic leads to paradox, self-application in Church’s untyped lambda calculus leads to non-terminating computations

I know that we can express a self-application in set theory as follow: E = {x | x $\notin$ x} but I am curious as to what it would look like in untyped lambda calculus?

I am not sure whether or not self-application refers to recursion or to another concepts and wasn't able to find an informal and direct clarification on the Internet.

In the case where the two concepts are the same, isn't the statement "self-application (recursion) leads to non-terminating computations" false?

Taking the example of the fixed point combinator theorem as defined in "Introduction to Lambda Calculus" by H.Barendregt and E.Barendsen:

• $\forall F \in \Lambda, \exists X \in \Lambda \ni FX = X$

• ($\exists Y \in \Lambda \ni Y \equiv \lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))\ni \forall F \in \Lambda, YF = FYF$

The Y-combinator seems to be a completely valid "self-application" in untyped lambda calculus.

Answer 1

It seems that self-application is indeed a synonym for "recursion". Philip Wadler mentions that untyped calculus can have a construct to allow self-application in which case it become possible to define recursive function although the Halting Problem remains to be non-terminating computation.

Untyped lambda calculus or typed lambda calculus with a construct for general recursion (sometimes called a fixpoint operator) permits the definition of any effectively computable function, but have a Halting Problem that is unsolvable.

The "fixedpoint operator" is the Y-Combinator defined in my original question. An example of non-terminating computation in untyped lambda calculus is the $\Omega$ combinator defined as follow in "The untyped $\lambda$-calculus by Manuel Eberl

$\omega := \lambda x. x x$

$\Omega := \omega \omega = (\lambda x. x x)(\lambda x. x x)$

where $\Omega \equiv (\lambda x. x x) \omega = \omega \omega$ etc...

Answer 2

Self-application is the application of a term to (a copy of) itself. Here are two examples:

1. $(\lambda x . x)(\lambda x. x)$
2. $(\lambda x . x x)(\lambda x . x x)$

The first examples applies the identity function $\lambda x . x$ to itself. It reduces in one step to the identity function, which is in normal form.

The second example applies the self-application function $\lambda x. x x$ to itself. It reduces in one step to a copy of the second example, which reduces in one step to a copy of the second example, etc. So this is an example of a nonterminating computation.

You are right that fixed-point combinators are another class of examples.

In the simply typed lambda calculus, the term $\lambda x . x x$ is ill-typed because we have to assign the same type to both bound occurrences of $x$. If we assign type $A$ to the second occurrence, we have to assign type $A \to A$ to the first occurrence to make the term well-typed. But $A$ and $A \to A$ cannot be the same, so the term cannot be well-typed.

Note that just because the second example is non-terminating in the untyped lambda-calculus, and ill-typed in the simply-typed lambda-calculus, doesn't mean it's not "valid". Many valid computer programs can have non-terminating behavior on purpose or by necessity, and maybe we want a mathematical theory of computation to model such programs. For example, a Web browser should only terminates if the user closes the window, but if the user never closes it, the browser should keep running forever.

This is an interesting difference between theories of truth (as in mathematical logic) and theories of computation (as in theoretical computer science): In a theory of truth, if something is not a valid proof of some truth, we don't really care for details. But in a theory of computation, if something doesn't terminate, we still might want to investigate the computational behavior that is shown while not terminating.