# Generalising Huet-style Projections in E-unification for Second-Order Abstract Syntax

Nikolai Kudasov

► To cite this version:

Nikolai Kudasov. Generalising Huet-style Projections in E-unification for Second-Order Abstract Syntax. UNIF 2023 - 37th International Workshop on Unification, Veena Ravishankar; Christophe Ringeissen, Jul 2023, Rome, Italy. hal-04128229

HAL Id: hal-04128229

https://inria.hal.science/hal-04128229

Submitted on 14 Jun 2023

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_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Generalising Huet-style Projections in E-unification for Second-Order Abstract Syntax

Nikolai Kudasov

Innopolis University, Innopolis, Tatarstan, Russia
n.kudasov@innopolis.ru

## Abstract

Second-order abstract syntax (SOAS) provides a well-founded framework when working with languages that have arbitrary binders. E-unification for SOAS is powerful enough to encode both E-unification and higher-order unification (HOU). In a previous work, we have presented an E-unification procedure, drawing inspiration from both E-unification and HOU algorithms. In this paper, we present a work-in-progress on an more efficient version of the procedure, aiming to bring E-unification for SOAS to perform on par with HOU algorithms. More specifically, in this work we focus on a generalisation of Huet-style projections (also known as *partial bindings* in HOU literature), commonly used in HOU algorithms.

## Contents

<table><tr><td>1</td><td>Introduction</td><td>1</td></tr><tr><td>2</td><td>E-unification for Second-Order Abstract Syntax</td><td>2</td></tr><tr><td>2.1</td><td>Second-Order Abstract Syntax</td><td>2</td></tr><tr><td>2.2</td><td>E-unification procedure for SOAS</td><td>3</td></tr><tr><td>3</td><td>Generalising Huet-style projection</td><td>4</td></tr><tr><td>3.1</td><td>Huet-style projection</td><td>4</td></tr><tr><td>3.2</td><td>Adding product types</td><td>5</td></tr><tr><td>3.3</td><td>Generalising to SOAS</td><td>6</td></tr><tr><td>4</td><td>Conclusion</td><td>6</td></tr></table>

## 1 Introduction

Second-order abstract syntax (SOAS) [3] offers a mathematically sound approach to work with languages with binders. SOAS is an abstract syntax with variable bindings and parameterised VARIABLES. FIORE and SZAMOZVANCEV [2] have successfully used SOAS to generate metatheory in Agda for user-defined languages with variable bindings. SOAS has also been used by Makoto Hamana in his studies of second-order rewriting and Second-Order Laboratory [5].

In a previous work, the author [9, 10] has introduced E-unification for second-order abstract syntax, combining approaches from first-order E-unification [4] and higher-order unification (HOU) [7, 13]. Although the algorithm is sound and complete, it is not particularly efficient and several directions for improvements are outlined in the papers.

In another work, the author [8] has implemented a typechecking algorithm based on a (simplified) second-order abstract syntax. One of the heuristics used in that implementation resembles generalised Huet-style project bindings for untyped syntax.
<figure><img src="image_2.png" /><figcaption>Figure 1: Second-order terms in context.</figcaption></figure>

In this paper, we demonstrate a work-in-progress for improving the efficiency of E-unification procedure for SOAS, by attempting to generalise Huet-style projection bindings (used in many HOU algorithms [6, 12, 1, 11, 13]) in the simply-typed setting, use them to improve (project), (imitate), and (iterate) transition rules [10, Section 4.2] and cut down the search space for the unification procedure [10, Definition 33].

# 2 E-unification for Second-Order Abstract Syntax

## 2.1 Second-Order Abstract Syntax

Second-order abstract syntax [3, Section 2] consists of

1. A signature $\Sigma$, defining the set of types T and available operators. Each operator F has an *arity* $(\overline{\sigma_1}..\overline{\sigma_n}, \tau)$ $\to$ $\tau$, that specifies a return type $\tau$ and, for each argument, types of bound variables $\overline{\sigma_i}$ introduced in that argument, and the type $\tau_i$ of the argument itself.

2. Typing contexts $\Xi$ | $\Gamma$, where $\Xi$ defines the types of parametrised metavariables and $\Gamma$ specifies the types of regular variables. For each metavariable typing $M: [\overline{\sigma}]\tau$, we specify the types of all parameters $\overline{\sigma}$ as well as the return type $\tau$.

3. Terms that are given by the rules in Fig. 1.

An *equational presentation* [3, Section 5] is a set of axioms each of which is a pair of terms in context.

