A static higher-order dependency pair framework

TL;DR

This paper extends the static dependency pair method for higher-order rewriting termination, introducing a new formalism, soundness criteria, a modular framework, and implementing it in the WANDA tool.

Contribution

It presents a comprehensive extension of the dependency pair framework for higher-order rewriting, including new formalisms, criteria, and techniques, with an implementation in WANDA.

Findings

Framework is sound and applicable to a large class of systems.

The new formalism handles algebraic functional systems with meta-variables.

Implementation in WANDA enables automatic termination proofs.

Abstract

We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework. The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.

Equations

$$\begin{array}[]{rcl}\mathtt{map}\ (\lambda x.Z\langle x\rangle)\ \mathtt{nil}&\Rightarrow&\mathtt{nil}\\ \mathtt{map}\ (\lambda x.Z\langle x\rangle)\ (\mathtt{cons}\ H\ T)&\Rightarrow&\mathtt{cons}\ Z\langle H\rangle\ (\mathtt{map}\ (\lambda x.Z\langle x\rangle)\ T)\\ \end{array}\vspace{-2pt}$$

$$\begin{array}[]{rcl}\mathtt{map}\ Z\ \mathtt{nil}&\Rightarrow&\mathtt{nil}\\ \mathtt{map}\ Z\ (\mathtt{cons}\ H\ T)&\Rightarrow&\mathtt{cons}\ (Z\ H)\ (\mathtt{map}\ Z\ T)\\ \end{array}$$

$$\begin{array}[]{rcl}\mathtt{rec}\ \mathtt{0}\ K\ F\ G&\Rightarrow&K\\ \mathtt{rec}\ (\mathtt{s}\ X)\ K\ F\ G&\Rightarrow&F\ X\ (\mathtt{rec}\ X\ K\ F\ G)\\ \mathtt{rec}\ (\mathtt{lim}\ H)\ K\ F\ G&\Rightarrow&G\ H\ (\lambda m.\mathtt{rec}\ (H\ m)\ K\ F\ G)\\ \end{array}$$

$$\begin{array}[]{c}\mathtt{rec}\ (\mathtt{lim}\ (\lambda n.H\langle n\rangle))\ K\ (\lambda x.\lambda n.F\langle x,n\rangle)\ (\lambda f.\lambda g.G\langle f,g\rangle)\ \Rightarrow\\ G\langle\lambda n.H\langle n\rangle,\ \lambda m.\mathtt{rec}\ H\langle m\rangle\ K\ (\lambda x.\lambda n.F\langle x,n\rangle)\ (\lambda f.\lambda g.G\langle f,g\rangle)\rangle\end{array}$$

$$\mathtt{rec}H⟨m⟩K(\lambda x.\lambda n.F⟨x,n⟩)(\lambda f.\lambda g.G⟨f,g⟩)(\{G:2\})$$

$$\begin{array}[]{rcll}\mathtt{rec}^{\sharp}\ (\mathtt{s}\ X)\ K\ F\ G&\Rrightarrow&\mathtt{rec}^{\sharp}\ X\ K\ F\ G\ (\emptyset)\\ \mathtt{rec}^{\sharp}\ (\mathtt{lim}\ H)\ K\ F\ G&\Rrightarrow&\mathtt{rec}^{\sharp}\ (H\ M)\ K\ F\ G\ (\emptyset)\\ \end{array}$$

$$\left\{\begin{array}[]{rrcll}(1)&\mathtt{f}^{\sharp}\ (\lambda x.F\langle x\rangle)\ (\mathtt{s}\ Y)&\Rrightarrow&\mathtt{f}^{\sharp}\ (\lambda x.\mathtt{0})\ (\mathtt{f}\ (\lambda x.F\langle x\rangle)\ Y)&(\{F:1\})\\ (2)&\mathtt{f}^{\sharp}\ (\lambda x.F\langle x\rangle)\ (\mathtt{s}\ Y)&\Rrightarrow&\mathtt{f}^{\sharp}\ (\lambda x.F\langle x\rangle)\ Y&(\{F:1\})\\ \end{array}\right\}$$

$$\begin{array}[]{rcl}\mathtt{deriv}\ (\lambda x.\mathtt{sin}\ F\langle x\rangle)&\succsim&\lambda y.\mathtt{times}\ (\mathtt{deriv}\ (\lambda x.F\langle x\rangle)\ y)\ (\mathtt{cos}\ F\langle y\rangle)\\ \mathtt{deriv}^{\sharp}\ (\lambda x.\mathtt{sin}\ F\langle x\rangle)&\succ&\mathtt{deriv}^{\sharp}\ (\lambda x.F\langle x\rangle)\\ \end{array}$$

$$\begin{array}[]{rclcrcl}\mathtt{f}\ (\mathtt{s}\ X)\ Y&\succsim&\mathtt{g}\ X\ Y&&\mathtt{f}^{\sharp}\ (\mathtt{s}\ X)\ Y&\succ&\mathtt{g}^{\sharp}\ X\ \bot_{\mathtt{nat}}\\ \mathtt{g}\ X&\succsim&\lambda z.\mathtt{f}\ X\ z&&\mathtt{g}^{\sharp}\ X\ Y&\succcurlyeq&\mathtt{f}^{\sharp}\ X\ Z\\ \end{array}$$

$$t=(\lambda x.q^{\prime })w_0^{\prime }{w}_1^{\prime }\cdots w_n^{\prime }{\Rightarrow }_{\mathtt{head}\beta }^{\ast }{q}^{\prime }[x:=w_0^{\prime }]w_1^{\prime }\cdots w_n^{\prime }=:v$$

$$\begin{array}[]{rcl}F_{\iota}(I)&=&\{s\in I\mid s:\kappa\not\approx^{\mathcal{S}}\iota\}\\ &\cup&\{s\in\mathcal{T}(\mathcal{F},\mathcal{V})\mid s:\kappa\approx^{\mathcal{S}}\iota\wedge s\ \text{is terminating}\\ &&\ \ \text{under}\ \sqsupset\cup\Rrightarrow_{I}\wedge\ \text{if}\ s\sqsupset^{*}\mathtt{f}\ s_{1}\cdots s_{m}\ \text{for a symbol}\\ &&\ \ \mathtt{f}\in\mathcal{F}\ \text{then}\ \forall i\in\mathit{Acc}(\mathtt{f}):\,s_{i}\ \text{is}\ I\text{-computable}]\}\end{array}$$

$$p_{\nu (\mathtt{g})}\gamma =q^{\prime }[x_1:=u_1\gamma ,\dots ,x_k:=u_k\gamma ]v_1\gamma \cdots v_n\gamma$$

$$\begin{array}[]{cl}&p_{\nu(\mathtt{g})}\gamma\\ =&q^{\prime}[x_{1}:=u_{1}^{\prime},\dots,x_{k}:=u_{k}^{\prime}]\ v_{1}^{\prime}\cdots v_{n}^{\prime}\\ =&q^{\prime\prime}[x_{1}:=u_{1}^{\prime},\dots,x_{i}:=u_{i}^{\prime}]\ u_{i+1}^{\prime}\cdots u_{k^{\prime}}^{\prime}\ v_{1}^{\prime}\cdots v_{n}^{\prime}\end{array}$$

Full text

The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.

1 Introduction

Term rewriting [3, 48] is an important area of logic, with applications in many different areas of computer science [4, 11, 18, 23, 25, 36, 41]. Higher-order term rewriting – which extends the traditional first-order term rewriting with higher-order types and binders as in the $\lambda$-calculus – offers a formal foundation of functional programming and a tool for equational reasoning in higher-order logic. A key question in the analysis of both first- and higher-order term rewriting is termination; both for its own sake, and as part of confluence and equivalence analysis.

In first-order term rewriting, a hugely effective method for proving termination (both manually and automatically) is the dependency pair (DP) approach [2]. This approach has been extended to the DP framework [20, 22], a highly modular methodology which new techniques for proving termination and non-termination can easily be plugged into in the form of processors.

In higher-order rewriting, two DP approaches with distinct costs and benefits are used: dynamic [45, 31] and static [6, 44, 34, 46, 32, 33] DPs. Dynamic DPs are more broadly applicable, yet static DPs often enable more powerful analysis techniques. Still, neither approach has the modularity and extendability of the DP framework, nor can they be used to prove non-termination. Also, these approaches consider different styles of higher-order rewriting, which means that for all results certain language features are not available.

In this paper, we address these issues for the static DP approach by extending it to a full higher-order dependency pair framework for both termination and non-termination analysis. For broad applicability, we introduce a new rewriting formalism, AFSMs, to capture several flavours of higher-order rewriting, including AFSs [26] (used in the annual Termination Competition [50]) and pattern HRSs [39, 37] (used in the annual Confluence Competition [10]). To show the versatility and power of this methodology, we define various processors in the framework – both adaptations of existing processors from the literature and entirely new ones.

Detailed contributions. We reformulate the results of [6, 44, 34, 46, 32] into a DP framework for AFSMs. In doing so, we instantiate the applicability restriction of [32] by a very liberal syntactic condition, and add two new flags to track properties of DP problems: one completely new, one from an earlier work by the authors for the first-order DP framework [16]. We give eight processors for reasoning in our framework: four translations of techniques from static DP approaches, three techniques from first-order or dynamic DPs, and one completely new.

This is a foundational paper, focused on defining a general theoretical framework for higher-order termination analysis using dependency pairs rather than questions of implementation. We have, however, implemented most of these results in the fully automatic termination analysis tool WANDA [28].

Related Work. There is a vast body of work in the first-order setting regarding the DP approach [2] and framework [20, 22, 24]. We have drawn from the ideas in these works for the core structure of the higher-order framework, but have added some new features of our own and adapted results to the higher-order setting.

There is no true higher-order DP framework yet: both static and dynamic approaches actually lie halfway between the original “DP approach” of first-order rewriting and a full DP framework as in [20, 22]. Most of these works [30, 31, 32, 34, 46] prove “non-loopingness” or “chain-freeness” of a set $\mathcal{P}$ of DPs through a number of theorems. Yet, there is no concept of DP problems, and the set $\mathcal{R}$ of rules cannot be altered. They also fix assumptions on dependency chains – such as minimality [34] or being “tagged” [31] – which frustrate extendability and are more naturally dealt with in a DP framework using flags.

The static DP approach for higher-order term rewriting is discussed in, e.g., [34, 44, 46]. The approach is limited to plain function passing (PFP) systems. The definition of PFP has been made more liberal in later papers, but always concerns the position of higher-order variables in the left-hand sides of rules. These works include non-pattern HRSs [34, 46], which we do not consider, but do not employ formative rules or meta-variable conditions, or consider non-termination, which we do. Importantly, they do not consider strictly positive inductive types, which could be used to significantly broaden the PFP restriction. Such types are considered in an early paper which defines a variation of static higher-order dependency pairs [6] based on a computability closure [8, 7]. However, this work carries different restrictions (e.g., DPs must be type-preserving and not introduce fresh variables) and considers only one analysis technique (reduction pairs).

Definitions of DP approaches for functional programming also exist [32, 33], which consider applicative systems with ML-style polymorphism. These works also employ a much broader, semantic definition than PFP, which is actually more general than the syntactic restriction we propose here. However, like the static approaches for term rewriting, they do not truly exploit the computability [47] properties inherent in this restriction: it is only used for the initial generation of dependency pairs. In the present work, we will take advantage of our exact computability notion by introducing a $\mathtt{computable}$ flag that can be used by the computable subterm criterion processor (Thm. 0.C.7) to handle benchmark systems that would otherwise be beyond the reach of static DPs. Also in these works, formative rules, meta-variable conditions and non-termination are not considered.

Regarding dynamic DP approaches, a precursor of the present work is [31], which provides a halfway framework (methodology to prove “chain-freeness”) for dynamic DPs, introduces a notion of formative rules, and briefly translates a basic form of static DPs to the same setting. Our formative reductions consider the shape of reductions rather than the rules they use, and they can be used as a flag in the framework to gain additional power in other processors. The adaptation of static DPs in [31] was very limited, and did not for instance consider strictly positive inductive types or rules of functional type.

For a more elaborate discussion of both static and dynamic DP approaches in the literature, we refer to [31] and the second author’s PhD thesis [29].

Organisation of the paper. § 2 introduces higher-order rewriting using AFSMs and recapitulates computability. In § 3 we impose restrictions on the input AFSMs for which our framework is soundly applicable. In § 4 we define static DPs for AFSMs, and derive the key results on them. § 5 formulates the DP framework and a number of DP processors for existing and new termination proving techniques. § 6 concludes. Detailed proofs for all results in this paper (extending [17]) and an experimental evaluation are available in the appendix. In addition, many of the results have been informally published in the second author’s PhD thesis [29].

2 Preliminaries

In this section, we first define our notation by introducing the AFSM formalism. Although not one of the standards of higher-order rewriting, AFSMs combine features from various forms of higher-order rewriting and can be seen as a form of IDTSs [5] which includes application. We will finish with a definition of computability, a technique often used for higher-order termination methods.

2.1 Higher-order term rewriting using AFSMs

Unlike first-order term rewriting, there is no single, unified approach to higher-order term rewriting, but rather a number of similar but not fully compatible systems aiming to combine term rewriting and typed $\lambda$-calculi. For generality, we will use Algebraic Functional Systems with Meta-variables: a formalism which admits translations from the main formats of higher-order term rewriting.

Definition 1 (Simple types)

We fix a set $\mathcal{S}$ of sorts. All sorts are simple types, and if $\sigma,\tau$ are simple types, then so is $\sigma\rightarrow\tau$.

We let $\rightarrow$ be right-associative. Note that all types have a unique representation in the form $\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ with $\iota\in\mathcal{S}$.

Definition 2 (Terms and meta-terms)

We fix disjoint sets $\mathcal{F}$ of function symbols, $\mathcal{V}$ of variables and $\mathcal{M}$ of meta-variables, each symbol equipped with a type. Each meta-variable is additionally equipped with a natural number. We assume that both $\mathcal{V}$ and $\mathcal{M}$ contain infinitely many symbols of all types. The set $\mathcal{T}(\mathcal{F},\mathcal{V})$ of terms over $\mathcal{F},\mathcal{V}$ consists of expressions $s$ where $s:\sigma$ can be derived for some type $\sigma$ by the following clauses:

[TABLE]

Meta-terms are expressions whose type can be derived by those clauses and:

[TABLE]

The $\lambda$ binds variables as in the $\lambda$-calculus; unbound variables are called free, and $\mathit{FV}(s)$ is the set of free variables in $s$. Meta-variables cannot be bound; we write $\mathit{FMV}(s)$ for the set of meta-variables occurring in $s$. A meta-term $s$ is called closed if $\mathit{FV}(s)=\emptyset$ (even if $\mathit{FMV}(s)\neq\emptyset$). Meta-terms are considered modulo $\alpha$-conversion. Application (@) is left-associative; abstractions ($\mathsf{\Lambda}$) extend as far to the right as possible. A meta-term $s$ has type $\sigma$ if $s:\sigma$; it has base type if $\sigma\in\mathcal{S}$. We define $\mathsf{head}(s)=\mathsf{head}(s_{1})$ if $s=s_{1}\ s_{2}$, and $\mathsf{head}(s)=s$ otherwise.

A (meta-)term $s$ has a sub-(meta-)term $t$, notation $s\unrhd t$, if either $s=t$ or $s\rhd t$, where $s\rhd t$ if (a) $s=\lambda x.s^{\prime}$ and $s^{\prime}\unrhd t$, (b) $s=s_{1}\ s_{2}$ and $s_{2}\unrhd t$ or (c) $s=s_{1}\ s_{2}$ and $s_{1}\unrhd t$. A (meta-)term $s$ has a fully applied sub-(meta-)term $t$, notation $s\mathbin{\hskip 1.0pt\underline{\blacktriangleright}\hskip 1.0pt}t$, if either $s=t$ or $s\blacktriangleright t$, where $s\blacktriangleright t$ if (a) $s=\lambda x.s^{\prime}$ and $s^{\prime}\mathbin{\hskip 1.0pt\underline{\blacktriangleright}\hskip 1.0pt}t$, (b) $s=s_{1}\ s_{2}$ and $s_{2}\mathbin{\hskip 1.0pt\underline{\blacktriangleright}\hskip 1.0pt}t$ or (c) $s=s_{1}\ s_{2}$ and $s_{1}\blacktriangleright t$ (so if $s=x\ s_{1}\ s_{2}$, then $x$ and $x\ s_{1}$ are not fully applied subterms, but $s$ and both $s_{1}$ and $s_{2}$ are).

For $Z:(\sigma,k)\in\mathcal{M}$, we call $k$ the arity of $Z$, notation $\mathit{arity}(Z)$.

Clearly, all fully applied subterms are subterms, but not all subterms are fully applied. Every term $s$ has a form $t\ s_{1}\cdots s_{n}$ with $n\geq 0$ and $t=\mathsf{head}(s)$ a variable, function symbol, or abstraction; in meta-terms $t$ may also be a meta-variable application $F\langle s_{1},\dots,s_{k}\rangle$. Terms are the objects that we will rewrite; meta-terms are used to define rewrite rules. Note that all our terms (and meta-terms) are, by definition, well-typed. For rewriting, we will employ patterns:

Definition 3 (Patterns)

A meta-term is a pattern if it has one of the forms $Z\langle x_{1},\dots,x_{k}\rangle$ with all $x_{i}$ distinct variables; $\lambda x.\ell$ with $x\in\mathcal{V}$ and $\ell$ a pattern; or $a\ \ell_{1}\cdots\ell_{n}$ with $a\in\mathcal{F}\cup\mathcal{V}$ and all $\ell_{i}$ patterns ($n\geq 0$).

In rewrite rules, we will use meta-variables for matching and variables only with binders. In terms, variables can occur both free and bound, and meta-variables cannot occur. Meta-variables originate in very early forms of higher-order rewriting (e.g., [1, 27]), but have also been used in later formalisms (e.g., [8]). They strike a balance between matching modulo $\beta$ and syntactic matching. By using meta-variables, we obtain the same expressive power as with Miller patterns [37], but do so without including a reversed $\beta$-reduction as part of matching.

Notational conventions: We will use $x,y,z$ for variables, $X,Y,Z$ for meta-variables, $b$ for symbols that could be variables or meta-variables, $\mathtt{f},\mathtt{g},\mathtt{h}$ or more suggestive notation for function symbols, and $s,t,u,v,q,w$ for (meta-)terms. Types are denoted $\sigma,\tau$, and $\iota,\kappa$ are sorts. We will regularly overload notation and write $x\in\mathcal{V}$, $\mathtt{f}\in\mathcal{F}$ or $Z\in\mathcal{M}$ without stating a type (or minimal arity). For meta-terms $Z\langle\rangle$ we will usually omit the brackets, writing just $Z$.

Definition 4 (Substitution)

A meta-substitution is a type-preserving function $\gamma$ from variables and meta-variables to meta-terms. Let the domain of $\gamma$ be given by: $\mathtt{dom}(\gamma)=\{(x:\sigma)\in\mathcal{V}\mid\gamma(x)\neq x\}\cup\{(Z:(\sigma,k))\in\mathcal{M}\mid\gamma(Z)\neq\lambda y_{1}\dots y_{k}.Z\langle y_{1},\dots,y_{k}\rangle\}$; this domain is allowed to be infinite. We let $[b_{1}:=s_{1},\dots,b_{n}:=s_{n}]$ denote the meta-substitution $\gamma$ with $\gamma(b_{i})=s_{i}$ and $\gamma(z)=z$ for $(z:\sigma)\in\mathcal{V}\setminus\{b_{1},\dots,b_{n}\}$, and $\gamma(Z)=\lambda y_{1}\dots y_{k}.Z\langle y_{1},\dots,y_{k}\rangle$ for $(Z:(\sigma,k))\in\mathcal{M}\setminus\{b_{1},\dots,b_{n}\}$. We assume there are infinitely many variables $x$ of all types such that (a) $x\notin\mathtt{dom}(\gamma)$ and (b) for all $b\in\mathtt{dom}(\gamma)$: $x\notin\mathit{FV}(\gamma(b))$.

A substitution is a meta-substitution mapping everything in its domain to terms. The result $s\gamma$ of applying a meta-substitution $\gamma$ to a term $s$ is obtained by:

[TABLE]

For meta-terms, the result $s\gamma$ is obtained by the clauses above and:

[TABLE]

Note that for fixed $k$, any term has exactly one of the two forms above ($\lambda x_{1}\dots x_{n}.s$ with $n<k$ and $s$ not an abstraction, or $\lambda x_{1}\dots x_{k}.s$).

Essentially, applying a meta-substitution that has meta-variables in its domain combines a substitution with (possibly several) $\beta$-steps. For example, we have that:$\mathtt{deriv}\ (\lambda x.\mathtt{sin}\ (F\langle x\rangle))[F:=\lambda y.\mathtt{plus}\ y\ x]$ equals $\mathtt{deriv}\ (\lambda z.\mathtt{sin}\ (\mathtt{plus}\ z\ x))$. We also have: $X\langle\mathtt{0},\mathtt{nil}\rangle[X:=\lambda x.\mathtt{map}\ (\lambda y.x)]$ equals $\mathtt{map}\ (\lambda y.\mathtt{0})\ \mathtt{nil}$.

Definition 5 (Rules and rewriting)

Let $\mathcal{F},\mathcal{V},\mathcal{M}$ be fixed sets of function symbols, variables and meta-variables respectively. A rule is a pair $\ell\Rightarrow r$ of closed meta-terms of the same type such that $\ell$ is a pattern of the form $\mathtt{f}\ \ell_{1}\cdots\ell_{n}$ with $\mathtt{f}\in\mathcal{F}$ and $\mathit{FMV}(r)\subseteq\mathit{FMV}(\ell)$. A set of rules $\mathcal{R}$ defines a rewrite relation $\Rightarrow_{\mathcal{R}}$ as the smallest monotonic relation on terms which includes:

[TABLE]

We say $s\Rightarrow_{\beta}t$ if $s\Rightarrow_{\mathcal{R}}t$ is derived using a (Beta) step. A term $s$ is terminating under $\Rightarrow_{\mathcal{R}}$ if there is no infinite reduction $s=s_{0}\Rightarrow_{\mathcal{R}}s_{1}\Rightarrow_{\mathcal{R}}\dots$, is in normal form if there is no $t$ such that $s\Rightarrow_{\mathcal{R}}t$, and is $\beta$-normal if there is no $t$ with $s\Rightarrow_{\beta}t$. Note that we are allowed to reduce at any position of a term, even below a $\lambda$. The relation $\Rightarrow_{\mathcal{R}}$ is terminating if all terms over $\mathcal{F},\mathcal{V}$ are terminating. The set $\mathcal{D}\subseteq\mathcal{F}$ of defined symbols consists of those $(\mathtt{f}:\sigma)\in\mathcal{F}$ such that a rule $\mathtt{f}\ \ell_{1}\cdots\ell_{n}\Rightarrow r$ exists; all other symbols are called constructors.

Note that $\mathcal{R}$ is allowed to be infinite, which is useful for instance to model polymorphic systems. Also, right-hand sides of rules do not have to be in $\beta$-normal form. While this is rarely used in practical examples, non-$\beta$-normal rules may arise through transformations, and we lose nothing by allowing them.

Example 1

Let $\mathcal{F}\supseteq\{\mathtt{0}:\mathtt{nat},\ \mathtt{s}:\mathtt{nat}\rightarrow\mathtt{nat},\ \mathtt{nil}:\mathtt{list},\mathtt{cons}:\mathtt{nat}\rightarrow\mathtt{list}\rightarrow\mathtt{list},\ \mathtt{map}:(\mathtt{nat}\rightarrow\mathtt{nat})\rightarrow\mathtt{list}\rightarrow\mathtt{list}\}$ and consider the following rules $\mathcal{R}$:

[TABLE]

Then $\mathtt{map}\ (\lambda y.\mathtt{0})\ (\mathtt{cons}\ (\mathtt{s}\ \mathtt{0})\ \mathtt{nil})\Rightarrow_{\mathcal{R}}\mathtt{cons}\ \mathtt{0}\ (\mathtt{map}\ (\lambda y.\mathtt{0})\ \mathtt{nil})\Rightarrow_{\mathcal{R}}\mathtt{cons}\ \mathtt{0}\ \mathtt{nil}$. Note that the bound variable $y$ does not need to occur in the body of $\lambda y.\mathtt{0}$ to match $\lambda x.Z\langle x\rangle$. However, a term like $\mathtt{map}\ \mathtt{s}\ (\mathtt{cons}\ \mathtt{0}\ \mathtt{nil})$ cannot be reduced, because $\mathtt{s}$ does not instantiate $\lambda x.Z\langle x\rangle$. We could alternatively consider the rules:

[TABLE]

Where the system before had $(Z:(\mathtt{nat}\rightarrow\mathtt{nat},1))\in\mathcal{M}$, here we assume $(Z:(\mathtt{nat}\rightarrow\mathtt{nat},0))\in\mathcal{M}$. Thus, rather than meta-variable application $Z\langle H\rangle$ we use explicit application $Z\ H$. Then $\mathtt{map}\ \mathtt{s}\ (\mathtt{cons}\ \mathtt{0}\ \mathtt{nil})\Rightarrow_{\mathcal{R}}\mathtt{cons}\ (\mathtt{s}\ \mathtt{0})\ (\mathtt{map}\ \mathtt{s}\ \mathtt{nil})$. However, we will often need explicit $\beta$-reductions; e.g., $\mathtt{map}\ (\lambda y.\mathtt{0})\ (\mathtt{cons}\ (\mathtt{s}\ \mathtt{0})\ \mathtt{nil})\linebreak\Rightarrow_{\mathcal{R}}\mathtt{cons}\ ((\lambda y.\mathtt{0})\ (\mathtt{s}\ \mathtt{0}))\ (\mathtt{map}\ (\lambda y.\mathtt{0})\ \mathtt{nil})\Rightarrow_{\beta}\mathtt{cons}\ \mathtt{0}\ (\mathtt{map}\ (\lambda y.\mathtt{0})\ \mathtt{nil})$.

Definition 6 (AFSM)

An AFSM is a tuple $(\mathcal{F},\mathcal{V},\mathcal{M},\mathcal{R})$ of a signature and a set of rules built from meta-terms over $\mathcal{F},\mathcal{V},\mathcal{M}$; as types of relevant variables and meta-variables can always be derived from context, we will typically just refer to the AFSM $(\mathcal{F},\mathcal{R})$. An AFSM implicitly defines the abstract reduction system $(\mathcal{T}(\mathcal{F},\mathcal{V}),\Rightarrow_{\mathcal{R}})$: a set of terms and a rewrite relation on this set. An AFSM is terminating if $\Rightarrow_{\mathcal{R}}$ is terminating (on all terms in $\mathcal{T}(\mathcal{F},\mathcal{V})$).

Discussion: The two most common formalisms in termination analysis of higher-order rewriting are algebraic functional systems [26] (AFSs) and higher-order rewriting systems [39, 37] (HRSs). AFSs are very similar to our AFSMs, but use variables for matching rather than meta-variables; this is trivially translated to the AFSM format, giving rules where all meta-variables have arity [math], like the “alternative” rules in Ex. 1. HRSs use matching modulo $\beta/\eta$, but the common restriction of pattern HRSs can be directly translated into AFSMs, provided terms are $\beta$-normalised after every reduction step. Even without this $\beta$-normalisation step, termination of the obtained AFSM implies termination of the original HRS; for second-order systems, termination is equivalent. AFSMs can also naturally encode CRSs [27] and several applicative systems (cf. [29, Chapter 3]).

Example 2 (Ordinal recursion)

