An Innermost DP Framework for Constrained Higher-Order Rewriting

Fuhs, Carsten; Guo, Liye; Kop, Cynthia

doi:10.4230/LIPIcs.FSCD.2025.20

An Innermost DP Framework for Constrained Higher-Order Rewriting

Carsten Fuhs

Birkbeck, University of London, UK Liye Guo

Radboud University, Nijmegen, The Netherlands Cynthia Kop

Radboud University, Nijmegen, The Netherlands

Abstract

Logically constrained simply-typed term rewriting systems (LCSTRSs) are a higher-order formalism for program analysis with support for primitive data types. The termination problem of LCSTRSs has been studied so far in the setting of full rewriting. This paper modifies the higher-order constrained dependency pair framework to prove innermost termination, which corresponds to the termination of programs under call by value. We also show that the notion of universal computability with respect to innermost rewriting can be effectively handled in the modified, innermost framework, which lays the foundation for open-world termination analysis of programs under call by value via LCSTRSs.

Keywords and phrases:

Higher-order term rewriting, constrained rewriting, innermost termination, call by value, open-world analysis, dependency pairs

Funding:

Liye Guo: NWO VI.Vidi.193.075, project “CHORPE”.

Cynthia Kop: NWO VI.Vidi.193.075, project “CHORPE”.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Equational logic and rewriting ; Theory of computation

\rightarrow

Logic and verification

Supplementary Material:

Software (Source Code): https://github.com/hezzel/cora [27]

Software (Source Code): https://zenodo.org/records/15318964 [28]

Acknowledgements:

We thank the reviewers for helpful comments that allowed us to improve the presentation.

DOI:

10.4230/LIPIcs.FSCD.2025.20

Event:

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Editors:

Maribel Fernández

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

In the study of term rewriting, termination has been an active area of research for decades. Hundreds of different termination techniques have been developed, along with a variety of (fully automatic) termination analyzers that compete against each other in an annual competition [6]. Many of those techniques have been adapted to different styles of term rewriting (e.g., context-sensitive, relative, constrained and higher-order).

In a recent work [22], we have introduced logically constrained simply-typed term rewriting systems (LCSTRSs): a variant of term rewriting that incorporates both higher-order terms and primitive data types such as integers and bit vectors. This formalism is proposed to be a stepping stone toward functional programming languages: by adapting analysis techniques from traditional term rewriting to LCSTRSs, we obtain many of the ingredients needed by the analysis of functional programs, without limiting ourselves to a particular language.

Our long-term goal is to use LCSTRSs as an intermediate verification language in a two-step process to prove correctness properties (e.g., termination, reachability and equivalence) of a program $P$ written in a real-world programming language with higher-order features (e.g., OCaml and Scala): (1) soundly translate $P$ to an LCSTRS $\mathcal{R}_{P}$ (i.e., if $\mathcal{R}_{P}$ is, say, terminating, then so is $P$ ), and (2) analyze $\mathcal{R}_{P}$ . This approach has been successfully applied across paradigms to multiple languages, such as Prolog [44, 17], Haskell [16], Java [39] and C [14], via various flavors of term rewriting. We consider LCSTRSs a highly suitable intermediate language that allows for a direct representation of many programming language features. We particularly study termination, both for its own relevance, and due to the fact that it allows the reduction relation to be used as a decreasing measure in induction, which is a powerful aid to proving many other properties.

Most modern termination techniques for term rewriting are defined within the dependency pair (DP) framework [3, 18], which essentially studies groups of recursive function calls. In [21], a higher-order variant of this framework [35, 36, 34, 13] has been adapted to LCSTRSs, and its usefulness in open-world termination analysis has also been established through the notion of universal computability. However, this method still faces limitations: many commonly used DP processors (termination techniques within the DP framework) have not yet been extended to the higher-order and constrained setting, and whereas the first-order DP framework can deal with both full rewriting and innermost rewriting, most higher-order versions – including the one for LCSTRSs – only concern full rewriting. The incapability to handle innermost rewriting is particularly unfortunate since many functional languages use call-by-value evaluation, which largely corresponds to innermost rewriting.

In this paper, we define the first innermost DP framework for LCSTRSs. We shall present DP processors that explicitly benefit from innermost or call-by-value rewriting.

Contributions.

We start in Section 2 with the preliminaries on LCSTRSs and the notion of computability, which is fundamental to static dependency pairs. Then this paper’s contributions follow:

$\blacksquare$

In Section 3, we discuss the innermost and the call-by-value strategies, and present a transformation that allows us to better utilize the call-by-value setting.
$\blacksquare$

In Section 4, we recall the notion of a static dependency pair for LCSTRSs [21], and extend it by introducing call-by-value dependency pairs and innermost chains.
$\blacksquare$
In Section 5, we present an innermost DP framework, which can be used to prove innermost (and call-by-value) termination through the use of various DP processors. We first review three classes of existing DP processors defined for full rewriting, and see how they adapt to the innermost setting. Then we define three more, specifically for the innermost DP framework:
- –
  
  In Section 5.2, following the idea of chaining from first-order rewriting with integer constraints [10, 11, 15], we propose a class of DP processors that merge call-by-value dependency pairs. These DP processors can be particularly useful in the analysis of automatically generated systems, which often give rise to a large body of dependency pairs representing intermediate steps of computation.
- –
  
  In Section 5.3, we extend the idea of usable rules [3, 19, 24]. While this idea has been applied to higher-order rewriting [2, 40], logical constraints still pose challenges. In the innermost setting, we are able to define this class of DP processors in their most powerful form, which permanently removes rewrite rules from a DP problem.
- –
  
  In Section 5.4, we show how usable rules with respect to an argument filtering may be defined, and how this technique makes first-order reduction pairs applicable. This way a large number of first-order techniques can be employed for higher-order termination without a higher-order modification; to be applied to LCSTRSs, those reduction pairs only need to adapt to logical constraints.
$\blacksquare$

In Section 6, we discuss the notion of universal computability [21] with respect to innermost rewriting. We will see that the employment of usable rules significantly increases the potential of the innermost DP framework to analyze universal computability: now we can use fully-fledged reduction pair processors for open-world termination analysis, and thereby harness one of the main benefits of the DP framework in this practical setting.
$\blacksquare$

We have implemented all the results in our open-source analyzer Cora. The implementation and the evaluation thereof are described in Section 7.

2 Preliminaries

This section collects the preliminaries from the literature. First, we recall the definition of an LCSTRS [22].¹¹1In contrast to [22] and following [21], we assume that $\ell$ is a pattern in every rewrite rule ${\ell}\rightarrow{r}\ [\varphi]$ . For notational convenience, we also assume that $\operatorname{Var}(r)\setminus\operatorname{Var}(\ell)\subseteq\operatorname{% Var}(\varphi)$ , which can be guaranteed by a simple transformation and is also adopted in the second half of [22]. Then, we recollect from [13] the definition of computability (with accessibility), particularly under the strategies. We borrow several definitions from the phrasing in [21].

2.1 Logically Constrained STRSs

Terms Modulo Theories.

Given a non-empty set $\mathcal{S}$ of sorts (or base types), the set $\mathcal{T}$ of (simple) types over $\mathcal{S}$ is generated by the grammar $\mathcal{T}\Coloneqq\mathcal{S}\mid(\mathcal{T}\rightarrow\mathcal{T})$ . Right-associativity is assigned to $\rightarrow$ so we can omit some parentheses. Given disjoint sets $\mathcal{F}$ and $\mathcal{V}$ , whose elements we call function symbols and variables, respectively, the set $\mathfrak{T}$ of pre-terms over $\mathcal{F}$ and $\mathcal{V}$ is generated by the grammar $\mathfrak{T}\Coloneqq\mathcal{F}\mid\mathcal{V}\mid({\mathfrak{T}}\ {\mathfrak% {T}})$ . Left-associativity is assigned to the juxtaposition operation, called application, so for instance ${{t_{0}}\ {t_{1}}}\ {t_{2}}$ stands for $({({t_{0}}\ {t_{1}})}\ {t_{2}})$ .

We assume every function symbol and variable is assigned a unique type. Typing works as expected: if pre-terms $t_{0}$ and $t_{1}$ have types $A\rightarrow B$ and $A$ , respectively, ${t_{0}}\ {t_{1}}$ has type $B$ . The set $T(\mathcal{F},\mathcal{V})$ of terms over $\mathcal{F}$ and $\mathcal{V}$ consists of pre-terms that have a type. We write $t : A$ if a term $t$ has type $A$ . We assume there are infinitely many variables of each type.

The set $\operatorname{Var}(t)$ of variables in $t\in T(\mathcal{F},\mathcal{V})$ is defined by $\operatorname{Var}(\mathsf{f})=\emptyset$ for $\mathsf{f}\in\mathcal{F}$ , $\operatorname{Var}(x)=\{\,x\,\}$ for $x\in\mathcal{V}$ and $\operatorname{Var}({t_{0}}\ {t_{1}})=\operatorname{Var}(t_{0})\cup% \operatorname{Var}(t_{1})$ . A term $t$ is called ground if $\operatorname{Var}(t)=\emptyset$ .

For constrained rewriting, we make further assumptions. First, we assume there is a distinguished subset ${\mathcal{S}}_{\vartheta}$ of $\mathcal{S}$ , called the set of theory sorts. The grammar ${\mathcal{T}}_{\vartheta}\Coloneqq{\mathcal{S}}_{\vartheta}\mid({\mathcal{S}}_% {\vartheta}\rightarrow{\mathcal{T}}_{\vartheta})$ generates the set ${\mathcal{T}}_{\vartheta}$ of theory types over ${\mathcal{S}}_{\vartheta}$ . Note that a theory type is essentially a non-empty list of theory sorts. Next, we assume there is a distinguished subset ${\mathcal{F}}_{\vartheta}$ of $\mathcal{F}$ , called the set of theory symbols, and the type of every theory symbol is in ${\mathcal{T}}_{\vartheta}$ , which means the type of any argument passed to a theory symbol is a theory sort. Theory symbols whose type is a theory sort are called theory values.²²2Such theory symbols are simply called values in [22]. In this paper, we call them differently so that they are not to be confused with term values as in call by value. Elements of $T({\mathcal{F}}_{\vartheta},\mathcal{V})$ are called theory terms.

Theory symbols are interpreted in an underlying theory: given an ${\mathcal{S}}_{\vartheta}$ -indexed family of sets $(\mathfrak{X}_{A})_{A\in{\mathcal{S}}_{\vartheta}}$ , we extend it to a ${\mathcal{T}}_{\vartheta}$ -indexed family by letting $\mathfrak{X}_{A\rightarrow B}$ be the set of mappings from $\mathfrak{X}_{A}$ to $\mathfrak{X}_{B}$ ; an interpretation of theory symbols is a ${\mathcal{T}}_{\vartheta}$ -indexed family of mappings $([\![\cdot]\!]_{A})_{A\in{\mathcal{T}}_{\vartheta}}$ where $[\![\cdot]\!]_{A}$ assigns to each theory symbol of type $A$ an element of $\mathfrak{X}_{A}$ and is bijective if $A\in{\mathcal{S}}_{\vartheta}$ . Given an interpretation of theory symbols $([\![\cdot]\!]_{A})_{A\in{\mathcal{T}}_{\vartheta}}$ , we extend each indexed mapping $[\![\cdot]\!]_{B}$ to one that assigns to each ground theory term of type $B$ an element of $\mathfrak{X}_{B}$ by letting $[\![{t_{0}}\ {t_{1}}]\!]_{B}$ be $[\![t_{0}]\!]_{A\rightarrow B}([\![t_{1}]\!]_{A})$ . We write just $[\![\cdot]\!]$ when the type can be deduced.

Example 1.

Let ${\mathcal{S}}_{\vartheta}$ be $\{\,\mathsf{int}\,\}$ . Then $\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{int}$ is a theory type over ${\mathcal{S}}_{\vartheta}$ while $(\mathsf{int}\rightarrow\mathsf{int})\rightarrow\mathsf{int}$ is not. Let ${\mathcal{F}}_{\vartheta}$ be $\{\,-\,\}\cup\mathbb{Z}$ where ${-}:\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{int}$ and $n:\mathsf{int}$ for all $n\in\mathbb{Z}$ . The theory values are the elements of $\mathbb{Z}$ . Let $\mathfrak{X}_{\mathsf{int}}$ be $\mathbb{Z}$ , $[\![\cdot]\!]_{\mathsf{int}}$ be the identity mapping and $[\![-]\!]$ be the mapping $\lambda{m}.\,\lambda{n}.\,m-n$ . The interpretation of ${(-)}\ {1}$ is the mapping $\lambda{n}.\,1-n$ (note that functions in our setting are curried).

Type-preserving mappings from $\mathcal{V}$ to $T(\mathcal{F},\mathcal{V})$ are called substitutions. The domain of a substitution $\sigma$ is the set $\operatorname{dom}(\sigma)=\{\,x\in\mathcal{V}\,|\,\sigma(x)\neq x\,\}$ . Let $[{x_{1}}\coloneq{t_{1}},\ldots,{x_{n}}\coloneq{t_{n}}]$ denote the substitution $\sigma$ such that $\operatorname{dom}(\sigma)\subseteq\{\,{x}_{1},\ldots,{x}_{n}\,\}$ and $\sigma(x_{i})=t_{i}$ for all $i$ . Every substitution $\sigma$ extends to a type-preserving mapping $\bar{\sigma}$ from $T(\mathcal{F},\mathcal{V})$ to $T(\mathcal{F},\mathcal{V})$ . We write $t\sigma$ for $\bar{\sigma}(t)$ and define it as follows: $\mathsf{f}\sigma=\mathsf{f}$ for $\mathsf{f}\in\mathcal{F}$ , $x\sigma=\sigma(x)$ for $x\in\mathcal{V}$ and $({t_{0}}\ {t_{1}})\sigma={(t_{0}\sigma)}\ {(t_{1}\sigma)}$ .

A context is a term containing a hole. That is, if we let $\square$ be a special symbol and assign to it a type $A$ , a context ${C}[]$ is an element of $T(\mathcal{F},\mathcal{V}\cup\{\,\square\,\})$ such that $\square$ occurs in ${C}[]$ exactly once. Given a term $t : A$ , let ${C}[t]$ denote the term produced by replacing $\square$ in ${C}[]$ with $t$ .

A term $t$ is called a (maximally applied) subterm of a term $s$ , written as $s\trianglerighteq t$ , if either $s=t$ , $s={s_{0}}\ {s_{1}}$ where $s_{1}\trianglerighteq t$ , or $s={s_{0}}\ {s_{1}}$ where $s_{0}\trianglerighteq t$ and $s_{0}\neq t$ ; i.e., $s={C}[t]$ for ${C}[]$ that is not of form ${C^{\prime}}[{\square}\ {t_{1}}]$ . We write $s\vartriangleright t$ and call $t$ a proper subterm of $s$ if $s\trianglerighteq t$ and $s\neq t$ .

Constrained Rewriting.

Constrained rewriting requires the theory sort $\mathsf{bool}$ : we henceforth assume that $\mathsf{bool}\in{\mathcal{S}}_{\vartheta}$ , $\{\,\mathfrak{f},\mathfrak{t}\,\}\subseteq{\mathcal{F}}_{\vartheta}$ , $\mathfrak{X}_{\mathsf{bool}}=\{\,0,1\,\}$ , $[\![\mathfrak{f}]\!]_{\mathsf{bool}}=0$ and $[\![\mathfrak{t}]\!]_{\mathsf{bool}}=1$ . Moreover, we require that ${\mathcal{F}}_{\vartheta}$ includes symbols $\wedge:\mathsf{bool}\rightarrow\mathsf{bool}\rightarrow\mathsf{bool}$ , and for each sort $A\in{\mathcal{S}}_{\vartheta}$ also a symbol $\equiv_{A}:A\rightarrow A\rightarrow\mathsf{bool}$ , interpreted respectively as conjunction and equality operators.

A logical constraint is a theory term $\varphi$ such that $\varphi$ has type $\mathsf{bool}$ and the type of each variable in $\operatorname{Var}(\varphi)$ is a theory sort. A (constrained) rewrite rule is a triple ${\ell}\rightarrow{r}\ [\varphi]$ where $\ell$ and $r$ are terms which have the same type, $\varphi$ is a logical constraint, $\operatorname{Var}(r)\setminus\operatorname{Var}(\ell)\subseteq\operatorname{% Var}(\varphi)$ , and $\ell$ is a pattern that takes the form ${\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for some $\mathsf{f}\in\mathcal{F}$ and contains at least one function symbol in $\mathcal{F}\setminus{\mathcal{F}}_{\vartheta}$ . Here a pattern is a term whose subterms are either ${\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for some $\mathsf{f}\in\mathcal{F}$ or a variable.³³3As usual in term rewriting, we do not require that each variable occurs at most once in a pattern. A substitution $\sigma$ is said to respect a logical constraint $\varphi$ if $\sigma(x)$ is a theory value for all $x\in\operatorname{Var}(\varphi)$ and $[\![\varphi\sigma]\!]=1$ ; $\sigma$ respects the rule ${\ell}\rightarrow{r}\ [\varphi]$ if it respects $\varphi$ .

A logically constrained simply-typed term rewriting system (LCSTRS) collects the above data – $\mathcal{S}$ , ${\mathcal{S}}_{\vartheta}$ , $\mathcal{F}$ , ${\mathcal{F}}_{\vartheta}$ , $\mathcal{V}$ , $(\mathfrak{X}_{A})$ and $[\![\cdot]\!]$ – along with a set $\mathcal{R}$ of rewrite rules. We usually let $\mathcal{R}$ alone stand for the system. The set $\mathcal{R}$ induces the rewrite relation $\rightarrow_{\mathcal{R}}$ over terms: $t\rightarrow_{\mathcal{R}}t^{\prime}$ if and only if there exists a context ${C}[]$ such that one of the following holds:

(1)

$t={C}[\ell\sigma]$ and $t^{\prime}={C}[r\sigma]$ for some ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ and substitution $\sigma$ which respects $\varphi$ , or
(2)

$t={C}[{\mathsf{f}}\ {{v}_{1}\cdots{v}_{n}}]$ and $t^{\prime}={C}[v^{\prime}]$ for some theory symbol $\mathsf{f}$ and some theory values ${v}_{1},\ldots,{v}_{n},v^{\prime}$ with $n>0$ and $[\![{\mathsf{f}}\ {{v}_{1}\cdots{v}_{n}}]\!]=[\![v^{\prime}]\!]$ .

If $t\rightarrow_{\mathcal{R}}t^{\prime}$ due to the second condition, we also write $t\rightarrow_{\kappa}t^{\prime}$ and call it a calculation step. Theory symbols that are not a theory value are called calculation symbols. Let $t\,{\downarrow}_{\kappa}$ denote the (unique) $\kappa$ -normal form of $t$ , i.e., the term $t^{\prime}$ such that $t\rightarrow_{\kappa}^{*}t^{\prime}$ and $t^{\prime}\not\rightarrow_{\kappa}t^{\prime\prime}$ for any $t^{\prime\prime}$ . For example, $({\mathsf{f}}\ {(7*(3*2))})\,{\downarrow}_{\kappa}={\mathsf{f}}\ {42}$ if $\mathsf{f}$ is not a calculation symbol, or if $\mathsf{f}:\mathsf{int}\rightarrow A\rightarrow B$ .

A term $t$ is in normal form if there is no term $t^{\prime}$ such that $t\rightarrow_{\mathcal{R}}t^{\prime}$ . Given an LCSTRS $\mathcal{R}$ , the set $\mathcal{N}\!\mathcal{F}(\mathcal{R})$ contains all terms that are in normal form with respect to $\rightarrow_{\mathcal{R}}$ .

Given an LCSTRS $\mathcal{R}$ , $\mathsf{f}$ is called a defined symbol if there is at least one rewrite rule of the form ${{\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}}\rightarrow{r}\ [\varphi]$ . Let $\mathcal{D}$ denote the set of defined symbols. Theory values and function symbols in $\mathcal{F}\setminus({\mathcal{F}}_{\vartheta}\cup\mathcal{D})$ are called constructors.

Example 2.

Consider the following LCSTRS $\mathcal{R}$ , where $\mathsf{gcdlist}:\mathsf{intlist}\rightarrow\mathsf{int}$ , $\mathsf{fold}:(\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{int})% \rightarrow\mathsf{int}\rightarrow\mathsf{intlist}\rightarrow\mathsf{int}$ and $\mathsf{gcd}:\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{int}$ :

We use infix notation for some binary operators, and omit logical constraints that are $\mathfrak{t}$ . Here is a rewrite sequence: ${\mathsf{gcdlist}}\ {({{\mathsf{cons}}\ {(1+1)}}\ {\mathsf{nil}})}\rightarrow_% {\mathcal{R}}{{{\mathsf{fold}}\ {\mathsf{gcd}}}\ {0}}\ {({{\mathsf{cons}}\ {(1% +1)}}\ {\mathsf{nil}})}\rightarrow_{\mathcal{R}}{{\mathsf{gcd}}\ {(1+1)}}\ {({% {{\mathsf{fold}}\ {\mathsf{gcd}}}\ {0}}\ {\mathsf{nil}})}\rightarrow_{\mathcal% {R}}{{\mathsf{gcd}}\ {(1+1)}}\ {0}\rightarrow_{\kappa}{{\mathsf{gcd}}\ {2}}\ {% 0}\rightarrow_{\mathcal{R}}2$ .

Innermost Rewriting.

The innermost rewrite relation $\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}$ requires all the proper subterms of a redex to be in normal form: $t\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}t^{\prime}$ if and only if either (1) there exist a context ${C}[]$ , a substitution $\sigma$ and a rewrite rule ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ such that $t={C}[\ell\sigma]$ , $s\not\rightarrow_{\mathcal{R}}s^{\prime}$ for any proper subterm $s$ of $\ell\sigma$ and any $s^{\prime}$ , $t^{\prime}={C}[r\sigma]$ and $\sigma$ respects $\varphi$ , or (2) $t\rightarrow_{\kappa}t^{\prime}$ .