**Example 1.** A signature for simply-typed $\lambda$-calculus with pairs over a set of base types A consists of:

1. a set of types $A^{\Rightarrow, \times}$ given by

$$ \frac{\tau \in A}{\tau \in A^{\Rightarrow, \times}} \qquad \frac{\sigma, \tau \in A^{\Rightarrow, \times}}{\sigma \Rightarrow \tau \in A^{\Rightarrow, \times}} \qquad \frac{\sigma, \tau \in A^{\Rightarrow, \times}}{\sigma \times \tau \in A^{\Rightarrow, \times}} $$
2. a family of operators for all $\sigma, \tau \in A \Rightarrow \times$

abs$^{\sigma,\tau}$ : $\sigma.\tau \to (\sigma \Rightarrow \tau)$ (abstraction)

app$^{\sigma,\tau}$ : $(\sigma \Rightarrow \tau, \sigma) \to \tau$ (application)

pair$^{\sigma,\tau}$ : $(\sigma, \tau) \to \sigma \times \tau$ (pair constructor)

fst$^{\sigma,\tau}$ : $\sigma \times \tau \to \sigma$ (first projection)

snd$^{\sigma,\tau}$ : $\sigma \times \tau \to \tau$ (second projection)

**Example 2.** The equational presentation of the simply-typed λ-calculus with pairs:

$M : [\sigma]\tau, N : []\sigma \mid \vdash \mathbf{app}(\mathbf{abs}(x.M[x]), N[]) \equiv M[N_] : \tau$ ($\beta_\lambda$)

$M : []\sigma, N : []\tau \mid \vdash \mathbf{fst}(\mathbf{pair}(M[], N[])) \equiv M[] : \sigma$ ($\beta_{\pi_1}$)

$M : []\sigma, N : []\tau \mid \vdash \mathbf{snd}(\mathbf{pair}(M[], N[])) \equiv N[] : \tau$ ($\beta_{\pi_2}$)

$M : []\sigma \Rightarrow \tau \mid \vdash \mathbf{abs}(x.\mathbf{app}(M[], x)) \equiv M[] : \sigma \Rightarrow \tau$ ($\eta_\lambda$)

$M : []\sigma \times \tau \mid \vdash \mathbf{pair}(\mathbf{fst}(M[]), \mathbf{snd}(M[])) \equiv M[] : \sigma \times \tau$ ($\eta_\times$)

## 2.2 E-unification procedure for SOAS

E-unification problems for SOAS are about finding a variable substitution that satisfies all of the collection of second-order constraints (i.e. equalities of second-order terms):

**Definition 1** ([10, Definition 8]). *Given an equational presentation E, an E-unification problem (Θ, S) is a finite set S of second-order constraints in a shared variable context Θ. We present an E-unification problem as a formula of the following form:*

$$ \exists (M_1 : [\sigma_1]\tau_1, \dots, M_n : [\sigma_n]\tau_n). (\forall (z_1 : \bar{\rho}_1). s_1 \stackrel{?}{=} t_1 : \tau_1) \wedge \dots \wedge (\forall (z_k : \bar{\rho}_k). s_k \stackrel{?}{=} t_k : \tau_k) $$

Here is an example of E-unification problem for simply-typed λ-terms:

$$ \exists (M : [\sigma \Rightarrow \tau, (\sigma \Rightarrow \tau) \Rightarrow \tau]) \forall (g : \sigma \Rightarrow \tau, y : \sigma). M[g, \mathbf{abs}(x.\mathbf{app}(x, y))] \stackrel{?}{=} \mathbf{app}(g, y) : \tau $$

An E-unification procedure introduced in a previous work [10] consists of a collection of transition rules that are applied non-deterministically:

**Definition 2** ([10, Definition 33]). *The E-unification procedure over an equational presentation E is defined by repeatedly applying the following transitions (non-deterministically) until a stop:*

1. If no constraints are left, then stop (succeed).

2. If possible, apply (**delete**) rule.

3. If possible, apply (**mutate**) or (**decompose**) rule (non-det.).

4. If there is a constraint consisting of two non-metavariables and none of the above transitions apply, stop (**fail**).

5. If there is a constraint $M[...] \stackrel{?}{=} F(...)$, apply (**imitate**) or (**project**) rules (non-det.).

6. If there is a constraint $M[...] \stackrel{?}{=} x$, apply (**project**) rules (non-det.).

7. If possible, apply (**identify**), (**eliminate**), or (**iterate**) rules (non-det.).
8. If none of the rules above are applicable, then stop (fail).