A running example is the AFSM $(\mathcal{F},\mathcal{R})$ with $\mathcal{F}\supseteq\{\mathtt{0}:\mathtt{ord},\ \mathtt{s}:\mathtt{ord}\rightarrow\mathtt{ord},\mathtt{lim}:(\mathtt{nat}\rightarrow\mathtt{ord})\rightarrow\mathtt{ord},\ \mathtt{rec}:\mathtt{ord}\rightarrow\mathtt{nat}\rightarrow(\mathtt{ord}\rightarrow\mathtt{nat}\rightarrow\mathtt{nat})\rightarrow((\mathtt{nat}\rightarrow\mathtt{ord})\rightarrow(\mathtt{nat}\rightarrow\mathtt{nat})\rightarrow\mathtt{nat})\rightarrow\mathtt{nat}\}$ and $\mathcal{R}$ given below. As all meta-variables have arity [math], this can be seen as an AFS.

[TABLE]

Observant readers may notice that by the given constructors, the type $\mathtt{nat}$ in Ex. 2 is not inhabited. However, as the given symbols are only a subset of $\mathcal{F}$, additional symbols (such as constructors for the $\mathtt{nat}$ type) may be included. The presence of additional function symbols does not affect termination of AFSMs:

Theorem 2.1 (Invariance of termination under signature extensions)

For an AFSM $(\mathcal{F},\mathcal{R})$ with $\mathcal{F}$ at most countably infinite, let $\mathtt{funs}(\mathcal{R})\subseteq\mathcal{F}$ be the set of function symbols occurring in some rule of $\mathcal{R}$. Then $(\mathcal{T}(\mathcal{F},\mathcal{V}),\Rightarrow_{\mathcal{R}})$ is terminating if and only if $(\mathcal{T}(\mathtt{funs}(\mathcal{R}),\mathcal{V}),\Rightarrow_{\mathcal{R}})$ is terminating.

Proof

Trivial by replacing all function symbols in $\mathcal{F}\setminus\mathtt{funs}(\mathcal{R})$ by corresponding variables of the same type. ∎

Therefore, we will typically only state the types of symbols occurring in the rules, but may safely assume that infinitely many symbols of all types are present (which for instance allows us to select unused constructors in some proofs).

2.2 Computability

A common technique in higher-order termination is Tait and Girard’s computability notion [47]. There are several ways to define computability predicates; here we follow, e.g., [5, 8, 9, 7] in considering accessible meta-terms using strictly positive inductive types. The definition presented below is adapted from these works, both to account for the altered formalism and to introduce (and obtain termination of) a relation $\Rrightarrow_{C}$ that we will use in the “computable subterm criterion processor” of Thm. 0.C.7 (a termination criterion that allows us to handle systems that would otherwise be beyond the reach of static DPs). This allows for a minimal presentation that avoids the use of ordinals that would otherwise be needed to obtain $\Rrightarrow_{C}$ (see, e.g., [9, 7]).

To define computability, we use the notion of an RC-set:

Definition 7

A set of reducibility candidates, or RC-set, for a rewrite relation $\Rightarrow_{\mathcal{R}}$ of an AFSM is a set $I$ of base-type terms $s$ such that: every term in $I$ is terminating under $\Rightarrow_{\mathcal{R}}$; $I$ is closed under $\Rightarrow_{\mathcal{R}}$ (so if $s\in I$ and $s\Rightarrow_{\mathcal{R}}t$ then $t\in I$); if $s=x\ s_{1}\cdots s_{n}$ with $x\in\mathcal{V}$ or $s=(\lambda x.u)\ s_{0}\cdots s_{n}$ with $n\geq 0$, and for all $t$ with $s\Rightarrow_{\mathcal{R}}t$ we have $t\in I$, then $s\in I$ (for any $u,s_{0},\dots,s_{n}\in\mathcal{T}(\mathcal{F},\mathcal{V})$).

We define $I$-computability for an RC-set $I$ by induction on types. For $s\in\mathcal{T}(\mathcal{F},\mathcal{V})$, we say that $s$ is $I$-computable if either $s$ is of base type and $s\in I$; or $s:\sigma\rightarrow\tau$ and for all $t:\sigma$ that are $I$-computable, $s\ t$ is $I$-computable.

The traditional notion of computability is obtained by taking for $I$ the set of all terminating base-type terms. Then, a term $s$ is computable if and only if (a) $s$ has base type and is terminating; or (b) $s:\sigma\rightarrow\tau$ and for all computable $t:\sigma$ the term $s\ t$ is computable. This choice is simple but, for reasoning, not ideal: we do not have a property like: “if $\mathtt{f}\ s_{1}\cdots s_{n}$ is computable then so is each $s_{i}$”. Such a property would be valuable to have for generalising termination proofs from first-order to higher-order rewriting, as it allows us to use computability where the first-order proof uses termination. While it is not possible to define a computability notion with this property alongside case (b) (as such a notion would not be well-founded), we can come close to this property by choosing a different set for $I$. To define this set, we will use the notion of accessible arguments, which is used for the same purpose also in the General Schema [8], the Computability Path Ordering [9], and the Computability Closure [7].

Definition 8 (Accessible arguments)

We fix a quasi-ordering $\succeq^{\mathcal{S}}$ on $\mathcal{S}$ with well-founded strict part $\succ^{\mathcal{S}}\ :=\ \succeq^{\mathcal{S}}\setminus\preceq^{\mathcal{S}}$.111Well-foundedness is immediate if $\mathcal{S}$ is finite, but we have not imposed that requirement. For a type $\sigma\equiv\sigma_{1}\!\rightarrow\!\dots\!\rightarrow\!\sigma_{m}\!\rightarrow\!\kappa$ (with $\kappa\in\mathcal{S}$) and sort $\iota$, let $\iota\succeq^{\mathcal{S}}_{+}\sigma$ if $\iota\succeq^{\mathcal{S}}\kappa$ and $\iota\succ^{\mathcal{S}}_{-}\sigma_{i}$ for all $i$, and let $\iota\succ^{\mathcal{S}}_{-}\sigma$ if $\iota\succ^{\mathcal{S}}\kappa$ and $\iota\succeq^{\mathcal{S}}_{+}\sigma_{i}$ for all $i$.222Here $\iota\succeq^{\mathcal{S}}_{+}\sigma$ corresponds to “$\iota$ occurs only positively in $\sigma$” in [5, 8, 9].

For $\mathtt{f}:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota\in\mathcal{F}$, let $\mathit{Acc}(\mathtt{f})=\{i\mid 1\leq i\leq m\wedge\iota\succeq^{\mathcal{S}}_{+}\sigma_{i}\}$. For $x:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota\in\mathcal{V}$, let $\mathit{Acc}(x)=\{i\mid 1\leq i\leq m\wedge\sigma_{i}$ has the form $\tau_{1}\rightarrow\dots\rightarrow\tau_{n}\rightarrow\kappa$ with $\iota\succeq^{\mathcal{S}}\kappa\}$. We write $s\unrhd_{\mathtt{acc}}t$ if either $s=t$, or $s=\lambda x.s^{\prime}$ and $s^{\prime}\unrhd_{\mathtt{acc}}t$, or $s=a\ s_{1}\cdots s_{n}$ with $a\in\mathcal{F}\cup\mathcal{V}$ and $s_{i}\unrhd_{\mathtt{acc}}t$ for some $i\in\mathit{Acc}(a)$ with $a\notin\mathit{FV}(s_{i})$.

With this definition, we will be able to define a set $C$ such that, roughly, $s$ is $C$-computable if and only if (a) $s:\sigma\rightarrow\tau$ and $s\ t$ is $C$-computable for all $C$-computable $t$, or (b) $s$ has base type, is terminating, and if $s=\mathtt{f}\ s_{1}\cdots s_{m}$ then $s_{i}$ is $C$-computable for all accessible $i$ (see Thm. 2.2 below). The reason that $\mathit{Acc}(x)$ for $x\in\mathcal{V}$ is different is proof-technical: computability of $\lambda x.x\ s_{1}\cdots s_{m}$ implies the computability of more arguments $s_{i}$ than computability of $\mathtt{f}\ s_{1}\cdots s_{m}$ does, since $x$ can be instantiated by anything.

Example 3

Consider a quasi-ordering $\succeq^{\mathcal{S}}$ such that $\mathtt{ord}\succ^{\mathcal{S}}\mathtt{nat}$. In Ex. 2, we then have $\mathtt{ord}\>\succeq^{\mathcal{S}}_{+}\>\mathtt{nat}\rightarrow\mathtt{ord}$. Thus, $1\in\mathit{Acc}(\mathtt{lim})$, which gives $\mathtt{lim}\ H\unrhd_{\mathtt{acc}}H$.

Theorem 2.2

Let $(\mathcal{F},\mathcal{R})$ be an AFSM. Let $\mathtt{f}\ s_{1}\cdots s_{m}\Rrightarrow_{I}s_{i}\ t_{1}\cdots t_{n}$ if both sides have base type, $i\in\mathit{Acc}(\mathtt{f})$, and all $t_{j}$ are $I$-computable. There is an RC-set $C$ such that $C=\{s\in\mathcal{T}(\mathcal{F},\mathcal{V})\mid s$ has base type $\wedge\ s$ is terminating under $\Rightarrow_{\mathcal{R}}\cup\Rrightarrow_{C}\wedge{}$ if $s\Rightarrow_{\mathcal{R}}^{*}\mathtt{f}\ s_{1}\cdots s_{m}$ then $s_{i}$ is $C$-computable for all $i\in\mathit{Acc}(\mathtt{f})\}$.

Proof (sketch)

Note that we cannot define $C$ as this set, as the set relies on the notion of $C$-computability. However, we can define $C$ as the fixpoint of a monotone function operating on RC-sets. This follows the proof in, e.g., [8, 9]. ∎

The full proof (for the definitions in this paper) is available in Appendix 0.A.

3 Restrictions

The termination methodology in this paper is restricted to AFSMs that satisfy certain limitations: they must be properly applied (a restriction on the number of terms each function symbol is applied to) and accessible function passing (a restriction on the positions of variables of a functional type in the left-hand sides of rules). Both are syntactic restrictions that are easily checked by a computer (mostly; the latter requires a search for a sort ordering, but this is typically easy).

3.1 Properly applied AFSMs

In properly applied AFSMs, function symbols are assigned a certain, minimal number of arguments that they must always be applied to.

Definition 9

An AFSM $(\mathcal{F},\mathcal{R})$ is properly applied if for every $\mathtt{f}\in\mathcal{D}$ there exists an integer $k$ such that for all rules $\ell\Rightarrow r\in\mathcal{R}$: (1) if $\ell=\mathtt{f}\ \ell_{1}\cdots\ell_{n}$ then $n=k$; and (2) if $r\mathbin{\hskip 1.0pt\underline{\blacktriangleright}\hskip 1.0pt}\mathtt{f}\ r_{1}\cdots r_{n}$ then $n\geq k$. We denote $\mathit{minar}(\mathtt{f})=k$.

That is, every occurrence of a function symbol in the right-hand side of a rule has at least as many arguments as the occurrences in the left-hand sides of rules. This means that partially applied functions are often not allowed: an AFSM with rules such as $\mathtt{double}\ X\Rightarrow\mathtt{plus}\ X\ X$ and $\mathtt{doublelist}\ L\Rightarrow\mathtt{map}\ \mathtt{double}\ L$ is not properly applied, because $\mathtt{double}$ is applied to one argument in the left-hand side of some rule, and to zero in the right-hand side of another.

This restriction is not as severe as it may initially seem since partial applications can be replaced by $\lambda$-abstractions; e.g., the rules above can be made properly applied by replacing the second rule by: $\mathtt{doublelist}\ L\Rightarrow\mathtt{map}\ (\lambda x.\mathtt{double}\ x)\ L$. By using $\eta$-expansion, we can transform any AFSM to satisfy this restriction:

Definition 10 ($\mathcal{R}^{\uparrow}$)

Given a set of rules $\mathcal{R}$, let their $\eta$-expansion be given by $\mathcal{R}^{\uparrow}=\{(\ell\ Z_{1}\cdots Z_{m})\!\!\uparrow^{\eta}\ \Rightarrow(r\ Z_{1}\cdots Z_{m})\!\!\uparrow^{\eta}\mid\ell\Rightarrow r\in\mathcal{R}$ with $r:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$, $\iota\in\mathcal{S}$, and $Z_{1},\dots,Z_{m}$ fresh meta-variables$\}$, where

• •

$s\!\!\uparrow^{\eta}=\lambda x_{1}\dots x_{m}.\overline{s}\ (x_{1}\!\!\uparrow^{\eta})\cdots(x_{m}\!\!\uparrow^{\eta})$ if $s$ is an application or element of $\mathcal{V}\cup\mathcal{F}$, and $s\!\!\uparrow^{\eta}=\overline{s}$ otherwise;

• •

$\overline{\mathtt{f}}=\mathtt{f}$ for $\mathtt{f}\in\mathcal{F}$ and $\overline{x}=x$ for $x\in\mathcal{V}$, while $\overline{Z\langle s_{1},\dots,s_{k}\rangle}=Z\langle\overline{s_{1}},\dots,\overline{s_{k}}\rangle$ and $\overline{(\lambda x.s)}=\lambda x.(s\!\!\uparrow^{\eta})$ and $\overline{s_{1}\ s_{2}}=\overline{s_{1}}\ (s_{2}\!\!\uparrow^{\eta})$.

Note that $\ell\!\!\uparrow^{\eta}$ is a pattern if $\ell$ is. By [29, Thm. 2.16], a relation $\Rightarrow_{\mathcal{R}}$ is terminating if $\Rightarrow_{\mathcal{R}^{\uparrow}}$ is terminating, which allows us to transpose any methods to prove termination of properly applied AFSMs to all AFSMs.

However, there is a caveat: this transformation can introduce non-termination in some special cases, e.g., the terminating rule $\mathtt{f}\ X\Rightarrow\mathtt{g}\ \mathtt{f}$ with $\mathtt{f}:\mathtt{o}\rightarrow\mathtt{o}$ and $\mathtt{g}:(\mathtt{o}\rightarrow\mathtt{o})\rightarrow\mathtt{o}$, whose $\eta$-expansion $\mathtt{f}\ X\Rightarrow\mathtt{g}\ (\lambda x.(\mathtt{f}\ x))$ is non-terminating. Thus, for a properly applied AFSM the methods in this paper apply directly. For an AFSM that is not properly applied, we can use the methods to prove termination (but not non-termination) by first $\eta$-expanding the rules. Of course, if this analysis leads to a counterexample for termination, we may still be able to verify whether this counterexample applies in the original, untransformed AFSM.

Example 4

Both AFSMs in Ex. 1 and the AFSM in Ex. 2 are properly applied.

Example 5

Consider an AFSM $(\mathcal{F},\mathcal{R})$ with $\mathcal{F}\supseteq\{\mathtt{sin},\mathtt{cos}:\real\rightarrow\real,\linebreak\mathtt{times}:\real\rightarrow\real\rightarrow\real,\ \mathtt{deriv}:(\real\rightarrow\real)\rightarrow\real\rightarrow\real\}$ and $\mathcal{R}=\{\mathtt{deriv}\ (\lambda x.\mathtt{sin}\ F\langle x\rangle)\Rightarrow\lambda y.\mathtt{times}\ (\mathtt{deriv}\ (\lambda x.F\langle x\rangle)\ y)\ (\mathtt{cos}\ F\langle y\rangle)\}$. Although the one rule has a functional output type ($\real\rightarrow\real$), this AFSM is properly applied, with $\mathtt{deriv}$ having always at least $1$ argument. Therefore, we do not need to use $\mathcal{R}^{\uparrow}$. However, if $\mathcal{R}$ were to additionally include some rules that did not satisfy the restriction (such as the $\mathtt{double}$ and $\mathtt{doublelist}$ rules above), then $\eta$-expanding all rules, including this one, would be necessary. We have: $\mathcal{R}^{\uparrow}=\{\mathtt{deriv}\ (\lambda x.\mathtt{sin}\ F\langle x\rangle)\ Y\Rightarrow(\lambda y.\mathtt{times}\ (\mathtt{deriv}\ (\lambda x.F\langle x\rangle)\ y)\ (\mathtt{cos}\ F\langle y\rangle))\ Y\}$. Note that the right-hand side of the $\eta$-expanded $\mathtt{deriv}$ rule is not $\beta$-normal.

3.2 Accessible Function Passing AFSMs

In accessible function passing AFSMs, variables of functional type may not occur at arbitrary places in the left-hand sides of rules: their positions are restricted using the sort ordering $\succeq^{\mathcal{S}}$ and accessibility relation $\unrhd_{\mathtt{acc}}$ from Def. 8.

Definition 11 (Accessible function passing)

An AFSM $(\mathcal{F},\mathcal{R})$ is accessible function passing (AFP) if there exists a sort ordering $\succeq^{\mathcal{S}}$ following Def. 8 such that: for all $\mathtt{f}\ \ell_{1}\cdots\ell_{n}\Rightarrow r\in\mathcal{R}$ and all $Z\in\mathit{FMV}(r)$: there are variables $x_{1},\dots,x_{k}$ and some $i$ such that $\ell_{i}\unrhd_{\mathtt{acc}}Z\langle x_{1},\dots,x_{k}\rangle$.

The key idea of this definition is that computability of each $\ell_{i}$ implies computability of all meta-variables in $r$. This excludes cases like Example 7 below. Many common examples satisfy this restriction, including those we saw before:

Example 6

Both systems from Ex. 1 are AFP: choosing the sort ordering $\succeq^{\mathcal{S}}$ that equates $\mathtt{nat}$ and $\mathtt{list}$, we indeed have $\mathtt{cons}\ H\ T\unrhd_{\mathtt{acc}}H$ and $\mathtt{cons}\ H\ T\unrhd_{\mathtt{acc}}T$ (as $\mathit{Acc}(\mathtt{cons})=\{1,2\}$) and both $\lambda x.Z\langle x\rangle\unrhd_{\mathtt{acc}}Z\langle x\rangle$ and $Z\unrhd_{\mathtt{acc}}Z$. The AFSM from Ex. 2 is AFP because we can choose $\mathtt{ord}\succ^{\mathcal{S}}\mathtt{nat}$ and have $\mathtt{lim}\ H\unrhd_{\mathtt{acc}}H$ following Ex. 3 (and also $\mathtt{s}\ X\unrhd_{\mathtt{acc}}X$ and $K\unrhd_{\mathtt{acc}}K,\ F\unrhd_{\mathtt{acc}}F,\ G\unrhd_{\mathtt{acc}}G$). The AFSM from Ex. 5 is AFP, because $\lambda x.\mathtt{sin}\ F\langle x\rangle\unrhd_{\mathtt{acc}}F\langle x\rangle$ for any $\succeq^{\mathcal{S}}$: $\lambda x.\mathtt{sin}\ F\langle x\rangle\unrhd_{\mathtt{acc}}F\langle x\rangle$ because $\mathtt{sin}\ F\langle x\rangle\unrhd_{\mathtt{acc}}F\langle x\rangle$ because $1\in\mathit{Acc}(\mathtt{sin})$.

In fact, all first-order AFSMs (where all fully applied sub-meta-terms of the left-hand side of a rule have base type) are AFP via the sort ordering $\succeq^{\mathcal{S}}$ that equates all sorts. Also (with the same sort ordering), an AFSM $(\mathcal{F},\mathcal{R})$ is AFP if, for all rules $\mathtt{f}\ \ell_{1}\cdots\ell_{k}\Rightarrow r\in\mathcal{R}$ and all $1\leq i\leq k$, we can write: $\ell_{i}=\lambda x_{1}\dots x_{n_{i}}.\ell^{\prime}$ where $n_{i}\geq 0$ and all fully applied sub-meta-terms of $\ell^{\prime}$ have base type.

This covers many practical systems, although for Ex. 2 we need a non-trivial sort ordering. Also, there are AFSMs that cannot be handled with any $\succeq^{\mathcal{S}}$.

Example 7 (Encoding the untyped $\lambda$-calculus)

Consider an AFSM with $\mathcal{F}\supseteq\{\mathtt{ap}:\mathtt{o}\rightarrow\mathtt{o}\rightarrow\mathtt{o},\ \mathtt{lm}:(\mathtt{o}\rightarrow\mathtt{o})\rightarrow\mathtt{o}\}$ and $\mathcal{R}=\{\mathtt{ap}\ (\mathtt{lm}\ F)\Rightarrow F\}$ (note that the only rule has type $\mathtt{o}\rightarrow\mathtt{o}$). This AFSM is not accessible function passing, because $\mathtt{lm}\ F\unrhd_{\mathtt{acc}}F$ cannot hold for any $\succeq^{\mathcal{S}}$ (as this would require $\mathtt{o}\succ^{\mathcal{S}}\mathtt{o}$).

Note that this example is also not terminating. With $t=\mathtt{lm}\ (\lambda x.\mathtt{ap}\ x\ x)$, we get this self-loop as evidence: $\mathtt{ap}\ t\ t\ \Rightarrow_{\mathcal{R}}(\lambda x.\mathtt{ap}\ x\ x)\ t\Rightarrow_{\beta}\mathtt{ap}\ t\ t$.

Intuitively: in an accessible function passing AFSM, meta-variables of a higher type may occur only in “safe” places in the left-hand sides of rules. Rules like the ones in Ex. 7, where a higher-order meta-variable is lifted out of a base-type term, are not admitted (unless the base type is greater than the higher type).

In the remainder of this paper, we will refer to a properly applied, accessible function passing AFSM as a PA-AFP AFSM.

Discussion: This definition is strictly more liberal than the notions of “plain function passing” in both [34] and [46] as adapted to AFSMs. The notion in [46] largely corresponds to AFP if $\succeq^{\mathcal{S}}$ equates all sorts, and the HRS formalism guarantees that rules are properly applied (in fact, all fully applied sub-meta-terms of both left- and right-hand sides of rules have base type). The notion in [34] is more restrictive. The current restriction of PA-AFP AFSMs lets us handle examples like ordinal recursion (Ex. 2) which are not covered by [34, 46]. However, note that [34, 46] consider a different formalism, which does take rules whose left-hand side is not a pattern into account (which we do not consider). Our restriction also quite resembles the “admissible” rules in [6] which are defined using a pattern computability closure [5], but that work carries additional restrictions.

In later work [32, 33], K. Kusakari extends the static DP approach to forms of polymorphic functional programming, with a very liberal restriction: the definition is parametrised with an arbitrary RC-set and corresponding accessibility (“safety”) notion. Our AFP restriction is actually an instance of this condition (although a more liberal one than the example RC-set used in [32, 33]). We have chosen a specific instance because it allows us to use dedicated techniques for the RC-set; for example, our computable subterm criterion processor (Thm. 0.C.7).

4 Static higher-order dependency pairs

To obtain sufficient criteria for both termination and non-termination of AFSMs, we will now transpose the definition of static dependency pairs [6, 34, 46, 33] to AFSMs. In addition, we will add the new features of meta-variable conditions, formative reductions, and computable chains. Complete versions of all proof sketches in this section are available in Appendix 0.B.

Although we retain the first-order terminology of dependency pairs, the setting with meta-variables makes it more suitable to define DPs as triples.

Definition 12 ((Static) Dependency Pair)

A dependency pair (DP) is a triple $\ell\Rrightarrow p\ (A)$, where $\ell$ is a closed pattern $\mathtt{f}\ \ell_{1}\cdots\ell_{k}$, $p$ is a closed meta-term $\mathtt{g}\ p_{1}\cdots p_{n}$, and $A$ is a set of meta-variable conditions: pairs $Z:i$ indicating that $Z$ regards its $i^{\text{th}}$ argument. A DP is conservative if $\mathit{FMV}(p)\subseteq\mathit{FMV}(\ell)$.

A substitution $\gamma$ respects a set of meta-variable conditions $A$ if for all $Z:i$ in $A$ we have $\gamma(Z)=\lambda x_{1}\dots x_{j}.t$ with either $i>j$, or $i\leq j$ and $x_{i}\in\mathit{FV}(t)$. DPs will be used only with substitutions that respect their meta-variable conditions.

For $\ell\Rrightarrow p\ (\emptyset)$ (so a DP whose set of meta-variable conditions is empty), we often omit the third component and just write $\ell\Rrightarrow p$.

Like the first-order setting, the static DP approach employs marked function symbols to obtain meta-terms whose instances cannot be reduced at the root.

Definition 13 (Marked symbols)

Let $(\mathcal{F},\mathcal{R})$ be an AFSM. Define $\mathcal{F}^{\sharp}:=\mathcal{F}\uplus\{\mathtt{f}^{\sharp}:\sigma\mid\mathtt{f}:\sigma\in\mathcal{D}\}$. For a meta-term $s=\mathtt{f}\ s_{1}\cdots s_{k}$ with $\mathtt{f}\in\mathcal{D}$ and $k=\mathit{minar}(\mathtt{f})$, we let $s^{\sharp}=\mathtt{f}^{\sharp}\ s_{1}\cdots s_{k}$; for $s$ of other forms $s^{\sharp}$ is not defined.

Moreover, we will consider candidates. In the first-order setting, candidate terms are subterms of the right-hand sides of rules whose root symbol is a defined symbol. Intuitively, these subterms correspond to function calls. In the current setting, we have to consider also meta-variables as well as rules whose right-hand side is not $\beta$-normal (which might arise for instance due to $\eta$-expansion).

Definition 14 ($\beta$-reduced-sub-meta-term,

$\unrhd_{\beta}$, $\unrhd_{A}$)

A meta-term $s$ has a fully applied $\beta$-reduced-sub-meta-term $t$ (shortly, BRSMT), notation $s\unrhd_{\beta}t$, if there exists a set of meta-variable conditions $A$ with $s\unrhd_{A}t$. Here $s\unrhd_{A}t$ holds if:

• •

$s=t$, or

• •

$s=\lambda x.u$ and $u\unrhd_{A}t$, or

• •

$s=(\lambda x.u)\ s_{0}\cdots s_{n}$ and some $s_{i}\unrhd_{A}t$, or $u[x:=s_{0}]\ s_{1}\cdots s_{n}\unrhd_{A}t$, or

• •

$s=a\ s_{1}\cdots s_{n}$ with $a\in\mathcal{F}\cup\mathcal{V}$ and some $s_{i}\unrhd_{A}t$, or

• •

$s=Z\langle t_{1},\dots,t_{k}\rangle\ s_{1}\cdots s_{n}$ and some $s_{i}\unrhd_{A}t$, or

• •

$s=Z\langle t_{1},\dots,t_{k}\rangle\ s_{1}\cdots s_{n}$ and $t_{i}\unrhd_{A}t$ for some $i\in\{1,\dots,k\}$ with $(Z:i)\in A$.

Essentially, $s\,\unrhd_{A}\,t$ means that $t$ can be reached from $s$ by taking $\beta$-reductions at the root and “subterm”-steps, where $Z:i$ is in $A$ whenever we pass into argument $i$ of a meta-variable $Z$. BRSMTs are used to generate candidates:

Definition 15 (Candidates)

For a meta-term $s$, the set $\mathsf{cand}(s)$ of candidates of $s$ consists of those pairs $t\ (A)$ such that (a) $t$ has the form $\mathtt{f}\ s_{1}\cdots s_{k}$ with $\mathtt{f}\in\mathcal{D}$ and $k=\mathit{minar}(\mathtt{f})$, and (b) there are $s_{k+1},\dots,s_{n}$ (with $n\geq k$) such that $s\unrhd_{A}t\ s_{k+1}\cdots s_{n}$, and (c) $A$ is minimal: there is no subset $A^{\prime}\subsetneq A$ with $s\unrhd_{A^{\prime}}t$.

Example 8

