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

HAL
open science

# Checking the type safety of rewrite rules in the $\lambda\Pi$-calculus modulo rewriting

Jui-Hsuan Wu

► To cite this version:

Jui-Hsuan Wu. Checking the type safety of rewrite rules in the $\lambda\Pi$-calculus modulo rewriting. Computer Science [cs]. 2019. hal-02288720

HAL Id: hal-02288720

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

Submitted on 15 Sep 2019

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
ÉCOLE NORMALE SUPÉRIEURE

COMPUTER SCIENCE DEPARTMENT

INTERNSHIP REPORT

Checking the type safety of rewrite rules in λΠ-calculus modulo
rewriting

WU JUI-HSUAN

supervised by

FRÉDÉRIC BLANQUI¹² & VALENTIN BLOT¹²

¹INRIA

²ENS Paris-Saclay

11 March 2019 – 31 July 2019
# 1 Introduction

Lambdapi is a new proof assistant based on the $\lambda\Pi$-calculus modulo theory [5], which extends the simply typed lambda calculus with dependent types and an equivalence relation on types generated by user-defined rewrite rules. The expressiveness of rewriting allows to formalize proofs that cannot be done in other proof assistants. However, as Lambdapi is based on the propositions-as-types interpretation, one should verify that the system satisfies the subject reduction property before starting to construct proofs within it. During my internship, I studied a new algorithm proposed by F. Blanqui for checking type preservation of rewrite rules and implemented it in Lambdapi. Besides, in order to improve the unification (modulo rewriting) procedure, I designed an algorithm for checking injectivity of function symbols.

# 2 $\lambda\Pi$-calculus modulo

## 2.1 $\lambda\Pi$-calculus

The $\lambda\Pi$-calculus is an extension of the simply typed lambda calculus ($\lambda \to$) with dependent types. In this calculus, we introduce a particular type $Type$ and "types" in $\lambda \to$ are just terms of type $Type$ in the $\lambda\Pi$-calculus. Some terms have the type $A \to Type$, where $A$ is of type $Type$, and can be applied to a term $t$ of type $A$ to build a type depending on $t$. Besides, a type $Kind$ is introduced as the type of terms $Type$, $A \to Type$, etc. Finally, the usual arrow $A \to B$ is extended to the dependent product $\Pi x : A.B$ to handle the possible dependency of the type $B$ on the type $A$.

We write $S$ for the set of sorts $\{Type, Kind\}$ and we assume given a set $\mathcal{X} = \{x, y, z, \dots\}$ of variables and a set $\mathcal{F}$ of function symbols.

Then we can define the set $\mathcal{T}$ of terms of the $\lambda\Pi$-calculus.

**Definition 2.1.** (Term) The set of terms in the $\lambda\Pi$-calculus is given by:

$$t := x \mid s \mid f \mid tt \mid \lambda x : t.t \mid \Pi x : t.t, \text{ where } x \in \mathcal{X}, s \in S \text{ and } f \in \mathcal{F}$$

We then assume that each function symbol $f$ is equipped with a type $\tau(f)$ and a sort $s(f)$. If $\tau(f) = \Pi x_1 : T_1 \dots \Pi x_n : T_n.U$ where $U$ is not a product, then $f$ is said of arity $n$. In fact, function symbols can be regarded as variables declared in a global context ("signature") of the system.

We now present the typing rules of the $\lambda\Pi$-calculus:

Well-formedness of the empty context

[ ] well-formed

Declaration of a variable

$$\frac{\Gamma \vdash A : s}{\Gamma, x : A \text{ well-formed}} s \in S$$

Type is of type Kind

$$\frac{\Gamma \text{ well-formed}}{\Gamma \vdash Type : Kind}$$

Variable

$$\frac{\Gamma \text{ well-formed}}{\Gamma \vdash x : A} x : A \in \Gamma$$
Product

$$ \frac{\Gamma \vdash A : Type \quad \Gamma, x : A \vdash B : s}{\Gamma \vdash \Pi x : A.B : s} \quad s \in S $$

Abstraction

$$ \frac{\Gamma \vdash A : Type \quad \Gamma, x : A \vdash B : s \quad \Gamma, x : A \vdash t : B}{\Gamma \vdash \lambda x : A.t : \Pi x : A.B} \quad s \in S $$

Application

$$ \frac{\Gamma \vdash t : \Pi x : A.B \quad \Gamma \vdash u : A}{\Gamma \vdash t u : (u/x)B} $$

Function symbols

$$ \frac{\vdash \tau(f) : s(f)}{\vdash f : \tau(f)} $$

Conversion

$$ \frac{\Gamma \vdash t : A \quad \Gamma \vdash A : s \quad \Gamma \vdash B : s}{\Gamma \vdash t : B} \quad s \in S, A \equiv_{\beta} B $$

**Fig. 1.** Typing rules of the λΠ-calculus.

We have the uniqueness (modulo $\equiv_{\beta}$) of types in λΠ-calculus.

**Proposition 2.1.** For all $\Gamma, t, A, B$, if $\Gamma \vdash t : A$ and $\Gamma \vdash t : B$, then $A \equiv_{\beta} B$.

## 2.2 λΠ-calculus modulo rewriting

The λΠ-calculus modulo rewriting is an extension of the λΠ-calculus with a set $R$ of rewrite rules. Let $\equiv$ be the minimal congruence that contains $R$ and $\beta$-conversion. The typing rules of the λΠ-calculus modulo $R$ can be obtained from those of the λΠ-calculus by replacing $\equiv_{\beta}$ with $\equiv$ in the conversion rule.

**Notation 2.1.** In the following, we denote the smallest congruence containing a relation $S$ by $\equiv_S$.

## 2.3 Lambdapi

### 2.3.1 Metavariables

In Lambdapi, we extend the λΠ-calculus modulo by introducing metavariables which are used to represent yet unknown term. We denote by $\mathcal{M}$ the set of metavariables.

$$ t := \dots | M \text{ where } M \in \mathcal{M} $$

We now define the types of metavariables and the algebraic fragment of Lambdapi.

Each metavariable $M$ is equipped with a type $t_M$, with some constraints explained below.

The type of a yet unknown object-level term is also yet unknown, but the type of this type should be a sort. We distinguish thus object-level metavariables and type-level metavariables:

**Definition 2.2.**

* A type-level metavariable is a metavariable $M$ s.t. $t_M \in S$.
* An object-level metabariable is a metabariable M s.t. $t_M$ is a type-level metabariable.

* A metabariable is either a type-level metabariable or an object-level metabariable.

* We denote by $M_0$ the set of object-level variables and by $Meta(t)$ the set of object-level variables occurring in $t$.

The algebraic fragment of the terms of Lambdapi corresponds to the terms of first-order rewriting:

**Definition 2.3.** Let $A_0$ be the smallest set of terms such that $M_0 \subseteq A_0$, and $fa_1 \cdots a_n \in A_0$ for all $f \in \mathcal{F}$, $a_1, \cdots, a_n \in A_0$. The set $\mathcal{A}$ of algebraic terms is defined as $A_0 - M_0$

We now define *substitutions*.

**Definition 2.4.** (substitutions) A substitution $\sigma$ is a map assigning to each metabariable M a term. Its application to a term is defined as follows:

* $x\sigma = x$ for $x \in \mathcal{X}$

* $f\sigma = f$ for $f \in \mathcal{F}$

* $(tu)\sigma = (t\sigma)(u\sigma)$

* $(\lambda x : A.t)\sigma = \lambda x : A\sigma.t\sigma$

* $(\Pi x : A.t)\sigma = \Pi x : A\sigma.t\sigma$

* $M\sigma = \sigma(M)$

* We define the domain $dom(\sigma)$ of a substitution $\sigma$ as the set $\{M \in \mathcal{M} | M\sigma \neq M\}$.

### 2.3.2 Type inference and type checking

The type inference relation of Lambdapi is the same as that of the $\lambda\Pi$-calculus modulo rewriting. Note that, if a term contains a metabariable, then it is not typable.

Since variables are used to represent unknown terms in a term $t$, one might want to infer the constraints on terms replacing the variables of $t$ that need to be satisfied to make the term $t$ typable.

We now present the constraint-generating type inference and type checking algorithm for algebraic terms, consisting of the following judgement forms.