We refer the reader to [10, Section 4] for the full description and examples of the transition rules. Importantly, all of these rules rely on exact matching with axioms (in particular, computation rules of a given language), use type information superficially, resulting in a small-step advancements towards a solution. For example, constraint `app(app(M], t₁), t₂) =? r` will perform two (mutate) rules to first figure out substitution `M] ↦ abs(x₁.abs(x₂.M₂[x₁, x₂]))` and get to solving `M₂[t₁, t₂] =? r`. Furthermore, without relying on the types of `t₁`, `t₂`, and `r` parameters, the procedure has to fallback to trial and error in figuring out how to use `t₁`, `t₂` to produce `r`. Huet-style projection [6], explicitly avoided in these transition rules, relies on the types of the arguments of a variable, to properly eliminate them in a single step. Instead, the procedure relies only on Jensen-Pietrzykowski-style (JP-style) [7], which simply selects the parameter to be used, but defers proper elimination (e.g. application to arguments) to other parts of the procedure.

# 3 Generalising Huet-style projection

## 3.1 Huet-style projection

We start with a formal definition of Huet-style projection bindings for first-order syntax:

**Definition 3.** Let $M: \alpha_1 \Rightarrow \dots \Rightarrow \alpha_n \Rightarrow \beta$ and for some $i$, $\alpha_i = \gamma_1 \Rightarrow \dots \Rightarrow \gamma_m \Rightarrow \beta$ such that $n > 0$ and $m \ge 0$. Then a first-order Huet-style projection binding is a substitution

$$M \mapsto \lambda \bar{x}.x_i (H_1 \bar{x}) \dots (H_m \bar{x})$$

where the *metavariables* $\bar{H}$ are fresh and bound variables $\bar{x}$ are of appropriate types (note that $i$ in $x_i$ and $\alpha_i$ is the same).

In a higher-order unification procedure, this binding can be used whenever we want to use one of the parameters of a *metavariable* directly to produce the desired term. For example, consider the following unification problem:

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\begin{array}{@{}c@{}}
  \begin{array}{@{}l@{}}
    \mathsf{M} (\lambda x.x y) f \stackrel{?}{=} f y \\
    \xrightarrow{\mathsf{H\text{-project}}} (\lambda x_1 x_2.x_1 (\mathsf{H}_1 x_1 x_2)) (\lambda x.x y) f \stackrel{?}{=} f y
  \end{array} &
  \text{via } [\mathsf{M} \mapsto \lambda x_1 x_2.x_1 (\mathsf{H}_1 x_1 x_2)] & \\
  \rightarrow_{\beta}^{*} (\mathsf{H}_1 (\lambda x.x y) f) y \stackrel{?}{=} f y & & \\
  \begin{array}{@{}c@{}}
    \begin{array}{@{}l@{}}
      \mathsf{decompose} \rightarrow \mathsf{H}_1 (\lambda x.x y) f \stackrel{?}{=} f \\
      \xrightarrow{\mathsf{JP\text{-project}}} ((\lambda x_1 x_2.x_2) (\lambda x.x y) f) \stackrel{?}{=} f
    \end{array} &
    \text{via } [\mathsf{H}_1 \mapsto \lambda x_1 x_2.x_2] & \\
    \rightarrow_{\beta}^{*} f \stackrel{?}{=} f & &
  \end{array} & &
\end{array}
$$

Let us recognise the following components of Definition 3:

1. The type of $i$-th parameter $(\alpha_i)$ determines if this parameter can be used to extract the result of type $\beta$. Note that $\gamma_1 \Rightarrow \gamma_2 \Rightarrow \beta = \gamma_1 \Rightarrow (\gamma_2 \Rightarrow \beta)$, which means, that we may need to go deep into the structure of the type $\alpha_i$ to understand if it contains the type $\beta$, moreover, if $\beta$ appears in a position that is suitable for extraction (a positive position for function types).
2. The type of M specifies the parameters as well as the return type. The usual assumption is that $\beta$ is not itself a function type. We use the parameter types to *introduce* as many parameters as needed using $\lambda$-abstraction.

3. The structure of the type of i-th parameter tells us how to *eliminate* it using a proper number of arguments to extract a term of type $\beta$.

4. Each argument used in the elimination of $x_i : \alpha_i$ is a fresh *metavariable* with the same parameters as the original *metavariable*. The arguments are added using function application (represented by juxtaposition) which is the eliminator for function types.

## 3.2 Adding product types

