Barendregt’s Theory of the $𝝀$-Calculus, Refreshed and Formalized

Partial recursive functions (shortened to PRFs) are based on the undefined value $\perp$, that induces the extensional preorder $f{\le }_{\text{prf}}g$ holding when $\forall n\in \mathrm{\mathbb{N}},f(n)=\perp$ or $f(n){=}_{\mathrm{\mathbb{N}}}g(n)$, having as minimum the everywhere undefined function $f_{\perp }(n)≔\perp$.

PRFs and the $\lambda$-calculus can represent each other. Moving to the $\lambda$-calculus provides dynamic computations, which yield different syntactic implementations of functions that – extensionally – do the same thing. Barendregt’s theory of the $\lambda$-calculus is based on the idea of studying the semantics – that is, the equational theory – induced on $\lambda$-terms by the representation of the extensional order on PRFs.

One of the first choices to make is how to represent undefinedness [64, 14, 16]. Intuitively, it corresponds to divergence. In the untyped $\lambda$-calculus, the paradigmatic never-ending computations is $\mathrm{\Omega }≔(\lambda x.xx)(\lambda x.xx)$, that rewrites to itself in one $\beta$-step. It is clear that $\mathrm{\Omega }$ is a representation of the everywhere undefined function $f_{\perp }$. What is less clear is the criterion that establishes when a given term is meaningless, that is, when it represents the undefined.

Identifying meaningless terms goes hand in hand with the study of program equivalences and equational theories: which $\lambda$-terms should be considered equivalent? A good criterion to validate a notion of meaningless term is collapsibility, that is, whether the equational theories that identify all those terms are consistent, that is, do not equate all terms.

It is natural to define as meaningless all the $\beta$-divergent terms. It turns out, however, that they are not collapsible: equational theories identifying $\beta$-divergent terms are inconsistent; this is the starting point of Barendregt’s theory. We provide a formalization of the simple standard proof of this fact, in Sect. 3. An intuition as to why this identification cannot work is that fixpoint combinators, that allow the encoding of recursion (and the minimization of PRFs) in the $\lambda$-calculus, are all $\beta$-divergent.

Barendregt and Wadsworth hence introduced a notion of meaninglessness based on divergence for a sub-reduction of $\beta$, namely head reduction. Restricting the rewriting rule restricts the set of meaningless term. Going back to our example, fixpoint combinators terminate for head reduction, while $\mathrm{\Omega }$ does not.

A number of results in Barendregt’s book focus on showing that the choice of head divergent as meaningless is a good one. In particular, he gives two proofs of their collapsibility, one considering $\mathscr{H}$, the minimal equational theory identifying head divergent terms, and one considering (head) contextual equivalence ${\simeq }_{𝒞}$ (also known as ${\mathscr{H}}^{\ast }$). Both collapsibility proofs are based on the crucial genericity lemma. For ${\simeq }_{𝒞}$, he also proves maximality: ${\simeq }_{𝒞}$ is the maximal consistent equational theory identifying head divergent terms.

The goal of the paper is to prove the collapsibility theorem, moderninizing and simplyfing the theory leading to it. For that, we choose the proof of collapsibility based on contextual equivalence, given the prominence that this concept has – along the decades – achieved in the study of programming languages. Additionally, we also prove the maximality theorem for ${\simeq }_{𝒞}$. Along the way, we formalize many theorems of Barendregt’s theory (confluence, standardization, head factorization, head normalization, solvability, genericity, and ${\simeq }_{𝒞}$ is an equational theory), but do so mostly without using their original proofs in the book [15]. We use several revisitations by Accattoli et al. [8], Takahashi [57], and Accattoli and Lancelot [9] that allow for easier, self-contained proofs.

We also adopt a different, strictly more general definition of head reduction – following Accattoli and Dal Lago [7] – that however validates the same properties with the same proofs. Additionally, we deal with the contextual preorder ${\precsim }_{𝒞}$ rather than with contextual equivalence, and more generally deal with inequational theories. Lastly, our formalization work contributes some revisitations of its own, mentioned below.

For the formalization, we rely on the Abella proof assistant [28, 12]. Our formal proofs faithfully follow the pen-and-paper ones in the cited papers. This is partly due to Abella’s primitive support for binders and for Miller and Tiu’s $\nabla$ (nabla) quantifier [46, 29], that allows a smooth treatment of free variables, but it is also due to the careful details provided in the neat pen-and-paper proofs we try to mimic.

The only point where there is a gap between the formalization and pen-and-paper reasoning is the treatment of contexts, in particular for contextual equivalence. Plugging in contexts is a variant of meta-level substitution that can capture variables, and that it is not primitively supported by Abella. Therefore, we represent contexts indirectly, via sub-term predicates: we represent $C⟨t⟩$ saying that $t$ is a sub-term of $u=C⟨t⟩$, see sections 6 and 9.

For the theory, the main contribution of our formalization concerns the genericity lemma. In a nutshell, genericity states that the contextual closure is monotone (with respect to the contextual preorder ${\precsim }_{𝒞}$) on meaningless terms, i.e. if $\perp {\precsim }_{𝒞}t$ then $C⟨\perp ⟩{\precsim }_{𝒞}C⟨t⟩$. While the statement is natural, its proofs are usually involved; it rather deserves to be referred to as theorem. Barendregt originally used a topological argument [15, Prop. 14.3.24] but other arguments exist in the literature: via intersection types by Ghilezan [31], rewriting-based ones by Takahashi [57], Kuper [39], Kennaway et al. [37], and Endrullis and de Vrijer [25], and via Taylor expansion by Barbarossa and Manzonetto [13].