In AFSMs where all meta-variables have arity [math] and the right-hand sides of rules are $\beta$-normal, the set $\mathsf{cand}(s)$ for a meta-term $s$ consists exactly of the pairs $t\ (\emptyset)$ where $t$ has the form $\mathtt{f}\ s_{1}\cdots s_{\mathit{minar}(\mathtt{f})}$ and $t$ occurs as part of $s$. In Ex. 2, we thus have $\mathsf{cand}(G\ H\ (\lambda m.\mathtt{rec}\ (H\ m)\ K\ F\ G))=\{\,\mathtt{rec}\ (H\ m)\ K\ F\ G\ (\emptyset)\,\}$.

If some of the meta-variables do take arguments, then the meta-variable conditions matter: candidates of $s$ are pairs $t\ (A)$ where $A$ contains exactly those pairs $Z:i$ for which we pass through the $i^{\text{th}}$ argument of $Z$ to reach $t$ in $s$.

Example 9

Consider an AFSM with the signature from Ex. 2 but a rule using meta-variables with larger arities:

[TABLE]

The right-hand side has one candidate:

[TABLE]

The original static approaches define DPs as pairs $\ell^{\sharp}\Rrightarrow p^{\sharp}$ where $\ell\Rightarrow r$ is a rule and $p$ a subterm of $r$ of the form $\mathtt{f}\ r_{1}\cdots r_{m}$ – as their rules are built using terms, not meta-terms. This can set variables bound in $r$ free in $p$. In the current setting, we use candidates with their meta-variable conditions and implicit $\beta$-steps rather than subterms, and we replace such variables by meta-variables.

Definition 16 ($\mathit{SDP}$)

Let $s$ be a meta-term and $(\mathcal{F},\mathcal{R})$ be an AFSM. Let $\mathit{metafy}(s)$ denote $s$ with all free variables replaced by corresponding meta-variables. Now $\mathit{SDP}(\mathcal{R})=\{\ell^{\sharp}\Rrightarrow\mathit{metafy}(p^{\sharp})\ (A)\mid\ell\Rightarrow r\in\mathcal{R}\wedge p\ (A)\in\mathsf{cand}(r)\}$.

Although static DPs always have a pleasant form $\mathtt{f}^{\sharp}\ \ell_{1}\cdots\ell_{k}\Rrightarrow\mathtt{g}^{\sharp}\ p_{1}\cdots p_{n}\ (A)$ (as opposed to the dynamic DPs of, e.g., [31], whose right-hand sides can have a meta-variable at the head, which complicates various techniques in the framework), they have two important complications not present in first-order DPs: the right-hand side $p$ of a DP $\ell\Rrightarrow p\ (A)$ may contain meta-variables that do not occur in the left-hand side $\ell$ – traditional analysis techniques are not really equipped for this – and the left- and right-hand sides may have different types. In § 5 we will explore some methods to deal with these features.

Example 10

For the non-$\eta$-expanded rules of Ex. 5, the set $\mathit{SDP}(\mathcal{R})$ has one element: $\mathtt{deriv}^{\sharp}\ (\lambda x.\mathtt{sin}\ F\langle x\rangle)\Rrightarrow\mathtt{deriv}^{\sharp}\ (\lambda x.F\langle x\rangle)$. (As $\mathtt{times}$ and $\mathtt{cos}$ are not defined symbols, they do not generate dependency pairs.) The set $\mathit{SDP}(\mathcal{R}^{\uparrow})$ for the $\eta$-expanded rules is $\{\mathtt{deriv}^{\sharp}\ (\lambda x.\mathtt{sin}\ F\langle x\rangle)\ Y\Rrightarrow\mathtt{deriv}^{\sharp}\ (\lambda x.F\langle x\rangle)\ Y\}$. To obtain the relevant candidate, we used the $\beta$-reduction step of BRSMTs.

Example 11

The AFSM from Ex. 2 is AFP following Ex. 6; here $\mathit{SDP}(\mathcal{R})$ is:

[TABLE]

Note that the right-hand side of the second DP contains a meta-variable that is not on the left. As we will see in Ex. 26, that is not problematic here.

Termination analysis using dependency pairs importantly considers the notion of a dependency chain. This notion is fairly similar to the first-order setting:

Definition 17 (Dependency chain)

Let $\mathcal{P}$ be a set of DPs and $\mathcal{R}$ a set of rules. A (finite or infinite) $(\mathcal{P},\mathcal{R})$-dependency chain (or just $(\mathcal{P},\mathcal{R})$-chain) is a sequence $[(\ell_{0}\Rrightarrow p_{0}\ (A_{0}),s_{0},t_{0}),(\ell_{1}\Rrightarrow p_{1}\ (A_{1}),s_{1},t_{1}),\ldots]$ where each $\ell_{i}\Rrightarrow p_{i}\ (A_{i})\in\mathcal{P}$ and all $s_{i},t_{i}$ are terms, such that for all $i$:

there exists a substitution $\gamma$ on domain $\mathit{FMV}(\ell_{i})\cup\mathit{FMV}(p_{i})$ such that $s_{i}=\ell_{i}\gamma,\ t_{i}=p_{i}\gamma$ and for all $Z\in\mathtt{dom}(\gamma)$: $\gamma(Z)$ respects $A_{i}$; 2. 2.

we can write $t_{i}=\mathtt{f}\ u_{1}\cdots u_{n}$ and $s_{i+1}=\mathtt{f}\ w_{1}\cdots w_{n}$ and each $u_{j}\Rightarrow_{\mathcal{R}}^{*}w_{j}$.

Example 12

In the (first) AFSM from Ex. 1, we have $\mathit{SDP}(\mathcal{R})=\{\mathtt{map}^{\sharp}\ (\lambda x.Z\langle x\rangle)\linebreak(\mathtt{cons}\ H\ T)\Rrightarrow\mathtt{map}^{\sharp}\ (\lambda x.Z\langle x\rangle)\ T\}$. An example of a finite dependency chain is $[(\rho,s_{1},t_{1}),(\rho,s_{2},t_{2})]$ where $\rho$ is the one DP, $s_{1}=\mathtt{map}^{\sharp}\ (\lambda x.\mathtt{s}\ x)\ (\mathtt{cons}\ \mathtt{0}\ (\mathtt{cons}\ (\mathtt{s}\ \mathtt{0})\ \linebreak(\mathtt{map}\ (\lambda x.x)\ \mathtt{nil})))$ and $t_{1}=\mathtt{map}^{\sharp}\ (\lambda x.\mathtt{s}\ x)\ (\mathtt{cons}\ (\mathtt{s}\ \mathtt{0})\ (\mathtt{map}\ (\lambda x.x)\ \mathtt{nil}))$ and $s_{2}=\mathtt{map}^{\sharp}\ (\lambda x.\mathtt{s}\ x)\ (\mathtt{cons}\ (\mathtt{s}\ \mathtt{0})\ \mathtt{nil})$ and $t_{2}=\mathtt{map}^{\sharp}\ (\lambda x.\mathtt{s}\ x)\ \mathtt{nil}$.

Note that here $t_{1}$ reduces to $s_{2}$ in a single step ($\mathtt{map}\ (\lambda x.x)\ \mathtt{nil}\Rightarrow_{\mathcal{R}}\mathtt{nil}$).

We have the following key result:

Theorem 4.1

Let $(\mathcal{F},\mathcal{R})$ be a PA-AFP AFSM. If $(\mathcal{F},\mathcal{R})$ is non-terminating, then there is an infinite $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chain.

Proof (sketch)

The proof is an adaptation of the one in [34], altered for the more permissive definition of accessible function passing over plain function passing as well as the meta-variable conditions; it also follows from Thm. 0.B.3 below. ∎

By this result we can use dependency pairs to prove termination of a given properly applied and AFP AFSM: if we can prove that there is no infinite $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-chain, then termination follows immediately. Note, however, that the reverse result does not hold: it is possible to have an infinite $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chain even for a terminating PA-AFP AFSM.

Example 13

Let $\mathcal{F}\supseteq\{\mathtt{0},\mathtt{1}:\mathtt{nat}$, $\mathtt{f}:\mathtt{nat}\rightarrow\mathtt{nat}$, $\mathtt{g}:(\mathtt{nat}\rightarrow\mathtt{nat})\rightarrow\mathtt{nat}\}$ and $\mathcal{R}=\{\mathtt{f}\ \mathtt{0}\Rightarrow\mathtt{g}\ (\lambda x.\mathtt{f}\ x),\mathtt{g}\ (\lambda x.F\langle x\rangle)\Rightarrow F\langle\mathtt{1}\rangle\}$. This AFSM is PA-AFP, with $\mathit{SDP}(\mathcal{R})=\{\mathtt{f}^{\sharp}\ \mathtt{0}\Rrightarrow\mathtt{g}^{\sharp}\ (\lambda x.\mathtt{f}\ x),\ \mathtt{f}^{\sharp}\ \mathtt{0}\Rrightarrow\mathtt{f}^{\sharp}\ X\}$; the second rule does not cause the addition of any dependency pairs. Although $\Rightarrow_{\mathcal{R}}$ is terminating, there is an infinite $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-chain $[(\mathtt{f}^{\sharp}\ \mathtt{0}\Rrightarrow\mathtt{f}^{\sharp}\ X,\mathtt{f}^{\sharp}\ \mathtt{0},\mathtt{f}^{\sharp}\ \mathtt{0}),(\mathtt{f}^{\sharp}\ \mathtt{0}\Rrightarrow\mathtt{f}^{\sharp}\ X,\mathtt{f}^{\sharp}\ \mathtt{0},\mathtt{f}^{\sharp}\ \mathtt{0}),\ldots]$.

The problem in Ex. 13 is the non-conservative DP $\mathtt{f}^{\sharp}\ \mathtt{0}\Rrightarrow\mathtt{f}^{\sharp}\ X$, with $X$ on the right but not on the left. Such DPs arise from abstractions in the right-hand sides of rules. Unfortunately, abstractions are introduced by the restricted $\eta$-expansion (Def. 10) that we may need to make an AFSM properly applied. Even so, often all DPs are conservative, like Ex. 1 and 5. There, we do have the inverse result:

Theorem 4.2

For any AFSM $(\mathcal{F},\mathcal{R})$: if there is an infinite $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-chain $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ with all $\rho_{i}$ conservative, then $\Rightarrow_{\mathcal{R}}$ is non-terminating.

Proof (sketch)

If $\mathit{FMV}(p_{i})\subseteq\mathit{FMV}(\ell_{i})$, then we can see that $s_{i}\Rightarrow_{\mathcal{R}}\cdot\Rightarrow_{\beta}^{*}t_{i}^{\prime}$ for some term $t_{i}^{\prime}$ of which $t_{i}$ is a subterm. Since also each $t_{i}\Rightarrow_{\mathcal{R}}^{*}s_{i+1}$, the infinite chain induces an infinite reduction $s_{0}\Rightarrow_{\mathcal{R}}^{+}t_{0}^{\prime}\Rightarrow_{\mathcal{R}}^{*}s_{1}^{\prime}\Rightarrow_{\mathcal{R}}^{+}t_{1}^{\prime\prime}\Rightarrow_{\mathcal{R}}^{*}\dots$. ∎

The core of the dependency pair framework is to systematically simplify a set of pairs $(\mathcal{P},\mathcal{R})$ to prove either absence or presence of an infinite $(\mathcal{P},\mathcal{R})$-chain, thus showing termination or non-termination as appropriate. By Theorems 4.1 and 0.B.2 we can do so, although with some conditions on the non-termination result. We can do better by tracking certain properties of dependency chains.

Definition 18 (Minimal and Computable chains)

Let $(\mathcal{F},{\mathcal{U}})$ be an AFSM and $C_{{\mathcal{U}}}$ an RC-set satisfying the properties of Thm. 2.2 for $(\mathcal{F},{\mathcal{U}})$. Let $\mathcal{F}$ contain, for every type $\sigma$, at least countably many symbols $\mathtt{f}:\sigma$ not used in ${\mathcal{U}}$.

A $(\mathcal{P},\mathcal{R})$-chain $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ is ${\mathcal{U}}$-computable if: $\Rightarrow_{{\mathcal{U}}}\mathop{\supseteq}\Rightarrow_{\mathcal{R}}$, and for all $i\in\mathbb{N}$ there exists a substitution $\gamma_{i}$ such that $\rho_{i}=\ell_{i}\Rrightarrow p_{i}\ (A_{i})$ with $s_{i}=\ell_{i}\gamma_{i}$ and $t_{i}=p_{i}\gamma_{i}$, and $(\lambda x_{1}\dots x_{n}.v)\gamma_{i}$ is $C_{{\mathcal{U}}}$-computable for all $v$ and $B$ such that $p_{i}\unrhd_{B}v$, $\gamma_{i}$ respects $B$, and $\mathit{FV}(v)=\{x_{1},\dots,x_{n}\}$.

A chain is minimal if the strict subterms of all $t_{i}$ are terminating under $\Rightarrow_{\mathcal{R}}$.

In the first-order DP framework, minimal chains give access to several powerful techniques to prove absence of infinite chains, such as the subterm criterion [24] and usable rules [22, 24]. Computable chains go a step further, by building on the computability inherent in the proof of Thm. 4.1 and the notion of accessible function passing AFSMs. In computable chains, we can require that (some of) the subterms of all $t_{i}$ are computable rather than merely terminating. This property will be essential in the computable subterm criterion processor (Thm. 0.C.7).

Another property of dependency chains is the use of formative rules, which has proven very useful for dynamic DPs [31]. Here we go further and consider formative reductions, which were introduced for the first-order DP framework in [16]. This property will be essential in the formative rules processor (Thm. 0.C.5).

Definition 19 (Formative chain, formative reduction)

A $(\mathcal{P},\mathcal{R})$-chain $[(\ell_{0}\Rrightarrow p_{0}\ (A_{0}),s_{0},t_{0}),(\ell_{1}\Rrightarrow p_{1}\ (A_{1}),s_{1},t_{1}),\ldots]$ is formative if for all $i$, the reduction $t_{i}\Rightarrow_{\mathcal{R}}^{*}s_{i+1}$ is $\ell_{i+1}$-formative. Here, for a pattern $\ell$, substitution $\gamma$ and term $s$, a reduction $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ is $\ell$-formative if one of the following holds:

• •

$\ell$ is not a fully extended linear pattern; that is: some meta-variable occurs more than once in $\ell$ or $\ell$ has a sub-meta-term $\lambda x.C[Z\langle\vec{s}\rangle]$ with $x\notin\{\vec{s}\}$

• •

$\ell$ is a meta-variable application $Z\langle x_{1},\dots,x_{k}\rangle$ and $s=\ell\gamma$

• •

$s=a\ s_{1}\cdots s_{n}$ and $\ell=a\ \ell_{1}\cdots\ell_{n}$ with $a\in\mathcal{F}^{\sharp}\cup\mathcal{V}$ and each $s_{i}\Rightarrow_{\mathcal{R}}^{*}\ell_{i}\gamma$ by an $\ell_{i}$-formative reduction

• •

$s=\lambda x.s^{\prime}$ and $\ell=\lambda x.\ell^{\prime}$ and $s^{\prime}\Rightarrow_{\mathcal{R}}^{*}\ell^{\prime}\gamma$ by an $\ell^{\prime}$-formative reduction

• •

$s=(\lambda x.u)\ v\ w_{1}\cdots w_{n}$ and $u[x:=v]\ w_{1}\cdots w_{n}\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ by an $\ell$-formative reduction

• •

$\ell$ is not a meta-variable application, and there are $\ell^{\prime}\Rightarrow r^{\prime}\in\mathcal{R}$, meta-variables $Z_{1}\dots Z_{n}$ ($n\geq 0$) and $\delta$ such that $s\Rightarrow_{\mathcal{R}}^{*}(\ell^{\prime}\ Z_{1}\cdots Z_{n})\delta$ by an $(\ell^{\prime}\ Z_{1}\cdots Z_{n})$-formative reduction, and $(r^{\prime}\ Z_{1}\cdots Z_{n})\delta\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ by an $\ell$-formative reduction.

The idea of a formative reduction is to avoid redundant steps: if $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ by an $\ell$-formative reduction, then this reduction takes only the steps needed to obtain an instance of $\ell$. Suppose that we have rules $\mathtt{plus}\ \mathtt{0}\ Y\Rightarrow Y,\ \mathtt{plus}\ (\mathtt{s}\ X)\ Y\Rightarrow\mathtt{s}\ (\mathtt{plus}\ X\ Y)$. Let $\ell:=\mathtt{g}\ \mathtt{0}\ X$ and $t:=\mathtt{plus}\ \mathtt{0}\ \mathtt{0}$. Then the reduction $\mathtt{g}\ t\ t\Rightarrow_{\mathcal{R}}\mathtt{g}\ \mathtt{0}\ t$ is $\ell$-formative: we must reduce the first argument to get an instance of $\ell$. The reduction $\mathtt{g}\ t\ t\Rightarrow_{\mathcal{R}}\mathtt{g}\ t\ \mathtt{0}\Rightarrow_{\mathcal{R}}\mathtt{g}\ \mathtt{0}\ \mathtt{0}$ is not $\ell$-formative, because the reduction in the second argument does not contribute to the non-meta-variable positions of $\ell$. This matters when we consider $\ell$ as the left-hand side of a rule, say $\mathtt{g}\ \mathtt{0}\ X\Rightarrow\mathtt{0}$: if we reduce $\mathtt{g}\ t\ t\Rightarrow_{\mathcal{R}}\mathtt{g}\ t\ \mathtt{0}\Rightarrow_{\mathcal{R}}\mathtt{g}\ \mathtt{0}\ \mathtt{0}\Rightarrow_{\mathcal{R}}\mathtt{0}$, then the first step was redundant: removing this step gives a shorter reduction to the same result: $\mathtt{g}\ t\ t\Rightarrow_{\mathcal{R}}\mathtt{g}\ \mathtt{0}\ t\Rightarrow_{\mathcal{R}}\mathtt{0}$. In an infinite reduction, redundant steps may also be postponed indefinitely.

We can now strengthen the result of Thm. 4.1 with two new properties.

Theorem 4.3

Let $(\mathcal{F},\mathcal{R})$ be a properly applied, accessible function passing AFSM. If $(\mathcal{F},\mathcal{R})$ is non-terminating, then there is an infinite $\mathcal{R}$-computable formative $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chain.

Proof (sketch)

We select a minimal non-computable (MNC) term $s:=\mathtt{f}\ s_{1}\cdots s_{k}$ (where all $s_{i}$ are $C_{\mathcal{R}}$-computable) and an infinite reduction starting in $s$. Then we stepwise build an infinite dependency chain, as follows. Since $s$ is non-computable but each $s_{i}$ terminates (as computability implies termination), there exist a rule $\mathtt{f}\ \ell_{1}\cdots\ell_{k}\Rightarrow r$ and substitution $\gamma$ such that each $s_{i}\Rightarrow_{\mathcal{R}}^{*}\ell_{i}\gamma$ and $r\gamma$ is non-computable. We can then identify a candidate $t\ (A)$ of $r$ such that $\gamma$ respects $A$ and $t\gamma$ is a MNC subterm of $r\gamma$; we continue the process with $t\gamma$ (or a term at its head). For the formative property, we note that if $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ and $u$ is terminating, then $u\Rightarrow_{\mathcal{R}}^{*}\ell\delta$ by an $\ell$-formative reduction for substitution $\delta$ such that each $\delta(Z)\Rightarrow_{\mathcal{R}}^{*}\gamma(Z)$. This follows by postponing those reduction steps not needed to obtain an instance of $\ell$. The resulting infinite chain is $\mathcal{R}$-computable because we can show, by induction on the definition of $\unrhd_{\mathtt{acc}}$, that if $\ell\Rightarrow r$ is an AFP rule and $\ell\gamma$ is a MNC term, then $\gamma(Z)$ is $C_{\mathcal{R}}$-computable for all $Z\in\mathit{FMV}(r)$. ∎

As it is easily seen that all $C_{{\mathcal{U}}}$-computable terms are $\Rightarrow_{{\mathcal{U}}}$-terminating and therefore $\Rightarrow_{\mathcal{R}}$-terminating, every ${\mathcal{U}}$-computable $(\mathcal{P},\mathcal{R})$-dependency chain is also minimal. The notions of $\mathcal{R}$-computable and formative chains still do not suffice to obtain a true inverse result, however (i.e., to prove that termination implies the absence of an infinite $\mathcal{R}$-computable chain over $\mathit{SDP}(\mathcal{R})$): the infinite chain in Ex. 13 is $\mathcal{R}$-computable.

To see why the two restrictions that the AFSM must be properly applied and accessible function passing are necessary, consider the following examples.

Example 14

Consider $\mathcal{F}\supseteq\{\mathtt{fix}:((\mathtt{o}\rightarrow\mathtt{o})\rightarrow\mathtt{o}\rightarrow\mathtt{o})\rightarrow\mathtt{o}\rightarrow\mathtt{o}\}$ and $\mathcal{R}=\{\mathtt{fix}\ F\ X\Rightarrow F\ (\mathtt{fix}\ F)\ X\}$. This AFSM is not properly applied; it is also not terminating, as can be seen by instantiating $F$ with $\lambda y.y$. However, it does not have any static DPs, since $\mathtt{fix}\ F$ is not a candidate. Even if we altered the definition of static DPs to admit a dependency pair $\mathtt{fix}^{\sharp}\ F\ X\Rrightarrow\mathtt{fix}^{\sharp}\ F$, this pair could not be used to build an infinite dependency chain.

Note that the problem does not arise if we study the $\eta$-expanded rules $\mathcal{R}^{\uparrow}=\{\mathtt{fix}\ F\ X\Rightarrow F\ (\lambda z.\mathtt{fix}\ F\ z)\ X\}$, as the dependency pair $\mathtt{fix}^{\sharp}\ F\ X\Rrightarrow\mathtt{fix}^{\sharp}\ F\ Z$ does admit an infinite chain. Unfortunately, as the one dependency pair does not satisfy the conditions of Thm. 0.B.2, we cannot use this to prove non-termination.

Example 15

The AFSM from Ex. 7 is not accessible function passing, since $\mathit{Acc}(\mathtt{lm})=\emptyset$. This is good because the set $\mathit{SDP}(\mathcal{R})$ is empty, which would lead us to falsely conclude termination without the restriction.

Discussion: Thm. 0.B.3 transposes the work of [34, 46] to AFSMs and extends it by using a more liberal restriction, by limiting interest to formative, $\mathcal{R}$-computable chains, and by including meta-variable conditions. Both of these new properties of chains will support new termination techniques within the DP framework.

The relationship with the works for functional programming [32, 33] is less clear: they define a different form of chains suited well to polymorphic systems, but which requires more intricate reasoning for non-polymorphic systems, as DPs can be used for reductions at the head of a term. It is not clear whether there are non-polymorphic systems that can be handled with one and not the other. The notions of formative and $\mathcal{R}$-computable chains are not considered there; meta-variable conditions are not relevant to their $\lambda$-free formalism.

5 The static higher-order DP framework

In first-order term rewriting, the DP framework [20] is an extendable framework to prove termination and non-termination. As observed in the introduction, DP analyses in higher-order rewriting typically go beyond the initial DP approach [2], but fall short of the full framework. Here, we define the latter for static DPs. Complete versions of all proof sketches in this section are available in Appendix 0.C.

We have now reduced the problem of termination to non-existence of certain chains. In the DP framework, we formalise this in the notion of a DP problem:

Definition 20 (DP problem)

A DP problem is a tuple $(\mathcal{P},\mathcal{R},m,f)$ with $\mathcal{P}$ a set of DPs, $\mathcal{R}$ a set of rules, $m\in\{\mathtt{minimal},\mathtt{arbitrary}\}\cup\{\mathtt{computable}_{\mathcal{U}}\mid\text{any set of rules}\ {\mathcal{U}}\}$, and $f\in\{\mathtt{formative},\mathtt{all}\}$.333Our framework is implicitly parametrised by the signature $\mathcal{F}^{\sharp}$ used for term formation. As none of the processors we present modify this component (as indeed there is no need to by Thm. 2.1), we leave it implicit.

A DP problem $(\mathcal{P},\mathcal{R},m,f)$ is finite if there exists no infinite $(\mathcal{P},\mathcal{R})$-chain that is ${\mathcal{U}}$-computable if $m=\mathtt{computable}_{\mathcal{U}}$, is minimal if $m=\mathtt{minimal}$, and is formative if $f=\mathtt{formative}$. It is infinite if $\mathcal{R}$ is non-terminating, or if there exists an infinite $(\mathcal{P},\mathcal{R})$-chain where all DPs used in the chain are conservative.

To capture the levels of permissiveness in the $m$ flag, we use a transitive-reflexive relation $\succeq$ generated by $\mathtt{computable}_{{\mathcal{U}}}\succeq\mathtt{minimal}\succeq\mathtt{arbitrary}$.

Thus, the combination of Theorems 0.B.3 and 0.B.2 can be rephrased as: an AFSM $(\mathcal{F},\mathcal{R})$ is terminating if $(\mathit{SDP}(\mathcal{R}),\mathcal{R},\mathtt{computable}_{\mathcal{R}},\mathtt{formative})$ is finite, and is non-terminating if $(\mathit{SDP}(\mathcal{R}),\mathcal{R},m,f)$ is infinite for some $m\in\{\mathtt{computable}_{\mathcal{U}},\mathtt{minimal},\mathtt{arbitrary}\}$ and $f\in\{\mathtt{formative},\mathtt{all}\}$.444The processors in this paper do not alter the flag $m$, but some require minimality or computability. We include the $\mathtt{minimal}$ option and the subscript ${\mathcal{U}}$ for the sake of future generalisations, and for reuse of processors in the dynamic approach of [31].

The core idea of the DP framework is to iteratively simplify a set of DP problems via processors until nothing remains to be proved:

Definition 21 (Processor)

A dependency pair processor (or just processor) is a function that takes a DP problem and returns either NO or a set of DP problems. A processor $\mathit{Proc}$ is sound if a DP problem $M$ is finite whenever $\mathit{Proc}(M)\neq\texttt{NO}$ and all elements of $\mathit{Proc}(M)$ are finite. A processor $\mathit{Proc}$ is complete if a DP problem $M$ is infinite whenever $\mathit{Proc}(M)=\texttt{NO}$ or contains an infinite element.

To prove finiteness of a DP problem $M$ with the DP framework, we proceed analogously to the first-order DP framework [22]: we repeatedly apply sound DP processors starting from $M$ until none remain. That is, we execute the following rough procedure: (1) let $A:=\{M\}$; (2) while $A\neq\emptyset$: select a problem $Q\in A$ and a sound processor $\mathit{Proc}$ with $\mathit{Proc}(Q)\neq\texttt{NO}$, and let $A:=(A\setminus\{Q\})\cup\mathit{Proc}(Q)$. If this procedure terminates, then $M$ is a finite DP problem.

To prove termination of an AFSM $(\mathcal{F},\mathcal{R})$, we would use as initial DP problem $(\mathit{SDP}(\mathcal{R}),\mathcal{R},\mathtt{computable}_{\mathcal{R}},\mathtt{formative})$, provided that $\mathcal{R}$ is properly applied and accessible function passing (where $\eta$-expansion following Def. 10 may be applied first). If the procedure terminates – so finiteness of $M$ is proved by the definition of soundness – then Thm. 0.B.3 provides termination of $\Rightarrow_{\mathcal{R}}$.

Similarly, we can use the DP framework to prove infiniteness: (1) let $A:=\{M\}$; (2) while $A\neq\texttt{NO}$: select a problem $Q\in A$ and a complete processor $\mathit{Proc}$, and let $A:=\texttt{NO}$ if $\mathit{Proc}(Q)=\texttt{NO}$, or $A:=(A\setminus\{Q\})\cup\mathit{Proc}(Q)$ otherwise. For non-termination of $(\mathcal{F},\mathcal{R})$, the initial DP problem should be $(\mathit{SDP}(\mathcal{R}),\mathcal{R},m,f)$, where $m,f$ can be any flag (see Thm. 0.B.2). Note that the algorithms coincide while processors are used that are both sound and complete. In a tool, automation (or the user) must resolve the non-determinism and select suitable processors.