Similarly, for an LCSTRS $\mathcal{Q}$ we define the relation $\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}$ as reduction using $\rightarrow_{\mathcal{R}}$ where all proper subterms of a redex are in $\rightarrow_{\mathcal{Q}}$ -normal form: $t\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}t^{\prime}$ if and only if either (1) there exist ${C}[]$ , $\sigma$ and ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ such that $t={C}[\ell\sigma]$ , $s\not\rightarrow_{\mathcal{Q}}s^{\prime}$ for any proper subterm $s$ of $\ell\sigma$ and any $s^{\prime}$ , $t^{\prime}={C}[r\sigma]$ and $\sigma$ respects $\varphi$ , or (2) $t\rightarrow_{\kappa}t^{\prime}$ . Note that $\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}$ is the same as $\xrightarrow{\scriptscriptstyle\mathcal{R}}_{\mathcal{R}}$ .

Call-By-Value Rewriting.

We may further restrict a redex by requiring each proper subterm to be a ground term value. Here a term value is either a variable or a term ${\mathsf{f}}\ {{v}_{1}\cdots{v}_{n}}$ where $\mathsf{f}$ is a function symbol, $v_{i}$ is a term value for all $i$ , and (1) if there is a rule ${{\mathsf{f}}\ {{t}_{1}\cdots{t}_{k}}}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ , then $k>n$ ; (2) if $\mathsf{f}$ is a calculation symbol, then it takes at least $n+1$ arguments (i.e., $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n+1}\rightarrow B$ ). In this paper, we will typically refer to term values as just values. By definition, all theory values are values, and all values are in normal form.

The definition of the call-by-value rewrite relation $\xrightarrow{\scriptscriptstyle\mathrm{v}}_{\mathcal{R}}$ follows the pattern of $\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}$ : $t\xrightarrow{\scriptscriptstyle\mathrm{v}}_{\mathcal{R}}t^{\prime}$ if and only if either (1) there exist a context ${C}[]$ , a substitution $\sigma$ and a rewrite rule ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ such that $t={C}[\ell\sigma]$ , $s$ is a ground value for each proper subterm $s$ of $\ell\sigma$ , $t^{\prime}={C}[r\sigma]$ and $\sigma$ respects $\varphi$ , or (2) $t\rightarrow_{\kappa}t^{\prime}$ .

Example 3.

The rewrite sequence in Example 2 is not innermost (and therefore not call-by-value). An example of a call-by-value rewrite sequence is:

Note that the redex in the first step is $\mathsf{gcdlist}$ , which does not have $1+1$ as subterm.

Example 4.

Consider the LCSTRS $\mathcal{R}=\{{\mathsf{hd}}\ {({{\mathsf{cons}}\ {x}}\ {l})}\rightarrow x,\;{% \mathsf{tl}}\ {({{\mathsf{cons}}\ {x}}\ {l})}\rightarrow l\}$ . Then the rewrite step ${\mathsf{hd}}\ {({{\mathsf{cons}}\ {42}}\ {({\mathsf{tl}}\ {\mathsf{nil}})})}% \xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}42$ is an innermost step, but not a call-by-value step. The reason is that the subterm ${\mathsf{tl}}\ {\mathsf{nil}}$ of the redex is in normal form, but not a value: innermost rewriting also allows for rewriting above function calls that are not defined on the given arguments; in a language like OCaml, the computation would abort with an error.

2.2 Accessibility and Computability

Accessibility.

Assume given a sort ordering – a quasi-ordering $\succsim$ over $\mathcal{S}$ whose strict part ${\succ}={\succsim}\setminus{\precsim}$ is well-founded. We inductively define two relations $\succsim_{+}$ and $\succ_{-}$ over $\mathcal{S}$ and $\mathcal{T}$ : for a sort $A$ and a type $B={B}_{1}\rightarrow\cdots\rightarrow{B}_{n}\rightarrow C$ where $C$ is a sort and $n\geq 0$ , $A\succsim_{+}B$ if $A\succsim C$ and $A\succ_{-}B_{i}$ for all $i$ , and $A\succ_{-}B$ if $A\succ C$ and $A\succsim_{+}B_{i}$ for all $i$ .

Given a function symbol $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B$ where $B$ is a sort, the set $\operatorname{Acc}(\mathsf{f})$ of the accessible argument positions of $\mathsf{f}$ is defined as $\{\,i\,|\,B\succsim_{+}A_{i}\,\}$ . A term $t$ is called an accessible subterm of a term $s$ , written as $s\trianglerighteq_{\mathrm{acc}}t$ , if either $s=t$ , or $s={\mathsf{f}}\ {{s}_{1}\cdots{s}_{n}}$ for some $\mathsf{f}\in\mathcal{F}$ and there exists $k\in\operatorname{Acc}(\mathsf{f})$ such that $s_{k}\trianglerighteq_{\mathrm{acc}}t$ . An LCSTRS $\mathcal{R}$ is called accessible function passing (AFP) if there exists a sort ordering such that for all ${{\mathsf{f}}\ {{s}_{1}\cdots{s}_{n}}}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ where $\mathsf{f}\in\mathcal{F}$ and $x\in\operatorname{Var}(r)\setminus\operatorname{Var}(\varphi)$ , there exists $k$ such that $s_{k}\trianglerighteq_{\mathrm{acc}}x$ .

Example 5.

An LCSTRS $\mathcal{R}$ is AFP (with $\succsim$ equating all the sorts) if for all ${{\mathsf{f}}\ {{s}_{1}\cdots{s}_{n}}}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ where $\mathsf{f}\in\mathcal{F}$ and $i\in\{\,1,\ldots,n\,\}$ , the type of each proper subterm of $s_{i}$ is a sort. This is typical for many common examples of higher-order programs manipulating first-order data; e.g., integer recursion or list folding, mapping or filtering; hence, Example 2 is AFP.

Consider $\{\,{{\mathsf{complst}}\ {\mathsf{fnil}}}\ {x}\rightarrow x,{{\mathsf{complst}% }\ {({{\mathsf{fcons}}\ {f}}\ {l})}}\ {x}\rightarrow{{\mathsf{complst}}\ {l}}% \ {({f}\ {x})}\,\}$ , where $\mathsf{complst}:\mathsf{funlist}\rightarrow\mathsf{int}\rightarrow\mathsf{int}$ composes a list of functions. This system is AFP with $\mathsf{funlist}\succ\mathsf{int}$ .

Consider $\{\,{\mathsf{app}}\ {({\mathsf{lam}}\ {f})}\rightarrow f\,\}$ where $\mathsf{app}:\mathsf{o}\rightarrow\mathsf{o}\rightarrow\mathsf{o}$ and $\mathsf{lam}:(\mathsf{o}\rightarrow\mathsf{o})\rightarrow\mathsf{o}$ . This system encodes the untyped lambda-calculus, with $\mathsf{app}$ serving as the application symbol and $\mathsf{lam}$ as a wrapper for abstractions. It is not AFP since $\mathsf{o}\succ\mathsf{o}$ cannot be true.

Computability.

A term is called neutral if it takes the form ${x}\ {{t}_{1}\cdots{t}_{n}}$ for some variable $x$ . A set of reducibility candidates, or an RC-set, for a type-preserving relation $\rightarrow$ over terms – which may stand for $\rightarrow_{\mathcal{R}}$ , $\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}$ , but also $\xrightarrow{\scriptscriptstyle\mathrm{v}}_{\mathcal{R}}$ – is an $\mathcal{S}$ -indexed family of sets $(I_{A})_{A\in\mathcal{S}}$ (let $I$ denote $\bigcup_{A}I_{A}$ ) satisfying the following conditions:

(1)

Each element of $I_{A}$ is a terminating (with respect to $\rightarrow$ ) term of type $A$ .
(2)

Given terms $s$ and $t$ such that $s\rightarrow t$ , if $s$ is in $I_{A}$ , so is $t$ .
(3)

Given a neutral term $s$ , if $t$ is in $I_{A}$ for all $t$ such that $s\rightarrow t$ , so is $s$ .

A term $t_{0}$ is called $I$ -computable if either the type of $t_{0}$ is a sort and $t_{0}\in I$ , or the type of $t_{0}$ is $A\rightarrow B$ and ${t_{0}}\ {t_{1}}$ is $I$ -computable for all $I$ -computable $t_{1}:A$ .

We are interested in a specific RC-set $\mathbb{C}$ :

Theorem 6 (see [13]).

Given a sort ordering and an RC-set $I$ for $\rightarrow$ , let $\Rrightarrow_{I}$ be the relation over terms such that $s\Rrightarrow_{I}t$ if and only if both $s$ and $t$ have a base type, $s={\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ for some function symbol $\mathsf{f}$ , $t={s_{k}}\ {{t}_{1}\cdots{t}_{n}}$ for some $k\in\operatorname{Acc}(\mathsf{f})$ and $t_{i}$ is $I$ -computable for all $i$ .

Given an LCSTRS $\mathcal{R}$ with a sort ordering, there exists an RC-set $\mathbb{C}$ for $\rightarrow$ such that $t\in\mathbb{C}_{A}$ if and only if $t : A$ is terminating with respect to ${\rightarrow}\cup{\Rrightarrow_{\mathbb{C}}}$ , and for all $t^{\prime}$ such that $t\rightarrow^{*}t^{\prime}$ , if $t^{\prime}={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for some function symbol $\mathsf{f}$ , $t_{i}$ is $\mathbb{C}$ -computable for all $i\in\operatorname{Acc}(\mathsf{f})$ .

$\mathbb{C}$ -computability with respect to the innermost reduction relation $\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}$ is at the heart of the soundness proofs for the DP framework defined in this paper (Theorems 14 and 36).

3 The Transformation of Call-By-Value Systems

Let us reflect on the shape of call-by-value LCSTRSs. First, we observe that if a pattern $t$ is not a value, neither are its instances, i.e., $t\sigma$ is not a value for any substitution $\sigma$ . Hence, under call by value, a rewrite rule ${\ell}\rightarrow{r}\ [\varphi]$ where not all the proper subterms of $\ell$ are values is never applicable, and we can exclude such rewrite rules without loss of generality.

Second, programming languages hardly allow the addition of constructors to pre-defined (in particular, primitive) data types, such as integers. Given an LCSTRS, in practice, we would also expect, for example, that integer literals are the only constructors for $\mathsf{int}$ . Formally, we call a theory sort $B$ inextensible if every function symbol $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B$ is a theory symbol or a defined symbol. We do not require that all theory sorts are inextensible; rather, we assume that for each rewrite rule ${\ell}\rightarrow{r}\ [\varphi]$ , all the variables in $\operatorname{Var}(\ell)$ whose type is an inextensible theory sort are also in $\operatorname{Var}(\varphi)$ . We can do so without loss of generality because such a variable can only be instantiated to a theory value under call by value. We only consider inextensible theory sorts in examples below.

We write $\varphi,{x}_{1},\ldots,{x}_{n}$ for $\varphi\wedge x_{1}\equiv x_{1}\wedge\cdots\wedge x_{n}\equiv x_{n}$ , and conclude the above discussion:

Lemma 7.

We apply the below transformation to an LCSTRS $\mathcal{R}$ and let $\mathcal{R}^{\prime}$ be the outcome.

(1)

Remove all ${\ell}\rightarrow{r}\ [\varphi]$ where $\ell$ has a proper subterm that is not a value.
(2)

Replace all remaining ${\ell}\rightarrow{r}\ [\varphi]$ with ${\ell}\rightarrow{r}\ [\varphi,{x}_{1},\ldots,{x}_{n}]$ where ${x}_{1},\ldots,{x}_{n}$ are the variables in $\operatorname{Var}(\ell)\setminus\operatorname{Var}(\varphi)$ whose type is an inextensible theory sort.

Then $t\xrightarrow{\scriptscriptstyle\mathrm{v}}_{\mathcal{R}}t^{\prime}$ if and only if $t\xrightarrow{\scriptscriptstyle\mathrm{v}}_{\mathcal{R}^{\prime}}t^{\prime}$ for all $t$ and $t^{\prime}$ .

Example 8.

The LCSTRS $\mathcal{R}$ from Example 2 is transformed as follows: (1) no rewrite rules are removed, and (2) four rewrite rules are replaced by the ones below.

	$\displaystyle{{{\mathsf{fold}}\ {f}}\ {y}}\ {\mathsf{nil}}$	$\displaystyle\rightarrow y$	$\displaystyle[\mathfrak{t},y]$	$\displaystyle{{\mathsf{gcd}}\ {m}}\ {n}$	$\displaystyle\rightarrow{{\mathsf{gcd}}\ {(-m)}}\ {n}$	$\displaystyle[m<0,n]$
	$\displaystyle{{{\mathsf{fold}}\ {f}}\ {y}}\ {({{\mathsf{cons}}\ {x}}\ {l})}$	$\displaystyle\rightarrow{{f}\ {x}}\ {({{{\mathsf{fold}}\ {f}}\ {y}}\ {l})}$	$\displaystyle[\mathfrak{t},x,y]$	$\displaystyle{{\mathsf{gcd}}\ {m}}\ {n}$	$\displaystyle\rightarrow{{\mathsf{gcd}}\ {m}}\ {(-n)}$	$\displaystyle[n<0,m]$

We will refer to the result of the transformation as $\mathcal{R}_{\mathsf{gcd}}$ .

We are particularly interested in call-by-value termination. However, innermost termination is more commonly considered in the term rewriting community, and has been studied extensively for first-order term rewriting. In practice, its difference from call-by-value termination is often irrelevant, and their respective techniques are generally similar. Since all values are in normal form, $\xrightarrow{\scriptscriptstyle\mathrm{v}}_{\mathcal{R}}$ is terminating if $\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}^{\prime}}$ is. Hence, we shall formulate our results in terms of innermost rewriting, for the sake of more generality and less bookkeeping.

4 Static Dependency Pairs and Chains

The dependency pair method [3] analyzes the recursive structure of function calls. Its variants are at the heart of most modern automatic termination analyzers for various styles of term rewriting. Static dependency pairs [35, 13], a higher-order generalization of the method, are adapted to LCSTRSs in [21]. Now we extend this adaptation for the evaluation strategies.

First, we recall a notation:

Definition 9.

Given an LCSTRS $\mathcal{R}$ , let $\mathcal{F}^{\sharp}$ be $\mathcal{F}\uplus\{\,\mathsf{f}^{\sharp}\,|\,\mathsf{f}\in\mathcal{D}\,\}$ where $\mathcal{D}$ is the set of defined symbols in $\mathcal{R}$ and $\mathsf{f}^{\sharp}$ is a fresh function symbol for all $\mathsf{f}$ . Let $\mathsf{dp}$ be a fresh sort, and for each defined symbol $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B$ where $B\in\mathcal{S}$ , we assign $\mathsf{f}^{\sharp}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow% \mathsf{dp}$ . Given a term $t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}\in T(\mathcal{F},\mathcal{V})$ where $\mathsf{f}\in\mathcal{D}$ , let $t^{\sharp}$ denote ${\mathsf{f}^{\sharp}}\ {{t}_{1}\cdots{t}_{n}}\in T(\mathcal{F}^{\sharp},% \mathcal{V})$ .

The definition of a static dependency pair is adapted as follows:

Definition 10.

A static dependency pair (SDP) is a triple ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]$ where $s^{\sharp}$ and $t^{\sharp}$ are terms of type $\mathsf{dp}$ , and $\varphi$ is a logical constraint. This SDP is considered call-by-value if all the proper subterms of $s^{\sharp}$ are values. For a rewrite rule ${\ell}\rightarrow{r}\ [\varphi]$ , let $\operatorname{SDP}({\ell}\rightarrow{r}\ [\varphi])$ denote the set of SDPs of form ${{\ell^{\sharp}}\ {{x}_{1}\cdots{x}_{m}}}\Rightarrow{{{\mathsf{g}^{\sharp}}\ {% {t}_{1}\cdots{t}_{q}}}\ {{y}_{q+1}\cdots{y}_{n}}}\ [\varphi]$ such that

(1)

$\ell^{\sharp}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow\mathsf{dp}$ with fresh variables ${x}_{1},\ldots,{x}_{m}$ ,
(2)

${r}\ {{x}_{1}\cdots{x}_{m}}\trianglerighteq{\mathsf{g}}\ {{t}_{1}\cdots{t}_{q}}$ for $\mathsf{g}\in\mathcal{D}$ , and
(3)

$\mathsf{g}^{\sharp}:{B}_{1}\rightarrow\cdots\rightarrow{B}_{n}\rightarrow% \mathsf{dp}$ with fresh variables ${y}_{q+1},\ldots,{y}_{n}$ .

Let $\operatorname{SDP}(\mathcal{R})$ be $\bigcup_{{\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}}\operatorname{SDP}({% \ell}\rightarrow{r}\ [\varphi])$ . For ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\mathfrak{t}]$ , we just write ${s^{\sharp}}\Rightarrow{t^{\sharp}}$ .

Compared to the quadruple definition in [21], this definition omits the $L$ component, because here its bookkeeping role can be assumed by the logical constraint.

Intuitively, every dependency pair in $\operatorname{SDP}(\mathcal{R})$ represents a function call in $\mathcal{R}$ . If $\mathcal{R}$ is non-terminating, there must be an infinite “chain” of function calls whose arguments are terminating (in other words, the chain is “minimal”: all the proper subterms are terminating). To distinguish the head symbols of those minimal potentially non-terminating terms, we write $\mathsf{f}^{\sharp}$ instead of $\mathsf{f}$ at head positions in SDPs. Then calls to a defined symbol $\mathsf{f}$ (the original) can be assumed to terminate, which is shown separately via $\mathsf{f}^{\sharp}$ . And the non-existence of an infinite chain starting from a call to any $\mathsf{f}^{\sharp}$ in $\operatorname{SDP}(\mathcal{R})$ implies the termination of $\mathcal{R}$ .

Example 11.

Following Example 8, $\operatorname{SDP}(\mathcal{R}_{\mathsf{gcd}})$ consists of the following SDPs:

(1)

${{\mathsf{gcdlist}^{\sharp}}\ {l^{\prime}}}\Rightarrow{{{\mathsf{gcd}^{\sharp}% }\ {m^{\prime}}}\ {n^{\prime}}}$
(2)

${{\mathsf{gcdlist}^{\sharp}}\ {l^{\prime}}}\Rightarrow{{{{\mathsf{fold}^{% \sharp}}\ {\mathsf{gcd}}}\ {0}}\ {l^{\prime}}}$
(3)

${{{\mathsf{gcd}^{\sharp}}\ {m}}\ {n}}\Rightarrow{{{\mathsf{gcd}^{\sharp}}\ {(-% m)}}\ {n}}\ [m<0,n]$
(4)

${{{\mathsf{gcd}^{\sharp}}\ {m}}\ {n}}\Rightarrow{{{\mathsf{gcd}^{\sharp}}\ {m}% }\ {(-n)}}\ [n<0,m]$
(5)

${{{\mathsf{gcd}^{\sharp}}\ {m}}\ {n}}\Rightarrow{{{\mathsf{gcd}^{\sharp}}\ {n}% }\ {(m\bmod n)}}\ [m\geq 0\wedge n>0]$
(6)

${{{{\mathsf{fold}^{\sharp}}\ {f}}\ {y}}\ {({{\mathsf{cons}}\ {x}}\ {l})}}% \Rightarrow{{{{\mathsf{fold}^{\sharp}}\ {f}}\ {y}}\ {l}}\ [\mathfrak{t},x,y]$

In this paper, a set $\mathcal{R}$ of rewrite rules plays two roles: (1) it specifies how to rewrite arguments in SDPs, and (2) it determines which rewrite steps are innermost and which terms are values. In Sections 5 and 6, a given set $\mathcal{R}$ in its first role may be modified (with rewrite rules removed). In this process, if we do not keep the original set, there can be unintended consequences for its second role. For example, consider $\mathcal{R}=\{\,{\mathsf{f}}\ {x}\rightarrow r_{1},\mathsf{a}\rightarrow r_{2}\,\}$ . Note that the first rewrite rule is not applicable to ${\mathsf{f}}\ {\mathsf{a}}$ with respect to innermost rewriting. Now if we remove the second rewrite rule from $\mathcal{R}$ and consider the new set, the remaining rewrite rule will be applicable, and the term $\mathsf{a}$ will be a value, which is generally an unwanted change.