We follow Takahashi’s rewriting-based technique – and, more precisely, its revisited presentation by Accattoli and Lancelot [9] – because it is self-contained and relies on other theorems we already prove (the head normalization one). To formalize Takahashi’s argument, we isolate two new concepts: a disentangling lemma (Lemma 14) turning context plugging into meta-level substitutions up to $\beta$-reduction, and a corollary of the head normalization theorem (Cor. 12) that encapsulates the rewriting argument in the proof of genericity.

As an high-level by-product, we show that the disentangling lemma in fact leads to a new notion of substitutions equivalence that is equivalent to contextual equivalence and does not mention contexts – it is the distilled essence of Takahashi’s argument. We believe it to be an interesting contribution, perhaps the main take-away from our formalization effort.

Formalizations of the $\lambda$-calculus abound. There are countless formalizations of confluence (e.g. [49, 54, 56, 52, 35, 63, 34, 48, 62, 66]), and some go further, dealing with standardization (e.g. McKinna and Pollack [43], Norrish [50], Crary [22], Guidi [33], Gheri and Popescu [30]) but we are not aware of any previous work dealing with the more advanced theorems we treat here (such as solvability, genericity, collapsibility, maximality). Larchey-Wendling formalizes in Coq good portions of Krivine’s book on the $\lambda$-calculus [38]; the Coq sources are available [41], but there is no associated paper. Norrish formalizes in HOL4 the relationship between PRFs and the $\lambda$-calculus [51].

Independently and in parallel to us, Norrish and Tian [59] formalized in HOL4 both the operational characterization of solvability (that we also formalize) and a restricted form of Böhm’s separation theorem. Böhm’s theorem is a very challenging result to mechanize; Norrish and Tian’s development is the first formalized proof of a separation result. Their work appears in the very same conference of this paper.

There are also many formalizations of techniques for program equivalence: e.g., for coinductive operational program equivalences in Coq by Biernacki et al. [18] and in Abella by Momigliano [47], equational theories for call-by-(push-)value in Coq by Rizkallah et al. [55], and for call-by-push-value in Coq (and partially in Abella) by Forster et al. [26, 27].

Our formal revisited results for the $\lambda$-calculus are similar in spirit to those in Accattoli [4] (cube property) and Accattoli et al. [5] (translation of $\lambda$ into the $\pi$-calculus).

They can be found on GitHub [40].

Abella [28, 12] belongs to the family of proof assistants based on higher-order abstract formalisms – namely, the one adopted by Abella is Miller and Nadathur’s $\lambda$-tree syntax [45] – which provides primitive support for binders and meta-level substitution. We assume basic familiarity with these formalisms. A survey by Kaiser et al. compares Coq, Abella, and Beluga by studying System F in the three frameworks [36].

Abella has two layers, the specification level and the reasoning level. They are based on different logics, the reasoning level being more powerful and provided with special tactics to reason about the specification level. In particular, it is only at the reasoning level that one can use Miller and Tiu’s $\nabla$ (nabla) quantifier [46, 29], that complements the primitive support for binders with a smooth treatment of free variables.

In many formalizations in Abella, definitions are given at the specification level while statements and proofs are given at the reasoning level. In particular, this is often done when formalizing typed calculi, since Abella provides some tactics for the involved typing contexts at the specification level. We follow another approach, giving the definitions at the reasoning level, which is sometimes preferred when formalizing untyped calculi. One of the reasons is that in this way we can exploit $\nabla$ to formalize terms with free variables, obtaining definitions, statements, and reasoning that are closer to those with pen-and-paper. The same approach is used also (at least) by section 7.3 of the Abella tutorial by Baelde et al. [12], Tiu and Miller [60], Accattoli [4], Chaudhuri et al. [21], and Accattoli et al. [5].

On paper, $\lambda$-terms are defined inductively, starting from a set of variables and via the abstraction and the application constructors:

On paper, we shall follow the standard conventions that application is left associative and has precedence over abstractions, so that $\lambda x.tus$ denotes $\lambda x.((tu)s)$.

In Abella, it is standard to define $\lambda$-terms via a type tm and two constructors $\mathrm{𝚊𝚙𝚙}$ and $\mathrm{𝚊𝚋𝚜}$ for applications and abstractions, without specifying variables, as in Fig. 1 (left).

Note that $\mathrm{𝚊𝚋𝚜}$ takes an argument of type $\text{tm}\to \text{tm}$ which is how Abella encodes binders. More precisely, an object-level binding constructor such as $\lambda x.t$ is encoded via a pair: an ordinary constructor $\mathrm{𝚊𝚋𝚜}$ applied to a meta-level abstraction of type $\text{tm}\to \text{tm}$. For example, the term $\lambda x.xx$ that binds $x$ in the scope $xx$ is encoded as $\mathtt{abs\; x\backslash \; app\; x\; x}$ (that is parsed as $\mathtt{abs\; (x\backslash \; app\; x\; x)}$) where $\mathtt{x\backslash \; app\; x\; x}$ is a meta-level abstraction of type $\text{tm}\to \text{tm}$ in the syntax of Abella. In the rest of the paper, with an abuse of terminology, we call binders such terms of type $\text{tm}\to \text{tm}$.