$\Gamma \vdash t \uparrow A[E]$ type checking

$\Gamma \vdash t \downarrow A[E]$ type inference

Note that we add a special field $E$ which contains a set of constraints.

Function applications

$$ \tau(f) = \Pi x_1 : A_1. \cdots \Pi x_n : A_n.U \quad \forall i \in \{1, \cdots, n\}, \vdash t_i \uparrow A_i[E_i] \\ \vdash f t_1 \cdots t_n \downarrow (t_1/x_1, \cdots, t_n/x_n) U[\bigcup_{1 \le i \le n} E_i] $$

Object-level variables

$$ \vdash M \uparrow T[\{(t_M, T)\}] $$
Type checking of function applications

$$ \frac{\vdash ft_1 \cdots t_n \downarrow A[E]}{\vdash ft_1 \cdots t_n \uparrow B[E \cup \{(A, B)\}]} $$

**Fig. 2.** (Constraint-generating) type inference and type checking algorithm for algebraic terms.

**Proposition 2.2.**

1. If $t$ is an algebraic term, then there exists at most one $(E, A)$ such that $\vdash t \downarrow A[E]$.

2. If $t$ is an algebraic term or an object-level metavariable, then for all term $A$, there exists at most one $E$ such that $\vdash t \uparrow A[E]$.

**Remark 2.1.** The proposition above guarantees the existence of two algorithms InferType and CheckType that correspond to the type inference and the type checking respectively.

**Definition 2.5.** We say that a substitution $\sigma$ satisfies a set $E$ of equations, written $\sigma \models E$, if for all $(a, b) \in E, a\sigma \equiv b\sigma$.

