Termination of $\lambda$$\Pi$ modulo rewriting using the size-change principle (work in progress)

TL;DR

This paper explores how the size-change termination principle can be applied to ensure termination in higher-order rewriting systems within dependent type theories, extending its original use in first-order functional programs.

Contribution

It demonstrates the applicability of the size-change principle to higher-order rewriting in a dependent type setting, advancing termination analysis techniques.

Findings

Size-change principle can be adapted for higher-order rewriting

Extension of LF with termination guarantees

Potential for improved termination proofs in dependent types

Abstract

The Size-Change Termination principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of dependent types extending LF.

Figures

Equations

$$n$$

$$x$$

Full text

1 Introduction

The Size-Change Termination principle (SCT) was first introduced by Lee, Jones and Ben Amram [8] to study the termination of first-order functional programs. It proved to be very effective, and a few extensions to typed $\lambda$-calculi and higher-order rewriting were proposed.

In his PhD thesis [13], Wahlstedt proposes one for proving the termination, in some presentation of Martin-Löf’s type theory, of an higher-order rewrite system $\mathcal{R}$ together with the $\beta$-reduction of $\lambda$-calculus. He proceeds in two steps. First, he defines an order, the instantiated call relation, and proves that ${\longrightarrow}={\longrightarrow_{\mathcal{R}}\cup\longrightarrow_{\beta}}$ terminates on well-typed terms whenever this order is well-founded. Then, he uses SCT to eventually show the latter.

However, Wahlstedt’s work has some limitations. First, it only considers weak normalization, that is, the mere existence of a normal form. Second, it makes a strong distinction between “constructor” symbols, on which pattern matching is possible, and “defined” symbols, which are allowed to be defined by rewrite rules. Hence, it cannot handle all the systems that one can define in the $\lambda\Pi$-calculus modulo rewriting, the type system implemented in Dedukti [2].

Other works on higher-order rewriting do not have those restrictions, like [3] in which strong normalization (absence of infinite reductions) is proved in the calculus of constructions by requiring each right-hand side of rule to belong to the Computability Closure ($\operatorname{CC}$) of its corresponding left-hand side.

In this paper, we present a combination and extension of both approaches.

2 The $\lambda\Pi$-calculus modulo rewriting

We consider the $\lambda\Pi$-calculus modulo rewriting [2]. This is an extension of Automath, Martin-Löf’s type theory or LF, where functions and types can be defined by rewrite rules, and where types are identified modulo those rules and the $\beta$-reduction of $\lambda$-calculus.

Assuming a signature made of a set $\mathcal{C}_{T}$ of type-level constants, a set $\mathcal{F}_{T}$ of type-level definable function symbols, and a set $\mathcal{F}_{o}$ of object-level function symbols, terms are inductively defined into three categories as follows:

[TABLE]

By $\bar{t}$, we denote a sequence of terms $t_{1}\dots t_{n}$ of length $|\bar{t}|=n$.

Next, we assume given a function $\tau$ associating a kind to every symbol of $\mathcal{C}_{T}$ and $\mathcal{F}_{T}$, and a type to every symbol of $\mathcal{F}_{o}$. If $\tau(f)=(x_{1}:T_{1})\rightarrow\dots\rightarrow(x_{n}:T_{n})\rightarrow U$ with $U$ not an arrow, then $f$ is said of arity $\operatorname{ar}(f)=n$.

An object-level function symbol $f$ of type $(x_{1}:T_{1})\rightarrow\dots\rightarrow(x_{n}:T_{n})\rightarrow D\,u_{1}\dots u_{\operatorname{ar}(D)}$ with $D\in\mathcal{C}_{T}$ and every $T_{i}$ of the form $E\,v_{1}\dots v_{\operatorname{ar}(E)}$ with $E\in\mathcal{C}_{T}$ is called a constructor. Let $\mathcal{C}_{o}$ be the set of constructors.

Terms built from variables and constructor application only are called patterns:

$p::=x\mid c\,p_{1}\dots p_{\operatorname{ar}(c)}\text{ where }c\in\mathcal{C}_{o}$.

