0
$\begingroup$

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)

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ This is great, thank you! $\endgroup$
    – Quelklef
    Jun 22, 2022 at 16:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.