**Definition 2.6.** We say that a substitution $\sigma'$ is a type-level extension of another substitution $\sigma$ if $M\sigma' = M\sigma$ for all $M \in \text{dom}(\sigma)$ and $\text{dom}(\sigma') - \text{dom}(\sigma) \subseteq \{t_M | M \in M_0 \cap \text{dom}(\sigma)\}$.

**Theorem 2.1.** Suppose that $\vdash t \uparrow T[E]$ (or $\vdash t \downarrow T[E]$). Let $\sigma$ be a substitution. Then we have:

1. $(\sigma \models E$ and $\forall M \in \text{Meta}(t), \Gamma \vdash M\sigma : t_M\sigma) \Rightarrow \Gamma \vdash t\sigma : T\sigma$.

2. $\Gamma \vdash t\sigma : V \Rightarrow$ there exists a type-level extension $\sigma'$ of $\sigma$ s.t. $V \equiv T\sigma', \sigma' \models E$ and $\forall M \in \text{Meta}(t), \Gamma \vdash M\sigma' : t_M\sigma'$).

*Proof.* By induction on the derivation of $\vdash t \downarrow T[E]$ (or $\vdash t \uparrow T[E]$)

* (Function applications)

1. Suppose that $\sigma \models \bigcup_{1 \le i \le n} E_i$ and $\forall M \in \text{Meta}(ft_1 \cdots t_n), \Gamma \vdash M\sigma : t_M\sigma$. We have, $\forall 1 \le i \le n, \sigma \models E_i$ and $\forall M \in \text{Meta}(t_i), \Gamma \vdash M\sigma : t_M\sigma$. By I.H., $\forall i \in \{1, \cdots, n\}, \Gamma \vdash t_i\sigma : A_i\sigma = A_i$ (the $A_i$'s and $U$ contain no metavariable since function symbols are declared in the global context). Hence, $\Gamma \vdash (ft_1 \cdots t_n)\sigma = f(t_1\sigma) \cdots (t_n\sigma) : (t_1\sigma/x_1, \cdots, t_n\sigma/x_n)U = ((t_1/x_1, \cdots, t_n/x_n)U)\sigma$.

2. Suppose that $\Gamma \vdash f(t_1\sigma) \cdots (t_n\sigma) : V$. We have $\forall i, \Gamma \vdash t_i\sigma : A_i$. Thus by I.H., we have, for all $i$, there exists a type-level extension $\sigma'_i$ of $\sigma$ s.t. $\sigma'_i \models E_i$ and $\forall M \in \text{Meta}(t_i), \Gamma \vdash M\sigma' : t_M\sigma'$. Let $\sigma'$ be the substitution defined by $\text{dom}(\sigma') = \bigcup_{1 \le i \le n} \text{dom}(\sigma'_i)$ and $M\sigma' = M\sigma'_i$. Note that, if an object-level metavariable $M$ occurs in the domains of $\sigma'_i$ and $\sigma'_j$, we have, by I.H., $\Gamma \vdash M\sigma'_i : t_M\sigma'_i$ and $\Gamma \vdash M\sigma'_j : t_M\sigma'_j$. $\sigma'_i$ (resp. $\sigma'_j$) is a type-level extension of $\sigma$, we have thus $M\sigma'_i = M\sigma = M\sigma'_j$. Hence, $t_M\sigma'_i \equiv t_M\sigma'_j$ by uniqueness of types. We choose thus the value of $t_M\sigma'$ to be either $t_M\sigma'_i$ or $t_M\sigma'_j$. By doing so, $\sigma' \models \bigcup_{1 \le i \le n} E_i$ and $\forall M \in \text{Meta}(ft_1 \cdots t_n), \Gamma \vdash M\sigma' : t_M\sigma'$. To finish, we have $V = (t_1\sigma/x_1, \cdots, t_n\sigma/x_n)U = ((t_1/x_1, \cdots, t_n/x_n)U)\sigma = ((t_1/x_1, \cdots, t_n/x_n)U)\sigma'$.

* (Object-level metavariables)

1. Suppose that $\sigma \models \{(t_M, T)\}$, i.e., $t_M\sigma \equiv T\sigma$ and $\Gamma \vdash M\sigma : t_M\sigma$. By the conversion rule, we have thus $\Gamma \vdash M\sigma : T\sigma$.

2. Suppose that $\Gamma \vdash M\sigma : V$. By defining $\sigma'$ as $N\sigma' = M\sigma$ if $N \neq t_M$ and $t_M\sigma' = V$, we have the required properties.

* (Type checking of function applications) Trivial.

□
### 2.3.3 Rewrite rules

We only consider algebraic rewrite rules in the algorithm proposed in the next section.

**Definition 2.7.** (Algebraic rewrite rules) An algebraic rewrite rule is a pair $(l, r)$ of terms, written as $l \to r$, such that:

1. $l$ is algebraic;

2. $r$ is either an object-level scavvariable or an algebraic term;

3. $Meta(r) \subseteq Meta(l)$;

Now we can define the rewrite relation induced by the rewrite system.

**Definition 2.8.** (Rewrites and rewrite steps)

* Let $l \to r$ be an algebraic rewrite rule and $\sigma$ be a substitution. Then $l\sigma \to r\sigma$ is called a rewrite and $l\sigma$ is called a redex.

* Let $C$ be a context and $l\sigma \to r\sigma$ be a rewrite. Then $C[l\sigma] \to C[r\sigma]$ is a rewrite step. This defines the rewrite relation $\to_R$ generated by the rewrite system $R$.

## 3 Subject reduction in $\lambda\Pi$-calculus modulo

We first give the notion of product compatibility.

**Definition 3.1.** (Product compatibility) We say the product compatibility property is satisfied if $\Pi x : A.B \equiv \Pi x : A'.B'$ implies $A \equiv A'$ and $B \equiv B'$.

Then we give a sufficient condition for the product compatibility.

**Proposition 3.1.** (Product compatibility from confluence) If $\to$ is confluent, then the product compatibility property holds.

Now we introduce the type preservation of rewrite rules, one of the main points we investigate in this work.

**Definition 3.2.** (Type preservation of rewrite rules) A rule $l \to r$ is type-preserving if for any well-formed context $\Gamma$, any substitution $\sigma$ and any term $T$, $\Gamma \vdash l\sigma : T$ implies $\Gamma \vdash r\sigma : T$.

In [4], F. Barbanera, M. Fernández, and H. Geuvers give the following theorem:

**Theorem 3.1.** (Subject reduction for $\to_\beta$) The subject reduction for $\to_\beta$, expressed below, is a consequence of the product compatibility.

$$SR_{\to_\beta} : \forall \Gamma, t_1, t_2, T, (\Gamma \vdash t_1 : T \text{ and } t_1 \to_\beta t_2) \Rightarrow \Gamma \vdash t_2 : T.$$

**Theorem 3.2.** (Subject reduction for $\to_R$) The subject reduction for $\to_R$, expressed below, is equivalent to the type preservation of all the rewrite rules in $R$.

$$SR_{\to_R} : \forall \Gamma, t_1, t_2, T, (\Gamma \vdash t_1 : T \text{ and } t_1 \to_R t_2) \Rightarrow \Gamma \vdash t_2 : T.$$

This result remains valid in Lambdapi. Since we assume always the confluence in Lambdapi, the subject reduction for $\to_R$ is equivalent to the type preservation of the rewrite system.
## 3.1 Type preservation of rewrite rules

In this section, we present an algorithm for checking type preservation of algebraic rewrite rules.

We first give an example to show the idea of the algorithm briefly.

**Example 3.1.** Consider the rule $l = tail\ n(cons\ x\ p\ v) \to v = r$ with $N: Type, s: N \Rightarrow N, A: Type, V: N \Rightarrow Type, cons: \Pi x: A. \Pi n: N.V\ n \Rightarrow V\ (s\ n)$, and $tail: \Pi n: N.V\ (s\ n) \Rightarrow V\ n$.

The idea is to retrieve some information about $\sigma$ from the typability of $l\sigma$ and then use this information to prove the typability of $r\sigma$. For example, to make tail ($n\sigma$) ($cons$ ($x\sigma$)($p\sigma$)($v\sigma$)) typable, we should ask the type of $n\sigma$ to be (convertible to) $N$.

We first infer the type of the LHS:

$\vdash tail\ n(cons\ x\ p\ v) \downarrow V\ n[\{(t_n, N), (t_p, N), (t_v, V\ p), (V\ (s\ p), V\ (s\ n))\}]$. We now check if the RHS has the same type $V\ n: \vdash v \uparrow V\ n[\{(t_v, V\ n)\}]$ (recall: $t_M$ represents the type of the object-level variable $M$).

By using the equation $(t_v, V\ p)$, we can transform the equation $(t_v, V\ n)$ to solve into the equation $(V\ p, V\ n)$. Since $V$ and $s$ are constants, it is possible to get the constraint $(p, n)$ from the constraint $(V\ (s\ p), V\ (s\ n))$, and the equation $(V\ p, V\ n)$ can be thus solved by the constraint $(p, n)$. This observation also shows that a refinement of constraints should be done before dealing with the equations to solve.

As the type inference and type checking algorithm is "constraint-generating", our main goal is to prove that the set $E$ of constraints generated by the LHS of a rule is "stronger" than the one generated by the RHS ($E_{to\_solve}$). More precisely, we want to prove that every substitution $\sigma$ satisfying $E$ satisfies $E_{to\_solve}$ as well. The problem is hard and might be undecidable. Here, we propose a partial solution using a completion procedure that gives a rewrite system $R'$ equivalent to $E'$, obtained from $E$ by replacing each variable $M$ with a fresh symbol $c_M$.

<table><caption>**Algorithm 1:** CheckSR</caption><thead><tr><th></th><th></th></tr></thead><tbody><tr><td>input</td><td>: an algebraic rule $l \to r$</td></tr><tr><td>output</td><td>: a boolean value $b$</td></tr><tr><td>1</td><td>res &larr; true</td></tr><tr><td>2</td><td>(U, E) &larr; InferType(l)</td></tr><tr><td>3</td><td>E<sub>to\_solve</sub> &larr; CheckType(U, r)</td></tr><tr><td>4</td><td>E' &larr; E&rho;</td></tr><tr><td colspan="2">/* &rho; replaces every variable M with a fresh (constant) symbol c<sub>M</sub> */</td></tr><tr><td>5</td><td>(E'<sub>fo</sub>, E'<sub>not\_fo</sub>) &larr; FO(E')</td></tr><tr><td colspan="2">/* split the equations into one first-order part and the rest */</td></tr><tr><td>6</td><td>R' &larr; Completion(E'<sub>fo</sub>)</td></tr><tr><td>7</td><td>E'<sub>to\_solve</sub> &larr; E<sub>to\_solve</sub>&rho;</td></tr><tr><td>8</td><td>for (t, u) &isin; E'<sub>to\_solve</sub> do</td></tr><tr><td>9</td><td>&nbsp;&nbsp;&nbsp;&nbsp;res &larr; res &and; (t &downarrow; R &cup; R' &cup; &beta; u &or; Eq<sub>constr</sub>(E'<sub>not\_fo</sub>, R', t, u))</td></tr><tr><td>10</td><td>end</td></tr><tr><td>11</td><td>return res</td></tr></tbody></table>

Here, InferType($l$) returns $(U, E)$ if and only if $\vdash l \downarrow U[E]$ and CheckType($U, r$) returns $E_{to\_solve}$ if and only if $\vdash r \uparrow U[E_{to\_solve}]$.

We now describe the completion procedure employed in the form of a rewrite system.
$$S \cup \{g \to d, l[g] \to r\} \hookrightarrow \begin{cases} S \cup \{g \to d, l[d] \to r\} & \text{if } l[d] > r \\ S \cup \{g \to d, r \to l[d]\} & \text{if } l[d] < r \\ S \cup \{g \to d\} & \text{if } l[d] = r \end{cases}$$

where $>$ is a total reduction order on terms

Note that only closed first-order term rewrite systems are considered here.

**Lemma 3.1.** The system above is terminating.

By considering the multiset ordering $>_{mul}$, the sum of the sizes of all the terms (LHS's and RHS's) strictly decreases after applying a rewrite step.

**Proposition 3.2.** Let $S$ be a normal term in the system above. Then $S$ has no critical pair.

*Proof.* First note that any critical pair between two "closed" rules $g \to d$ and $l \to r$ is of the form $(d, c[r])$ or $(c[d], r)$ where $c$ is a context. In both cases, one of the LHS's is a subterm of the other. Hence, if $S$ has a critical pair, then $S$ is not in normal form, which leads to a contradiction. $\square$

**Theorem 3.3.** Let $S$ be a rewrite system included in the reduction order $>$. Then the normal form $nf(S)$ of $S$ is a confluent and terminating rewrite system. Moreover, $\equiv_{nf(S)} = \equiv_S$.

*Proof.* By Proposition 3.2, the normal form $nf(S)$ of $S$ is locally confluent. It is not difficult to prove that it is also included in $>$, which implies its termination. By Newman's lemma, $nf(S)$ is confluent. To prove the equivalence of the systems, it suffices to prove that $S \hookrightarrow S' \Rightarrow \leftrightarrow_S^* = \leftrightarrow_{S'}^*$. $\square$

The completion procedure takes a set $E$ of equations as input, orients it following the reduction order $>$:

$$S = \{max_>(a, b), min_>(a, b) | (a, b) \in E, a \neq b\}$$

and returns the normal form of $S$.

A problem of modularity arises when we consider the union of the user-defined system, the beta-conversion, and the one generated by completion. To guarantee the conversion is decidable in the union, we want the latter to be confluent and terminating. In general, there is no guarantee that this property is verified. It might be interesting to restrict to some special cases. For instance, if the user-defined system is left-linear, confluent and there is no critical pair between the two systems, then the union is confluent. There are some works about the modularity of termination in first-order term rewriting, but it is still unknown whether these results can be generalized to higher-order cases.

Since the union might not be complete, we propose a simple function that strengthens the power of the algorithm using higher-order constraints.

**Algorithm 2: Eq<sub>constr</sub>**

**input**: a set $E$ of constraints, a rewrite system $R'$, two terms $t$ and $u$

**output**: a boolean value $b$

1. $b \leftarrow false$

2. **for** $(v, w) \in E$ **do**

3. $b \leftarrow b \lor (t \downarrow_{R \cup R' \cup \beta} v \land u \downarrow_{R \cup R'} w) \lor (t \downarrow_{R \cup R' \cup \beta} w \land u \downarrow_{R \cup R'} v)$

4. **end**

5. **return** $b$

We now give the main theorem of this section:

**Theorem 3.4.** If $CheckSR(l \to r)$ returns true, then the rule $l \to r$ is type-preserving.
**Algorithm 3: Unification**

input : a unification problem *P*
output: a substitution and a set of unsolved equations
1 **if** P.to_solve = [] **then**
2 &nbsp;&nbsp;&nbsp;**if** P.recheck = false **then**
3 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return (P.subst, P.unsolved)
4 **else**
5 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.to_solve &larr; P.unsolved
6 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.unsolved &larr; []
7 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.recheck &larr; false
8 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return Unification(P)
9 **else**
10 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(t, u) &larr; P.to_solve.pop()
11 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Unification_aux((t, u), P)

We now present an algorithm for unification modulo rewriting:

**Algorithm 4: Unification_aux**

input : an equation (t, u) on terms and a unification problem *P*
output: a substitution and a set of unsolved equations
1 t &larr; t &darr;
2 u &larr; u &darr;
3 **if** t = u **then**
4 &nbsp;&nbsp;&nbsp;return Unification(P)
5 **else if** t = gt₁...tₙ and u = hu₁...h uₘ with g, h two symbols **then**
6 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** g and h are distinct constants **then**
7 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;raise Unsolvable
8 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else if** g = h and g is constant **then**
9 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for** i = 1 to n **do**
10 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.to_solve.insert((tᵢ, uᵢ))
11 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**end**
12 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return Unification(P)
13 **else**
14 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.unsolved.insert((t, u))
15 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return Unification(P)
16 **else if** (t, u) = (x, s) or (s, x) with x &isin; V - Var(s) **then**
17 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P &larr; P[x &larr; s] /* replace all occurrences of x in P with s */
18 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.subst.insert((x, s))
19 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.recheck &larr; true
20 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return Unification(P)
21 **else**
22 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.unsolved.insert((t, u))
23 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return Unification(P)

**Proposition 4.1.**

* If the call `Unification_aux((t, u), P)` raises the exception `Unsolvable`, then `t` and `u` are not unifiable.

* If in the call `Unification_aux((t, u), P)` we make the call `Unification(P')`, then `{(t, u)} &cup; eq(P)` and `eq(P')` are equivalent.

* If in the call `Unification(P)` we make the call `Unification(P')` then `eq(P)` and `eq(P')` are equivalent.
• If in the call `Unification(P)` we make the call `Unification_aux((t, u), P')`, then `eq(P)` and `((t, u)) ∪ eq(P')` are equivalent.

• If the call `Unification(P)` returns $(\rho, Q)$ without any other call, then `eq(P)` and the union of $\rho$ (a substitution $\{x_1 \mapsto t_1, \dots, x_n \mapsto t_n\}$ is identified with the set $\{(x_1, t_1), \dots, (x_n, t_n)\}$ and $eq(Q)$ are equivalent.

**Theorem 4.1.**

• Suppose that `Unification(P)` raises an error. Then `eq(P)` is not unifiable.

• Suppose that `Unification(P)` returns $(\rho, Q)$. Then `eq(P)` is equivalent to the union of $\rho$ and `eq(Q)`.

In a syntactic unification, unifying two terms of the form $ft_1 \cdots t_n$ and $fu_1 \cdots u_n$ is equivalent to unifying the pairs $(t_1, u_1), \cdots, (t_n, u_n)$. However, this is no longer true in our setting with congruence. This observation gives rise to the study of the injectivity of symbols, given in detail in the next section.

The study of injectivity can be useful for checking the subject reduction property. For example, we can encode in Lambdapi/Dedukti [1] some logical systems using a type $T$ for representing propositions and a function symbol $\epsilon : T \Rightarrow Type$ for interpreting the Curry-Howard correspondence. The injectivity of $\epsilon$ is sometimes needed when checking the subject reduction for certain rules.

**4.2 Injectivity of function symbols**

Assume that the symbols of $R$ are defined in a certain order, i.e., there exists an order $>_{symb}$ on the set $S$ of symbols such that $f >_{symb} g$ iff $f$ is defined after $g$ (the rules defining $g$ do not contain any symbol $f$ s.t. $f >_{symb} g$).

Alternatively, we can reformulate this by saying the dependency graph between symbols is a DAG:

**Definition 4.3.** We say that $f$ depends on $g$ if there exists a rule $fl \to r$ such that $g$ appears in $l$ or $r$. The dependency graph between symbols is a directed graph $(V, E)$ defined by $V = S$ and $E = \{(f, g) | f \text{ depends on } g\}$.

Moreover, we assume that each symbol has a fixed arity.

Consider the following example:

**Example 4.1.** Let $o$ and $s$ be two constant symbols.

The following rules define the symbol `id`:

$$R_1 : id \ o \to o$$

$$R_2 : id (s \ x) \to s (id \ x)$$

Since the rewrite system is assumed to be terminating and confluent, the relation $> := (\triangleright \cup \to)^+$ is well-defined and well-founded. The relation $>_{id}$ defined by $(t, u) >_{id} (t', u') \Leftrightarrow (id \ t \geq id \ t'$ and $id \ u > id \ u'$) or $(id \ t > id \ t'$ and $id \ u \geq id \ u')$ is also well-founded.

We now prove $id \ t \equiv id \ u \Rightarrow t \equiv u$ by induction on $(t, u)$ using the relation $>_{id}$.

• If $id \ t$ and $id \ u$ are in normal form, then $id \ t = id \ u$ by confluence and thus $t = u$.

• If $id \ t$ is in normal form and there exists $v$ s.t. $id \ u \to v$. We distinguish two cases:

1. $u$ is in normal form: we have $id \ u \to_{R_1} v$ or $id \ u \to_{R_2} v$.

If $id \ u \to_{R_1} v$, then $u = v = o$. We have thus $id \ t = id \ t \downarrow = id \ u \downarrow = o$, which is impossible.

If $id \ u \to_{R_2} v$, then there exists $w$ such that $u = s \ w$ and $v = s$ ($id \ w$). Since $s$ is a constant, the normal form of $v$ is also headed by $s$, which leads to a contradiction since $v \downarrow = id \ u \downarrow = id \ t \downarrow = id \ t$.
2. there exists $u'$ such that $u \to u'$. We have $(t, u) >_{id} (t, u')$ and $id u' \equiv id u \equiv id t$. Thus by I.H., we have $u' \equiv t$, which gives $u \equiv t$.

* If *id u* is in normal form and there exists *w* s.t. *id t* → *w*, then we proceed as in the previous case.

* If *id t* and *id u* are not in normal form, then we distinguish two cases:

1. If one of the terms *t* and *u* is not in normal form, then we can conclude by simply applying the I.H..

2. If *t* and *u* are in normal form, then there exist *i*, *j* ∈ {1, 2} and two terms *v* and *w* s.t. *id t* →$_{R_i}$ *v* and *id u* →$_{R_j}$ *w*.

If $(i, j) = (1, 1)$, then it is clear that $t = u = o$.

If $(i, j) = (1, 2)$ (resp. $(2, 1)$), then it is contradictory since *v* is headed by the constant *o* (resp. *s*) while *w* is headed by the constant *s* (resp. *o*).

If $(i, j) = (2, 2)$, then there exist $t'$ and $u'$ such that $t = s t'$, $v = s (id t')$, $u = s u'$ and $w = s (id u')$. We have $v \equiv id t \equiv id u \equiv w$, which implies $id t' \equiv id u'$ since *s* is constant.

We have $(t, u) >_{id} (t', u')$ since $id t \to s (id t') \triangleright id t$ and $id u > id u'$ for the same reason. Thus, by I.H., $t' \equiv u'$, which gives $t \equiv u$.

Intuitively, we want to design an algorithm that checks the injectivity of a given symbol "by induction" following the structure of the proof above. The second point in the proof by induction above gives rise to a function (*CheckSingleRule*) that checks if the structure of each rule verifies certain properties while the fourth point leads to a function (*CheckTwoRules*) that compares the structure of each rule with another (and itself).

**Definition 4.4.** Let $n$ be the arity of $f$. We say that $f$ is *I*-injective (modulo) if

$$ (ft_1 \cdots t_n \equiv fu_1 \cdots u_n \wedge \forall i \in I, t_i \equiv u_i) \Rightarrow \forall i \notin I, t_i \equiv u_i. $$

In the following, we propose an algorithm for checking *I*-injectivity.

<table><caption>**Algorithm 5: CheckInjectivity**</caption><thead><tr><th></th><th>input</th><th>: f, I</th></tr></thead><tbody><tr><td>1</td><td>res ← true</td><td></td></tr><tr><td>2</td><td>for fl → r ∈ R do</td><td></td></tr><tr><td>3</td><td>res ← res ∧ CheckSingleRule(f, I, fl → r)</td><td></td></tr><tr><td>4</td><td>end</td><td></td></tr><tr><td>5</td><td>for fl → r ∈ R do</td><td></td></tr><tr><td>6</td><td>for fg → d ∈ R do</td><td></td></tr><tr><td>7</td><td>res ← res ∧ CheckTwoRules(f, I, fl → r, fg → d)</td><td></td></tr><tr><td>8</td><td>end</td><td></td></tr><tr><td>9</td><td>end</td><td></td></tr><tr><td>10</td><td>return res</td><td></td></tr></tbody></table>

Note that, if $fl \to r$ is the same as $fg \to d$, the metavariables in the latter are renamed before calling to *CheckTwoRules*.

The call *CheckSingleRule*(*f*, *I*, *fl* → *r*) corresponds to the case where exactly one of the terms *ft* and *fu* is in normal form, and the other can be reduced at the top-level using the rule *fl* → *r*. The idea is quite straightforward: we attempt to use the conditions *ft* ≡ *fu* and *t*ᵢ ≡ *u*ᵢ(*i* ∈ *I*) to solve the equations *t*ᵢ ≡ *u*ᵢ(*i* ∉ *I*). The most delicate part is that we proceed in an abstract level: we consider rules and metavariables instead of actual terms. Thus, it is appropriate to adapt the approach "Unification as refinement of constraints" taken in *checkSR* to this case, by using a
hypothetical unification procedure, instead of the one presented previously.

<table><caption>**Algorithm 6: CheckSingleRule**</caption><tr><td>input</td><td>: f, I and a rule fl &rarr; r</td></tr><tr><td>output</td><td>: a boolean value b</td></tr><tr><td>1</td><td>if &exist; i &isin; I, l<sub>i</sub> = r then</td></tr><tr><td>2</td><td>&nbsp;&nbsp;&nbsp;&nbsp;return true</td></tr><tr><td>3</td><td>else if r is of the form gl' with g &ne; f then</td></tr><tr><td>4</td><td>&nbsp;&nbsp;&nbsp;&nbsp;if NoErasing_rec(g) then</td></tr><tr><td>5</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return true</td></tr><tr><td>6</td><td>&nbsp;&nbsp;&nbsp;&nbsp;else</td></tr><tr><td>7</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return false</td></tr><tr><td>8</td><td>else</td></tr><tr><td>9</td><td>&nbsp;&nbsp;&nbsp;&nbsp;P &larr; {(fx<sub>1</sub> &middot;&middot;&middot; x<sub>n</sub>, r)} &cup; {(x<sub>i</sub>, l<sub>i</sub>) | i &isin; I}</td><td>* x<sub>i</sub> are fresh variables *</td></tr><tr><td>10</td><td>Q &larr; {(x<sub>i</sub>, l<sub>i</sub>) | i &notin; I}</td><td></td></tr><tr><td>11</td><td>return InferFromConstraints(f, I, P, Q)</td><td></td></tr></table>

As observed in Example 4.1, if we can prove that the normal form of a term cannot be headed by *f* after applying the rule *fl* → *r*, then the case where exactly one of the terms *ft* and *fu* is in normal form and the other can be reduced at the top-level using the rule *fl* → *r* can be eliminated. The following function *NoErasing_rec* gives one sufficient condition for having this property.

**Proposition 4.2.** If *NoErasing_rec*(*f*) returns *true*, then the normal form of a term headed by *f* is headed by *f* or a symbol defined previously.

*Proof.* By induction on $>_{symb}$. Trivial. $\square$

<table><caption>**Algorithm 7: NoErasing_rec**</caption><tr><td>input</td><td>: a symbol f</td></tr><tr><td>output</td><td>: a boolean value b</td></tr><tr><td>1</td><td>if f has erasing rules, i.e., rules of the form fl &rarr; x then</td></tr><tr><td>2</td><td>&nbsp;&nbsp;&nbsp;&nbsp;return false</td></tr><tr><td>3</td><td>else</td></tr><tr><td>4</td><td>&nbsp;&nbsp;&nbsp;&nbsp;res &larr; true</td></tr><tr><td>5</td><td>&nbsp;&nbsp;&nbsp;&nbsp;for fl &rarr; gl' &isin; Rules with f &ne; g do</td></tr><tr><td>6</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;res &larr; res &and; NoErasing_rec(g)</td></tr><tr><td>7</td><td>&nbsp;&nbsp;&nbsp;&nbsp;end</td></tr><tr><td>8</td><td>&nbsp;&nbsp;&nbsp;&nbsp;return res</td></tr></table>

The call *CheckTwoRules*(*f*, *I*, *fl* → *r*, *fg* → *d*) corresponds to the case where *ft* (resp. *fu*) can be reduced at the top-level using the rule *fl* → *r* (resp. *fg* → *d*). The idea is almost the same as that of *CheckSingleRule*.

<table><caption>**Algorithm 8: CheckTwoRules**</caption><tr><td>input</td><td>: f, I, two rules fl &rarr; r and fg &rarr; d</td></tr><tr><td>output</td><td>: a boolean value b</td></tr><tr><td>1</td><td>P &larr; {(r, d)} &cup; {(l<sub>i</sub>, g<sub>i</sub>) | i &isin; I}</td></tr><tr><td>2</td><td>Q &larr; {(l<sub>i</sub>, g<sub>i</sub>) | i &notin; I}</td></tr><tr><td>3</td><td>return InferFromConstraints(f, I, P, Q)</td></tr></table>
**Algorithm 9:** InferFromConstraints

input : *f*, *I*, two sets of constraints *P* and *Q*
output: a boolean value *b*

1 try:
2 &nbsp;&nbsp;P ← {subst = {}, unsolved = {}, to_solve = *P*, recheck = false}
3 &nbsp;&nbsp;(*ρ*, *constr*) ← Hypo_Unification(*f*, *I*, *P*)
4 &nbsp;&nbsp;*Q'* ← *Qρ*[*x* ← *c*<sub>*x*</sub>]                 /* *c*<sub>*x*</sub> are fresh variables */
5 &nbsp;&nbsp;res ← true
6 &nbsp;&nbsp;for (*t*, *u*) ∈ *Q'* do
7 &nbsp;&nbsp;&nbsp;&nbsp;res ← res ∧ (*t* ≡<sub>*R∪constr*[*x*←*c*<sub>*x*</sub>] *u*</sub>)
8 &nbsp;&nbsp;end
9 &nbsp;&nbsp;return res
10 catch Unsolvable :
11 &nbsp;&nbsp;return true
12 end

Intuitively, InferFromConstraints(*f*, *I*, *P*, *Q*) attempts to solve the constraints *Q* by using the constraints generated from Hypo_Unification(*f*, *I*, *P*).

We now describe a first-order hypothetical unification (modulo rewriting) algorithm.

**Algorithm 10:** Hypo_Unification

input : *f*, *I* and a unification problem *P*
output: a substitution and a set of unsolved equations

1 **if** *P.to_solve* = [] **then**
2 &nbsp;&nbsp;**if** *P.recheck* = false **then**
3 &nbsp;&nbsp;&nbsp;&nbsp;return *unmarked*(*P.subst*, *P.unsolved*)
4 &nbsp;&nbsp;**else**
5 &nbsp;&nbsp;&nbsp;&nbsp;*P.to_solve* ← *P.unsolved*
6 &nbsp;&nbsp;&nbsp;&nbsp;*P.unsolved* ← []
7 &nbsp;&nbsp;&nbsp;&nbsp;*P.recheck* ← false
8 &nbsp;&nbsp;&nbsp;&nbsp;return *Hypo_Unification*(*f*, *I*, *P*)
9 **else**
10 &nbsp;&nbsp;(*t*, *u*) ← *P.to_solve*.pop()
11 &nbsp;&nbsp;*Hypo_Unification_aux*(*f*, *I*, (*t*, *u*), *P*)
<table><caption>**Algorithm 11:** Hypo_Unification_aux</caption>
  <thead>
    <tr>
      <th>line</th>
      <th>expression</th>
      <th>meaning</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>1</td>
      <td>t &larr; t &downarrow;</td>
      <td></td>
    </tr>
    <tr>
      <td>2</td>
      <td>u &larr; u &downarrow;</td>
      <td></td>
    </tr>
    <tr>
      <td>3</td>
      <td>if t = u then</td>
      <td></td>
    </tr>
    <tr>
      <td>4</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;return Hypo_Unification(f, I, P)</td>
      <td></td>
    </tr>
    <tr>
      <td>5</td>
      <td>else if t = gt<sub>1</sub> &middot;&middot;&middot; t<sub>n</sub> and u = hu<sub>1</sub> &middot;&middot;&middot; u<sub>m</sub> with g, h two symbols then</td>
      <td></td>
    </tr>
    <tr>
      <td>6</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;if g = f<sup>#</sup> or h = f<sup>#</sup> then</td>
      <td></td>
    </tr>
    <tr>
      <td>7</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.unsolved.insert((t, u))</td>
      <td></td>
    </tr>
    <tr>
      <td>8</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return Hypo_Unification(f, I, P)</td>
      <td></td>
    </tr>
    <tr>
      <td>9</td>
      <td>else if g &ne; h then</td>
      <td></td>
    </tr>
    <tr>
      <td>10</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if g and h are constants then</td>
      <td></td>
    </tr>
    <tr>
      <td>11</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;raise Unsolvable</td>
      <td></td>
    </tr>
    <tr>
      <td>12</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;else</td>
      <td></td>
    </tr>
    <tr>
      <td>13</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.unsolved.insert((t, u))</td>
      <td></td>
    </tr>
    <tr>
      <td>14</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return Hypo_Unification(f, I, P)</td>
      <td></td>
    </tr>
    <tr>
      <td>15</td>
      <td>else</td>
      <td></td>
    </tr>
    <tr>
      <td>16</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;J &larr; {i | t<sub>i</sub> &equiv; u<sub>i</sub>}</td>
      <td></td>
    </tr>
    <tr>
      <td>17</td>
      <td>if (g = f and I &sub; J) or CheckInjectivity(g, J) then</td>
      <td></td>
    </tr>
    <tr>
      <td>18</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;for i &notin; J do</td>
      <td></td>
    </tr>
    <tr>
      <td>19</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P.to_solve.insert((t<sub>i</sub>, u<sub>i</sub>))</td>
      <td></td>
    </tr>
    <tr>
      <td>20</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;end</td>
      <td></td>
    </tr>
    <tr>
      <td>21</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;return Hypo_Unification(f, I, P)</td>
      <td></td>
    </tr>
    <tr>
      <td>22</td>
      <td>else</td>
      <td></td>
    </tr>
    <tr>
      <td>23</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;P.unsolved.insert((t, u))</td>
      <td></td>
    </tr>
    <tr>
      <td>24</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;return Hypo_Unification(f, I, P)</td>
      <td></td>
    </tr>
    <tr>
      <td>25</td>
      <td>else if (t, u) = (x, s) or (s, x) with x &isin; V &ndash; Var(s) then</td>
      <td></td>
    </tr>
    <tr>
      <td>26</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;P &larr; P[x &larr; s<sub>f<sup>#</sup></sub>]</td>
      <td>/* replace all occurrences of x in P with s<sub>f<sup>#</sup></sub> */</td>
    </tr>
    <tr>
      <td>27</td>
      <td>P.subst.insert((x, s))</td>
      <td></td>
    </tr>
    <tr>
      <td>28</td>
      <td>P.recheck &larr; true</td>
      <td></td>
    </tr>
    <tr>
      <td>29</td>
      <td>return Hypo_Unification(f, I, P)</td>
      <td></td>
    </tr>
    <tr>
      <td>30</td>
      <td>else</td>
      <td></td>
    </tr>
    <tr>
      <td>31</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;P.unsolved.insert((t, u))</td>
      <td></td>
    </tr>
    <tr>
      <td>32</td>
      <td>&nbsp;&nbsp;&nbsp;&nbsp;return Hypo_Unification(f, I, P)</td>
      <td></td>
    </tr>
  </tbody>
</table>

Here, $f^#$ is a special symbol introduced to guarantee that the induction hypothesis in our proof by induction is applied "correctly". It is considered exactly the same as $f$ except when unifying a term headed by $f^#$ with another term. When we consider a $f$ which is not marked with #, we use $f^o$ to avoid the confusion. We denote by $s_{f^#}$ the term obtained from $s$ by replacing all occurrences of $f$ with $f^#$. If we admit that $CheckInjectivity(f, I) = true \Rightarrow f$ is I-injective, then $Hypo_Unification$ implements the first-order unification (modulo rewriting) under the hypothesis that $f$ is I-injective (on some set of terms).

The following theorem gives a sufficient condition for I-injectivity.

**Theorem 4.2.** Let $f$ be a symbol and $I \subseteq \{1, \dots, \text{arity}(f)\}$. If $\text{CheckInjectivity}(f, I)$ returns true, then $f$ is I-injective.

*Proof.* We first define a relation $S$ on the set $E = \{(f, I) \mid \text{CheckInjectivity}(f, I) \text{ terminates}\}$ such that $(f, I) S (g, J)$ if the call $\text{CheckInjectivity}(g, J)$ appears in the recursion tree of the call $\text{CheckInjectivity}(f, I)$. $S$ is well-founded since for all $(f, I) \in E$, $\text{CheckInjectivity}(f, I)$ terminates.

We prove $H_0(f, I) : \text{CheckInjectivity}(f, I)$ returns true $\Rightarrow f$ is I-injective by induction on $E$ using
the well-founded relation S.

Now, fix $f$ and $I$ and suppose that $H_0(g, J)$ holds for all $(f, I) S (g, J)$.

Since the rewrite system $R$ is assumed to be terminating and confluent, the relation $>:= (\triangleright \cup \to)^+$ is well-founded. Let $>_{prod\_f}$ be the well-founded relation defined by $(t, u) >_{prod\_f} (t', u') \Leftrightarrow (ft > ft'$ and $fu \ge fu'$) or $(ft \ge ft'$ and $fu > fu'$). Note that $t, u, t'$, and $u'$ are $n$-tuples of terms, where $n = \text{arity}(f)$. In the following, we write $t \to t'$ if there exists $i$ s.t. $t_i \to t'_i$ and $t_j = t'_j \forall j \neq i$.

Suppose that $\text{CheckInjectivity}(f, I)$ returns true.

We now prove $H_1((t, u)) : (ft \equiv fu \wedge \forall i \in I, t_i \equiv u_i) \Rightarrow \forall i \notin I, t_i \equiv u_i$ by induction on $(t, u)$ using $>_{prod\_f}$.

* Suppose that $ft$ and $fu$ are in normal form. Then $ft = ft \downarrow = fu \downarrow = fu$ and $\forall i, t_i = u_i$.

* Suppose that $ft$ is in normal form and that there exists $v$ s.t. $fu \to v$. We distinguish two cases:

1. $u_i$ are all in normal form. There exist thus a rule $fl \to r$ and a substitution $\sigma$ such that $fu = fl\sigma$ and $v = r\sigma$. Since $\text{CheckSingleRule}(f, I, fl \to r)$ returns true, we can distinguish three cases:

- there exists $i \in I$ s.t. $l_i = r$. In this case $v = r\sigma = l_i\sigma = u_i \equiv t_i$, but we also have $v \equiv fu \equiv ft$, which leads to a contradiction since $ft$ and $t_i$ are both in normal form.

- $r$ is of the form $gl'$ with $g \neq f$ and $\text{NoErasing\_rec}(g)$ returns true. This case is impossible since $v = r\sigma = gl'\sigma$ and by Proposition 1.2., $v \downarrow$ cannot be headed by $f$.

- $\text{InferFromConstraints}(f, I, P, Q)$ returns true where $P = \{(fx_1 \cdots x_n, r)\} \cup \{(x_i, l_i) \mid i \in I\}$ and $Q = \{(x_i, l_i) \mid i \notin I\}$. Let $\sigma'$ be the substitution that extends $\sigma$ with $x_i\sigma' = t_i$.

Consider the call to $\text{Hypo\_Unification}$ in $\text{InferFromConstraints}(f, I, P, Q)$ and let $\text{Hypo\_Unification}(f, I, P_0), \cdots, \text{Hypo\_Unification}(f, I, P_k)$ be the sequence of the recursive calls to $\text{Hypo\_Unification}$ in this call (in particular, $\text{eq}(P_0) = P$).

We now prove $H_2(i) : \forall (a, b) \in \text{eq}(P_i), a\sigma' \equiv b\sigma'$ and

$H_3(i) : \forall (a, b) \in \text{eq}(P_i), \forall f^o t' \leq a, \forall f^o u' \leq b, (t, u) >_{prod\_f} (t'\sigma' \downarrow, u'\sigma' \downarrow)$ by induction on $i$ ($f^o$ denotes the unmarked symbol $f$).

$H_2(0)$ holds since $r\sigma' = r\sigma = v \equiv fu \equiv ft = (fx_1 \cdots x_n)\sigma'$ and for all $i \in I$, $l_i\sigma' = l_i\sigma = u_i \equiv t_i = x_i\sigma'$.

Let $(a, b) \in \text{eq}(P_0) = P$. If $(a, b) = (fx_1 \cdots x_n, r)$, then for all $f^o t' \leq a, f^o u' \leq b, f^o t'\sigma' \leq (fx_1 \cdots x_n)\sigma' = ft$ and $f^o u'\sigma' \leq r\sigma' = v \leftarrow fu$ which proves $(t, u) >_{prod\_f} (t'\sigma' \downarrow, u'\sigma' \downarrow)$ since $fc \geq f(c \downarrow)$ for all $c$. Thus $H_3(0)$ holds.

Now suppose that $H_2(i)$ and $H_3(i)$ hold and prove that $H_2(i+1)$ and $H_3(i+1)$ hold. Note that we only need to check these properties for the equations inserted into $P_i$. The only non-trivial inductive steps are (consider the equation treated in the call to $\text{Hypo\_Unification\_aux}$ between the calls $\text{Hypo\_Unification}(f, I, P_i)$ and $\text{Hypo\_Unification}(f, I, P_{i+1}))$:

(a) ($f^o t'_1 \cdots t'_n, f^o u'_1 \cdots u'_n$) and $I \subseteq J$ where $J = \{j \mid t'_j \equiv u'_j\}$ (case 1 in the line 17):
(H_2): By I.H. ($H_3$), $(t, u) >_{prod\_f} (t'\sigma' \downarrow, u'\sigma' \downarrow)$. By I.H. ($H_2$), $f^o(t'\sigma' \downarrow) \equiv f^o t'\sigma' \equiv f^o u'\sigma' \equiv f^o(u'\sigma' \downarrow)$ and thus by I.H. ($H_1$), $t'_j\sigma' \equiv t'_j\sigma' \downarrow \equiv u'_j\sigma' \downarrow \equiv u'_j\sigma' \forall j \notin I \subseteq J$.

(H_3): Trivial.

(b) ($gt'_1 \cdots t'_m, gu'_1 \cdots u'_m$) such that $g \neq f$ and that $\text{CheckInjectivity}(g, J)$ returns true where $J = \{j \mid t'_j \equiv u'_j\}$ (case 2 in the line 17):

(H_2): By I.H. ($H_2$), $g(t'_1\sigma') \cdots (t'_m\sigma') \equiv g(u'_1\sigma') \cdots (u'_m\sigma')$ and by I.H. ($H_0$), $g$ is $J$-injective. Thus $t'_j\sigma' \equiv u'_j\sigma' \forall j \notin J$.

(H_3): Trivial.
(c) $(x, s)$ where $x \in V$ (line 25):

(H2): By I.H. (H2), $x\sigma' \equiv s\sigma'$ (we have even $s\sigma' \downarrow = x\sigma'$ since there exists $i$ s.t. $x\sigma' \triangleleft t_i$ (or $u_i$) which is in normal form). For all $(a, b) \in \text{eq}(P_{i+1})$, there exists $(c, d) \in \text{eq}(P_i)$ such that $a = c[x \leftarrow s]$ and $b = d[x \leftarrow s]$. We have thus $a\sigma' = c[x \leftarrow s]\sigma' = c\sigma'[x\sigma' \leftarrow s\sigma'] \equiv c\sigma'$ and $b\sigma' \equiv d\sigma'$. Note that the notation $c\sigma'[x\sigma' \leftarrow s\sigma']$ here is not standard and it simply denotes the substitution of all subterms $x\sigma'$ corresponding to an occurrence of $x$ in $c$ with $s\sigma'$.

(H3): Let $(a, b) \in \text{eq}(P_{i+1})$ and $f^o t'$ (resp. $f^o u'$) be a subterm of $a$ (resp. $b$). Since the substitution $[x \leftarrow s_{f^o}]$ does not introduce any occurrence of $f^o$ (unmarked $f$) in $P_{i+1}$, there exist $(c, d) \in \text{eq}(P_i)$, $f^o t'' \trianglelefteq c$ and $f^o u'' \trianglelefteq d$ such that $f^o t' = f^o t''[x \leftarrow s]$ and $f^o u' = f^o u''[x \leftarrow s]$. We have thus $t'\sigma' \downarrow = t''\sigma'[x\sigma' \leftarrow s\sigma'] \downarrow = t''\sigma' \downarrow$ and $u'\sigma' \downarrow = u''\sigma' \downarrow$ since $x\sigma' \equiv s\sigma'$ by I.H. (H2).

By I.H. (H3), we have $(t, u) >_{\text{prod\_f}} (t''\sigma' \downarrow, u''\sigma' \downarrow) = (t'\sigma' \downarrow, u'\sigma' \downarrow)$.

It is clear that $\forall(x, s) \in P_i$.subst, $x\sigma' \equiv s\sigma'$. By (H2), we have:

- If Hypo_Unification(f, I, $P_0$) raises the exception *Unsolvable*, then there does not exist a substitution $\rho$ s.t. $\forall (a, b) \in P_0, a\rho \equiv b\rho$, which is impossible, since $\sigma'$ verifies this property.

- If Hypo_Unification(f, I, $P_0$) returns $(\rho, \text{constr})$, then $\forall (x, x\rho) \in \rho, x\sigma' \equiv x\rho\sigma'$ and $\forall (a, b) \in \text{constr}, a\sigma' = b\sigma'(*)$. By induction, we have further $a\sigma' \equiv a\rho\sigma'$ for all term $a$. In this case, since InferFromConstrs(f, I, P, Q) returns true, we have, for all $(c, d) \in Q, c\rho[x \leftarrow c_x] \equiv_{R \cup \text{constr}[x \leftarrow c_x]} d\rho[x \leftarrow c_x]$. Thus, by replacing $c_x$ with $x\sigma'$, $c\rho\sigma' \equiv_{R \cup \text{constr}\sigma'} d\rho\sigma'$ and $c\rho\sigma' \equiv d\rho\sigma'$ by $(*)$. Hence, $c\sigma' \equiv d\sigma'$ for all $(c, d) \in Q$.

2. there exists $v = fu'$ with $u \to u'$. We have $(t, u) >_{\text{prod\_f}} (t, u')$ and $\forall i \in I \ u'_i \equiv u_i \equiv t_i$. By I.H., $\forall i \notin I \ t_i \equiv u'_i \equiv u_i$.

* there exist $v$ and $w$ such that $ft \to v$ and $fu \to w$. We assume that $t_i$ and $u_i$ are all in normal form (if not, then the assertion can be proved by simply applying the I.H. (H1)). There exist thus two rules $fl \to r, fg \to d$ and a substitution $\sigma$ s.t. $ft = fl\sigma, v = r\sigma, fu = fg\sigma$ and $w = d\sigma$ (we can assume $\text{Var}(l) \cap \text{Var}(g) = \emptyset$ by renaming). By hypothesis, CheckTwoRules(f, I, $fl \to r, fg \to d$) returns true, which means that InferFromConstraints(f, I, P, Q) returns true where $P = \{(r, d) \cup \{(l_i, g_i) \mid i \in I\}\}$ and $Q = \{(l_i, g_i) \mid i \notin I\}$.

We can proceed as in the first point in the previous case by replacing $\sigma'$ with $\sigma$, $P$ and $Q$ with their counterparts here.

□

**Example 4.2.** Let $s$ and $o$ be two constant symbols.

$$R_1: f \circ y \to y$$

$$R_2: f(s \circ x) \to s(f \circ x y)$$

We can prove that $f$ is $\{1\}$-injective by applying the algorithm above:

* In the call `CheckSingleRule(f, \{1\}, R_1)`, the branch chosen is that of the line 8. Thus we first make a call to `Hypo_Unification` to unify the equations $(fx_1x_2, y)$ and $(x_1, o)$. The sequence of unification problems considered in the recursive calls to `Hypo_Unification` is presented below:
<figure><img src="image_3.png" /></figure>

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

We now apply the substitution obtained to the equation $(x_2, y)$ to solve and the equation obtained is an equality. Hence, `CheckSingleRule(f, {1}, R_1)` returns true.

* In the call `CheckSingleRule(f, {1}, R_2)`, the branch chosen is that of the line 3. Since *s* is constant, `NoErasing_rec(s)` returns true. Hence, `CheckSingleRule(f, {1}, R_2)` returns true.

* In the call `CheckTwoRules(f, {1}, R_1, R_1)`, we make the call `InferFromConstraints(f, {1}, P, Q)` with $P = \{(y, y'), (o, o)\}$ and $Q = \{(y, y')\}$. The call `Hypo_Unification(f, {1}, P)` returns $(\{y \mapsto y'\}, \{\})$ and the application of the substitution to *Q* produces an equality. Hence, `CheckTwoRules(f, {1}, R_1, R_1)` returns true.

* In the call `CheckTwoRules(f, {1}, R_2, R_2)`, we make the call `InferFromConstraints(f, {1}, P, Q)` with $P = \{(s (f x y), s (f x' y'))$, $(s x, s x')\}$ and $Q = \{(y, y')\}$. The call `Hypo_Unification(f, {1}, P)` returns $(\{x \mapsto x', y \mapsto y'\}, \{\})$.

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

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

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

The application of the substitution obtained to *Q* produces an equality. Hence `CheckTwoRules(f, {1}, R_2, R_2)` returns true.

* In the call `CheckTwoRules(f, {1}, R_1, R_2)`, we make the call `InferFromConstraints(f, {1}, P, Q)` with $P = \{(y, s (f x y'))$, $(o, s x)\}$ and $Q = \{(y, y')\}$. Within this call, the call `Hypo_Unification(P)` raises the error `Unsolvable` since *s* and *o* are both constant. Thus `CheckTwoRules(f, {1}, R_1, R_2)` returns true.

Thus, `CheckInjectivity(f, {1})` returns true.

However, the algorithm does not allow us to prove that *f* is {2}-injective. In fact, in the call `CheckTwoRules(f, {2}, R_1, R_2)`, we make the call `InferFromConstraints(f, {2}, P, Q)` with $P = \{(y, y'), (y, s (f x y'))\}$ and $Q = \{(o, s x)\}$. The call `Hypo_Unification(P, Q)` returns $(\{y \mapsto y'\}, \{(y', s (f x y'))\})$, but we do not have $o \equiv_{R \cup (c_y, s(f_x c_y))} sc_x$
**Remark 4.1.** The algorithm might not terminate in some cases: when we call *CheckInjectivity*(*f*, *I*), there might be a call *CheckInjectivity*(*f*, *J*) and when we call *CheckInjectivity*(*f*, *J*), there might be a call *CheckInjectivity*(*f*, *I*) with *I* ⊈ *J* and *J* ⊈ *I*. A possible solution is to pass as argument a list of pairs (*f*, *J*) that should be avoided when making a recursive call to *CheckInjectivity*. For example, when calling *CheckInjectivity*(*f*, *J*), we pass an extra argument (*f*, *I*) to make sure that the call *CheckInjectivity*(*f*, *I*) will not be made in this call.

This approach can be extended to the case where there does not exist an order on symbols that is compatible with their dependency, however, it does not allow us to deal with the following example:

**Example 4.3.** Let *s* be a constant symbol.

$R_1 : f x \rightarrow g x$

$R_2 : g (s x) \rightarrow s(f x)$

In this example, to prove the injectivity of *f*, we need to have the injectivity of *g*, and vice versa. What we need here is therefore a proof by mutual induction for the injectivity of *f* and *g*.

This observation leads to the generalization obtained from the original algorithm by replacing (*f*, *I*) with a list (*f*<sub>*k*</sub>, *I*<sub>*k*</sub>) of injective conditions to check.

# 5 Related work

The subject reduction is a well-known property for the simply typed λ-calculus, but it becomes a difficult problem in presence of dependent types and rewriting. In [4], Barbanera, Fernández, and Geuvers proved that for the algebraic-λ-cube, which extends Barendregt's λ-cube with algebraic rewriting, the product compatibility (PC) implies the subject reduction property for β-reduction. In [3], Blanqui worked on the case of the calculus of algebraic constructions, an extension of the calculus of constructions with object-level and type-level rewrite rules. In [8], Saillard proved the equivalence between the subject reduction for β-reduction and the product compatibility property in the λΠ-calculus modulo rewriting.

The injectivity of function symbols is a new topic but some works on program inversion using term rewriting systems have been done in the last few decades. For example, in [7], Nishida, Sakai, and Sakabe proposed a partial-inversion compiler of constructor term rewriting systems and in [2], Almendros-Jiménez and Vidal worked on systems expressing functional input-output relations.

# 6 Conclusion and future work

In this report, we propose an algorithm for checking the well-typedness of rewrite rules. The completion procedure allows to retrieve more information from constraints and makes it more possible to solve the equations that need to be satisfied to guarantee that the RHS has the same type as the LHS. However, since higher-order completion is difficult in general, our approach here considers the union of the user-defined rewrite system and the rewrite system obtained by (first-order) completion. Thus, a problem of modularity arises. Until now, we cannot guarantee that the union obtained is confluent and terminating, which makes the conversion decidable, and this is definitely to be improved in the future.

I also propose an algorithm for checking the injectivity of symbols. The use of marked symbols is the most delicate part of this algorithm but this might be improved in the future by choosing a special well-founded relation instead of the one chosen here. Moreover, as mentioned in the last paragraph of the previous section, there exists a generalization of the algorithm that allows to prove several injectivity conditions at the same time. However, it is still not yet known whether there exists an efficient way of determining the injectivity conditions that need to be proved simultaneously from a
single condition. If there exists such a way, then the algorithm proposed can be significantly improved and generalized.

Both algorithms have been implemented in Lambdapi and the code is now available on
https://github.com/wujuihsuan2016/lambdapi/tree/sr/src.

References

[1] A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, R. Saillard. *Dedukti: a logical framework based on the λΠ-calculus modulo theory*, 2016. Draft.

[2] J. M. Almendros-Jiménez and G. Vidal. Automatic partial inversion of inductively sequential functions. In Z. Horváth, et al., editors, *Implementations and Applications of Functional Languages*, volume 4449 of LNCS, pages 253-270. Springer 2007.

[3] F. Blanqui. Definitions by rewriting in the calculus of constructions. *Mathematical Structures in Computer Science*, 15(1):37-92, 2005.

[4] F. Barbanera, M. Fernández, H. Geuvers. Modularity of strong normalization in the algebraic-λ-cube. *Journal of Functional Programming*, 7(6):613-660, 1997.

[5] D. Cousineau and G. Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In Simona Ronchi Della Rocca, editor, *TLCA 2007*, volume 4583 of LNCS, pages 102-117. Springer, 2007.

[6] D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. *Journal of Logic and Computation*, 1:253-281, 1991.

[7] N., Nishida, M. Sakai and T. Sakabe. Partial inversion of constructor term rewriting systems. In J. Giesl, editor, *Term Rewriting and Applications*, volume 3467 of LNCS, pages 264-278, 2005.

[8] R. Saillard. Type checking in the lambda-Pi-calculus modulo: theory and practice. PhD thesis, Mines ParisTech, France, 2015.