Next, we assume given a set $\mathcal{R}$ of rewrite rules of the form $f\,p_{1}\dots p_{\operatorname{ar}(f)}\longrightarrow r$, where $f$ is in $\mathcal{F}_{o}$ or $\mathcal{F}_{T}$, the $p_{i}$’s are patterns and $r$ is $\beta$-normal. Then, let ${\longrightarrow}={\longrightarrow_{\beta}\cup\longrightarrow_{\mathcal{R}}}$ where $\longrightarrow_{\mathcal{R}}$ is the smallest rewrite relation containing $\mathcal{R}$.

Note that rewriting at type level is allowed. For instance, we can define a function taking a natural number $n$ and returning $\operatorname{Nat}\rightarrow\operatorname{Nat}\rightarrow\dots\rightarrow\operatorname{Nat}$ with as many arrows as $n$. In Dedukti syntax, this gives:

⬇

def F : Nat -> Type.

[TABLE]

F 0 --> Nat.

[TABLE]

F (S n) --> Nat -> (F n).

Well-typed terms are defined as in LF, except that types are identified not only modulo $\beta$-equivalence but modulo $\mathcal{R}$-equivalence also, by adding the following type conversion rule:

$\Gamma\vdash t:A$         $\Gamma\vdash A:s$         $\Gamma\vdash B:s$

$\quad\text{if }A\longleftrightarrow^{*}B\text{ and }s\in\{\operatorname{Type},\operatorname{Kind}\}$

$\Gamma\vdash t:B$

Convertibility of $A$ and $B$, $A\longleftrightarrow^{*}B$, is undecidable in general. However, it is decidable if $\longrightarrow$ is confluent and terminating. So, a type-checker for the $\lambda\Pi$-calculus modulo $\longleftrightarrow^{*}$, like Dedukti, needs a criterion to decide termination of $\longrightarrow$. This is the reason of this work.

To this end, we assume that $\longrightarrow$ is confluent and preserves typing.

There exist tools to check confluence, even for higher-order rewrite systems, like CSI^ho or ACPH. The difficulty in presence of type-level rewrite rules, is that we cannot assume termination to show confluence since we need confluence to prove termination. Still, there is a simple criterion in this case: orthogonality [12].

Checking that $\longrightarrow$ preserves typing is undecidable too (for $\longrightarrow_{\beta}$ alone already), and often relies on confluence except when type-level rewrite rules are restricted in some way [3]. Saillard designed and implemented an heuristic in Dedukti [10].

Finally, note that constructors can themselves be defined by rewrite rules. This allows us to define, for instance, the type of integers with two constructors for the predecessor and successor, together with the rules stating that they are inverse of each other.

3 The Size-Change Termination principle

Introduced for first-order functional programming languages by Lee, Jones and Ben Amram [8], the SCT is a simple but powerful criterion to check termination. We recall hereafter the matrix-based presentation of SCT by Lepigre and Raffalli [9].

Definition 3.1** (Size-Change Termination principle).**

The (strict) constructor subterm relation $\lhd$ is the smallest transitive relation such that $t_{i}\lhd c\,t_{1}\dots t_{n}$ when $c\in\mathcal{C}_{o}$.

We define the formal call relation by $f\,\bar{p}$ $>_{call}g\,\bar{t}$ if there is a rewrite rule $f\,\bar{p}\longrightarrow r\in\mathcal{R}$ such that $g\in\mathcal{F}_{T}\cup\mathcal{F}_{o}$ and $g\,\bar{t}$ is a subterm of $r$ with $|\bar{t}|=\operatorname{ar}(g)$.

From this relation, we construct a call graph whose nodes are labeled with the defined symbols. For every call $f\,\bar{p}>_{call}g\,\bar{t}$, an edge labeled with the call matrix $(a_{i,j})_{i\leqslant\operatorname{ar}(f),j\leqslant\operatorname{ar}(g)}$ links the nodes $f$ and $g$, where $a_{i,j}=-1$ if $t_{j}\lhd p_{i}$, $a_{i,j}=0$ if $t_{j}=p_{i}$, and $a_{i,j}=\infty$ otherwise.

A set of rewrite rules $\mathcal{R}$ satisfies the size-change termination principle if the transitive closure of the call graph (using the max-plus semi-ring to multiply the matrices) is such that all arrows linking a node with itself are labeled with a matrix having at least one $-1$ on the diagonal.

The formal call relation is also called the dependency pair relation [1].

4 Wahlstedt’s extension of SCT to Martin-Löf’s Type Theory