Reasoning by induction on the structure of tm terms is not possible in Abella because of the open world assumption, stating that new constructors can always be added later to any type. Thus, one rather defines an additional tm predicate, as in Fig. 1 (right), which is added to the hypotheses of statements whenever one needs to reason by induction on terms. The first clause of the tm predicate uses nabla to say that the free variable $𝚡$ is a term. Variables with capitalized names in the last two clauses are implicitly quantified by $\forall$ at the clause level. The second clause states that an abstraction $\mathtt{abs\; T}$ is a term if its body is a term. The body is obtained applying the binder $𝚃$ (of type $\text{tm}\to \text{tm}$ ) to a fresh variable $𝚡$ to obtain a term of type tm. Such application corresponds in a pen-and-paper proof to the (usually implicit) logical step that replaces the bound variable with a fresh one.

The primitive support for substitution of Abella shows up in the following definition of $\beta$-reduction, where $t\{x\leftarrow u\}$ is the capture-avoiding meta-level substitution of $u$ for all the occurrences of $x$ in $t$, represented in Abella simply with $\mathtt{T\; U}$ where $𝚃$ is a binder.

We shall repeatedly use the confluence property of $\beta$-reduction, that is, the following statement.

This is possibly the theorem with the highest number of formalized proofs. We provide one following the standard Tait–Martin-Löf technique based on parallel $\beta$-reduction ${\Rightarrow }_{\beta }$, defined as follows, and to which we shall come back to in Sect. 5:

An equational theory for the $\lambda$-calculus is an equivalence relation that contains $\beta$ and is compatible (a property also referred to as context-closure or compositionality). We shall rather work with inequational theories, simply obtained by starting with a preorder rather than an equivalence, as they carry enough information and avoid duplications of symmetric proofs.

The smallest (in)equational theory is $\beta$-conversion, that is, the transitive, reflexive and symmetric closure of $\beta$-reduction.

In rewriting theory, normal forms are the results of the rewriting computational process. When using $\lambda$-terms to represent partial recursive functions (shortened to PRFs), it is tempting to consider $\beta$-normal forms as results and $\beta$-diverging terms as representing the special undefined value $\perp$ of PRFs. From an equational point of view, this means considering the (in)equational theory that identifies all $\beta$-diverging terms. It turns out that such a natural approach does not work because any such (in)equational theory is inconsistent, as the closure properties of theories end up identifying all terms.

Consider the term $s_r≔(\lambda y.yr\mathrm{\Omega })(\lambda z.\lambda w.z)$ parametric in $r$, where $\mathrm{\Omega }≔(\lambda x.xx)(\lambda x.xx)$ is the paradigmatic $\beta$-divergent term. Note that $s_r{\to }_{\beta }^{\ast }r$. Then note that $t{\le }_{ℛ}{s}_t{\le }_{ℛ}{s}_u{\le }_{ℛ}u$ for any two terms $t$ and $u$, because $ℛ$ contains $\beta$ and $s_r$ is $\beta$-divergent for any $r$. $◀$

The traditional notion of head reduction ${\to }_{𝚑}$ is defined as follows:

For formalizing it, one needs an inductive definition, which is easily obtained, as follows:

Traditional head reduction is a deterministic rewriting rule. When it exists, the head redex is the leftmost-outermost $\beta$-redex.

The second clause in (2) is somewhat ugly. One might wonder what happens if one adopts the following more elegant definition of head reduction – to be referred to as refreshed here – as done by Accattoli and Dal Lago [7]:

Strictly speaking, the refreshed definition is not equivalent because it is more liberal: it defines a non-deterministic rewriting rule. For instance, one has the refreshed head step $r≔(\lambda x.(\lambda y.t)u)s{\to }_{𝚑}(\lambda x.t\{y\leftarrow u\})s$ besides the traditional one $r{\to }_{𝚑}((\lambda y.t)u)\{x\leftarrow s\}$.

It turns out, however, that – beyond determinism – the refreshed definition preserves all the properties of traditional head reduction. In particular, it induces the same sets of head terminating and diverging terms, and the same notion of head normal form. And it actually verifies a relaxed form of determinism, as discussed below.

In this work, we adopt the refreshed definition to show that it can indeed replace the traditional one in Barendregt’s theory. We actually developed the whole formalization with respect to both definitions. There is only one point where the difference has a minimum impact, we shall point it out.

The formalization forces to clarify that there are two predicates for head normal forms, often confused in pen-and-paper proofs. The dynamic, or rewriting one simply says that ${\to }_{𝚑}$ does not apply. The static one is an inductive description of head normal forms, via the auxiliary notion of rigid term, and is modeled on the following grammar.

Our formalization uses repeatedly the following easy stability of head normal forms.

In fact, not only refreshed head reduction is confluent, it actually has the stronger diamond property: according to Martini and Dal Lago [23], a relation ${\to }_{𝗋}$ is diamond if $u_1{}_{𝗋}{}^{}\leftarrow t{\to }_{𝗋}{u}_2$ imply $u_1=u_2$ or $u_1{\to }_{𝗋}s{}_{𝗋}{}^{}\leftarrow u_2$ for some $s$¹¹1Note that this formulation of the diamond property is weaker than the one for parallel $\beta$-reduction ${\Rightarrow }_{\beta }$ at work in the Tait–Martin-Löf proof of confluence (which does not have “$u_1=u_2$ or”). This is because ${\Rightarrow }_{\beta }$ is reflexive (that is, $t{\Rightarrow }_{\beta }t$ for any term $t$), thus it does not need that refinement, which is instead mandatory for non-reflexive reductions such as head reduction.. If ${\to }_{𝗋}$ is diamond then ${\to }_{𝗋}$ is confluent and moreover:

1. 1.

   Length invariance: all evaluations to normal form with the same start term have the same length (i.e. if $d:t{\to }_{𝗋}^{\ast }u$ and $d^{\prime }:t{\to }_{𝗋}^{\ast }u$ with $u$ ${\to }_{𝗋}$-normal then $|d|=|d^{\prime }|$);

2. 2.

   Uniform normalization: $t$ is weakly ${\to }_{𝗋}$-normalizing – or simply terminating – if and only if it is strongly ${\to }_{𝗋}$-normalizing.

Essentially, the diamond property captures a more liberal form of determinism.

For (refreshed) head reduction, we formalize the diamond property and the length invariance and uniform normalization corollaries. In fact, these properties are never used after this section, apart from the important fact that we implicitly rest on uniform normalization for using weak normalization as the termination property of reference for head reduction.

The proof of uniform termination is the only place where adopting refreshed head reduction requires slightly more work: for traditional head reduction, it is an immediate consequence of determinism, while in the refreshed case it has to be proved by induction on the number of head steps using the diamond property.

The statement of the head normalization theorem has three subtleties. Firstly, because of the non-determinism of our refreshed head reduction, the conclusion of the general rewriting formulation of normalization would ask for strong normalization of ${\to }_{𝚑}$ on $t$. Because of uniform normalization, we can simplify it as termination of ${\to }_{𝚑}$. Secondly, $t$ might ${\to }_{\beta }$-reduce to a term in ${\to }_{𝚑}$-normal form in many different ways, possibly without using ${\to }_{𝚑}$, so that the hypotheses do not immediately imply that ${\to }_{𝚑}$ terminates. Thirdly, the conclusion is “${\to }_{𝚑}$ terminates on $t$” and not $t{\to }_{𝚑}^{\ast }u$, because in general maximal ${\to }_{𝚑}$-sequences from $t$ all end on the same term $s$ but it might be that $s\ne u$. For instance, let $𝙸≔\lambda y.y$: then $𝙸(x(\mathrm{𝙸𝙸})){\to }_{\beta }𝙸(x𝙸){\to }_{\beta }x𝙸$ is a ${\to }_{\beta }$-sequence to head normal form, and yet the unique maximal ${\to }_{𝚑}$-sequence $𝙸(x(\mathrm{𝙸𝙸})){\to }_{𝚑}x(\mathrm{𝙸𝙸})$ ends in a different term.

Following Accattoli et al. [8], there is a very simple abstract proof of head normalization based on two properties. To state them, we need (refreshed) non-head reduction ${\to }_{\neg 𝚑}$, given by (traditional ${\to }_{\neg 𝚑}$ – sometimes called internal – has an additional clause, see [8]):

The two properties then are (where $\cdot$ denotes the concatenation of rewriting relations):

1. 1.

   Persistence: if $t{\to }_{𝚑}u$ and $t{\to }_{\neg 𝚑}s$ then $s{\to }_{𝚑}r$ for some $r$;

2. 2.

   Factorization: if $t{\to }_{\beta }^{\ast }u$ then $t{\to }_{𝚑}^{\ast }\cdot {\to }_{\neg 𝚑}^{\ast }u$.

Intuitively, persistence states that non-head steps cannot erase head steps. Its proof is straightforward.

Factorization expresses the fact that head reduction is more important than its complement; it is a non-trivial theorem. To appreciate the result, note that the opposite factorization does not hold, that is, one cannot have $t{\to }_{\neg 𝚑}^{\ast }\cdot {\to }_{𝚑}^{\ast }u$. For instance, the sequence:

cannot be re-organized as to have the ${\to }_{\neg 𝚑}$ step before the ${\to }_{𝚑}$ step.

We provide two proofs of factorization (inducing two proofs of head normalization), one as a corollary of the standardization theorem and one based on parallel reduction.

Standardization is another classic operational theorem. It is a complex, hard to grasp rewriting topic, the full appreciation of which requires technical concepts such as residuals. For the $\lambda$-calculus, there exist simple treatments of standardization based on Plotkin’s approach [53] (originally desgined for the call-by-value $\lambda$-calculus) that succeed in hiding all the technicalities. Our formalization of standardization is the adaptation to the reasoning level of Abel’s Abella development [1], who builds on Loader [42], who builds on Xi [67], who, in turn, builds on Plotkin.

The theorem states that every reduction sequence can be re-organized into a special standard form. Plotkin’s technique stems from the existence in the $\lambda$-calculus of a very simple inductive definition of standard sequence, given here in refreshed form.

Our definition of standard sequence is slightly different from Abel’s (and most treatments of standardization) as we use refreshed head reduction in the fourth clause, while he uses weak (i.e. not under abstraction) head reduction, which is deterministic. Our approach changes the notion of standard sequence: for instance, $(\lambda x.(\lambda y.t)u)s{\to }_{𝚑}(\lambda x.t\{y\leftarrow u\}){\to }_{𝚑}t\{x\leftarrow u\}\{x\leftarrow s\}$ is a standard sequence for us, while traditionally is not. Technically, standard sequences in our case are not unique, or, equivalently, we are standardizing with respect to a partial order on redexes (rather than the total leftmost-outermost order). The theory of standardization for partial orders is complex [32, 44, 6]. Our proof of standardization, however, is remarkably simple: it follows exactly the structure of Abel’s, and it is actually even simpler, since moving definitions to the reasoning level removes the need of a few lemmas. ^††margin: The implication is
proved in 05-3-head
_factorization.thm Additionally, our theorem implies factorization exactly as the traditional standardization one.

