<figure><img src="image_1.png" /></figure>

HAL
open science

# Higher-Order unification for free!

Davide Fissore, Enrico Tassi

► To cite this version:

Davide Fissore, Enrico Tassi. Higher-Order unification for free!: Reusing the meta-language unification for the object language. 2024. [https://arxiv.org/abs/2405.04693](https://arxiv.org/abs/2405.04693)

HAL Id: hal-04547069

https://inria.hal.science/hal-04547069v3

Preprint submitted on 13 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Higher-Order unification for free!

## Reusing the meta-language unification for the object language

Davide Fissore

davide.fissore@inria.fr

Université Côte d'Azur, Inria

France

Enrico Tassi

enrico.tassi@inria.fr

Université Côte d'Azur, Inria

France

## ABSTRACT

Specifying and implementing a proof system from scratch requires significant effort. Logical Frameworks and Higher Order Logic Programming Languages provide dedicated, high-level meta languages to facilitate this task in two ways: 1) variable binding and substitution are for free when meta language binders represent object logic ones; 2) proof construction, and proof search, are greatly simplified by leveraging the unification procedure provided by the meta language. Notable examples of meta languages are Elf [21], Twelf [23], λProlog [16], Beluga [24], Abella [8] and Isabelle [30] which have been used to implement or specify many formal systems such as First Order Logic [5], Set Theory [20], Higher Order Logic [19], and the Calculus of Constructions [4].

The object logic we are interested in is Coq's type theory [28]. We aim to develop a higher-order unification-based proof search procedure using the meta language Elpi [3], a dialect of λProlog. Elpi's equational theory includes βη-equivalence and features a higher-order unification procedure ≈m for the pattern fragment [15]. Elpi offers an encoding of Coq terms that is suitable for meta programming [27, 26, 9, 6] but that restricts ≈m to first-order unification problems only. We refer to this basic encoding as O.

In this paper we translate unification problems in O to an alternative encoding called M, from which we derive ≈o, the higher-order unification procedure of O. ≈o honours βη-equivalence for terms within the pattern fragment, and allows for the use of heuristics when the terms fall outside the pattern fragment. Moreover, as ≈o delegates most of the work to ≈m, it can be used to efficiently simulate a logic program in O by taking advantage of unification-related optimizations of the meta language, such as clause indexing.

## KEYWORDS

Logic Programming, Meta-Programming, Higher-Order Unification

## ACM Reference Format:

Davide Fissore and Enrico Tassi. 2024. Higher-Order unification for free!: Reusing the meta-language unification for the object language. In 26th International Symposium on Principles and Practice of Declarative Programming (PPDP 2024), September 10–11, 2024, Milano, Italy. ACM, New York, NY, USA, 14 pages. https://doi.org/10.1145/3678232.3678233

## 1 INTRODUCTION

We aim to implement a form of proof search known as type-class resolution [29, 25] for Coq's type system [28]. Type-class solvers are unification based proof search procedures reminiscent of Prolog, which back-chain lemmas taken from a database of "type-class instances". Given this analogy with Logic Programming we want to leverage the Elpi meta programming language [27], a dialect of λProlog, already used to extend Coq in various ways [27, 26, 9, 6].

The use of a meta language facilitates the implementation of a proof system in two key ways. The first and most well-known one is that variable binding and substitution come for free. The second one is that these meta languages come equipped with some form of unification, a cornerstone of proof construction and proof search. In this paper we focus on this last aspect of the implementation of a Prolog-like proof system, precisely how to reuse the higher-order unification procedure of the meta language in order to simulate a higher-order logic program for the object language.

We take as an example the Decision and Finite type classes from the Stdpp library [12]. The class Decision identifies predicates equipped with a decision procedure, while Finite identifies types whose inhabitants can be enumerated in a (finite) list. The following three type-class instances state that: 1) the type of natural numbers smaller than n, called fin n, is finite; 2) the predicate nfact n nf, relating a natural number n to the number of its prime factors nf, is decidable; 3) the universal closure of a predicate has a decision procedure if its domain is finite and if the predicate is decidable.

Instance fin_fin: ∀n, Finite (fin n). (* r1 *)
Instance nfact_dec: ∀n nf, Decision (nfact n nf). (* r2 *)
Instanceforall_dec: ∀A P, Finite A → (* r3 *)
(∀x:A, Decision (P x)) → Decision (∀x:A, P x).

Given this database, a type-class solver is expected to prove the following statement automatically:

Decision (∀x: fin 7, nfact x 3) (* g *)

The proof found by the solver back-chains on rule 3 (the only rule about the ∀ quantifier), and then solves the premises with rules 1 and 2 respectively. Note that rule 3 features a second-order parameter P that represents a function of type A → Prop (a 1-argument predicate over A). The solver infers a value for P by unifying the conclusion of rule 3 with the goal, and in particular, it has to solve the unification problem P x = nfact x 3. This higher-order problem falls in the so-called pattern fragment and admits a unique solution:

P = λx.nfact x 3 (ρ)

In the rest of this paper, we refer to the pattern fragment as L [14].

In order to implement such a search in Elpi, we shall describe the encoding of Coq terms and then the encoding of instances as rules. Elpi comes equipped with a Higher-Order Abstract Syntax

<footnote>Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).</footnote>

<footnote>PPDP 2024, September 10–11, 2024, Milano, Italy</footnote>

<footnote>© 2024 Copyright held by the owner/author(s).</footnote>

<footnote>ACM ISBN 979-8-4007-0969-2/24/09.</footnote>

<footnote>https://doi.org/10.1145/3678232.3678233</footnote>
# Higher-Order unification for free!

## Reusing the meta-language unification for the object language

Davide Fissore

davide.fissore@inria.fr

Université Côte d'Azur, Inria

France

## ABSTRACT

Specifying and implementing a proof system from scratch requires significant effort. Logical Frameworks and Higher Order Logic Programming Languages provide dedicated, high-level meta languages to facilitate this task in two ways: 1) variable binding and substitution are for free when meta language binders represent object logic ones; 2) proof construction, and proof search, are greatly simplified by leveraging the unification procedure provided by the meta language. Notable examples of meta languages are Elf [19], Twelf [21], λProlog [14], Beluga [22], Abella [8] and Isabelle [28] which have been used to implement or specify many formal systems such as First Order Logic [5], Set Theory [18], Higher Order Logic [17], and the Calculus of Constructions [4].

The object logic we are interested in is Coq's type theory [26]. We aim to develop a higher-order unification-based proof search procedure using the meta language Elpi [3], a dialect of λProlog. Elpi's equational theory includes ηβ-equivalence and features a higher-order unification procedure ≈m for the pattern fragment [13]. Elpi offers an encoding of Coq terms that is suitable for meta programming [25, 24, 9, 6] but that restricts ≈m to first-order unification problems only. We refer to this basic encoding as O.

In this paper we propose a more well-behaved encoding called M, and show how to translate unification problems from O to corresponding ones in M. Consequently, we derive ≈o, the higher-order unification procedure of O that honours ηβ-equivalence (for Coq functions), addresses problems within the pattern fragment, and allows for the use of heuristics to deal with problems outside the pattern fragment. Moreover, as ≈o delegates most of the work to ≈m, it can be used to efficiently simulate a logic program in O by taking advantage of unification-related optimizations of the meta language, such as clause indexing.

## KEYWORDS

Logic Programming, Meta-Programming, Higher-Order Unification

## ACM Reference Format:

Davide Fissore and Enrico Tassi. 2024. Higher-Order unification for free!: Reusing the meta-language unification for the object language. In. ACM, New York, NY, USA, 14 pages. https://doi.org/10.1145/nnnnnnn.nnnnnnn

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

Conference'17, July 2017, Washington, DC, USA

© 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM ISBN 978-x-xxxx-xxxx-x/YY/MM

https://doi.org/10.1145/nnnnnnn.nnnnnnn

Enrico Tassi

enrico.tassi@inria.fr

Université Côte d'Azur, Inria

France

## 1 INTRODUCTION

We aim to implement a form of proof search known as type-class resolution [27, 23] for the Coq's system [26]. Type-class solvers are unification based proof search procedures reminiscent of Prolog, which back-chain lemmas taken from a database of "type-class instances". Given this analogy with Logic Programming we want to leverage the Elpi meta programming language [25], a dialect of λProlog, already used to extend Coq in various ways [25, 24, 9, 6].

The use of a meta language facilitates the implementation of a proof system in two key ways. The first and most well-known one is that variable binding and substitution come for free. The second one is that these meta languages come equipped with some form of unification, a cornerstone of proof construction and proof search. In this paper we focus on this last aspect of the implementation of a Prolog-like proof system, precisely how to reuse the higher-order unification procedure of the meta language in order to simulate a higher-order logic program for the object language.

We take as an example the Decision and Finite type classes from the Stdpp library [12]. The class Decision identifies predicates equipped with a decision procedure, while Finite identifies types whose inhabitants can be enumerated in a (finite) list. The following three type-class instances state that: 1) the type of natural numbers smaller than n, called fin n, is finite; 2) the predicate nfact n nf, relating a natural number n to the number of its prime factors nf, is decidable; 3) the universal closure of a predicate has a decision procedure if its domain is finite and if the predicate is decidable.

Instance fin_fin: ∀n, Finite (fin n). (* r1 *)
Instance nfact_dec: ∀n nf, Decision (nfact n nf). (* r2 *)
Instanceforall_dec: ∀A P, Finite A → (∗ r3 ∗)
Vx:A, Decision (P x) → Decision (�forall x: A, P x).

Given this database, a type-class solver is expected to prove the following statement automatically:

Decision (�forall x: fin 7, nfact x 3) (* g *)

The proof found by the solver back-chains on rule 3 (the only rule about the ∀ quantifier), and then solves the premises with rules 1 and 2 respectively. Note that rule 3 features a second-order parameter P that represents a function of type A → Prop (a 1-argument predicate over A). The solver infers a value for P by unifying the conclusion of rule 3 with the goal, and in particular, it has to solve the unification problem P x = nfact x 3. This higher-order problem falls in the so-called pattern fragment and admits a unique solution:

P = λx.nfact x 3 (ρ)

In the rest of this paper, we refer to the pattern fragment as L [13].

In order to implement such a search in Elpi, we shall describe the encoding of Coq terms and then the encoding of instances as rules. Elpi comes equipped with an Higher-Order Abstract Syntax
(HOAS [22]) datatype of Coq terms, called `tm`, that includes (among others) the following constructors:

<table><tr><td>type lam</td><td>tm -> (tm -> tm) -> tm.</td><td>% lambda abstraction</td></tr><tr><td>type app</td><td>list tm -> tm.</td><td>% n-ary application</td></tr><tr><td>type all</td><td>tm -> (tm -> tm) -> tm.</td><td>%forall quantifier</td></tr><tr><td>type con</td><td>string -> tm.</td><td>% constants</td></tr></table>

Following the standard syntax of λProlog [16], the meta-level binding of a variable `x` in an expression `e` is written as «`x`\ `e`», while square brackets delimit a list of terms separated by comma. For example, the term «∀y:t, nfact y 3» is encoded as follows:

all (con"t") y\ app [con"nfact", y, con"3"]

We now illustrate a naive encoding of the three instances above as higher-order logic programming rules: capital letters denote rule parameters; `:-` separates the rule's head from the premises, and «`pi w\ p`» introduces a fresh nominal constant `w` for the premise `p`.

finite (app [con"fin", N]). (r1)

decision (app [con"nfact", N, NF]). (r2)

decision (all A x\ app [P, x]) :- finite A, pi w\ decision (app [P, w]). (r3)

Unfortunately this encoding of rule (r3) does not work since it uses the predicate `P` as a first order term: for the meta language its type is `tm`. If we try to back-chain the rule (r3) on the encoding of the goal (`g`) given here

decision (all (app [con"fin", con"7"]) x\ app [con"nfact", x, con"3"]). (g)

we obtain an unsolvable unification problem (p): the two lists of terms have different lengths!

app [con"nfact", x, con"3"] = app [P, x] (p)

The problem above has no solution in a first-order language where `P` can only stand for a predicate symbol, while in a higher-order language `P` can stand for any 1-argument predicate.

In this paper we study a more sophisticated encoding of Coq terms and rules that, on a first approximation, would reshape (r3) as follows:

decision (all A x\ Pm x) :- link Pm P A, finite A, pi x\ decision (app [P, x]). (r3')

Since `Pm` is a higher-order unification variable of type `tm -> tm`, with `x` in its scope, the unification problem (p') admits one solution:

app [con"nfact", x, con"3"] = Pm x (p')

Pm = x\ app [con"nfact", x, con"3"] (σ)

Once the head of rule (r3') unifies with the goal (`g`), the premise «link Pm A P» brings the assignment (`σ`) back to the domain `tm` of Coq terms, obtaining the expected solution (`ρ`):

P = lam A x\ app [con"nfact", x, con"3"]

This simple example is sufficient to show that the encoding we seek is not trivial and does not only concern the head of rules, but the entire sequence of unification problems that constitute the execution of a logic program.

In fact the solution for `P` above generates a (Coq) `β`-redex in the second premise (the predicate under the `pi w\`). In turn, this redex prevents rule (r2) from backchaining properly since the following unification problem has no solution:

app [lam A (a\ app [con"nfact", a, con"3"]) , x] = app [con"nfact" , N, NF]

The root cause of the problems we outlined in this example is a subtle mismatch between the equational theories of the meta language and the object language, which in turn makes the unification procedures of the meta language weak. The equational theory of the meta-language Elpi encompasses `βη`-equivalence and its unification procedure can solve higher-order problems in the pattern fragment. Although the equational theory of Coq is much richer, for efficiency and predictability reasons automatic proof search procedures typically employ a unification procedure that only captures a `βη`-equivalence and only operates in $\mathcal{L}$. The similarity is striking, but one needs to exercise some caution in order to simulate a higher-order logic program in Coq using the unification of Elpi.

*Contributions.* In this paper we identify a minimal language $\mathcal{O}$ in which the problems sketched in the introduction can be formally described. We detail an encoding of a logic program in $\mathcal{O}$ to a strongly related logic program in $\mathcal{M}$, the language of the meta language, and we show that the higher-order unification procedure of the meta language $\approx_m$ can be used to simulate a higher-order unification procedure $\approx_o$ for the object language that features $\beta\eta$-conversion. We show how $\approx_o$ can be extended with heuristics to deal with problems outside the pattern fragment. Section 2 states the problem formally and gives the intuition behind our solution; section 3 sets up a basic simulation of first-order logic programs, section 4 and section 5 extend it to higher-order logic programs in the pattern fragment while section 7 goes beyond the pattern fragment. Section 8 discusses the implementation in Elpi. The λProlog code discussed in the paper can be accessed at the address https://github.com/FissoreD/ho-unif-for-free.

## 2 PROBLEM STATEMENT AND SOLUTION

Even if we encountered the problem working on Coq's Calculus of Inductive Constructions, we devise a minimal setting to ease its study. In this setting, we have a (first order) language $\mathcal{O}$ with a rich equational theory and a $\mathcal{M}$ language with a simpler one.

### 2.1 Preliminaries: $\mathcal{O}$ and $\mathcal{M}$

In order to reason about unification we provide a description of the $\mathcal{O}$ and $\mathcal{M}$ languages where unification variables are first-class terms, i.e. they have a concrete syntax as shown in fig. 1. Unification variables in $\mathcal{O}$ (o-uva term constructor) have no explicit scope: the “arguments” of a higher-order variable are given via the o-app constructor. For example the term «`P x`» is represented as «`o-app [o-uva N, x]`», where `N` is the memory address of `P` and `x` is a bound variable. In $\mathcal{M}$ the representation of «`P x`» is instead «`uva N [x]`», since unification variables are higher-order and come equipped with an explicit scope.

kind to type. kind tm type.
type o-app list to -> to. type app list tm -> tm.
type o-lam (to -> to) -> to. type lam (tm -> tm) -> tm.
type o-con string -> to. type con string -> tm.
type o-uva addr -> to. type uva addr -> list tm -> tm.

<caption>Figure 1: The $\mathcal{O}$ and $\mathcal{M}$ languages</caption>
(HOAS [20]) datatype of Coq terms, called `tm`, that includes (among others) the following constructors:

<table><tr><td>type lam tm -> (tm -> tm) -> tm.</td><td>% lambda abstraction</td></tr><tr><td>type app list tm -> tm.</td><td>% n-ary application</td></tr><tr><td>type all tm -> (tm -> tm) -> tm.</td><td>%forall quantifier</td></tr><tr><td>type con string -> tm.</td><td>% constants</td></tr></table>

Following the standard syntax of λProlog [14], the meta-level binding of a variable `x` in an expression `e` is written as «`x`\ `e`», while square brackets delimit a list of terms separated by comma. For example, the term «∀y:t, nfact y 3» is encoded as follows:

all (con"t") y\ app [con"nfact", y, con"3"]

We now illustrate a naive encoding of the three instances above as higher-order logic programming rules: capital letters denote rule parameters; `:-` separates the rule's head from the premises, and «`pi w\ p`» introduces a fresh nominal constant `w` for the premise `p`.

finite (app [con"fin", N]). (r1)

decision (app [con"nfact", N, NF]). (r2)

decision (all A x\ app [P, x]) :- finite A, pi w\ decision (app [P, w]). (r3)

Unfortunately this encoding of rule (r3) does not work since it uses the predicate `P` as a first order term: for the meta language its type is `tm`. If we try to back-chain the rule (r3) on the encoding of the goal (`g`) given here

decision (all (app [con"fin", con"7"]) x\ app [con"nfact", x, con"3"]). (g)

we obtain an unsolvable unification problem (p): the two lists of terms have different lengths!

app [con"nfact", x, con"3"] = app [P, x] (p)

The problem above has no solution in a first-order language where `P` can only stand for a predicate symbol, while in a higher-order language `P` can stand for any 1-argument predicate.

In this paper we study a more sophisticated encoding of Coq terms and rules that, on a first approximation, would reshape (r3) as follows:

decision (all A x\ Pm x) :- link Pm P A, finite A, pi x\ decision (app [P, x]). (r3')

Since `Pm` is a higher-order unification variable of type `tm -> tm`, with `x` in its scope, the unification problem (p') admits one solution:

app [con"nfact", x, con"3"] = Pm x (p')

Pm = x\ app [con"nfact", x, con"3"] (σ)

Once the head of rule (r3') unifies with the goal (`g`), the premise «link Pm A P» brings the assignment (`σ`) back to the domain `tm` of Coq terms, obtaining the expected solution (`ρ`):

P = lam A x\ app [con"nfact", x, con"3"]

This simple example is sufficient to show that the encoding we seek is not trivial and does not only concern the head of rules, but the entire sequence of unification problems that constitute the execution of a logic program.

In fact the solution for `P` above generates a (Coq) `β`-redex in the second premise (the predicate under the `pi w\`). In turn, this redex prevents rule (r2) from backchaining properly since the following unification problem has no solution:

app [lam A (a\ app [con"nfact", a, con"3"]) , x] = app [con"nfact", N, NF] (175)

The root cause of the problems we outlined in this example is a subtle mismatch between the equational theories of the meta language and the object language, which in turn makes the unification procedures of the meta language weak. The equational theory of the meta-language Elpi encompasses ηβ-equivalence and its unification procedure can solve higher-order problems in the pattern fragment. Although the equational theory of Coq is much richer, for efficiency and predictability reasons automatic proof search procedures typically employ a unification procedure that only captures a ηβ-equivalence and only operates in L. The similarity is striking, but one needs to exercise some caution in order to simulate a higher-order logic program in Coq using the unification of Elpi.

*Contributions.* In this paper we identify a minimal language *O* in which the problems sketched in the introduction can be formally described. We detail an encoding of a logic program in *O* to a strongly related logic program in *M*, the language of the meta language, and we show that the higher-order unification procedure of the meta language ≈<sub>m</sub> can be used to simulate a higher-order unification procedure ≈<sub>o</sub> for the object language that features ηβ-conversion. We show how ≈<sub>o</sub> can be extended with heuristics to deal with problems outside the pattern fragment. Section 2 states the problem formally and gives the intuition behind our solution; section 3 sets up a basic simulation of first-order logic programs, section 4 and section 5 extend it to higher-order logic programs in the pattern fragment while section 7 goes beyond the pattern fragment. Section 8 discusses the implementation in Elpi. The λProlog code discussed in the paper can be accessed at the address https://github.com/FissoreD/ho-unif-for-free.

## 2 PROBLEM STATEMENT AND SOLUTION

Even if we encountered the problem working on Coq's Calculus of Inductive Constructions, we devise a minimal setting to ease its study. In this setting, we have a (first order) language *O* with a rich equational theory and a *M* language with a simpler one.

### 2.1 Preliminaries: *O* and *M*

In order to reason about unification we provide a description of the *O* and *M* languages where unification variables are first-class terms, i.e. they have a concrete syntax as shown in fig. 1. Unification variables in *O* (o-uva term constructor) have no explicit scope: the “arguments” of a higher-order variable are given via the o-app constructor. For example the term «`P x`» is represented as «`o-app [o-uva N, x]`», where `N` is the memory address of `P` and `x` is a bound variable. In *M* the representation of «`P x`» is instead «`uva N [x]`», since unification variables are higher-order and come equipped with an explicit scope.

kind to type. kind tm type.
type o-app list to -> to. type app list tm -> tm.
type o-lam (to -> to) -> to. type lam (tm -> tm) -> tm.
type o-con string -> to. type con string -> tm.
type o-uva addr -> to. type uva addr -> list tm -> tm.

<caption>Figure 1: The *O* and *M* languages</caption>
**Notational conventions.** When we write $\mathcal{M}$ terms outside code blocks we follow the usual $\lambda$-calculus notation, reserving $f, g, a, b$ for constants, $x, y, z$ for bound variables and $X, Y, Z, F, G, H$ for unification variables. However, we need to distinguish between the “application” of a unification variable to its scope and the application of a term to a list of arguments. We write the scope of unification variables in subscript while we use juxtaposition for regular application. Here are few examples:

<table><tr><td>$f$</td><td>app [con "f", con "a"]</td></tr><tr><td>$\lambda x.\lambda y.F_{xy}$</td><td>lam x\ lam y\ uva F [x, y]</td></tr><tr><td>$\lambda x.F_x a$</td><td>lam x\ app [uva F [x], con "a"]</td></tr><tr><td>$\lambda x.F_x x$</td><td>lam x\ app [uva F [x], x]</td></tr></table>

When it is clear from the context, we shall use the same syntax for $\mathcal{O}$ terms (although we never use subscripts for unification variables). We use $s_1, \dots$ for terms in $\mathcal{O}$ and $t, t_1, \dots$ for terms in $\mathcal{M}$.

## 2.2 Equational theories and unification

### 2.2.1 Term equality: $=o$ and $=m$
For both languages, we extend the equational theory over ground terms to the full language by adding reflexivity for unification variables, i.e. a unification variable is equal to itself but different to any other term.

The first four rules are common to both equalities and define the usual congruence over terms. Since we use an HOAS encoding, they also capture $\alpha$-equivalence. In addition to that, $=o$ has rules for $\eta$ and $\beta$-equivalence.

<table><tr><td>type (=o) to -> to -> o.</td><td>(=o)</td></tr><tr><td>o-con X =o o-con X.</td><td></td></tr><tr><td>o-app A =o o-app B :-forall2 (=o) A B.</td><td></td></tr><tr><td>o-lam F =o o-lam G :-pi x\ x =o x => F x =o G x.</td><td>(λλ)</td></tr><tr><td>o-uva N =o o-uva N.</td><td></td></tr><tr><td>o-lam F =o T :-</td><td>(ηl)</td></tr><tr><td>pi x\ beta T [x] (T' x), x =o x => F x =o T' x.</td><td></td></tr><tr><td>T =o o-lam F :-</td><td>(ηr)</td></tr><tr><td>pi x\ beta T [x] (T' x), x =o x => T' x =o F x.</td><td></td></tr><tr><td>o-app [o-lam X|L] =o T :-beta (o-lam X) LR, R =o T.</td><td>(βl)</td></tr><tr><td>T =o o-app [o-lam X|L] :-beta (o-lam X) LR, T =o R.</td><td>(βr)</td></tr><tr><td>type (=m) tm -> tm -> o.</td><td></td></tr><tr><td>con C =m con C.</td><td></td></tr><tr><td>app A =m app B :-forall2 (=m) A B.</td><td></td></tr><tr><td>lam F =m lam G :-pi x\ x =m x => F x =m G x.</td><td></td></tr><tr><td>uva N A =m uva N B :-forall2 (=m) A B.</td><td></td></tr></table>

Note that the symbol $|$ separates the head of a list from the tail; that `forall2` applies a binary predicate to two lists (of equal length); and that `=>` is `λProlog` syntax for implication and is used to augment the current program with an extra rule. Both procedures use implication to assume that the fresh nominal constants introduces by `pi` are equal to themselves.

The main point in showing these equality tests is to remark how weaker $=m$ is, and to identify the four rules that need special treatment in the implementation of $\approx_o$. For brevity, we omit the code of beta: it is sufficient to know that «beta F L R» computes in $R$ the weak-head normal form of «o-app [F|L]».

**Substitution:** $\rho s$ and $\sigma t$. We write $\sigma = \{ X \mapsto t \}$ for the substitution that assigns the term $t$ to the variable $X$. We write $\sigma t$ for the

application of the substitution to a term $t$, and $\sigma X = \{ \sigma t | t \in X \}$ when $X$ is a set of terms. We write $\sigma \subseteq \sigma'$ when $\sigma$ is more general than $\sigma'$. We shall use $\rho$ for $\mathcal{O}$ substitutions, and $\sigma$ for the $\mathcal{M}$ ones. For brevity, in this section, we consider the substitution for $\mathcal{O}$ and $\mathcal{M}$ identical. We defer to section 3.1 a more precise description pointing out their differences.

**Term unification:** $\approx_o$ vs. $\approx_m$. $\mathcal{M}$'s unification signature is:

type ($\approx_m$) tm -> tm -> subst -> subst -> o.

We write $\sigma t_1 \approx_m \sigma t_2 \mapsto \sigma'$ when $\sigma t_1$ and $\sigma t_2$ unify with substitution $\sigma'$. Note that $\sigma'$ is a refined (i.e. extended) version of $\sigma$; this is reflected by the signature above that relates two substitutions. We write $t_1 \approx_m t_2 \mapsto \sigma'$ when the initial substitution $\sigma$ is empty. We write $\mathcal{L}$ as the set of terms that are in the pattern-fragment, i.e. every unification variable is applied to a list of distinct names.

The specification of a “good” unification procedure restricted to a domain $\mathcal{D}$ is the following:

**PROPOSITION 2.1 (GOOD UNIFICATION).** A good unification $\approx$ for equality $=$ in the domain $\mathcal{D}$ satisfies the following properties:

$$ \{ t_1, t_2 \} \subseteq \mathcal{D} \Rightarrow t_1 \approx t_2 \mapsto \rho \Rightarrow \rho t_1 = \rho t_2 \quad (1) $$

$$ \{ t_1, t_2 \} \subseteq \mathcal{D} \Rightarrow \rho t_1 = \rho t_2 \Rightarrow \exists \rho', t_1 \approx t_2 \mapsto \rho' \land \rho' \subseteq \rho \quad (2) $$

The meta language of choice is expected to provide an implementation of $\approx_m$ that is a good unification for $=m$ in $\mathcal{L}$.

Even if we provide an implementation of the object-language unification $\approx_o$ in section 3.6, our final goal is to simulate the execution of an entire logic-program.

## 2.3 The problem: logic-program simulation

We represent a logic program `run` in $\mathcal{O}$ as a sequence of $n$ steps. Each step $p$ consists in unifying two terms, $\mathbb{P}_{p1}$ and $\mathbb{P}_{pr}$, taken from the list of all unification problems $\mathbb{P}$. We write $\mathbb{P}_p = \{ \mathbb{P}_{p1}, \mathbb{P}_{pr} \}$ and $s \in \mathbb{P} \Leftrightarrow \exists p, s \in \mathbb{P}_p$. The composition of these steps starting from the empty substitution $\rho_0$ produces the final substitution $\rho_n$, which is the result of the logic program execution.

$$ \begin{align*} \text{step}_o(\mathbb{P}, p, \rho) &\mapsto \rho' \stackrel{\text{def}}{=} \rho_{\mathbb{P}_{p1}} \approx_o \rho_{\mathbb{P}_{pr}} &\mapsto \rho' \\ \text{run}_o(\mathbb{P}, n) &\mapsto \rho_n \stackrel{\text{def}}{=} \bigwedge_{p=1}^n \text{step}_o(\mathbb{P}, p, \rho_{p-1}) &\mapsto \rho_p \end{align*} $$

In order to simulate a logic program we start by compiling $\mathbb{P}$ to $\mathbb{Q}$, i.e. each $\mathcal{O}$-term $s \in \mathbb{P}$ is translated to a $\mathcal{M}$-term $t \in \mathbb{Q}$. We write this translation as $\langle s \rangle \mapsto (t, m, l)$. The implementation of the compiler is detailed in sections 3, 5 and 7, here we just point out that it additionally produces a variable map $m$ and a list of links $l$. The variable map connects unification variables in $\mathcal{M}$ to variables in $\mathcal{O}$ and is used to “decompile” the substitution, that is written $\langle \sigma, m, l \rangle^{-1} \mapsto \rho$. Links are an accessory piece of information whose description is deferred to section 2.4.

Then we simulate each run in $\mathcal{O}$ with a run in $\mathcal{M}$ as follows:

$$ \begin{align*} \text{step}_m(\mathbb{Q}, p, \sigma, \mathbb{L}) &\mapsto (\sigma'', \mathbb{L}') \stackrel{\text{def}}{=} \\ \sigma_{\mathbb{Q}_{p1}} &\approx_m \sigma_{\mathbb{Q}_{pr}} \mapsto \sigma' \land \text{progress}(\mathbb{L}, \sigma') \mapsto (\mathbb{L}', \sigma'') \\ \text{run}_m(\mathbb{P}, n) &\mapsto \rho_n \stackrel{\text{def}}{=} \\ \mathbb{Q} \times \mathbb{M} \times \mathbb{L}_0 &= \{(t, m, l) | s \in \mathbb{P}, \langle s \rangle \mapsto (t, m, l)\} \\ \bigwedge_{p=1}^n \text{step}_m(\mathbb{Q}, p, \sigma_{p-1}, \mathbb{L}_{p-1}) &\mapsto (\sigma_p, \mathbb{L}_p) \\ \langle \sigma_n, \mathbb{M}, \mathbb{L}_n \rangle^{-1} &\mapsto \rho_n \end{align*} $$
**Notational conventions.** When we write $\mathcal{M}$ terms outside code blocks we follow the usual $\lambda$-calculus notation, reserving $f, g, a, b$ for constants, $x, y, z$ for bound variables and $X, Y, Z, F, G, H$ for unification variables. However, we need to distinguish between the “application” of a unification variable to its scope and the application of a term to a list of arguments. We write the scope of unification variables in subscript while we use juxtaposition for regular application. Here are few examples:

f a app [con "f", con "a"]

$\lambda x.\lambda y.F_{xy}$ lam x\ lam y\ uva F [x, y]

$\lambda x.F_x a$ lam x\ app [uva F [x], con "a"]

$\lambda x.F_x x$ lam x\ app [uva F [x], x]

When it is clear from the context, we shall use the same syntax for $\mathcal{O}$ terms (although we never subscripts unification variables). We use $s, s_1, \dots$ for terms in $\mathcal{O}$ and $t, t_1, \dots$ for terms in $\mathcal{M}$.

## 2.2 Equational theories and unification

### 2.2.1 Term equality: $=o$ and $=m$
For both languages, we extend the equational theory over ground terms to the full language by adding reflexivity for unification variables, i.e. a unification variable is equal to itself but different to any other term.

The first four rules are common to both equalities and define the usual congruence over terms. Since we use an HOAS encoding, they also capture $\alpha$-equivalence. In addition to that, $=o$ has rules for $\eta$ and $\beta$-equivalence.

type ($=o$) to -> to -> o. (=o)

o-con X =o o-con X.

o-app A =o o-app B :-forall2 (=o) A B.

o-lam F =o o-lam G :- pi x\ x =o x => F x =o G x. (\lambda\lambda)

o-uva N =o o-uva N.

o-lam F =o T :- (η_l)

pi x\ beta T [x] (T' x), x =o x => F x =o T' x.

T =o o-lam F :- (η_r)

pi x\ beta T [x] (T' x), x =o x => T' x =o F x.

o-app [o-lam X|L] =o T :- beta (o-lam X) L R, R =o T. (β_l)

T =o o-app [o-lam X|L] :- beta (o-lam X) L R, T =o R. (β_r)

type ($=m$) tm -> tm -> o.

con C =m con C.

app A =m app B :-forall2 (=m) A B.

lam F =m lam G :- pi x\ x =m x => F x =m G x.

uva N A =m uva N B :-forall2 (=m) A B.

Note that the symbol $|$ separates the head of a list from the tail; that $\mathrm{forall2}$ applies a binary predicate to two lists (of equal length); and that $=>$ is $\lambda$Prolog syntax for implication and is used to augment the current program with an extra rule. Both procedures use implication to assume that the fresh nominal constants introduces by $\mathrm{pi}$ are equal to themselves.

The main point in showing these equality tests is to remark how weaker $=m$ is, and to identify the four rules that need special treatment in the implementation of $\approx_o$. For brevity, we omit the code of beta: it is sufficient to know that «beta F L R» computes in $R$ the weak-head normal form of «o-app [F|L]».

**Substitution:** $\rho s$ and $\sigma t$. We write $\sigma = \{ X \mapsto t \}$ for the substitution that assigns the term $t$ to the variable $X$. We write $\sigma t$ for the

application of the substitution to a term $t$, and $\sigma X = \{ \sigma t | t \in X \}$ when $X$ is a set of terms. We write $\sigma \subseteq \sigma'$ when $\sigma$ is more general than $\sigma'$. We shall use $\rho$ for $\mathcal{O}$ substitutions, and $\sigma$ for the $\mathcal{M}$ ones. For brevity, in this section, we consider the substitution for $\mathcal{O}$ and $\mathcal{M}$ identical. We defer to section 3.1 a more precise description pointing out their differences.

**Term unification:** $\approx_o$ vs. $\approx_m$. $\mathcal{M}$'s unification signature is:

type ($\approx_m$) tm -> tm -> subst -> subst -> o.

We write $\sigma t_1 \approx_m \sigma t_2 \mapsto \sigma'$ when $\sigma t_1$ and $\sigma t_2$ unify with substitution $\sigma'$. Note that $\sigma'$ is a refined (i.e. extended) version of $\sigma$; this is reflected by the signature above that relates two substitutions. We write $t_1 \approx_m t_2 \mapsto \sigma'$ when the initial substitution $\sigma$ is empty. We write $\mathcal{L}$ as the set of terms that are in the pattern-fragment, i.e. every unification variable is applied to a list of distinct names.

The specification of a “good” unification procedure restricted to a domain $\mathcal{D}$ is the following:

**PROPOSITION 2.1 (GOOD UNIFICATION).** A good unification $\approx$ for equality $=$ in the domain $\mathcal{D}$ satisfies the following properties:

$$ \{ t_1, t_2 \} \subseteq \mathcal{D} \Rightarrow t_1 \approx t_2 \mapsto \rho \Rightarrow \rho t_1 = \rho t_2 \quad (1) $$

$$ \{ t_1, t_2 \} \subseteq \mathcal{D} \Rightarrow \rho t_1 = \rho t_2 \Rightarrow \exists \rho', t_1 \approx t_2 \mapsto \rho' \wedge \rho' \subseteq \rho \quad (2) $$

The meta language of choice is expected to provide an implementation of $\approx_m$ that is a good unification for $=m$ in $\mathcal{L}$.

Even if we provide an implementation of the object-language unification $\approx_o$ in section 3.6, our real goal is to simulate the execution of an entire logic-program.

## 2.3 The problem: logic-program simulation

We represent a logic program run in $\mathcal{O}$ as a sequence of $n$ steps. Each step $p$ consists in unifying two terms, $\mathbb{P}_{p_1}$ and $\mathbb{P}_{p_r}$, taken from the list of all unification problems $\mathbb{P}$. We write $\mathbb{P}_p = \{ \mathbb{P}_{p_1}, \mathbb{P}_{p_r} \}$ and $s \in \mathbb{P} \Leftrightarrow \exists p, s \in \mathbb{P}_p$. The composition of these steps starting from the empty substitution $\rho_0$ produces the final substitution $\rho_n$, which is the result of the logic program execution.

step$_o(\mathbb{P}, p, \rho) \mapsto \rho' \stackrel{def}{=} \rho \mathbb{P}_{p_1} \approx_o \rho \mathbb{P}_{p_r} \mapsto \rho'$

run$_o(\mathbb{P}, n) \mapsto \rho_n \stackrel{def}{=} \bigwedge_{p=1}^n \mathrm{step}_o(\mathbb{P}, p, \rho_{p-1}) \mapsto \rho_p

In order to simulate a logic program we start by compiling $\mathbb{P}$ to $\mathbb{Q}$, i.e. each $\mathcal{O}$-term $s \in \mathbb{P}$ is translated to a $\mathcal{M}$-term $t \in \mathbb{Q}$. We write this translation as $\langle s \rangle \mapsto (t, m, l)$. The implementation of the compiler is detailed in sections 3, 5 and 7, here we just point out that it additionally produces a variable map $m$ and a list of links $l$. The variable map connects unification variables in $\mathcal{M}$ to variables in $\mathcal{O}$ and is used to “decompile” the substitution, that is written $\langle \sigma, m, l \rangle^{-1} \mapsto \rho$. Links are an accessory piece of information whose description is deferred to section 2.4.

Then we simulate each run in $\mathcal{O}$ with a run in $\mathcal{M}$ as follows:

step$_m(\mathbb{Q}, p, \sigma, \mathbb{L}) \mapsto (\sigma'', \mathbb{L}') \stackrel{def}{=} \sigma \mathbb{Q}_{p_1} \approx_m \sigma \mathbb{Q}_{p_r} \mapsto \sigma' \wedge \mathrm{progress}(\mathbb{L}, \sigma') \mapsto (\mathbb{L}', \sigma'')

run$_m(\mathbb{P}, n) \mapsto \rho_n \stackrel{def}{=} \mathbb{Q} \times \mathbb{M} \times \mathbb{L}_0 = \{(t, m, l) | s \in \mathbb{P}, \langle s \rangle \mapsto (t, m, l)\}

$\bigwedge_{p=1}^n \mathrm{step}_m(\mathbb{Q}, p, \sigma_{p-1}, \mathbb{L}_{p-1}) \mapsto (\sigma_p, \mathbb{L}_p)$

$\langle \sigma_n, \mathbb{M}, \mathbb{L}_n \rangle^{-1} \mapsto \rho_n$
By analogy with $\mathbb{P}$, we write $\mathbb{Q}_{p_1}$ and $\mathbb{Q}_{p_r}$ for the two $\mathcal{M}$ terms being unified at step $p$, and we write $\mathbb{Q}_p$ for the set $\{ \mathbb{Q}_{p_1}, \mathbb{Q}_{p_r} \}$. The step$_m$ procedure is made of two sub-steps: a call to the meta-language unification and a check for progress on the set of links, that intuitively will compensate for the weaker equational theory honored by $\approx_m$. Procedure run$_m$ compiles all terms in $\mathbb{P}$, then executes each step, and finally decompiles the solution. We claim:

**PROPOSITION 2.2 (RUN EQUIVALENCE).** $\forall \mathbb{P}, \forall n, \text{ if } \mathbb{P} \subseteq \mathcal{L}$
$$ \mathrm{run}_o(\mathbb{P}, n) \mapsto \rho \wedge \mathrm{run}_m(\mathbb{P}, n) \mapsto \rho' \Rightarrow \forall s \in \mathbb{P}, \rho s =_o \rho' s $$

That is, the two executions give equivalent results if all terms in $\mathbb{P}$ are in the pattern fragment. Moreover:

**PROPOSITION 2.3 (SIMULATION FIDELITY).** In the context of run$_o$ and run$_m$, if $\mathbb{P} \subseteq \mathcal{L}$ we have that $\forall p \in 1...n$,

$$ \mathrm{step}_o(\mathbb{P}, p, \rho_{p-1}) \mapsto \rho_p \Leftrightarrow \mathrm{step}_m(\mathbb{Q}, p, \sigma_{p-1}, \mathbb{L}_{p-1}) \mapsto (\sigma_p, \mathbb{L}_p) $$

In particular, this property guarantees that a failure in the $\mathcal{O}$ run is matched by a failure in $\mathcal{M}$ at the same step. We consider this property very important from a practical point of view since it guarantees that the execution traces are strongly related, and in turn, this enables a user to debug a logic program in $\mathcal{O}$ by looking at its execution trace in $\mathcal{M}$.

We also claim that run$_m$ handles terms outside $\mathcal{L}$ in the following sense:

**PROPOSITION 2.4 (FIDELITY RECOVERY).** In the context of run$_o$ and run$_m$, if $\rho_{p-1} \mathbb{P}_p \subseteq \mathcal{L}$ (even if $\mathbb{P}_p \not\subseteq \mathcal{L}$) then

$$ \mathrm{step}_o(\mathbb{P}, p, \rho_{p-1}) \mapsto \rho_p \Leftrightarrow \mathrm{step}_m(\mathbb{Q}, p, \sigma_{p-1}, \mathbb{L}_{p-1}) \mapsto (\sigma_p, \mathbb{L}_p) $$

In other words, if the two terms involved in a step re-enter $\mathcal{L}$, then step$_m$ and step$_o$ are again related, even if $\mathbb{P} \not\subseteq \mathcal{L}$ and hence proposition 2.3 does not apply. Indeed, the main difference between proposition 2.3 and proposition 2.4 is that the assumption of the former is purely static, it can be checked upfront. When this assumption is not satisfied, one can still simulate a logic program and have guarantees of fidelity if, at run time, decidability of higher-order unification is restored.

This property has practical relevance since in many logic programming implementations, including Elpi, the order in which unification problems are tackled does matter. The simplest example is the sequence $F \approx \lambda x.a$ and $F a \approx a$: the second problem is not in $\mathcal{L}$ and has two unifiers, namely $\sigma_1 = \{ F \mapsto \lambda x.x \}$ and $\sigma_2 = \{ F \mapsto \lambda x.a \}$. The first problem picks $\sigma_2$, making the second problem re-enter $\mathcal{L}$.

**Backtracking.** We omit it from our model of logic-program execution since it plays a very minor role, orthogonal to higher-order unification. We point out that each run corresponds to a (proof search) branch in the logic program that either fails at some point, or succeeds. A computation that succeeds by backtracking, exploring multiple branches, could be modeled as a set of runs with a (possibly non-empty) common prefix.

## 2.4 The solution (in a nutshell)

A term $s$ is compiled to a term $t$ where every “problematic” subterm $e$ is replaced by a fresh unification variable $h$ with an accessory link that represents a suspended unification problem $h \approx_m e$. As a result,

$\approx_m$ is “well behaved” on $t$, in the sense that it does not contradict $=_o$ as it would otherwise do on the “problematic” sub-terms. We now define “problematic” and “well behaved” more formally. We use the $\diamond$ symbol since it stands for “possibly” in modal logic and all problematic terms are characterized by some uncertainty.

**Definition 2.5 ($\diamond\beta$).** $\diamond\beta$ is the set of terms of the form $F x_1...x_n$ such that $x_1...x_n$ are distinct names (of bound variables).

An example of a $\diamond\beta$ term is the application $F x$. This term is problematic since the application node of its syntax tree cannot be used to justify a unification failure, i.e. by properly instantiating $F$, the term head constructor may become a $\lambda$, or a constant, or a name, or remain an application.

**Definition 2.6 ($\diamond\eta$).** $\diamond\eta$ is the set of terms $\lambda x.s$ such that $\exists\rho, \rho(\lambda x.s)$ is an $\eta$-redex.

An example of a term $s$ in $\diamond\eta$ is $\lambda x.\lambda y. F y x$ since the substitution $\rho = \{F \mapsto \lambda x.\lambda y. f y x\}$ makes $\rho s =_o \lambda x.\lambda y. f x y$, which is the eta-long form of $f$. This term is problematic since its leading $\lambda$ abstraction cannot justify a unification failure against a constant $f$.

**Definition 2.7 ($\diamond\mathcal{L}$).** $\diamond\mathcal{L}$ is the set of terms of the form $F \cdot t_1...t_n$ such that $t_1...t_n$ are not distinct names.

These terms are problematic for the very same reason terms in $\diamond\beta$ are, but they cannot be handled directly by the unification of the meta language, which is only required to handle terms in $\mathcal{L}$. Still, given $s \in \diamond\mathcal{L}$ there may exist a substitution $\rho$ such that $\rho s \in \mathcal{L}$.

We write $\mathcal{P}(t)$ for the set of sub-terms of $t$, and we write $\mathcal{P}(X) = \bigcup_{t \in X} \mathcal{P}(t)$ when $X$ is a set of terms.

**Definition 2.8 (Well behaved set).** Given a set of terms $X$,

$$ \mathcal{W}(X) \Leftrightarrow \forall t \in \mathcal{P}(X), t \notin (\diamond\beta \cup \diamond\eta \cup \diamond\mathcal{L}) $$

We write $\mathcal{W}(t)$ as a short for $\mathcal{W}(\{t\})$. We claim our compiler validates the following properties:

**PROPOSITION 2.9 (W-ENFORCING).** Given a term $s$ in $\mathcal{O}$,

$$ \langle s \rangle \mapsto (t, m, l) \Rightarrow \mathcal{W}(t) $$

**PROPOSITION 2.10 (COMPILER-USEFUL).** Given two terms $s_1$ and $s_2$, if $\exists\rho, \rho s_1 =_o \rho s_2$, then

$$ \langle s_i \rangle \mapsto (t_i, m_i, l_i) \text{ for } i \in \{1, 2\} \Rightarrow t_1 \approx_m t_2 \mapsto \sigma $$

In other words the compiler outputs terms in $\mathcal{W}$ even if its input is not. And if two terms can be unified in the source language then their images can also be unified in the target language. Note that the property holds for any substitution, not necessarily a most general one: when applied to terms in $\mathcal{W}$ the meta-language unification $\approx_m$ agrees with the object-language equality $=_o$. Note that a compiler that translate all terms to unification variables would satisfy this property, but wound certainly fail to verify proposition 2.3.

**PROPOSITION 2.11 (W-PRESERVATION).** $\forall \mathbb{Q}, \forall \mathbb{L}, \forall p, \forall \sigma, \forall \sigma'$

$$ \begin{aligned} \mathcal{W}(\sigma(\mathbb{Q}) \wedge \sigma(\mathbb{Q}_{p_1}) \approx_m \sigma(\mathbb{Q}_{p_r}) \mapsto \sigma') &\Rightarrow \mathcal{W}(\sigma'(\mathbb{Q})) \\ \mathcal{W}(\sigma(\mathbb{Q}) \wedge \mathrm{progress}(\mathbb{L}, \sigma) \mapsto (\cdot, \sigma') &\Rightarrow \mathcal{W}(\sigma'(\mathbb{Q})) \end{aligned} $$

Proposition 2.11 is key to proving propositions 2.2 and 2.3. Informally, it says that the problematic terms moved on the side by the compiler are not reintroduced by step$_m$, hence $\approx_m$ can continue
By analogy with $\mathbb{P}$, we write $\mathbb{Q}_{p_1}$ and $\mathbb{Q}_{p_r}$ for the two $\mathcal{M}$ terms being unified at step $p$, and we write $\mathbb{Q}_p$ for the set $\{\mathbb{Q}_{p_1}, \mathbb{Q}_{p_r}\}$. The step$_m$ procedure is made of two sub-steps: a call to the meta-language unification and a check for progress on the set of links, that intuitively will compensate for the weaker equational theory honored by $\approx_m$. Procedure run$_m$ compiles all terms in $\mathbb{P}$, then executes each step, and finally decompiles the solution. We claim:

**PROPOSITION 2.2 (RUN EQUIVALENCE).** $\forall \mathbb{P}, \forall n, \text{ if } \mathbb{P} \subseteq \mathcal{L}$
$$ \text{run}_o(\mathbb{P}, n) \mapsto \rho \wedge \text{run}_m(\mathbb{P}, n) \mapsto \rho' \Rightarrow \forall s \in \mathbb{P}, \rho s =_o \rho' s $$

That is, the two executions give equivalent results if all terms in $\mathbb{P}$ are in the pattern fragment. Moreover:

**PROPOSITION 2.3 (SIMULATION FIDELITY).** In the context of run$_o$ and run$_m$, if $\mathbb{P} \subseteq \mathcal{L}$ we have that $\forall p \in 1...n$,

$$ \text{step}_o(\mathbb{P}, p, \rho_{p-1}) \mapsto \rho_p \Leftrightarrow \text{step}_m(\mathbb{Q}, p, \sigma_{p-1}, \mathbb{L}_{p-1}) \mapsto (\sigma_p, \mathbb{L}_p) $$

In particular, this property guarantees that a failure in the $\mathcal{O}$ run is matched by a failure in $\mathcal{M}$ at the same step. We consider this property very important from a practical point of view since it guarantees that the execution traces are strongly related, and in turn, this enables a user to debug a logic program in $\mathcal{O}$ by looking at its execution trace in $\mathcal{M}$.

We also claim that run$_m$ handles terms outside $\mathcal{L}$ in the following sense:

**PROPOSITION 2.4 (FIDELITY RECOVERY).** In the context of run$_o$ and run$_m$, if $\rho_{p-1}\mathbb{P}_p \subseteq \mathcal{L}$ (even if $\mathbb{P}_p \not\subseteq \mathcal{L}$) then

$$ \text{step}_o(\mathbb{P}, p, \rho_{p-1}) \mapsto \rho_p \Leftrightarrow \text{step}_m(\mathbb{Q}, p, \sigma_{p-1}, \mathbb{L}_{p-1}) \mapsto (\sigma_p, \mathbb{L}_p) $$

In other words, if the two terms involved in a step re-enter $\mathcal{L}$, then step$_m$ and step$_o$ are again related, even if $\mathbb{P} \not\subseteq \mathcal{L}$ and hence proposition 2.3 does not apply. Indeed, the main difference between proposition 2.3 and proposition 2.4 is that the assumption of the former is purely static, it can be checked upfront. When this assumption is not satisfied, one can still simulate a logic program and have guarantees of fidelity if, at run time, decidability of higher-order unification is restored.

This property has practical relevance since in many logic programming implementations, including Elpi, the order in which unification problems are tackled does matter. The simplest example is the sequence $F \approx \lambda x.a$ and $F a \approx a$: the second problem is not in $\mathcal{L}$ and has two unifiers, namely $\sigma_1 = \{F \mapsto \lambda x.x\}$ and $\sigma_2 = \{F \mapsto \lambda x.a\}$. The first problem picks $\sigma_2$, making the second problem re-enter $\mathcal{L}$.

**Backtracking.** We omit it from our model of logic-program execution since it plays a very minor role, orthogonal to higher-order unification. We point out that each run corresponds to a (proof search) branch in the logic program that either fails at some point, or succeeds. A computation that succeeds by backtracking, exploring multiple branches, could be modeled as a set of runs with a (possibly non-empty) common prefix.

## 2.4 The solution (in a nutshell)

A term $s$ is compiled to a term $t$ where every “problematic” subterm $e$ is replaced by a fresh unification variable $h$ with an accessory link that represents a suspended unification problem $h \approx_m e$. As a result,

$\approx_m$ is “well behaved” on $t$, in the sense that it does not contradict $=_o$ as it would otherwise do on the “problematic” sub-terms. We now define “problematic” and “well behaved” more formally. We use the $\diamond$ symbol since it stands for “possibly” in modal logic and all problematic terms are characterized by some uncertainty.

**Definition 2.5 ($\diamond\beta$).** $\diamond\beta$ is the set of terms of the form $F x_1...x_n$ such that $x_1...x_n$ are distinct names (of bound variables).

An example of a $\diamond\beta$ term is the application $F x$. This term is problematic since the application node of its syntax tree cannot be used to justify a unification failure, i.e. by properly instantiating $F$, the term head constructor may become a $\lambda$, or a constant, or a name, or remain an application.

**Definition 2.6 ($\diamond\eta$).** $\diamond\eta$ is the set of terms $\lambda x.s$ such that $\exists\rho, \rho(\lambda x.s)$ is an eta expansion.

An example of a term $s$ in $\diamond\eta$ is $\lambda x.\lambda y. F y x$ since the substitution $\rho = \{F \mapsto \lambda x.\lambda y. f y x\}$ makes $\rho s =_o \lambda x.\lambda y. f x y$, which is the eta-long form of $f$. This term is problematic since its leading $\lambda$ abstraction cannot justify a unification failure against a constant $f$.

**Definition 2.7 ($\diamond\mathcal{L}$).** $\diamond\mathcal{L}$ is the set of terms of the form $F \cdot t_1...t_n$ such that $t_1...t_n$ are not distinct names.

These terms are problematic for the very same reason terms in $\diamond\beta$ are, but they cannot be handled directly by the unification of the meta language, which is only required to handle terms in $\mathcal{L}$. Still, given $s \in \diamond\mathcal{L}$ there may exist a substitution $\rho$ such that $\rho s \in \mathcal{L}$.

We write $\mathcal{P}(t)$ for the set of sub-terms of $t$, and we write $\mathcal{P}(X) = \bigcup_{t \in X} \mathcal{P}(t)$ when $X$ is a set of terms.

**Definition 2.8 (Well behaved set).** Given a set of terms $X$,

$$ \mathcal{W}(X) \Leftrightarrow \forall t \in \mathcal{P}(X), t \notin (\diamond\beta \cup \diamond\eta \cup \diamond\mathcal{L}) $$

We write $\mathcal{W}(t)$ as a short for $\mathcal{W}(\{t\})$. We claim our compiler validates the following properties:

**PROPOSITION 2.9 (W-ENFORCING).** Given a term $s$ in $\mathcal{O}$,

$$ \langle s \rangle \mapsto (t, m, l) \Rightarrow \mathcal{W}(t) $$

**PROPOSITION 2.10 (COMPILER-USEFUL).** Given two terms $s_1$ and $s_2$, if $\exists\rho, \rho s_1 =_o \rho s_2$, then

$$ \langle s_i \rangle \mapsto (t_i, m_i, l_i) \text{ for } i \in \{1, 2\} \Rightarrow t_1 \approx_m t_2 \mapsto \sigma $$

In other words the compiler outputs terms in $\mathcal{W}$ even if its input is not. And if two terms can be unified in the source language then their images can also be unified in the target language. Note that the property holds for any substitution, not necessarily a most general one: when applied to terms in $\mathcal{W}$ the meta-language unification $\approx_m$ agrees with the object-language equality $=_o$. Note that a compiler that translate all terms to unification variables would satisfy this property, but wound certainly fail to verify proposition 2.3.

**PROPOSITION 2.11 (W-PRESERVATION).** $\forall \mathbb{Q}, \forall \mathbb{L}, \forall p, \forall \sigma, \forall \sigma'$

$$ \begin{aligned} \mathcal{W}(\sigma(\mathbb{Q}) \wedge \sigma(\mathbb{Q}_{p_1}) \approx_m \sigma(\mathbb{Q}_{p_r}) \mapsto \sigma') &\Rightarrow \mathcal{W}(\sigma'(\mathbb{Q})) \\ \mathcal{W}(\sigma(\mathbb{Q}) \wedge \text{progress}(\mathbb{L}, \sigma) \mapsto (\cdot, \sigma') &\Rightarrow \mathcal{W}(\sigma'(\mathbb{Q})) \end{aligned} $$

Proposition 2.11 is key to proving propositions 2.2 and 2.3. Informally, it says that the problematic terms moved on the side by the compiler are not reintroduced by step$_m$, hence $\approx_m$ can continue
the term and map one syntax tree to the other. In order to bring back the substitution from *M* to *O* the compiler builds a “memory map” connecting the *O* variables to the *M* ones.

The signature of the comp predicate below allows for the genera-
tion of links (suspended unification problems), which plays no role
in this section but plays a major role in sections 4, 5 and 7.

type comp to -> tm -> mmap -> mmap -> links -> links ->
    subst -> subst -> o.
comp (o-con C) (con C) M M L L S S.
comp (o-lam F) (lam F1) M1 M2 L1 L2 S1 S2 :-
    comp-lam F F1 M1 M2 L1 L2 S1 S2.
comp (o-uva A) (uva B[]) M1 M2 L L S1 S2 :-
    m-alloc (ov A) (mv B (arity z)) M1 M2 S1 S2.
comp (o-app A) (app A1) M1 M2 L1 L2 S1 S2 :-
    fold6 comp A1 M1 M2 L1 L2 S1 S2.
(cλ)

type compile to -> tm -> mmap -> mmap -> links -> links ->
    subst -> subst -> o.
compile F G M1 M2 L1 L2 S1 S2 :-
    beta-normal F F', comp F' G M1 M2 L1 L2 S1 S2.
(c@)

With respect to section 2, the signature also allows for updates to
the substitution. The code above uses that possibility in order to
allocate space for the variables, i.e. it sets their memory address to
none (a detail not worth mentioning in the previous sections).

type comp-lam (to -> to) -> (tm -> tm) ->
    mmap -> mmap -> links -> links -> subst -> subst -> o.
comp-lam F G M1 M2 L1 L3 S1 S2 :-
    pi x y\ (pi M L S\ comp x y M M L L S S) =>
        comp (F x) (G y) M1 M2 L1 (L2 y) S1 S2,
        close-links L2 L3.
(Hλ)

In the code above, the syntax pi x y\.. is syntactic sugar for it-
erated pi abstraction, as in pi x\ pi y\... The auxiliary predicate
fold6 folds a predicate with three accumulators (the memory map,
the links and the substitution) over a lists to obtain a new list and
the final values of the accumulators.

The auxiliary function close-links tests if the bound variable
v really occurs in the link. If it does, the link is wrapped into an
additional abs node binding v. In this way links generated deep
inside the compiled terms can be moved outside their original
context of binders.

type close-links (tm -> links) -> links -> o.
close-links (v\[X v|L v]) [abs X|R] :- close-links L R.
close-links (_\[] [].

**3.4 Execution**

A step in *M* consists in unifying two terms and reconsidering all
links for progress. If either of these tasks fails, we consider the
entire step to fail. It is at this granularity that we can relate steps in
the two languages.

type hstep tm -> tm -> links -> links -> subst -> subst -> o.
hstep T1 T2 L1 L2 S1 S3 :-
    (T1 ≅<sub>m</sub> T2) S1 S2,
    progress L1 L2 S2 S3.

Note that the infix notation ((A ≅<sub>m</sub> B) C D) is syntactic sugar for
((≈<sub>m</sub>) A B C D).

Reconsidering links is a fixpoint process because the progress of
a link can update the substitution, which may then enable another
link to progress.

type progress links -> links -> subst -> subst -> o.
progress L L3 S S3 :-
    progress1 L L1 S S1,
    occur-check-links L1,
    scope-check L1 L2 S1 S2
    if (L = L2, S = S2) (L3 = L2, S3 = S2)
        (progress L2 L3 S2 S3).

3.4.1 *Progress.* In the base compilation scheme, progress¹ is the identity function on both the links and the substitution, so the fixpoint trivially terminates. Sections 5 and 7 add rules to progress¹ and explain why the do not hinder termination.

3.4.2 *Scope check.* The predicate scope-check replaces each link of the form $\Gamma \vdash X_{x_1}...x_n =_\eta t$ with a link $x_1...x_n \vdash X_{x_1}...x_n =_\eta t'$ whenever $\{x_1...x_n\} \subset \Gamma$. The term $t' = \lambda x. Y_{x_1}...x_n x$ is obtained after executing $\lambda x. Y_{x_1}...x_n x \cong_m t$ using a fresh Y. This unification ensures that $t'$ cannot contain variables in $\Gamma / \{x_1...x_n\}$, and if it fails then progress hence step$_m$ fails. In turn this grants fidelity in the case where the rhs of an $\eta$-link is pruned of a name that occurs (rigidly) in t: links represent suspended unification problems that may succeed.

3.4.3 *Occur check.* Since compilation moves problematic terms out of the sight of $\cong_m$, that procedure can only perform a partial occur check. For example, the unification problem $X \cong_m f Y$ cannot generate a cyclic substitution alone, but should be disallowed if $L$ contains a link like $\vdash Y =_\eta \lambda z.Xz$: we don't know yet if $Y$ will feature a lambda in head position, but we surely know it contains $X$. The procedure occur-check-links is in charge of performing this check that is needed in order to guarantee proposition 2.3 (SIMULATION FIDELITY).

**3.5 Substitution decompilation**

Decompiling the substitution involves three steps.

First and foremost, problematic terms stored in $L$ have to be
moved back into the game: a suspended link must be turned into
a valid assignment. This operation is possible thanks to invari-
ant 2 (LINK LEFT HAND SIDE), and that no link causes an occur-
check (3.4.3) and the fact that $L$ is duplicate-free (see section 6).

The second step allocates in the memory of *O* new variables used
to implement the pruning of higher-order variables. For example,
$F x y = F x z$ requires allocating a variable *G* in order to express
the assignment $F_{ab} \mapsto G_a$.

The final step is to decompile each assignment. The val node
carries a term that is easy to decompile since *M* is a bijection. Since
the o-lam node carries no additional information (other than the
function body), each abs node can be decompiled to a o-lam one.

However, if the o-lam node was carrying more information, as
is the case for Coq where it holds the type of the bound variable,
one would need to store this piece of information in the memory
map, were we store the arity (that is a very simple function type).
the term and map one syntax tree to the other. In order to bring back the substitution from *M* to *O* the compiler builds a “memory map” connecting the *O* variables to the *M* ones.

The signature of the comp predicate below allows for the genera-
tion of links (suspended unification problems), which plays no role
in this section but plays a major role in sections 4, 5 and 7.

type comp to -> tm -> mmap -> mmap -> links -> links ->
    subst -> subst -> o.
comp (o-con C) (con C) M M L L S S.
comp (o-lam F) (lam F1) M1 M2 L1 L2 S1 S2 :- (c_λ)
comp-lam F F1 M1 M2 L1 L2 S1 S2.
comp (o-uva A) (uva B[]) M1 M2 L L S1 S2 :-
    m-alloc (ov A) (mv B (arity z)) M1 M2 S1 S2.
comp (o-app A) (app A1) M1 M2 L1 L2 S1 S2 :-
    fold6 comp A1 M1 M2 L1 L2 S1 S2.
(c@)

type compile to -> tm -> mmap -> mmap -> links -> links ->
    subst -> subst -> o.
compile F G M1 M2 L1 L2 S1 S2 :-
    beta-normal F F', comp F' G M1 M2 L1 L2 S1 S2.

With respect to section 2, the signature also allows for updates to
the substitution. The code above uses that possibility in order to
allocate space for the variables, i.e. it sets their memory address to
none (a detail not worth mentioning in the previous sections).

type comp-lam (to -> to) -> (tm -> tm) ->
    mmap -> mmap -> links -> links -> subst -> subst -> o.
comp-lam F G M1 M2 L1 L3 S1 S2 :-
    pi x y\ (pi M L S\ comp x y M M L L S S) => (H_λ)
    comp (F x) (G y) M1 M2 L1 (L2 y) S1 S2,
    close-links L2 L3.

In the code above, the syntax pi x y\.. is syntactic sugar for it-
erated pi abstraction, as in pi x\ pi y\... . The auxiliary predicate
fold6 folds a predicate with three accumulators (the memory map,
the links and the substitution) over a lists to obtain a new list and
the final values of the accumulators.

The auxiliary function close-links tests if the bound variable
v really occurs in the link. If it does, the link is wrapped into an
additional abs node binding v. In this way links generated deep
inside the compiled terms can be moved outside their original
context of binders.

type close-links (tm -> links) -> links -> o.
close-links (v\[X v|L v]) [abs X|R] :- close-links L R.
close-links (_\[] [] .

3.4 Execution

A step in *M* consists in unifying two terms and reconsidering all
links for progress. If either of these tasks fails, we consider the
entire step to fail. It is at this granularity that we can relate steps in
the two languages.

type hstep tm -> tm -> links -> links -> subst -> subst -> o.
hstep T1 T2 L1 L2 S1 S3 :-
    (T1 ≈_m T2) S1 S2,
    progress L1 L2 S2 S3.

Note that the infix notation ((A ≈_m B) C D) is syntactic sugar for
((≈_m) A B C D). 639
640

Reconsidering links is a fixpoint process because the progress of
a link can update the substitution, which may then enable another
link to progress.

type progress links -> links -> subst -> subst -> o.
progress L L3 S S3 :-
    progress1 L L1 S S1,
    occur-check-links L1,
    scope-check L1 L2 S1 S2
    if (L = L2, S = S2) (L3 = L2, S3 = S2)
        (progress L2 L3 S2 S3).

3.4.1 *Progress.* In the base compilation scheme, progress¹ is the identity function on both the links and the substitution, so the fixpoint trivially terminates. Sections 5 and 7 add rules to progress¹ and explain why the do not hinder termination.

3.4.2 *Scope check.* The predicate scope-check replaces each link of the form $\Gamma \vdash X_{x_1}...x_n =_\eta t$ with a link $x_1...x_n \vdash X_{x_1}...x_n =_\eta t'$ whenever $\{x_1...x_n\} \subset \Gamma$. The term $t' = \lambda x. Y_{x_1}...x_n x$ is obtained after executing $\lambda x. Y_{x_1}...x_n x \approx_m t$ using a fresh $Y$. This unification ensures that $t'$ cannot contain variables in $\Gamma / \{x_1...x_n\}$, and if it fails then progress hence step$_m$ fails. In turn this grants fidelity in the case where the rhs of an $\eta$-link is pruned of a name that occurs (rigidly) in $t$: links represent suspended unification problems that may succeed.

3.4.3 *Occur check.* Since compilation moves problematic terms out of the sight of ≈<sub>m</sub>, that procedure can only perform a partial occur check. For example, the unification problem X ≈<sub>m</sub> f Y cannot generate a cyclic substitution alone, but should be disallowed if L contains a link like ⊢ Y =<sub>η</sub> λz.Xz: we don't know yet if Y will feature a lambda in head position, but we surely know it contains X. The procedure occur-check-links is in charge of performing this check that is needed in order to guarantee proposition 2.3 (SIMULATION FIDELITY).

3.5 Substitution decompilation

Decompiling the substitution involves three steps.

First and foremost, problematic terms stored in L have to be
moved back into the game: a suspended link must be turned into
a valid assignment. This operation is possible thanks to invari-
ant 2 (LINK LEFT HAND SIDE), and that no link causes an occur-
check (3.4.3) and the fact that L is duplicate-free (see section 6).

The second step allocates in the memory of *O* new variables used
to implement the pruning of higher-order variables. For example,
F x y = F x z requires allocating a variable *G* in order to express
the assignment *F*<sub>*ab*</sub> ↦ *G*<sub>*a*</sub>.

The final step is to decompile each assignment. The val node
carries a term that is easy to decompile since M is a bijection. Since
the o-lam node carries no additional information (other than the
function body), each abs node can be decompiled to a o-lam one.

However, if the o-lam node was carrying more information, as
is the case for Coq where it holds the type of the bound variable,
one would need to store this piece of information in the memory
map, were we store the arity (that is a very simple function type).
**PROPOSITION 3.1 (COMPILATION ROUND TRIP).** If $\langle s \rangle \mapsto (t, m, l)$ and $l \in \mathbb{L}$ and $m \in \mathcal{M}$ and $\sigma = \{A \mapsto t\}$ and $X \mapsto A^n \in \mathcal{M}$ then $\langle \sigma, \mathcal{M}, \mathbb{L} \rangle^{-1} \mapsto \rho$ and $\rho X =_o \rho s$.

We omit to sketch the proof of this property for brevity.

## 3.6 Definition of $\approx_o$ and its properties

We already have all the ingredients to show the code of $\approx_o$.

type ($\approx_o$) to -> to -> fsubst -> o.

(A $\approx_o$ B) F :-
compile A A' [] M1 [] L1 [] S1,
compile B B' M1 M2 L1 L2 S1 S2,
hstep A' B' L2 L3 S2 S3,
decompile M2 L3 S3 [] F.

So far the compiler is very basic. It does not really enforce that the terms passed to step$_m$ are in $\mathcal{W}$, and indeed makes no use of the higher-order capabilities of the meta language (all generated variables have an empty scope). Still, we can prove that $\approx_o$ is a good “first-order” unification algorithm if the input already happens to be in $\mathcal{W}$. Later, when the compiler will ensure proposition 2.9 (W-ENFORCING), the proof will be refined to cover for the new cases.

**THEOREM 3.2 (PROPERTIES OF $\approx_o$ IN $\mathcal{W}$).** The implementation of $\approx_o$ above is a good unification for $=o$ (as per proposition 2.1) in the domain $\mathcal{W}$.

**PROOF SKETCH.** In this setting, $=m$ is as strong as $=o$ on ground terms. What we have to show is that whenever two different $\mathcal{O}$ terms can be made equal by a substitution $\rho$, we can produce this $\rho$ by finding a $\sigma$ via $\approx_m$ on the corresponding $\mathcal{M}$ terms and by decompiling it. If we look at the syntax of $\mathcal{O}$, the only interesting case is «o-uva $X \approx_o s$». In this case, after compilation, we have «uva $Y$ [] $\approx_m$ $t$» that succeeds with $\sigma = \{Y \mapsto t\}$ and $\sigma$ is decompiled to $\rho = \{X \mapsto s\}$ by proposition 3.1. □

**THEOREM 3.3 (FIDELITY IN $\mathcal{W}$).** Proposition 2.2 (RUN EQUIVALENCE) and proposition 2.3 (SIMULATION FIDELITY) hold if $\mathcal{W}(\mathbb{P})$.

**PROOF SKETCH.** Since progress is a no-op then step$_o$ and step$_m$ are the same. By theorem 3.2, $\approx_m$ is equivalent to $\approx_o$ in $\mathcal{W}$. □

## 3.7 Notational conventions

In the following sections we use the following notation for input and output of the compiler. $\mathbb{P}$ represents the input unification problems in $\mathcal{O}$ while $\mathbb{Q}$ their corresponding compiled version with memory mapping $\mathcal{M}$ and links $\mathbb{L}$. For example:

$$ 
\begin{align*}
\mathbb{P} &= \{ p_1 \approx_o p_2 \quad p_3 \approx_o p_4 \} \\
\mathbb{Q} &= \{ t_1 \approx_m t_2 \quad t_3 \approx_m t_4 \} \\
\mathcal{M} &= \{ X_1 \mapsto A_1^n \quad X_2 \mapsto A_2^m \} \\
\mathcal{L} &= \{ \Gamma \vdash a =_\eta b \}
\end{align*}
$$

We index each sub-problem, sub-mapping, and sub-link with its position starting from 1 and counting from left to right, top to bottom. For example, $\mathbb{Q}_2$ corresponds to the $\mathcal{M}$ problem $t_3 \approx_m t_4$.

As we deal with each category of problematic terms we weaken the assumptions of theorem 3.3 using the following definitions:

**Definition 3.4 ($\mathcal{W}_\beta$).** $\mathcal{W}_\beta(X) \Leftrightarrow \forall t \in \mathcal{P}(X), t \notin (\diamond\eta \cup \diamond\mathcal{L})$

**Definition 3.5 ($\mathcal{W}_{\beta\eta}$).** $\mathcal{W}_{\beta\eta}(X) \Leftrightarrow \forall t \in \mathcal{P}(X), t \notin \diamond\mathcal{L}$

# 4 HANDLING OF $\diamond\beta$

The basic compiler given in the previous section is unable to make the following higher-order unification problem succeed.

$$ 
\begin{align*}
\mathbb{P} &= \{ \lambda x.(f(X x) a) \approx_o \lambda x.(f x a) \} \\
\mathbb{Q} &= \{ \lambda x.(f(A x) a) \approx_m \lambda x.(f x a) \} \\
\mathcal{M} &= \{ X \mapsto A^0 \}
\end{align*}
$$

The unification problem $\mathbb{Q}_1$ fails while trying to unify $A x$ and $x$, which is equivalent to «app [uva A [], x]» versus $x$. In order to exploit the higher-order unification algorithm of the meta language, we compile the $\mathcal{O}$ term $X x$ into the $\mathcal{M}$ term $A_x$.

## 4.1 Compilation and decompilation

We add the following rule before rule (c$_@$), where pattern-fragment is a predicate checking if a list of terms is a list of distinct names.

comp (o-app [o-uva A|Ag]) (uva B Ag1) M1 M2 L L S1 S2 :-
pattern-fragment Ag, !,
fold6 comp Ag Ag1 M1 M1 L L S1 S1,
len Ag Arity,
m-alloc (ov A) (mv B (arity Arity)) M1 M2 S1 S2.

Note that compiling $Ag$ cannot create new mappings nor links, since $Ag$ is made of bound variables, and the hypothetical rule $(H_\lambda)$ loaded by comp-lam grants this property.

**Decompilation.** No change to commit-link since no link is added.

**Progress.** No change to progress since no link is added.

**LEMMA 4.1 (PROPERTIES OF $\approx_o$ IN $\mathcal{W}_\beta$).** Given the updated compilation scheme, the $\approx_o$ of section 3.6 is a good unification (as per proposition 2.1) for $=o$ in the domain $\mathcal{W}_\beta$.

**PROOF SKETCH.** If we look at the $\mathcal{O}$ terms, there is one more interesting case, namely o-app[o-uva X|W] $\approx_o$ s when W are distinct names compiled to $\tilde{w}$. In this case the $\mathcal{M}$ problem is $Y_{\tilde{w}} \approx_m t$ that succeeds with $\sigma = \{Y_{\tilde{y}} \mapsto t[\tilde{w}/\tilde{y}]\}$, which in turn is decompiled to $\rho = \{Y \mapsto \lambda_{\tilde{y}}.s[\tilde{w}/\tilde{y}]\}$. Thanks to $\beta_l$ we have $(\lambda_{\tilde{y}}.s[\tilde{w}/\tilde{y}]) \tilde{w} =_o s$. □

**LEMMA 4.2 (W-PARTIAL-ENFORCEMENT).** $\forall s, \langle s \rangle \mapsto (t, m, l)$, if $\mathcal{W}_\beta(s)$ then $\mathcal{W}(t)$.

In other words the compiler eliminates all subterms that are in $\diamond\beta$.

**THEOREM 4.3 (FIDELITY IN $\mathcal{W}_\beta$).** Proposition 2.2 (RUN EQUIVALENCE) and proposition 2.3 (SIMULATION FIDELITY) hold if $\mathcal{W}_\beta(\mathbb{P})$.

**PROOF SKETCH.** Thanks to lemma 4.2, $\approx_m$ is as powerful as $\approx_o$ in $\mathcal{W}_\beta$, as well as in $\mathcal{W}$ by theorem 3.3. □

# 5 HANDLING OF $\diamond\eta$

A term $\lambda x.t x$ is said to be the $\eta$-redex of $t$ if $x$ does not occur free in $t$, and conversely we say that $t$ is the $\eta$-contraction of $\lambda x.t x$. The equational theory of $\mathcal{O}$ identifies these terms, but the current compilation scheme does not, as shown by the following example:
**PROPOSITION 3.1 (COMPILATION ROUND TRIP).** If $\langle s \rangle \mapsto (t, m, l)$ and $l \in \mathbb{L}$ and $m \in \mathbb{M}$ and $\sigma = \{A \mapsto t\}$ and $X \mapsto A^n \in \mathbb{M}$ then $\langle \sigma, \mathbb{M}, \mathbb{L} \rangle^{-1} \mapsto \rho$ and $\rho X =_o \rho s$.

We omit to sketch the proof of this property for brevity.

## 3.6 Definition of $\approx_o$ and its properties

We already have all the ingredients to show the code of $\approx_o$.

```
type (\approx_o) to -> to -> fsubst -> o.
(A \approx_o B) F :-
    compile A A' [] M1 [] L1 [] S1,
    compile B B' M1 M2 L1 L2 S1 S2,
    hstep A' B' L2 L3 S2 S3,
    decompile M2 L3 S3 [] F.
```

So far the compiler is very basic. It does not really enforce that the terms passed to step<sub>m</sub> are in W, and indeed makes no use of the higher-order capabilities of the meta language (all generated variables have an empty scope). Still, we can prove that $\approx_o$ is a good “first-order” unification algorithm if the input already happens to be in W. Later, when the compiler will ensure proposition 2.9 (W-ENFORCING), the proof will be refined to cover for the new cases.

**THEOREM 3.2 (PROPERTIES OF $\approx_o$ IN W).** *The implementation of $\approx_o$ above is a good unification for $=o$ (as per proposition 2.1) in the domain W.*

**PROOF SKETCH.** In this setting, $=m$ is as strong as $=o$ on ground terms. What we have to show is that whenever two different O terms can be made equal by a substitution $\rho$, we can produce this $\rho$ by finding a $\sigma$ via $\approx_m$ on the corresponding M terms and by decompiling it. If we look at the syntax of O, the only interesting case is «o-uva X $\approx_o$ s». In this case, after compilation, we have «uva Y [] $\approx_m$ t» that succeeds with $\sigma = \{Y \mapsto t\}$ and $\sigma$ is decompiled to $\rho = \{X \mapsto s\}$ by proposition 3.1. □

**THEOREM 3.3 (FIDELITY IN W).** *Proposition 2.2 (RUN EQUIVALENCE) and proposition 2.3 (SIMULATION FIDELITY) hold if W(\mathbb{P}).*

**PROOF SKETCH.** Since progress is a no-op then step<sub>o</sub> and step<sub>m</sub> are the same. By theorem 3.2, $\approx_m$ is equivalent to $\approx_o$ in W. □

## 3.7 Notational conventions

In the following sections we use the following notation for input and output of the compiler. P represents the input unification problems in O while Q their corresponding compiled version with memory mapping M and links L. For example:

```
P = \{ p_1 \approx_o p_2 \quad p_3 \approx_o p_4 \}
Q = \{ t_1 \approx_m t_2 \quad t_3 \approx_m t_4 \}
M = \{ X_1 \mapsto A_1^n \quad X_2 \mapsto A_2^m \}
L = \{ \Gamma \vdash a =_\eta b \}
```

We index each sub-problem, sub-mapping, and sub-link with its position starting from 1 and counting from left to right, top to bottom. For example, $\mathbb{Q}_2$ corresponds to the M problem $t_3 \approx_m t_4$.

As we deal with each category of problematic terms we weaken the assumptions of theorem 3.3 using the following definitions:

**Definition 3.4 (W<sub>β</sub>).** $W_{\beta}(X) \Leftrightarrow \forall t \in \mathcal{P}(X), t \notin (\diamond\eta \cup \diamond\mathcal{L})$

**Definition 3.5 (W<sub>βη</sub>).** $W_{\beta\eta}(X) \Leftrightarrow \forall t \in \mathcal{P}(X), t \notin \diamond\mathcal{L}$

# 4 HANDLING OF ♦β

The basic compiler given in the previous section is unable to make the following higher-order unification problem succeed.

```
P = \{ \lambda x.(f(X x) a) \approx_o \lambda x.(f x a) \}
Q = \{ \lambda x.(f(A x) a) \approx_m \lambda x.(f x a) \}
M = \{ X \mapsto A^0 \}
```

The unification problem $\mathbb{Q}_1$ fails while trying to unify A x and x, which is equivalent to «app [uva A [], x]» versus x. In order to exploit the higher-order unification algorithm of the meta language, we compile the O term X x into the M term $A_x$.

## 4.1 Compilation and decompilation

We add the following rule before rule (c<sub>@</sub>), where pattern-fragment is a predicate checking if a list of terms is a list of distinct names.

```
comp (o-app [o-uva A|Ag]) (uva B Ag1) M1 M2 L L S1 S2 :-
pattern-fragment Ag, !,
fold6 comp Ag Ag1 M1 M1 L L S1 S1,
len Ag Arity,
m-alloc (ov A) (mv B (arity Arity)) M1 M2 S1 S2.
```

Note that compiling Ag cannot create new mappings nor links, since Ag is made of bound variables, and the hypothetical rule ($H_\lambda$) loaded by comp-lam grants this property.

**Decompilation.** No change to commit-link since no link is added.

**Progress.** No change to progress since no link is added.

**LEMMA 4.1 (PROPERTIES OF $\approx_o$ IN W<sub>β</sub>).** *Given the updated compilation scheme, the $\approx_o$ of section 3.6 is a good unification (as per proposition 2.1) for $=o$ in the domain W<sub>β</sub>.*

**PROOF SKETCH.** If we look at the O terms, there is one more interesting case, namely o-app[o-uva X|W] $\approx_o$ s when W are distinct names compiled to $\tilde{w}$. In this case the M problem is $Y_{\tilde{w}} \approx_m t$ that succeeds with $\sigma = \{Y_{\tilde{y}} \mapsto t[\tilde{w}/\tilde{y}]\}$, which in turn is decompiled to $\rho = \{Y \mapsto \lambda_{\tilde{y}}.s[\tilde{w}/\tilde{y}]\}$. Thanks to $\beta_l$ we have $(\lambda_{\tilde{y}}.s[\tilde{w}/\tilde{y}]) \tilde{w} =_o s$. □

**LEMMA 4.2 (W-PARTIAL-ENFORCEMENT).** $\forall s, \langle s \rangle \mapsto (t, m, l)$, if W<sub>β</sub>(s) then W(t).

In other words the compiler eliminates all subterms that are in ♦β.

**THEOREM 4.3 (FIDELITY IN W<sub>β</sub>).** *Proposition 2.2 (RUN EQUIVALENCE) and proposition 2.3 (SIMULATION FIDELITY) hold if W<sub>β</sub>(\mathbb{P}).*

**PROOF SKETCH.** Thanks to lemma 4.2, $\approx_m$ is as powerful as $\approx_o$ in W<sub>β</sub>, as well as in W by theorem 3.3. □

# 5 HANDLING OF ♦η

A term $\lambda x.t x$ is said to be the $\eta$-expansion of t if x does not occur free in t, and conversely we say that t is the $\eta$-contraction of $\lambda x.t x$. The equational theory of O identifies these terms, but the current compilation scheme does not, as shown by the following example:

755

756

757

758

759

760

761

762

763

764

765

766

767

768

769

770

771

772

773

774

775

776

777

778

779

780

781

782

783

784

785

786

787

788

789

790

791

792

793

794

795

796

797

798

799

800

801

802

803

804

805

806

807

808

809

810

811

812

813

814

815

816

817
while $\lambda x.X x \approx_o f$ does admit the solution $\rho = \{ X \mapsto f \}$, the corresponding problem in $\mathbb{Q}$ does not.

$$ 
\begin{aligned}
\mathbb{P} &= \{ \lambda x.X x \approx_o f \} \\
\mathbb{Q} &= \{ \lambda x.A_x \approx_m f \} \\
\mathbb{M} &= \{ X \mapsto A^1 \}
\end{aligned}
 $$

The reason is that «lam x\ uva A [x]» and «con"f» start with different term constructors.

In order to guarantee proposition 2.2, we detect lambda abstractions that can disappear by $\eta$-contraction (section 5.1), and we modify the compiler so that it generates fresh unification variables in their place and moves the problematic term from $\mathbb{Q}$ to $\mathbb{L}$ (section 5.2). The compilation of the problem $\mathbb{P}$ above is refined to:

$$ 
\begin{aligned}
\mathbb{P} &= \{ \lambda x.X x \approx_o f \} \\
\mathbb{Q} &= \{ A \approx_m f \} \\
\mathbb{M} &= \{ X \mapsto B^1 \} \\
\mathbb{L} &= \{ \vdash A =_\eta \lambda x.B_x \}
\end{aligned}
 $$

As per invariant 2 the $\eta$-link left-hand side is a variable while the right-hand side is a term in $\diamond\eta$ that has the following property:

**INvariant 3 ($\eta$-link RHS).** The rhs of any $\eta$-link has the shape $\lambda x.t$ and $t$ is in $\mathbb{W}$.

Each $\eta$-link is kept in the link store $\mathbb{L}$ during execution and is activated under some conditions. Activation is implemented in section 5.3 by extending the progress predicate defined in section 3.4.

## 5.1 Detection of $\diamond\eta$

When compiling a term $t$, we need to determine if any subterm $s \in \mathcal{P}(t)$ that is of the form $\lambda x.r$ can be an $\eta$-redex, i.e. if there exists a substitution $\rho$ such that $\rho(\lambda x.r) =_o s$. The detection of lambda abstractions that can “disappear” is not as trivial as it may seems. Here a few examples:

$$ 
\begin{aligned}
\lambda x.f (A x) &\in \diamond\eta \quad \rho = \{ A \mapsto \lambda x.x \} \\
\lambda x.f (A x) x &\in \diamond\eta \quad \rho = \{ A \mapsto \lambda x.a \} \\
\lambda x.f (A x) &\notin \diamond\eta \\
\lambda x.\lambda y.f (A x) (B y x) &\in \diamond\eta \quad \rho = \{ A \mapsto \lambda x.x ; B \mapsto \lambda y.\lambda x.y \}
\end{aligned}
 $$

The first two examples are easy, and show how a unification variable can expose or erase a variable in its scope, turning the resulting term into an $\eta$-redex or not.

The third example shows that when a variable occurs outside the scope of a unification variable, it cannot be erased and can hence prevent a term from being an $\eta$-redex.

The last example shows the recursive nature of the check we need to implement. The term starts with a spine of two lambdas, hence the whole term is in $\diamond\eta$ iff the inner term $\lambda y.f (A x) (B y x)$ is in $\diamond\eta$ itself. If it is, it could $\eta$-contract to $f (A x)$ making $\lambda x.f (A x)$ a potential $\eta$-redex.

We can now detail how $\diamond\eta$ terms are detected.

**Definition 5.1 (may-contract-to).** A $\beta$-normal term $s$ may-contract-to a name $x$ if there exists a substitution $\rho$ such that $\rho s =_o x$.

**Lemma 5.2.** A $\beta$-normal term $s = \lambda x_1 \dots x_n.t$ may-contract-to $x$ only if one of the following three conditions holds:

$$ (1) n = 0 \text{ and } t = x; $$

(2) $t$ is the application of $x$ to a list of terms $l$ and each $l_i$ may-contract-to $x_i$ (e.g. $\lambda x_1 \dots x_n.x x_1 \dots x_n =_o x$);

(3) $t$ is a unification variable with scope $W$, and for any $v \in \{x, x_1 \dots x_n\}$, there exists a $w \in W$, such that $w$ may-contract-to $v$ (if $n = 0$ this is equivalent to $x \in W$).

**PROOF SKETCH.** Since our terms are in $\beta$-normal form the only rule that can play a role is $\eta_1$, and note that that rule uses $\beta$-to add an argument to an application or to the scope of a variable. If the term $s$ is not exactly $x$ (case 1) it can only be an $\eta$-redex of $x$, or a unification variable that can be assigned to $x$, or a combination of both. If $s$ begins with a lambda, then the lambda can only disappear by $\eta$ contraction. In that case, the term $t$ under the spine of binders $x_1 \dots x_n$ can either be $x$ applied to terms that may-contract-to these variables (case 2), or a unification variable that can be assigned to the application $x x_1 \dots x_n$ (case 3). $\square$

**Definition 5.3 (occurs-rigidly).** A name $x$ occurs-rigidly in a $\beta$-normal term $t$, if $\forall \rho, x \in \mathcal{P}(\rho t)$

In other words, $x$ occurs-rigidly in $t$ if it occurs in $t$ outside of the scope of a unification variable $X$; otherwise, an instantiation of $X$ can make $x$ disappears from $t$. Note that $\eta$-contracting $t$ cannot make $x$ disappear, since $x$ is not a locally bound variable inside $t$.

We can now describe the implementation of $\diamond\eta$ detection:

**Definition 5.4 (maybe-eta).** Given a $\beta$-normal term $s = \lambda x_1 \dots x_n.t$, maybe-eta $s$ holds if any of the following holds:

(1) $t$ is a constant $c$ or a name $y$ applied to the arguments $l_1 \dots l_m$ such that $m \ge n$ and for every $i$ such that $m - n < i \le m$ the term $l_i$ may-contract-to $x_i$, and no $x_i$ occurs-rigidly in $l_1 \dots l_{m-n} y$;

(2) $t$ is a unification variable with scope $W$ and for each $x_i$ there exists a $w_j \in W$ such that $w_j$ may-contract-to $x_i$.

**Lemma 5.5 ($\diamond\eta$ DETECTION).** If $t$ is a $\beta$-normal term and $t \in \diamond\eta$ then maybe-eta $t$ holds.

**PROOF SKETCH.** Follows from definition 5.3 and lemma 5.2 $\square$

Remark that the converse of lemma 5.5 does not hold: there exists a term $t$ satisfying the criteria (1) of definition 5.4 that is not in $\diamond\eta$, i.e. there exists no substitution $\rho$ such that $\rho t$ is an $\eta$-redex. A simple counter example is $\lambda x.f (A x) (A x)$ since $x$ does not occur-rigidly in the first argument of $f$, and the second argument of $f$ may-contract-to $x$. In other words $A x$ may either use or discard $x$, but our analysis does not take into account that the same term cannot have two contrasting behaviors.

As we will see in the rest of this section, this is not a problem since it does not break proposition 2.2 nor proposition 2.3.

## 5.2 Compilation and decompilation

**Compilation.** The following rule is inserted just before rule (c$_{\lambda}$) from the code in section 3.3.

comp (o-lam F) (uva A Scope) M1 M2 L1 L3 S1 S3 :-
maybe-eta (o-lam F) [], !,
alloc S1 A S2,
comp-lam F F1 M1 M2 L1 L2 S2 S3,
get-scope (lam F1) Scope,
L3 = [val (link-eta (uva A Scope) (lam F1)) | L2].
813

814

815

816

817

818

819

820

821

822

823

824

825

826

827

828

829

830

831

832

833

834

835

836

837

838

839

840

841

842

843

844

845

846

847

848

849

850

851

852

853

854

855

856

857

858

859

860

861

862

863

864

865

866

867

868

869

870

while $\lambda x.X x \approx_o f$ does admit the solution $\rho = \{ X \mapsto f \}$, the corresponding problem in $\mathbb{Q}$ does not.

$$ \mathbb{P} = \{ \lambda x.X x \approx_o f \} $$

$$ \mathbb{Q} = \{ \lambda x.A_x \approx_m f \} $$

$$ \mathbb{M} = \{ X \mapsto A^1 \} $$

The reason is that «lam x\ uva A [x]» and «con"f"» start with different term constructors.

In order to guarantee proposition 2.2, we detect lambda abstractions that can disappear by $\eta$-contraction (section 5.1), and we modify the compiler so that it generates fresh unification variables in their place and moves the problematic term from $\mathbb{Q}$ to $\mathbb{L}$ (section 5.2). The compilation of the problem $\mathbb{P}$ above is refined to:

$$ \mathbb{P} = \{ \lambda x.X x \approx_o f \} $$

$$ \mathbb{Q} = \{ A \approx_m f \} $$

$$ \mathbb{M} = \{ X \mapsto B^1 \} $$

$$ \mathbb{L} = \{ \vdash A =_\eta \lambda x.B_x \} $$

As per invariant 2 the $\eta$-link left-hand side is a variable while the right-hand side is a term in $\diamond\eta$ that has the following property:

**INvariant 3 ($\eta$-link RHS).** The rhs of any $\eta$-link has the shape $\lambda x.t$ and $t$ is in $\mathbb{W}$.

Each $\eta$-link is kept in the link store $\mathbb{L}$ during execution and is activated under some conditions. Activation is implemented in section 5.3 by extending the progress predicate defined in section 3.4.

## 5.1 Detection of $\diamond\eta$

When compiling a term $t$, we need to determine if any subterm $s \in \mathcal{P}(t)$ that is of the form $\lambda x.r$ can be an $\eta$-expansion, i.e. if there exists a substitution $\rho$ such that $\rho(\lambda x.r) =_o s$. The detection of lambda abstractions that can “disappear” is not as trivial as it may seems. Here a few examples:

$$ \lambda x.f (A x) \qquad \in \diamond\eta \qquad \rho = \{ A \mapsto \lambda x.x \} $$

$$ \lambda x.f (A x) x \qquad \in \diamond\eta \qquad \rho = \{ A \mapsto \lambda x.a \} $$

$$ \lambda x.f (A x) \qquad \notin \diamond\eta $$

$$ \lambda x.\lambda y.f (A x) (B y x) \qquad \in \diamond\eta \qquad \rho = \{ A \mapsto \lambda x.x ; B \mapsto \lambda y.\lambda x.y \} $$

The first two examples are easy, and show how a unification variable can expose or erase a variable in its scope, turning the resulting term into an $\eta$-expansion or not.

The third example shows that when a variable occurs outside the scope of a unification variable, it cannot be erased and can hence prevent a term from being an $\eta$-expansion.

The last example shows the recursive nature of the check we need to implement. The term starts with a spine of two lambdas, hence the whole term is in $\diamond\eta$ iff the inner term $\lambda y.f (A x) (B y x)$ is in $\diamond\eta$ itself. If it is, it could $\eta$-contract to $f (A x)$ making $\lambda x.f (A x)$ a potential $\eta$-expansion.

We can now detail how $\diamond\eta$ terms are detected.

**Definition 5.1 (may-contract-to).** A $\beta$-normal term $s$ may-contract-to a name $x$ if there exists a substitution $\rho$ such that $\rho s =_o x$.

**Lemma 5.2.** A $\beta$-normal term $s = \lambda x_1 \dots x_n.t$ may-contract-to $x$ only if one of the following three conditions holds:

$$ (1) \quad n = 0 \text{ and } t = x; $$

(2) $t$ is the application of $x$ to a list of terms $l$ and each $l_i$ may-contract-to $x_i$ (e.g. $\lambda x_1 \dots x_n.x x_1 \dots x_n =_o x$);

871

872

873

874

875

876

877

878

879

880

881

882

883

884

885

886

887

888

889

890

891

892

893

894

895

896

897

898

899

900

901

902

903

904

905

906

907

908

909

910

911

912

913

914

915

916

917

918

919

920

921

922

923

924

925

926

927

928

**PROOF SKETCH.** Since our terms are in $\beta$-normal form the only rule that can play a role is $\eta_1$, and note that that rule uses beta to add an argument to an application or to the scope of a variable. If the term $s$ is not exactly $x$ (case 1) it can only be an $\eta$-expansion of $x$, or a unification variable that can be assigned to $x$, or a combination of both. If $s$ begins with a lambda, then the lambda can only disappear by $\eta$ contraction. In that case, the term $t$ under the spine of binders $x_1 \dots x_n$ can either be $x$ applied to terms that may-contract-to these variables (case 2), or a unification variable that can be assigned to the application $x x_1 \dots x_n$ (case 3). $\square$

**Definition 5.3 (occurs-rigidly).** A name $x$ occurs-rigidly in a $\beta$-normal term $t$, if $\forall \rho, x \in \mathcal{P}(\rho t)$

In other words, $x$ occurs-rigidly in $t$ if it occurs in $t$ outside of the scope of a unification variable $X$; otherwise, an instantiation of $X$ can make $x$ disappears from $t$. Note that $\eta$-contracting $t$ cannot make $x$ disappear, since $x$ is not a locally bound variable inside $t$.

We can now describe the implementation of $\diamond\eta$ detection:

**Definition 5.4 (maybe-eta).** Given a $\beta$-normal term $s = \lambda x_1 \dots x_n.t$, maybe-eta $s$ holds if any of the following holds:

(1) $t$ is a constant $c$ or a name $y$ applied to the arguments $l_1 \dots l_m$ such that $m \ge n$ and for every $i$ such that $m - n < i \le m$ the term $l_i$ may-contract-to $x_i$, and no $x_i$ occurs-rigidly in $l_1 \dots l_{m-n} y$;

(2) $t$ is a unification variable with scope $W$ and for each $x_i$ there exists a $w_j \in W$ such that $w_j$ may-contract-to $x_i$.

**Lemma 5.5 ($\diamond\eta$ DETECTION).** If $t$ is a $\beta$-normal term and $t \in \diamond\eta$ then maybe-eta $t$ holds.

**PROOF SKETCH.** Follows from definition 5.3 and lemma 5.2 $\square$

Remark that the converse of lemma 5.5 does not hold: there exists a term $t$ satisfying the criteria (1) of definition 5.4 that is not in $\diamond\eta$, i.e. there exists no substitution $\rho$ such that $\rho t$ is an $\eta$-expansion. A simple counter example is $\lambda x.f (A x) (A x)$ since $x$ does not occur-rigidly in the first argument of $f$, and the second argument of $f$ may-contract-to $x$. In other words $A x$ may either use or discard $x$, but our analysis does not take into account that the same term cannot have two contrasting behaviors.

As we will see in the rest of this section, this is not a problem since it does not break proposition 2.2 nor proposition 2.3.

## 5.2 Compilation and decompilation

**Compilation.** The following rule is inserted just before rule (c$_{\lambda}$) from the code in section 3.3.

$$ \begin{align*} \text{comp} (\text{o-lam F}) (\text{uva A Scope}) & \quad \text{M1 M2 L1 L3 S1 S3 :-} \\ & \quad \text{maybe-eta} (\text{o-lam F}) \text{ [], !,} \\ & \quad \text{alloc S1 A S2,} \\ & \quad \text{comp-lam F F1 M1 M2 L1 L2 S2 S3,} \\ & \quad \text{get-scope (lam F1) Scope,} \\ & \quad \text{L3 = [val (link-eta (uva A Scope) (lam F1)) | L2].} \end{align*} $$
Whenever o-lam F is detected to be in ◇η it is compiled to lam F1 and replaced by the fresh variable A. This variable sees all the names free in lam F1 and is connected to lam F1 via a η-link. Invariant 2 (LINK LEFT HAND SIDE) holds for this link. Moreover:

**COROLLARY 5.6.** *The rhs of any η-link has exactly one lambda abstraction, hence the rule above respects invariant 3 (η-link RHS).*

**PROOF SKETCH.** By contradiction, suppose that the rule above is applied and that the rhs of the link is $\lambda x.\lambda y.t$, where x and y occur in t. If maybe-eta $\lambda y.t$ holds then the recursive call to comp (made by comp-lam) must have put a fresh variable in its place, so this case is impossible. Otherwise, if maybe-eta $\lambda y.t$ does not hold, then also maybe-eta $\lambda x.\lambda y.t$ does not hold either, contradicting the assumption that the rule was applied. □

**LEMMA 5.7 (W-PARTIAL-ENFORCEMENT).** $\forall s, \langle s \rangle \mapsto (t, m, l)$, if $W_{\beta\eta}(s)$ then $W(t)$.

**PROOF SKETCH.** By lemma 5.5 □

<figure><img src="image_1.png" /></figure>

*Decompilation.* The decompilation of a η-link is performed by unifying the lhs with the rhs. Note that this unification never fails, since the rhs is a flexible term not appearing in any other η-link (by definition 5.9).

## 5.3 Progress

η-links are meant to delay the unification of “problematic” terms until we know for sure if their head lambdas can be η-contracted.

**Definition 5.8 (η-progress-lhs).** A link $\Gamma \vdash X =_\eta t$ is removed from $\mathbb{L}$ when X becomes rigid. Let $y \in \Gamma$. There are two cases:

(1) if $X = a$ or $X = y$ or $X = f a_1 \dots a_n$ we unify the η-redex of X with t, that is we run $\lambda x.X x \approx_m t$

(2) if $X = \lambda x.s$ we run $X \approx_m t$.

**Definition 5.9 (η-progress-deduplicate).** A link $\Gamma \vdash X_{\bar{s}} =_\eta T$ is removed from $\mathbb{L}$ when another link $\Delta \vdash X_{\bar{r}} =_\eta T'$ is in $\mathbb{L}$. By invariant 1 the length of $\bar{s}$ and $\bar{r}$ is the same; hence we can move the term $T'$ from $\Delta$ to $\Gamma$ by renaming its bound variables, i.e. $T'' = T'[\bar{r}/\bar{s}]$. We then run $T \approx_m T''$ (under the context $\Gamma$).

**LEMMA 5.10.** Let $\lambda x.t$ be the rhs of a η-link, then $W(t)$, enforcing invariant 3.

**PROOF SKETCH.** By lemma 5.7. □

<figure><img src="image_2.png" /></figure>

**LEMMA 5.11.** Given a η-link $\Gamma \vdash X =_\eta \lambda x.t$, the unification done by η-progress-lhs is between terms in $W'$.

**PROOF SKETCH.** Let $\sigma$ be a substitution such that $W(\sigma X)$ (since $\approx_m$ preserves $W$). By invariant 3, we have $W(t)$. If $\sigma X = \lambda x.r$, then r is unified with t and both terms are in $W$. Otherwise, $\lambda x.X x$ is unified with $\lambda x.t$, and X x and t are both in $W$. □

<figure><img src="image_3.png" /></figure>

**LEMMA 5.12.** *The unification done by η-progress-deduplicate is between terms in $W$.*

**PROOF.** Given two η-links $\Gamma_1 \vdash X =_\eta \lambda x.t$ and $\Gamma_2 \vdash Y =_\eta \lambda x.t'$, the unification is performed between t and t'. By lemma 5.7 both terms are in $W$. □

<figure><img src="image_4.png" /></figure>

**LEMMA 5.13.** *The progress of η-link guarantees proposition 2.11 (W-PRESERVATION).*

**PROOF SKETCH.** By lemmas 5.11 and 5.12, every unification performed by the activation of a η-link is between terms in $W$. □

**LEMMA 5.14.** *progress terminates.*

**PROOF SKETCH.** Rules 5.8 and 5.9 remove one link from $\mathbb{L}$, hence they cannot be applied indefinitely. Moreover each rule only relies on terminating operations such as $\approx_m$, η-contraction, η-redex, relocation (a recursive copy of a finite term). □

**THEOREM 5.15 (FIDELITY IN $W_{\beta\eta}$).** Given a list of unification problems $\mathbb{P}$ such that $W_{\beta\eta}(\mathbb{P})$, if the memory map is bijective then the introduction of η-link guarantees proposition 2.3 (SIMULATION FIDELITY).

**PROOF SKETCH.** We want to prove that step$_o$ succeeds iff step$_m$ succeeds, where step$_m$ is made by a unification step u and a link progression p. Without loss of generality we consider a *O* unification problem of the form $s_1 \approx_o s_2$ where $s_1 \in \diamond\eta$ and is compiled to a variable X with the accessory link $\Gamma \vdash X =_\eta \lambda x.t_1$. The unification u always succeeds, since X is a fresh variable, we only have to consider the link progression p. Two cases should be analyzed:

* $s_2 \in \diamond\eta$, in this case, the unification problem becomes $X \approx_m Y$ with the extra link $\vdash Y =_\eta \lambda x.t_2$. After the unification of X and Y, η-progress-deduplicate is fired and, once the lambdas are crossed, $t_1$ and $t_2$ are unified. This unification succeeds iff $s_1 \approx_o s_2$ succeeds by theorem 4.3.

* $s_2 \notin \diamond\eta$, in this case $s_2$ is compiled to $t_2$ and the unification step u assigns $t_2$ to X and triggers η-progress-lhs. If $s_1$ and $s_2$ are equal thanks to $\eta_l$ then progression p unifies $\lambda x.t_1$ with the η-redex of $t_2$ namely $\lambda x.t_2 x$, otherwise they are equal thanks to rule $\lambda\lambda$ and the link progress p unifies $\lambda x.t_1$ with $t_2$. Alternatively, if $s_1$ are different $s_2$ it cannot be because of the $\lambda$ constructor in the head of $t_1$, since rule $\lambda\lambda$ or rule $\eta_l$ move under it, eventually finding two different subterms $s'_1$ and $s'_2$. By theorem 4.3, $\approx_m$ fails on terms $t'_1$ and $t'_2$ even if η-progress-lhs η-expands $t_2$. □

<figure><img src="image_5.png" /></figure>

**COROLLARY 5.16 (PROPERTIES OF $\approx_o$ IN $W_{\beta\eta}$).** Given the updated compilation scheme, procedure $\approx_o$ of section 3.6 is a good unification (as per proposition 2.1) for $=o$ in the domain $W_{\beta\eta}$.

*Example of η-progress-lhs.* The example at the beginning of section 5, once $\sigma = \{ A \mapsto f \}$, triggers η-progress-lhs since the link becomes $\vdash f =_\eta \lambda x.B_x$ and the rhs is a constant. This rule runs $\lambda x.f x \approx_m \lambda x.B_x$, resulting in $\sigma = \{ A \mapsto f ; B_x \mapsto f \}$. Since X is mapped to B and $B_x$ is decompiled into $\lambda x.f x$, by the definition of η-link decompilation $\sigma$ is decompiled to $\rho = \{ X \mapsto \lambda x.f x \}$. □

# 6 MAKING M A BIJECTION

We want to allow for partial application of functions. As a consequence the same unification variable X can be used multiple
Whenever o-lam F is detected to be in ◇η it is compiled to lam F1 and replaced by the fresh variable A. This variable sees all the names free in lam F1 and is connected to lam F1 via a η-link. Invariant 2 (LINK LEFT HAND SIDE) holds for this link. Moreover:

**COROLLARY 5.6.** The rhs of any η-link has exactly one lambda abstraction, hence the rule above respects invariant 3 (η-link RHS).

**PROOF SKETCH.** By contradiction, suppose that the rule above is applied and that the rhs of the link is λx.λy.t, where x and y occur in t. If maybe-eta λy.t holds then the recursive call to comp (made by comp-lam) must have put a fresh variable in its place, so this case is impossible. Otherwise, if maybe-eta λy.t does not hold, then also maybe-eta λx.λy.t does not hold either, contradicting the assumption that the rule was applied. □

**LEMMA 5.7 (W-PARTIAL-ENFORCEMENT).** ∀s, ⟨s⟩ ↦→ (t, m, l), if W<sub>βη</sub>(s) then W(t).

**PROOF SKETCH.** By lemma 5.5 □

**Decompilation.** The decompilation of a η-link is performed by unifying the lhs with the rhs. Note that this unification never fails, since theANTI is a flexible term not appearing in any other η-link (by definition 5.9).

## 5.3 Progress

η-links are meant to delay the unification of “problematic” terms until we know for sure if their head lambdas can be η-contracted.

**Definition 5.8 (η-progress-lhs).** A link Γ ⊢ X =η t is removed from L when X becomes rigid. Let y ∈ Γ. There are two cases:

(1) if X = a or X = y or X = f a₁...aₙ we unify the η-expansion of X with t, that is we run λx.X x ≈_m t

(2) if X = λx.s we run X ≈_m t.

**Definition 5.9 (η-progress-deduplicate).** A link Γ ⊢ X̄ =η T is removed from L when another link Δ ⊢ X̄ =η T' is in L. By invariant 1 the length of s̄ and r̄ is the same; hence we can move the term T' from Δ to Γ by renaming its bound variables, i.e. T'' = T'[r̄/s̄]. We then run T ≈_m T'' (under the context Γ).

**LEMMA 5.10.** Let λx.t be the rhs of a η-link, then W(t), enforcing invariant 3.

**PROOF SKETCH.** By lemma 5.7. □

**LEMMA 5.11.** Given a η-link Γ ⊢ X =η λx.t, the unification done by η-progress-lhs is between terms in W.

**PROOF SKETCH.** Let σ be a substitution such that W(σX) (since ≈_m preserves W). By invariant 3, we have W(t). If σX = λx.r, then r is unified with t and both terms are in W. Otherwise, λx.X x is unified with λx.t, and X x and t are both in W. □

**LEMMA 5.12.** The unification done by η-progress-deduplicate is between terms in W.

**PROOF.** Given two η-links Γ₁ ⊢ X =η λx.t and Γ₂ ⊢ Y =η λx.t' . By lemma 5.7 both terms are in W. □

**LEMMA 5.13.** The progress of η-link guarantees proposition 2.11 (W-PRESERVATION).

**PROOF SKETCH.** By lemmas 5.11 and 5.12, every unification performed by the activation of a η-link is between terms in W. □

**LEMMA 5.14.** progress terminates.

**PROOF SKETCH.** Rules 5.8 and 5.9 remove one link from L, hence they cannot be applied indefinitely. Moreover each rule only relies on terminating operations such as ≈_m, η-contraction, η-expansion, relocation (a recursive copy of a finite term). □

**THEOREM 5.15 (FIDELITY IN W<sub>βη</sub>).*** Given a list of unification problems P such that W<sub>βη</sub>(P), if the memory map is bijective then the introduction of η-link guarantees proposition 2.3 (SIMULATION FIDELITY).

**PROOF SKETCH.** We want to prove that step<sub>o</sub> succeeds iff step<sub>m</sub> succeeds, where step<sub>m</sub> is made by a unification step u and a link progression p. Without loss of generality we consider a O unification problem of the form s₁ ≈<sub>o</sub> s₂ where s₁ ∈ ◇η and is compiled to a variable X with the accessory link Γ ⊢ X =η λx.t₁. The unification u always succeeds, since X is a fresh variable, we only have to consider the link progression p. Two cases should be analyzed:

* s₂ ∈ ◇η, in this case, the unification problem becomes X ≈_m Y with the extra link ⊢ Y =η λx.t₂. After the unification of X and Y, η-progress-deduplicate is fired and, once the lambdas are crossed, t₁ and t₂ are unified. This unification succeeds iff s₁ ≈<sub>o</sub> s₂ succeeds by theorem 4.3.

* s₂ ∉ ◇η, in this case s₂ is compiled to t₂ and the unification step u assigns t₂ to X and triggers η-progress-lhs. If s₁ and s₂ are equal thanks to η<sub>l</sub> then progression p unifies λx.t₁ with the η-expansion of t₂ namely λx.t₂ x, otherwise they are equal thanks to rule λλ and the link progress p unifies λx.t₁ with t₂. Alternatively, if s₁ are different s₂ it cannot be because of the λ constructor in the head of t₁, since rule λλ or rule η<sub>l</sub> move under it, eventually finding two different subterms s'<sub>1</sub> and s'<sub>2</sub>. By theorem 4.3, ≈_m fails on terms t'<sub>1</sub> and t'<sub>2</sub> even if η-progress-lhs η-expands t₂. □

**COROLLARY 5.16 (PROPERTIES OF ≈<sub>o</sub> IN W<sub>βη</sub>).*** Given the updated compilation scheme, procedure ≈<sub>o</sub> of section 3.6 is a good unification (as per proposition 2.1) for =<sub>o</sub> in the domain W<sub>βη</sub>.

**Example of η-progress-lhs.** The example at the beginning of section 5, once σ = { A ↦→ f }, triggers η-progress-lhs since the link becomes ⊢ f =η λx.Bx and theANTI is a constant. This rule runs λx.f x ≈_m λx.Bx, resulting in σ = { A ↦→ f ; Bx ↦→ f }. Since X is mapped to B and Bx is decompiled into λx.f x, by the definition of η-link decompilation σ is decompiled to ρ = { X ↦→ λx.f x }.

## 6 MAKING M A BIJECTION

We want to allow for partial application of functions. As a consequence the same unification variable X can be used multiple
times with different arities. When it is the case the memory map $M$ generated by the compiler is not a bijection. For example:

$$ 
\begin{align*}
\mathbb{P} &= \{ \lambda x.(X \ \dot{x}) \approx_o f \quad X \approx_o \lambda x.a \} \\
\mathbb{Q} &= \{ \quad A \approx_m f \quad C \approx_m \lambda x.a \} \\
\mathbb{M} &= \{ X \mapsto C^0 \quad X \mapsto B^1 \} \\
\mathbb{L} &= \{ \vdash A =_\eta \lambda x.B_x \}
\end{align*}
$$

in the unification problems $\mathbb{P}$ above, $X$ is used with arity 1 in $\mathbb{P}_1$ and with arity 0 in $\mathbb{P}_2$. In order to preserve invariant 1 (UNIFICATION-VARIABLE ARITY) the compiler did generate two entries in $M$ for $X$, namely $B$ and $C$. However, there is no connection between these two variables and any incompatible assignments to them would not be detected, in turn breaking proposition 2.3. To address this issue, we post-process $M$ to ensure the following property:

**PROPOSITION 6.1 (M IS A BIJECTION).** *After compilation, for each O-variable X in $\mathbb{P}$ and for each M-variable A in $\mathbb{Q}$ there is exactly one entry $X \mapsto A^n$ in $M$.*

Note that running $\approx_m$ may require allocating new variables in $M$ as explained in section 3.5. The property above ignores these variables since they are fresh and have no corresponding variable in $O$.

The core procedure of this post-processing step is *align-arity* that is iterated by *map-deduplication*:

**Definition 6.2 (align-arity).** Given two mappings $m_1: X \mapsto A^m$ and $m_2: X \mapsto C^n$ where $m < n$ and $d = n - m$, *align-arity* $m_1 m_2$ generates the following $d$ links, one for each $i$ such that $0 \le i < d$,

$$ x_0 \dots x_{m+i} \vdash B_{x_0 \dots x_{m+i}}^i =_\eta \lambda x_{m+i+1} B_{x_0 \dots x_{m+i+1}}^{i+1} $$

where $B^i$ is a fresh variable of *arity* $m+i$, and $B^0 = A$ as well as $B^d = C$.

The intuition is that we $\eta$-expand the occurrence of the variable with lower *arity* to match the higher *arity*. Since each $\eta$-link can add exactly one lambda, we need as many links as the difference between the two *arities*.

**Definition 6.3 (map-deduplication).** For all mappings $m_1, m_2 \in M$ such that $m_1: X \mapsto A^m$ and $m_2: X \mapsto C^n$ and $m < n$ we remove $m_1$ from $M$ and add to $\mathbb{L}$ the result of *align-arity* $m_1 m_2$.

**THEOREM 6.4 (FIDELITY WITH MAP-DEDUPLICATION).** *Given a list of unification problems $\mathbb{P}$, such that $W_{\beta\eta}(\mathbb{P})$, if $\mathbb{P}$ contains the same O-variable used at different *arities*, then map-deduplication guarantees proposition 2.3 (SIMULATION FIDELITY)*

**PROOF SKETCH.** Let $X$ be a *O*-variable appearing in two different subterms $s_1$ and $s_2$. In $s_1$ variable $X$ is applied to the list of terms $x_1 \dots x_m$ while, in $s_2$, it is applied to $y_1 \dots y_n$. Without loss of generality we take $m < n$. After *map-deduplication* we have two distinct *M*-variables for $X$, say $A$ and $C$, related by a chain $\bar{c}$ of $\eta$-links of length $n - m$. We prove that if $A$ and $C$ are assigned respectively to the *W* terms $\lambda x_1 \dots x_p.t_1$ and $\lambda x_1 \dots x_q.t_2$, then a failure occurs iff these terms do not unify. By $\eta$-progress-lhs, the assignment of $A$ activates *p* links of $\bar{c}$. In particular, when $p \ge n$, then the entire chain collapses and unification is performed between $\lambda x_n \dots x_p.t_1$ and $\lambda x_1 \dots x_q.t_2$. By theorem 4.3 and since we work with *W* terms, this unification succeeds iff it does in *O*. Otherwise if $p < n$ then we have to consider two cases. 1) If $t_1$ is a rigid term then $t_2$ must be the $\eta$-redex of $t_1$, implying $q = 0$. If it is not the case, then $\eta$-progress-lhs

would eventually cause a failure. 2) If $t_1$ is a unification variable then scope-check guarantees that $t_2$ does not use $x_1 \dots x_p$ as free variables, causing otherwise a unification failure. After this check, $m - n - p$ links of $\bar{c}$ remain suspended, as we expect: decompilation is charged to wake all links in $\mathbb{L}$ and eventually relate $t_1$ with $t_2$. □

*Example of map-deduplication.* If we take back the example given at the beginning of this section, *map-deduplication* produces the following result:

$$ 
\begin{align*}
\mathbb{P} &= \{ \lambda x.(X \ \dot{x}) \approx_o f \quad X \approx_o \lambda x.a \} \\
\mathbb{Q} &= \{ \quad A \approx_m f \quad C \approx_m \lambda x.a \} \\
\mathbb{M} &= \{ X \mapsto B^1 \} \\
\mathbb{L} &= \{ \vdash C =_\eta \lambda x.B_x \quad \vdash A =_\eta \lambda x.B_x \}
\end{align*}
$$

Note that $X \mapsto C^0$ disappears from $M$ in favour of the auxiliary $\eta$-link $\vdash C =_\eta \lambda x.B_x$. The resolution of $Q_1$ assigns $a$ to $A$. This wakes up $L_2$ by $\eta$-progress-lhs, assigning «$f \ \dot{x}$» to $B_x$. The resolution of $Q_2$ instantiates $C$ to $\lambda x.a$, which, in turn triggers $L_1$ by $\eta$-progress-lhs. In turn, this performs $\lambda x.a \approx_m \lambda x.(f \ \dot{x})$ that fails as expected.

# 7 HANDLING OF ♦L

As observed in [17] it is worth handling terms in $\diamond L$ since, in practice, these terms often re-enter $L$ at runtime.

In the following example problem $\mathbb{P}_2$, namely $X a \approx_o a$, admits two different solutions: $\rho_1 = \{ X \mapsto \lambda x.x \}$ and $\rho_2 = \{ X \mapsto \lambda x.a \}$. The unification algorithm alone cannot chose the right one, since no solution is more general than the other, but for the first problem the choice is obvious, and in turn this choice makes $\mathbb{P}_2 \subseteq L$:

$$ 
\begin{align*}
\mathbb{P} &= \{ X \approx_o \lambda x.a \quad (X a) \approx_o a \} \\
\mathbb{Q} &= \{ A \approx_m \lambda x.a \quad (A a) \approx_m a \} \\
\mathbb{M} &= \{ X \mapsto A^0 \}
\end{align*}
$$

In order to support this scenario we have to improve a little our compiler and progress routines. In particular $Q_1$ generates $\sigma = \{ A \mapsto \lambda x.a \}$ making $\sigma Q_2$ equal to $(\lambda x.a) a \approx_m a$ that $\approx_m$ cannot solve since it lacks rules $\beta_l$ and $\beta_r$.

To address this problem the compiler must recognize $\diamond L$ terms and replace them with fresh variables and generate a new kind of links that we call $L$-link.

In addition to invariant 2 (LINK LEFT HAND SIDE), the term on the rhs of a $L$-link has the following property:

**INvariant 4 (L-link RHS).** *The rhs of any L-link has the shape $X_{s_1 \dots s_n} t_1 \dots t_m$ where $X$ is a unification variable in $L$ (with scope $s_1 \dots s_n$) and $t_1 \dots t_m$ is a list of terms such that $m > 0$ and $t_1$ is either a variable occurring in $s_1 \dots s_n$ or a term other than a variable.*

Note that the shape of such as rhs is «app [uva X S | L]», where S is $[s_1, \dots, s_n]$ and L is $[t_1, \dots, t_m]$.

## 7.1 Compilation and decompilation

We insert this rule just before rule (c@):

comp (o-app [o-uva A|Ag]) (uva B Sc) M1 M3 L1 L3 S1 S4 :- 1,
pattern-fragment-prefix Ag Pf Extra, alloc S1 B S2,
len Pf Ar, m-alloc (ov A) (mv C (arity Ar)) M1 M2 S2 S3,
fold6 comp Pf Pf1 M2 M2 L1 L1 S3 S3,
times with different arities. When it is the case the memory map $M$ generated by the compiler is not a bijection. For example:

$$ 
\begin{align*}
\mathbb{P} &= \{ \lambda x.(X \ x) \approx_o f \quad X \approx_o \lambda x.a \} \\
\mathbb{Q} &= \{ \quad A \approx_m f \quad C \approx_m \lambda x.a \} \\
\mathbb{M} &= \{ X \mapsto C^0 \quad X \mapsto B^1 \} \\
\mathbb{L} &= \{ \vdash A =_\eta \lambda x.B_x \}
\end{align*}
$$

in the unification problems $\mathbb{P}$ above, $X$ is used with arity 1 in $\mathbb{P}_1$ and with arity 0 in $\mathbb{P}_2$. In order to preserve invariant 1 (UNIFICATION-VARIABLE ARITY) the compiler did generate two entries in $M$ for $X$, namely $B$ and $C$. However, there is no connection between these two variables and any incompatible assignments to them would not be detected, in turn breaking proposition 2.3. To address this issue, we post-process $M$ to ensure the following property:

**PROPOSITION 6.1 (M IS A BIJECTION).** After compilation, for each $O$-variable $X$ in $\mathbb{P}$ and for each $M$-variable $A$ in $\mathbb{Q}$ there is exactly one entry $X \mapsto A^n$ in $M$.

Note that running $\approx_m$ may require allocating new variables in $M$ as explained in section 3.5. The property above ignores these variables since they are fresh and have no corresponding variable in $O$.

The core procedure of this post-processing step is *align-arity* that is iterated by *map-deduplication*:

**Definition 6.2 (align-arity).** Given two mappings $m_1: X \mapsto A^m$ and $m_2: X \mapsto C^n$ where $m < n$ and $d = n - m$, align-arity $m_1, m_2$ generates the following $d$ links, one for each $i$ such that $0 \le i < d$,

$$ x_0 \dots x_{m+i} \vdash B_{x_0 \dots x_{m+i}}^i =_\eta \lambda x_{m+i+1} B_{x_0 \dots x_{m+i+1}}^{i+1} $$

where $B^i$ is a fresh variable of arity $m+i$, and $B^0 = A$ as well as $B^d = C$.

The intuition is that we $\eta$-expand the occurrence of the variable with lower arity to match the higher arity. Since each $\eta$-link can add exactly one lambda, we need as many links as the difference between the two arities.

**Definition 6.3 (map-deduplication).** For all mappings $m_1, m_2 \in M$ such that $m_1: X \mapsto A^m$ and $m_2: X \mapsto C^n$ and $m < n$ we remove $m_1$ from $M$ and add to $\mathbb{L}$ the result of *align-arity* $m_1, m_2$.

**THEOREM 6.4 (FIDELITY WITH MAP-DEDUPLICATION).** Given a list of unification problems $\mathbb{P}$, such that $W_{\beta\eta}(\mathbb{P})$, if $\mathbb{P}$ contains the same $O$-variable used at different arities, then map-deduplication guarantees proposition 2.3 (SIMULATION FIDELITY)

**PROOF SKETCH.** Let $X$ be a $O$-variable appearing in two different subterms $s_1$ and $s_2$. In $s_1$ variable $X$ is applied to the list of terms $x_1 \dots x_m$ while, in $s_2$, it is applied to $y_1 \dots y_n$. Without loss of generality we take $m < n$. After map-deduplication we have two distinct $M$-variables for $X$, say $A$ and $C$, related by a chain $\bar{c}$ of $\eta$-links of length $n - m$. We prove that if $A$ and $C$ are assigned respectively to the $W$ terms $\lambda x_1 \dots x_p.t_1$ and $\lambda x_1 \dots x_q.t_2$, then a failure occurs iff these terms do not unify. By $\eta$-progress-lhs, the assignment of $A$ activates $p$ links of $\bar{c}$. In particular, when $p \ge n$, then the entire chain collapses and unification is performed between $\lambda x_n \dots x_p.t_1$ and $\lambda x_1 \dots x_q.t_2$. By theorem 4.3 and since we work with $W$ terms, this unification succeeds iff it does in $O$. Otherwise if $p < n$ then we have to consider two cases. 1) If $t_1$ is a rigid term then $t_2$ must be the $\eta$-expansion of $t_1$, implying $q = 0$. If it is not

the case, then $\eta$-progress-lhs would eventually cause a failure. 2) If $t_1$ is a unification variable then scope-check guarantees that $t_2$ does not use $x_1 \dots x_p$ as free variables, causing otherwise a unification failure. After this check, $m - n - p$ links of $\bar{c}$ remain suspended, as we expect: decompilation is charged to wake all links in $\mathbb{L}$ and eventually relate $t_1$ with $t_2$. $\square$

*Example of map-deduplication.* If we take back the example given at the beginning of this section, *map-deduplication* produces the following result:

$$ 
\begin{align*}
\mathbb{P} &= \{ \lambda x.(X \ x) \approx_o f \quad X \approx_o \lambda x.a \} \\
\mathbb{Q} &= \{ \quad A \approx_m f \quad C \approx_m \lambda x.a \} \\
\mathbb{M} &= \{ X \mapsto B^1 \} \\
\mathbb{L} &= \{ \vdash C =_\eta \lambda x.B_x \quad \vdash A =_\eta \lambda x.B_x \}
\end{align*}
$$

Note that $X \mapsto C^0$ disappears from $M$ in favour of the auxiliary $\eta$-link $\vdash C =_\eta \lambda x.B_x$. The resolution of $\mathbb{Q}_1$ assigns $a$ to $A$. This wakes up $\mathbb{L}_2$ by $\eta$-progress-lhs, assigning «$f x$» to $B_x$. The resolution of $\mathbb{Q}_2$ instantiates $C$ to $\lambda x.a$, which, in turn triggers $\mathbb{L}_1$ by $\eta$-progress-lhs. In turn, this performs $\lambda x.a \approx_m \lambda x.(f x)$ that fails as expected.

# 7 HANDLING OF ♦L

As observed in [15] it is worth handling terms in $\diamond L$ since, in practice, these terms often re-enter $L$ at runtime.

In the following example problem $\mathbb{P}_2$, namely $X a \approx_o a$, admits two different solutions: $\rho_1 = \{ X \mapsto \lambda x.x \}$ and $\rho_2 = \{ X \mapsto \lambda x.a \}$. The unification algorithm alone cannot chose the right one, since no solution is more general than the other, but for the first problem the choice is obvious, and in turn this choice makes $\mathbb{P}_2 \subseteq L$:

$$ 
\begin{align*}
\mathbb{P} &= \{ X \approx_o \lambda x.a \quad (X a) \approx_o a \} \\
\mathbb{Q} &= \{ A \approx_m \lambda x.a \quad (A a) \approx_m a \} \\
\mathbb{M} &= \{ X \mapsto A^0 \}
\end{align*}
$$

In order to support this scenario we have to improve a little our compiler and progress routines. In particular $\mathbb{Q}_1$ generates $\sigma = \{ A \mapsto \lambda x.a \}$ making $\sigma \mathbb{Q}_2$ equal to $(\lambda x.a) a \approx_m a$ that $\approx_m$ cannot solve since it lacks rules $\beta_l$ and $\beta_r$.

To address this problem the compiler must recognize $\diamond L$ terms and replace them with fresh variables and generate a new kind of links that we call $L$-link.

In addition to invariant 2 (LINK LEFT HAND SIDE), the term on the rhs of a $L$-link has the following property:

**INVARIANT 4 (L-link RHS).** The rhs of any $L$-link has the shape $X_{s_1 \dots s_n} t_1 \dots t_m$ where $X$ is a unification variable in $L$ (with scope $s_1 \dots s_n$) and $t_1 \dots t_m$ is a list of terms such that $m > 0$ and $t_1$ is either a variable occurring in $s_1 \dots s_n$ or a term other than a variable.

Note that the shape of such as rhs is «app [uva X S | L]», where S is $[s_1, \dots, s_n]$ and L is $[t_1, \dots, t_m]$.

## 7.1 Compilation and decompilation

We insert this rule just before rule (c@):

comp (o-app [o-uva A|Ag]) (uva B Sc) M1 M3 L1 L3 S1 S4 :- !, pattern-fragment-prefix Ag Pf Extra, alloc S1 B S2, len Pf Ar, m-alloc (ov A) (mv C (arity Ar)) M1 M2 S2 S3,

1103

1104

1105

1106

1107

1108

1109

1110

1111

1112

1113

1114

1115

1116

1117

1118

1119

1120

1121

1122

1123

1124

1125

1126

1127

1128

1129

1130

1131

1132

1133

1134

1135

1136

1137

1138

1139

1140

1141

1142

1143

1144

1145

1146

1147

1148

1149

1150

1151

1152

1153

1154

1155

1156

1157

1158

1159

1160
fold6 comp Extra Extra1 M2 M3 L1 L2 S3 S4,
Beta = app [uva C Pf1 | Extra1],
get-scope Beta Sc,
L3 = [val (link-llam (uva B Sc) Beta) | L2].

The list Ag is split into two parts: Pf is in $\mathcal{L}$, and can be empty; Extra cannot be empty and is such that «append Pf Extra Ag». The rhs of the $\mathcal{L}$-link is the application of a fresh variable C having in scope all names in Pf1 (the compilation of Pf). The variable B, returned as the compiled term, is a fresh variable having in scope all the free variables occurring in Pf1 and Extra1 (the compilation of Extra). This construction enforces invariant 4 ($\mathcal{L}$-link RHS).

**LEMMA 7.1 (W-ENFORCEMENT).** $\forall s, \langle s \rangle \mapsto (t, m, l)$, then $W(t)$.

**PROOF SKETCH.** By lemmas 4.2 and 5.7 and the rule above. $\square$

<figure><img src="image_6.png" /></figure>

**Decompilation.** All $\mathcal{L}$-link should be solved before decompilation. If any $\mathcal{L}$-link remains in $\mathcal{L}$, decompilation fails.

## 7.2 Progress

Let $l$ be a $\mathcal{L}$-link of the form $\Gamma \vdash T =_L X_{s_1 \dots s_n} t_1 \dots t_m$

**Definition 7.2 ($\mathcal{L}$-progress-refine).** Let $\sigma$ be a substitution such that $\sigma t_1$ is a name s not occurring in $s_1 \dots s_n$. If $m = 1$, then $l$ is removed and the rhs is unified with $X_{s_1 \dots s_n} s$. If $m > 1$, then $l$ is replaced by the link $\Gamma \vdash T =_L Y_{s_1 \dots s_n} s t_2 \dots t_m$ (where Y is a fresh variable of arity $n+1$) and link $\Gamma \vdash X_{s_1 \dots s_n} =_\eta \lambda x. Y_{s_1 \dots s_n} x$ is added to $\mathcal{L}$.

**Definition 7.3 ($\mathcal{L}$-progress-rhs).** Link $l$ is removed from $\mathcal{L}$ if $X_{s_1 \dots s_n}$ is instantiated to a term $t$ and $t_1 \dots t_m$ $\beta$-reduces to a $t' \in \mathcal{L}$.

**Definition 7.4 ($\mathcal{L}$-progress-fail).** progress fails when either

* there exists another link $l' \in \mathcal{L}$ with the same rhs as $l$; or

* the rhs of $l$ become rigid.

We relax this condition and accommodate for heuristics in 7.3.

Finally we introduce the following $\eta$-link progress rule.

**Definition 7.5 ($\eta$-progress-rhs).** A link $\Gamma \vdash X =_\eta T$ is removed from $\mathcal{L}$ when either

* maybe-eta T does not hold (anymore), in this case X is unified with T; or

* T $\eta$-contracts to a term $T'$ not starting with the 1am constructor. In this case X is unified with $T'$

The idea behind this rule is to instantiate the rhs variable of a $\eta$-link whenever its rhs is for sure a W term.

**LEMMA 7.6.** *progress terminates*

**PROOF SKETCH.** Let $l = \Gamma \vdash T =_L X_{s_1 \dots s_n} t_1 \dots t_m$ a $\mathcal{L}$-link in the store $\mathcal{L}$. The progression made by $\mathcal{L}$-progress-rhs terminates: $l$ is removed from $\mathcal{L}$ after having performed terminating instructions. If $l$ is not activated by $\mathcal{L}$-progress-rhs, then X is a variable. The activation of $\mathcal{L}$-progress-refine replaces $l$ with the new $\mathcal{L}$-link $\Gamma \vdash T =_L Y_{s_1 \dots s_n} s t_2 \dots t_m$. This progression can be triggered at most m times, since at each time the number of terms applied to X decreases. In the end $l_m$ will be removed from $\mathcal{L}$ after the unification

between rhs with rhs. We also note that each $\mathcal{L}$-progress-refine generates a $\eta$-link, yet, according to lemma 5.14, this does not affect termination. $\mathcal{L}$-progress-fail terminates since it stop progression with failure. Finally, $\eta$-progress-rhs performs terminating operations and, if its permises succeed, the considered $\eta$-link is removed from $\mathcal{L}$, ensuring termination. $\square$

<figure><img src="image_7.png" /></figure>

**THEOREM 7.7 (FIDELITY IN O).** *The introduction of $\mathcal{L}$-link guarantees proposition 2.4 (FIDELITY RECOVERY) if $P \not\subseteq \mathcal{L}$.*

**PROOF SKETCH.** Let $P_i$ be the first problem in $P$ such that it is not in $\mathcal{L}$ and let $\sigma$ be the substitution obtained solving $Q_1 \dots Q_{i-1}$. After the execution of step$_m$ for the $i-1$ time, each variable X corresponding to a $\diamond\eta$ subterm in the original O unification problem, is instantiated iff it is known for sure that X is no more in $\diamond\eta$. If $\sigma_{Q_i}$ is in $\mathcal{L}$, then by definitions 7.2 and 7.3 the associated $\mathcal{L}$-link is solved and removed. In this case, all calls to $\approx_m$ are between terms in $\mathcal{L}$ and by theorem 4.3 fidelity is guaranteed. If $\sigma_Q$ is still in $\diamond\mathcal{L}$, then by definition 7.4 unification fails as the corresponding unification in O would (it is called outside its domain). $\square$

<figure><img src="image_8.png" /></figure>

## 7.3 Relaxing definition 7.4 ($\mathcal{L}$-PROGRESS-FAIL)

Working with terms in $\mathcal{L}$ is sometime too restrictive [1] and we could find in literature a few strategies to go beyond $\mathcal{L}$ without implementing Huet's algorithm [11]. Some implementations of $\lambda$Prolog [18] such as Teyjus [17] delay the resolution of $\diamond\mathcal{L}$ unification problems until the substitution makes them reenter $\mathcal{L}$. Other systems apply heuristics like preferring projection over mimic, and commit to that solution. This is the case for the unification algorithm Coq uses in its type-class solver [25],

In this section we show how we can implement these strategies by simply adding (or removing) rules to the progress predicate. In the example below $P_1$ is in $\diamond\mathcal{L}$.

$$ \mathcal{P} = \{ (X a) \approx_o a \quad X \approx_o \lambda x. Y \} \\ \mathcal{Q} = \{ A \approx_m a \quad B \approx_m \lambda x. C \} \\ \mathcal{M} = \{ Y \mapsto C^0 \quad X \mapsto B^0 \} \\ \mathcal{L} = \{ \vdash A =_L (B a) \} $$

If we want the object-language unification to delay the first unification problem (waiting for X to be instantiated), we can relax definition 7.4. Instead of failing when the rhs of $L_1$ becomes rigid (equal to a), we keep it in $\mathcal{L}$ until the head of its rhs also become rigid. In this case, since both the rhs and rhs have rigid heads, they can be unified. While this relaxed rule does not break proposition 2.3 (SIMULATION FIDELITY) per se, the occur-check-links procedure becomes incomplete since invariant 2 (LINK LEFT HAND SIDE) is broken. Also note that delaying unification outside $\mathcal{L}$ can leave $\mathcal{L}$-link for the decompilation phase. Therefore commit-links should be modified accordingly.

If instead we want $\approx_o$ to follow the second strategy and pick an arbitrary solution we can modify progress by applying the desired heuristic instead of failing. For instance, in $X a b = Y b$, the last argument of the two terms is the same and unification can succeed by assigning $Xa$ to Y. This heuristic is used by [25].
# 8 ACTUAL IMPLEMENTATION IN ELPI

In this paper we did study a compiler and a simulation loop on a minimal language. The actual implementation uses the Coq-Elpi meta language to both compile the sequence of problems (the rules) and execute them, that is Elpi plays the role of *M* as well.

The main difference is that we cannot implement run<sub>m</sub> since it is the runtime of the programming language. In particular the runtime iterates ≈<sub>m</sub>, but step<sub>m</sub> also needs to check links for progress. Luckily Elpi extends λProlog with constraints (suspended goals) and Constraint Handling Rules (CHR) to operate on them [10, 7]. Similarly to [13] a constraint is a goal suspended on a list of variables that is resumed as soon as one of these variable is assigned, before any other existing goal is considered. In turn link activation grants proposition 2.3 (SIMULATION FIDELITY). We point out that [13] delays ♦L unification problems while we also delay problems that are in ♦η. For brevity we only provide two pseudo-code snippets. The first one depicts how η-link are suspended or make progress.

link-eta L R :- not (var L), !, eta-progress-lhs L R.
link-eta L R :- not (maybe-eta R), !, eta-progress-rhs L R.
link-eta L R :- declare_constraint (link-eta L R) [L,R].

The second snippet illustrates the deduplication of η-link. The syntax «N ▷ G ?- P» denotes a λProlog sequent, that is a goal P under a set G of hypothetical rules (introduced by =>) and where the program context binds (via the pi operator) eigenvariables in N. Sequents are presented to CHR with their higher order unification variables replaced by “frozen constants”, that is A<sub>xyz</sub> becomes «uvar f<sub>A</sub> [x,y,z]» for a fresh constant f<sub>A</sub>. Frozen constants are “defrost” when they are part of a new goal (see [10, section 4.3]).

rule (N1 ▷ G1 ?- link-eta (uvar X LX1) T1) % match
/ (N2 ▷ G2 ?- link-eta (uvar X LX2) T2) % remove
| (relocate LX1 LX2 T2 T2') % condition
 <=> (N1 ▷ G1 ?- T1 = T2') % new goal

The first directive matches a constraint whose rhs is a variable X; the second matches and removes a constraint on the same variable; the third relocates T2 and the latter crafts the new goal that unifies T1 with T2' under G1 and the set of heigenvariables N1.

# 9 RELATED WORK AND CONCLUSION

Object-language terms can be unified using different strategies.

The first approach that comes to mind consist in implementing ≈<sub>o</sub> as a regular routine, i.e. write rules as follows

decision X :- unify X (all A x\ app [P, x]), finite A,
pi x\ decision (app [P, x]).

where unify is a regular predicate. This method fails to take advantage of the logic programming engine provided by the meta language since it removes all the data from the rule's heads and makes indexing degrade. Additionally, implementing a unification procedure in the meta language is likely to be significantly slower compared to the built-in one on the common domain of first order terms.

Another possibility is to avoid having application and abstraction nodes in the syntax tree, and use the meta language ones, as in:

decision (all A x\ P x) :- finite A, pi x\ decision (P x).

However, this encoding has two big limitations. First it is not always feasible to adopt it for Coq due to the fact that the type system of the meta language is too limited to accommodate the one of the object language, e.g. Coq can typecheck variadic functions [2]. Second, the encoding of Coq terms provided by Elpi is primarily used for meta programming, i.e. to extend the Coq system. Consequently, it must be able to manipulate terms that are not known in advance without relying on introspection primitives such as Prolog's functor/3 and arg/3. To avoid that constants cannot be symbols of the meta language, but must rather live in an open world, akin to the string data type used in the con constructor.

In the literature we could find a related encoding of the Calculus of Constructions (CC) [4]. The goal of that work is to exhibit a logic program performing proof checking for CC and hence relate the proof system of intuitionistic higher-order logic (that animates λProlog programs) with the one of CC. The encoding is hence tailored toward a different goal, for example it utilizes three relations to represent the equational theory of CC, and that choice alone makes things harder for us. Section 6 contains a discussion about the use of the unification procedure of the meta language in presence of non ground goals, but the authors are not interested in exploiting a decidable fragment of higher-order unification but are rather leaning towards an interactive system where the user is given control over the search procedure.

Another work that is, somewhat surprisingly, only superficially related to ours is the type-class engine built in Isabelle's meta language. In [31] classes identify (simple) types, they are not higher order predicates as in Coq, hence the solver does not require a higher-order unification procedure.

The approach presented in this paper addresses all the concerns mentioned earlier. It takes advantage of the unification capabilities of the meta language at the price of handling problematic sub terms on the side. As a result our encoding takes advantage of indexing data structures and mode analysis for clause filtering. It is worth mentioning that we replace terms with variables only when it is strictly needed, leaving the rest of the term structure intact and hence indexable. Some preliminary benchmarks on the Stdpp library [12] show encouraging results: our type-class solver has some overhead on small goals but is consistently faster than the Coq one starting from goals made of 32 nodes. Moreover our approach is flexible enough to accommodate different strategies and heuristics to handle terms outside the pattern fragment. Finally, our encoding is sufficiently shallow to: 1) allow to lift forms of static analysis for the meta language, such as determinacy, also to the object language; 2) take advantage of future improvements to the logic-programming engine of Elpi, such as tabled search.

We considered mechanizing our results with Abella [8], especially in the early phase of this work, but unfortunately we could not. The main reason is that the logic of Abella does not let one quantify over predicates nor use the cut operator. Eliminating cut or higher order combinators like map orforall2 is surely possible, but has a high cost in verbosity given how pervasively they are used. Moreover, and more importantly, it creates a distance between the verified and the actual code, which we found to hinder our exploration. However, we did establish a test suite with about a hundred cases. It is available at https://github.com/FissoreD/ho-unif-for-free.
# 8 ACTUAL IMPLEMENTATION IN ELPI

In this paper we did study a compiler and a simulation loop on a minimal language. The actual implementation uses the Coq-Elpi meta language to both compile the sequence of problems (the rules) and execute them, that is Elpi plays the role of *M* as well.

The main difference is that we cannot implement $run_m$ since it is the runtime of the programming language. In particular the runtime iterates $\approx_m$, but $step_m$ also needs to check links for progress. Luckily Elpi extends $\lambda$Prolog with constraints (suspended goals) and Constraint Handling Rules (CHR) to operate on them [10, 7]. An important design choice is that constraints are suspended on a user computed list of unification variables, and are resumed as soon as one of them is assigned, before any other existing goal is considered. In turn this property allows for a timely activation of links that grants proposition 2.3 (SIMULATION FIDELITY). For brevity we only provide two pseudo-code snippets. The first one depicts how $\eta$-link are suspended or make progress.

link-eta L R :- not (var L), !, eta-progress-lhs L R.

link-eta L R :- not (maybe-eta R), !, eta-progress-rhs L R.

link-eta L R :- declare_constraint (link-eta L R) [L,R].

The second snippet illustrates the deduplication of $\eta$-link. The syntax «N $\rightarrow$ G ?- P» denotes a $\lambda$Prolog sequent, that is a goal P under a set G of hypothetical rules (introduced by $\Rightarrow$) and where the program context binds (via the pi operator) heigenvariables in N. Sequents are presented to CHR with their higher order unification variables replaced by “frozen constants”, that is $A_{xyz}$ becomes «uvar f_A [x,y,z]» for a fresh constant $f_A$. Frozen constants are “defrost” when they are part of a new goal (see [10, section 4.3]).

rule (N1 $\rightarrow$ G1 ?- link-eta (uvar X LX1) T1) % match
/ (N2 $\rightarrow$ G2 ?- link-eta (uvar X LX2) T2) % remove
| (relocate LX1 LX2 T2 T2') % condition
$\Rightarrow$ (N1 $\rightarrow$ G1 ?- T1 = T2'). % new goal

The first directive matches a constraint whose lhs is a variable X; the second mathes and removes a constraint on the same variable; the third relocates T2 and the latter crafts the new goal that unifies T1 with T2' under G1 and the set of heigenvariables N1.

# 9 RELATED WORK AND CONCLUSION

Object-language terms can be unified using different strategies.

The first approach that comes to mind consist in implementing $\approx_o$ as a regular routine, i.e. write rules as follows

decision X :- unify X (all A x\ app [P, x]), finite A,
pi x\ decision (app [P, x]).

where unify is a regular predicate. This method fails to take advantage of the logic programming engine provided by the meta language since it removes all data from rule's heads and makes indexing degrade. Additionally, implementing a unification procedure in the meta language is likely to be significantly slower compared to the built-in one on the common domain of first order terms.

Another possibility is to avoid having application and abstraction nodes in the syntax tree, and use the meta language ones, as in:

decision (all A x\ P x) :- finite A, pi x\ decision (P x).

However, this encoding has two big limitations. First it is not always feasible to adopt it for Coq due to the fact that the type system of

the meta language is too limited to accommodate for the one of the object language, e.g. Coq can typecheck variadic functions [2]. Second, the encoding of Coq terms provided by Elpi is primarily used for meta programming, i.e. to extend the Coq system. Consequently, it must be able to manipulate terms that are not known in advance without relying on introspection primitives such as Prolog's functor/3 and arg/3. To avoid that constants cannot be symbols of the meta language, but must rather live in an open world, akin to the string data type used in the con constructor.

In the literature we could find a related encoding of the Calculus of Constructions (CC) [4]. The goal of that work is to exhibit a logic program performing proof checking for CC and hence relate the proof system of intuitionistic higher-order logic (that animates $\lambda$Prolog programs) with the one of CC. The encoding is hence tailored toward a different goal, for example it utilizes three relations to represent the equational theory of CC, and that choice alone makes things harder for us. Section 6 contains a discussion about the use of the unification procedure of the meta language in presence of non ground goals, but the authors are not interested in exploiting a decidable fragment of higher-order unification but are rather leaning towards an interactive system where the user is given control over the search procedure.

Another work that is, somewhat surprisingly, only superficially related to ours is the type-class engine built in Isabelle's meta language. In [29] classes identify (simple) types, they are not higher order predicates as in Coq, hence the solver does not require a higher-order unification procedure.

The approach presented in this paper addresses all the concerns mentioned earlier. It takes advantage of the unification capabilities of the meta language at the price of handling problematic sub terms on the side. As a result our encoding takes advantage of indexing data structures and mode analysis for clause filtering. It is worth mentioning that we replace terms with variables only when it is strictly needed, leaving the rest of the term structure intact and hence indexable. Some preliminary benchmarks on the Stdpp library [12] show encouraging results: our type-class solver has some overhead on small goals but is consistently faster than the Coq one starting from goals made of 32 nodes. Moreover our approach is flexible enough to accommodate different strategies and heuristics to handle terms outside the pattern fragment. Finally, our encoding is sufficiently shallow to: 1) allow to lift forms of static analysis for the meta language, such as determinacy, also to the object language; 2) take advantage of future improvements to the logic-programming engine of Elpi, such as tabled search.

We considered mechanizing our results with Abella [8], especially in the early phase of this work, but unfortunately we could not. The main reason is that the logic of Abella does not let one quantify over predicates nor use the cut operator. Eliminating cut or higher order combinators like map orforall2 is surely possible, but has a high cost in verbosity given how pervasively they are used. Moreover, and more importantly, it creates a distance between the verified and the actual code, which we found to hinder our exploration. However, we did establish a test suite with about a hundred cases. It is available at https://github.com/FissoreD/ho-unif-for-free.
## ACKNOWLEDGMENTS

This work has been supported by the French government, through the France 2030 investment plan managed by the Agence Nationale de la Recherche, as part of the "UCA DS4H" project, reference ANR-17-EURE-0004.

## REFERENCES

[1] Andreas Abel and Brigitte Pientka. "Extensions to Miller's Pattern Unification for Dependent Types and Records". In: 2018. URL: https://api semanticscholar. org / CorpusID: 51885863.

[2] Adam Chlipala. *Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant*. The MIT Press, 2013. ISBN: 0262026651.

[3] Cvetan Dunchev et al. "ELPI: Fast, Embeddable, λProlog Interpreter". In: *Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings*. Ed. by Martin Davis et al. Vol. 9450. 2015, pp. 460-468. DOI: 10.1007/978-3-662-48899-7_32. URL: http://dx.doi.org/10.1007/978-3-662-48899-7%5C_32.

[4] Amy Felty. "Encoding the Calculus of Constructions in a Higher-Order Logic". In: ed. by M. Vardi. IEEE, June 1993, pp. 233-244. DOI: 10.1109/LICS.1993.287584.

[5] Amy Felty and Dale Miller. "Specifying theorem provers in a higher-order logic programming language". In: *Ninth International Conference on Automated Deduction*. Ed. by Ewing Lusk and Ross Overbeck. 310. Argonne, IL: Springer, May 1988, pp. 61-80. DOI: 10.1007/BFb0012823.

[6] Davide Fissore and Enrico Tassi. "A new Type-Class solver for Coq in Elpi". In: *The Coq Workshop 2023*. Bialystok, Poland, July 2023. URL: https://inria.hal.science/hal-04467855.

[7] Thom Fruehwirth. *Constraint Handling Rules - What Else? 2017*. arXiv: 1701.02668 [cs.PL].

[8] Andrew Gacek. *The Abella Interactive Theorem Prover (System Description)*. 2008. arXiv: 0803.2305 [cs.LO].

[9] Benjamin Grégoire, Jean-Christophe Léchenet, and Enrico Tassi. "Practical and sound equality tests, automatically - Deriving eqType instances for Jasmin's data types with Coq-Elpi". In: *CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2023: Proceedings* of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. Boston, MA, USA: ACM, Jan. 2023, pp. 167-181. DOI: 10.1145/3573105.3575683. URL: https://inria.hal.science/hal-03800154.

[10] Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. "Implementing type theory in higher order constraint logic programming". In: *Mathematical Structures in Computer Science* 29.8 (2019), pp. 1125-1150. DOI: 10.1017/S0960129518000427.

[11] Gérard P. Huet. "A Unification Algorithm for Typed lambda-Calculus". In: *Theor. Comput. Sci.* 1.1 (1975), pp. 27-57. DOI: 10.1016/0304-3975(75)90011-0. URL: https://doi.org/10.1016/0304-3975(75)90011-0.

[12] Ralf Jung et al. "Iris from the ground up: A modular foundation for higher-order concurrent separation logic". In: *Journal of Functional Programming* 28 (2018). DOI: 10.1017/S0956796818000151.

URL: https://api semanticscholar. org / CorpusID:2023423.

[13] Spiro Michaylov and Frank Pfenning. "Higher-Order Logic Programming as Constraint Logic Programming". In: *Principles and Practice of Constraint Programming*. 1993. URL: https://apiidis. org / CorpusID:9980455.

[14] Dale Miller. "A logic programming language with lambda-abstraction, function variables, and simple unification". In: *Extensions of Logic Programming*. Ed. by Peter Schroeder-Heister. Berlin, Heidelberg: Springer Berlin Heidelberg, 1991, pp. 253-281. ISBN: 978-3-540-46879-0.

[15] Dale Miller. "Unification under a mixed prefix". In: *Journal of Symbolic Computation* 14.4 (1992), pp. 321-358. DOI: 10.1016/0747-7171(92)90011-R.

[16] Dale Miller and Gopalan Nadathur. *Programming with Higher-Order Logic*. Cambridge University Press, 2012. DOI: 10.1017/CBO9781139021326.

[17] Gopalan Nadathur. "The Metalanguage λprolog and Its Implementation". In: *Functional and Logic Programming*. Ed. by Herbert Kuchen and Kazunori Ueda. Berlin, Heidelberg: Springer Berlin Heidelberg, 2001, pp. 1-20. ISBN: 978-3-540-44716-0.

[18] Gopalan Nadathur and Dale Miller. "An Overview of Lambda-Prolog". In: June 1988, pp. 810-827.

[19] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. *Isabelle/HOL - A Proof Assistant for Higher-Order Logic*. Vol. 2283. Lecture Notes in Computer Science. Springer, 2002. ISBN: 3-540-43376-7.

[20] Lawrence C. Paulson. "Set theory for verification. I: from foundations to functions". In: *J. Autom. Reason*. 11.3 (Dec. 1993), pp. 353-389. ISSN: 0168-7433. DOI: 10.1007/BF00881873. URL: https://doi.org/10.1007/BF00881873.

[21] F. Pfenning. "Elf: a language for logic definition and verified metaprogramming". In: *Proceedings of the Fourth Annual Symposium on Logic in Computer Science*. Pacific Grove, California, USA: IEEE Press, 1989, pp. 313-322. ISBN: 0818619546.

[22] Frank Pfenning and Conal Elliott. "Higher-order abstract syntax". In: *Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation*. PLDI '88. Atlanta, Georgia, USA: Association for Computing Machinery, 1988, pp. 199-208. ISBN: 0897912691. DOI: 10.1145/53990.54010. URL: https://doi.org/10.1145/53990.54010.

[23] Frank Pfenning and Carsten Schürmann. "System Description: Twelf — A Meta-Logical Framework for Deductive Systems". In: *Automated Deduction — CADE-16*. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 202-206. ISBN: 978-3-540-48660-2.

[24] Brigitte Pientka and Jana Dunfield. "Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)". In: *Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings*. Ed. by Jürgen Giesl and Reiner Hähnle. Vol. 6173. Lecture Notes in Computer Science. Springer, 2010, pp. 15-21. DOI: 10.1007/978-3-642-14203-1_2. URL: https://doi.org/10.1007/978-3-642-14203-1%5C_2.

[25] Matthieu Sozeau and Nicolas Oury. "First-Class Type Classes". In: *Theorem Proving in Higher Order Logics*. Ed. by Otmane
1393

1394

1395

1396

1397

1398

1399

1400

1401

1402

1403

1404

1405

1406

1407

1408

1409

1410

1411

1412

1413

1414

1415

1416

1417

1418

1419

1420

1421

1422

1423

1424

1425

1426

1427

1428

1429

1430

1431

1432

1433

1434

1435

1436

1437

1438

1439

1440

1441

1442

1443

1444

1445

1446

1447

1448

1449

1450

REFERENCES

[1] Andreas Abel and Brigitte Pientka. "Extensions to Miller's Pattern Unification for Dependent Types and Records". In: 2018. URL: https://api semanticscholar org / CorpusID : 51885863.

[2] Adam Chlipala. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013. ISBN: 0262026651.

[3] Cvetan Dunchev et al. "ELPI: Fast, Embeddable, λProlog Interpreter". In: Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings. Ed. by Martin Davis et al. Vol. 9450. 2015, pp. 460-468. DOI: 10.1007/978-3-662-48899-7\_32. URL: http://dx.doi.org/10.1007/978-3-662-48899-7%5C_32.

[4] Amy Felty. "Encoding the Calculus of Constructions in a Higher-Order Logic". In: ed. by M. Vardi. IEEE, June 1993, pp. 233-244. DOI: 10.1109/LICS.1993.287584.

[5] Amy Felty and Dale Miller. "Specifying theorem provers in a higher-order logic programming language". In: Ninth International Conference on Automated Deduction. Ed. by Ewing Lusk and Ross Overbeck. 310. Argonne, IL: Springer, May 1988, pp. 61-80. DOI: 10.1007/BFb0012823.

[6] Davide Fissore and Enrico Tassi. "A new Type-Class solver for Coq in Elpi". In: The Coq Workshop 2023. Bialystok, Poland, July 2023. URL: https://inria.hal.science/hal-04467855.

[7] Thom Fruehwirth. Constraint Handling Rules - What Else? 2017. arXiv: 1701.02668 [cs.PL].

[8] Andrew Gacek. The Abella Interactive Theorem Prover (System Description). 2008. arXiv: 0803.2305 [cs.LO].

[9] Benjamin Grégoire, Jean-Christophe Léchenet, and Enrico Tassi. "Practical and sound equality tests, automatically – Deriving eqType instances for Jasmin’s data types with Coq-Elpi". In: CPP ’23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. Boston, MA, USA: ACM, Jan. 2023, pp. 167-181. DOI: 10.1145/3573105.3575683. URL: https://inria.hal.science/hal-03800154.

[10] Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. "Implementing type theory in higher order constraint logic programming". In: Mathematical Structures in Computer Science 29.8 (2019), pp. 1125-1150. DOI: 10.1017/S0960129518000427.

[11] Gérard P. Huet. "A Unification Algorithm for Typed lambda-Calculus". In: Theor. Comput. Sci. 1.1 (1975), pp. 27-57. DOI: 10.1016/0304-3975(75)90011-0. URL: https://doi.org/10.1016/0304-3975(75)90011-0.

[12] Ralf Jung et al. "Iris from the ground up: A modular foundation for higher-order concurrent separation logic". In: Journal of Functional Programming 28 (2018). DOI: 10.1017/ S0956796818000151. URL: https://api semanticscholar org / CorpusID:2023423.

[13] Dale Miller. "Unification under a mixed prefix". In: Journal of Symbolic Computation 14.4 (1992), pp. 321-358. DOI: 10.1016/0747-7171(92)90011-R.

[14] Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, 2012. DOI: 10.1017/ CBO9781139021326.

[15] Gopalan Nadathur. "The Metalanguage λprolog and Its Implementation". In: Functional and Logic Programming. Ed. by Herbert Kuchen and Kazunori Ueda. Berlin, Heidelberg: Springer Berlin Heidelberg, 2001, pp. 1-20. ISBN: 978-3-540-44716-0.

[16] Gopalan Nadathur and Dale Miller. "An Overview of Lambda-Prolog". In: June 1988, pp. 810-827.

[17] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Vol. 2283. Lecture Notes in Computer Science. Springer, 2002. ISBN: 3-540-43376-7.

[18] Lawrence C. Paulson. "Set theory for verification. I: from foundations to functions". In: J. Autom. Reason. 11.3 (Dec. 1993), pp. 353-389. ISSN: 0168-7433. DOI: 10.1007/BF00881873. URL: https://doi.org/10.1007/BF00881873.

[19] F. Pfenning. "Elf: a language for logic definition and verified metaprogramming". In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science. Pacific Grove, California, USA: IEEE Press, 1989, pp. 313-322. ISBN: 0818619546.

[20] Frank Pfenning and Conal Elliott. "Higher-order abstract syntax". In: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation. PLDI '88. Atlanta, Georgia, USA: Association for Computing Machinery, 1988, pp. 199-208. ISBN: 0897912691. DOI: 10.1145/53990.54010. URL: https://doi.org/10.1145/53990.54010.

[21] Frank Pfenning and Carsten Schürmann. "System Description: Twelf — A Meta-Logical Framework for Deductive Systems". In: Automated Deduction — CADE-16. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 202-206. ISBN: 978-3-540-48660-2.

[22] Brigitte Pientka and Jana Dunfield. "Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)". In: Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings. Ed. by Jürgen Giesl and Reiner Hähnle. Vol. 6173. Lecture Notes in Computer Science. Springer, 2010, pp. 15-21. DOI: 10.1007/978-3-642-14203-1\_2. URL: https://doi.org/10.1007/978-3-642-14203-1%5C_2.

[23] Matthieu Sozeau and Nicolas Oury. "First-Class Type Classes". In: Theorem Proving in Higher Order Logics. Ed. by Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 278-293. ISBN: 978-3-540-71067-7.

[24] Enrico Tassi. "Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq". In: ITP 2019 - 10th International Conference on Interactive Theorem Proving. Portland, OR, United States, Sept. 2019. DOI: 10.4230/LIPIcs.CVIT.2016.23. URL: https://inria.hal.science/hal-01897468.

[25] Enrico Tassi. "Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)". In: The Fourth International Workshop on Coq for Programming Languages. Los Angeles, CA, United States, Jan. 2018. URL: https://inria.hal.science/hal-01637063.

1451

1452

1453

1454

1455

1456

1457

1458

1459

1460

1461

1462

1463

1464

1465

1466

1467

1468

1469

1470

1471

1472

1473

1474

1475

1476

1477

1478

1479

1480

1481

1482

1483

1484

1485

1486

1487

1488

1489

1490

1491

1492

1493

1494

1495

1496

1497

1498

1499

1500

1501

1502

1503

1504

1505

1506

1507

1508
Ait Mohamed, César Muñoz, and Sofiène Tahar. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 278–293. ISBN: 978-3-540-71067-7.

[26] Enrico Tassi. "Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq". In: *ITP 2019 - 10th International Conference on Interactive Theorem Proving*. Portland, OR, United States, Sept. 2019. DOI: 10.4230/LIPIcs.CVIT.2016.23. URL: https://inria.hal.science/hal-01897468.

[27] Enrico Tassi. "Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)". In: *The Fourth International Workshop on Coq for Programming Languages*. Los Angeles, CA, United States, Jan. 2018. URL: https://inria.hal.science/hal-01637063.

[28] The Coq Development Team. *The Coq Reference Manual – Release 8.18.0*. https://coq.inria.fr/doc/V8.18.0/refman. 2023.

[29] P. Wadler and S. Blott. "How to Make Ad-Hoc Polymorphism Less Ad Hoc". In: *Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*. POPL '89. Austin, Texas, USA: Association for Computing Machinery, 1989, pp. 60–76. ISBN: 0897912942. DOI: 10.1145/75277.75283. URL: https://doi.org/10.1145/75277.75283.

[30] Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. "The Isabelle Framework". In: *Theorem Proving in Higher Order Logics*. Ed. by Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 33–38. ISBN: 978-3-540-71067-7.

[31] Markus Wenzel. "Type classes and overloading in higher-order logic". In: *Theorem Proving in Higher Order Logics*. Ed. by Elsa L. Gunter and Amy Felty. Berlin, Heidelberg: Springer Berlin Heidelberg, 1997, pp. 307–322. ISBN: 978-3-540-69526-4.
1509

1510

1511

1512

1513

1514

1515

1516

1517

1518

1519

1520

1521

1522

1523

1524

1525

1526

1527

1528

1529

1530

1531

1532

1533

1534

1535

1536

1537

1538

1539

1540

1541

1542

1543

1544

1545

1546

1547

1548

1549

1550

1551

1552

1553

1554

1555

1556

1557

1558

1559

1560

1561

1562

1563

1564

1565

1566

[26] The Coq Development Team. *The Coq Reference Manual – Release 8.18.0*. https://coq.inria.fr/doc/V8.18.0/refman. 2023.

[27] P. Wadler and S. Blott. "How to Make Ad-Hoc Polymorphism Less Ad Hoc". In: *Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*. POPL '89. Austin, Texas, USA: Association for Computing Machinery, 1989, pp. 60–76. ISBN: 0897912942. DOI: 10.1145/75277.75283. URL: https://doi.org/10.1145/75277.75283.

[28] Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. "The Isabelle Framework". In: *Theorem Proving in Higher Order Logics*. Ed. by Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 33–38. ISBN: 978-3-540-71067-7.

[29] Markus Wenzel. "Type classes and overloading in higher-order logic". In: *Theorem Proving in Higher Order Logics*. Ed. by Elsa L. Gunter and Amy Felty. Berlin, Heidelberg: Springer Berlin Heidelberg, 1997, pp. 307–322. ISBN: 978-3-540-69526-4.

1567

1568

1569

1570

1571

1572

1573

1574

1575

1576

1577

1578

1579

1580

1581

1582

1583

1584

1585

1586

1587

1588

1589

1590

1591

1592

1593

1594

1595

1596

1597

1598

1599

1600

1601

1602

1603

1604

1605

1606

1607

1608

1609

1610

1611

1612

1613

1614

1615

1616

1617

1618

1619

1620

1621

1622

1623

1624