Below, we will present a number of processors within the framework. We will typically present processors by writing “for a DP problem $M$ satisfying $X$, $Y$, $Z$, $\mathit{Proc}(M)=\dots$”. In these cases, we let $\mathit{Proc}(M)=\{M\}$ for any problem $M$ not satisfying the given properties. Many more processors are possible, but we have chosen to present a selection which touches on all aspects of the DP framework:

• •

processors which map a DP problem to NO (Thm. 5.8), a singleton set (most processors) and a non-singleton set (Thm. 22);

• •

changing the set $\mathcal{R}$ (Thm. 0.C.5, 5.4) and various flags (Thm. 5.4);

• •

using specific values of the $f$ (Thm. 0.C.5) and $m$ flags (Thm. 0.C.6, 5.4, 0.C.7);

• •

using term orderings (Thm. 0.C.2, 0.C.3), a key part of many termination proofs.

5.1 The dependency graph

We can leverage reachability information to decompose DP problems. In first-order rewriting, a graph structure is used to track which DPs can possibly follow one another in a chain [2]. Here, we define this dependency graph as follows.

Definition 22 (Dependency graph)

A DP problem $(\mathcal{P},\mathcal{R},m,f)$ induces a graph structure $\mathit{DG}$, called its dependency graph, whose nodes are the elements of $\mathcal{P}$. There is a (directed) edge from $\rho_{1}$ to $\rho_{2}$ in $\mathit{DG}$ iff there exist $s_{1},t_{1},s_{2},t_{2}$ such that $[(\rho_{1},s_{1},t_{1}),(\rho_{2},s_{2},t_{2})]$ is a $(\mathcal{P},\mathcal{R})$-chain with the properties for $m,f$.

Example 16

Consider an AFSM with $\mathcal{F}\supseteq\{\mathtt{f}:(\mathtt{nat}\rightarrow\mathtt{nat})\rightarrow\mathtt{nat}\rightarrow\mathtt{nat}\}$ and $\mathcal{R}=\{\mathtt{f}\ (\lambda x.F\langle x\rangle)\ (\mathtt{s}\ Y)\Rightarrow F\langle\mathtt{f}\ (\lambda x.\mathtt{0})\ (\mathtt{f}\ (\lambda x.F\langle x\rangle)\ Y)\rangle\}$. Let $\mathcal{P}:=\mathit{SDP}(\mathcal{R})=$

[TABLE]

The dependency graph of $(\mathcal{P},\mathcal{R},\mathtt{minimal},\mathtt{formative})$ is:

(1)$$(2)

There is no edge from (1) to itself or (2) because there is no substitution $\gamma$ such that $(\lambda x.\mathtt{0})\gamma$ can be reduced to a term $(\lambda x.F\langle x\rangle)\delta$ where $\delta(F)$ regards its first argument (as $\Rightarrow_{\mathcal{R}}^{*}$ cannot introduce new variables).

In general, the dependency graph for a given DP problem is undecidable, which is why we consider approximations.

Definition 23 (Dependency graph approximation [31])

A finite graph $G_{\theta}$ approximates $\mathit{DG}$ if $\theta$ is a function that maps the nodes of $\mathit{DG}$ to the nodes of $G_{\theta}$ such that, whenever $\mathit{DG}$ has an edge from $\rho_{1}$ to $\rho_{2}$, $G_{\theta}$ has an edge from $\theta(\rho_{1})$ to $\theta(\rho_{2})$. ($G_{\theta}$ may have edges that have no corresponding edge in $\mathit{DG}$.)

Note that this definition allows for an infinite graph to be approximated by a finite one; infinite graphs may occur if $\mathcal{R}$ is infinite (e.g., the union of all simply-typed instances of polymorphic rules).

If $\mathcal{P}$ is finite, we can take a graph approximation $G_{\mathtt{id}}$ with the same nodes as $\mathit{DG}$. A simple approximation may have an edge from $\ell_{1}\Rrightarrow p_{1}\ (A_{1})$ to $\ell_{2}\Rrightarrow p_{2}\ (A_{2})$ whenever both $p_{1}$ and $\ell_{2}$ have the form $\mathtt{f}^{\sharp}\ s_{1}\cdots s_{k}$ for the same $\mathtt{f}$ and $k$. However, one can also take the meta-variable conditions into account, as we did in Ex. 16.

Theorem 5.1 (Dependency graph processor)

The processor $\mathit{Proc}_{G_{\theta}}$ that maps a DP problem $M=(\mathcal{P},\mathcal{R},m,f)$ to $\{(\{\rho\in\mathcal{P}\mid\theta(\rho)\in C_{i}\},\mathcal{R},m,f)\mid 1\leq i\leq n\}$ if $G_{\theta}$ is an approximation of the dependency graph of $M$ and $C_{1},\dots,C_{n}$ are the (nodes of the) non-trivial strongly connected components (SCCs) of $G_{\theta}$, is both sound and complete.

Proof (sketch)

In an infinite $(\mathcal{P},\mathcal{R})$-chain $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$, there is always a path from $\rho_{i}$ to $\rho_{i+1}$ in DG. Since $G_{\theta}$ is finite, every infinite path in $DG$ eventually remains in a cycle in $G_{\theta}$. This cycle is part of an SCC. ∎

Example 17

Let $\mathcal{R}$ be the set of rules from Ex. 16 and $G$ be the graph given there. Then $\mathit{Proc}_{G}(\mathit{SDP}(\mathcal{R}),\mathcal{R},\mathtt{computable}_{\mathcal{R}},\mathtt{formative})=\{(\{\mathtt{f}^{\sharp}\ (\lambda x.F\langle x\rangle)\ (\mathtt{s}\ Y)\Rrightarrow\mathtt{f}^{\sharp}\ (\lambda x.F\langle x\rangle)\ Y\ (\{F:1\})\},\mathcal{R},\mathtt{computable}_{\mathcal{R}},\mathtt{formative})\}$.

Example 18

Let $\mathcal{R}$ consist of the rules for $\mathtt{map}$ from Ex. 1 along with $\mathtt{f}\ L\Rightarrow\mathtt{map}\ (\lambda x.\mathtt{g}\ x)\ L$ and $\mathtt{g}\ X\Rightarrow X$. Then \mathit{SDP}(\mathcal{R})=\{(1)\ \mathtt{map}^{\sharp}\ (\lambda x.Z\langle x\rangle)\ (\mathtt{cons}\ H\ T)$$\Rrightarrow\mathtt{map}^{\sharp}\ (\lambda x.Z\langle x\rangle)\ T,\ (2)\ \mathtt{f}^{\sharp}\ L\Rrightarrow\mathtt{map}^{\sharp}\ (\lambda x.\mathtt{g}\ x)\ L,\ (3)\ \mathtt{f}^{\sharp}\ L\Rrightarrow\mathtt{g}^{\sharp}\ X\}. DP (3) is not conservative, but it is not on any cycle in the graph approximation $G_{\mathtt{id}}$ obtained by considering head symbols as described above:

(3)$$(2)$$(1)

As $(1)$ is the only DP on a cycle, $\mathit{Proc}_{\mathit{SDP}_{G_{\mathtt{id}}}}(\mathit{SDP}(\mathcal{R}),\mathcal{R},\mathtt{computable}_{\mathcal{R}},\linebreak\mathtt{formative})=\{\ (\{(1)\},\mathcal{R},\mathtt{computable}_{\mathcal{R}},\mathtt{formative})\ \}$.

Discussion: The dependency graph is a powerful tool for simplifying DP problems, used since early versions of the DP approach [2]. Our notion of a dependency graph approximation, taken from [31], strictly generalises the original notion in [2], which uses a graph on the same node set as $DG$ with possibly further edges. One can get this notion here by using a graph $G_{\mathtt{id}}$. The advantage of our definition is that it ensures soundness of the dependency graph processor also for infinite sets of DPs. This overcomes a restriction in the literature [34, Corollary 5.13] to dependency graphs without non-cyclic infinite paths.

5.2 Processors based on reduction triples

At the heart of most DP-based approaches to termination proving lie well-founded orderings to delete DPs (or rules). For this, we use reduction triples [24, 31].

Definition 24 (Reduction triple)

A reduction triple $(\succsim,\succcurlyeq,\succ)$ consists of two quasi-orderings $\succsim$ and $\succcurlyeq$ and a well-founded strict ordering $\succ$ on meta-terms such that $\succsim$ is monotonic, all of $\succsim,\succcurlyeq,\succ$ are meta-stable (that is, $\ell\succsim r$ implies $\ell\gamma\succsim r\gamma$ if $\ell$ is a closed pattern and $\gamma$ a substitution on domain $\mathit{FMV}(\ell)\cup\mathit{FMV}(r)$, and the same for $\succcurlyeq$ and $\succ$), $\Rightarrow_{\beta}\mathop{\subseteq}\succsim$, and both $\succsim\circ\succ\mathop{\subseteq}\succ$ and $\succcurlyeq\circ\succ\mathop{\subseteq}\succ$.

In the first-order DP framework, the reduction pair processor [20] seeks to orient all rules with $\succsim$ and all DPs with either $\succsim$ or $\succ$; if this succeeds, those pairs oriented with $\succ$ may be removed. Using reduction triples rather than pairs, we obtain the following extension to the higher-order setting:

Theorem 5.2 (Basic reduction triple processor)

Let $M=(\mathcal{P}_{1}\uplus\mathcal{P}_{2},\mathcal{R},m,\linebreak f)$ be a DP problem. If $(\succsim,\succcurlyeq,\succ)$ is a reduction triple such that

for all $\ell\Rightarrow r\in\mathcal{R}$, we have $\ell\succsim r$; 2. 2.

for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$, we have $\ell\succ p$; 3. 3.

for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{2}$, we have $\ell\succcurlyeq p$;

then the processor that maps $M$ to $\{(\mathcal{P}_{2},\mathcal{R},m,f)\}$ is both sound and complete.

Proof (sketch)

For an infinite $(\mathcal{P}_{1}\uplus\mathcal{P}_{2},\mathcal{R})$-chain $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ the requirements provide that, for all $i$: (a) $s_{i}\succ t_{i}$ if $\rho_{i}\in\mathcal{P}_{1}$; (b) $s_{i}\succcurlyeq t_{i}$ if $\rho_{i}\in\mathcal{P}_{2}$; and (c) $t_{i}\succsim s_{i+1}$. Since $\succ$ is well-founded, only finitely many DPs can be in $\mathcal{P}_{1}$, so a tail of the chain is actually an infinite $(\mathcal{P}_{2},\mathcal{R},m,f)$-chain. ∎

Example 19

Let $(\mathcal{F},\mathcal{R})$ be the (non-$\eta$-expanded) rules from Ex. 5, and $\mathit{SDP}(\mathcal{R})$ the DPs from Ex. 10. From Thm. 0.C.2, we get the following ordering requirements:

[TABLE]

We can handle both requirements by using a polynomial interpretation $\mathcal{J}$ to $\mathbb{N}$ [43, 15], by choosing $\mathcal{J}_{\mathtt{sin}}(n)=n+1$, $\mathcal{J}_{\mathtt{cos}}(n)=0$, $\mathcal{J}_{\mathtt{times}}(n_{1},n_{2})=n_{1}$, $\mathcal{J}_{\mathtt{deriv}}(f)=\mathcal{J}_{\mathtt{deriv}^{\sharp}}(f)=\lambda n.f(n)$. Then the requirements are evaluated to: $\lambda n.f(n)+1\geq\lambda n.f(n)$ and $\lambda n.f(n)+1>\lambda n.f(n)$, which holds on $\mathbb{N}$.

Thm. 0.C.2 is not ideal since, by definition, the left- and right-hand side of a DP may have different types. Such DPs are hard to handle with traditional techniques such as HORPO [26] or polynomial interpretations [43, 15], as these methods compare only (meta-)terms of the same type (modulo renaming of sorts).

Example 20

Consider the toy AFSM with $\mathcal{R}=\{\mathtt{f}\ (\mathtt{s}\ X)\ Y\Rightarrow\mathtt{g}\ X\ Y,\ \mathtt{g}\ X\Rightarrow\lambda z.\mathtt{f}\ X\ z\}$ and $\mathit{SDP}(\mathcal{R})=\{\mathtt{f}^{\sharp}\ (\mathtt{s}\ X)\ Y\Rrightarrow\mathtt{g}^{\sharp}\ X,\ \mathtt{g}^{\sharp}\ X\Rrightarrow\mathtt{f}^{\sharp}\ X\ Z\}$. If $\mathtt{f}$ and $\mathtt{g}$ both have a type $\mathtt{nat}\rightarrow\mathtt{nat}\rightarrow\mathtt{nat}$, then in the first DP, the left-hand side has type $\mathtt{nat}$ while the right-hand side has type $\mathtt{nat}\rightarrow\mathtt{nat}$. In the second DP, the left-hand side has type $\mathtt{nat}\rightarrow\mathtt{nat}$ and the right-hand side has type $\mathtt{nat}$.

To be able to handle examples like the one above, we adapt [31, Thm. 5.21] by altering the ordering requirements to have base type.

Theorem 5.3 (Reduction triple processor)

Let $\mathsf{Bot}$ be a set $\{\bot_{\sigma}:\sigma\mid$ $\sigma\text{ a type}\}\subseteq\mathcal{F}^{\sharp}$ of unused constructors, $M=(\mathcal{P}_{1}\uplus\mathcal{P}_{2},\mathcal{R},m,f)$ a DP problem and $(\succsim,\succcurlyeq,\succ)$ a reduction triple such that: (a) for all $\ell\Rightarrow r\in\mathcal{R}$, we have $\ell\succsim r$; and (b) for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}\uplus\mathcal{P}_{2}$ with $\ell:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ and $p:\tau_{1}\rightarrow\dots\rightarrow\tau_{n}\rightarrow\kappa$ we have, for fresh meta-variables $Z_{1}:\sigma_{1},\dots,Z_{m}:\sigma_{m}$:

• •

$\ell\ Z_{1}\cdots Z_{m}\succ p\ \bot_{\tau_{1}}\cdots\bot_{\tau_{n}}$* if $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$*

• •

$\ell\ Z_{1}\cdots Z_{m}\succcurlyeq p\ \bot_{\tau_{1}}\cdots\bot_{\tau_{n}}$* if $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{2}$*

Then the processor that maps $M$ to $\{(\mathcal{P}_{2},\mathcal{R},m,f)\}$ is both sound and complete.

Proof (sketch)

If $(\succsim,\succcurlyeq,\succ)$ is such a triple, then for $R\in\{\succcurlyeq,\succ\}$ define $R^{\prime}$ as follows: for $s:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ and $t:\tau_{1}\rightarrow\dots\rightarrow\tau_{n}\rightarrow\kappa$, let $s\ R^{\prime}\ t$ if for all $u_{1}:\sigma_{1},\dots,u_{m}:\sigma_{m}$ there exist $w_{1}:\tau_{1},\dots,w_{n}:\tau_{n}$ such that $s\ u_{1}\cdots u_{m}\ R\ t\ w_{1}\cdots w_{n}$. Now apply Thm. 0.C.2 with the triple $(\succsim,\succcurlyeq^{\prime},\succ^{\prime})$. ∎

Here, the elements of $\mathsf{Bot}$ take the role of minimal terms for the ordering. We use them to flatten the type of the right-hand sides of ordering requirements, which makes it easier to use traditional methods to generate a reduction triple.

While $\succ$ and $\succcurlyeq$ may still have to orient meta-terms of distinct types, these are always base types, which we could collapse to a single sort. The only relation required to be monotonic, $\succsim$, regards pairs of meta-terms of the same type. This makes it feasible to apply orderings like HORPO or polynomial interpretations.

Both the basic and non-basic reduction triple processor are difficult to use for non-conservative DPs, which generate ordering requirements whose right-hand side contains a meta-variable not occurring on the left. This is typically difficult for traditional techniques, although possible to overcome, by choosing triples that do not regard such meta-variables (e.g., via an argument filtering [35, 46]):

Example 21

We apply Thm. 0.C.3 on the DP problem $(\mathit{SDP}(\mathcal{R}),\mathcal{R},\mathtt{computable}_{\mathcal{R}},\linebreak\mathtt{formative})$ of Ex. 20. This gives for instance the following ordering requirements:

[TABLE]

The right-hand side of the last DP uses a meta-variable $Z$ that does not occur on the left. As neither $\succ$ nor $\succcurlyeq$ are required to be monotonic (only $\succsim$ is), function symbols do not have to regard all their arguments. Thus, we can use a polynomial interpretation $\mathcal{J}$ to $\mathbb{N}$ with $\mathcal{J}_{\bot_{\mathtt{nat}}}=0$, $\mathcal{J}_{\mathtt{s}}(n)=n+1$ and $\mathcal{J}_{\mathtt{h}}(n_{1},n_{2})=n_{1}$ for $\mathtt{h}\in\{\mathtt{f},\mathtt{f}^{\sharp},\mathtt{g},\mathtt{g}^{\sharp}\}$. The ordering requirements then translate to $X+1\geq X$ and $\lambda y.X\geq\lambda z.X$ for the rules, and $X+1>X$ and $X\geq X$ for the DPs. All these inequalities on $\mathbb{N}$ are clearly satisfied, so we can remove the first DP. The remaining problem is quickly dispersed with the dependency graph processor.

5.3 Rule removal without search for orderings

While processors often simplify only $\mathcal{P}$, they can also simplify $\mathcal{R}$. One of the most powerful techniques in first-order DP approaches that can do this are usable rules. The idea is that for a given set $\mathcal{P}$ of DPs, we only need to consider a subset $\mathit{UR}(\mathcal{P},\mathcal{R})$ of $\mathcal{R}$. Combined with the dependency graph processor, this makes it possible to split a large term rewriting system into a number of small problems.

In the higher-order setting, simple versions of usable rules have also been defined [46, 31]. We can easily extend these definitions to AFSMs:

Theorem 5.4

Given a DP problem $M=(\mathcal{P},\mathcal{R},m,f)$ with $m\succeq\mathtt{minimal}$ and $\mathcal{R}$ finite, let $\mathit{UR}(\mathcal{P},\mathcal{R})$ be the smallest subset of $\mathcal{R}$ such that:

• •

if a symbol $\mathtt{f}$ occurs in the right-hand side of an element of $\mathcal{P}$ or $\mathit{UR}(\mathcal{P},\mathcal{R})$, and there is a rule $\mathtt{f}\ \ell_{1}\cdots\ell_{k}\Rightarrow r$, then this rule is also in $\mathit{UR}(\mathcal{P},\mathcal{R})$;

• •

if there exists $\ell\Rightarrow r\in\mathcal{R}$ or $\ell\Rrightarrow r\ (A)\in\mathcal{P}$ such that $r\unrhd F\langle s_{1},\dots,s_{k}\rangle\ t_{1}\cdots t_{n}$ with $s_{1},\dots,s_{k}$ not all distinct variables or with $n>0$, then $\mathit{UR}(\mathcal{P},\mathcal{R})=\mathcal{R}$.

Then the processor that maps $M$ to $\{(\mathcal{P},\mathit{UR}(\mathcal{P},\mathcal{R}),\mathtt{arbitrary},\mathtt{all})\}$ is sound.

For the proof we refer to the very similar proofs in [46, 31].

Example 22

For the set $\mathit{SDP}(\mathcal{R})$ of the ordinal recursion example (Ex. 2 and 11), all rules are usable due to the occurrence of $H\ M$ in the second DP. For the set $\mathit{SDP}(\mathcal{R})$ of the map example (Ex. 1 and 12), there are no usable rules, since the one DP contains no defined function symbols or applied meta-variables.

This higher-order processor is much less powerful than its first-order version: if any DP or usable rule has a sub-meta-term of the form $F\ s$ or $F\langle s_{1},\dots,s_{k}\rangle$ with $s_{1},\dots,s_{k}$ not all distinct variables, then all rules are usable. Since applying a higher-order meta-variable to some argument is extremely common in higher-order rewriting, the technique is usually not applicable. Also, this processor imposes a heavy price on the flags: minimality (at least) is required, but is lost; the formative flag is also lost. Thus, usable rules are often combined with reduction triples to temporarily disregard rules, rather than as a way to permanently remove rules.

To address these weaknesses, we consider a processor that uses similar ideas to usable rules, but operates from the left-hand sides of rules and DPs rather than the right. This adapts the technique from [31] that relies on the new formative flag. As in the first-order case [16], we use a semantic characterisation of formative rules. In practice, we then work with over-approximations of this characterisation, analogous to the use of dependency graph approximations in Thm. 0.C.1.

Definition 25

A function $\mathit{FR}$ that maps a pattern $\ell$ and a set of rules $\mathcal{R}$ to a set $\mathit{FR}(\ell,\mathcal{R})\subseteq\mathcal{R}$ is a formative rules approximation if for all $s$ and $\gamma$: if $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ by an $\ell$-formative reduction, then this reduction can be done using only rules in $\mathit{FR}(\ell,\mathcal{R})$.

We let $\mathit{FR}(\mathcal{P},\mathcal{R})=\bigcup\{\mathit{FR}(\ell_{i},\mathcal{R})\mid\mathtt{f}\ \ell_{1}\cdots\ell_{n}\Rrightarrow p\,(A)\>\in\,\mathcal{P}\wedge 1\leq i\leq n\}$.

Thus, a formative rules approximation is a subset of $\mathcal{R}$ that is sufficient for a formative reduction: if $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$, then $s\Rightarrow_{\mathit{FR}(\ell,\mathcal{R})}^{*}\ell\gamma$. It is allowed for there to exist other formative reductions that do use additional rules.

Example 23

We define a simple formative rules approximation: (1) $\mathit{FR}(Z,\mathcal{R})=\emptyset$ if $Z$ is a meta-variable; (2) $\mathit{FR}(\mathtt{f}\ \ell_{1}\cdots\ell_{m},\mathcal{R})=\mathit{FR}(\ell_{1},\mathcal{R})\cup\dots\cup\mathit{FR}(\ell_{m},\mathcal{R})$ if $\mathtt{f}:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ and no rules have type $\iota$; (3) $\mathit{FR}(s,\mathcal{R})=\mathcal{R}$ otherwise. This is a formative rules approximation: if $s\Rightarrow_{\mathcal{R}}^{*}Z\gamma$ by a $Z$-formative reduction, then $s=Z\gamma$, and if $s\Rightarrow_{\mathcal{R}}^{*}\mathtt{f}\ \ell_{1}\cdots\ell_{m}$ and no rules have the same output type as $s$, then $s=\mathtt{f}\ s_{1}\cdots s_{m}$ and each $s_{i}\Rightarrow_{\mathcal{R}}^{*}\ell_{i}\gamma$ (by an $\ell_{i}$-formative reduction).

The following result follows directly from the definition of formative rules.

Theorem 5.5 (Formative rules processor)

For a formative rules approximation $\mathit{FR}$, the processor $\mathit{Proc}_{\mathit{FR}}$ that maps a DP problem $(\mathcal{P},\mathcal{R},m,\mathtt{formative})$ to $\{(\mathcal{P},\mathit{FR}(\mathcal{P},\mathcal{R}),m,\mathtt{formative})\}$ is both sound and complete.

Proof (sketch)

A processor that only removes rules (or DPs) is always complete. For soundness, if the chain is formative then each step $t_{i}\Rightarrow_{\mathcal{R}}^{*}s_{i+1}$ can be replaced by $t_{i}\Rightarrow_{\mathit{FR}(\mathcal{P},\mathcal{R})}^{*}s_{i+1}$. Thus, the chain can be seen as a $(\mathcal{P},\mathit{FR}(\mathcal{P},\mathcal{R}))$-chain. ∎

Example 24

For our ordinal recursion example (Ex. 2 and 11), none of the rules are included when we use the approximation of Ex. 23 since all rules have output type $\mathtt{ord}$. Thus, $\mathit{Proc}_{\mathit{FR}}$ maps $(\mathit{SDP}(\mathcal{R}),\mathcal{R},\mathtt{computable}_{\mathcal{R}},\mathtt{formative})$ to $(\mathit{SDP}(\mathcal{R}),\emptyset,\mathtt{computable}_{\mathcal{R}},\mathtt{formative})$. Note: this example can also be completed without formative rules (see Ex. 26). Here we illustrate that, even with a simple formative rules approximation, we can often delete all rules of a given type.

Formative rules are introduced in [31], and the definitions can be adapted to a more powerful formative rules approximation than the one sketched in Ex. 24. Several examples and deeper intuition for the first-order setting are given in [16].

5.4 Subterm criterion processors

Reduction triple processors are powerful, but they exert a computational price: we must orient all rules in $\mathcal{R}$. The subterm criterion processor allows us to remove DPs without considering $\mathcal{R}$ at all. It is based on a projection function [24], whose higher-order counterpart [34, 46, 31] is the following:

Definition 26

For $\mathcal{P}$ a set of DPs, let $\mathtt{heads}(\mathcal{P})$ be the set of all symbols $\mathtt{f}$ that occur as the head of a left- or right-hand side of a DP in $\mathcal{P}$. A projection function for $\mathcal{P}$ is a function $\nu:\mathtt{heads}(\mathcal{P})\to\mathbb{N}$ such that for all DPs $\ell\Rrightarrow p\ (A)\in\mathcal{P}$, the function $\overline{\nu}$ with $\overline{\nu}(\mathtt{f}\ s_{1}\cdots s_{n})=s_{\nu(\mathtt{f})}$ is well-defined both for $\ell$ and for $p$.

Theorem 5.6 (Subterm criterion processor)

The processor $\mathit{Proc}_{\mathtt{subcrit}}$ that maps a DP problem $(\mathcal{P}_{1}\uplus\mathcal{P}_{2},\mathcal{R},m,f)$ with $m\succeq\mathtt{minimal}$ to $\{(\mathcal{P}_{2},\mathcal{R},m,f)\}$ if a projection function $\nu$ exists such that $\overline{\nu}(\ell)\rhd\overline{\nu}(p)$ for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$ and $\overline{\nu}(\ell)=\overline{\nu}(p)$ for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{2}$, is sound and complete.

Proof (sketch)

If the conditions are satisfied, every infinite $(\mathcal{P},\mathcal{R})$-chain induces an infinite $\unrhd\mathop{\cdot}\Rightarrow_{\mathcal{R}}^{*}$ sequence that starts in a strict subterm of $t_{1}$, contradicting minimality unless all but finitely many steps are equality. Since every occurrence of a pair in $\mathcal{P}_{1}$ results in a strict $\rhd$ step, a tail of the chain lies in $\mathcal{P}_{2}$. ∎

Example 25

Using $\nu(\mathtt{map}^{\sharp})=2$, $\mathit{Proc}_{\mathtt{subcrit}}$ maps the DP problem $(\{(1)\},\mathcal{R},\linebreak\mathtt{computable}_{\mathcal{R}},\mathtt{formative})$ from Ex. 18 to $\{(\emptyset,\mathcal{R},\mathtt{computable}_{\mathcal{R}},\mathtt{formative})\}$.

The subterm criterion can be strengthened, following [34, 46], to also handle DPs like the one in Ex. 10. Here, we focus on a new idea. For computable chains, we can build on the idea of the subterm criterion to get something more.

Theorem 5.7 (Computable subterm criterion processor)

The processor $\mathit{Proc}_{\mathtt{statcrit}}$ that maps a DP problem $(P_{1}\uplus\mathcal{P}_{2},\mathcal{R},\mathtt{computable}_{\mathcal{U}},f)$ to $\{(\mathcal{P}_{2},\mathcal{R},\linebreak\mathtt{computable}_{\mathcal{U}},f)\}$ if a projection function $\nu$ exists such that $\overline{\nu}(\ell)\sqsupset\overline{\nu}(p)$ for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$ and $\overline{\nu}(\ell)=\overline{\nu}(p)$ for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{2}$, is sound and complete. Here, $\sqsupset$ is the relation on base-type terms with $s\sqsupset t$ if $s\neq t$ and (a) $s\unrhd_{\mathtt{acc}}t$ or (b) a meta-variable $Z$ exists with $s\unrhd_{\mathtt{acc}}Z\langle x_{1},\dots,x_{k}\rangle$ and $t=Z\langle t_{1},\dots,t_{k}\rangle\ s_{1}\cdots s_{n}$.