Takahashi [58] gives an original proof of head factorization based on parallel $\beta$-reduction ${\Rightarrow }_{\beta }$, similarly to the famous Tait–Martin-Löf proof for confluence. Accattoli et al. [8] revisit Takahashi’s work, simplifying her proof technique. In particular, they identify two abstract properties of parallel $\beta$ with respect to head reduction – the merge and split properties below – from which factorization easily follows, similarly to how confluence follows from the diamond property for ${\Rightarrow }_{\beta }$.

We have formalized their proof, and refer to their paper for extensive discussions, here we only provide a quick overview. The formalization follows their pen-and-paper proofs faithfully. The slight difference, again, is that we adopt the refreshed definition of head reduction, while in [8] they work with the traditional one. Beyond the already discussed refreshed non-head reduction ${\to }_{\neg 𝚑}$, we also need its parallel variant ${\Rightarrow }_{\neg 𝚑}$ defined as follows (traditional ${\Rightarrow }_{\neg 𝚑}$ has an additional clause):

The proof of factorization is based on the following three properties, the first of which is simply the basic requirement for parallel reductions:

• $\mathrm{■}$

  Parallel: ${\to }_{\neg 𝚑}\subseteq {\Rightarrow }_{\neg 𝚑}\subseteq {\to }_{\neg 𝚑}^{\ast }$;

• $\mathrm{■}$

  Merge: if $t{\Rightarrow }_{\neg 𝚑}\cdot {\to }_{𝚑}u$ then $t{\Rightarrow }_{\beta }u$;

• $\mathrm{■}$

  Split: if $t{\Rightarrow }_{\beta }u$ then $t{\to }_{𝚑}^{\ast }\cdot {\Rightarrow }_{\neg 𝚑}u$.

The parallel and merge properties are easily proved. Split instead is tricky. Accattoli et al. show that it can be proved easily by considering the following refinement ${\stackrel{𝑛}{\Rightarrow }}_{\beta }$ of parallel $\beta$-reduction ${\Rightarrow }_{\beta }$, where the index $n\in \mathrm{\mathbb{N}}$ intuitively denotes the number of ordinary $\beta$-steps done in parallel by the underlying ${\Rightarrow }_{\beta }$ step, and ${|t|}_x$ (used in the fourth clause) is the number of occurrences of $x$ in $t$:

The key property of ${\stackrel{𝑛}{\Rightarrow }}_{\beta }$ is its substitutivity, which is proved by decorating with indices the standard proof of the underlying substitutivity property for ${\Rightarrow }_{\beta }$ (which is used in Tait–Martin-Löf’s proof of confluence).

The formalization of this proof is faithful to Accattoli et al.’s pen-and-paper proof. The slightly annoying aspect is that it requires basic arithmetical properties for manipulating the indices, and Abella has no arithmetical library. Thus, we had to prove them all by hand.

To define solvability, we need to concept of (refreshed) head contexts $H$, defined inductively by $H≔⟨\cdot ⟩\mid Hu\mid \lambda x.H$, together with the standard plugging operation $H⟨t⟩$ of a term $t$ in a context (here $H$), which might involve capture of free variables; for instance, $(\lambda x.⟨\cdot ⟩u)⟨xy⟩=\lambda x.xyu$.

Such a characterization is of a rewriting nature, but not of $t$ in isolation, rather of $t$ with respect to a head context. The idea is that the head context can decompose $t$ into pieces and leave nothing, that is, it can (dis)solve it. The requirement of a head context $H$ (rather than a general context $C$) forces that contexts cannot simply erase $t$ and replace it with the identity (a context taking such shortcut is $C≔(\lambda x.𝙸)⟨\cdot ⟩$, but it is not a head context), they rather have to dissolve $t$ by interacting with its internal structure.

Solvability shows that there are two kinds of strong (that is, all paths) divergence:

• $\mathrm{■}$

  Unremovable strong divergence, that is, strong divergence that cannot be removed by a head context. The looping term $\mathrm{\Omega }$ is of this kind, because no head context can erase it.

• $\mathrm{■}$

  Removable strong divergence, that is, sub-terms that are strongly divergent but that they appear in argument position and thus can be removed by a head context. For instance, $\mathrm{\Omega }$ in $x\mathrm{\Omega }$ is removable by the head context $(\lambda x.⟨\cdot ⟩)(\lambda y.𝙸)$; note that it happens in Prop. 4.

Unremovable strong divergences have to be considered as loops, or undefined terms. On the other hand, terms with removable strong divergences should not be considered in the same way, as there are some scenarios/interactions in which their divergence gets removed.

To formalize the definition of solvability, we shall find some way of formalizing contexts in Abella. Unfortunately, there is no way of having a direct, first-class representation because plugging can capture free variables: there is no primitive support for it in Abella, nor it can be defined by the user, as it goes against the treatment of free variables in Abella. The workaround is building a predicate head_ctx of type $\text{tm}\to \text{tm}\to \text{prop}$ such that $\text{head\_ctx}tu$ holds if there exists a head context $H$ such that $H⟨t⟩=u$; thus one is actually stating that $t$ is a head sub-term of $u$. The predicate is easily defined inductively, breaking down the structure of the context construct by construct.