Let us add product types, pairs of terms, and pair projections to the simply typed $\lambda$-calculus:

1. For all types $\sigma, \tau$, we add the product type $\sigma \times \tau$.

2. If $t_1 : \sigma$ and $t_2 : \tau$ are terms, then $\langle t_1, t_2 \rangle : \sigma \times \tau$ is a pair.

3. If $t : \sigma \times \tau$, then $\pi_1 t : \sigma$ and $\pi_2 t : \tau$ are the first and second projections, respectively.

Consider the constraint

$$ M \langle \lambda x.x y, f \rangle \stackrel{?}{=} f y $$

Assuming $f : \sigma \Rightarrow \tau$ and $y : \sigma$, the type of the only parameter to M is $((\sigma \Rightarrow \tau) \Rightarrow \tau) \times (\sigma \Rightarrow \tau)$.

It is clear that we should can extract both components with $\pi_1$ or $\pi_2$ projections. In particular, a binding that will lead to a unifier for this constraint looks as follows:

$$ M \mapsto \lambda x_1. \pi_1 x_1 (H_1 x_1) $$

We observe the following from this example:

1. The type of a parameter to M determines whether it can be used to extract the result of appropriate type.

2. The structure of the parameter type tells us how to *eliminate* it. However, unlike the case of function types, we now have two eliminators: $\pi_1$ and $\pi_2$.

To generalise Huet-style projection bindings to include product types, we define the set of possible formulas on the right hand side recursively over the type of i-th parameter of the *metavariable*.

$$ 1. \text{rhs}_{\bar{x},\beta}(t, \beta) = \{t\} $$

$$ 2. \text{rhs}_{\bar{x},\beta}(t, \delta) = \emptyset \text{ when } \delta \neq \beta \text{ and } \delta \text{ is not a function or product type} $$

$$ 3. \text{rhs}_{\bar{x},\beta}(t, \gamma \Rightarrow \delta) = \text{rhs}_{\bar{x},\beta}(t (H_1 \bar{x}), \delta) \text{ where } H_1 : \alpha_1 \Rightarrow \dots \Rightarrow \alpha_n \Rightarrow \gamma \text{ is fresh} $$

$$ 4. \text{rhs}_{\bar{x},\beta}(t, \delta_1 \times \delta_2) = \text{rhs}_{\bar{x},\beta}(\pi_1 t, \delta_1) \cup \text{rhs}_{\bar{x},\beta}(\pi_2 t, \delta_2) $$

The set of possible Huet-style projection bindings for *metavariable* M : $\alpha_1 \Rightarrow \dots \Rightarrow \alpha_n \Rightarrow \beta$ at position i is defined as

$$ \{[M \mapsto \lambda \bar{x}.s] \mid s \in \text{rhs}_{\bar{x},\beta}(x_i, \alpha_i)\} $$

The cases 3 and 4 above stem from the canonical values for function and product types and the following computation rules for simply-typed $\lambda$-calculus with pairs:

$$ (\lambda x.M) N \rightarrow [x \mapsto N]M \qquad (\beta_{\lambda}) $$

$$ \pi_1 \langle M, N \rangle \rightarrow M \qquad (\beta_{\pi_1}) $$

$$ \pi_2 \langle M, N \rangle \rightarrow N \qquad (\beta_{\pi_2}) $$
This suggests that a generalisation of Huet-style bindings is possible based on the set of type constructors and the set of axioms E as given in Example 2.

## 3.3 Generalising to SOAS

We now consider a generalisation of Huet-style projection bindings for an arbitrary second-order abstract syntax. First, assume that $M : [\alpha_1, \dots, \alpha_n]\beta$. Let $x : \alpha_1, \dots, x_n : \alpha_n$. Then we define the set of right-hand side formulas $\text{rhs}_{\bar{x},\beta}$ recursively as follows:

1. $\text{rhs}_{\bar{x},\beta}(t, \beta) = \{t\}$

2. $\text{rhs}_{\bar{x},\beta}(t, \delta) = \bigcup_{\langle l, \xi \rangle \in L} \text{rhs}_{\bar{x},\beta}([y \mapsto t]\xi l, \varepsilon)$

where $L = \{\langle l, \xi \rangle \mid \exists (\Theta \mid \vdash s : \delta).(\Theta \mid \vdash [y \mapsto s]l \equiv r : \varepsilon) \in E\}$

and each $l \neq y$ and each $\xi$ instantiates $l$ in the appropriate context by substituting each
metavariable with a fresh one