Hence, we keep a copy of the original set $\mathcal{R}$ of rewrite rules to faithfully determine which rewrite steps are innermost and which terms are values. Following [18, 41], we let $\mathcal{Q}$ denote this copy. In contrast to the literature, we consider $\mathcal{Q}$ fixed throughout the analysis of a given system.⁴⁴4A fixed set $\mathcal{Q}$ suffices in this paper because our DP processors may remove rewrite rules, but may not add new rewrite rules or change the signature (e.g., with semantic labeling [45]). Now we formalize the idea of a chain of function calls in the innermost setting:

Definition 12.

Given a set $\mathcal{P}$ of SDPs and a set $\mathcal{R}$ of rewrite rules, an innermost $(\mathcal{P},\mathcal{R})$ -chain is a (finite or infinite) sequence $({s_{0}^{\sharp}}\Rightarrow{t_{0}^{\sharp}}\ [\varphi_{0}],\sigma_{0}),({s_{1% }^{\sharp}}\Rightarrow{t_{1}^{\sharp}}\ [\varphi_{1}],\sigma_{1}),\ldots$ such that for all $i$ , ${s_{i}^{\sharp}}\Rightarrow{t_{i}^{\sharp}}\ [\varphi_{i}]\in\mathcal{P}$ , $\sigma_{i}$ is a substitution which respects $\varphi_{i}$ , $s_{i}^{\sharp}\sigma_{i}$ is in normal form with respect to $\rightarrow_{\mathcal{Q}}$ , and $t_{i-1}^{\sharp}\sigma_{i-1}\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{% \mathcal{R}}^{*}s_{i}^{\sharp}\sigma_{i}$ if $i>0$ .

Example 13.

Following Example 11, $(\text{\ref{itm:gcdlistGcdlGcdf}},[{l^{\prime}}\coloneq{\mathsf{nil}},{m^{% \prime}}\coloneq{24},{n^{\prime}}\coloneq{18}]),(\text{\ref{itm:% gcdlistGcdfGcdfMod}},[{m}\coloneq{24},{n}\coloneq{18}]),(\text{\ref{itm:% gcdlistGcdfGcdfMod}},[{m}\coloneq{18},{n}\coloneq{6}])$ is an innermost $(\operatorname{SDP}(\mathcal{R}_{\mathsf{gcd}}),\mathcal{R}_{\mathsf{gcd}})$ -chain.

In the above definition, the requirement that $s_{i}^{\sharp}\sigma_{i}$ is in normal form implies that $\sigma_{i}(x)$ is in normal form for all $x\in\operatorname{Var}(s_{i}^{\sharp})$ , including fresh variables such as $l^{\prime}$ in SDP (1). Hence, the call-by-value (and therefore innermost) rewrite sequence in Example 3 does not directly translate to an innermost $(\operatorname{SDP}(\mathcal{R}),\mathcal{R})$ -chain. Nevertheless, we have the following result:

Theorem 14.

An AFP system $\mathcal{R}$ is innermost (and therefore call-by-value) terminating if there exists no infinite innermost $(\operatorname{SDP}(\mathcal{R}),\mathcal{R})$ -chain.

Proof Idea.

The full proof is in Section A.2, and is very similar to its counterpart for termination with respect to full rewriting [21]: in a non-terminating LCSTRS, we can always identify a non-terminating base-type term $t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ such that all $t_{i}$ are $\mathbb{C}$ -computable; and from an infinite reduction $t\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}t^{\prime}% \xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}t^{\prime\prime}% \xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}}\dots$ we can find $s, u$ such that $s={\mathsf{f}}\ {(t_{1}\,{\downarrow}_{\mathcal{R}})\cdots(t_{n}\,{\downarrow}% _{\mathcal{R}})}$ , $(s^{\sharp},u^{\sharp})$ is an instance of a dependency pair, and $u$ is again non-terminating with $\mathbb{C}$ -computable arguments. The primary difference from [21] is the need to ensure all variables are instantiated to normal forms, which for the fresh variables discussed above means that we must choose the right normal form that still yields non-termination. $\hfill\blacktriangleleft$

5 The Innermost DP Framework

In this section, we modify the constrained DP framework [21] to prove innermost termination. The DP framework is a collection of DP processors, each of which represents a technique.

Definition 15.

A DP problem is a pair $(\mathcal{P},\mathcal{R})$ where $\mathcal{P}$ is a set of SDPs and $\mathcal{R}$ is a set of rewrite rules. If no infinite innermost $(\mathcal{P},\mathcal{R})$ -chain exists, $(\mathcal{P},\mathcal{R})$ is called finite. A DP processor is a partial mapping which possibly assigns to a DP problem a set of DP problems. A DP processor $\rho$ is called sound if $(\mathcal{P},\mathcal{R})$ is finite whenever all the elements of $\rho(\mathcal{P},\mathcal{R})$ are.

Theorem 14 tells us that an AFP system $\mathcal{R}$ is innermost terminating if $(\operatorname{SDP}(\mathcal{R}),\mathcal{R})$ is a finite DP problem. Given a collection of sound DP processors, we have the following procedure: (1) $\mathcal{Q}\coloneq\mathcal{R}$ , $S\coloneq\{\,(\operatorname{SDP}(\mathcal{R}),\mathcal{R})\,\}$ ; (2) while $S$ contains a DP problem $(\mathcal{P},\mathcal{R})$ to which some sound DP processor $\rho$ is applicable, $S\coloneq(S\setminus\{\,(\mathcal{P},\mathcal{R})\,\})\cup\rho(\mathcal{P},% \mathcal{R})$ . If this procedure ends with $S=\emptyset$ , we can conclude that $\mathcal{R}$ is innermost terminating.

5.1 Graph, Subterm Criterion and Integer Mapping Processors

Three classes of DP processors in [21] remain essentially unchanged in the innermost setting. Let us review their application to the system $\mathcal{R}_{\mathsf{gcd}}$ from Example 8, which is discussed by [21] in the form of Example 2. First, we consider a graph approximation for $(\operatorname{SDP}(\mathcal{R}_{\mathsf{gcd}}),\mathcal{R}_{\mathsf{gcd}})$ :

Definition 16.

For a DP problem $(\mathcal{P},\mathcal{R})$ , a graph approximation $(G,\theta)$ consists of a finite directed graph $G$ and a mapping $\theta$ from $\mathcal{P}$ to the vertices of $G$ such that there is an edge from $\theta(p_{0})$ to $\theta(p_{1})$ whenever $(p_{0},\sigma_{0}),(p_{1},\sigma_{1})$ is an innermost $(\mathcal{P},\mathcal{R})$ -chain for some $\sigma_{0}$ and $\sigma_{1}$ .

Compared to [21], the main change is that we now check for innermost $(\mathcal{P},\mathcal{R})$ -chains to determine which edges must exist. A graph approximation for $(\operatorname{SDP}(\mathcal{R}_{\mathsf{gcd}}),\mathcal{R}_{\mathsf{gcd}})$ is in Figure 1. Despite the slightly different SDPs (due to the transformation of the call-by-value system), this graph approximation is the same as the one in [21].

Figure 1: A graph approximation for

(\operatorname{SDP}(\mathcal{R}_{\mathsf{gcd}}),\mathcal{R}_{\mathsf{gcd}})

.

Given a graph approximation, we can decompose the DP problem:

Definition 17.

Given a DP problem $(\mathcal{P},\mathcal{R})$ , a graph processor computes a graph approximation $(G,\theta)$ for $(\mathcal{P},\mathcal{R})$ and the strongly connected components (SCCs) of $G$ , then returns $\{\,(\{\,p\in\mathcal{P}\,|\,\theta(p)\text{ belongs to }S\,\},\mathcal{R})\,|% \,S\text{ is a non-trivial SCC of }G\,\}$ .

If a graph processor produces the graph approximation in Figure 1, it will return the set $\{\,(\{\,\text{\ref{itm:gcdlistFoldFold}}\,\},\mathcal{R}_{\mathsf{gcd}}),(\{% \,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{\ref{itm:gcdlistGcdfGcdfN}}\,\},% \mathcal{R}_{\mathsf{gcd}}),(\{\,\text{\ref{itm:gcdlistGcdfGcdfMod}}\,\},% \mathcal{R}_{\mathsf{gcd}})\,\}$ . Next, we observe that $\mathsf{fold}$ is defined by structural recursion, which can be handled by subterm criterion processors. Let $\operatorname{heads}(\mathcal{P})$ denote the set of function symbols heading either side of an SDP in $\mathcal{P}$ , and we have the following definition:

Definition 18.

A projection $\nu$ for a set $\mathcal{P}$ of SDPs is a mapping from $\operatorname{heads}(\mathcal{P})$ to integers such that $1\leq\nu(\mathsf{f}^{\sharp})\leq n$ if $\mathsf{f}^{\sharp}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow% \mathsf{dp}$ . Let $\bar{\nu}({\mathsf{f}^{\sharp}}\ {{t}_{1}\cdots{t}_{n}})$ denote $t_{\nu(\mathsf{f}^{\sharp})}$ . A projection $\nu$ is said to $\vartriangleright$ -orient a subset $\mathcal{P}^{\prime}$ of $\mathcal{P}$ if $\bar{\nu}(s^{\sharp})\vartriangleright\bar{\nu}(t^{\sharp})$ for all ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]\in\mathcal{P}^{\prime}$ and $\bar{\nu}(s^{\sharp})=\bar{\nu}(t^{\sharp})$ for all ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]\in\mathcal{P}\setminus\mathcal{% P}^{\prime}$ . A subterm criterion processor maps $(\mathcal{P},\mathcal{R})$ to $\{\,(\mathcal{P}\setminus\mathcal{P}^{\prime},\mathcal{R})\,\}$ for some non-empty $\mathcal{P}^{\prime}\subseteq\mathcal{P}$ which is $\vartriangleright$ -oriented by some projection for $\mathcal{P}$ .

Choosing $\nu(\mathsf{fold}^{\sharp})=3$ , we have $\bar{\nu}({{{\mathsf{fold}^{\sharp}}\ {f}}\ {y}}\ {({{\mathsf{cons}}\ {x}}\ {l% })})={{\mathsf{cons}}\ {x}}\ {l}\vartriangleright l=\bar{\nu}({{{\mathsf{fold}% ^{\sharp}}\ {f}}\ {y}}\ {l})$ , so a subterm criterion processor maps $(\{\,\text{\ref{itm:gcdlistFoldFold}}\,\},\mathcal{R}_{\mathsf{gcd}})$ to $\{\,(\emptyset,\mathcal{R}_{\mathsf{gcd}})\,\}$ , and $(\emptyset,\mathcal{R}_{\mathsf{gcd}})$ can (trivially) be removed by a graph processor. Now we are left with $(\{\,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{\ref{itm:gcdlistGcdfGcdfN}}\,\},% \mathcal{R}_{\mathsf{gcd}})$ and $(\{\,\text{\ref{itm:gcdlistGcdfGcdfMod}}\,\},\mathcal{R}_{\mathsf{gcd}})$ , which involve recursion over integers. We deal with those by means of integer mappings:

Definition 19.

Given a set $\mathcal{P}$ of SDPs, for all $\mathsf{f}^{\sharp}\in\operatorname{heads}(\mathcal{P})$ where $\mathsf{f}^{\sharp}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow% \mathsf{dp}$ , let $\iota(\mathsf{f}^{\sharp})$ be the subset of $\{\,1,\ldots,n\,\}$ such that $i\in\iota(\mathsf{f}^{\sharp})$ if and only if $A_{i}\in{\mathcal{S}}_{\vartheta}$ and the $i$ -th argument of any occurrence of $\mathsf{f}^{\sharp}$ in an SDP ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]\in\mathcal{P}$ is in $T({\mathcal{F}}_{\vartheta},\operatorname{Var}(\varphi))$ . Let $\mathcal{X}(\mathsf{f}^{\sharp})$ be a set of fresh variables $\{\,x_{i}\,|\,i\in\iota(\mathsf{f}^{\sharp})\,\}$ where $x_{i}:A_{i}$ for all $i$ . An integer mapping $\mathcal{J}$ for $\mathcal{P}$ is a mapping from $\operatorname{heads}(\mathcal{P})$ to theory terms such that for all $\mathsf{f}^{\sharp}$ , $\mathcal{J}(\mathsf{f}^{\sharp}):\mathsf{int}$ and $\operatorname{Var}(\mathcal{J}(\mathsf{f}^{\sharp}))\subseteq\mathcal{X}(% \mathsf{f}^{\sharp})$ . Let $\bar{\mathcal{J}}({\mathsf{f}^{\sharp}}\ {{t}_{1}\cdots{t}_{n}})$ denote $\mathcal{J}(\mathsf{f}^{\sharp})[{x_{i}}\coloneq{t_{i}}]_{i\in\iota(\mathsf{f}% ^{\sharp})}$ .

Integer mapping processors handle decreasing integer values:

Definition 20.

Given a set $\mathcal{P}$ of SDPs, an integer mapping $\mathcal{J}$ is said to $>$ -orient a subset $\mathcal{P}^{\prime}$ of $\mathcal{P}$ if $\varphi\models\bar{\mathcal{J}}(s^{\sharp})\geq 0\wedge\bar{\mathcal{J}}(s^{% \sharp})>\bar{\mathcal{J}}(t^{\sharp})$ for all ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]\in\mathcal{P}^{\prime}$ , and $\varphi\models\bar{\mathcal{J}}(s^{\sharp})\geq\bar{\mathcal{J}}(t^{\sharp})$ for all ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]\in\mathcal{P}\setminus\mathcal{% P}^{\prime}$ , where $\varphi\models\varphi^{\prime}$ denotes that $[\![\varphi\sigma]\!]=1$ implies $[\![\varphi^{\prime}\sigma]\!]=1$ for each substitution $\sigma$ which maps variables in $\operatorname{Var}(\varphi)\cup\operatorname{Var}(\varphi^{\prime})$ to theory values. An integer mapping processor maps $(\mathcal{P},\mathcal{R})$ to $\{\,(\mathcal{P}\setminus\mathcal{P}^{\prime},\mathcal{R})\,\}$ for some non-empty $\mathcal{P}^{\prime}\subseteq\mathcal{P}$ which is $>$ -oriented by some integer mapping for $\mathcal{P}$ .

To deal with $(\{\,\text{\ref{itm:gcdlistGcdfGcdfMod}}\,\},\mathcal{R}_{\mathsf{gcd}})$ , let $\mathcal{J}(\mathsf{gcd}^{\sharp})$ be $x_{2}$ so $\bar{\mathcal{J}}({{\mathsf{gcd}^{\sharp}}\ {m}}\ {n})=n$ , $\bar{\mathcal{J}}({{\mathsf{gcd}^{\sharp}}\ {n}}\ {(m\bmod n)})=m\bmod n$ and $m\geq 0\wedge n>0\models n\geq 0\wedge n>m\bmod n$ . Then an integer mapping processor returns $\{\,(\emptyset,\mathcal{R}_{\mathsf{gcd}})\,\}$ , and $(\emptyset,\mathcal{R}_{\mathsf{gcd}})$ can (trivially) be removed by a graph processor.

Unlike [21], here an integer mapping processor is applicable to $(\{\,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{\ref{itm:gcdlistGcdfGcdfN}}\,\},% \mathcal{R}_{\mathsf{gcd}})$ : $\mathcal{J}(\mathsf{gcd}^{\sharp})={-x_{1}}$ and the processor returns $\{\,(\{\,\text{\ref{itm:gcdlistGcdfGcdfN}}\,\},\mathcal{R}_{\mathsf{gcd}})\,\}$ . Then $(\{\,\text{\ref{itm:gcdlistGcdfGcdfN}}\,\},\mathcal{R}_{\mathsf{gcd}})$ can be removed by a graph processor. This simpler proof is due to the transformation of the call-by-value system; in both SDPs, $m$ and $n$ can be instantiated only to theory values, which is not the case in [21], and a theory argument processor is needed there. To elaborate, we consider the system $\mathcal{R}$ :

{{{\mathsf{f}}\ {x}}\ {y}}\ {z}\rightarrow{{{\mathsf{f}}\ {x}}\ {(x+1)}}\ {(x-% 1)}\quad[y<z]\qquad{{\mathsf{c}}\ {x}}\ {y}\rightarrow x\qquad{{\mathsf{c}}\ {% x}}\ {y}\rightarrow y

We have ${{{\mathsf{f}}\ {({{\mathsf{c}}\ {0}}\ {3})}}\ {1}}\ {2}\rightarrow_{\mathcal{% R}}{{{\mathsf{f}}\ {({{\mathsf{c}}\ {0}}\ {3})}}\ {(({{\mathsf{c}}\ {0}}\ {3})% +1)}}\ {(({{\mathsf{c}}\ {0}}\ {3})-1)}\rightarrow_{\mathcal{R}}^{+}{{{\mathsf% {f}}\ {({{\mathsf{c}}\ {0}}\ {3})}}\ {1}}\ {2}$ , and therefore $\mathcal{R}$ is not terminating with respect to full rewriting. Under call by value, $\mathcal{R}$ is terminating: the first rewrite rule with $x$ appended to the logical constraint gives the only SDP ${{{{\mathsf{f}^{\sharp}}\ {x}}\ {y}}\ {z}}\Rightarrow{{{{\mathsf{f}^{\sharp}}% \ {x}}\ {(x+1)}}\ {(x-1)}}\ [y<z,x]$ , then let $\mathcal{J}(\mathsf{f}^{\sharp})$ be $x_{3}-x_{2}$ . Here we benefit from call by value.

5.2 The Chaining of Call-By-Value SDPs

Another benefit of call by value is that we may chain together consecutive SDPs, e.g., ${{\mathsf{fact}^{\sharp}}\ {x}}\Rightarrow{{{\mathsf{u}_{1}^{\sharp}}\ {x}}\ {% 1}}\ [\mathfrak{t},x]$ and ${{{\mathsf{u}_{1}^{\sharp}}\ {x}}\ {z}}\Rightarrow{{{{\mathsf{u}_{2}^{\sharp}}% \ {x}}\ {z}}\ {1}}\ [\mathfrak{t},x,z]$ may merge to form ${{\mathsf{fact}^{\sharp}}\ {x}}\Rightarrow{{{{\mathsf{u}_{2}^{\sharp}}\ {x}}\ % {1}}\ {1}}\ [\mathfrak{t},x]$ . This capability can be important for automatically generated systems.

Definition 21.

Given SDPs $p_{0}=({s_{0}^{\sharp}}\Rightarrow{{\mathsf{f}^{\sharp}}\ {{t^{\prime}}_{1}% \cdots{t^{\prime}}_{n}}}\ [\varphi_{0}])$ and $p_{1}=({{\mathsf{f}^{\sharp}}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{n}}}% \Rightarrow{t_{1}^{\sharp}}\ [\varphi_{1}])$ where $\mathsf{f}\in\mathcal{D}$ and variables are renamed if necessary to avoid name collisions, $p_{0}$ and $p_{1}$ are called chainable if $p_{1}$ is a call-by-value SDP and there exists a substitution $\sigma$ such that $\operatorname{dom}(\sigma)=\bigcup_{i=1}^{n}\operatorname{Var}(s_{i}^{\prime})$ , $t_{i}^{\prime}=s_{i}^{\prime}\sigma$ for all $i$ , and $\sigma(x)\in T({\mathcal{F}}_{\vartheta},\operatorname{Var}(\varphi_{0}))$ for all $x\in\operatorname{dom}(\sigma)\cap\operatorname{Var}(\varphi_{1})$ . The chaining $\operatorname{ch}(p_{0},p_{1})$ of $p_{0}$ and $p_{1}$ is ${s_{0}^{\sharp}}\Rightarrow{t_{1}^{\sharp}\sigma}\ [\varphi_{0}\wedge(\varphi_% {1}\sigma)]$ .

Note that in the context of call-by-value rewriting, all SDPs can be assumed to be call-by-value, and therefore it is not particularly restrictive to so require $p_{1}$ above. To see the importance of this requirement, consider the DP problem $(\{\,{{{\mathsf{f}^{\sharp}}\ {\mathsf{a}}}\ {\mathsf{b}}}\Rightarrow{{\mathsf% {g}^{\sharp}}\ {({{\mathsf{h}}\ {\mathsf{b}}}\ {\mathsf{a}})}},{{\mathsf{g}^{% \sharp}}\ {({{\mathsf{h}}\ {x}}\ {y})}}\Rightarrow{{{\mathsf{f}^{\sharp}}\ {x}% }\ {y}}\,\},\{\,{{\mathsf{h}}\ {\mathsf{b}}}\ {\mathsf{a}}\rightarrow{{\mathsf% {h}}\ {\mathsf{a}}}\ {\mathsf{b}}\,\})$ . If we dropped the call-by-value requirement for the second SDP, the two SDPs would be chainable and yield ${{{\mathsf{f}^{\sharp}}\ {\mathsf{a}}}\ {\mathsf{b}}}\Rightarrow{{{\mathsf{f}^% {\sharp}}\ {\mathsf{b}}}\ {\mathsf{a}}}$ . However, ${{\mathsf{f}^{\sharp}}\ {\mathsf{b}}}\ {\mathsf{a}}$ is not reachable from ${{\mathsf{f}^{\sharp}}\ {\mathsf{a}}}\ {\mathsf{b}}$ initially, and replacing the original SDPs with the new one is not sound.