The characterization of solvability (Thm. 11) has two directions. Proving that head normalizing terms are solvable requires to refine the static predicates for head normal forms with information about the head variable (whether it is free, and, in case, which one is it). The solving context is then built by induction on the refined predicates by substituting on the head variable $x$ a term erasing all the arguments of $x$ and leaving the identity, plus providing dummy arguments for extra head abstractions, if any.

Proving that solvable terms are head terminating requires a big tool. The fact that ${\to }_{\beta }$ appears in the definition of solvable means we need to use head normalization (Thm. 7). Then, what remains to show is the easy fact that, if $H⟨t⟩$ is head normalizing, then so is $t$.

Genericity has recently been revisited by Accattoli and Lancelot [9] who identify a simpler alternative statement, dubbed light genericity, while they refer to Barendregt’s statement as heavy. They show that the light version is enough for the main aim of genericity, that is, proving the collapsibility of head diverging terms. The two statements follow:

• $\mathrm{■}$

  Light genericity: let $u$ be ${\to }_{𝚑}$-divergent and $C$ be a context such that $C⟨u⟩$ is ${\to }_{𝚑}$-normalizing. Then, $C⟨t⟩$ is ${\to }_{𝚑}$-normalizing for all $t$.

• $\mathrm{■}$

  Heavy genericity: let $u$ be ${\to }_{𝚑}$-divergent and $C$ be a context such that $C⟨u⟩{\to }_{\beta }^{\ast }n$ with $n$ $\beta$-normal. Then, $C⟨t⟩{\to }_{\beta }^{\ast }n$ for all $t$.

The proofs of the genericity properties that we shall develop are based on the head normalization theorem. Actually, we rather use the following strengthened corollary (its proof uses confluence as well), the isolation of which is a contribution of this paper. It shall provide very compact and elegant proofs of genericity.

Accattoli and Lancelot give a proof of light genericity obtained by adapting and polishing Takahashi’s one for heavy genericity, from her two-page long paper titled a simple proof of the genericity lemma [57]. The technique is based on:

1. 1.

   Substitutions: factoring the statement via an auxiliary one based on substitutions instead of contexts, as substitutions interact nicely with reduction;

2. 2.

   Trick: reducing contexts to substitutions via a closure of the plugged term, and transferring termination between the two via a reasoning that is here encapsulated in the extended head normalization property above.

We formalize the proofs of both light and heavy genericity. The difficulty is formalizing Takahashi’s trick, recalled next by adapting Accattoli and Lancelot’s proof using Cor. 12.

1. 1.

   See [9]. In fact, [9] uses head normalization, our Abella proof does not.

2. 2.

   [Takahashi’s trick] Let $\mathrm{𝚏𝚟}(u)\cup \mathrm{𝚏𝚟}(s)=\{x_1,\mathrm{\dots },x_k\}$, and $y$ be a variable fresh with respect to $\mathrm{𝚏𝚟}(u)\cup \mathrm{𝚏𝚟}(s)\cup \mathrm{𝚏𝚟}(C)$ and not captured by $C$. Note that $\overline{u}≔\lambda x_1.\mathrm{\dots }\lambda x_k.u$ is a closed term. Consider $t≔C⟨y{x}_1\mathrm{\dots }{x}_k⟩$, and note that:

   $$\begin{array}{cccccc}t\{y\leftarrow \overline{u}\}=C⟨\overline{u}{x}_1\mathrm{\dots }{x}_k⟩=C⟨(\lambda x_1.\mathrm{\dots }\lambda x_k.u)x_1\mathrm{\dots }{x}_k⟩{\to }_{\beta }^{k}C⟨u⟩.\hfill & & & & & \end{array}$$

   (4)

   The fact that $u$ is head divergent implies that $\overline{u}$ is head divergent. Similarly, take $\overline{s}≔\lambda x_1.\mathrm{\dots }\lambda x_k.s$ and note that $t\{y\leftarrow \overline{s}\}{\to }_{\beta }^{\ast }C⟨s⟩$. By extended normalization (Cor. 12), $C⟨u⟩$ head terminating implies that so is $t\{y\leftarrow \overline{u}\}$. By genericity as substitution, $t\{y\leftarrow \overline{s}\}$ is head terminating. By extended normalization (Cor. 12), $C⟨s⟩$ is head terminating.

$◀$

During the formalization process, we went back and forth with multiple phrasings of Takahashi’s trick. The difficulty is formalizing the argument for (4), which relies on knowing the set of free variables of a term – unproblematic on paper but tricky in Abella – and then uses many abstractions and applications at once. Our attempts led us to the following disentangling lemma that neatly isolates the idea with respect to a single term, avoiding the set of free variables of the term and the $k$-ary notations.

In fact, the proof of the lemma collects – one at at time – all the variables captured by the context, rather than all the free variables of the plugged term.

By induction on $C$. Cases:

• $\mathrm{■}$

  Empty, i.e. $C=⟨\cdot ⟩$. Pick any $x$, the statement holds with respect to $t_C≔x$ and $u_C≔u$.