Proof (sketch)

By the conditions, every infinite $(\mathcal{P},\mathcal{R})$-chain induces an infinite $(\Rrightarrow_{C_{\mathcal{U}}}\cup\Rightarrow_{\beta})^{*}\cdot\Rightarrow_{\mathcal{R}}^{*}$ sequence (where $C_{\mathcal{U}}$ is defined following Thm. 2.2). This contradicts computability unless there are only finitely many inequality steps. As pairs in $\mathcal{P}_{1}$ give rise to a strict decrease, they may occur only finitely often. ∎

Example 26

Following Ex. 2 and 11, consider the projection function $\nu$ with $\nu(\mathtt{rec}^{\sharp})=1$. As $\mathtt{s}\ X\unrhd_{\mathtt{acc}}X$ and $\mathtt{lim}\ H\unrhd_{\mathtt{acc}}H$, both $\mathtt{s}\ X\sqsupset X$ and $\mathtt{lim}\ H\sqsupset H\ M$ hold. Thus $\mathit{Proc}_{\mathtt{statc}}(\mathcal{P},\mathcal{R},\mathtt{computable}_{\mathcal{R}},\mathtt{formative})=\{(\emptyset,\mathcal{R},\mathtt{computable}_{\mathcal{R}},\linebreak\mathtt{formative})\}$. By the dependency graph processor, the AFSM is terminating.

The computable subterm criterion processor fundamentally relies on the new $\mathtt{computable}_{\mathcal{U}}$ flag, so it has no counterpart in the literature so far.

5.5 Non-termination

While (most of) the processors presented so far are complete, none of them can actually return NO. We have not yet implemented such a processor; however, we can already provide a general specification of a non-termination processor.

Theorem 5.8 (Non-termination processor)

Let $M=(\mathcal{P},\mathcal{R},m,f)$ be a DP problem. The processor that maps $M$ to NO if it determines that a sufficient criterion for non-termination of $\Rightarrow_{\mathcal{R}}$ or for existence of an infinite conservative $(\mathcal{P},\mathcal{R})$-chain according to the flags $m$ and $f$ holds is sound and complete.

Proof

Obvious. ∎

This is a very general processor, which does not tell us how to determine such a sufficient criterion. However, it allows us to conclude non-termination as part of the framework by identifying a suitable infinite chain.

Example 27

If we can find a finite $(\mathcal{P},\mathcal{R})$-chain $[(\rho_{0},s_{0},t_{0}),\dots,(\rho_{n},s_{n},t_{n})]$ with $t_{n}=s_{0}\gamma$ for some substitution $\gamma$ which uses only conservative DPs, is formative if $f=\mathtt{formative}$ and is ${\mathcal{U}}$-computable if $m=\mathtt{computable}_{\mathcal{U}}$, such a chain is clearly a sufficient criterion: there is an infinite chain $[(\rho_{0},s_{0},t_{0}),\dots,(\rho_{0},s_{0}\gamma,t_{0}\gamma),\dots,\linebreak(\rho_{0},s_{0}\gamma\gamma,t_{0}\gamma\gamma),\ldots]$. If $m=\mathtt{minimal}$ and we find such a chain that is however not minimal, then note that $\Rightarrow_{\mathcal{R}}$ is non-terminating, which also suffices.

For example, for a DP problem $(\mathcal{P},\mathcal{R},\mathtt{minimal},\mathtt{all})$ with $\mathcal{P}=\{\mathtt{f}^{\sharp}\ F\ X\Rrightarrow\mathtt{g}^{\sharp}\ (F\ X),\ \mathtt{g}^{\sharp}\ X\Rrightarrow\mathtt{f}^{\sharp}\ \mathtt{h}\ X\}$, there is a finite dependency chain: $[(\mathtt{f}^{\sharp}\ F\ X\Rrightarrow\mathtt{g}^{\sharp}\ (F\ X),\ \mathtt{f}^{\sharp}\ \mathtt{h}\ x,\ \mathtt{g}^{\sharp}\ (\mathtt{h}\ x)),\ \;(\mathtt{g}^{\sharp}\ X\Rrightarrow\mathtt{f}^{\sharp}\ \mathtt{h}\ X,\ \mathtt{g}^{\sharp}\ (\mathtt{h}\ x),\ \mathtt{f}^{\sharp}\ \mathtt{h}\ (\mathtt{h}\ x))]$. As $\mathtt{f}^{\sharp}\ \mathtt{h}\ (\mathtt{h}\ x)$ is an instance of $\mathtt{f}^{\sharp}\ \mathtt{h}\ x$, the processor maps this DP problem to NO.

To instantiate Thm. 5.8, we can borrow non-termination criteria from first-order rewriting [21, 42, 13], with minor adaptions to the typed setting. Of course, it is worthwhile to also investigate dedicated higher-order non-termination criteria.

6 Conclusions and Future Work

We have built on the static dependency pair approach [6, 34, 46, 33] and formulated it in the language of the DP framework from first-order rewriting [20, 22]. Our formulation is based on AFSMs, a dedicated formalism designed to make termination proofs transferrable to various higher-order rewriting formalisms.

This framework has two important additions over existing higher-order DP approaches in the literature. First, we consider not only arbitrary and minimally non-terminating dependency chains, but also minimally non-computable chains; this is tracked by the $\mathtt{computable}_{\mathcal{U}}$ flag. Using the flag, a dedicated processor allows us to efficiently handle rules like Ex. 2. This flag has no counterpart in the first-order setting. Second, we have generalised the idea of formative rules in [31] to a notion of formative chains, tracked by a $\mathtt{formative}$ flag. This makes it possible to define a corresponding processor that permanently removes rules.

Implementation and experiments. To provide a strong formal groundwork, we have presented several processors in a general way, using semantic definitions of, e.g., the dependency graph approximation and formative rules rather than syntactic definitions using functions like $\mathit{TCap}$ [21]. Even so, most parts of the DP framework for AFSMs have been implemented in the open-source termination prover WANDA [28], alongside a dynamic DP framework [31] and a mechanism to delegate some ordering constraints to a first-order tool [14]. For reduction triples, polynomial interpretations [15] and a version of HORPO [29, Ch. 5] are used. To solve the constraints arising in the search for these orderings, and also to determine sort orderings (for the accessibility relation) and projection functions (for the subterm criteria), WANDA employs an external SAT-solver. WANDA has won the higher-order category of the International Termination Competition [50] four times. In the International Confluence Competition [10], the tools ACPH [40] and CSI^ho [38] use WANDA as their “oracle” for termination proofs on HRSs.

We have tested WANDA on the Termination Problems Data Base [49], using AProVE [19] and MiniSat [12] as back-ends. When no additional features are enabled, WANDA proves termination of 124 (out of 198) benchmarks with static DPs, versus 92 with only a search for reduction orderings; a 34% increase. When all features except static DPs are enabled, WANDA succeeds on 153 benchmarks, versus 166 with also static DPs; an 8% increase, or alternatively, a 29% decrease in failure rate. The full evaluation is available in Appendix 0.D.

Future work. While the static and the dynamic DP approaches each have their own strengths, there has thus far been little progress on a unified approach, which could take advantage of the syntactic benefits of both styles. We plan to combine the present work with the ideas of [31] into such a unified DP framework.

In addition, we plan to extend the higher-order DP framework to rewriting with strategies, such as implicit $\beta$-normalisation or strategies inspired by functional programming languages like OCaml and Haskell. Other natural directions are dedicated automation to detect non-termination, and reducing the number of term constraints solved by the reduction triple processor via a tighter integration with usable and formative rules with respect to argument filterings.

Appendix 0.A Computability: the set $C$

In this appendix, we prove Thm. 2.2: the existence of an RC-set $C$ that provides an accessibility relation $\unrhd_{\mathtt{acc}}$ that preserves computability, and a base-type accessibility step $\Rrightarrow_{C}$ that preserves both computability and termination.

As we have said before, $\mathcal{V}$ and $\mathcal{F}$ contain infinitely many symbols of all types. We will use this to select variables or constructor symbol of any given type without further explanation.

These proofs do not require that computability is considered with respect to a rewrite relation: other relations (such as recursive path orderings) may be used as well. To make this explicit, we will use an alternative relation symbol, $\sqsupset$.

The proofs here consider a computability notion over the set $\mathcal{T}(\mathcal{F},\mathcal{V})$ of terms without restrictions. However, they could easily be extended to subsets of a different set of terms $T$, provided $T$ is closed under $\Rightarrow_{\mathcal{R}}$. This could for instance be used to obtain a computability result for terms that satisfy certain arity restrictions. To make this generality clear, each quantification over terms is explicitly marked with $\mathcal{T}(\mathcal{F},\mathcal{V})$.

Note: a more extensive discussion of computability can be found in [7]. Our notion of accessibility largely corresponds to membership of the computability closure defined there (although not completely).

0.A.1 Definitions and main computability result

Definition 27

In Appendix 0.A, $\sqsupset$ is assumed to be a given relation on terms of the same type, with respect to which we consider computability. We require that:

• •

$\sqsupset$ is monotonic (that is, $s\sqsupset t$ implies that $s\ u\sqsupset t\ u$ and $u\ s\sqsupset u\ t$ and $\lambda x.s\sqsupset\lambda x.t$);

• •

for all variables $x$: $x\ s_{1}\cdots s_{n}\sqsupset t$ implies that $t$ has the form $x\ s_{1}\cdots s_{i}^{\prime}\cdots s_{n}$ with $s_{i}\sqsupset s_{i}^{\prime}$;

• •

if $s\Rightarrow_{\mathtt{head}\beta}^{*}u$ and $s\sqsupset t$, then there exists $v$ such that $u\sqsupset^{*}v$ and $t\Rightarrow_{\mathtt{head}\beta}^{*}v$; here, $\Rightarrow_{\mathtt{head}\beta}$ is the relation generated by the step $(\lambda x.u)\ v\ w_{1}\cdots w_{n}\Rightarrow_{\mathtt{head}\beta}u[x:=v]\ w_{1}\cdots w_{n}$;

• •

if $t$ is the $\mathtt{head}\beta$-normal form of $s$, then $s\sqsupset^{*}t$.

We call a term neutral if it has the form $x\ s_{1}\cdots s_{n}$ or $(\lambda x.u)\ s_{0}\cdots s_{n}$.

The generality obtained by imposing only the minimal requirements on $\sqsupset$ is not needed in the current paper (where we only consider computability with respect to a rewrite relation), but could be used to extend the method to other domains. First note:

Lemma 1

A rewrite relation $\Rightarrow_{\mathcal{R}}$ satisfies the requirements of $\sqsupset$ stated in Def. 27.

Proof

Clearly $\Rightarrow_{\mathcal{R}}$ is monotonic, applications with a variable at the head cannot be reduced at the head, and moreover $\Rightarrow_{\mathcal{R}}$ includes $\Rightarrow_{\mathtt{head}\beta}$.

The third property we prove by induction on $s$ with $\Rightarrow_{\beta}$, using $\Rightarrow_{\mathcal{R}}^{*}$ instead of $\Rightarrow_{\mathcal{R}}$ for a stronger induction hypothesis. If $s=u$, then we are done choosing $v:=t$. Otherwise we can write $s=(\lambda x.q)\ w_{0}\ w_{1}\cdots w_{n}$ and $s\Rightarrow_{\mathtt{head}\beta}s^{\prime}:=q[x:=w_{0}]\ w_{1}\cdots w_{n}$, and $s^{\prime}\Rightarrow_{\mathtt{head}\beta}^{*}u$. If the reduction $s\Rightarrow_{\mathcal{R}}^{*}t$ does not take any head steps, then

[TABLE]

and indeed $u\Rightarrow_{\mathcal{R}}^{*}v$ by monotonicity. Otherwise, by the same argument we can safely assume that the head step is done first, so $s^{\prime}\Rightarrow_{\mathcal{R}}^{*}t$; we complete by the induction hypothesis. ∎

Recall Def. 7 from the text.

Definition 28 (with $\sqsupset$ rather than $\Rightarrow_{\mathcal{R}}$)

A set of reducibility candidates, or RC-set, for a relation $\sqsupset$ as in Def. 27 is a set $I$ of base-type terms $s\in\mathcal{T}(\mathcal{F},\mathcal{V})$ such that:

• •

every term in $I$ is terminating under $\sqsupset$

• •

$I$ is closed under $\sqsupset$ (so if $s\in I$ and $s\sqsupset t$ then $t\in I$)

• •

if $s\in\mathcal{T}(\mathcal{F},\mathcal{V})$ is neutral, and for all $t$ with $s\sqsupset t$ we have $t\in I$, then $s\in I$

We define $I$-computability for an RC-set $I$ by induction on types; for $s\in\mathcal{T}(\mathcal{F},\mathcal{V})$ we say $s$ is $I$-computable if:

• •

$s:\iota$ for some $\iota\in\mathcal{S}$ and $s\in I$ ($\iota\in\mathcal{S}$)

• •

$s:\sigma\rightarrow\tau$ and for all terms $t:\sigma\in\mathcal{T}(\mathcal{F},\mathcal{V})$ that are $I$-computable, $s\ t$ is $I$-computable

For $\iota$ a sort and $I$ an RC-set, we will write $I(\iota)=\{s\in I\mid s:\iota\}$.

Let us illustrate Def. 7 with two examples:

Lemma 2

The set SN of all terminating base-type terms in $\mathcal{T}(\mathcal{F},\mathcal{V})$ is an RC-set. The set MIN of all terminating base-type terms in $\mathcal{T}(\mathcal{F},\mathcal{V})$ whose $\mathtt{head}\beta$-normal form can be written $x\ s_{1}\cdots s_{m}$ with $x\in\mathcal{V}$ is also an RC-set.

Proof

It is easy to verify that the requirements hold for SN. For MIN, clearly termination holds. If $s\in\textsf{MIN}$, then $s\Rightarrow_{\mathtt{head}\beta}^{*}x\ s_{1}\cdots s_{m}=:s^{\prime}$, so for any $t$ with $s\sqsupset^{*}t$ the assumptions on $\sqsupset$ provide that $t\Rightarrow_{\mathtt{head}\beta}^{*}v$ for some $\sqsupset^{*}$-reduct of $s^{\prime}$, which can only have the form $x\ t_{1}\cdots t_{m}$. Finally, we prove that a neutral term $s\in\mathcal{T}(\mathcal{F},\mathcal{V})$ is in MIN if all its $\sqsupset^{+}$-reducts are, by induction on $s$ with $\Rightarrow_{\beta}$ (this suffices because we have already seen that MIN is closed under $\sqsupset$). If $s=x\ s_{1}\cdots s_{m}$ then it is included in MIN if it is terminating, which is the case if all its reducts are terminating, which is certainly the case if they are in MIN. If $s=(\lambda x.u)\ v\ w_{1}\cdots w_{m}$ then it is included if (a) all its reducts are terminating (which is satisfied if they are in MIN), and (b) the $\mathtt{head}\beta$-normal form $s^{\prime}$ of $s$ has the right form, which holds because $s\sqsupset^{+}s^{\prime}$ (as $\Rightarrow_{\mathtt{head}\beta}$ is included in $\sqsupset$) and therefore $s^{\prime}\in\textsf{MIN}$ by assumption. ∎

In fact, we have that MIN $\subseteq I\subseteq$ SN for all RC-sets $I$. The latter inclusion is obvious by the termination requirement in the definition of RC-sets. The former inclusion follows easily:

Lemma 3

For all RC-sets $I$, MIN $\subseteq I$.

Proof

We prove by induction on $\sqsupset$ that all elements of MIN are also in $I$. It is easy to see that if $s\in\textsf{MIN}$ then $s$ is neutral. Therefore, $s\in I$ if $t\in I$ whenever $s\sqsupset t$. But since MIN is closed by Lemma 2, each such $t$ is in MIN, so also in $I$ by the induction hypothesis. ∎

Aside from minimality of MIN, Lemma 3 actually provides $I$-computability of all variables, regardless of $I$. We prove this alongside termination of all $I$-computable terms.

Lemma 4

Let $I$ be an RC-set. The following statements hold for all types $\sigma$:

all variables $x:\sigma$ are $I$-computable 2. 2.

all $I$-computable terms $s:\sigma$ are terminating (w.r.t. $\sqsupset$)

Proof

By a mutual induction on the form of $\sigma$, which we may safely write $\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ (with $m\geq 0$ and $\iota\in\mathcal{S}$).

(1) By definition of $I$-computability, $x:\sigma$ is computable if and only if $x\ s_{1}\cdots s_{m}\in I$ for all $I$-computable terms $s_{1}:\sigma_{1},\dots,s_{m}:\sigma_{m}$ in $\mathcal{T}(\mathcal{F},\mathcal{V})$. However, as all $\sigma_{i}$ are smaller types, we know that such terms $s_{i}$ are terminating, so Lemma 3 gives the required result.

(2) Let $x_{1}:\sigma_{1},\dots,x_{m}:\sigma_{m}$ be variables; by the induction hypothesis they are computable, and therefore $s\ x_{1}\cdots x_{m}$ is in $I$ and therefore terminating. Then the head, $s$, cannot itself be non-terminating (by monotonicity of $\sqsupset$). ∎

While SN is indisputably the easiest RC-set to define and work with, it will be beneficial for the strength of the method to consider a set strictly between MIN and SN. To this end, we assume given an ordering on types, and a function mapping each function symbol $\mathtt{f}$ to a set $\mathit{Acc}(\mathtt{f})$ of arguments positions. Here, we deviate from the text by not fixing $\mathit{Acc}$; again, this generality is not needed for the current paper, but is done with an eye on future extensions.

Definition 29 (Generalisation of Def. 8)

Assume given a quasi-ordering $\succeq^{\mathcal{S}}$ on $\mathcal{S}$ whose strict part $\succ^{\mathcal{S}}\ :=\ \succeq^{\mathcal{S}}\setminus\preceq^{\mathcal{S}}$ is well-founded. Let $\approx^{\mathcal{S}}$ denote the corresponding equivalence relation $\approx^{\mathcal{S}}\ :=\ \succeq^{\mathcal{S}}\cap\preceq^{\mathcal{S}}$.

For a type $\sigma\ \equiv\ \sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\kappa$ (with $\kappa\in\mathcal{S}$) and sort $\iota$, we write $\iota\succeq^{\mathcal{S}}_{+}\sigma$ if $\iota\succeq^{\mathcal{S}}\kappa$ and $\iota\succ^{\mathcal{S}}_{-}\sigma_{i}$ for each $i$, and we write $\iota\succ^{\mathcal{S}}_{-}\sigma$ if $\iota\succ^{\mathcal{S}}\kappa$ and $\iota\succeq^{\mathcal{S}}_{+}\sigma_{i}$ for each $i$.

For $\mathtt{f}:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ we assume given a set $\mathit{Acc}(\mathtt{f})\subseteq\{i\mid 1\leq i\leq m\wedge\iota\succeq^{\mathcal{S}}_{+}\sigma_{i}\}$. For $x:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota\in\mathcal{V}$, we write $\mathit{Acc}(x)=\{i\mid 1\leq i\leq m\wedge\sigma_{i}=\tau_{1}\rightarrow\dots\rightarrow\tau_{n}\rightarrow\kappa\wedge\iota\succeq^{\mathcal{S}}\kappa\}$. We write $s\unrhd_{\mathtt{acc}}t$ if either $s=t$, or $s=\lambda x.s^{\prime}$ and $s^{\prime}\unrhd_{\mathtt{acc}}t$, or $s=a\ s_{1}\cdots s_{n}$ with $a\in\mathcal{F}\cup\mathcal{V}$ and $s_{i}\unrhd_{\mathtt{acc}}t$ for some $i\in\mathit{Acc}(a)$ with $a\notin\mathit{FV}(s_{i})$.

Remark: This definition of the accessibility relations deviates from, e.g., [9] by using a pair of relations ($\succeq^{\mathcal{S}}_{+}$ and $\succ^{\mathcal{S}}_{-}$) rather than positive and negative positions. This is not an important difference, but simply a matter of personal preference; using a pair of relations avoids the need to discuss type positions in the text, allowing for a shorter presentation. It is also not common to allow a choice in $\mathit{Acc}(\mathtt{f})$, but rather to fix $\mathit{Acc}(\mathtt{f})=\{\sigma_{i}\mid 1\leq i\leq m\wedge\iota\succeq^{\mathcal{S}}_{+}\sigma\}$ for some symbols (for instance constructors) and $\mathit{Acc}(\mathtt{f})=\emptyset$ for the rest. We elected to leave the choice open for greater generality.

The interplay of the positive and negative relations $\succeq^{\mathcal{S}}_{+}$ and $\succ^{\mathcal{S}}_{-}$ leads to an important result on RC-sets.

Lemma 5

Fix a sort $\iota\in\mathcal{S}$. Suppose $I,J$ are RC-sets such that $I(\kappa)=J(\kappa)$ for all $\kappa$ with $\iota\succ^{\mathcal{S}}\kappa$ and $I(\kappa)\subseteq J(\kappa)$ if $\iota\approx^{\mathcal{S}}\kappa$. Let $s:\sigma$. Then we have:

• •

If $\iota\succeq^{\mathcal{S}}_{+}\sigma$, then if $s$ is $I$-computable also $s$ is $J$-computable.

• •

If $\iota\succ^{\mathcal{S}}_{-}\sigma$, then if $s$ is $J$-computable also $s$ is $I$-computable.

Proof

We prove both statements together by a shared induction on the form of $\sigma$. We can always write $\sigma\ \equiv\ \sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\kappa$ with $\kappa\in\mathcal{S}$.

First suppose $\iota\succeq^{\mathcal{S}}_{+}\sigma$; then $\iota\succeq^{\mathcal{S}}\kappa$ – so $I(\kappa)\subseteq J(\kappa)$ – and each $\iota\succ^{\mathcal{S}}_{-}\sigma_{i}$. Assume that $s$ is $I$-computable; we must show that it is $J$-computable, so that for all $J$-computable $t_{1}:\sigma_{1},\dots,t_{m}:\sigma_{m}$ we have: $s\ t_{1}\cdots t_{m}\in J$. However, by the induction hypothesis each $t_{i}$ is also $I$-computable, so $s\ t_{1}\cdots t_{m}\in I(\kappa)\subseteq J(\kappa)$ by the assumption.

For the second statement, suppose $\iota\succ^{\mathcal{S}}_{-}\sigma$; then $\iota\succ^{\mathcal{S}}\kappa$, so $I(\kappa)=J(\kappa)$. Assume that $s$ is $J$-computable; $I$-computability follows if $s\ t_{1}\cdots t_{m}\in I(\kappa)=J(\kappa)$ whenever $t_{1},\dots,t_{m}$ are $I$-computable. By the induction hypothesis they are $J$-computable, so this holds by assumption. ∎

The RC-set $C$ whose existence is asserted below offers computability with a notion of accessibility. It is worth noting that this is not a standard definition, but is designed to provide an additional relationship $\Rrightarrow_{I}$ that is terminating on computable terms. This relation will be useful in termination proofs using static DPs.

Theorem 0.A.1

Let $\Rrightarrow_{I}$ be the relation on base-type terms where $\mathtt{f}\ s_{1}\cdots s_{m}\Rrightarrow_{I}s_{i}\ t_{1}\cdots t_{n}$ whenever $i\in\mathit{Acc}(\mathtt{f})$ and $s_{i}:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{n}\rightarrow\iota$ and each $t_{j}$ is $I$-computable.

There exists an RC-set $C$ such that $C=\{s\in\mathcal{T}(\mathcal{F},\mathcal{V})\mid$ $s$ has base type $\wedge\ s$ is terminating under $\sqsupset\cup\Rrightarrow_{C}$ and if $s\sqsupset^{*}\mathtt{f}\ s_{1}\cdots s_{m}$ then $s_{i}$ is $C$-computable for all $i\in\mathit{Acc}(\mathtt{f})\}$.

Proof

We will define, by well-founded induction on $\iota$ using $\succeq^{\mathcal{S}}$, a set $A_{\iota}$ of terms as follows.

Assume $A_{\kappa}$ has already been defined for all $\kappa$ with $\iota\succ^{\mathcal{S}}\kappa$, and let $X_{\iota}$ be the set of RC-sets $I$ such that $I(\kappa)=A_{\kappa}$ whenever $\iota\succ^{\mathcal{S}}\kappa$. We observe that $X_{\iota}$ is a complete lattice with respect to $\subseteq$: defining the bottom element $\sqcup\emptyset:=\bigcup\{A_{\kappa}\mid\iota\succ^{\mathcal{S}}\kappa\}\cup\textsf{MIN}$ and the top element $\sqcap\emptyset:=\bigcup\{A_{\kappa}\mid\iota\succ^{\mathcal{S}}\kappa\}\cup\bigcup\{$ SN$(\kappa)\mid\neg(\iota\succ^{\mathcal{S}}\kappa)\}$, and letting $\sqcup Z:=\bigcup Z,\ \sqcap Z:=\bigcap Z$ for non-empty $Z$, it is easily checked that $\sqcap$ and $\sqcup$ give a greatest lower and least upper bound within $X_{\iota}$ respectively. Now for an RC-set $I\in X_{\iota}$, we let:

[TABLE]

Clearly, $F_{\iota}$ maps elements of $X_{\iota}$ to $X_{\iota}$: terms of type $\kappa\not\approx^{\mathcal{S}}\iota$ are left alone, and $F_{\iota}(I)$ satisfies the properties to be an RC-set. Moreover, $F_{\iota}$ is monotone. To see this, let $I,J\in X_{\iota}$ such that $I\subseteq J$; we must see that $F_{\iota}(I)\subseteq F_{\iota}(J)$. To this end, let $s\in F_{\iota}(I)$; we will see that also $s\in F_{\iota}(J)$. This is immediate if $s:\kappa\not\approx^{\mathcal{S}}\iota$, as membership in $X_{\iota}$ guarantees that $F_{\iota}(I)(\kappa)=I(\kappa)\subseteq J(\kappa)=F_{\iota}(J)(\kappa)$. So assume $s:\kappa\approx^{\mathcal{S}}\iota$. We must see two things:

• •

$s$ is terminating under $\sqsupset\cup\Rrightarrow_{J}$. We show that $\sqsupset\cup\Rrightarrow_{J}\ \subseteq\ \sqsupset\cup\Rrightarrow_{I}$; as $s$ is terminating in the latter, the requirement follows. Clearly $\sqsupset\ \subseteq\ \sqsupset\cup\Rrightarrow_{I}$, so assume $s\Rrightarrow_{J}s^{\prime}$. Then $s=\mathtt{f}\ t_{1}\cdots t_{m}$ and $s^{\prime}=t_{i}\ u_{1}\cdots u_{n}$ for $i\in\mathit{Acc}(\mathtt{f})$ and $J$-computable $u_{1},\dots,u_{n}$. We can write $t_{i}:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{n}\rightarrow\kappa$ and since $i\in\mathit{Acc}(\mathtt{f})$ we have $\iota\succeq^{\mathcal{S}}\kappa$ and $\iota\succ^{\mathcal{S}}_{-}\sigma_{j}$ for each $j$. By Lemma 5 then each $u_{j}$ is also $I$-computable, so also $s\Rrightarrow_{I}s_{1}$.

• •