Definition 22.

Given a set $\mathcal{P}$ of SDPs and $\mathsf{f}\in\mathcal{D}$ such that $\mathcal{P}_{\mathsf{f}}^{\ell}\neq\emptyset$ , $\mathcal{P}_{\mathsf{f}}^{r}\neq\emptyset$ , $\mathcal{P}_{\mathsf{f}}^{\ell}\cap\mathcal{P}_{\mathsf{f}}^{r}=\emptyset$ and every pair in $\mathcal{P}_{\mathsf{f}}^{r}\times\mathcal{P}_{\mathsf{f}}^{\ell}$ is chainable where $\mathcal{P}_{\mathsf{f}}^{\ell}=\{\,{s^{\sharp}}\Rightarrow{t^{\sharp}}\ [% \varphi]\in\mathcal{P}\,|\,s^{\sharp}={\mathsf{f}^{\sharp}}\ {{s}_{1}\cdots{s}% _{n}}\,\}$ and $\mathcal{P}_{\mathsf{f}}^{r}=\{\,{s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi% ]\in\mathcal{P}\,|\,t^{\sharp}={\mathsf{f}^{\sharp}}\ {{t}_{1}\cdots{t}_{n}}\,\}$ , a chaining processor assigns to a DP problem $(\mathcal{P},\mathcal{R})$ the singleton $\{\,((\mathcal{P}\setminus(\mathcal{P}_{\mathsf{f}}^{\ell}\cup\mathcal{P}_{% \mathsf{f}}^{r}))\cup\mathcal{P}^{\prime},\mathcal{R})\,\}$ where $\mathcal{P}^{\prime}=\{\,\operatorname{ch}(p_{0},p_{1})\,|\,p_{0}\in\mathcal{P% }_{\mathsf{f}}^{r}\text{ and }p_{1}\in\mathcal{P}_{\mathsf{f}}^{\ell}\,\}$ .

Example 23.

Consider the below set $\mathcal{P}$ of SDPs generated from an imperative program [14]:

$\displaystyle{\mathsf{fact}^{\sharp}}\ {x}$	$\displaystyle\Rightarrow{{\mathsf{u}_{1}^{\sharp}}\ {x}}\ {1}$	$\displaystyle[\mathfrak{t},x]$	$\displaystyle{{\mathsf{u}_{1}^{\sharp}}\ {x}}\ {z}$	$\displaystyle\Rightarrow{{{\mathsf{u}_{2}^{\sharp}}\ {x}}\ {z}}\ {1}$	$\displaystyle[\mathfrak{t},x,z]$
$\displaystyle{{{\mathsf{u}_{2}^{\sharp}}\ {x}}\ {z}}\ {i}$	$\displaystyle\Rightarrow{{{\mathsf{u}_{3}^{\sharp}}\ {x}}\ {z}}\ {i}$	$\displaystyle[i\leq x,z]$	$\displaystyle{{{\mathsf{u}_{3}^{\sharp}}\ {x}}\ {z}}\ {i}$	$\displaystyle\Rightarrow{{{\mathsf{u}_{4}^{\sharp}}\ {x}}\ {(z*i)}}\ {i}$	$\displaystyle[\mathfrak{t},x,z,i]$
$\displaystyle{{{\mathsf{u}_{2}^{\sharp}}\ {x}}\ {z}}\ {i}$	$\displaystyle\Rightarrow{{\mathsf{u}_{5}^{\sharp}}\ {x}}\ {z}$	$\displaystyle[\neg(i\leq x),z]$	$\displaystyle{{{\mathsf{u}_{4}^{\sharp}}\ {x}}\ {z}}\ {i}$	$\displaystyle\Rightarrow{{{\mathsf{u}_{2}^{\sharp}}\ {x}}\ {z}}\ {(i+1)}$	$\displaystyle[\mathfrak{t},x,z,i]$

Chaining processors can iteratively remove the occurrences of $\mathsf{u}_{1}^{\sharp}$ , $\mathsf{u}_{3}^{\sharp}$ and $\mathsf{u}_{4}^{\sharp}$ , and end with (1) ${{\mathsf{fact}^{\sharp}}\ {x}}\Rightarrow{{{{\mathsf{u}_{2}^{\sharp}}\ {x}}\ % {1}}\ {1}}\ [\mathfrak{t},x]$ , (2) ${{{{\mathsf{u}_{2}^{\sharp}}\ {x}}\ {z}}\ {i}}\Rightarrow{{{{\mathsf{u}_{2}^{% \sharp}}\ {x}}\ {(z*i)}}\ {(i+1)}}\ [i\leq x,z]$ , and (3) ${{{{\mathsf{u}_{2}^{\sharp}}\ {x}}\ {z}}\ {i}}\Rightarrow{{{\mathsf{u}_{5}^{% \sharp}}\ {x}}\ {z}}\ [\neg(i\leq x),z]$ . Note that a chaining processor for $\mathsf{f}\in\mathcal{D}$ removes all the occurrences of $\mathsf{f}^{\sharp}$ in $\mathcal{P}$ , and therefore the process of iteratively applying chaining processors always terminates (on the assumption that $\operatorname{heads}(\mathcal{P})$ is finite). In this example, the above outcome cannot be further chained; there is no chaining processor for $\mathsf{u}_{2}$ because $\mathcal{P}_{\mathsf{u}_{2}}^{\ell}\cap\mathcal{P}_{\mathsf{u}_{2}}^{r}$ contains SDP (23).

Example 24.

Consider the following set $\mathcal{P}$ of SDPs:

	$\displaystyle{{\mathsf{f}^{\sharp}}\ {x}}\ {y}$	$\displaystyle\Rightarrow{\mathsf{g}^{\sharp}}\ {({{\mathsf{comb}}\ {x}}\ {y})}$	$\displaystyle[x\geq 0,y]$	$\displaystyle{\mathsf{g}^{\sharp}}\ {({{\mathsf{comb}}\ {z}}\ {w})}$	$\displaystyle\Rightarrow{\mathsf{h}^{\sharp}}\ {(z+w)}$	$\displaystyle[w\geq 0,z]$
	$\displaystyle{{\mathsf{f}^{\sharp}}\ {x}}\ {y}$	$\displaystyle\Rightarrow{\mathsf{g}^{\sharp}}\ {({{\mathsf{comb}}\ {(-x)}}\ {y% })}$	$\displaystyle[x<0,y]$	$\displaystyle{\mathsf{g}^{\sharp}}\ {({{\mathsf{comb}}\ {z}}\ {w})}$	$\displaystyle\Rightarrow{\mathsf{h}^{\sharp}}\ {(z-w)}$	$\displaystyle[w<0,z]$

where $\mathsf{comb}:\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{intpair}$ is a constructor. Note that ${{\mathsf{comb}}\ {z}}\ {w}$ is a value. Chaining processors can remove the occurrences of $\mathsf{g}^{\sharp}$ , and end with (1) ${{{\mathsf{f}^{\sharp}}\ {x}}\ {y}}\Rightarrow{{\mathsf{h}^{\sharp}}\ {(x+y)}}% \ [x\geq 0\wedge y\geq 0]$ , (2) ${{{\mathsf{f}^{\sharp}}\ {x}}\ {y}}\Rightarrow{{\mathsf{h}^{\sharp}}\ {(x-y)}}% \ [x\geq 0\wedge y<0]$ , (3) ${{{\mathsf{f}^{\sharp}}\ {x}}\ {y}}\Rightarrow{{\mathsf{h}^{\sharp}}\ {(-x+y)}% }\ [x<0\wedge y\geq 0]$ , and (4) ${{{\mathsf{f}^{\sharp}}\ {x}}\ {y}}\Rightarrow{{\mathsf{h}^{\sharp}}\ {(-x-y)}% }\ [x<0\wedge y<0]$ .

5.3 Usable Rules

A key processor in the DP framework for full rewriting, which also applies in the innermost setting, is the reduction pair processor [21, Definition 25]. This processor is so powerful because it can potentially be used with a wide variety of different reduction pairs and does not require $\succ$ to be monotonic: we must show ${s^{\sharp}}\mathrel{\succ}_{\varphi}{t^{\sharp}}$ or ${s^{\sharp}}\mathrel{\succeq}_{\varphi}{t^{\sharp}}$ for all SDPs ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]$ , and ${s}\mathrel{\succeq}_{\varphi}{t}$ for all rules ${s}\rightarrow{t}\ [\varphi]$ , and we may then remove the SDPs oriented with $\succ$ .

The challenge is that, no matter how small $\mathcal{P}$ , we must orient all rules $\mathcal{R}$ in the DP problem – and all processors considered so far only modify the set $\mathcal{P}$ of SDPs. Fortunately, in the innermost setting, we can see that only some of the rules could potentially be relevant.

To illustrate the idea, consider a system $\mathcal{R}_{\mathsf{drop}}$ which includes at least the following rewrite rules and no other defining $\mathsf{drop}$ , $\mathsf{dfoldr}$ , $\mathsf{cons}$ , or $\mathsf{nil}$ :

	$\displaystyle{{{\mathsf{drop}}\ {n}}\ {l}}\rightarrow{l}\ [n\leq 0]\quad{{{% \mathsf{drop}}\ {n}}\ {\mathsf{nil}}}\rightarrow{\mathsf{nil}}\ [\mathfrak{t},% n]\quad{{{\mathsf{drop}}\ {n}}\ {({{\mathsf{cons}}\ {x}}\ {l})}}\rightarrow{{{% \mathsf{drop}}\ {(n-1)}}\ {l}}\ [n>0]$
	$\displaystyle\begin{aligned} {{{{\mathsf{dfoldr}}\ {f}}\ {y}}\ {n}}\ {\mathsf{% nil}}&\rightarrow y&&[\mathfrak{t},n]\\ {{{{\mathsf{dfoldr}}\ {f}}\ {y}}\ {n}}\ {({{\mathsf{cons}}\ {x}}\ {l})}&% \rightarrow{{f}\ {x}}\ {({{{{\mathsf{dfoldr}}\ {f}}\ {y}}\ {n}}\ {({{\mathsf{% drop}}\ {n}}\ {l})})}&&[\mathfrak{t},n]\end{aligned}$

where $\mathsf{drop}:\mathsf{int}\rightarrow\mathsf{alist}\rightarrow\mathsf{alist}$ and $\mathsf{dfoldr}:(\mathsf{a}\rightarrow\mathsf{b}\rightarrow\mathsf{b})% \rightarrow\mathsf{b}\rightarrow\mathsf{int}\rightarrow\mathsf{alist}% \rightarrow\mathsf{b}$ . To deal with the SDP $(\{\,{{{{{\mathsf{dfoldr}^{\sharp}}\ {f}}\ {y}}\ {n}}\ {({{\mathsf{cons}}\ {x}% }\ {l})}}\Rightarrow{{{{{\mathsf{dfoldr}^{\sharp}}\ {f}}\ {y}}\ {n}}\ {({{% \mathsf{drop}}\ {n}}\ {l})}}\ [\mathfrak{t},n]\,\},\mathcal{R}_{\mathsf{drop}})$ , we need a reduction pair processor; roughly, we should show that ${{\mathsf{cons}}\ {x}}\ {l}$ is somehow “greater” than ${{\mathsf{drop}}\ {n}}\ {l}$ , which cannot be done by a subterm criterion or an integer mapping processor. However, since the variables are to be instantiated to normal forms, any rules other than the ones defining $\mathsf{drop}$ would not be used in a chain for this problem. Hence, only these three rules need to be oriented. This observation leads to the notion of usable rules [3, 13]. We base our formulation on a higher-order version [26] and start with two auxiliary definitions:

Definition 25.

For ${\ell}\rightarrow{r}\ [\varphi]$ where $\ell:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B$ for $B\in\mathcal{S}$ , let $({\ell}\rightarrow{r}\ [\varphi])^{\mathrm{ex}}$ be $\{\,{\ell}\rightarrow{r}\ [\varphi],{{\ell}\ {x_{1}}}\rightarrow{{r}\ {x_{1}}}% \ [\varphi],\ldots,{{\ell}\ {{x}_{1}\cdots{x}_{n}}}\rightarrow{{r}\ {{x}_{1}% \cdots{x}_{n}}}\ [\varphi]\,\}$ where ${x}_{1},\ldots,{x}_{n}$ are fresh variables. Let $\mathcal{R}^{\mathrm{ex}}$ denote $\bigcup_{{\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}}({\ell}\rightarrow{r}\ % [\varphi])^{\mathrm{ex}}$ .

Definition 26.

The set of usable symbols in a term $t$ with respect to a logical constraint $\varphi$ , denoted by $\mathcal{U}_{\mathcal{F}}(t)[\varphi]$ , is defined inductively as follows:

(1)

Suppose $t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for $\mathsf{f}\in\mathcal{F}^{\sharp}$ . If $t\in T({\mathcal{F}}_{\vartheta},\operatorname{Var}(\varphi))$ , then $\mathcal{U}_{\mathcal{F}}(t)[\varphi]=\emptyset$ ; otherwise $\mathcal{U}_{\mathcal{F}}(t)[\varphi]=\{\,(\mathsf{f},n)\,\}\cup\bigcup_{i=1}^% {n}\mathcal{U}_{\mathcal{F}}(t_{i})[\varphi]$ .
(2)

Suppose $t={x}\ {{t}_{1}\cdots{t}_{n}}$ for $x\in\mathcal{V}$ . If $n=0$ , then $\mathcal{U}_{\mathcal{F}}(t)[\varphi]=\emptyset$ ; otherwise $\mathcal{U}_{\mathcal{F}}(t)[\varphi]=\{\,\bot\,\}$ .

Here $\bot$ is a special symbol indicating that potentially any symbol could be usable.

The set of usable symbols for a set $\mathcal{P}$ of SDPs and a set $\mathcal{R}$ of rewrite rules, denoted by $\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , is the smallest set $U$ such that (1) $\mathcal{U}_{\mathcal{F}}(t^{\sharp})[\varphi]\subseteq U$ for all ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]\in\mathcal{P}$ , and (2) $\mathcal{U}_{\mathcal{F}}(r)[\varphi]\subseteq U$ for all $(\mathsf{f},n)\in U$ and ${{\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}}\rightarrow{r}\ [\varphi]\in\mathcal{R}^% {\mathrm{ex}}$ . Then $\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ exists because it is the least pre-fixed point of an order-preserving mapping on a complete lattice.

We present usable rules as a class of DP processors:

Definition 27.

Given sets $\mathcal{P}$ of SDPs and $\mathcal{R}$ of rules: if $\bot\notin\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , the set $\mathcal{U}(\mathcal{P},\mathcal{R})$ of usable rules is defined as $\{\,{{\mathsf{f}}\ {{t}_{1}\cdots{t}_{k}}}\rightarrow{r}\ [\varphi]\in\mathcal% {R}\,|\,(\mathsf{f},n)\in\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})% \text{ and }k\leq n\,\}$ ; otherwise, $\mathcal{U}(\mathcal{P},\mathcal{R})$ is undefined. A usable-rules processor assigns to a DP problem $(\mathcal{P},\mathcal{R})$ with $\mathcal{N}\!\mathcal{F}(\mathcal{Q})\subseteq\mathcal{N}\!\mathcal{F}(% \mathcal{R})$ the singleton $\{\,(\mathcal{P},\mathcal{U}(\mathcal{P},\mathcal{R}))\,\}$ .

Example 28.

We continue the discussion about $\mathsf{drop}$ and $\mathsf{dfoldr}$ . Consider the DP problem $(\mathcal{P},\mathcal{R}_{\mathsf{drop}})$ where $\mathcal{P}=\{\,{{{{{\mathsf{dfoldr}^{\sharp}}\ {f}}\ {y}}\ {n}}\ {({{\mathsf{% cons}}\ {x}}\ {l})}}\Rightarrow{{{{{\mathsf{dfoldr}^{\sharp}}\ {f}}\ {y}}\ {n}% }\ {({{\mathsf{drop}}\ {n}}\ {l})}}\ [\mathfrak{t},n]\,\}$ . We have $\mathcal{U}_{\mathcal{F}}({{{{\mathsf{dfoldr}^{\sharp}}\ {f}}\ {y}}\ {n}}\ {({% {\mathsf{drop}}\ {n}}\ {l})})[\mathfrak{t},n]=\{\,(\mathsf{dfoldr}^{\sharp},4)% ,(\mathsf{drop},2)\,\}$ and can derive $\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})=\{\,(\mathsf{dfoldr}^{% \sharp},4),(\mathsf{drop},2),(\mathsf{nil},0)\,\}$ . Hence, $\mathcal{U}(\mathcal{P},\mathcal{R})$ consists of the three rules defining $\mathsf{drop}$ .

5.4 Argument Filterings

Let us consider the role of $\bot$ in the definition of usable rules: $\mathcal{U}(\mathcal{P},\mathcal{R})$ is undefined if $\bot\in\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ – which occurs if the right-hand side of some SDP in $\mathcal{P}$ , or the right-hand side of any rule ${{\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}}\rightarrow{r}\ [\varphi]\in\mathcal{R}^% {\mathrm{ex}}$ with $(\mathsf{f},n)\in\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , is not a pattern. This is not a rare occasion in higher-order rewriting. For example, let us rework $\mathsf{dfoldr}$ into $\mathsf{dfoldl}$ :

{{{{\mathsf{dfoldl}}\ {f}}\ {y}}\ {n}}\ {\mathsf{nil}}\rightarrow y\ [% \mathfrak{t},n]\quad\quad{{{{\mathsf{dfoldl}}\ {f}}\ {y}}\ {n}}\ {({{\mathsf{% cons}}\ {x}}\ {l})}\rightarrow{{{{\mathsf{dfoldl}}\ {f}}\ {({{f}\ {y}}\ {x})}}% \ {n}}\ {({{\mathsf{drop}}\ {n}}\ {l})}\ [\mathfrak{t},n]

where $\mathsf{drop}$ is defined by the same rules as before. Now we have ${{{{{\mathsf{dfoldl}^{\sharp}}\ {f}}\ {y}}\ {n}}\ {({{\mathsf{cons}}\ {x}}\ {l% })}}\Rightarrow{{{{{\mathsf{dfoldl}^{\sharp}}\ {f}}\ {({{f}\ {y}}\ {x})}}\ {n}% }\ {({{\mathsf{drop}}\ {n}}\ {l})}}\ [\mathfrak{t},n]$ , which produces $\bot$ .

However, observe that the problematic subterm ${{f}\ {y}}\ {x}$ and the decreasing subterm ${{\mathsf{drop}}\ {n}}\ {l}$ occur in different arguments of $\mathsf{dfoldl}^{\sharp}$ . If we use a reduction pair that considers only the fourth argument, intuitively we can disregard any rules that may be used to reduce the second. This is formalized via an argument filtering [3, 26], which temporarily removes certain subterms from both sides of an ordering requirement before computing usable rules, often drastically reducing the number of usable rules that the reduction pair must consider.

Traditionally, argument filterings are defined for function symbols with a fixed number of arguments. Extending this notion to our curried setting imposes new technical challenges; e.g., if we filter away the second argument of $\mathsf{f}:A\rightarrow B\rightarrow C$ , what type to use for the filtering of ${\mathsf{f}}\ {x}$ , $C$ or $B\rightarrow C$ ? Fortunately, this problem is solvable if we do not allow variables to occur at the head of an application in the result of a filtering. This is very different from the approach in [2], which heavily restricts what filtering can be used, to ensure that a variable of higher type and all its possible instances have the same filtering applied to them.

Definition 29.

We assume given a set $\mathcal{S}_{1}$ of sorts such that ${\mathcal{S}}_{\vartheta}\subseteq\mathcal{S}_{1}$ , and a mapping $\mu$ from $\mathcal{T}$ to $\mathcal{S}_{1}$ such that $\mu(A)=A$ for all $A\in{\mathcal{S}}_{\vartheta}$ . In addition, for each function symbol $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B$ with $B\in\mathcal{S}$ , we assume given a set $\operatorname{regard}(\mathsf{f})\subseteq\{\,1,\ldots,n\,\}$ . Define:

\begin{array}[]{rcl}\Sigma={\mathcal{F}}_{\vartheta}&\cup\ \ \{&\mathsf{f}_{m}% :\mu(A_{i_{1}})\rightarrow\dots\rightarrow\mu(A_{i_{k}})\rightarrow\mu(A_{m+1}% \rightarrow\dots\rightarrow A_{n}\rightarrow B)\ \mid\\ &&\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B\in% \mathcal{F}^{\sharp}\ \text{with}\ B\in\mathcal{S}\ \text{and}\ 0\leq m\leq n% \ \text{and}\\ &&\operatorname{regard}(\mathsf{f})\cap\{\,1,\ldots,m\,\}=\{\,{i}_{1},\ldots,{% i}_{k}\,\}\ \text{and}\ {i}_{1}<\cdots<{i}_{k}\ \ \}\\ &\cup\ \ \{&\bullet_{\mu(A)}:\mu(A)\mid A\in\mathcal{T}\ \ \}\\ \end{array}