• $\mathrm{■}$

  Abstraction, i.e. $C=\lambda y.C^{\prime }$. By i.h., there exists $t_{C^{\prime }}$ and $x^{\prime }\notin \mathrm{𝚏𝚟}(C^{\prime })$ such that for all $u$, there exists $u_{C^{\prime }}$ such that $t_{C^{\prime }}\{x^{\prime }\leftarrow u_{C^{\prime }}\}{\to }_{\beta }^{\ast }{C}^{\prime }⟨u⟩$ and if $u$ is head divergent then so is $u_{C^{\prime }}$. Then let $x$ be a fresh variable and set $t_C≔\lambda y.t_{C^{\prime }}\{x^{\prime }\leftarrow xy\}$ and $u_C≔\lambda y.u_{C^{\prime }}$. Note that $u_C$ is head divergent if $u_{C^{\prime }}$ is, and that:

  Where the first ${\to }_{\beta }^{\ast }$ is obtained via a standard substitution lemma.

• $\mathrm{■}$

  Application left, i.e. $C=C^{\prime }r$. By i.h., there exists $t_{C^{\prime }}$ and $x^{\prime }\notin \mathrm{𝚏𝚟}(C^{\prime })$ such that for all $u$, there exists $u_{C^{\prime }}$ such that $t_{C^{\prime }}\{x^{\prime }\leftarrow u_{C^{\prime }}\}{\to }_{\beta }^{\ast }{C}^{\prime }⟨u⟩$ and if $u$ is head divergent then so is $u_{C^{\prime }}$. Pick $x$ fresh for $C$ and note that $t_{C^{\prime }}\{x^{\prime }\leftarrow x\}\{x\leftarrow u_{C^{\prime }}\}=t_{C^{\prime }}\{x^{\prime }\leftarrow u_{C^{\prime }}\}$. The statement holds with respect to $t_C≔t_{C^{\prime }}\{x^{\prime }\leftarrow x\}r$ and $u_C≔u_{C^{\prime }}$.

• $\mathrm{■}$

  Application right, i.e. $C=r{C}^{\prime }$. Analogous to the previous case.

$◀$

The lemma captures the difficult-to-formalize part of the trick, and the proof is basic enough to be easily formalized. Unfortunately, the statement concerns a first-class context, while our representation of contexts in Abella is indirect, via the sub-term predicate, that is, always mentioning a plugged-in term – first-class contexts are not available in Abella.

Therefore, we have to rephrase the disentangling lemma in sub-term style. For that, we introduce a disentangling predicate, that holds as $\text{disentangling}uC⟨u⟩t_C{u}_C$ (using the notation of the lemma) and where the type of the third argument is $\text{tm}\to \text{tm}$ because it is given as a binder to capture the substitution on $x$.

The disentangling lemma (Lemma 14) is represented in sub-term style by two statements. The first one expresses the fact that the disentangling predicate does capture the property of the lemma for a given plugged term $u$:

The second statement expresses the fact that $t_C$ does not depend on $u$. This is essential: the proof of light genericity as context (Thm. 13.2) requires to apply the lemma in sub-term style twice (for $u$ and $s$ in the notations of Thm. 13), obtaining two terms $t_C$ and $t_C^{\prime }$ that might be different. We have to ensure instead that they coincide, which is expressed as follows:

Using this formalization of Takahashi’s trick, the formalized proofs of light and heavy genericity smoothly follow the pen-and-paper proofs of Accattoli and Lancelot [9] and Takahashi [57]. ^††margin: Grammar of $\beta$-normal forms defined in 08-3-beta-nfs.thm. To formalize heavy genericity, we also have to make explicit a mutually inductive grammar of $\beta$-normal forms, which Takahashi hid on paper by writing down full normal forms.

A natural notion of program equivalence is contextual equivalence, that equates terms which behave the same way in any context. We now define the head contextual preorder, refining the equivalence to an asymmetric relation and where the “behavior” of a term is whether or not it is head terminating.

Head contextual equivalence is sometimes referred to as (the equational theory) ${\mathscr{H}}^{\ast }$, especially in Barendregt’s study of the $\lambda$-calculus [15].

Contextual relations are sometimes defined slightly differently: they may be restricted to contexts $C$ such that $C⟨t⟩$ and $C⟨t^{\prime }⟩$ are closed terms. The contextual relations without the closed requirement are in general stronger, yet in some cases they are equivalent. When the observation is head termination – as it is the case here – they are equivalent, see [9].

We may now transpose the definition of the head contextual preorder to Abella:

The disentangling lemma of the previous section is a technical lemma but it actually has an interesting high-level consequence: it allows one to reformulate contextual preorder/equivalence with no reference to contexts.

First of all, note that the term $u_C$ in the statement of the lemma can be described as $\lambda y_1.\mathrm{\dots }\lambda y_n.u$ for some variables $y_1,\mathrm{\dots },y_n$ with $n\ge 0$. Then, the following new substitution preorder is shown equivalent to the contextual preorder thanks to the disentangling lemma. This is an original contribution of our work, and the distilled essence of Takahashi’s trick.

Direction $\Rightarrow$. Suppose that $C⟨t⟩$ is ${\to }_{𝚑}$-terminating. By disentangling, there exists $s_C$, $x$ and a lists of variables $y_1,\mathrm{\dots },y_n$ with $n\ge 0$ such that $t^{\prime }≔s_C\{x\leftarrow \lambda y_1.\mathrm{\dots }\lambda y_n.t\}{\to }_{\beta }^{\ast }C⟨t⟩$. By the head normalization theorem, $t^{\prime }$ is ${\to }_{𝚑}$-terminating. By substitution preorder, $u^{\prime }≔s_C\{x\leftarrow \lambda y_1.\mathrm{\dots }\lambda y_n.u\}$ is ${\to }_{𝚑}$-terminating. By the disentangling lemma, $u^{\prime }{\to }_{\beta }^{\ast }C⟨u⟩$. By extended head normalization (Cor. 12), $C⟨u⟩$ is ${\to }_{𝚑}$-normalizing.