If $s\sqsupset^{*}\mathtt{f}\ s_{1}\cdots s_{m}$ for some symbol $\mathtt{f}$ then for all $i\in\mathit{Acc}(\mathtt{f})$: $s_{i}$ is $J$-computable. But this is obvious: as $s\in F_{\iota}(I)$, we know that such $s_{i}$ are $I$-computable, and since $\iota\succeq^{\mathcal{S}}_{+}\sigma_{i}$ for $i\in\mathit{Acc}(\mathtt{f})$, Lemma 5 provides $J$-computability.

Thus, $F$ is a monotone function on a complete lattice; by Tarski’s fixpoint theorem there is a fixpoint, so an RC-set $I$ such that for all sorts $\kappa$:

• •

if $\iota\succ^{\mathcal{S}}\kappa$ then $I(\kappa)=A_{\kappa}$;

• •

if $\iota\approx^{\mathcal{S}}\kappa$ then $I(\kappa)=\{s\in\mathcal{T}(\mathcal{F},\mathcal{V})\mid s:\kappa\wedge s$ is terminating under $\sqsupset\cup\Rrightarrow_{I}\wedge$ if $s\sqsupset^{*}\mathtt{f}\ s_{1}\cdots s_{m}$ for a symbol $\mathtt{f}$ then $\forall i\in\mathit{Acc}(\mathtt{f}):\,s_{i}$ is $I$-computable$\}$

We define $A_{\kappa}:=I(\kappa)$ for all $\kappa\approx^{\mathcal{S}}\iota$.

Now we let $C:=\bigcup_{\iota\in\mathcal{S}}A_{\iota}$. Clearly, $C$ satisfies the given requirement. ∎

Thm. 0.A.1 easily gives the proof of Thm. 2.2 in the text:

Proof (Proof of Thm. 2.2)

Thm. 2.2 follows by taking $\Rightarrow_{\mathcal{R}}$ for $\sqsupset$ (which satisfies the requirements by Lemma 1) and taking for each $\mathit{Acc}(\mathtt{f})$ the maximum set $\{i\mid 1\leq i\leq m\wedge\iota\succeq^{\mathcal{S}}_{+}\sigma_{i}\}$. ∎

0.A.2 Additional properties of computable terms

For reasoning about computable terms (as we will do when defining static DPs and reasoning about computable chains), there are a number of properties besides those in Lemma 4 that will prove very useful to have. In the following, we fix the RC-set $C$ as obtained from Thm. 0.A.1.

Lemma 6

If $s$ is $C$-computable and $s\sqsupset t$, then $t$ is also $C$-computable.

(This actually holds for any RC-set, but we will only use it for $C$.)

Proof

By induction on the type of $s$. If $s$ has base type, then $C$-computability implies that $s\in C$, and because $C$ is an RC-set all reducts of $s$ are also in $C$. Otherwise, $s:\sigma\rightarrow\tau$ and computability of $s$ implies computability of $s\ u$ for all computable $u:\sigma$. By the induction hypothesis, the fact that $s\ u\sqsupset t\ u$ by monotonicity of $\sqsupset$ implies that $t\ u$ is computable for all computable $u$, and therefore by definition $t$ is computable. ∎

Thus, computability is preserved under $\sqsupset$; the following result shows that it is also preserved under $\Rrightarrow_{C}$.

Lemma 7

If $s$ is $C$-computable and $s\Rrightarrow_{C}t$, then $t$ is also $C$-computable.

Proof

If $s\Rrightarrow_{C}t$, then both terms have base type, so $C$-computability is simply membership in $C$. We have $s=\mathtt{f}\ s_{1}\cdots s_{m}$ and $t=s_{i}\ t_{1}\cdots t_{n}$ with each $t_{j}$ $C$-computable. Since, by definition of $C$, also $s_{i}$ is $C$-computable, $C$-computability of $t$ immediately follows. ∎

Finally, we will see that $C$-computability is also preserved under $\unrhd_{\mathtt{acc}}$. For this, we first make a more general statement, which will also handle variables below binders (which are freed in subterms).

Lemma 8

Let $s:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ and $t:\tau_{1}\rightarrow\dots\rightarrow\tau_{n}\rightarrow\kappa$ be meta-terms, such that $s\unrhd_{\mathtt{acc}}t$. Let $\gamma$ be a substitution with $\mathit{FMV}(s)\subseteq\mathtt{dom}(\gamma)\subseteq\mathcal{M}$.

Let $u_{1}:\tau_{1},\dots,u_{n}:\tau_{n}$ be $C$-computable terms, and $\delta$ a substitution with $\mathtt{dom}(\delta)\subseteq\mathcal{V}$ such that each $\delta(x)$ is $C$-computable, and for $t^{\prime}:=(t(\gamma\cup\delta))\ u_{1}\cdots u_{n}$ there is no overlap between $\mathit{FV}(t^{\prime})$ and the variables bound in $s$.

Then there exist a $C$-computable substitution $\xi$ with $\mathtt{dom}(\xi)\subseteq\mathcal{V}$ and $C$-computable terms $v_{1}:\sigma_{1},\dots,v_{m}:\sigma_{m}$ such that we have $(s(\gamma\cup\xi))\ v_{1}\cdots v_{m}\ (\Rrightarrow_{C}\cup\Rightarrow_{\mathtt{head}\beta})^{*}\ t^{\prime}$.

Proof

We prove the lemma by induction on the derivation of $s\unrhd_{\mathtt{acc}}t$; in this, we can assume (by $\alpha$-conversion) that variables that occur bound in $s$ do not also occur free or occur in $\gamma$.

If $s=t$, then we are done choosing $\xi$ and $\vec{v}$ equal to $\delta$ and $\vec{u}$.

If $s=\lambda x.s^{\prime}$ with $x:\sigma_{1}$ and $s^{\prime}\unrhd_{\mathtt{acc}}t$, then by the assumption based on $\alpha$-conversion above, $x$ does not occur free in $s$ or in the range of $\gamma$. By the induction hypothesis, there exist a computable substitution $\xi^{\prime}$ and computable terms $v_{2},\dots,v_{m}$ such that $(s^{\prime}(\gamma\cup\xi^{\prime}))\ v_{2}\cdots v_{m}\ (\Rrightarrow_{C}\cup\Rightarrow_{\mathtt{head}\beta})^{*}\ t^{\prime}$. We can safely assume that $x$ does not occur in the range of $\xi^{\prime}$, since $x$ does not occur in $t^{\prime}$ either (if $x$ does occur, we can replace it by a different variable). Therefore, if we define $\xi:=[x:=x]\cup[y:=\xi^{\prime}(y)\mid y\in\mathcal{V}\wedge y\neq x]$, we have $s^{\prime}(\gamma\cup\xi^{\prime})=(s^{\prime}(\gamma\cup\xi))[x:=\xi^{\prime}(x)]$. Choosing $v_{1}:=\xi^{\prime}(x)$, we get $(s(\gamma\cup\xi))\ v_{1}\cdots v_{m}\Rightarrow_{\mathtt{head}\beta}(s^{\prime}(\gamma\cup\xi^{\prime}))\ v_{2}\cdots v_{m}\ (\Rrightarrow_{C}\cup\Rightarrow_{\mathtt{head}\beta})^{*}\ t^{\prime}$.

If $s=x\ s_{1}\cdots s_{j}$ for $s_{i}:\pi_{1}\rightarrow\dots\rightarrow\pi_{n^{\prime}}\rightarrow\kappa^{\prime}$ with $\iota\succeq^{\mathcal{S}}\kappa^{\prime}$ and $x\notin\mathit{FV}(s_{i})$ and $s_{i}\unrhd_{\mathtt{acc}}t$, then the induction hypothesis provides $C$-computable terms $w_{1}:\pi_{1},\dots,w_{n^{\prime}}:\pi_{n^{\prime}}$ and a substitution $\xi^{\prime}$ such that $(s_{i}(\gamma\cup\xi^{\prime}))\ w_{1}\cdots w_{n^{\prime}}\ (\Rrightarrow_{C}\cup\Rightarrow_{\mathtt{head}\beta})^{*}\ t^{\prime}$. Since $x\notin\mathit{FV}(s_{i})$ by definition of $\unrhd_{\mathtt{acc}}$, we can safely assume that $x\notin\mathtt{dom}(\xi^{\prime})$. Now recall that by assumption $\mathcal{F}$ contains infinitely many constructors of all types; let $\mathtt{c}:\kappa\rightarrow\iota$ be a symbol that does not occur anywhere in $\mathcal{R}$. We can safely assume that $\mathit{Acc}(\mathtt{c})=\{1\}$. Then $w:=\lambda y_{1}\dots y_{j}z_{1}\dots z_{m}.\mathtt{c}\ (y_{i}\ w_{1}\cdots w_{n^{\prime}})$ is $C$-computable. Now let $\xi:=[x:=w]\cup[y:=\xi^{\prime}(y)\mid y\in\mathcal{V}\wedge y\neq x]$, and let $v_{1},\dots,v_{m}$ be variables (which are $C$-computable by Lemma 4(1)). Then $(s(\gamma\cup\xi))\ v_{1}\cdots v_{m}\Rightarrow_{\mathtt{head}\beta}^{j+m}s_{i}(\gamma\cup\xi^{\prime})\ w_{1}\cdots w_{n}^{\prime}\ (\Rrightarrow_{C}\cup\Rightarrow_{\mathtt{head}\beta})^{*}\ t^{\prime}$.

Otherwise, $s=\mathtt{f}\ s_{1}\cdots s_{n}$ and $s_{i}\unrhd_{\mathtt{acc}}t$ for some $i\in\mathit{Acc}(\mathtt{f})$; by the induction hypothesis there exist $\xi$ and $C$-computable terms $w_{1},\dots,w_{n^{\prime}}$ such that $s^{\prime}:=(s_{i}(\gamma\cup\xi))\ w_{1}\cdots w_{n^{\prime}}\ (\Rrightarrow_{C}\cup\Rightarrow_{\mathtt{head}\beta})^{*}t^{\prime}$. We have $(s(\gamma\cup\xi))\ v_{1}\cdots v_{m}\Rrightarrow_{C}s^{\prime}$ for any $\vec{v}$ (e.g., variables). ∎

From this we conclude:

Lemma 9

Let $s$ be a closed meta-term, $\gamma$ a substitution with $\mathit{FMV}(s)\subseteq\mathtt{dom}(\gamma)\subseteq\mathcal{M}$ and $t$ such that $s\unrhd_{\mathtt{acc}}t$ and $s\gamma$ is $C$-computable. Then for all substitutions $\delta$ mapping $\mathit{FV}(t)$ to computable terms: $t(\gamma\cup\delta)$ is $C$-computable.

Proof

$t(\gamma\cup\delta)$ is $C$-computable if $(t(\gamma\cup\delta))\ u_{1}\cdots u_{n}$ is $C$-computable for all computable $u_{1},\dots,u_{n}$. By Lemma 8 and the fact that $s$ is closed, there exist $C$-computable terms $v_{1},\dots,v_{m}$ such that $(s\gamma)\ v_{1}\cdots v_{m}\ (\Rrightarrow_{C}\cup\Rightarrow_{\mathtt{head}\beta})^{*}\ (t(\gamma\cup\delta))\ u_{1}\cdots u_{n}$. But $s\gamma$ is $C$-computable, and therefore so is $(s\gamma)\ v_{1}\cdots v_{m}$. Since $\Rrightarrow_{C}$ and $\Rightarrow_{\mathtt{head}\beta}$ are both computability-preserving by Lemmas 7 and 6 respectively (as $\Rightarrow_{\mathtt{head}\beta}$ is included in $\sqsupset$) we are done. ∎

Lemma 10

A neutral term is $C$-computable if and only if all its $\sqsupset$-reducts are $C$-computable.

Proof

That $C$-computability of a term implies $C$-computability of its reducts is given by Lemma 6. For the other direction, let $s:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ be neutral and suppose that all its reducts are $C$-computable. To prove that also $s$ is $C$-computable, we must see that for all $C$-computable terms $t_{1}:\sigma_{1},\dots,t_{m}:\sigma_{m}$ the term $u:=s\ t_{1}\cdots t_{m}$ is in $C$. We prove this by induction on $(t_{1},\dots,t_{m})$ ordered by $\sqsupset_{\mathtt{prod}}$. Clearly, since $s$ does not have the form $\mathtt{f}\ s_{1}\cdots s_{n}$ with $\mathit{Acc}(\mathtt{f})\neq\emptyset$, nor does $u$, so $u\in C$ if all its reducts are in $C$. But since $s$ is neutral, all reducts of $u$ either have the form $s^{\prime}\ t_{1}\cdots t_{m}$ with $s\sqsupset s^{\prime}$ – which is in $C$ because all $t_{i}$ are $C$-computable and $s^{\prime}$ is computable as a reduct of $s$ – or the form $s\ t_{1}\cdots t_{i}^{\prime}\cdots t_{m}$ with $t_{i}\sqsupset t_{i}^{\prime}$ – which is in $C$ by the induction hypothesis. ∎

Using the $\Rightarrow_{\mathtt{head}\beta}$-restrictions on $\sqsupset$, we obtain the following result:

Lemma 11

Let $x:\sigma\in\mathcal{V}$. A term $\lambda x.s\in\mathcal{T}(\mathcal{F},\mathcal{V})$ is $C$-computable if and only if $s[x:=t]$ is computable for all $C$-computable $t:\sigma$.

Proof

If $\lambda x.s$ is $C$-computable, then by definition so is $(\lambda x.s)\ t$ for all $C$-computable $t$; by Lemma 6 and inclusion of $\Rightarrow_{\mathtt{head}\beta}$ in $\sqsupset$, this implies $C$-computability of the reducts $s[x:=t]$.

For the other direction, suppose $s[x:=t]$ is $C$-computable for all $C$-computable $t:\sigma$. To obtain $C$-computability of $\lambda x.s$, we must see that $(\lambda x.s)\ t$ is $C$-computable for all $C$-computable $t:\sigma$. As $(\lambda x.s)\ t$ is neutral, this holds if all its $\sqsupset$-reducts $u$ are $C$-computable by Lemma 10, and certainly if all its $\sqsupset^{+}$-reducts are $C$-computable, which we prove by induction on $u$ oriented with $\sqsupset$. But by definition of $\sqsupset$ (and induction on the derivation $(\lambda x.s)\ t\sqsupset^{+}u$) there exists a term $v$ such that $s[x:=t]\sqsupset^{*}v$ and $u\Rightarrow_{\mathtt{head}\beta}^{*}v$. If $u=v$, we thus obtain the required property, and if $u\Rightarrow_{\mathtt{head}\beta}^{+}v$, then $u$ is neutral and hence is $C$-computable if all its $\sqsupset$-reducts are, which is the case by the induction hypothesis. ∎

Appendix 0.B Static dependency pairs

In this appendix, we will first prove the main result from § 4: Thm. 0.B.3. Then, we will prove the “inverse” result, Thm. 0.B.2. Finally, to provide a greater context to the current work, we will discuss how the definitions in [34, 46] relate to the definitions here.

0.B.1 Static dependency pairs: the main result

To start, we prove Thm. 0.B.3, which states that a properly applied, accessible function passing AFSM with rules $\mathcal{R}$ is terminating if it admits no $\mathcal{R}$-computable formative $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chains. Thm. 4.1, which states that an AFSM is terminating if it admits no $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chains, follows as a corollary.

In the following, let $C=C_{\mathcal{R}}$ be a computability predicate following Def. 0.A.1 for $\sqsupset$ the rewrite relation $\Rightarrow_{\mathcal{R}}$. We will briefly call a term “computable” if it is $C$-computable.

Henceforth, we will assume without explicitly stating it that $(\mathcal{F},\mathcal{R})$ is properly applied, so we can speak of $\mathit{minar}(\mathtt{f})$ without disclaimers; we let $\mathit{minar}(\mathtt{f})=0$ for $\mathtt{f}\notin\mathcal{D}$. We start with an observation on the consequences of accessible function passingness:

Lemma 12

Let $\ell$ be a closed pattern, $Z$ a meta-variable and $x_{1},\dots,x_{k}$ variables such that $\ell\unrhd_{\mathtt{acc}}Z\langle x_{1},\dots,x_{k}\rangle$. If $\ell\gamma$ is a computable term, then so is $\gamma(Z)$.

Proof

Since $\ell$ is closed, $\ell(\gamma\cup\delta)=\ell\gamma$ is computable for all computable substitutions $\delta$ whose domain is contained in $\mathcal{V}$. By Lemma 9, we thus have computability of $Z\langle x_{1},\dots,x_{k}\rangle(\gamma\cup\delta)$ for all such $\delta$. Since $\ell\gamma$ is a term, $Z\in\mathtt{dom}(\gamma)$ so we can either write $\gamma(Z)=\lambda x_{1}\dots x_{k}.s$ or $\gamma(Z)=\lambda x_{1}\dots x_{i}.s^{\prime}$ with $i<k$ and $s^{\prime}$ not an abstraction.

In the first case, if we let $\delta:=[x_{1}:=u_{1},\dots,x_{k}:=u_{k}]$ for computable terms $u_{1},\dots,u_{k}$ we have computability of $Z\langle x_{1},\dots,x_{k}\rangle(\gamma\cup\delta)=s[x_{1}:=u_{1},\dots,x_{k}:=u_{k}]$. Since this holds for all computable $u_{1},\dots,u_{k}$, Lemma 11 provides computability of $\lambda x_{1}\dots x_{k}.s=\gamma(Z)$. In the second case, the same substitution $\delta$ provides computability of $s^{\prime}[x_{1}:=u_{1},\dots,x_{i}:=u_{i}]\ u_{i+1}\cdots u_{n}$ which (since this holds for any $u_{i+1},\dots,u_{n}$) implies computability of $s^{\prime}[x_{1}:=u_{1},\dots,x_{i}:=u_{i}]$, and this in turn implies computability of $\gamma(Z)$ as before. ∎

Thus, computability of the left-hand side of an instantiated DP implies computability of all instantiated meta-variables. To transfer this property to the right-hand side of the instantiated pair, we have a closer look at the relation $\unrhd_{A}$.

In the following, we say that a meta-term $s$ respects $\mathit{minar}$ if $s\unrhd_{\beta}\mathtt{f}\ t_{1}\cdots t_{n}$ implies $n\geq\mathit{minar}(\mathtt{f})$.

Lemma 13

Let $s$ be a meta-term that respects $\mathit{minar}$ and $\gamma$ a substitution on a finite domain with $\mathit{FMV}(s)\subseteq\mathtt{dom}(\gamma)\subseteq\mathcal{M}$, such that all $\gamma(Z)$ are computable. If there exists a computable substitution $\delta$ on a variable domain (that is, $\mathtt{dom}(\gamma)\subseteq\mathcal{V}$) such that $s(\gamma\cup\delta)$ is not computable, then there exists a pair $t\ (A)\in\mathsf{cand}(s)$ such that all of the following hold:

• •

there is a computable substitution $\delta$ on variable domain such that $t(\gamma\cup\delta)$ is not computable;

• •

$\gamma$* respects $A$;*

• •

for all $t^{\prime}\neq t$ such that $t\unrhd_{B}t^{\prime}$ holds for some $B$ respected by $\gamma$: $t^{\prime}(\gamma\cup\delta)$ is computable for all computable substitutions $\delta$ on variable domain.

Proof

Let $S$ be the set of all pairs $t\ (A)$ such that (a) $s\unrhd_{A}t$, (b) there exists a computable substitution $\delta$ on variable domain such that $t(\gamma\cup\delta)$ is not computable, and (c) $\gamma$ respects $A$. This set is non-empty, as it contains $\{s\ (\emptyset)\}$. As the relations $\unrhd_{\beta}$ and $\supseteq$ are both well-founded quasi-orderings (the latter on finite sets), we can select a pair $t\ (A)$ that is, in a sense, minimal in $S$: for all $t^{\prime}\ (A^{\prime})\in S$: if $t\unrhd_{\beta}t^{\prime}$ then $t=t^{\prime}$ and not $A^{\prime}\subsetneq A$ (it is possible that $A$ and $A^{\prime}$ are incomparable). We observe that for all $t^{\prime},B$ such that $t^{\prime}\neq t$ and $t\unrhd_{B}t^{\prime}$ and $\gamma$ respects $B$ we cannot have $t^{\prime}\ (A\cup B)\in S$ by minimality of $t\ (A)$, so since $s\unrhd_{A\cup B}t\unrhd_{A\cup B}t^{\prime}$ and clearly $\gamma$ respects $A\cup B$, it can only follow that requirement (b) is not satisfied for $t^{\prime}$.

Now suppose that $t$ has the form $\mathtt{f}\ t_{1}\cdots t_{n}$. Then by the above reasoning, all $t_{i}(\gamma\cup\delta)$ are computable, and by definition of “$s$ respects $\mathit{minar}$” we know that $n\geq k:=\mathit{minar}(\mathtt{f})$. Thus, $(\mathtt{f}\ t_{1}\cdots t_{k})(\gamma\cup\delta)$ is not computable (since otherwise $t(\gamma\cup\delta)$ would be computable), and by definition of $S$ as a set of BRSMTs of $s$ (and minimality of $A$) we have $\mathtt{f}\ t_{1}\cdots t_{k}\ (A)\in\mathsf{cand}(s)$. By minimality of $t$ in $S$, we see that $\mathtt{f}\ t_{1}\cdots t_{k}\ (A)$ satisfies all the requirements for the lemma to hold.

Thus, if $t$ has the form $\mathtt{f}\ t_{1}\cdots t_{n}$, we are done; towards a contradiction we will show that if $t$ does not have this form, then $t\ (A)$ is not minimal.

Consider the form of $t$:

• •

$t=\lambda x.t^{\prime}$: by Lemma 11, non-computability of $t(\gamma\cup\delta)$ implies non-computability of $t^{\prime}(\gamma\cup\delta)[x:=u]$ for some computable $u$. Since, by $\alpha$-conversion, we can assume that $x$ does not occur in domain or range of $\gamma$ or $\delta$, we have non-computability of $t^{\prime}(\gamma\cup\delta\cup[x:=u])$, and $\delta\cup[x:=u]$ is a computable substitution on variable domain while $t\unrhd_{A}t^{\prime}$.

• •

$t=x\ t_{1}\cdots t_{n}$ with $x\in\mathcal{V}$: whether $x\in\mathtt{dom}(\delta)$ or not, $\delta(x)$ is computable (either by the assumption on $\delta$ or by Lemma 4(1)). Therefore, the only way for $t(\gamma\cup\delta)$ to not be computable is if some $s_{i}(\gamma\cup\delta)$ is not computable, and $s\unrhd_{A}s_{i}$.

• •

$t=\mathtt{c}\ t_{1}\cdots t_{n}$ with $\mathtt{c}\in\mathcal{F}\setminus\mathcal{D}$: $t(\gamma\cup\delta)$ is non-computable only if there exist computable terms $u_{n+1},\dots,u_{m}$ such that the term $\mathtt{c}\ t_{1}\cdots t_{n}\ u_{n+1}\cdots u_{m}$ of base type is not in $C$. This can only be the case if it is non-terminating or some $t_{i}(\gamma\cup\delta)$ is not computable. Since head-reductions are impossible, non-termination implies non-termination of some $t_{i}(\gamma\cup\delta)$ or $u_{j}$, which by Lemma 4(2) implies non-computability; as all $u_{j}$ are computable by assumption, this means some $t_{i}(\gamma\cup\delta)$ is non-computable. We are done because $t\unrhd_{A}t_{i}$.

• •

$t=\mathtt{f}\ t_{1}\cdots t_{n}$ with $\mathtt{f}\in\mathcal{D}$ but $n<\mathit{arity}(\mathtt{f})$: same as above, because terms of this form cannot be reduced at the head (or the root).

• •

$t=(\lambda x.u)\ t_{0}\cdots t_{n}$: $t(\gamma\cup\delta)$ is neutral, so by Lemma 10 non-computability implies the non-computability of a reduct. If the reduct $u(\gamma\cup\delta)[x:=t_{0}(\gamma\cup\delta)]\ (t_{1}(\gamma\cup\delta))\cdots(t_{n}(\gamma\cup\delta))=(u[x:=t_{0}]\ t_{1}\cdots t_{n})(\gamma\cup\delta)$ is non-computable, we are done because $t\unrhd_{A}u[x:=t_{0}]\ t_{1}\cdots t_{n}$. Otherwise, note that all many-step reducts of $t(\gamma\cup\delta)$ are either also a reduct of $(u[x:=t_{0}]\ t_{1}\cdots t_{n})(\gamma\cup\delta)$ – and therefore computable – or have the form $(\lambda x.u^{\prime})\ t_{0}^{\prime}\cdots t_{n}^{\prime}$ with $u(\gamma\cup\delta)\Rightarrow_{\mathcal{R}}^{*}u^{\prime}$ and each $t_{i}(\gamma\cup\delta)\Rightarrow_{\mathcal{R}}^{*}t_{i}^{\prime}$. Thus, at least one of $u(\gamma\cup\delta)$ or $t_{i}(\gamma\cup\delta)$ has to be non-terminating. But if $u(\gamma\cup\delta)$ is non-terminating, then so is $u[x:=u^{\prime}](\gamma\cup\delta)$, contradicting computability of $(u[x:=t_{0}]\ t_{1}\cdots t_{n})(\gamma\cup\delta)$. The same holds if $t_{i}(\gamma\cup\delta)$ is non-terminating for some $i\geq 1$. Thus, $t_{0}(\gamma\cup\delta)$ is non-terminating and therefore non-computable, and we indeed have $t\unrhd_{A}t_{0}$.

• •

$t=Z\langle s_{1},\dots,s_{k}\rangle\ t_{1}\cdots t_{n}$: we either have $\gamma(Z)=\lambda x_{1}\dots x_{k}.u$ or $\gamma(Z)=\lambda x_{1}\dots x_{i}.u^{\prime}$ with $i<k$ and $u^{\prime}$ not an abstraction; in the latter case let $u:=\lambda x_{i+1}\dots x_{k}.u^{\prime}\ x_{i+1}\cdots x_{k}$. Either way, $t(\gamma\cup\delta)=u[x_{1}:=s_{1}(\gamma\cup\delta),\dots,x_{k}:=s_{k}(\gamma\cup\delta)]\ (t_{1}(\gamma\cup\delta))\cdots(t_{n}(\gamma\cup\delta))$.

For this term to be non-computable, either some $t_{i}(\gamma\cup\delta)$ should be non-computable, or $u[x_{1}:=s_{1}(\gamma\cup\delta),\dots,x_{k}:=s_{k}(\gamma\cup\delta)]$. The former case immediately contradicts minimality, since $t\unrhd_{\emptyset}t_{i}$, so we assume the latter. However, if all $s_{i}(\gamma\cup\delta)$ are computable, then so is $u[x_{1}:=s_{1}(\gamma\cup\delta),\dots,x_{k}:=s_{k}(\gamma\cup\delta)]$:

• –

if $\gamma(Z)=\lambda x_{1}\dots x_{k}.u$ then this holds by computability of all $\gamma(Z)$ and Lemma 11;

• –

if $\gamma(Z)=\lambda x_{1}\dots x_{i}.u^{\prime}$ with $i<k$ and $u=u^{\prime}\ x_{i+1}\cdots x_{k}$, then computability of $\gamma(Z)$ and Lemma 11 provide computability of $u^{\prime}[x_{1}:=q_{1},\dots,x_{i}:=q_{i}]$, which by definition of computability for higher-order terms implies computability for $u^{\prime}[x_{1}:=q_{1},\dots,x_{i}:=q_{i}]\ q_{i+1}\cdots q_{n}=u[x_{1}:=q_{1},\dots,x_{n}:=q_{n}]$.

Thus, some $s_{i}(\gamma\cup\delta)$ must be non-computable, and since substituting an unused variable has no effect, this must be the case for some $i$ with $x_{i}\in\mathit{FV}(u)$. So in this case, $\gamma$ respects $B:=A\cup\{Z:i\}$ and we obtain $s\unrhd_{B}t\unrhd_{B}s_{i}$. ∎