The argument filtering with respect to a logical constraint $\varphi$ is a mapping $\pi_{\varphi}$ from $T(\mathcal{F}^{\sharp},\mathcal{V})$ to $T(\Sigma^{\sharp},\{x:\mu(A)\mid x:A\in\mathcal{V}\})$ , defined as follows:

(1)

$\pi_{\varphi}({\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}})={\mathsf{f}}\ {{t}_{1}% \cdots{t}_{n}}$ if ${\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}\in T({\mathcal{F}}_{\vartheta},% \operatorname{Var}(\varphi))$ and has a base type
(2)

$\pi_{\varphi}({\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}})={\mathsf{f}_{n}}\ {\pi_{% \varphi}(t_{i_{1}})\cdots\pi_{\varphi}(t_{i_{k}})}$ otherwise, where $\{\,{i}_{1},\ldots,{i}_{k}\,\}=\operatorname{regard}(\mathsf{f})\cap\{\,1,% \ldots,n\,\}$ and ${i}_{1}<\cdots<{i}_{k}$
(3)

$\pi_{\varphi}(x)=x$ for $x\in\mathcal{V}$ ; and $\pi_{\varphi}({x}\ {{t}_{1}\cdots{t}_{n}})=\bullet_{\mu(A)}$ if $x\in\mathcal{V}$ and $n>0$

By definition, $\pi_{\varphi}(t):\mu(A)$ for all $t : A$ . Moreover, no subterm of $\pi_{\varphi}(t)$ has a variable at the head of an application, and all function symbols have a first-order type and occur maximally applied. Hence, $\pi_{\varphi}(t)$ is a (many-sorted) first-order term, just written in applicative notation. For $\mathcal{S}_{1}$ , we may for instance choose ${\mathcal{S}}_{\vartheta}\cup\{\,\mathsf{o}\,\}$ , i.e., there is a single sort besides theory sorts.

Now we define usable rules with respect to an argument filtering:

Definition 30.

Given the mapping $\operatorname{regard}(\cdot)$ , $\mathcal{U}_{\mathcal{F}}({\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}})[\varphi]$ is redefined as $\{\,(\mathsf{f},n)\,\}\cup\bigcup_{i\in\operatorname{regard}(\mathsf{f})\cap\{% \,1,\ldots,n\,\}}\mathcal{U}_{\mathcal{F}}(t_{i})[\varphi]$ in the case where ${\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}\notin T({\mathcal{F}}_{\vartheta},% \operatorname{Var}(\varphi))$ . The definition in other cases is unchanged, and so is the definition of $\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ .

Let $U_{1}$ be $\{\,{\pi_{\varphi}({\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}})}\rightarrow{\pi_{% \varphi}(r)}\ [\varphi]\,|\,(\mathsf{f},n)\in\mathcal{U}_{\mathcal{F}}(% \mathcal{P},\mathcal{R})\text{ and }{{\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}}% \rightarrow{r}\ [\varphi]\in\mathcal{R}^{\mathrm{ex}}\,\}$ , and $U_{2}$ be $\{\,{{\mathsf{f}_{n}}\ {x_{i_{1}}\cdots x_{i_{k}}}}\rightarrow{y}\ [y={\mathsf% {f}}\ {{x}_{1}\cdots{x}_{n}}]\,|\,(\mathsf{f},n)\in\mathcal{U}_{\mathcal{F}}(% \mathcal{P},\mathcal{R}),\mathsf{f}\in{\mathcal{F}}_{\vartheta},n>0,\mathsf{f}% :{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B\text{ with }B\in% \mathcal{S},\operatorname{regard}(\mathsf{f})=\{\,{i}_{1},\ldots,{i}_{k}\,\}% \text{ and }{i}_{1}<\cdots<{i}_{k}\,\}$ .

We redefine $\mathcal{U}(\mathcal{P},\mathcal{R})$ as $U_{1}\cup U_{2}$ if $\bot\notin\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , and $p+i\in\operatorname{regard}(\mathsf{f})$ for all $(\mathsf{f},n)\in\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , ${{\mathsf{f}}\ {{s}_{1}\cdots{s}_{p}}}\rightarrow{{\mathsf{g}}\ {{t}_{1}\cdots% {t}_{q}}}\ [\varphi]\in\mathcal{R}$ where $p<n$ and $\mathsf{g}\in\mathcal{F}$ , and $i\in\{\,1,\ldots,n-p\,\}$ such that $q+i\in\operatorname{regard}(\mathsf{g})$ . Otherwise, $\mathcal{U}(\mathcal{P},\mathcal{R})$ is undefined.

That is, we consider usable rules only with respect to the positions that are not filtered away. The requirement that $p+i\in\operatorname{regard}(\mathsf{f})$ if $(\mathsf{f},n)$ is a usable symbol and $p+i\leq n$ is a technical limitation needed to ensure that applying a rewrite rule at the head of an application does not conflict with the argument filtering.

Next, we recall the notion of a constrained reduction pair from [21], but use a more liberal monotonicity requirement due to the first-order setting created by the filtering.

Definition 31.

A constrained relation $R$ is a set of triples $(s,t,\varphi)$ where $s$ and $t$ are (first-order) terms which have the same sort and $\varphi$ is a logical constraint. We write ${s}\mathrel{R}_{\varphi}{t}$ if $(s,t,\varphi)\in R$ . A binary relation $R^{\prime}$ over terms is said to cover a constrained relation $R$ if ${s}\mathrel{R}_{\varphi}{t}$ implies that $(s\sigma)\,{\downarrow}_{\kappa}\mathrel{R^{\prime}}(t\sigma)\,{\downarrow}_{\kappa}$ for each substitution $\sigma$ which respects $\varphi$ .

A constrained reduction pair $(\succeq,\succ)$ is a pair of constrained relations where $\succeq$ is covered by some reflexive and transitive relation $\sqsupseteq$ such that $t_{k}\sqsupseteq t_{k}^{\prime}$ implies ${{{\mathsf{f}}\ {{t}_{1}\cdots{t}_{k-1}}}\ {t_{k}}}\ {{t}_{k+1}\cdots{t}_{n}}% \sqsupseteq{{{\mathsf{f}}\ {{t}_{1}\cdots{t}_{k-1}}}\ {t_{k}^{\prime}}}\ {{t}_% {k+1}\cdots{t}_{n}}$ (i.e., monotonicity) for all $\mathsf{f}\in\Sigma$ and $k\in\{\,1,\ldots,n\,\}$ , $\succ$ is covered by some well-founded relation $\sqsupset$ , and ${\sqsupset}\mathrel{;}{\sqsupseteq}\subseteq{\sqsupset^{+}}$ .

Having this, we can define reduction pair processors with respect to an argument filtering:

Definition 32.

A reduction pair processor with argument filterings assigns to a DP problem $(\mathcal{P},\mathcal{R})$ with $\mathcal{N}\!\mathcal{F}(\mathcal{Q})\subseteq\mathcal{N}\!\mathcal{F}(% \mathcal{R})$ the singleton $\{\,(\mathcal{P}\setminus\mathcal{P}^{\prime},\mathcal{R})\,\}$ for some non-empty $\mathcal{P}^{\prime}\subseteq\mathcal{P}$ if there exists a mapping $\operatorname{regard}(\cdot)$ and a constrained reduction pair $(\succeq,\succ)$ such that (1) ${\pi_{\varphi}(s^{\sharp})}\mathrel{\succ}_{\varphi}{\pi_{\varphi}(t^{\sharp})}$ for all ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]\in\mathcal{P}^{\prime}$ , (2) ${\pi_{\varphi}(s^{\sharp})}\mathrel{\succeq}_{\varphi}{\pi_{\varphi}(t^{\sharp% })}$ for all ${s^{\sharp}}\Rightarrow{t^{\sharp}}\ [\varphi]\in\mathcal{P}\setminus\mathcal{% P}^{\prime}$ , and (3) ${\ell}\mathrel{\succeq}_{\varphi}{r}$ for all ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{U}(\mathcal{P},\mathcal{R})$ .

Example 33.

Consider $\mathsf{dfoldl}$ , with the following DP problem: $(\{\,{{{{{\mathsf{dfoldl}^{\sharp}}\ {f}}\ {y}}\ {n}}\ {({{\mathsf{cons}}\ {x}% }\ {l})}}\Rightarrow{{{{{\mathsf{dfoldl}^{\sharp}}\ {f}}\ {({{f}\ {y}}\ {x})}}% \ {n}}\ {({{\mathsf{drop}}\ {n}}\ {l})}}\ [\mathfrak{t},n]\,\},\mathcal{R})$ Let $\operatorname{regard}(\mathsf{dfoldl}^{\sharp})$ be $\{\,4\,\}$ , $\operatorname{regard}(\mathsf{drop})$ be $\{\,2\,\}$ , and $\operatorname{regard}(\mathsf{cons})$ be $\{\,2\,\}$ . We are obliged to prove (1) ${{\mathsf{dfoldl}^{\sharp}_{4}}\ {({\mathsf{cons}_{2}}\ {l})}}\mathrel{\succ}_% {\mathfrak{t},n}{{\mathsf{dfoldl}^{\sharp}_{4}}\ {({\mathsf{drop}_{2}}\ {l})}}$ , (2) ${{\mathsf{drop}_{2}}\ {l}}\mathrel{\succeq}_{n\leq 0}{l}$ , (3) ${{\mathsf{drop}_{2}}\ {\mathsf{nil}_{0}}}\mathrel{\succeq}_{\mathfrak{t},n}{% \mathsf{nil}_{0}}$ , and (4) ${{\mathsf{drop}_{2}}\ {({\mathsf{cons}_{2}}\ {l})}}\mathrel{\succeq}_{n>0}{{% \mathsf{drop}_{2}}\ {l}}$ . The recursive path ordering for first-order LCTRSs [29] can be used to fulfill these obligations.

6 Universal Computability with Usable Rules

In this section, we study universal computability [21] with respect to innermost rewriting. This concept concerns a modular programming scenario where the LCSTRS represents a single module in a larger program, and corresponds to the termination of a function in all “reasonable” uses, including unknown uses. We recall the notion of a hierarchical combination [31, 32, 33, 9] rephrased in terms of LCSTRSs:

Definition 34 ([21]).

An LCSTRS $\mathcal{R}_{1}$ is called an extension of a base system $\mathcal{R}_{0}$ if the two systems’ interpretations of theory symbols coincide over all the theory symbols in common, and function symbols in $\mathcal{R}_{0}$ are not defined by any rewrite rule in $\mathcal{R}_{1}$ . Given a base system $\mathcal{R}_{0}$ and an extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$ , the system $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ is called a hierarchical combination.

In a hierarchical combination, function symbols in the base system can occur in the extension, but cannot be (re)defined; one may think of $\mathcal{R}_{0}$ as an imported module.

Universal computability is defined on the basis of hierarchical combinations:

Definition 35 ([21]).

Given an LCSTRS $\mathcal{R}_{0}$ with a sort ordering $\succsim$ , a term $t$ is called universally computable if for each extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$ and each extension $\succsim^{\prime}$ of $\succsim$ to sorts in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ (i.e., $\succsim^{\prime}$ coincides with $\succsim$ over sorts in $\mathcal{R}_{0}$ ), $t$ is $\mathbb{C}$ -computable in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ with $\succsim^{\prime}$ . $\mathcal{R}_{0}$ is called universally computable if all its terms are.

In summary, we consider passing $\mathbb{C}$ -computable arguments to a defined symbol in $\mathcal{R}_{0}$ the “reasonable” way of calling the function. We use SDPs to establish universal computability:

Theorem 36.

An accessible function passing system $\mathcal{R}_{0}$ with sort ordering $\succsim$ is universally computable if there exists no infinite innermost $(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$ -chain for any extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$ and extension $\succsim^{\prime}$ of $\succsim$ to sorts in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ .

This is a more general version of Theorem 14 and will be proved alongside it in Appendix A.2. Note that the original set of rules, $\mathcal{Q}$ , in the definition of innermost chain is now $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ . We modify the DP framework to prove universal computability for a fixed base system $\mathcal{R}_{0}$ .

Definition 37.

A (universal) DP problem $(\mathcal{P},\mathcal{R},\mathtt{p})$ consists of a set $\mathcal{P}$ of SDPs, a set $\mathcal{R}$ of rewrite rules and a flag $\mathtt{p}\in\{\,\mathfrak{def},\mathfrak{ind}\,\}$ (for definite or indefinite). A DP problem $(\mathcal{P},\mathcal{R},\mathtt{p})$ is finite if either (1) $\mathtt{p}=\mathfrak{def}$ and there exists no infinite innermost $(\mathcal{P},\mathcal{R})$ -chain (with $\mathcal{Q}\coloneq\mathcal{R}_{0}$ ), or (2) $\mathtt{p}=\mathfrak{ind}$ and there exists no infinite innermost $(\mathcal{P},\mathcal{R}\cup\mathcal{R}_{1})$ -chain for any extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$ (with $\mathcal{Q}\coloneq\mathcal{R}_{0}\cup\mathcal{R}_{1}$ ).

DP processors are defined in the same way as before, now for universal DP problems. The goal is to show that $(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0},\mathfrak{ind})$ is finite, and the procedure for termination in Section 5 still works if we change the initialization accordingly. Unlike [21], here we have the advantage of usable rules: if $\mathcal{U}(\mathcal{P},\mathcal{R})$ is defined, then $\mathcal{U}(\mathcal{P},\mathcal{R}\cup\mathcal{R}_{1})=\mathcal{U}(\mathcal{P% },\mathcal{R})$ for any extension $\mathcal{R}_{1}$ (provided all symbols in $\mathcal{P}$ and $\mathcal{R}$ are from $\mathcal{R}_{0}$ , which is typically the case as DP processors generally do not introduce new symbols). Hence a usable-rules processor assigns to a DP problem $(\mathcal{P},\mathcal{R},\mathtt{p})$ the singleton $\{\,(\mathcal{P},\mathcal{U}(\mathcal{P},\mathcal{R}),\mathfrak{def})\,\}$ .

Even if usable-rules processors are not applicable, we may still use a reduction pair processor with an argument filtering: we do not have to orient the rules in $\mathcal{R}_{1}$ since they cannot be usable. Referring to Definition 32, a reduction pair processor now assigns to a DP problem $(\mathcal{P},\mathcal{R},\mathtt{p})$ the singleton $\{\,(\mathcal{P}\setminus\mathcal{P}^{\prime},\mathcal{R},\mathtt{p})\,\}$ without changing the input flag because it does not permanently discard any rule. The other DP processors discussed in Section 5 apply to universal DP problems similarly; they just keep the input flag unchanged in the output.

7 Implementation and Evaluation

We have implemented our results in Cora [27], using a version of HORPO (based on the initial definition in [22]) and its first-order limitation RPO as the only reduction pair. Constraint validity checks are delegated to the SMT solver Z3 [8]. We also use Z3 to seek a good argument filtering and HORPO instance by encoding the requirements into an SMT problem.

Our implementation of the chaining processor from Definition 22 aims to minimize the number of DPs in the resulting problem. To this end, it chooses a function symbol $\mathsf{f}$ such that the expression $|\mathcal{P}^{\prime}|-|\mathcal{P}_{\mathsf{f}}^{\ell}\cup\mathcal{P}_{% \mathsf{f}}^{r}|$ with the sets defined as in Definition 22 is minimized.

We evaluated Cora on three groups of benchmarks: our own collected LCSTRS benchmarks, the lambda-free problems from the higher-order category of the TPDB [7], and problems from the first-order “integer TRS innermost” category. The results are summarized below, where “full” considers the framework for full termination with the methods from [21], and “call-by-value” does the transformation of Lemma 7 before applying the innermost framework:

	Termination			Universal Computability
	Full	Innermost	Call-by-value	Full	Innermost	Call-by-value
Total yes	171	179	182	155	179	182
Total maybe	104	96	93	116	96	93

Note that we gain significant power compared to [21] when analyzing universal computability. This is largely due to the two usable-rules processors: the reduction pair processor cannot be applied on its own in an indefinite DP problem, so either changing the flag from $\mathfrak{ind}$ to $\mathfrak{def}$ , or being able to omit the extra rules in a reduction pair, gives a lot of power.

However, the gains for termination are more modest. We suspect the reason is that the new processors primarily find their power in large systems (where it is essential to eliminate many rules when searching for a reduction pair), and automatically generated systems (where there are often many chainable rules), not in the handcrafted benchmarks of the TPDB.

Another observation is that there is no difference in proving power between termination or universal computability, both for innermost and for call-by-value reduction. This may be due to Cora having only one reduction pair (HORPO): on this benchmark set, when HORPO can be applied to simplify a DP problem, then it is also possible to filter away problematic subterms that would stop us from applying usable rules.

A detailed evaluation page is available through the following link:

https://www.cs.ru.nl/˜cynthiakop/experiments/fscd25/

Comparison to Other Analyzers.

While we have made progress, the additions of this paper are not yet sufficient for Cora to compete with dedicated analyzers for first-order integer rewriting, or unconstrained higher-order term rewriting.

In the “integer TRS innermost” category, AProVE [15] can prove innermost termination of 102 benchmarks, while Cora can handle 72 for innermost evaluation and 73 for call-by-value. The most important difference seems to be that AProVE has a much more sophisticated implementation of what we call the integer mapping processor as a reduction pair processor with polynomial interpretations and usable rules with respect to argument filterings [12]. In addition, these benchmarks often have rules such as $\mathsf{f}(x)\rightarrow\mathsf{g}(x>0,x),\ \mathsf{g}(\mathfrak{t},x)% \rightarrow r_{1},\ \mathsf{g}(\mathfrak{f},x)\rightarrow r_{2}$ , which would benefit from a transformation to turn the Boolean subterm $x>0$ into a proper constraint. Improving on these points is obvious future work.

In the “higher-order union beta” category, Wanda [25] can prove termination of full rewriting of 105 benchmarks, while Cora can handle 79 for innermost or call-by-value reduction. Since these benchmarks are unconstrained, Cora does not benefit here from any of the processors that consider the theory, while Wanda does have many more features to increase its prover ability; for example, polynomial interpretations, dynamic dependency pairs, and delegation of partial problems to a first-order termination tool.

8 Related Work

Dependency Pair frameworks are the cornerstone of most fully automated termination analysis tools for various flavors of first-order [1, 19, 23] and higher-order [2, 13, 30] rewriting. A common theme of these DP frameworks lies in the notions of a problem to be analyzed for presence of infinite chains and processors to advance the proofs of (non-)termination. The notion of DP frameworks has been lifted to constrained rewriting, both in the first-order [10, 12] and recently also in the higher-order [21] setting. The latter work also includes the notion of universal computability, allowing for termination proofs also in the presence of further library functions that are not known at the time of analysis.

Our present DP framework for innermost rewriting is specially designed with termination analysis of functional programs in call-by-value languages (e.g., Scala, OCaml) in mind as a target application. Such LCSTRSs may come from an automated syntactic translation and thus have more rewrite rules with “intermediate” defined symbols than hand-optimized rewrite systems. Our chaining processor renders the analysis of such problems feasible. This kind of program transformation is used also in other program analysis tools [4, 10, 14, 15]; here, we have adapted the technique to higher-order rewriting with constraints.

Usable rules w.r.t. an argument filtering were introduced for first-order rewriting in [19] and soon extended to simply-typed higher-order rewriting for arbitrary rewrite strategies in [2]. Our contribution here is to lift usable rules w.r.t. an argument filtering to a setting with theory constraints and to universal computability, thus opening up the door for applications in analysis of programs for real-world languages. Moreover, we adapt the technique to innermost rewriting and thus do not require that the constrained reduction pair $(\succeq,\succ)$ satisfies ${{\mathsf{c}}\ {x}}\ {y}\succeq x$ and ${{\mathsf{c}}\ {x}}\ {y}\succeq y$ for fresh symbols $\mathsf{c}$ .

9 Conclusion and Future Work

In this paper, we have extended the static dependency pair framework for LCSTRSs to innermost and call-by-value evaluation strategies. In doing so, we have adapted several existing processors for full termination and proposed three processors – chaining, usable rules, reduction pairs with usable rules w.r.t. argument filterings – that were not present for the setting of full termination. These processors apply not only to conventional closed-world termination analysis, but also to open-world termination analysis via universal computability, where the presence of further rewrite rules for library functions is assumed, thus broadening the set of potential start terms that must be considered. Our experimental results on several benchmark collections indicate improvements over the state of the art by exploiting the evaluation strategy via the new processors, most pronounced for universal computability.

There are several directions for future work. Our chaining processors could be improved, e.g., by using unification instead of matching, thus defining a form of narrowing for our constrained DPs in the higher-order setting. Moreover, so far our implementation prohibits chaining a DP with itself to prevent non-termination of repeated applications of the chaining processors. We might loosen this restriction via appropriate heuristics to detect cases in which such self-chaining could be beneficial. In addition, we could investigate chaining not just for DPs, but also for rewrite rules. The integer mapping processor could be improved by lifting polynomial interpretations [43] for higher-order rewriting to the constrained setting of LCSTRSs. Another improvement would consist of moving Boolean expressions from the right-hand side of rewrite rules into their constraints. Techniques like the integer mapping processor or the subterm criterion, which establish weak or strict decrease between certain arguments of dependency pairs, could also be improved by combining them with the size-change termination principle [37]. Size-change termination has been integrated into the first-order DP framework [42, 5], and a natural next step would be to lift this integration to the higher-order DP framework for LCSTRSs, both for innermost and for full termination.