The proof of weak normalization in Wahlstedt’s thesis uses an extension to rewriting of Girard’s notion of reducibility candidate [7], called computability predicate here. This technique requires to define an interpretation of every type $T$ as a set of normalizing terms $\llbracket{T}\rrbracket$ called the set of computable terms of type $T$. Once this interpretation is defined, one shows that every well-typed term $t:T$ is computable, that is, belongs to the interpretation of its type: $t\in\llbracket{T}\rrbracket$, ending the normalization proof. To do so, Wahlstedt proceeds in two steps. First, he shows that every well-typed term is computable whenever all symbols are computable. Then, he introduces the following relation which, roughly speaking, corresponds to the notion of minimal chain in the DP framework [1]:

Definition 4.1** (Instantiated call relation).**

Let $f\,\bar{t}\leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\ g\,\bar{v}$ if there exist $\bar{p}$, $\bar{u}$ and a substitution $\gamma$ such that $\bar{t}$ is normalizing, $\bar{t}\longrightarrow^{*}\bar{p}\gamma$, $f\,\bar{p}>_{call}g\,\bar{u}$ and $\bar{u}\gamma=\bar{v}$.

and proves that all symbols are computable if \leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\ is well-founded:

Lemma 4.2** ([13, Lemma 3.6.6, p. 82]).**

If \leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\ is well-founded, then all symbols are computable.

Finally, to prove that \leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\ is well-founded, he uses SCT:

Lemma 4.3** ([13, Theorem 4.2.1, p. 91]).**

\leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\* is well-founded whenever the set of rewrite rules satisfies $\operatorname{SCT}$.*

Indeed, if \leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\ were not well-founded, there would be an infinite sequence $f_{1}\,\bar{t}_{1}\leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\ f_{2}\,\bar{t}_{2}\leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\ \dots$, leading to an infinite path in the call graph which would visit infinitely often at least one node, say $f$. But the matrices labelling the looping edges in the transitive closure all contain at least one $-1$ on the diagonal, meaning that there is an argument of $f$ which strictly decreases in the constructor subterm order at each cycle. This would contradict the well-foundedness of the constructor subterm order.

However, Wahlstedt only considers weak normalization of orthogonal systems, in which constructors are not definable. There exist techniques which do not suffer those restrictions, like the Computability Closure.

5 Computability Closure

The Computability Closure ($\operatorname{CC}$) is also based on an extension of Girard’s computability predicates [4], but for strong normalization. The gist of $\operatorname{CC}$ is, for every left-hand side of a rule $f\,\bar{l}$, to inductively define a set $\operatorname{CC}_{\sqsupset}(f\,\bar{l})$ of terms that are computable whenever the $l_{i}$’s so are. Function applications are handled through the following rule:

$f\,\bar{l}\sqsupset g\,\bar{u}$         $\bar{u}\in\operatorname{CC}_{\sqsupset}(f\,\bar{l})$

$g\,\bar{u}\in\operatorname{CC}_{\sqsupset}(f\,\bar{l})$

where ${\sqsupset}={(\succ_{\mathcal{F}},(\rhd\cup\longrightarrow)_{\mathrm{stat}})_{\mathrm{lex}}}$ is a well-founded order on terms $f\,\bar{t}$ such that $\bar{t}$ are computable, with $\succ_{\mathcal{F}}$ a precedence on function symbols and $\mathrm{stat}$ either the multiset or the lexicographic order extension, depending on $f$.

Then, to get strong normalization, it suffices to check that, for every rule $f\,\bar{l}\longrightarrow r$, we have $r\in\operatorname{CC}_{\sqsupset}(f\,\bar{l})$. This is justified by Lemma 6.38 [3, p.85] stating that all symbols are computable whenever the rules satisfy $\operatorname{CC}$, which looks like Lemma 4.2. It is proved by induction on ${\sqsupset}$. By definition, $f\,\bar{t}$ is computable if, for every $u$ such that $f\,\bar{t}\longrightarrow u$, $u$ is computable. There are two cases. If $u=f\,\bar{t}^{\prime}$ and $\bar{t}\longrightarrow\bar{t}^{\prime}$, then we conclude by the induction hypothesis. Otherwise, $u=r\,\gamma$ where $r$ is the right-hand side of a rule whose left-hand side is of the form $f\,\bar{l}$. This case is handled by induction on the proof that $r\in\operatorname{CC}_{\sqsupset}(f\,\bar{l})$.

