# Are there syntactic conditions on divergent $\lambda$-terms?

Probably the most famous example of a divergent term (ie, one which admits infinitely many $$\beta$$-reductions) in the $$\lambda$$-calculus is the Y combinator

$$Y = \lambda f. (\lambda x. f(xx)) (\lambda x. f(xx))$$

The kind of the "heart" of the recursion here is the inclusion of the subterm $$xx$$. I wondered if this is true in general; ie, if we have the theorem

$$E \text{ is a divergent \lambda-term} \implies E \text{ contains a subterm of the form } AA$$

(Note: $$A$$ can be any term, not just names as in $$A = x$$).

The answer is no. The following term reduces to itself (and thus diverges), but does not contain a subterm of the form $$AA$$.

\begin{align*} &(\lambda ab.bab) (\lambda ab.aba) (\lambda ab.bab) \\ \rightarrow_\beta& (\lambda b.b(\lambda ab.aba)b)(\lambda ab.bab) \\ \rightarrow_\beta& (\lambda ab.bab) (\lambda ab.aba) (\lambda ab.bab) \end{align*}

However, this term does contain the subterm $$bab$$, which although not of the form $$AA$$ is of the form $$AYA$$, which also looks suspicious.

Is there any such "syntactic" condition on divergent terms?

Here's a conjecture: if $$E$$ is a divergent $$\lambda$$-term, then $$E$$ contains a subterm $$S$$ of the form $$S = F A_1 A_2 \cdots A_n$$ where at least one $$A_i$$ contains $$F$$ as a subterm. That is, "for a term to be divergent, it must afford itself the possibility for a subterm $$F$$ to receive itself as an argument"

(The converse is false, as $$(\lambda x.xx)(\lambda a.a)$$ satisfies this via inclusion of $$xx$$ but does not diverge)

This is essentially the criterion used by type systems to avoid divergence. Take, for instance, the simply typed lambda calculus. In order for $$f\ x$$ to be well typed, we must have:

$$f : T → U \\ x : T$$

In order for $$f\ f$$ to be well typed, it would have to be the case that:

$$T = T → U$$

But types are required to be inductively generated by $$→$$ and some base types, so there is no type that satisfies this equation. Similarly, in order for $$f$$ to receive itself as an argument at all, it would have to be the case that:

$$T = \cdots → T → \cdots$$

which is not allowed.

More elaborate type systems can allow some cases of self-application without enabling divergence. For instance, in the polymorphic lambda calculus, we can write:

$$λ(f : ∀T. T → T). f_{∀T. T → T}\ f$$

In this case, it is safe because $$f$$ can only be the identity function. Or, even more precisely, intersection types allow cases of self-application like so:

$$λ(f : T \cap (T → U)). f f$$

and these sort of intersection types classify exactly the normalizing lambda terms. I suspect the intuition is that for any normalizing term involving self-application, only finitely many unfoldings of the $$T = \cdots → T → \cdots$$ equation are necessary, and can be expressed by a finite intersection, while the diverging terms genuinely require an infinite type that cannot be sufficiently approximated by any finite intersection.

• This is great, thank you! Jun 22, 2022 at 16:08