A different avenue could be to research to what extent the termination analysis techniques in this paper can be ported from innermost or call-by-value evaluation to arbitrary evaluation strategies, or to lazy evaluation, as used in Haskell. For the latter, we might consider an approximation of lazy evaluation via a higher-order form of context-sensitive rewriting [1, 38].

Finally, to go back to one of the main motivations of this work, we could devise translations from higher-order functional programming languages with call-by-value semantics (e.g., Scala, OCaml) to LCSTRSs. This would allow for applying the contributions of this paper to prove termination of programs written in these languages, a long-term goal of this line of research.

References

[1] B. Alarcón, R. Gutiérrez, and S. Lucas. Context-sensitive dependency pairs. IC, 208(8):922–968, 2010. doi:10.1016/J.IC.2010.03.003.
[2] T. Aoto and T. Yamada. Argument filterings and usable rules for simply typed dependency pairs. In S. Ghilardi and R. Sebastiani, editors, Proc. FroCoS, pages 117–132, 2009. doi:10.1007/978-3-642-04222-5_7.
[3] T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. TCS, 236(1–2):133–178, 2000. doi:10.1016/S0304-3975(99)00207-8.
[4] D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software model checking via large-block encoding. In A. Biere and C. Pixley, editors, Proc. FMCAD, pages 25–32, 2009. doi:10.1109/FMCAD.2009.5351147.
[5] M. Codish, C. Fuhs, J. Giesl, and P. Schneider-Kamp. Lazy abstraction for size-change termination. In C. G. Fermüller and A. Voronkov, editors, Proc. LPAR (Yogyakarta), pages 217–232, 2010. doi:10.1007/978-3-642-16242-8_16.
[6] Community. Termination competition (TermCOMP). URL: https://termination-portal.org/wiki/Termination_Competition.
[7] Community. The termination problem database (TPDB). URL: https://github.com/TermCOMP/TPDB.
[8] L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In C.R. Ramakrishnan and J. Rehof, editors, Proc. TACAS, pages 337–340, 2008. doi:10.1007/978-3-540-78800-3_24.
[9] N. Dershowitz. Hierarchical termination. In N. Dershowitz and N. Lindenstrauss, editors, Proc. CTRS, pages 89–105, 1995. doi:10.1007/3-540-60381-6_6.
[10] S. Falke and D. Kapur. A term rewriting approach to the automated termination analysis of imperative programs. In R. A. Schmidt, editor, Proc. CADE, pages 277–293, 2009. doi:10.1007/978-3-642-02959-2_22.
[11] S. Falke, D. Kapur, and C. Sinz. Termination analysis of C programs using compiler intermediate languages. In M. Schmidt-Schauß, editor, Proc. RTA, pages 41–50, 2011. doi:10.4230/LIPIcs.RTA.2011.41.
[12] C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke. Proving termination of integer term rewriting. In R. Treinen, editor, Proc. RTA, pages 32–47, 2009. doi:10.1007/978-3-642-02348-4_3.
[13] C. Fuhs and C. Kop. A static higher-order dependency pair framework. In L. Caires, editor, Proc. ESOP, pages 752–782, 2019. doi:10.1007/978-3-030-17184-1_27.
[14] C. Fuhs, C. Kop, and N. Nishida. Verifying procedural programs via constrained rewriting induction. ACM TOCL, 18(2):14:1–14:50, 2017. doi:10.1145/3060143.
[15] J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Analyzing program termination and complexity automatically with AProVE. JAR, 58(1):3–31, 2017. doi:10.1007/s10817-016-9388-y.
[16] J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated termination proofs for Haskell by term rewriting. ACM TOPLAS, 33(2):7:1–7:39, 2011. doi:10.1145/1890028.1890030.
[17] J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs. Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs. In A. King, editor, Proc. PPDP, pages 1–12, 2012. doi:10.1145/2370776.2370778.
[18] J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: combining techniques for automated termination proofs. In F. Baader and A. Voronkov, editors, Proc. LPAR, pages 301–331, 2005. doi:10.1007/978-3-540-32275-7_21.
[19] J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and improving dependency pairs. JAR, 37(3):155–203, 2006. doi:10.1007/s10817-006-9057-7.
[20] L. Guo, K. Hagens, C. Kop, and D. Vale. Higher-order constrained dependency pairs for (universal) computability. pre-publication Arxiv copy of [21] with additional appendix. doi:10.48550/arXiv.2406.19379.
[21] L. Guo, K. Hagens, C. Kop, and D. Vale. Higher-order constrained dependency pairs for (universal) computability. In R. Královič and A. Kučera, editors, Proc. MFCS, pages 57:1–57:15, 2024. doi:10.4230/LIPIcs.MFCS.2024.57.
[22] L. Guo and C. Kop. Higher-order LCTRSs and their termination. In S. Weirich, editor, Proc. ESOP, pages 331–357, 2024. doi:10.1007/978-3-031-57267-8_13.
[23] N. Hirokawa and A. Middeldorp. Automating the dependency pair method. IC, 199(1-2):172–199, 2005. doi:10.1016/J.IC.2004.10.004.
[24] N. Hirokawa and A. Middeldorp. Tyrolean Termination Tool: techniques and features. IC, 205(4):474–511, 2007. doi:10.1016/j.ic.2006.08.010.
[25] C. Kop. WANDA – a higher order termination tool (system description). In Z. M. Ariola, editor, Proc. FSCD, pages 36:1–36:19, 2020. doi:10.4230/LIPICS.FSCD.2020.36.
[26] C. Kop. Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting. In A. P. Felty, editor, Proc. FSCD, pages 1:1–1:17, 2022. doi:10.4230/LIPIcs.FSCD.2022.1.
[27] C. Kop et al. The Cora analyzer. URL: https://github.com/hezzel/cora.
[28] C. Kop et al. hezzel/cora: FSCD 2025. doi:10.5281/zenodo.15318964.
[29] C. Kop and N. Nishida. Term rewriting with logical constraints. In P. Fontaine, C. Ringeissen, and R. A. Schmidt, editors, Proc. FroCoS, pages 343–358, 2013. doi:10.1007/978-3-642-40885-4_24.
[30] C. Kop and F. van Raamsdonk. Dynamic dependency pairs for algebraic functional systems. LMCS, 8(2), 2012. doi:10.2168/LMCS-8(2:10)2012.
[31] M. R. K. Krishna Rao. Completeness of hierarchical combinations of term rewriting systems. In R. K. Shyamasundar, editor, Proc. FSTTCS, pages 125–138, 1993. doi:10.1007/3-540-57529-4_48.
[32] M. R. K. Krishna Rao. Simple termination of hierarchical combinations of term rewriting systems. In M. Hagiya and J. C. Mitchell, editors, Proc. TACS, pages 203–223, 1994. doi:10.1007/3-540-57887-0_97.
[33] M. R. K. Krishna Rao. Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, Proc. CAAP, pages 379–393, 1995. doi:10.1007/3-540-59293-8_208.
[34] K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static dependency pair method based on strong computability for higher-order rewrite systems. IEICE Trans. Inf. Syst., E92.D(10):2007–2015, 2009. doi:10.1587/transinf.E92.D.2007.
[35] K. Kusakari and M. Sakai. Enhancing dependency pair method using strong computability in simply-typed term rewriting. AAECC, 18(5):407–431, 2007. doi:10.1007/s00200-007-0046-9.
[36] K. Kusakari and M. Sakai. Static dependency pair method for simply-typed term rewriting and related techniques. IEICE Trans. Inf. Syst., E92.D(2):235–247, 2009. doi:10.1587/transinf.E92.D.235.
[37] C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In C. Hankin and D. Schmidt, editors, Proc. POPL, pages 81–92, 2001. doi:10.1145/360204.360210.
[38] S. Lucas. Context-sensitive computations in functional and functional logic programs. JFLP, 1998(1), 1998. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-01/A98-01.html.
[39] C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl. Automated termination analysis of Java bytecode by term rewriting. In C. Lynch, editor, Proc. RTA, pages 259–276, 2010. doi:10.4230/LIPIcs.RTA.2010.259.
[40] S. Suzuki, K. Kusakari, and F. Blanqui. Argument filterings and usable rules in higher-order rewrite systems. IPSJ Online Trans., 4:114–125, 2011. doi:10.2197/ipsjtrans.4.114.
[41] R. Thiemann. The DP framework for proving termination of term rewriting. PhD thesis, RWTH Aachen University, Germany, 2007. URL: http://darwin.bth.rwth-aachen.de/opus3/volltexte/2007/2066/.
[42] R. Thiemann and J. Giesl. The size-change principle and dependency pairs for termination of term rewriting. AAECC, 16(4):229–270, 2005. doi:10.1007/S00200-005-0179-7.
[43] J. van de Pol. Termination proofs for higher-order rewrite systems. In J. Heering, K. Meinke, B. Möller, and T. Nipkow, editors, Proc. HOA, pages 305–325, 1993. doi:10.1007/3-540-58233-9_14.
[44] F. van Raamsdonk. Translating logic programs into conditional rewriting systems. In L. Naish, editor, Proc. ICLP, pages 168–182, 1997. doi:10.7551/mitpress/4299.003.0018.
[45] H. Zantema. Termination of term rewriting by semantic labelling. FI, 24(1/2):89–105, 1995. doi:10.3233/FI-1995-24124.

Appendix A Full Proofs

A.1 Soundness for Section 5

For soundness of the graph, subterm criterion and integer mapping processors, we refer to Appendix A.2 in [20]; only minimal changes are needed. Below we address the rest.

Theorem 38.

Chaining processors are sound.

Proof of Theorem 38.

Given a DP problem $(\mathcal{P},\mathcal{R})$ , a defined symbol $\mathsf{f}$ with the said properties and an infinite innermost $(\mathcal{P},\mathcal{R})$ -chain $({s_{0}^{\sharp}}\Rightarrow{t_{0}^{\sharp}}\ [\varphi_{0}],\sigma_{0}),({s_{1% }^{\sharp}}\Rightarrow{t_{1}^{\sharp}}\ [\varphi_{1}],\sigma_{1}),\ldots$ where variables are renamed to avoid name collisions between any two of the SDPs and $\operatorname{dom}(\sigma_{i})\subseteq\operatorname{Var}(s_{i}^{\sharp})\cup% \operatorname{Var}(t_{i}^{\sharp})\cup\operatorname{Var}(\varphi_{i})$ for all $i$ , we consider $k>0$ such that $t_{k-1}^{\sharp}={\mathsf{f}^{\sharp}}\ {{t^{\prime}}_{1}\cdots{t^{\prime}}_{n}}$ and $s_{k}^{\sharp}={\mathsf{f}^{\sharp}}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{n}}$ . By definition, $t^{\prime}_{i}\sigma_{k-1}\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{% \mathcal{R}}^{*}s^{\prime}_{i}\sigma_{k}$ for all $i$ . Because ${s_{k-1}^{\sharp}}\Rightarrow{t_{k-1}^{\sharp}}\ [\varphi_{k-1}]$ and ${s_{k}^{\sharp}}\Rightarrow{t_{k}^{\sharp}}\ [\varphi_{k}]$ are chainable, there exists a substitution $\sigma^{\prime}$ such that $\operatorname{dom}(\sigma^{\prime})=\bigcup_{i=1}^{n}\operatorname{Var}(s^{% \prime}_{i})$ , $s^{\prime}_{i}\sigma^{\prime}=t^{\prime}_{i}$ for all $i$ and $\sigma^{\prime}(x)\in T({\mathcal{F}}_{\vartheta},\operatorname{Var}(\varphi_{% k-1}))$ for all $x\in\operatorname{dom}(\sigma^{\prime})\cap\operatorname{Var}(\varphi_{k})$ . Hence, $s^{\prime}_{i}\sigma^{\prime}\sigma_{k-1}\xrightarrow{\scriptscriptstyle% \mathcal{Q}}_{\mathcal{R}}^{*}s^{\prime}_{i}\sigma_{k}$ for all $i$ . Since $s^{\prime}_{i}$ is a value for all $i$ , $\sigma_{k-1}(\sigma^{\prime}(x))\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{% \mathcal{R}}^{*}\sigma_{k}(x)$ for all $x\in\bigcup_{i=1}^{n}\operatorname{Var}(s^{\prime}_{i})$ . Now we show that replacing $({s_{k-1}^{\sharp}}\Rightarrow{t_{k-1}^{\sharp}}\ [\varphi_{k-1}],\sigma_{k-1})$ and $({s_{k}^{\sharp}}\Rightarrow{t_{k}^{\sharp}}\ [\varphi_{k}],\sigma_{k})$ by $({s_{k-1}^{\sharp}}\Rightarrow{t_{k}^{\sharp}\sigma^{\prime}}\ [\varphi_{k-1}% \wedge(\varphi_{k}\sigma^{\prime})],\sigma_{k-1}\cup\sigma_{k})$ yields an infinite innermost chain. First, it is routine to verify that $\sigma_{k-1}\cup\sigma_{k}$ respects $\varphi_{k-1}\wedge(\varphi_{k}\sigma^{\prime})$ . Next, $s_{k-1}^{\sharp}(\sigma_{k-1}\cup\sigma_{k})=s_{k-1}^{\sharp}\sigma_{k-1}$ so it is in normal form. Last, $t_{k}^{\sharp}\sigma^{\prime}(\sigma_{k-1}\cup\sigma_{k})\xrightarrow{% \scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}^{*}t_{k}^{\sharp}\sigma_{k}% \xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}^{*}s_{k+1}^{\sharp}% \sigma_{k+1}$ . $\hfill\blacktriangleleft$

We present some auxiliary results for the two classes of DP processors based on usable rules in a unified way, regardless of whether an argument filtering is applied. When no filtering is applied, let $\operatorname{regard}(\mathsf{f})=\{\,1,\ldots,n\,\}$ for each $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B$ with $B\in\mathcal{S}$ .

Definition 39.

The set $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t)$ of actually usable symbols in a term $t$ is (1) $\{\,(\mathsf{f},n)\,\}\cup\bigcup_{i\in\operatorname{regard}(\mathsf{f})\cap\{% \,1,\ldots,n\,\}}\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t_{i})$ if $t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for $\mathsf{f}\in\mathcal{F}^{\sharp}$ , $t$ is not a ground theory term, and is not in normal form (with respect to $\mathcal{Q}$ ), or (2) $\emptyset$ otherwise.

Lemma 40.

Given a constraint $\varphi$ and a substitution $\sigma$ such that $\sigma(x)$ is in normal form for all $x$ and is a theory value if $x\in\operatorname{Var}(\varphi)$ : $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t\sigma)\subseteq\mathcal{U}_{% \mathcal{F}}(t)[\varphi]$ for all $t$ with $\bot\notin\mathcal{U}_{\mathcal{F}}(t)[\varphi]$ .

Proof of Lemma 40.

By induction on $t$ . If $t={x}\ {{t}_{1}\cdots{t}_{n}}$ with $x\in\mathcal{V}$ , then $n=0$ because $\bot\notin\mathcal{U}_{\mathcal{F}}(t)[\varphi]$ . Hence, $t\sigma=\sigma(x)$ is in normal form, and therefore $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t\sigma)=\emptyset$ . Otherwise, $t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for $\mathsf{f}\in\mathcal{F}^{\sharp}$ . If $t\sigma={\mathsf{f}}\ {(t_{1}\sigma)\cdots(t_{n}\sigma)}$ is not a ground theory term, $t\notin T({\mathcal{F}}_{\vartheta},\operatorname{Var}(\varphi))$ because $\sigma(x)$ is a theory value for all $x\in\operatorname{Var}(\varphi)$ . So if $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t\sigma)\neq\emptyset$ , $\mathcal{U}_{\mathcal{F}}(t)[\varphi]=\{\,(\mathsf{f},n)\,\}\cup\bigcup_{i\in% \operatorname{regard}(\mathsf{f})\cap\{\,1,\ldots,n\,\}}\mathcal{U}_{\mathcal{% F}}(t_{i})[\varphi]$ , and therefore $\bot\notin\mathcal{U}_{\mathcal{F}}(t_{i})[\varphi]$ for each such $i$ . By induction, $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t_{i}\sigma)\subseteq\mathcal{U}_{% \mathcal{F}}(t_{i})[\varphi]$ . Hence, $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t\sigma)\subseteq\mathcal{U}_{% \mathcal{F}}(t)[\varphi]$ . $\hfill\blacktriangleleft$

Lemma 41.

Given a set $\mathcal{P}$ of SDPs and a set $\mathcal{R}$ of rules such that $\mathcal{N}\!\mathcal{F}(\mathcal{Q})\subseteq\mathcal{N}\!\mathcal{F}(% \mathcal{R})$ and $\mathcal{U}(\mathcal{P},\mathcal{R})$ is defined: for all terms $t$ , $t^{\prime}$ , if $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t)\subseteq\mathcal{U}_{\mathcal{F}}(% \mathcal{P},\mathcal{R})$ and $t\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}t^{\prime}$ , $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})\subseteq\mathcal{U}_{% \mathcal{F}}(\mathcal{P},\mathcal{R})$ .

Proof of Lemma 41.

By induction on $t$ .

(1)

$t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for $\mathsf{f}\in\mathcal{F}$ , and there exist a rewrite rule ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ , substitution $\sigma$ and number $p\leq n$ such that ${\mathsf{f}}\ {{t}_{1}\cdots{t}_{p}}=\ell\sigma$ , $t^{\prime}={(r\sigma)}\ {{t}_{p+1}\cdots{t}_{n}}$ , $\sigma(x)$ is in normal form for all $x$ and $\sigma$ respects $\varphi$ . Since $\mathcal{N}\!\mathcal{F}(\mathcal{Q})\subseteq\mathcal{N}\!\mathcal{F}(% \mathcal{R})$ , $t$ is not in $\mathcal{Q}$ -normal form, so $(\mathsf{f},n)\in\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t)\subseteq\mathcal{% U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , and therefore $\mathcal{U}_{\mathcal{F}}({r}\ {{x}_{p+1}\cdots{x}_{n}})[\varphi]\subseteq% \mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ where ${x}_{p+1},\ldots,{x}_{n}$ are fresh variables. Since $\mathcal{U}(\mathcal{P},\mathcal{R})$ is defined, $\bot\notin\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , and therefore $\bot\notin\mathcal{U}_{\mathcal{F}}({r}\ {{x}_{p+1}\cdots{x}_{n}})[\varphi]$ . If $p=n$ , due to Lemma 40, $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})=\mathcal{U}_{\mathcal{F}}% ^{\mathfrak{a}}(r\sigma)\subseteq\mathcal{U}_{\mathcal{F}}(r)[\varphi]% \subseteq\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ . Otherwise, $r={\mathsf{g}}\ {{r}_{1}\cdots{r}_{q}}$ for $\mathsf{g}\in\mathcal{F}$ . Then $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})=\mathcal{U}_{\mathcal{F}}% ^{\mathfrak{a}}({(r\sigma)}\ {{t}_{p+1}\cdots{t}_{n}})\subseteq\{\,(\mathsf{g}% ,q+n-p)\,\}\cup\bigcup\{\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(r_{i}\sigma)% \mid 1\leq i\leq q,i\in\operatorname{regard}(\mathsf{g})\}\cup\bigcup\{% \mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t_{p+j})\mid 1\leq j\leq n-p,q+j\in% \operatorname{regard}(\mathsf{g})\}$ and $\mathcal{U}_{\mathcal{F}}({r}\ {{x}_{p+1}\cdots{x}_{n}})[\varphi]=\{\,(\mathsf% {g},q+n-p)\,\}\cup\bigcup\{\mathcal{U}_{\mathcal{F}}(r_{i})[\varphi]\mid 1\leq i% \leq q,i\in\operatorname{regard}(\mathsf{g})\}$ . Since $\bot\notin\mathcal{U}_{\mathcal{F}}({r}\ {{x}_{p+1}\cdots{x}_{n}})[\varphi]$ , for each such $i$ , $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(r_{i}\sigma)\subseteq\mathcal{U}_{% \mathcal{F}}(r_{i})[\varphi]$ due to Lemma 40. Since $\mathcal{U}(\mathcal{P},\mathcal{R})$ is defined, each $p+j\in\operatorname{regard}(\mathsf{f})$ , and therefore $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t_{p+j})\subseteq\mathcal{U}_{% \mathcal{F}}^{\mathfrak{a}}(t)$ . Hence, $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})\subseteq\mathcal{U}_{% \mathcal{F}}({r}\ {{x}_{p+1}\cdots{x}_{n}})[\varphi]\cup\mathcal{U}_{\mathcal{% F}}^{\mathfrak{a}}(t)\subseteq\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ .
(2)

$t={\mathsf{f}}\ {{v}_{1}\cdots{v}_{n}}$ where $\mathsf{f}$ is a calculation symbol and ${v}_{1},\ldots,{v}_{n}$ are theory values, and $t$ has a base type. Then $t\rightarrow_{\kappa}t^{\prime}$ and $t^{\prime}$ is a theory value. Hence, $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})=\emptyset$ .
(3)