So, except for the order, the structures of the proofs are very similar in both works. This is an induction on the order, a case distinction and, in the case of a recursive call, another induction on a refinement of the typing relation, restricted to $\beta$-normal terms in Wahlstedt’s work and to the Computability Closure membership in the other one.

6 Applying ideas of Computability Closure in Wahlstedt’s criterion

We have seen that each method has its own weaknesses: Wahlstedt’s SCT deals with weak normalization only and does not allow pattern-matching on defined symbols, while $\operatorname{CC}$ enforces mutually defined functions to perform a strict decrease in each call.

We can subsume both approaches by combining them and replacing in the definition of $\operatorname{CC}$ the order $\sqsupset$ by the formal call relation:

$f\,\bar{l}>_{call}g\,\bar{u}$         $\bar{u}\in\operatorname{CC}_{>_{call}}(f\,\bar{l})$

$g\,\bar{u}\in\operatorname{CC}_{>_{call}}(f\,\bar{l})$

We must note here that, even if $>_{call}$ is defined from the constructor subterm order, this new definition of $\operatorname{CC}$ does not enforce an argument to be strictly smaller at each recursive call, but only smaller or equal, with the additional constraint that any looping sequence of recursive calls contains a step with a strict decrease, which is enforced by SCT.

Proposition 6.1**.**

Let $\mathcal{R}$ be a rewrite system such that ${\longrightarrow}={\longrightarrow_{\beta}\cup\longrightarrow_{\mathcal{R}}}$ is confluent and preserves typing. If $\mathcal{R}$ satisfies $\operatorname{CC}_{>_{call}}$ and $\operatorname{SCT}$, then $\longrightarrow$ terminates on every term typable in the $\lambda\Pi$-calculus modulo $\longleftrightarrow^{*}$.

Note that $\operatorname{CC}_{>_{call}}$ essentially reduces to checking that the right-hand sides of rules are well-typed which is a condition that is generally satisfied.

The main difficulty is to define an interpretation for types and type symbols that can be defined by rewrite rules. It requires to use induction-recursion [6]. Note that the well-foundedness of the call relation \leavevmode\nobreak\ \widetilde{\succ}\leavevmode\nobreak\ is used not only to prove reducibility of defined symbols, but also to ensure that the interpretation of types is well-defined.

If we consider the example of integers mentioned earlier and define the function erasing every constructor using an auxiliary function, we get a system rejected both by Wahlstedt’s criterion since $\mathtt{S}$ and $\mathtt{P}$ are defined, and by the $CC_{\sqsupset}$ criterion since there is no strict decrease in the first rule. On the other hand, it is accepted by our combined criterion.

⬇

Int : Type. 0 : Int.

def S : Int -> Int. def P : Int -> Int.

[TABLE]

S (P x) --> x.

[TABLE]

P (S x) --> x.

[TABLE]

returnZero x --> aux x.

[TABLE]

aux 0 --> 0.

[TABLE]

aux (S x) --> returnZero x.

[TABLE]

aux (P x) --> returnZero x.

7 Conclusion

We have shown that Wahlstedt’s thesis [13] and the first author’s work [3] have strong similarities. Based on this observation, we developed a combination of both techniques that strictly subsumes both approaches.

This criterion has been implemented in the type-checker Dedukti [2] and gives promising results, even if automatically proving termination of expressive logic encodings remains a challenge. The code is available at https://github.com/Deducteam/Dedukti/tree/sizechange.

Many opportunities exist to enrich our new criterion. For instance, the use of an order leaner than the strict constructor subterm for SCT, like the one defined by Coquand [5] for handling data types with constructors taking functions as arguments. This question is studied in the first-order case by Thiemann and Giesl [11].

Finally, it is important to note the modularity of Wahlstedt’s approach. Termination is obtained by proving 1) that all terms terminate whenever the instantiated call relation is well-founded, and 2) that the instantiated call relation is indeed well-founded. Wahlstedt and we use SCT to prove 2) but it should be noted that other techniques could be used as well. This opens the possibility of applying to type systems like the ones implemented in Dedukti, Coq or Agda, techniques and tools developed for proving the termination of DP problems.

Acknowledgments. The authors thank Olivier Hermant for his comments, as well as the anonymous referees.