Next, let us consider formative reductions. We will prove that reductions from a terminating term to some instance of a pattern may be assumed to be formative.

Lemma 14

Let $\ell$ be a pattern and $\gamma$ a substitution on domain $\mathit{FMV}(\ell)$ such that a meta-variable $Z$ with $\mathit{arity}(Z)=k$ is mapped to a term $\lambda x_{1}\dots x_{k}.t$. Let $s$ be a terminating term. If $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$, then there exists a substitution $\delta$ on the same domain as $\gamma$ such that each $\delta(Z)\Rightarrow_{\mathcal{R}}^{*}\gamma(Z)$ and $s\Rightarrow_{\mathcal{R}}^{*}\ell\delta$ by an $\ell$-formative reduction.

Note that the restriction on $\gamma$ is very light: every substitution $\gamma$ on domain $\mathit{FMV}(\ell)$ can be altered to map meta-variables with arity $k$ to terms with $k$ abstracted variables: if $\gamma(Z)=\lambda x_{1}\dots x_{k}.t$ with $k=\mathit{arity}(Z)$ then let $\gamma^{\prime}(Z)=\gamma(Z)$, and if $\gamma(Z)=\lambda x_{1}\dots x_{i}.t$ with $i<\mathit{arity}(Z)$ and $t$ not an abstraction, then replace this by setting $\gamma^{\prime}(Z):=\lambda x_{1}\dots x_{k}.t\ x_{i+1}\cdots x_{k}$. Note that $Z\langle x_{1},\dots,x_{k}\rangle\gamma=Z\langle x_{1},\dots,x_{k}\rangle\gamma^{\prime}$. Therefore, we always have $\ell\gamma=\ell\gamma^{\prime}$.

Proof

We prove the lemma by induction first on $s$ ordered by $\Rightarrow_{\mathcal{R}}\mathop{\cup}\rhd$, second on the length of the reduction $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$. If $\ell$ is not a fully extended linear pattern, then we are done choosing $\delta:=\gamma$. Otherwise, we consider four cases:

$\ell$ is a meta-variable application $Z\langle x_{1},\dots,x_{k}\rangle$; 2. 2.

$\ell$ is not a meta-variable application, and the reduction $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ does not contain any headmost steps; 3. 3.

$\ell$ is not a meta-variable application, and the reduction $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ contains headmost steps, the first of which is a $\Rightarrow_{\beta}$ step; 4. 4.

$\ell$ is not a meta-variable application, and the reduction $s\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ contains headmost steps, the first of which is not a $\Rightarrow_{\beta}$ step.

In the first case, if $\ell$ is a meta-variable application $Z\langle x_{1},\dots,x_{k}\rangle$, then by $\alpha$-conversion we may write $\gamma=[Z:=\lambda x_{1}\dots x_{k}.t]$ with $\ell\gamma=t$. Let $\delta$ be $[Z:=\lambda x_{1}\dots x_{k}.s]$. Then $\delta$ has the same domain as $\gamma$, and indeed $\delta(Z)=\lambda x_{1}\dots x_{k}.s\Rightarrow_{\mathcal{R}}^{*}\lambda x_{1}\dots x_{k}.(\ell\gamma)=\gamma(Z)$.

In the second case, a reduction without any headmost steps, note that $s$ has the same outer shape as $\ell$: either (a) $s=\lambda x.s^{\prime}$ and $\ell=\lambda x.\ell^{\prime}$, or (b) $s=a\ s_{1}\cdots s_{n}$ and $\ell=a\ \ell_{1}\cdots\ell_{n}$ for some $a\in\mathcal{V}\cup\mathcal{F}$ (since $\ell$ is a pattern, $a$ cannot be a meta-variable application or abstraction if $n>0$). In case (a), we obtain $\delta$ such that $s^{\prime}\Rightarrow_{\mathcal{R}}^{*}\ell^{\prime}\delta$ by an $\ell^{\prime}$-formative reduction and $\delta\Rightarrow_{\mathcal{R}}^{*}\gamma$ by the induction hypothesis (as sub-meta-terms of linear patterns are still linear patterns). In case (b), we let $\gamma_{i}$ be the restriction of $\gamma$ to $\mathit{FMV}(\ell_{i})$ for $1\leq i\leq n$; by linearity of $\ell$, all $\gamma_{i}$ have non-overlapping domains and $\gamma=\gamma_{1}\cup\dots\cup\gamma_{n}$. The induction hypothesis provides $\delta_{1},\dots,\delta_{n}$ on the same domains such that each $s_{i}\Rightarrow_{\mathcal{R}}^{*}\ell_{i}\delta_{i}$ by an $\ell_{i}$-formative reduction and $\delta_{i}\Rightarrow_{\mathcal{R}}^{*}\gamma_{i}$; we are done choosing $\delta:=\delta_{1}\cup\dots\cup\delta_{n}$.

In the third case, if the first headmost step is a $\beta$-step, note that $s$ must have the form $(\lambda x.t)\ u\ q_{1}\cdots q_{n}$, and moreover $s\Rightarrow_{\mathcal{R}}^{*}(\lambda x.t^{\prime})\ u^{\prime}\ q_{1}^{\prime}\cdots q_{n}^{\prime}\Rightarrow_{\beta}t^{\prime}[x:=u^{\prime}]\ q_{1}^{\prime}\cdots q_{n}^{\prime}\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ by steps in the respective subterms. But then also $s\Rightarrow_{\beta}t[x:=u]\ q_{1}\cdots q_{n}\Rightarrow_{\mathcal{R}}^{*}t^{\prime}[x:=u^{\prime}]\ q_{1}^{\prime}\cdots q_{n}^{\prime}\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$, and we can get $\delta$ and an $\ell$-formative reduction for $t[x:=u]\ q_{1}\cdots q_{n}\Rightarrow_{\mathcal{R}}^{*}\ell\delta$ by the induction hypothesis.

In the last case, if the first headmost step is not a $\beta$-step, then we can write $s=\mathtt{f}\ s_{1}\cdots s_{n}\Rightarrow_{\mathcal{R}}^{*}\mathtt{f}\ s_{1}^{\prime}\cdots s_{n}^{\prime}=(\ell^{\prime}\eta)\ s_{i+1}^{\prime}\cdots s_{n}^{\prime}\Rightarrow_{\mathcal{R}}(r\eta)\ s_{i+1}^{\prime}\cdots s_{n}^{\prime}\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$ for some $\mathtt{f}\in\mathcal{D}$, terms $s_{j}\Rightarrow_{\mathcal{R}}^{*}s_{j}^{\prime}$ for $1\leq j\leq n$, rule $\ell^{\prime}\Rightarrow r$ and substitution $\eta$ on domain $\mathit{FMV}(\ell^{\prime})$. But then $\ell^{\prime}\ Z_{i+1}\cdots Z_{n}\Rightarrow r\ Z_{i+1}\cdots Z_{n}\in\mathcal{R}^{\mathtt{ext}}$, and for $\eta^{\prime}:=\eta\cup[Z_{i+1}:=s_{i+1}^{\prime},\dots,Z_{n}:=s_{n}^{\prime}]$ we both have $s\Rightarrow_{\mathcal{R}}^{*}(\ell^{\prime}\ Z_{i+1}\cdots Z_{n})\eta^{\prime}$ without any headmost steps, and $(r\ Z_{i+1}\cdots Z_{n})\eta^{\prime}\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$. By the second induction hypothesis, there exists a substitution $\xi$ such that $s\Rightarrow_{\mathcal{R}}^{*}(\ell^{\prime}\ Z_{i+1}\cdots Z_{n})\xi$ by a $(\ell^{\prime}\ Z_{i+1}\cdots Z_{n})$-formative reduction and $\xi\Rightarrow_{\mathcal{R}}^{*}\eta^{\prime}$. This gives $s\Rightarrow_{\mathcal{R}}^{+}(r\ Z_{i+1}\cdots Z_{n})\xi\Rightarrow_{\mathcal{R}}^{*}(r\ Z_{i+1}\cdots Z_{n})\eta^{\prime}\Rightarrow_{\mathcal{R}}^{*}\ell\gamma$, so by the first induction hypothesis we obtain $\delta$ such that $(r\ Z_{i+1}\cdots Z_{n})\xi\Rightarrow_{\mathcal{R}}^{*}\ell\delta$ by an $\ell$-formative reduction, and $\delta\Rightarrow_{\mathcal{R}}^{*}\gamma$. ∎

Essentially, Lemma 14 states that we can postpone reductions that are not needed to obtain an instance of the given pattern. This is not overly surprising, but will help us eliminate some proof obligations later in the termination proof.

From this, we have the main result on static dependency chains.

Theorem 0.B.3

Let $(\mathcal{F},\mathcal{R})$ be a properly applied, accessible function passing AFSM. If $(\mathcal{F},\mathcal{R})$ is non-terminating, then there is an infinite $\mathcal{R}$-computable formative $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chain.

Proof

In the following, let a minimal non-computable term be a term $s:=\mathtt{f}\ s_{1}\cdots s_{k}$ with $k=\mathit{minar}(\mathtt{f})$, such that $\mathtt{f}\in\mathcal{D}$, and $s$ is not computable but all $s_{i}$ are $C$-computable. We say that $s$ is MNC.

We first observe that if $\Rightarrow_{\mathcal{R}}$ is non-terminating, then there exists a MNC term. After all, if $\Rightarrow_{\mathcal{R}}$ is non-terminating, then there is a non-terminating term $s$, which (by Lemma 4(2)) is also non-computable. Let $t\ (A)$ be the element of $\mathsf{cand}(s)$ that is given by Lemma 13 for $\gamma=\delta=[]$. Then $A=\emptyset$ and $t$ has the form $\mathtt{f}\ t_{1}\cdots t_{k}$ with $k=\mathit{minar}(\mathtt{f})$, and there exists a computable substitution $\delta$ such that $t\delta$ is not computable but all $t_{i}\delta$ are.

Thus, assuming $\Rightarrow_{\mathcal{R}}$ is non-terminating, we can select a MNC term $t_{-1}$.

Now for $i\in\mathbb{N}$, let a MNC term $t_{i-1}=\mathtt{f}\ q_{1}\cdots q_{k}$ be given. By definition of computability, there are computable $q_{k+1},\dots,q_{m}$ such that $\mathtt{f}\ q_{1}\cdots q_{k}$ has base type and is not computable. Since all $q_{i}$ are computable this implies that $\mathtt{f}\ q_{1}\cdots q_{k}$ is non-terminating, and since they are terminating, there is eventually a reduction at the head: there exist a rule $\mathtt{f}\ \ell_{1}\cdots\ell_{k}\Rightarrow r$ and a substitution $\gamma$ such that $\mathtt{f}\ q_{1}\cdots q_{m}\Rightarrow_{\mathcal{R},in}^{*}\mathtt{f}\ q_{1}^{\prime}\cdots q_{m}^{\prime}$ (where $\Rightarrow_{\mathcal{R},in}^{*}$ indicates a reduction in the argument terms $q_{j}$) $=\mathtt{f}\ (\ell_{1}\gamma)\cdots(\ell_{k}\gamma)\ q_{k+1}^{\prime}\cdots q_{m}^{\prime}\Rightarrow_{\mathcal{R}}(r\gamma)\ q_{k+1}^{\prime}\cdots q_{m}^{\prime}$, which latter term is still non-terminating. But then also $(r\gamma)\ q_{k+1}\cdots q_{m}$ is non-terminating (as it reduces to the term above), so $r\gamma$ is not computable.

From the above we conclude: $t_{i-1}\Rightarrow_{\mathcal{R},in}^{*}(\mathtt{f}\ \ell_{1}\cdots\ell_{k})\gamma\Rightarrow_{\mathcal{R}}r\gamma$, and $r\gamma$ is not computable. By Lemma 14, we can safely assume that the reductions $q_{j}\Rightarrow_{\mathcal{R}}^{*}\ell_{j}\gamma$ are $\ell_{j}$-formative if $\mathtt{f}\ \ell_{1}\cdots\ell_{k}$ is a fully extended linear pattern; and since $\mathtt{f}\ \ell_{1}\cdots\ell_{k}$ is closed we can safely assume that $\mathtt{dom}(\gamma)=\mathit{FMV}(\mathtt{f}\ \ell_{1}\cdots\ell_{k})$.

Let $s_{i}:=\mathtt{f}^{\sharp}\ (\ell_{1}\gamma)\cdots(\ell_{k}\gamma)$, and note that all $\ell_{j}\gamma$ are computable by Lemma 6. We observe that for all $Z$ occurring in $r$ we have that $\gamma(Z)$ is $C$-computable by a combination of accessible function passingness, computability of $\ell_{j}\gamma$ and Lemma 12. As $r\gamma$ is non-computable, Lemma 13 provides an element $t\ (A)$ of $\mathsf{cand}(r)$ with pleasant minimality properties and a computable substitution $\delta$ on domain $\mathit{FV}(t)$ such that $\gamma$ respects $A$ and $t(\gamma\cup\delta)$ is not computable. For $\mathit{FV}(t)=\{x_{1},\dots,x_{n}\}$, let $Z_{1},\dots,Z_{n}$ be fresh meta-variables; then $p:=t[x_{1}:=Z_{1},\dots,x_{n}:=Z_{n}]=\mathit{metafy}(t)$, and $p\eta=t\delta$ for $\eta$ the substitution mapping $X\in\mathit{FMV}(\ell)$ to $\gamma(\ell)$ and each $Z_{j}$ to $\delta(x_{j})$.

Set $\rho_{i}:=\ell^{\sharp}\Rrightarrow p^{\sharp}\ (A)$ and $t_{i}:=p^{\sharp}\eta$. Then $t_{i}$ is MNC, because the meta-term $t$ supplied by Lemma 13 has the form $\mathtt{g}\ u_{1}\cdots u_{m}$ with $m=\mathit{arity}(\mathtt{g})$ and $u_{j}(\gamma\cup\delta)$ is $C$-computable for each $j$ because $t\unrhd_{A}u_{j}$. Thus, we can continue the construction.

The chain $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ thus constructed is an infinite formative $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chain. That it is a $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chain is obvious because each $\rho_{i}\in\mathit{SDP}(\mathcal{R})$ (since $t\ (A)\in\mathsf{cand}(r)$), because $\gamma$ respects $A$ and $\eta$ corresponds with $\gamma$ on all meta-variables that take arguments, and because $\mathit{FV}(p)=\emptyset$ and $\mathtt{dom}(\eta)=\mathit{FMV}(\ell)\cup\{Z_{1},\dots,Z_{n}\}=\mathit{FMV}(\ell)\cup\mathit{FMV}(p)$. That it is a formative chain follows by the initial selection of $\gamma$, as we assumed formative reductions to each $\ell_{j}\gamma$.

It is also a computable chain: clearly we have $t_{i}=p\eta$ in step $i$ in the construction above. Suppose $p^{\sharp}\unrhd_{B}v$ and $\eta$ respects $B$, but $(\lambda y_{1}\dots y_{n}.v)\eta$ is not computable for $\mathit{FV}(v)=\{y_{1},\dots,y_{n}\}$ – so by Lemma 11, $v(\eta\cup\zeta)$ is not computable for some computable substitution $\zeta$ on domain $\mathit{FV}(v)$. Since the meta-variables $Z_{j}$ do not occur applied in $p$, we can safely assume that $B$ contains only conditions for the meta-variables in $\mathtt{dom}(\gamma)$. By renaming each $Z_{j}$ back to $x_{j}$, we obtain that $\gamma$ respects $B$ and $t\unrhd_{B}v^{\prime}$ with $v=v^{\prime}[x_{1}:=Z_{1},\dots,x_{n}:=Z_{n}]$. But then $r\gamma\unrhd_{A\cup B}t\unrhd_{A\cup B}v^{\prime}$ and $\gamma$ respects $A\cup B$ and $v^{\prime}(\gamma\cup\delta\cup\zeta)$ is non-computable. By minimality of the choice $t\ (A)$, we have $v^{\prime}=t$, so $v=p^{\sharp}$. However, $p^{\sharp}\eta$ has a marked symbol $\mathtt{g}^{\sharp}$ as a head symbol, and thus cannot be reduced at the top; by $C$-computability of its immediate subterms, it is computable. ∎

We also prove the statement that ${\mathcal{U}}$-computability implies minimality:

Lemma 15

Every ${\mathcal{U}}$-computable $(\mathcal{P},\mathcal{R})$-dependency chain is minimal.

Proof

Let $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ be a ${\mathcal{U}}$-computable $(\mathcal{P},\mathcal{R})$-chain and let $i\in\mathbb{N}$; we must prove that the strict subterms of $t_{i}$ are terminating under $\Rightarrow_{\mathcal{R}}$. By definition, since $\unrhd_{\emptyset}$ is a reflexive relation, $t_{i}$ is $C_{{\mathcal{U}}}$-computable where $C_{{\mathcal{U}}}$ is given by Thm. 2.2 for a relation $\Rightarrow_{{\mathcal{U}}}\mathop{\supseteq}\Rightarrow_{\mathcal{R}}$. By Lemma 4(2), $t_{i}$ is therefore terminating under $\Rightarrow_{{\mathcal{U}}}$, so certainly under $\Rightarrow_{\mathcal{R}}$ as well. The strict subterms of a terminating term are all terminating. ∎

0.B.2 Static dependency pairs: the inverse result

In this section, we prove Thm. 0.B.2, which states that the existence of certain kinds of dependency chains implies non-termination of the original AFSM. This is not a true inverse of Thm. 0.B.3 or even Thm. 4.1: as observed in the text, there are terminating AFSMs that do admit an infinite chain. It does, however, give us a way to use the DP framework to prove non-termination in some cases.

We begin by exploring the connection between $\unrhd_{\beta}$ and reduction steps. Note that this result is not limited to PA-AFP AFSMs, so in the following we do not assume that the rules or dependency pairs involved satisfy arity restrictions.

Lemma 16

Let $s,t$ be meta-terms and suppose $s\unrhd_{A}t$ for some set $A$ of meta-variable conditions. Then for any substitution $\gamma$ that respects $A$ and has a finite domain with $\mathit{FMV}(s)\subseteq\mathtt{dom}(\gamma)\subseteq\mathcal{M}$: $s\gamma\ (\blacktriangleright\mathop{\cup}\Rightarrow_{\beta})^{*}\ t\gamma$.

Proof

By induction on the definition of $\unrhd_{A}$. Consider the last step in its derivation.

• •

If $s=t$ then $s\gamma=t\gamma$.

• •

If $s=\lambda x.u$ and $u\unrhd_{A}t$, then by $\alpha$-conversion we can assume that $x\notin\mathit{FV}(\gamma(Z))$ for any $Z\in\mathit{FMV}(s)$. Thus, $s\gamma=\lambda x.(u\gamma)\blacktriangleright u\gamma\ (\blacktriangleright\mathop{\cup}\Rightarrow_{\beta})^{*}\ t\gamma$ by the induction hypothesis.

• •

If $s=(\lambda x.u)\ s_{0}\cdots s_{n}$ and $u[x:=s_{0}]\ s_{1}\cdots s_{n}\unrhd_{A}t$, then by $\alpha$-conversion we can safely assume that $x$ is fresh w.r.t. $\gamma$ as above; thus, $s\gamma=(\lambda x.(u\gamma))\ (s_{0}\gamma)\cdots\linebreak(s_{n}\gamma)\Rightarrow_{\beta}(u\gamma[x:=s_{0}\gamma])\ (s_{1}\gamma)\cdots(s_{n}\gamma)=(u[x:=s_{0}]\ s_{1}\cdots s_{n})\gamma$, which reduces to $t\gamma$ by the induction hypothesis.

• •

If $s=u\ s_{1}\cdots s_{n}$ for $u$ an abstraction, variable, function symbol or meta-variable application, and $s_{i}\unrhd_{A}t$, then $s\gamma=(u\gamma)\ (s_{1}\gamma)\cdots(s_{n}\gamma)\blacktriangleright s_{i}\gamma\ (\blacktriangleright\mathop{\cup}\Rightarrow_{\beta})^{*}\ t\gamma$ by the induction hypothesis.

• •

If $s=Z\langle t_{1},\dots,t_{k}\rangle\ s_{1}\cdots s_{n}$ and $t_{i}\unrhd_{A}t$ for some $1\leq i\leq k$ with $(Z:i)\in A$, then we can write $\gamma(Z)=\lambda x_{1}\dots x_{n}.w$ (where $n\leq k$), and $s\gamma=w[x_{1}:=t_{1}\gamma,\dots,x_{n}:=t_{n}\gamma]\ (t_{n+1}\gamma)\cdots(t_{k}\gamma)$. Since $\gamma$ respects $A$, either $x_{i}$ occurs in $w$ or $i>n$; therefore $\gamma(Z)\mathbin{\hskip 1.0pt\underline{\blacktriangleright}\hskip 1.0pt}t_{i}\gamma$. We again complete by the induction hypothesis. ∎

In fact, the text is ambiguous regarding the definition of $\mathit{SDP}$ when an AFSM is not properly applied, since $\mathit{minar}(\mathtt{f})$ may not be uniquely defined. However, the result holds for any choice of $\mathit{minar}(\mathtt{f})$. In the following lemma, we only use that the elements of $\mathit{SDP}(\mathcal{R})$ are DPs $\mathtt{f}^{\sharp}\ \ell_{1}\cdots\ell_{k}\Rrightarrow\mathtt{g}^{\sharp}\ p_{1}\cdots p_{i}\ (A)$ where $\mathtt{f}^{\sharp}\ \ell_{1}\cdots\ell_{k}\Rightarrow r$ is a rule and there exist $p_{i+1}\dots p_{n}$ such that $r\unrhd_{A}\mathtt{g}\ p_{1}\cdots p_{n}$.

Lemma 17

For $\ell^{\sharp}\Rrightarrow p^{\sharp}\ (A)\in\mathit{SDP}(\mathcal{R})$ such that $\mathit{FMV}(p)\subseteq\mathit{FMV}(\ell)$, and substitution $\gamma$ on domain $\mathit{FMV}(\ell)$ such that $\gamma$ respects the meta-variable conditions in $A$: both $\ell\gamma$ and $p\gamma$ are terms and $\ell\gamma\ (\Rightarrow_{\mathcal{R}}\mathop{\cup}\rhd)^{+}\ p\gamma$.

Proof

By definition of $\mathit{SDP}$ and the fact that no fresh meta-variables occur on the right, there is a rule $\ell\Rightarrow r$ such that $p\ (A)\in\mathsf{cand}(r)$, so there are $r_{1},\dots,r_{n}$ such that $r\unrhd_{A}p\ r_{1}\cdots r_{n}$. Clearly, we have $\ell\gamma\Rightarrow_{\mathcal{R}}r\gamma$ by that rule, and $r\gamma\ (\rhd\mathop{\cup}\Rightarrow_{\mathcal{R}})^{*}\ (p\ r_{1}\cdots r_{n})\gamma\unrhd p\gamma$ by Lemma 16 (using that $\blacktriangleright$ is a sub-relation of $\rhd$). We are done because $\Rightarrow_{\beta}$ is included in $\Rightarrow_{\mathcal{R}}$. ∎

This allows us to draw the required conclusion:

Theorem 0.B.2

For any AFSM $(\mathcal{F},\mathcal{R})$: if there is an infinite $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-chain $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ with all $\rho_{i}$ conservative, then $\Rightarrow_{\mathcal{R}}$ is non-terminating.

Proof

Let $s_{i}^{\flat},t_{i}^{\flat}$ denote the terms $s_{i},t_{i}$ with all $\sharp$ marks removed. An infinite $(\mathit{SDP}(\mathcal{R}),\mathcal{R})$-dependency chain that does not use any DPs where fresh meta-variables are introduced on the right-hand side provides a sequence $(s_{i},t_{i})$ for $i\in\mathbb{N}$ such that for all $i$, $s_{i}^{\flat}\ (\Rightarrow_{\mathcal{R}}\mathop{\cup}\rhd)^{+}\ t_{i}^{\flat}$ (by Lemma 17), and $t_{i}^{\flat}\Rightarrow_{\mathcal{R}}^{*}s_{i+1}^{\flat}$. Thus, we obtain an infinite $\Rightarrow_{\mathcal{R}}\mathop{\cup}\rhd$ sequence, which provides an infinite $\Rightarrow_{\mathcal{R}}$ sequence due to monotonicity of $\Rightarrow_{\mathcal{R}}$. ∎

0.B.3 Original static dependency pairs

Since the most recent work on static dependency pairs has been defined for a polymorphic variation of the HRS formalism, it is not evident from sight how our definitions relate. Here, we provide context by showing how the definitions from [34, 46] apply to the restriction of HRSs that can be translated to AFSMs.

It should be noted that HRSs, as translated to AFSMs, should be seen as $\eta$-expanded rules; in practice, for $\ell\Rightarrow r$ we have that $\ell\mathbin{\hskip 1.0pt\underline{\blacktriangleright}\hskip 1.0pt}s$ or $r\mathbin{\hskip 1.0pt\underline{\blacktriangleright}\hskip 1.0pt}s$ implies that either $s$ is an abstraction, or $s$ has base type. This definition implies that the system is properly applied, but is much stronger. We will refer to this restriction as fully applied.

Definition 30

An AFSM $(\mathcal{F},\mathcal{R})$ is plain function passing following [34] if:

• •

for all rules $\mathtt{f}\ \ell_{1}\cdots\ell_{m}\Rightarrow r$ and all $Z\in\mathit{FMV}(r)$: if $Z$ does not have base type, then there are variables $x_{1},\dots,x_{n}$ and some $i$ such that $\ell_{i}=\lambda x_{1}\dots x_{n}.Z\langle x_{j_{1}},\dots,x_{j_{k}}\rangle$.

An AFSM $(\mathcal{F},\mathcal{R})$ is plain function passing following [46] if:

• •

for all rules $\mathtt{f}\ \ell_{1}\cdots\ell_{m}\Rightarrow r$ and all $Z\in\mathit{FMV}(r)$: there are some variables $x_{1},\dots,x_{k}$ and some $i\leq m$ such that $\ell_{i}\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}Z\langle x_{1},\dots,x_{k}\rangle$, where the relation $\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}$ is given by:

• –

$s\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}s$,

• –

$\lambda x.t\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}s$ if $t\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}s$,

• –

$x\ t_{1}\cdots t_{n}\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}s$ if $t_{i}\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}s$ for some $i$ with $x\in\mathcal{V}\setminus\mathit{FV}(t_{i})$

• –

$\mathtt{f}\ t_{1}\cdots t_{n}\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}s$ if $t_{i}\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}s$ for some $t_{i}$ of base type.555The authors of [46] refer to such subterms as accessible. We do not use this terminology, as it does not correspond to the accessibility notion in [8, 9] which we follow here. In particular, the accessibility notion we use considers the relation $\succeq^{\mathcal{S}}_{+}$, which corresponds to the positive/negative inductive types in [8, 9]. This is not used in [46].

In addition, in both cases right-hand sides of rules are assumed to be presented in $\beta$-normal form and are fully applied.

The definitions of PFP in [34, 46] also capture some non-pattern HRSs, but these cannot be represented as AFSMs. Note that the key difference between $\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}$ and $\unrhd$ for patterns is that the former is not allowed to descend into a non-base argument of a function symbol. The same difference applies when comparing $\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}$ with $\unrhd_{\mathtt{acc}}$: $\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}$ also cannot descend into the accessible higher-order arguments.

Example 28

The rules from Ex. 1 are PFP following both definitions. The rules from Ex. 5 are PFP following [46] but not following [34]. The rules from Ex. 2 are not PFP in either definition, since $\mathtt{lim}\ F\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}F$ does not hold (although they are AFP).