$t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for $\mathsf{f}\in\mathcal{F}^{\sharp}$ , and $t^{\prime}={{{\mathsf{f}}\ {{t}_{1}\cdots{t}_{k-1}}}\ {t_{k}^{\prime}}}\ {{t}_% {k+1}\cdots{t}_{n}}$ for some $k$ with $t_{k}\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}t_{k}^{\prime}$ . If $t$ is a ground theory term, so is $t^{\prime}$ , hence $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})=\emptyset$ ; so assume otherwise. If $k\notin\operatorname{regard}(\mathsf{f})$ , $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})\subseteq\mathcal{U}_{% \mathcal{F}}^{\mathfrak{a}}(t)\subseteq\mathcal{U}_{\mathcal{F}}(\mathcal{P},% \mathcal{R})$ . If $k\in\operatorname{regard}(\mathsf{f})$ , $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t_{k})\subseteq\mathcal{U}_{\mathcal{% F}}^{\mathfrak{a}}(t)\subseteq\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ . By induction, $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t_{k}^{\prime})\subseteq\mathcal{U}_{% \mathcal{F}}(\mathcal{P},\mathcal{R})$ . Then $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})\subseteq\mathcal{U}_{% \mathcal{F}}^{\mathfrak{a}}(t)\cup\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t_{% k}^{\prime})\subseteq\mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ .
(4)

$t={x}\ {{t}_{1}\cdots{t}_{n}}$ for $x\in\mathcal{V}$ , and $t^{\prime}={{{x}\ {{t}_{1}\cdots{t}_{k-1}}}\ {t_{k}^{\prime}}}\ {{t}_{k+1}% \cdots{t}_{n}}$ ; then $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})=\emptyset$ .

$\hfill\blacktriangleleft$

Theorem 42.

Usable-rules processors are sound.

Proof of Theorem 42.

Given a DP problem $(\mathcal{P},\mathcal{R})$ such that $\mathcal{N}\!\mathcal{F}(\mathcal{Q})\subseteq\mathcal{N}\!\mathcal{F}(% \mathcal{R})$ and $\mathcal{U}(\mathcal{P},\mathcal{R})$ is defined, and an infinite innermost $(\mathcal{P},\mathcal{R})$ -chain $({s_{0}^{\sharp}}\Rightarrow{t_{0}^{\sharp}}\ [\varphi_{0}],\sigma_{0}),({s_{1% }^{\sharp}}\Rightarrow{t_{1}^{\sharp}}\ [\varphi_{1}],\sigma_{1}),\ldots$ : for all $i$ , since $\mathcal{U}_{\mathcal{F}}(t_{i}^{\sharp})[\varphi_{i}]\subseteq\mathcal{U}_{% \mathcal{F}}(\mathcal{P},\mathcal{R})$ , $\bot\notin\mathcal{U}_{\mathcal{F}}(t_{i}^{\sharp})[\varphi_{i}]$ , and due to Lemma 40, $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t_{i}^{\sharp}\sigma_{i})\subseteq% \mathcal{U}_{\mathcal{F}}(t_{i}^{\sharp})[\varphi_{i}]\subseteq\mathcal{U}_{% \mathcal{F}}(\mathcal{P},\mathcal{R})$ . Now due to Lemma 41, for all $t^{\prime}$ such that $t_{i}^{\sharp}\sigma_{i}\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{% R}}^{*}t^{\prime}$ , $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})\subseteq\mathcal{U}_{% \mathcal{F}}(\mathcal{P},\mathcal{R})$ , so any $\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}$ -step from $t^{\prime}$ is a $\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{U}(\mathcal{P},\mathcal{% R})}$ -step, given the definition of $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}()$ . $\hfill\blacktriangleleft$

Below we let $\pi$ denote $\pi_{\mathfrak{t}}$ – the argument filtering with respect to the Boolean $\mathfrak{t}$ – and define $\sigma^{\pi}$ for each substitution $\sigma$ by letting $\sigma^{\pi}(x)$ be $\pi(\sigma(x))$ .

Lemma 43.

Given a logical constraint $\varphi$ and a substitution $\sigma$ such that $\sigma(x)$ is a theory value for all $x\in\operatorname{Var}(\varphi)$ , $\pi_{\varphi}(t)\sigma^{\pi}=\pi(t\sigma)$ for each pattern $t$ such that all the variables in $\operatorname{Var}(t)$ whose type is a theory sort are also in $\operatorname{Var}(\varphi)$ .

Proof of Lemma 43.

By induction on $t$ . If $t={x}\ {{t}_{1}\cdots{t}_{n}}$ with $x\in\mathcal{V}$ , then $n=0$ because $t$ is a pattern. Hence, $\pi_{\varphi}(t)\sigma^{\pi}=\sigma^{\pi}(x)=\pi(\sigma(x))=\pi(t\sigma)$ . Otherwise, $t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for $\mathsf{f}\in\mathcal{F}^{\sharp}$ . If $t$ is in $T({\mathcal{F}}_{\vartheta},\operatorname{Var}(\varphi))$ and has a base type, $\pi_{\varphi}(t)\sigma^{\pi}=t\sigma^{\pi}=t\sigma=\pi(t\sigma)$ because $\sigma(x)$ is a theory value for all $x\in\operatorname{Var}(t)$ and $\pi(v)=v$ for each theory value $v$ . Otherwise, if $\operatorname{regard}(\mathsf{f})\cap\{\,1,\ldots,n\,\}=\{\,{i}_{1},\ldots,{i}% _{k}\,\}$ (with ${i}_{1}<\cdots<{i}_{k}$ ), $\pi_{\varphi}(t)\sigma^{\pi}={\mathsf{f}_{n}}\ {(\pi_{\varphi}(t_{i_{1}})% \sigma^{\pi})\cdots(\pi_{\varphi}(t_{i_{k}})\sigma^{\pi})}$ and $\pi(t\sigma)={\mathsf{f}_{n}}\ {\pi(t_{i_{1}}\sigma)\cdots\pi(t_{i_{k}}\sigma)}$ . By induction, $\pi_{\varphi}(t_{i_{j}})\sigma^{\pi}=\pi(t_{i_{j}}\sigma)$ for all $j\in\{\,1,\ldots,k\,\}$ . $\hfill\blacktriangleleft$

Lemma 44.

Given a set $\mathcal{P}$ of SDPs, a set $\mathcal{R}$ of rewrite rules and a constrained relation $\succeq$ such that $\mathcal{U}(\mathcal{P},\mathcal{R})$ is defined, ${\ell}\mathrel{\succeq}_{\varphi}{r}$ for all ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{U}(\mathcal{P},\mathcal{R})$ and $\succeq$ is covered by some reflexive, transitive and monotonic relation $\sqsupseteq$ : if $\mathcal{U}_{\mathcal{F}}(t)[\varphi]\subseteq\mathcal{U}_{\mathcal{F}}(% \mathcal{P},\mathcal{R})$ and $\sigma(x)$ is a theory value for all $x\in\operatorname{Var}(\varphi)$ , $\pi_{\varphi}(t)\sigma^{\pi}\,{\downarrow}_{\kappa}\sqsupseteq\pi(t\sigma)\,{% \downarrow}_{\kappa}$ .

Proof of Lemma 44.

By induction on $t$ . If $t={x}\ {{t}_{1}\cdots{t}_{n}}$ with $x\in\mathcal{V}$ then $n=0$ because $\bot\notin\mathcal{U}_{\mathcal{F}}(t)[\varphi]$ . Hence, $\pi_{\varphi}(t)\sigma^{\pi}=\sigma^{\pi}(x)=\pi(\sigma(x))=\pi(t\sigma)$ . Otherwise, $t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for $\mathsf{f}\in\mathcal{F}^{\sharp}$ . If $t$ is in $T({\mathcal{F}}_{\vartheta},\operatorname{Var}(\varphi))$ and has a base type, $\pi_{\varphi}(t)\sigma^{\pi}=t\sigma^{\pi}=t\sigma=\pi(t\sigma)$ because each $\sigma(x)$ is a theory value so $\pi(\sigma(x))=\sigma(x)$ . Otherwise, we have $\pi_{\varphi}(t)\sigma^{\pi}={\mathsf{f}_{n}}\ {(\pi_{\varphi}(t_{i_{1}})% \sigma^{\pi})\cdots(\pi_{\varphi}(t_{i_{k}})\sigma^{\pi})}$ where $\operatorname{regard}(\mathsf{f})\cap\{\,1,\ldots,n\,\}=\{\,{i}_{1},\ldots,{i}% _{k}\,\}$ and ${i}_{1}<\cdots<{i}_{k}$ . By induction, $\pi_{\varphi}(t_{i_{j}})\sigma^{\pi}\,{\downarrow}_{\kappa}\sqsupseteq\pi(t_{i% _{j}}\sigma)\,{\downarrow}_{\kappa}$ for all $j\in\{\,1,\ldots,k\,\}$ , and therefore $\pi_{\varphi}(t)\sigma^{\pi}\,{\downarrow}_{\kappa}\sqsupseteq{\mathsf{f}_{n}}% \ {\pi(t_{i_{1}}\sigma)\,{\downarrow}_{\kappa}\cdots\pi(t_{i_{k}}\sigma)\,{% \downarrow}_{\kappa}}$ . If $t\sigma$ is a ground theory term with a base type, ${{\mathsf{f}_{n}}\ {x_{i_{1}}\cdots x_{i_{k}}}}\rightarrow{y}\ [y={\mathsf{f}}% \ {{x}_{1}\cdots{x}_{n}}]\in\mathcal{U}(\mathcal{P},\mathcal{R})$ ; because $\sqsupseteq$ covers $\succeq$ , ${\mathsf{f}_{n}}\ {\pi(t_{i_{1}}\sigma)\,{\downarrow}_{\kappa}\cdots\pi(t_{i_{% k}}\sigma)\,{\downarrow}_{\kappa}}={\mathsf{f}_{n}}\ {(t_{i_{1}}\sigma)\,{% \downarrow}_{\kappa}\cdots(t_{i_{k}}\sigma)\,{\downarrow}_{\kappa}}\sqsupseteq% (t\sigma)\,{\downarrow}_{\kappa}=\pi(t\sigma)\,{\downarrow}_{\kappa}$ . Otherwise, we have $\pi(t\sigma)={\mathsf{f}_{n}}\ {\pi(t_{i_{1}}\sigma)\cdots\pi(t_{i_{k}}\sigma)}$ . $\hfill\blacktriangleleft$

Lemma 45.

Given a set $\mathcal{P}$ of SDPs, a set $\mathcal{R}$ of rules and a constrained relation $\succeq$ where (1) $\mathcal{N}\!\mathcal{F}(\mathcal{Q})\subseteq\mathcal{N}\!\mathcal{F}(% \mathcal{R})$ , (2) $\mathcal{U}(\mathcal{P},\mathcal{R})$ is defined, (3) for all ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ , all $x\in\operatorname{Var}(\ell)$ whose type is a theory sort, $x\in\operatorname{Var}(\varphi)$ , (4) ${\ell}\mathrel{\succeq}_{\varphi}{r}$ for all ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{U}(\mathcal{P},\mathcal{R})$ and (5) $\succeq$ is covered by a reflexive, transitive, monotonic $\sqsupseteq$ : if $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t)\subseteq\mathcal{U}_{\mathcal{F}}(% \mathcal{P},\mathcal{R})$ and $t\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}t^{\prime}$ , $\pi(t)\,{\downarrow}_{\kappa}\sqsupseteq\pi(t^{\prime})\,{\downarrow}_{\kappa}$ .

Proof of Lemma 45.

By induction on $t$ .

(1)

$t$ is a base-type ground theory term; then so is $t^{\prime}$ , and $t\rightarrow_{\kappa}t^{\prime}$ . Hence, $\pi(t)\,{\downarrow}_{\kappa}=\pi(t^{\prime})\,{\downarrow}_{\kappa}$ .
(2)

$t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ for $\mathsf{f}\in\mathcal{F}$ , and there exist a number $p\leq n$ , substitution $\sigma$ and rule ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ such that $\ell={\mathsf{f}}\ {{\ell}_{1}\cdots{\ell}_{p}}$ , $t_{i}=\ell_{i}\sigma$ for all $i\in\{\,1,\ldots,p\,\}$ , $t^{\prime}={(r\sigma)}\ {{t}_{p+1}\cdots{t}_{n}}$ , $\sigma(x)$ is in normal form for all $x$ and $\sigma$ respects $\varphi$ . Since $\mathcal{N}\!\mathcal{F}(\mathcal{Q})\subseteq\mathcal{N}\!\mathcal{F}(% \mathcal{R})$ , $(\mathsf{f},n)\in\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t)\subseteq\mathcal{% U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , and therefore $\mathcal{U}_{\mathcal{F}}({r}\ {{x}_{p+1}\cdots{x}_{n}})[\varphi]\subseteq% \mathcal{U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ and ${\pi_{\varphi}({\ell}\ {{x}_{p+1}\cdots{x}_{n}})}\rightarrow{\pi_{\varphi}({r}% \ {{x}_{p+1}\cdots{x}_{n}})}\ [\varphi]\in\mathcal{U}(\mathcal{P},\mathcal{R})$ for ${x}_{p+1},\ldots,{x}_{n}$ fresh variables. We have $\pi(t)={\mathsf{f}_{n}}\ {\pi(t_{i_{1}})\cdots\pi(t_{i_{k}})}$ where $\operatorname{regard}(\mathsf{f})\cap\{\,1,\ldots,n\,\}=\{\,{i}_{1},\ldots,{i}% _{k}\,\}$ and ${i}_{1}<\cdots<{i}_{l}\leq p<{i}_{l+1}<\cdots<{i}_{k}$ . By Lemma 43, $\pi_{\varphi}(\ell_{j})\sigma^{\pi}=\pi(\ell_{j}\sigma)=\pi(t_{j})$ for all $j\in\{\,1,\ldots,l\,\}$ . Since $\pi_{\varphi}(x_{j})([{x_{i}}\coloneq{t_{i}}]_{i=p+1}^{n})^{\pi}=\pi(t_{j})$ for all $j\in\{\,l+1,\ldots,k\,\}$ , $\pi(t)=\pi_{\varphi}({\ell}\ {{x}_{p+1}\cdots{x}_{n}})(\sigma\cup[{x_{i}}% \coloneq{t_{i}}]_{i=p+1}^{n})^{\pi}$ . Due to Lemma 44, $\pi_{\varphi}({r}\ {{x}_{p+1}\cdots{x}_{n}})(\sigma\cup[{x_{i}}\coloneq{t_{i}}% ]_{i=p+1}^{n})^{\pi}\,{\downarrow}_{\kappa}\sqsupseteq\pi(t^{\prime})\,{% \downarrow}_{\kappa}$ . Because $\sqsupseteq$ covers $\succeq$ and $(\sigma\cup[{x_{i}}\coloneq{t_{i}}]_{i=p+1}^{n})^{\pi}$ respects $\varphi$ , $\pi(t)\,{\downarrow}_{\kappa}\sqsupseteq\pi(t^{\prime})\,{\downarrow}_{\kappa}$ .
(3)

$t={\mathsf{f}}\ {{t}_{1}\cdots{t}_{n}}$ ( $\mathsf{f}\in\mathcal{F}^{\sharp}$ ) is not a base-type ground theory term, and there is $m$ such that $t^{\prime}={{{\mathsf{f}}\ {{t}_{1}\cdots{t}_{m-1}}}\ {t_{m}^{\prime}}}\ {\\ {t}_{m+1}\cdots{t}_{n}}$ and $t_{m}\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{R}}t_{m}^{\prime}$ . Then $\pi(t)={\mathsf{f}_{n}}\ {\pi(t_{i_{1}})\cdots\pi(t_{i_{k}})}$ where $\operatorname{regard}(\mathsf{f})\cap\{\,1,\ldots,n\,\}=\{\,{i}_{1},\ldots,{i}% _{k}\,\}$ and ${i}_{1}<\cdots<{i}_{k}$ . Let $t_{i}^{\prime}$ be $t_{i}$ for all $i\in\{\,1,\ldots,n\,\}\setminus\{\,m\,\}$ . By induction, $\pi(t_{m})\,{\downarrow}_{\kappa}\sqsupseteq\pi(t_{m}^{\prime})\,{\downarrow}_% {\kappa}$ , and therefore $\pi(t)\,{\downarrow}_{\kappa}\sqsupseteq{\mathsf{f}_{n}}\ {\pi(t_{i_{1}}^{% \prime})\,{\downarrow}_{\kappa}\cdots\pi(t_{i_{k}}^{\prime})\,{\downarrow}_{% \kappa}}$ . If $t^{\prime}$ is a ground theory term that has a base type, since $(\mathsf{f},n)\in\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t)\subseteq\mathcal{% U}_{\mathcal{F}}(\mathcal{P},\mathcal{R})$ , we have ${{\mathsf{f}_{n}}\ {x_{i_{1}}\cdots x_{i_{k}}}}\rightarrow{y}\ [y={\mathsf{f}}% \ {{x}_{1}\cdots{x}_{n}}]\in\mathcal{U}(\mathcal{P},\mathcal{R})$ ; because $\sqsupseteq$ covers $\succeq$ , ${\mathsf{f}_{n}}\ {\pi(t_{i_{1}}^{\prime})\,{\downarrow}_{\kappa}\cdots\pi(t_{% i_{k}}^{\prime})\,{\downarrow}_{\kappa}}={\mathsf{f}_{n}}\ {t_{i_{1}}^{\prime}% \,{\downarrow}_{\kappa}\cdots t_{i_{k}}^{\prime}\,{\downarrow}_{\kappa}}% \sqsupseteq t^{\prime}\,{\downarrow}_{\kappa}=\pi(t^{\prime})\,{\downarrow}_{\kappa}$ . Otherwise, $\pi(t^{\prime})\,{\downarrow}_{\kappa}={\mathsf{f}_{n}}\ {\pi(t_{i_{1}}^{% \prime})\,{\downarrow}_{\kappa}\cdots\pi(t_{i_{k}}^{\prime})\,{\downarrow}_{% \kappa}}$ .
(4)

$t={x}\ {{t}_{1}\cdots{t}_{k}}\cdots t_{n}$ for $x\in\mathcal{V}$ , and $t^{\prime}=x\ t_{1}\cdots t_{k}^{\prime}\cdots t_{n}$ ; then $\pi(t)=\bullet_{\mu(A)}=\pi(t^{\prime})$ .

$\hfill\blacktriangleleft$

Theorem 46.

If the rewrite rules are preprocessed by Lemma 7, and all theory sorts are inextensible, then reduction pair processors with an argument filtering are sound.

Proof of Theorem 46.

Following Theorem 42, for all $i$ and $t^{\prime}$ such that $t_{i}^{\sharp}\sigma_{i}\xrightarrow{\scriptscriptstyle\mathcal{Q}}_{\mathcal{% R}}^{*}t^{\prime}$ , $\mathcal{U}_{\mathcal{F}}^{\mathfrak{a}}(t^{\prime})\subseteq\mathcal{U}_{% \mathcal{F}}(\mathcal{P},\mathcal{R})$ . Due to Lemma 45, $\pi(t_{i}^{\sharp}\sigma_{i})\,{\downarrow}_{\kappa}\sqsupseteq\pi(s_{i+1}^{% \sharp}\sigma_{i+1})\,{\downarrow}_{\kappa}$ for all $i$ . For all $i$ , if ${s_{i}^{\sharp}}\Rightarrow{t_{i}^{\sharp}}\ [\varphi_{i}]\in\mathcal{P}^{\prime}$ , due to Lemmas 43 and 44, $\pi(s_{i}^{\sharp}\sigma_{i})\,{\downarrow}_{\kappa}=\pi_{\varphi_{i}}(s_{i}^{% \sharp})\sigma_{i}^{\pi}\,{\downarrow}_{\kappa}\sqsupset\pi_{\varphi_{i}}(t_{i% }^{\sharp})\sigma_{i}^{\pi}\,{\downarrow}_{\kappa}\sqsupseteq\pi(t_{i}^{\sharp% }\sigma_{i})\,{\downarrow}_{\kappa}$ ; if ${s_{i}^{\sharp}}\Rightarrow{t_{i}^{\sharp}}\ [\varphi_{i}]\in\mathcal{P}% \setminus\mathcal{P}^{\prime}$ , similarly $\pi(s_{i}^{\sharp}\sigma_{i})\,{\downarrow}_{\kappa}\sqsupseteq\pi(t_{i}^{% \sharp}\sigma_{i})\,{\downarrow}_{\kappa}$ . Since $\sqsupset$ is well-founded, an infinite innermost $(\mathcal{P},\mathcal{R})$ -chain leads to an infinite innermost $(\mathcal{P}\setminus\mathcal{P}^{\prime},\mathcal{R})$ -chain. $\hfill\blacktriangleleft$

A.2 The Proofs of Theorems 14 and 36

For the properties of $\mathbb{C}$ -computability, see Appendix A in the extended version of [13]. The following proofs are largely based on Appendix A.3 in [20]; here the novelty lies on the innermostness of chains. Note that undefined function symbols are $\mathbb{C}$ -computable (see [20]).

Lemma 47.