Direction $\Leftarrow$. Suppose that $t^{\prime }≔s\{x\leftarrow \lambda y_1.\mathrm{\dots }\lambda y_n.t\}$ is ${\to }_{𝚑}$-normalizing. Consider the context $C≔(\lambda x.s)(\lambda y_1.\mathrm{\dots }\lambda y_n.⟨\cdot ⟩)$ and note that $C⟨t⟩{\to }_{𝚑}{t}^{\prime }$, so that $C⟨t⟩$ is ${\to }_{𝚑}$-normalizing. By contextual preorder, $C⟨u⟩$ is ${\to }_{𝚑}$-normalising. Note that $C⟨u⟩{\to }_{𝚑}{u}^{\prime }≔s\{x\leftarrow \lambda y_1.\mathrm{\dots }\lambda y_n.u\}$, so that $u^{\prime }$ is ${\to }_{𝚑}$-normalizing. $◀$

For the study of collapsibility, the following terminology borrowed from Accattoli and Lancelot [9] shall simplify the discussion.

Note that if a theory ${\le }_{ℛ}$ is ground then one has $t{\le }_{ℛ}u$ and $u{\le }_{ℛ}t$ for any two minimum elements $t$ and $u$, which implies that ${\le }_{ℛ}$ equates all head divergent terms.

We are now ready for proving that all head diverging terms can be consistently equated (unlike $\beta$-diverging terms) by showing that the contextual preorder is an equational theory that is ground, and thus equates them.

The difficult part of the theorem is the first point; precisely, that ${\precsim }_{𝒞}$ contains $\beta$. We formalize the proof by Accattoli and Lancelot [9] that uses non-trivial rewriting theorems, such as head normalisation (Thm. 7) and confluence of ${\to }_{\beta }$ (Thm. 1). Up to minor details, the formal proof follows the pen-and-paper one.

1. 1.

   It follows the proof in [9].

2. 2.

   $𝙸{\precsim ̸}_{𝒞}\mathrm{\Omega }$ holds by considering the empty context $C≔⟨\cdot ⟩$.

3. 3.

   Note that light genericity (Thm. 13.2) is exactly the fact that ${\precsim }_{𝒞}$ is ground.

$◀$

Barendregt’s book studies in-depth $\mathscr{H}$, the smallest equational theory equating all head divergent terms. We consider its associated preorder, and show it consistent.^††margin: The preorder is defined in 10-2-definition
-H.thm and proved consistent in 10-3-consistency
-H.thm.

It follows from the fact that ${\le }_{\mathscr{H}}$ is included in ${\precsim }_{𝒞}$, which is consistent (Thm. 21). $◀$

We qualify some inequational theories as adequate, following Accattoli and Lancelot and various work on program equivalence.

An inadequate theory is a theory that does not satisfy the adequacy property and a constructively inadequate theory is a theory where there (constructively) exists $t$ and $u$ such that $t$ is head normalizing but $u$ is head divergent.

Another cornerstone result in Barendregt’s study of equational theories is the fact that head contextual equivalence ${\simeq }_{𝒞}$ is the unique maximal consistent ground equational theory, that is, it captures all the identifications that one can do on top of identifying head divergent terms without risking identifying everything.

Barendregt shows that ${\simeq }_{𝒞}$ is a maximal consistent theory [15, Thm 16.2.6] relying on Böhm’s separation theorem. Barendregt and Manzonetto refine the result for ${\precsim }_{𝒞}$ [17], using the same technique. We formalize the simpler proof by Accattoli and Lancelot [9] based on light genericity and solvability, and not needing Böhm’s theorem. Our technique originates from the proof of maximality for CbV by Egidi et al. [24], also used by Arrial et al. [10].

There are two difficulties when dealing with Thm. 24 in Abella. Firstly, Point 1 of Thm. 24 and the very concept of maximality require quantification over equational theories. This cannot be done in Abella because there is no quantification over binary term relations: quantifying over the type prop is disabled [3] (because of soundness issues). Fortunately, we may still phrase maximality by showing it for a constant r of type $\text{tm}\to \text{tm}\to \text{prop}$ for which we know nothing.

The proof of this statement mimics the pen-and-paper proof of Point 1 of Thm. 24, as written by Accattoli and Lancelot [9].

Secondly, there is a delicate point in formalizing the proof of Point 2 of the theorem. The paper proof starts by picking a theory $𝒯$ that is strictly larger than ${\precsim }_{𝒞}$ and two terms $t$ and $u$ that are related in $𝒯$ but not by ${\precsim }_{𝒞}$. As $t$ and $u$ are not contextually related, there exists a context $C$ for which, say, $C⟨t⟩$ is head terminating while $C⟨u⟩$ is not. This step cannot be formalized in an intuistionistic setting because it directly changes a $\neg \forall \varphi$ statement into a $\exists \neg \varphi$ statement and also uses the fact that $\neg (\varphi \Rightarrow \psi )\Rightarrow \varphi \wedge \neg \psi$; in all generality, these statements are equivalent to the law of excluded middle [19, 61]. We circumvent the issue by adding as an axiom the exact statement that is needed for our proof to go through.

We plan to explore the intuistionic/classical aspects of the maximality theorem (constructive proofs? constructive definition of contextual preorder?), for which we currently resort to a classical axiom, and to formalize Böhm’s separation theorem building on Norrish and Tian’s work [59].