3. $\text{rhs}_{\bar{x},\beta}(t, \delta) = \emptyset$ otherwise

Intuitively, the set $L$ in case 2 specifies all possible contexts where we could put a term of type $\delta$ such that one of the axioms (e.g. computation rules) will fire. Note that we are not looking at the term $t$ to find such contexts, only its type. For example, if $\delta = \sigma \Rightarrow \tau$ and we work in $\lambda$-calculus, then the first axiom in Example 2 has a proper subterm of this type, which means that $\text{rhs}_{\bar{x},\tau}(t, \sigma \Rightarrow \tau) = \{\text{app}(t, N[\bar{x}])\}$ where $N : [\alpha_1, \dots, \alpha_n]\sigma$ is a fresh variable.

The set of generalised Huet-style projection bindings for a given type $M : [\alpha_1, \dots, \alpha_n]\beta$ at position $i$ is defined as

$$ \{[M[\bar{x}] \mapsto s] \mid s \in \text{rhs}_{\bar{x},\beta}(x_i, \alpha_i)\} $$

Note that such sets of binding can be precomputed for a given set of types $T$ and axioms $E$. Once computed, it is possible to use Huet-style bindings to cut down the search space for the $E$-unification procedure. In particular, the (project), (imitate), and (iterate) transition rules may be improved.

Intuitively, the improvement comes from the fact that we perform a substitution that brings us as much as possible to the application of the (mutate) rule, instead of guessing which path will work.

## 4 Conclusion

We have described an approach to generalise Huet-style bindings and sketched a way those can be used to reduce the search space for the E-unification procedure for second-order syntax, making a step towards an efficient E-unification procedure. It remains to properly update the procedure, formalising conditions when Huet-style projections must be utilised (we expect it to be similar to full HOU procedure by Vukmirovic, Bentkamp, and Nummelin [13]). It would also be good to see the theoretical performance improvement confirmed with an implementation and benchmarking, especially in comparison with the existing implementations of HOU not based on SOAS.

## References

[1] Dominic Duggan. Unification with extended patterns. *Theor. Comput. Sci.*, 206(1-2):1-50, 1998.
[2] Marcelo Fiore and Dmitrij Szamozvancev. Formal Metatheory of Second-Order Abstract Syntax. *Proc. ACM Program. Lang.*, 6(POPL), jan 2022.

[3] Marcelo P. Fiore and Chung-Kil Hur. Second-Order Equational Logic (Extended Abstract). In Anuj Dawar and Helmut Veith, editors, *Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings*, volume 6247 of *Lecture Notes in Computer Science*, pages 320-335. Springer, 2010.

[4] Jean H. Gallier and Wayne Snyder. Complete sets of transformations for general E-unification. *Theor. Comput. Sci.*, 67(2&3):203-260, 1989.

[5] Makoto Hamana. Theory and practice of second-order rewriting: Foundation, evolution, and SOL. In Keisuke Nakano and Konstantinos Sagonas, editors, *Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings*, volume 12073 of *Lecture Notes in Computer Science*, pages 3-9. Springer, 2020.

[6] Gérard P. Huet. A unification algorithm for typed lambda-calculus. *Theor. Comput. Sci.*, 1(1):27-57, 1975.

[7] D. C. Jensen and Tomasz Pietrzykowski. Mechanizing ω-order type theory through unification. *Theor. Comput. Sci.*, 3(2):123-171, 1976.

[8] Nikolai Kudasov. Functional Pearl: Dependent type inference via free higher-order unification, 2022.

[9] Nikolai Kudasov. Higher-order unification from e-unification with second-order equations and parametrised metavariables. In *UNIF 2022 Worskhop Proceedings. The 36th International Workshop on Unification*. EasyChair, 2022.

[10] Nikolai Kudasov. E-unification for second-order abstract syntax. In Marco Gaboardi and Femke van Raamsdonk, editors, *8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), FSCD 2023, July 3-July 6, 2023, Rome, Italy*, volume 260 of *LIPIcs*, pages 6:1-6:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.

[11] Tomer Libal and Dale Miller. Functions-as-Constructors Higher-Order Unification. In Delia Kesner and Brigitte Pientka, editors, *1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal*, volume 52 of *LIPIcs*, pages 26:1-26:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.

[12] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. *J. Log. Comput.*, 1(4):497-536, 1991.

[13] Petar Vukmirovic, Alexander Bentkamp, and Visa Nummelin. Efficient Full Higher-Order Unification. *Log. Methods Comput. Sci.*, 17(4), 2021.