Assume given an AFP system $\mathcal{R}_{0}$ with sort ordering $\succsim$ , an extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$ and a sort ordering $\succsim^{\prime}$ which extends $\succsim$ over sorts in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ . For each defined symbol $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow B$ in $\mathcal{R}_{0}$ where $B$ is a sort, if ${\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ is not $\mathbb{C}$ -computable in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ with $\succsim^{\prime}$ but $s_{i}$ is for all $i$ , then there exist an SDP ${{\mathsf{f}^{\sharp}}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}}\Rightarrow{{% \mathsf{g}^{\sharp}}\ {{t}_{1}\cdots{t}_{n}}}\ [\varphi]\in\operatorname{SDP}(% \mathcal{R}_{0})$ , a substitution $\sigma$ and a natural number $p$ such that (1) $s_{i}\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}_{0}\cup\mathcal{R% }_{1}}^{*}s_{i}^{\prime}\sigma$ and $s_{i}^{\prime}\sigma$ is in normal form for all $i\leq p$ , (2) $s_{i}^{\prime}$ is a fresh variable ( $s_{i}^{\prime}$ does not occur in $s_{j}^{\prime}$ for any $j\neq i$ ) and $\sigma(s_{i}^{\prime})=s_{i}$ for all $i>p$ , (3) $\sigma$ respects $\varphi$ , and (4) $({\mathsf{g}}\ {{t}_{1}\cdots{t}_{n}})\sigma={\mathsf{g}}\ {(t_{1}\sigma)% \cdots(t_{n}\sigma)}$ is not $\mathbb{C}$ -computable in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ with $\succsim^{\prime}$ but $u\sigma$ is for each proper subterm $u$ of ${\mathsf{g}}\ {{t}_{1}\cdots{t}_{n}}$ .

Proof.

If the only reducts of ${\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ were values or ${\mathsf{f}}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}$ with $s_{i}\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}_{0}\cup\mathcal{R% }_{1}}^{*}s_{i}^{\prime}$ for all $i$ then ${\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ would be computable. Hence, there exist ${{\mathsf{f}}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{p}}}\rightarrow{r}\ [% \varphi]\in\mathcal{R}_{0}$ ( $\mathsf{f}$ cannot be defined in $\mathcal{R}_{1}$ ) and $\sigma^{\prime}$ such that $s_{i}\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}_{0}\cup\mathcal{R% }_{1}}^{*}s_{i}^{\prime}\sigma^{\prime}$ and $s_{i}^{\prime}\sigma^{\prime}$ is in normal form for all $i\leq p$ , and $\sigma^{\prime}$ respects $\varphi$ ; ${(r\sigma^{\prime})}\ {{s}_{p+1}\cdots{s}_{m}}$ is thus a reduct of ${\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ . At least one such reduct is uncomputable. Let ${(r\sigma^{\prime})}\ {{s}_{p+1}\cdots{s}_{m}}$ be uncomputable, and therefore so is $r\sigma^{\prime}$ . Also all $\sigma^{\prime}(x)$ are computable, since these are accessible subterms of some $s_{i}^{\prime}$ , since $\mathcal{R}_{0}$ is AFP.

Take a minimal subterm ${a}\ {{t}_{1}\cdots{t}_{q}}$ of $r$ such that $t\sigma^{\prime}$ is uncomputable. By minimality, each $t_{i}\sigma^{\prime}$ is computable. Hence, $a$ cannot be a variable, value or constructor, as then $\sigma^{\prime}(x)$ would be computable, implying computability of $t\sigma^{\prime}$ . Hence, $a$ is a defined symbol $\mathsf{g}$ .

We have ${{{\mathsf{f}^{\sharp}}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{p}}}\ {{x}_{p+1}% \cdots{x}_{m}}}\Rightarrow{{{\mathsf{g}^{\sharp}}\ {{t}_{1}\cdots{t}_{q}}}\ {{% y}_{q+1}\cdots{y}_{n}}}\ [\varphi]\in\operatorname{SDP}(\mathcal{R}_{0})$ . Because $t\sigma^{\prime}$ is uncomputable, there exist computable terms ${t^{\prime}}_{q+1},\ldots,{t^{\prime}}_{n}$ such that ${(t\sigma^{\prime})}\ {{t^{\prime}}_{q+1}\cdots{t^{\prime}}_{n}}={{\mathsf{g}}% \ {(t_{1}\sigma^{\prime})\cdots(t_{q}\sigma^{\prime})}}\ {{t^{\prime}}_{q+1}% \cdots{t^{\prime}}_{n}}$ is uncomputable. Let $\sigma$ be such that $\sigma(x_{i})=s_{i}$ for all $i>p$ , $\sigma(y_{i})=t_{i}^{\prime}$ for all $i>q$ , and $\sigma(z)=\sigma^{\prime}(z)$ for any other $z$ . Let $s_{i}^{\prime}$ denote $x_{i}$ for $i>p$ and $t_{i}$ denote $y_{i}$ for $i>q$ ; then ${{\mathsf{f}^{\sharp}}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}}\Rightarrow{{% \mathsf{g}^{\sharp}}\ {{t}_{1}\cdots{t}_{n}}}\ [\varphi]$ , $\sigma$ and $p$ satisfy all requirements. $\hfill\blacktriangleleft$

Corollary 48.

Given an AFP system $\mathcal{R}_{0}$ with sort ordering $\succsim$ , an extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$ and a sort ordering $\succsim^{\prime}$ which extends $\succsim$ over sorts in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ , for each defined symbol $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow B$ in $\mathcal{R}_{0}$ ( $B$ a sort), if ${\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ is not $\mathbb{C}$ -computable in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ with $\succsim^{\prime}$ but each $s_{i}$ is, there exists an infinite innermost $(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$ -chain $({{\mathsf{f}^{\sharp}}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}}\Rightarrow{% t^{\sharp}}\ [\varphi],\sigma),\ldots$

Proof.

Repeatedly applying Lemma 47 (on ${\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ , then on ${\mathsf{g}}\ {(t_{1}\sigma)\cdots(t_{n}\sigma)}$ and so on) we get three infinite sequences: one of SDPs in $\operatorname{SDP}(\mathcal{R}_{0})$ $({{\mathsf{f}_{i}^{\sharp}}\ {{s}_{i,1}\cdots{s}_{i,m_{i}}}}\Rightarrow{{% \mathsf{f}_{i+1}^{\sharp}}\ {{t}_{i,1}\cdots{t}_{i,n_{i}}}}\ [\varphi_{i}])_{i}$ where $\mathsf{f}_{0}=\mathsf{f}$ , one of substitutions $(\sigma_{i})_{i}$ and one of natural numbers $(p_{i})_{i}$ . Since $\xrightarrow{\scriptscriptstyle\mathrm{i}}_{\mathcal{R}_{0}\cup\mathcal{R}_{1}}$ is exactly $\xrightarrow{\scriptscriptstyle\mathcal{R}_{0}\cup\mathcal{R}_{1}}_{\mathcal{R% }_{0}\cup\mathcal{R}_{1}}$ , combining the SDPs and the substitutions almost gives us an infinite innermost $(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$ -chain, except that $s_{i,j}\sigma_{i}$ may not be in normal form if $j>p_{i}$ .

We define $(\sigma^{\prime}_{i})_{i}$ so that, together with the SDPs, we obtain an infinite chain. For all $i, j$ with $p_{i}<j\leq m_{i}$ , $s_{i,j}$ is a fresh variable and $\sigma_{i}(s_{i,j})$ is $\mathbb{C}$ -computable. Let $\sigma^{\prime}_{i}(x)$ be $\sigma_{i}(x)$ for $x\in\mathcal{V}\setminus\{\,{s}_{i,p_{i}+1},\ldots,{s}_{i,m_{i}}\,\}$ . To define $\sigma^{\prime}_{i}(s_{i,j})$ for $j>p_{i}$ , let $k_{0}$ be $j$ and for $l\geq 0$ , if $k_{l}$ exists and $k_{l}>p_{i+l}$ , let $k_{l+1}$ be the index (if any) with $s_{i+l,k_{l}}=t_{i+l,k_{l+1}}$ . There are two options:

(1)

If $k_{l}>p_{i+l}$ for all $l$ such that $k_{l}$ is defined, regardless of whether the sequence is finite, $\sigma_{i+l}(s_{i+l,k_{l}})=\sigma_{i+l}(t_{i+l,k_{l+1}})=\sigma_{i+l+1}(s_{i+% l+1,k_{l+1}})$ for all $l$ such that $k_{l+1}$ is defined. Let $u$ be an arbitrary normal form of $\sigma_{i}(s_{i,j})$ , and let $\sigma^{\prime}_{i+l}(s_{i+l,k_{l}})$ be $u$ for all $l$ where $k_{l}$ is defined.
(2)

Otherwise, the sequence $(k_{l})_{l}$ is finite, and $k_{q}\leq p_{i+q}$ where $k_{q}$ is the last in the sequence. Then $s_{i+q,k_{q}}\sigma_{i+q}$ is in normal form. Let $\sigma^{\prime}_{i+l}(s_{i+l,k_{l}})$ be $s_{i+q,k_{q}}\sigma_{i+q}$ for all $l<q$ .

Hence, we have built an infinite innermost $(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$ -chain. $\hfill\blacktriangleleft$

Theorem 14. [Restated, see original statement.]

An AFP system $\mathcal{R}$ is innermost (and therefore call-by-value) terminating if there exists no infinite innermost $(\operatorname{SDP}(\mathcal{R}),\mathcal{R})$ -chain.

Proof.

Towards a contradiction, assume that $\mathcal{R}$ is not innermost terminating. Then there is an uncomputable (not $\mathbb{C}$ -computable) term $u$ . Take a minimal subterm $s$ of $u$ that is uncomputable; then $u={\mathsf{f}}\ {{s}_{1}\cdots{s}_{k}}$ where $\mathsf{f}$ is defined and each $s_{i}$ is computable. Let $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow B$ for $B\in\mathcal{S}$ . Since $s={\mathsf{f}}\ {{s}_{1}\cdots{s}_{k}}$ is uncomputable, there exist computable ${s}_{k+1},\ldots,{s}_{m}$ with ${s}\ {{s}_{k+1}\cdots{s}_{m}}={\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ uncomputable. By Corollary 48 (with $\mathcal{R}_{1}=\emptyset$ ), there is an infinite innermost $(\operatorname{SDP}(\mathcal{R}),\mathcal{R})$ -chain, giving the required contradiction. $\hfill\blacktriangleleft$

Theorem 36. [Restated, see original statement.]

An accessible function passing system $\mathcal{R}_{0}$ with sort ordering $\succsim$ is universally computable if there exists no infinite innermost $(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$ -chain for any extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$ and extension $\succsim^{\prime}$ of $\succsim$ to sorts in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ .

Proof.

Towards a contradiction, assume that $\mathcal{R}_{0}$ is not universally computable. There exist an extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$ , sort ordering $\succsim^{\prime}$ which extends $\succsim$ over sorts in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ and term $u$ of $\mathcal{R}_{0}$ that is not $\mathbb{C}$ -computable in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ with $\succsim^{\prime}$ . We consider $\mathbb{C}$ -computability in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ . Take a minimal uncomputable subterm $s$ of $u$ ; then $s$ must take the form ${\mathsf{f}}\ {{s}_{1}\cdots{s}_{k}}$ with $\mathsf{f}$ a defined symbol in $\mathcal{R}_{0}$ and each $s_{i}$ computable. Let $\mathsf{f}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow B$ . Because $s$ is uncomputable, there exist computable ${s}_{k+1},\ldots,{s}_{m}$ of $\mathcal{R}_{0}\cup\mathcal{R}_{1}$ with ${s}\ {{s}_{k+1}\cdots{s}_{m}}={\mathsf{f}}\ {{s}_{1}\cdots{s}_{m}}$ uncomputable. Corollary 48 gives the required chain to obtain a contradiction. $\hfill\blacktriangleleft$

[bib.bib1] [1] B. Alarcón, R. Gutiérrez, and S. Lucas. Context-sensitive dependency pairs. IC, 208(8):922–968, 2010. doi:10.1016/J.IC.2010.03.003.

[bib.bib2] [2] T. Aoto and T. Yamada. Argument filterings and usable rules for simply typed dependency pairs. In S. Ghilardi and R. Sebastiani, editors, Proc. FroCoS, pages 117–132, 2009. doi:10.1007/978-3-642-04222-5_7.

[bib.bib3] [3] T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. TCS, 236(1–2):133–178, 2000. doi:10.1016/S0304-3975(99)00207-8.

[bib.bib4] [4] D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software model checking via large-block encoding. In A. Biere and C. Pixley, editors, Proc. FMCAD, pages 25–32, 2009. doi:10.1109/FMCAD.2009.5351147.

[bib.bib5] [5] M. Codish, C. Fuhs, J. Giesl, and P. Schneider-Kamp. Lazy abstraction for size-change termination. In C. G. Fermüller and A. Voronkov, editors, Proc. LPAR (Yogyakarta), pages 217–232, 2010. doi:10.1007/978-3-642-16242-8_16.

[bib.bib6] [6] Community. Termination competition (TermCOMP). URL: https://termination-portal.org/wiki/Termination_Competition.

[bib.bib7] [7] Community. The termination problem database (TPDB). URL: https://github.com/TermCOMP/TPDB.

[bib.bib8] [8] L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In C.R. Ramakrishnan and J. Rehof, editors, Proc. TACAS, pages 337–340, 2008. doi:10.1007/978-3-540-78800-3_24.

[bib.bib9] [9] N. Dershowitz. Hierarchical termination. In N. Dershowitz and N. Lindenstrauss, editors, Proc. CTRS, pages 89–105, 1995. doi:10.1007/3-540-60381-6_6.

[bib.bib10] [10] S. Falke and D. Kapur. A term rewriting approach to the automated termination analysis of imperative programs. In R. A. Schmidt, editor, Proc. CADE, pages 277–293, 2009. doi:10.1007/978-3-642-02959-2_22.

[bib.bib11] [11] S. Falke, D. Kapur, and C. Sinz. Termination analysis of C programs using compiler intermediate languages. In M. Schmidt-Schauß, editor, Proc. RTA, pages 41–50, 2011. doi:10.4230/LIPIcs.RTA.2011.41.

[bib.bib12] [12] C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke. Proving termination of integer term rewriting. In R. Treinen, editor, Proc. RTA, pages 32–47, 2009. doi:10.1007/978-3-642-02348-4_3.

[bib.bib13] [13] C. Fuhs and C. Kop. A static higher-order dependency pair framework. In L. Caires, editor, Proc. ESOP, pages 752–782, 2019. doi:10.1007/978-3-030-17184-1_27.

[bib.bib14] [14] C. Fuhs, C. Kop, and N. Nishida. Verifying procedural programs via constrained rewriting induction. ACM TOCL, 18(2):14:1–14:50, 2017. doi:10.1145/3060143.

[bib.bib15] [15] J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Analyzing program termination and complexity automatically with AProVE. JAR, 58(1):3–31, 2017. doi:10.1007/s10817-016-9388-y.

[bib.bib16] [16] J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated termination proofs for Haskell by term rewriting. ACM TOPLAS, 33(2):7:1–7:39, 2011. doi:10.1145/1890028.1890030.

[bib.bib17] [17] J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs. Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs. In A. King, editor, Proc. PPDP, pages 1–12, 2012. doi:10.1145/2370776.2370778.

[bib.bib18] [18] J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: combining techniques for automated termination proofs. In F. Baader and A. Voronkov, editors, Proc. LPAR, pages 301–331, 2005. doi:10.1007/978-3-540-32275-7_21.

[bib.bib19] [19] J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and improving dependency pairs. JAR, 37(3):155–203, 2006. doi:10.1007/s10817-006-9057-7.

[bib.bib20] [20] L. Guo, K. Hagens, C. Kop, and D. Vale. Higher-order constrained dependency pairs for (universal) computability. pre-publication Arxiv copy of [21] with additional appendix. doi:10.48550/arXiv.2406.19379.

[bib.bib21] [21] L. Guo, K. Hagens, C. Kop, and D. Vale. Higher-order constrained dependency pairs for (universal) computability. In R. Královič and A. Kučera, editors, Proc. MFCS, pages 57:1–57:15, 2024. doi:10.4230/LIPIcs.MFCS.2024.57.

[bib.bib22] [22] L. Guo and C. Kop. Higher-order LCTRSs and their termination. In S. Weirich, editor, Proc. ESOP, pages 331–357, 2024. doi:10.1007/978-3-031-57267-8_13.

[bib.bib23] [23] N. Hirokawa and A. Middeldorp. Automating the dependency pair method. IC, 199(1-2):172–199, 2005. doi:10.1016/J.IC.2004.10.004.

[bib.bib24] [24] N. Hirokawa and A. Middeldorp. Tyrolean Termination Tool: techniques and features. IC, 205(4):474–511, 2007. doi:10.1016/j.ic.2006.08.010.

[bib.bib25] [25] C. Kop. WANDA – a higher order termination tool (system description). In Z. M. Ariola, editor, Proc. FSCD, pages 36:1–36:19, 2020. doi:10.4230/LIPICS.FSCD.2020.36.

[bib.bib26] [26] C. Kop. Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting. In A. P. Felty, editor, Proc. FSCD, pages 1:1–1:17, 2022. doi:10.4230/LIPIcs.FSCD.2022.1.

[bib.bib27] [27] C. Kop et al. The Cora analyzer. URL: https://github.com/hezzel/cora.

[bib.bib28] [28] C. Kop et al. hezzel/cora: FSCD 2025. doi:10.5281/zenodo.15318964.

[bib.bib29] [29] C. Kop and N. Nishida. Term rewriting with logical constraints. In P. Fontaine, C. Ringeissen, and R. A. Schmidt, editors, Proc. FroCoS, pages 343–358, 2013. doi:10.1007/978-3-642-40885-4_24.

[bib.bib30] [30] C. Kop and F. van Raamsdonk. Dynamic dependency pairs for algebraic functional systems. LMCS, 8(2), 2012. doi:10.2168/LMCS-8(2:10)2012.

[bib.bib31] [31] M. R. K. Krishna Rao. Completeness of hierarchical combinations of term rewriting systems. In R. K. Shyamasundar, editor, Proc. FSTTCS, pages 125–138, 1993. doi:10.1007/3-540-57529-4_48.

[bib.bib32] [32] M. R. K. Krishna Rao. Simple termination of hierarchical combinations of term rewriting systems. In M. Hagiya and J. C. Mitchell, editors, Proc. TACS, pages 203–223, 1994. doi:10.1007/3-540-57887-0_97.

[bib.bib33] [33] M. R. K. Krishna Rao. Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, Proc. CAAP, pages 379–393, 1995. doi:10.1007/3-540-59293-8_208.

[bib.bib34] [34] K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static dependency pair method based on strong computability for higher-order rewrite systems. IEICE Trans. Inf. Syst., E92.D(10):2007–2015, 2009. doi:10.1587/transinf.E92.D.2007.

[bib.bib35] [35] K. Kusakari and M. Sakai. Enhancing dependency pair method using strong computability in simply-typed term rewriting. AAECC, 18(5):407–431, 2007. doi:10.1007/s00200-007-0046-9.

[bib.bib36] [36] K. Kusakari and M. Sakai. Static dependency pair method for simply-typed term rewriting and related techniques. IEICE Trans. Inf. Syst., E92.D(2):235–247, 2009. doi:10.1587/transinf.E92.D.235.

[bib.bib37] [37] C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In C. Hankin and D. Schmidt, editors, Proc. POPL, pages 81–92, 2001. doi:10.1145/360204.360210.

[bib.bib38] [38] S. Lucas. Context-sensitive computations in functional and functional logic programs. JFLP, 1998(1), 1998. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-01/A98-01.html.

[bib.bib39] [39] C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl. Automated termination analysis of Java bytecode by term rewriting. In C. Lynch, editor, Proc. RTA, pages 259–276, 2010. doi:10.4230/LIPIcs.RTA.2010.259.

[bib.bib40] [40] S. Suzuki, K. Kusakari, and F. Blanqui. Argument filterings and usable rules in higher-order rewrite systems. IPSJ Online Trans., 4:114–125, 2011. doi:10.2197/ipsjtrans.4.114.

[bib.bib41] [41] R. Thiemann. The DP framework for proving termination of term rewriting. PhD thesis, RWTH Aachen University, Germany, 2007. URL: http://darwin.bth.rwth-aachen.de/opus3/volltexte/2007/2066/.

[bib.bib42] [42] R. Thiemann and J. Giesl. The size-change principle and dependency pairs for termination of term rewriting. AAECC, 16(4):229–270, 2005. doi:10.1007/S00200-005-0179-7.

[bib.bib43] [43] J. van de Pol. Termination proofs for higher-order rewrite systems. In J. Heering, K. Meinke, B. Möller, and T. Nipkow, editors, Proc. HOA, pages 305–325, 1993. doi:10.1007/3-540-58233-9_14.

[bib.bib44] [44] F. van Raamsdonk. Translating logic programs into conditional rewriting systems. In L. Naish, editor, Proc. ICLP, pages 168–182, 1997. doi:10.7551/mitpress/4299.003.0018.

[bib.bib45] [45] H. Zantema. Termination of term rewriting by semantic labelling. FI, 24(1/2):89–105, 1995. doi:10.3233/FI-1995-24124.