For a PFP AFSM, static dependency pairs are then defined as pairs $\ell^{\sharp}\Rrightarrow\mathtt{f}^{\sharp}\ p_{1}\cdots p_{m}$. This allows for a very simple notion of chains, even closer to the one in the first-order setting than our Def. 17.

Definition 31

A static dependency chain following [34, 46] is an infinite sequence $[(\ell_{0}\Rrightarrow p_{0},\gamma_{0}),(\ell_{1}\Rrightarrow p_{1},\gamma_{1}),\ldots]$ where $p_{i}\gamma_{i}\Rightarrow_{\mathcal{R}}^{*}\ell_{i+1}\gamma_{i+1}$ for all $i$. It is minimal if each $p_{i}\gamma_{i}$ is terminating under $\Rightarrow_{\mathcal{R}}$.

Both papers present a counterpart of Theorems 4.1 and 0.B.3 that roughly translates to the following:

Theorem 0.B.1 ([34, 46])

Let $\mathcal{R}$ be plain function passing following either definition in Def. 30. Let $\mathcal{P}=\{\ell^{\sharp}\Rrightarrow\mathtt{f}^{\sharp}\ p_{1}\cdots p_{m}\mid\ell\Rightarrow r\in\mathcal{R}\wedge r\unrhd\mathtt{f}\ p_{1}\cdots p_{m}\wedge\mathtt{f}\in\mathcal{D}\wedge m=\mathit{arity}(\mathtt{f})\}$. If $\Rightarrow_{\mathcal{R}}$ is non-terminating, then there is an infinite minimal static dependency chain with all $\ell_{i}\Rrightarrow p_{i}\in\mathcal{P}$.

Note that the chains are proved minimal, but not computable (which is a new definition in the current paper).

However, there is no counterpart to Thm. 0.B.2: this result relies on the presence of meta-variable conditions, which are not present in the static DPs from the literature.

Note that $\unrhd_{\mathtt{acc}}$ corresponds to $\unrhd_{\mathtt{safe}}^{\text{\tiny\cite[cite]{[\@@bibref{}{suz:kus:bla:11}{}{}]}}}$ (from Def. 30) if $\succeq^{\mathcal{S}}$ equates all sorts (as then always $\mathit{Acc}(\mathtt{f})=\{$ the indices of all base type arguments of $\mathtt{f}\}$). Thus, Def. 11 includes both notions from Def. 30.

Appendix 0.C Dependency pair processors

In this appendix, we prove the soundness – and where applicable completeness – of all DP processors defined in the text.

We first observe:

Lemma 18

If $\mathit{Proc}$ maps every DP problem to a set of problems such that for all $(\mathcal{P}^{\prime},\mathcal{R}^{\prime},m^{\prime},f^{\prime})\in\mathit{Proc}(\mathcal{P},\mathcal{R},m,f)$ we have that $\mathcal{P}^{\prime}\subseteq\mathcal{P}$, $\mathcal{R}^{\prime}\subseteq\mathcal{R}$, $m^{\prime}\succeq m$ and $f^{\prime}=f$, then $\mathit{Proc}$ is complete.

Proof

$\mathit{Proc}(\mathcal{P},\mathcal{R},m,f)$ is never NO. Suppose $\mathit{Proc}(\mathcal{P},\mathcal{R},m,f)$ contains an infinite element $(\mathcal{P}^{\prime},\mathcal{R}^{\prime},m^{\prime},f^{\prime})$; we must prove that then $(\mathcal{P},\mathcal{R},m,f)$ is infinite as well. This is certainly the case if $\Rightarrow_{\mathcal{R}}$ is non-terminating, so assume that $\Rightarrow_{\mathcal{R}}$ is terminating. Then certainly $\Rightarrow_{\mathcal{R}^{\prime}}\mathop{\subseteq}\Rightarrow_{\mathcal{R}}$ is terminating as well, so $(\mathcal{P}^{\prime},\mathcal{R}^{\prime},m^{\prime},f^{\prime})$ can be infinite only because there exists an infinite $(\mathcal{P}^{\prime},\mathcal{R}^{\prime})$-chain that is ${\mathcal{U}}$-computable if $m^{\prime}=\mathtt{computable}_{\mathcal{U}}$, minimal if $m^{\prime}=\mathtt{minimal}$ and formative if $f^{\prime}=\mathtt{formative}$. By definition, this is also a $(\mathcal{P},\mathcal{R})$-dependency chain, which is formative if $f=f^{\prime}=\mathtt{formative}$. Since $\Rightarrow_{\mathcal{R}}$ is terminating, this chain is also minimal. If we have $m=\mathtt{computable}_{\mathcal{U}}$, then also $m^{\prime}=\mathtt{computable}_{\mathcal{U}}$ (since $\mathtt{computable}_{\mathcal{U}}$ is maximal under $\succeq$) and the chain is indeed ${\mathcal{U}}$-computable. ∎

0.C.1 The dependency graph

The dependency graph processor lets us split a DP problem into multiple smaller ones. To prove soundness of its main processor, we first prove a helper result.

Lemma 19

Let $M=(\mathcal{P},\mathcal{R},m,f)$ and $G_{\theta}$ an approximation of its dependency graph. Then for every infinite $M$-chain $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ there exist $n\in\mathbb{N}$ and a cycle $C$ in $G_{\theta}$ such that for all $i>n$: $\theta(\rho_{i})\in C$.

Proof

We claim (**): for all $i\in\mathbb{N}$, there is an edge from $\theta(\rho_{i})$ to $\theta(\rho_{i+1})$. By definition of approximation, the claim follows if $DG$ has an edge from $\rho_{i}$ to $\rho_{i+1}$. But this is obvious: by definition of a chain, if $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ is a dependency chain, then so is $[(\rho_{i},s_{i},t_{i}),(\rho_{i+1},s_{i+1},t_{i+1})]$.

Now, having (), the chain traces an infinite path in $G_{\theta}$. Let $C$ be the set of nodes that occur infinitely often on this path; then for every node $d$ that is not in $C$, there is an index $n_{d}$ after which $\theta(\rho_{i})$ is never $d$ anymore. Since $G_{\theta}$ is a finite graph, we can take $n:=\max(\{n_{d}\mid d$ a node in $G_{\theta}\wedge d\notin C\})$. Now for every pair $d,b\in C$: because they occur infinitely often, there is some $i>n$ with $\theta(\rho_{i})=d$ and there is $j>i$ with $\theta(\rho_{j})=b$. Thus, by () there is a path in $G_{\theta}$ from $d$ to $b$. Similarly, there is a path from $b$ to $d$. Hence, they are on a cycle. ∎

Note that to find a chain with all $\theta(\rho_{i})\in C$, we do not need to modify the original chain at all: the satisfying chain is a tail of the original chain. Hence, the same flags apply to the resulting chain. This makes it very easy to prove correctness of the main processor:

Theorem 0.C.1 (Dependency graph processor)

The processor $\mathit{Proc}_{G_{\theta}}$ that maps a DP problem $M=(\mathcal{P},\mathcal{R},m,f)$ to $\{(\{\rho\in\mathcal{P}\mid\theta(\rho)\in C_{i}\},\mathcal{R},m,f)\mid 1\leq i\leq n\}$ if $G_{\theta}$ is an approximation of the dependency graph of $M$ and $C_{1},\dots,C_{n}$ are the (nodes of the) non-trivial strongly connected components (SCCs) of $G_{\theta}$, is both sound and complete.

Proof

Completeness follows by Lemma 18. Soundness follows because if $(\mathcal{P},\mathcal{R},m,\linebreak f)$ admits an infinite chain, then by Lemma 19 there is a cycle $C$ such that a tail of this chain is mapped into $C$. Let $C^{\prime}$ be the strongly connected component in which $C$ lies, and $\mathcal{P}^{\prime}=\{\rho\in\mathcal{P}\mid\theta(\rho)\in C^{\prime}\}$. Then clearly the same tail lies in $\mathcal{P}^{\prime}$, giving an infinite $(\mathcal{P}^{\prime},\mathcal{R},m,f)$-chain, and $(\mathcal{P}^{\prime},\mathcal{R},m,f)$ is one of the elements of the set returned by the dependency graph processor. ∎

The dependency graph processor is essential to prove termination in our framework because it is the only processor defined so far that can map a DP problem to $\emptyset$.

0.C.2 Processors based on reduction triples

Theorem 0.C.2 (Basic reduction triple processor)

Let $M=(\mathcal{P}_{1}\uplus\mathcal{P}_{2},\mathcal{R},m,\linebreak f)$ be a DP problem. If $(\succsim,\succcurlyeq,\succ)$ is a reduction triple such that

for all $\ell\Rightarrow r\in\mathcal{R}$, we have $\ell\succsim r$; 2. 2.

for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$, we have $\ell\succ p$; 3. 3.

for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{2}$, we have $\ell\succcurlyeq p$;

then the processor that maps $M$ to $\{(\mathcal{P}_{2},\mathcal{R},m,f)\}$ is both sound and complete.

Proof

Completeness follows by Lemma 18. Soundness follows because every infinite $(\mathcal{P}_{1}\uplus\mathcal{P}_{2},\mathcal{R})$-chain $[(\rho_{0},s_{0},t_{0}),(\rho_{1},s_{1},t_{1}),\ldots]$ with $\mathcal{P}_{1},\mathcal{P}_{2},\mathcal{R}$ satisfying the given properties induces an infinite $\succ\cup\succcurlyeq\cup\succsim$ sequence, and every occurrence of a DP in $\mathcal{P}_{1}$ in the chain corresponds to a $\succ$ step in the sequence. By compatibility of the relations, well-foundedness guarantees that there can only be finitely many such steps, so there exists some $n$ such that $[(\rho_{n},s_{n},t_{n}),(\rho_{n+1},s_{n+1},t_{n+1}),\ldots]$ is an infinite $(\mathcal{P}_{2},\mathcal{R})$-chain.

To see that we indeed obtain the sequence, let $i\in\mathbb{N}$. Denote $\rho_{i}:=\ell\Rrightarrow\ p\ (A)$, and let $\gamma$ be a substitution on domain $\mathit{FMV}(\ell)\cup\mathit{FMV}(p)$ such that $s_{i}=\ell\gamma$ and $t_{i}=p\gamma$. Meta-stability gives us that $s_{i}=\ell\gamma\ (\succcurlyeq\cup\succ)\ p\gamma=t_{i}$. As $\Rightarrow_{\mathcal{R}}$ is included in $\succsim$ by meta-stability and monotonicity, and because $t_{i}\Rightarrow_{\mathcal{R}}^{*}s_{i+1}$, we have $t_{i}\succsim s_{i+1}$. Thus, $s_{i}(\succcurlyeq\cup\succ)\cdot\succsim s_{i+1}$. Moreover, a $\succ$ step is used if $\rho_{i}\in\mathcal{P}_{1}$. ∎

Now that we have seen a basic processor using reduction triples, soundness of the base-type processor presented in the text follows easily.

Theorem 0.C.3 (Reduction triple processor)

Let $\mathsf{Bot}$ be a set $\{\bot_{\sigma}:\sigma\mid$ $\sigma\text{ a type}\}\subseteq\mathcal{F}^{\sharp}$ of unused constructors, $M=(\mathcal{P}_{1}\uplus\mathcal{P}_{2},\mathcal{R},m,f)$ a DP problem and $(\succsim,\succcurlyeq,\succ)$ a reduction triple such that: (a) for all $\ell\Rightarrow r\in\mathcal{R}$, we have $\ell\succsim r$; and (b) for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}\uplus\mathcal{P}_{2}$ with $\ell:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ and $p:\tau_{1}\rightarrow\dots\rightarrow\tau_{n}\rightarrow\kappa$ we have, for fresh meta-variables $Z_{1}:\sigma_{1},\dots,Z_{m}:\sigma_{m}$:

• •

$\ell\ Z_{1}\cdots Z_{m}\succ p\ \bot_{\tau_{1}}\cdots\bot_{\tau_{n}}$* if $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$*

• •

$\ell\ Z_{1}\cdots Z_{m}\succcurlyeq p\ \bot_{\tau_{1}}\cdots\bot_{\tau_{n}}$* if $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{2}$*

Then the processor that maps $M$ to $\{(\mathcal{P}_{2},\mathcal{R},m,f)\}$ is both sound and complete.

Proof

Completeness follows by Lemma 18. Soundness follows by soundness of Thm. 0.C.2: let $(\succsim,\succcurlyeq,\succ)$ be a reduction triple satisfying the requirements above, and for $R\in\{\succcurlyeq,\succ\}$ define $R^{\prime}$ as follows: for $s:\sigma_{1}\rightarrow\dots\rightarrow\sigma_{m}\rightarrow\iota$ and $t:\tau_{1}\rightarrow\dots\rightarrow\tau_{n}\rightarrow\kappa$, let $s\ R^{\prime}\ t$ if for all $u_{1}:\sigma_{1},\dots,u_{m}:\sigma_{m}$ there exist $w_{1}:\tau_{1},\dots,w_{n}:\tau_{n}$ such that $s\ u_{1}\cdots u_{m}\ R\ t\ w_{1}\cdots w_{n}$. We claim that $(\succsim,\succcurlyeq^{\prime},\succ^{\prime})$ is a reduction triple satisfying the requirements of Thm. 0.C.2, which implies soundness of the present processor.

It is clear that $\succcurlyeq^{\prime}$ and $\succ^{\prime}$ satisfy the requirements of Thm. 0.C.2: if $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$, then for any $u_{1},\dots,u_{m}$ we let $w_{1}:=\bot_{\tau_{1}},\dots,w_{n}:=\bot_{\tau_{n}}$ and have $\ell\ u_{1}\cdots u_{m}\succ p\ w_{1}\cdots w_{n}$ by meta-stability of $\succ$; the same holds for $\succcurlyeq$. It remains to be seen that $\succ^{\prime}$ and $\succcurlyeq^{\prime}$ are both transitive and meta-stable, that $\succcurlyeq^{\prime}$ is reflexive and that $\succ^{\prime}$ is well-founded.

• •

Meta-stability: given that $\ell\succ^{\prime}p$ and $\gamma$ is a substitution on domain $\mathit{FMV}(\ell)\cup\mathit{FMV}(p)$, we must see that $\ell\gamma\succ^{\prime}p\gamma$ (the case for $\succcurlyeq^{\prime}$ follows in the same way). Let $u_{1},\dots,u_{m}$ be arbitrary terms and $\delta:=\gamma\cup[Z_{1}:=u_{1},\dots,Z_{m}:=u_{m}]$; then $(\ell\ Z_{1}\cdots Z_{m})\delta\succ(p\ \bot_{\tau_{1}}\cdots\bot_{\tau_{n}})\delta$, so indeed $\ell\delta=\ell\gamma\succ^{\prime}p\gamma$.

• •

Transitivity: if $s\succ t\succ v$ then for all $\vec{u}$ there exist $\vec{w}$ such that $s\ \vec{u}\succ t\ \vec{w}$, and for all $\vec{w}$ there exist $\vec{q}$ such that $t\ \vec{w}\succ v\ \vec{q}$; thus, also $s\ \vec{u}\succ v\ \vec{q}$. The case for $\succcurlyeq$ is similar.

• •

Reflexivity of $\succcurlyeq^{\prime}$: always $s\succcurlyeq^{\prime}s$ since for all $u_{1},\dots,u_{m}$ we have $s\ \vec{u}\succcurlyeq s\ \vec{u}$.

• •

Well-foundedness of $\succ^{\prime}$: suppose $s_{1}\succ^{\prime}s_{2}\succ^{\prime}\dots$ and let $\vec{u_{1}}$ be a sequence of variables; we find $\vec{u_{2}},\vec{u_{3}},\dots$ such that $s_{1}\ \vec{u_{1}}\succ^{\prime}s_{2}\ \vec{u_{2}}\succ^{\prime}\dots$ as in the case for transitivity. ∎

0.C.3 Rule removal without search for orderings

There is very little to prove: the importance is in the definition.

Theorem 0.C.5 (Formative rules processor)

For a formative rules approximation $\mathit{FR}$, the processor $\mathit{Proc}_{\mathit{FR}}$ that maps a DP problem $(\mathcal{P},\mathcal{R},m,\mathtt{formative})$ to $\{(\mathcal{P},\mathit{FR}(\mathcal{P},\mathcal{R}),m,\mathtt{formative})\}$ is both sound and complete.

Proof

Completeness follows by Lemma 18. Soundness follows by definition of a formative rules approximation (a formative infinite $(\mathcal{P},\mathcal{R})$-dependency chain can be built using only rules in $\mathit{FR}(\mathcal{P},\mathcal{R})$). ∎

The practical challenge lies in proving that a given formative rules approximation really is one. The definition of a good approximation function is left to future work.

0.C.4 Subterm criterion processors

Next, we move on to the subterm processors. We first present the basic one – which differs little from its first-order counterpart, but is provided for context.

Theorem 0.C.6 (Subterm criterion processor)

The processor $\mathit{Proc}_{\mathtt{subcrit}}$ that maps a DP problem $(\mathcal{P}_{1}\uplus\mathcal{P}_{2},\mathcal{R},m,f)$ with $m\succeq\mathtt{minimal}$ to $\{(\mathcal{P}_{2},\mathcal{R},m,f)\}$ if a projection function $\nu$ exists such that $\overline{\nu}(\ell)\rhd\overline{\nu}(p)$ for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$ and $\overline{\nu}(\ell)=\overline{\nu}(p)$ for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{2}$, is sound and complete.

Proof

Completeness follows by Lemma 18. Soundness follows because an infinite $(\mathcal{P},\mathcal{R},m,f)$-chain with the properties above induces an infinite sequence $\overline{\nu}(s_{0})\unrhd\overline{\nu}(t_{0})\Rightarrow_{\mathcal{R}}^{*}\overline{\nu}(s_{1})\unrhd\overline{\nu}(t_{1})\Rightarrow_{\mathcal{R}}^{*}\dots$. Since the chain is minimal (either because $m=\mathtt{minimal}$, or by Lemma 15 if $m=\mathtt{computable}_{\mathcal{U}}$), $\overline{\nu}(p_{0})$ is terminating, and therefore it is terminating under $\Rightarrow_{\mathcal{R}}\mathop{\cup}\rhd$. Thus, there is some index $n$ such that for all $i\geq n$: $\overline{\nu}(s_{i})=\overline{\nu}(t_{i})=\overline{\nu}(s_{i+1})$. But this can only be the case if $\overline{\nu}(\ell_{i})=\overline{\nu}(p_{i})$. But then the tail of the chain starting at position $n$ does not use any pair in $\mathcal{P}_{1}$, and is therefore an infinite $(\mathcal{P}_{2},\mathcal{R},m,f)$-chain. ∎

We now turn to the proof of the computable subterm criterion processor. This proof is very similar to the one for the normal subterm criterion, but it fundamentally uses the definition of a computable chain.

Theorem 0.C.7 (Computable subterm criterion processor)

The processor $\mathit{Proc}_{\mathtt{statcrit}}$ that maps a DP problem $(P_{1}\uplus\mathcal{P}_{2},\mathcal{R},\mathtt{computable}_{\mathcal{U}},f)$ to $\{(\mathcal{P}_{2},\mathcal{R},\linebreak\mathtt{computable}_{\mathcal{U}},f)\}$ if a projection function $\nu$ exists such that $\overline{\nu}(\ell)\sqsupset\overline{\nu}(p)$ for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$ and $\overline{\nu}(\ell)=\overline{\nu}(p)$ for all $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{2}$, is sound and complete. Here, $\sqsupset$ is the relation on base-type terms with $s\sqsupset t$ if $s\neq t$ and (a) $s\unrhd_{\mathtt{acc}}t$ or (b) a meta-variable $Z$ exists with $s\unrhd_{\mathtt{acc}}Z\langle x_{1},\dots,x_{k}\rangle$ and $t=Z\langle t_{1},\dots,t_{k}\rangle\ s_{1}\cdots s_{n}$.

Proof

Completeness follows by Lemma 18. Soundness follows because, for $C:=C_{\mathcal{U}}$ the computability predicate corresponding to $\Rightarrow_{S}$, an infinite $(\mathcal{P},\mathcal{R},\linebreak\mathtt{computable}_{\mathcal{U}},f)$-chain induces an infinite $\Rrightarrow_{C}\cup\Rightarrow_{\mathcal{R}}$ sequence starting in the $C$-computable term $\overline{\nu}(s_{1})$, with always $s_{i}(\Rrightarrow_{C}\cup\Rightarrow_{\mathcal{R}})^{*}t_{i}$ if $\rho_{i}\in\mathcal{P}_{1}$ and $\overline{\nu}(s_{i})=\overline{\nu}(t_{i})$ if $\rho_{i}\in\mathcal{P}_{2}$; like in the proof of the subterm criterion, this proves that the chain has a tail that is a $(\mathcal{P}_{2},\mathcal{R},\mathtt{computable}_{\mathcal{U}},f)$-chain because, by definition of $C$, $\Rightarrow_{\mathcal{R}}\cup\Rrightarrow_{C}$ is terminating on $C$-computable terms.

It remains to be seen that we indeed have $\overline{\nu}(s_{i})\ (\Rrightarrow_{C}\cup\ \Rightarrow_{\mathcal{R}})^{+}\overline{\nu}(t_{i})$ whenever $\rho_{i}\in\mathcal{P}_{1}$. So suppose that $\rho$ is a dependency pair $\ell\Rrightarrow p\ (A)\in\mathcal{P}_{1}$ such that $\overline{\nu}(\ell)\sqsupset\overline{\nu}(p)$; we must see that $\overline{\nu}(\ell\gamma)\ (\Rrightarrow_{C}\cup\Rightarrow_{\beta})^{+}\overline{\nu}(p\gamma)$ for any substitution $\gamma$ on domain $\mathit{FMV}(\ell)\cup\mathit{FMV}(r)$ such that $v\gamma$ is $C$-computable for all $v,B$ such that $r\unrhd_{B}v$ and $\gamma$ respects $B$.

Write $\ell=\mathtt{f}\ \ell_{1}\cdots\ell_{k}$ and $p=\mathtt{g}\ p_{1}\cdots p_{n}$; then $\overline{\nu}(\ell\gamma)=\ell_{\nu(\mathtt{f})}\gamma$ and $\overline{\nu}(p\gamma)=p_{\nu(\mathtt{g})}\gamma$. Since, by definition of a dependency pair, $\ell$ is closed, we also have $\mathit{FV}(\ell_{\nu(\mathtt{f})})=\emptyset$. Consider the two possible reasons why $\ell_{\nu(\mathtt{f})}\sqsupset p_{\nu(\mathtt{g})}$.

• •

$\ell_{\nu(\mathtt{f})}\unrhd_{\mathtt{acc}}p_{\nu(\mathtt{g})}$: since both sides have base type by assumption and $\ell_{\nu(\mathtt{f})}$ is closed, by Lemma 8 also $\ell_{\nu(\mathtt{f})}\gamma\ (\Rrightarrow_{C}\cup\Rightarrow_{\beta})^{*}p_{\nu(\mathtt{g})}\gamma$.

• •

$\ell_{\nu(\mathtt{f})}\unrhd_{\mathtt{acc}}Z\langle x_{1},\dots,x_{k}\rangle$ and $p_{\nu(\mathtt{g})}=Z\langle u_{1},\dots,u_{k}\rangle\ v_{1}\cdots v_{n}$: denote $\gamma(Z)=\lambda x_{1}\dots x_{k}.q$ and also $\gamma(Z)\approx_{k}\lambda x_{1}\dots x_{k}.q^{\prime}$. Then we can write $q=\linebreak\lambda x_{k+1}\dots x_{i}.q^{\prime\prime}$ as well as $q^{\prime}=q^{\prime\prime}\ x_{i+1}\cdots x_{k}$ for some $k\leq i\leq k$. Moreover:

[TABLE]

By definition of an ${\mathcal{U}}$-computable chain, $v_{j}\gamma$ is computable for each $1\leq j\leq n$, and $u_{j}\gamma$ is computable for each $1\leq j\leq k$ such that $x_{j}\in\mathit{FV}(q^{\prime})$. Write $v_{j}^{\prime}:=v_{j}\gamma$ and let $u_{j}^{\prime}:=u_{j}\gamma$ if $x_{j}\in\mathit{FV}(q^{\prime})$, otherwise $u_{j}^{\prime}:=$ a fresh variable; then all $u_{j}^{\prime}$ and $v_{j}^{\prime}$ are computable, and still:

[TABLE]

On the other hand, by Lemma 8 and the observation that $\mathit{FV}(\ell_{\nu(\mathtt{f})})=\emptyset$, we have $\ell_{\nu(\mathtt{f})}\gamma\ (\Rrightarrow_{C}\cup\Rightarrow_{\beta})^{+}\ q[x_{1}:=u_{1}^{\prime},\dots,x_{k}:=u_{k}^{\prime}]\ u_{k+1}^{\prime}\cdots u_{k}^{\prime}\ v_{1}^{\prime}\cdots v_{n}^{\prime}$, and as $q=\lambda x_{k+1}\dots x_{i}.q^{\prime\prime}$ this term $\beta$-reduces to $q^{\prime\prime}[x_{1}:=u_{1}^{\prime},\dots,x_{i}:=u_{i}^{\prime}]\ u_{i+1}^{\prime}\cdots u_{k^{\prime}}^{\prime}\ v_{1}^{\prime}\cdots v_{n}^{\prime}=p_{\nu(\mathtt{g})}\gamma$. ∎

0.C.5 Non-termination

Soundness and completeness of the non-termination processor in Thm. 5.8 are both direct consequences of Def. 20 and Def. 21.

Appendix 0.D Experimental results

Finally, while the main paper focuses on a theoretical exposition, we here present an experimental evaluation of the results in this paper. The work has been implemented in the second author’s termination tool WANDA, using higher-order polynomial interpretations [15] and a recursive path ordering [29, Chapter 5] for reduction triples. Both methods rely on an encoding of underlying constraints into SAT. The search for a sort ordering, and a projection function for the subterm criterion, is also delegated to SAT. The non-termination processor has not been implemented (WANDA performs some loop analysis, but outside the DP framework; this is a planned future improvement), and the subterm criterion processor has been merged with the computable subterm criterion processor.

In addition to the results in this paper, WANDA includes a search for monotonic termination orderings outside the DP framework (using successive rule removal), a dynamic DP framework (following [31]), and a mechanism [14] within both DP frameworks to delegate some first-order parts of the AFSM to a first-order termination tool (here we use AProVE [19]).

We have evaluated the power of our techniques on the Termination Problems Database [49], version 10.5. Of the 198 benchmarks in the category Higher Order Union Beta, 153 are accessible function passing. Comparing the power of static DPs versus dynamic DPs or no DP framework gives the following results (where Time is the average runtime on success in seconds):

[TABLE]

While static DPs have a slightly lower success rate than dynamic DPs, their evaluation is much faster, since they allow for greater modularity: the dynamic setting includes dependency pairs where the right-hand does not have a (marked) defined symbol at the head (e.g., $\mathtt{map}\ F\ (\mathtt{cons}\ H\ T)\Rrightarrow F\ H$), which make both the subterm criterion processor and the dependency graph processor harder to apply. The combination of static and dynamic DPs performs substantially better than either style alone: although the gains can be seen as modest if the size of the data set is not taken into account (153 versus 166 YES+NO, giving an 8% increase), the numbers indicate a 29% decrease in failure rate (from 45 to 32).

We have also compared the individual techniques in this paper by disabling them from the second test above. This gives the table below:

[TABLE]

Note that none of the techniques individually give much power except for reduction triples: where one method is disabled, another can typically pick up the slack. If all processors except reduction triples are disabled, only 105 benchmarks are proved. Most processors do individually give a significant speedup. Only formative rules does not; this processor is useful in the dynamic setting, but does not appear to be so here.

Evaluation pages for these and further experiments are available at:

https://www.cs.ru.nl/~cynthiakop/experiments/esop19/