Radboud University, Nijmegen, The
Netherlandsl.guo@cs.ru.nlhttps://orcid.org/0000-0002-3064-2691 Radboud
University, Nijmegen, The
Netherlandsk.hagens@cs.ru.nlhttps://orcid.org/0009-0005-2382-0559 Radboud
University, Nijmegen, The
Netherlandsc.kop@cs.ru.nlhttps://orcid.org/0000-0002-6337-2544 Radboud
University, Nijmegen, The
Netherlandsd.vale@cs.ru.nlhttps://orcid.org/0000-0003-1350-3478 Liye Guo,
Kasper Hagens, Cynthia Kop and Deivid Vale [500]Theory of computation
Equational logic and rewriting The authors are supported by NWO
VI.Vidi.193.075, project “CHORPE”. John Q. Open and Joan R. Access 2 42nd
Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT 2016 December
24–27, 2016 Little Whinging, United Kingdom 42 23

# Higher-Order Constrained Dependency Pairs for (Universal) Computability

Liye Guo  Kasper Hagens  Cynthia Kop  Deivid Vale

###### Abstract

Dependency pairs constitute a series of very effective techniques for the
termination analysis of term rewriting systems. In this paper, we adapt the
static dependency pair framework to logically constrained simply-typed term
rewriting systems (LCSTRSs), a higher-order formalism with logical constraints
built in. We also propose the concept of universal computability, which
enables a form of open-world termination analysis through the use of static
dependency pairs.

###### keywords:

Higher-order term rewriting, constrained rewriting, dependency pairs

##  1 Introduction

Logically constrained simply-typed term rewriting systems (LCSTRSs) [10] are a
formalism of higher-order term rewriting with logical constraints (built on
its first-order counterpart [17]). Proposed for program analysis, LCSTRSs
offer a flexible representation of programs owing to—in contrast with
traditional TRSs—their support for primitive data types such as (arbitrary-
precision or fixed-width) integers and floating-point numbers. Without
compromising chance to directly reason about these widely used data types,
LCSTRSs bridge the gap between the abundant techniques based on term rewriting
and automatic program analysis.

We consider _termination_ analysis in this paper. The termination of LCSTRSs
was first discussed in [10] through a variant of the higher-order recursive
path ordering (HORPO) [12]. This paper furthers that discussion by introducing
dependency pairs [1] to LCSTRSs. As a broad framework for termination, this
method was initially proposed for unconstrained first-order term rewriting,
and was later generalized in a variety of higher-order settings (see, e.g.,
[29, 20, 28, 2]). Modern termination analyzers rely heavily on dependency
pairs.

In higher-order termination analysis, dependency pairs take two forms: the
dynamic [29, 20] and the static [28, 2, 21, 6]. This paper concentrates on
_static_ dependency pairs, and is based on the definitions in [6, 21]. First-
order dependency pairs with logical constraints have been informally defined
by the third author [13], from which we also take inspiration.

For program analysis, the traditional notion of termination can be
inefficient, and arguably insufficient. It assumes that the whole program is
known and analyzed, i.e., _closed-world_ analysis. This way even small
programs that happen to import a large standard library need sophisticated
analysis; local changes in a multipart, previously verified program also
require the entire analysis to be redone. As O’Hearn argues in [23] (in a
different context though), studying _open-world_ analysis opens up many
applications. In particular, it is practically desirable to analyze the
termination of standard libraries—or modules of a larger program—without prior
knowledge of how the functions they define may be used.

It is tricky to characterize such a property, especially in the presence of
higher-order arguments. For example, $\mathsf{map}$ and $\mathsf{fold}$ are
usually considered “terminating”, even though passing a non-terminating
function to them can surely result in non-termination. Hence, we need to
narrow our focus to certain “reasonable” calls. On the other hand, the
function ${\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}$ would
generally be considered “non-terminating”, because if we define ${\mathsf{w}}\
{x}\rightarrow{{\mathsf{app}}\ {x}}\ {x}$, an infinite rewrite sequence starts
from ${{\mathsf{app}}\ {({\mathsf{lam}}\ {\mathsf{w}})}}\ {({\mathsf{lam}}\
{\mathsf{w}})}$—this encodes the famous $\Omega$ in the untyped
$\lambda$-calculus. The property we are looking for must distinguish
$\mathsf{map}$ and $\mathsf{fold}$ from $\mathsf{app}$.

To capture this property, we propose a new concept, called _universal
computability_. In light of information hiding, this concept can be further
generalized to _public computability_. We will see that static dependency
pairs are a natural vehicle for analyzing these properties.

Various modular aspects of term rewriting have been studied by the community.
Our scenario roughly corresponds to hierarchical combinations [25, 26, 27, 5],
where different parts of a program are analyzed separately. We follow this
terminology so that it will be easier to compare our work with the literature.
However, our setup—higher-order constrained rewriting—is separate from the
first-order and unconstrained setting in which hierarchical combinations were
initially proposed. Furthermore, our approach has a different focus—namely,
the use of static dependency pairs.

#### Contributions.

We recall the formalism of LCSTRSs and the predicate of computability in
Section 2. Then the contributions of this paper follow:

  * •

We propose in Section 3 the first definition of _dependency pairs_ for higher-
order logically constrained TRSs. This is also the first DP approach for
constrained rewriting as the prior work on first-order constrained dependency
pairs [13] has never been formally published.

  * •

We define in Section 4 the _constrained DP framework_ for termination analysis
with five classes of _DP processors_ , which can be used to simplify
termination problems.

  * •

We extend the notion of a _hierarchical combination_ [25, 26, 27, 5] to
LCSTRSs and define _universal_ and _public computability_ in Section 5. We
also fine-tune the DP framework to support these properties, and provide extra
DP processors for public computability. This allows the DP framework to be
used for open-world analysis.

  * •

We have implemented the DP framework for both termination and public
computability in our open-source analyzer Cora. We describe the experimental
evaluation in Section 6.

##  2 Preliminaries

In this section, we collect the preliminary definitions and results we need
from the literature. First, we recall the definition of an LCSTRS [10]. In
this paper, we put a restriction on rewrite rules: $\ell$ is always a pattern
in ${\ell}\rightarrow{r}\ [\varphi]$. Next, we recall the definition of
computability (with accessibility) from [6]. This version is particularly
tailored for static dependency pairs.

###  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 ${{t_{0}}\ {t_{1}}}\ {t_{2}}$ stands for
$({({t_{0}}\ {t_{1}})}\ {t_{2}})$, for example.

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}(f)=\emptyset$ for $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 that
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 that there is a distinguished
subset ${\mathcal{F}}_{\vartheta}$ of $\mathcal{F}$, called the set of _theory
symbols_ , and that the type of every theory symbol is in
${\mathcal{T}}_{\vartheta}$, which means that the type of any argument passed
to a theory symbol is a theory sort. Theory symbols whose type is a theory
sort are called _values_. 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 2.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 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$.

#### Substitutions, Contexts and Subterms.

Type-preserving mappings from $\mathcal{V}$ to
$T({\mathcal{F}},{\mathcal{V}})$ are called _substitutions_. 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: $f\sigma=f$ for
$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)}$. Let
$[{x_{1}}\coloneq{t_{1}},\ldots,{x_{n}}\coloneq{t_{n}}]$ denote the
substitution $\sigma$ such that $\sigma(x_{i})=t_{i}$ for all $i$, and
$\sigma(y)=y$ for all
$y\in\mathcal{V}\setminus\\{\,{x}_{1},\ldots,{x}_{n}\,\\}$.

A context is a term containing a hole. Let $\square$ be a special terminal
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$. 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, the type of each variable in
$\operatorname{Var}(r)\setminus\operatorname{Var}(\ell)$ is a theory sort and
$\ell$ is a pattern that takes the form ${f}\ {{t}_{1}\cdots{t}_{n}}$ for some
function symbol $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 ${f}\ {{t}_{1}\cdots{t}_{n}}$ for some function
symbol $f$ or a variable. A substitution $\sigma$ is said to _respect_
${\ell}\rightarrow{r}\ [\varphi]$ if $\sigma(x)$ is a value for all
$x\in\operatorname{Var}(\varphi)\cup(\operatorname{Var}(r)\setminus\operatorname{Var}(\ell))$
and $[\\![\varphi\sigma]\\!]=1$.

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 either (1) $t={C}[\ell\sigma]$ and $t^{\prime}={C}[r\sigma]$
for some rewrite rule ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ and some
substitution $\sigma$ which respects ${\ell}\rightarrow{r}\ [\varphi]$, or (2)
$t={C}[{f}\ {{v}_{1}\cdots{v}_{n}}]$ and $t^{\prime}={C}[v^{\prime}]$ for some
theory symbol $f$ and some values ${v}_{1},\ldots,{v}_{n},v^{\prime}$ with
$n>0$ and $[\\![{f}\ {{v}_{1}\cdots{v}_{n}}]\\!]=[\\![v^{\prime}]\\!]$. When
no ambiguity arises, we may write $\rightarrow$ for
$\rightarrow_{\mathcal{R}}$.

If $t\rightarrow_{\mathcal{R}}t^{\prime}$ due to the second condition above,
we also write $t\rightarrow_{\kappa}t^{\prime}$ and call it a _calculation
step_. Theory symbols that are not a 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, ${f}\ {(7*(3*2))}\,{\downarrow}_{\kappa}={f}\
{42}$ if $f$ is not a calculation symbol or $f:\mathsf{int}\rightarrow
A\rightarrow B$.

A rewrite rule ${\ell}\rightarrow{r}\ [\varphi]$ is said to _define_ a
function symbol $f$ if $\ell={f}\ {{t}_{1}\cdots{t}_{n}}$. Given an LCSTRS
$\mathcal{R}$, $f$ is called a _defined symbol_ if some rewrite rule in
$\mathcal{R}$ defines $f$. Let $\mathcal{D}$ denote the set of defined
symbols. Values and function symbols in
$\mathcal{F}\setminus({\mathcal{F}}_{\vartheta}\cup\mathcal{D})$ are called
_constructors_.

######  Example 2.2.

Below is the factorial function in continuation-passing style as an LCSTRS:

$\displaystyle{{\fact}\ {n}}\ {k}$ $\displaystyle\rightarrow{k}\ {1}$
$\displaystyle[n\leq 0]$ $\displaystyle{{{\mathsf{comp}}\ {g}}\ {f}}\ {x}$
$\displaystyle\rightarrow{g}\ {({f}\ {x})}$ $\displaystyle{{\fact}\ {n}}\ {k}$
$\displaystyle\rightarrow{{\fact}\ {(n-1)}}\ {({{\mathsf{comp}}\ {k}}\
{({(*)}\ {n})})}$ $\displaystyle[n>0]$ $\displaystyle{\mathsf{id}}\ {x}$
$\displaystyle\rightarrow x$

We use infix notation for some binary operators, and omit the logical
constraint of a rewrite rule when it is $\mathfrak{t}$. An example rewrite
sequence is ${{\fact}\ {1}}\ {\mathsf{id}}\rightarrow{{\fact}\ {(1-1)}}\
{({{\mathsf{comp}}\ {\mathsf{id}}}\ {({(*)}\
{1})})}\rightarrow_{\kappa}{{\fact}\ {0}}\ {({{\mathsf{comp}}\ {\mathsf{id}}}\
{({(*)}\ {1})})}\rightarrow{{{\mathsf{comp}}\ {\mathsf{id}}}\ {({(*)}\ {1})}}\
{1}\rightarrow{\mathsf{id}}\ {({{(*)}\ {1}}\
{1})}\rightarrow_{\kappa}{\mathsf{id}}\ {1}\rightarrow 1$.

###  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}$: given 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 and only if $A\succsim C$ and
$\forall{i}.\,A\succ_{-}B_{i}$, and $A\succ_{-}B$ if and only if $A\succ C$
and $\forall{i}.\,A\succsim_{+}B_{i}$.

Given a function symbol
$f:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B$ where $B$ is a
sort, the set $\operatorname{Acc}(f)$ of the _accessible argument positions_
of $f$ is defined as $\\{\,1\leq i\leq n\,|\,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={f}\
{{s}_{1}\cdots{s}_{m}}$ for some $f\in\mathcal{F}$ and there exists
$k\in\operatorname{Acc}(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 ${{f}\
{{s}_{1}\cdots{s}_{m}}}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ and
$x\in\operatorname{Var}({f}\
{{s}_{1}\cdots{s}_{m}})\cap\operatorname{Var}(r)\setminus\operatorname{Var}(\varphi)$,
there exists $k$ such that $s_{k}\trianglerighteq_{\mathrm{acc}}x$.

######  Example 2.3.

An LCSTRS $\mathcal{R}$ is AFP (with $\succsim$ equating all the sorts) if for
all ${{f}\ {{s}_{1}\cdots{s}_{m}}}\rightarrow{r}\ [\varphi]\in\mathcal{R}$ and
$i\in\\{\,1,\ldots,m\,\\}$, the type of each proper subterm of $s_{i}$ is a
sort. Rewrite rules for common higher-order functions, e.g., $\mathsf{map}$
and $\mathsf{fold}$, usually fit this criterion.

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}$.

The system $\\{\,{\mathsf{app}}\ {({\mathsf{lam}}\ {f})}\rightarrow f\,\\}$ in
Section 1 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 the rewrite relation $\rightarrow_{\mathcal{R}}$ of an LCSTRS
$\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:

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

Given terms $s$ and $t$ such that $s\rightarrow_{\mathcal{R}}t$, if $s$ is in
$I_{A}$, so is $t$.

Given a neutral term $s$, if $t$ is in $I_{A}$ for all $t$ such that
$s\rightarrow_{\mathcal{R}}t$, so is $s$. Given an RC-set $I$ for
$\rightarrow_{\mathcal{R}}$, 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}$, whose existence is
guaranteed by Theorem 2.4.

######  Theorem 2.4 (see [6]).

Given a sort ordering and an RC-set $I$ for $\rightarrow_{\mathcal{R}}$, 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={f}\
{{s}_{1}\cdots{s}_{m}}$ for some function symbol $f$, $t={s_{k}}\
{{t}_{1}\cdots{t}_{n}}$ for some $k\in\operatorname{Acc}(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_{\mathcal{R}}$ such that $t\in\mathbb{C}_{A}$ if
and only if $t:A$ is terminating with respect to
${\rightarrow_{\mathcal{R}}}\cup{\Rrightarrow_{\mathbb{C}}}$, and for all
$t^{\prime}$ such that $t\rightarrow_{\mathcal{R}}^{*}t^{\prime}$, if
$t^{\prime}={f}\ {{t}_{1}\cdots{t}_{n}}$ for some function symbol $f$, $t_{i}$
is $\mathbb{C}$-computable for all $i\in\operatorname{Acc}(f)$.

Thus, given a $\mathbb{C}$-computable term ${f}\ {{t}_{1}\cdots{t}_{n}}$, all
its reducts and the accessible arguments—$t_{i}$ for
$i\in\operatorname{Acc}(f)$—are also $\mathbb{C}$-computable. We consider
$\mathbb{C}$-computability throughout this paper.

##  3 Static Dependency Pairs for LCSTRSs

Originally proposed for unconstrained first-order term rewriting, the
dependency pair approach [1]—a methodology that analyzes the recursive
structure of function calls—is at the heart of most modern automatic
termination analyzers for various styles of term rewriting. There follow
multiple higher-order generalizations, among which we adopt here the _static_
branch [21, 6]. As we shall see in Section 5, this approach extends well to
open-world analysis.

In this section, we adapt static dependency pairs to LCSTRSs. We start with a
notation:

######  Definition 3.1.

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

In the presence of logical constraints, a dependency pair should be more than
a pair. Two extra components—a logical constraint and a set of variables—keep
track of what substitutions are expected by the dependency pair.

######  Definition 3.2.

A _static dependency pair_ (SDP) is a quadruple
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid L]$ where
${s}^{\sharp}$ and ${t}^{\sharp}$ are terms of type $\mathsf{dp}$, $\varphi$
is a logical constraint and $L\supseteq\operatorname{Var}(\varphi)$ is a set
of variables whose types are theory sorts. Given 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{{{{g}^{\sharp}}\ {{t}_{1}\cdots{t}_{q}}}\
{{y}_{q+1}\cdots{y}_{n}}}\
[\varphi\mid\operatorname{Var}(\varphi)\cup(\operatorname{Var}(r)\setminus\operatorname{Var}(\ell))]$
such that

${\ell}^{\sharp}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow\mathsf{dp}$
while $x_{i}:A_{i}$ is a fresh variable for all $i$,

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

${g}^{\sharp}:{B}_{1}\rightarrow\cdots\rightarrow{B}_{n}\rightarrow\mathsf{dp}$
while $y_{i}:B_{i}$ is a fresh variable for all $i>q$. Let
$\operatorname{SDP}(\mathcal{R})$ be $\bigcup_{{\ell}\rightarrow{r}\
[\varphi]\in\mathcal{R}}\operatorname{SDP}({\ell}\rightarrow{r}\ [\varphi])$.
A substitution $\sigma$ is said to _respect_ an SDP
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid L]$ if $\sigma(x)$ is a
ground theory term for all $x\in L$ and $[\\![\varphi\sigma]\\!]=1$.

The component $L$ is new compared to [13]. We shall see its usefulness in
Section 4.4, as it gives us more freedom to manipulate dependency pairs. We
introduce two shorthand notations for SDPs:
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi]$ for
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\
[\varphi\mid\operatorname{Var}(\varphi)]$, and
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}$ for
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\mathfrak{t}\mid\emptyset]$.

######  Example 3.3.

Consider the system $\mathcal{R}$ consisting of the following rewrite rules,
in which $\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}$.

$\displaystyle\mathsf{gcdlist}\rightarrow{{\mathsf{fold}}\ {\mathsf{gcd}}}\
{0}\qquad{{{\mathsf{fold}}\ {f}}\ {y}}\ {\mathsf{nil}}\rightarrow
y\qquad{{{\mathsf{fold}}\ {f}}\ {y}}\ {({{\mathsf{cons}}\ {x}}\
{l})}\rightarrow{{f}\ {x}}\ {({{{\mathsf{fold}}\ {f}}\ {y}}\ {l})}$
$\displaystyle\begin{aligned} {{\mathsf{gcd}}\ {m}}\
{n}&\rightarrow{{\mathsf{gcd}}\ {(-m)}}\ {n}&&[m<0]&{{\mathsf{gcd}}\ {m}}\
{n}&\rightarrow{{\mathsf{gcd}}\ {m}}\ {(-n)}&&[n<0]\\\ {{\mathsf{gcd}}\ {m}}\
{0}&\rightarrow m&&[m\geq 0]&{{\mathsf{gcd}}\ {m}}\
{n}&\rightarrow{{\mathsf{gcd}}\ {n}}\ {(m\bmod n)}&&[m\geq 0\wedge
n>0]\end{aligned}$

The set $\operatorname{SDP}(\mathcal{R})$ consists of (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{fold}}^{\sharp}}\ {f}}\ {y}}\
{({{\mathsf{cons}}\ {x}}\ {l})}}\Rightarrow{{{{{\mathsf{fold}}^{\sharp}}\
{f}}\ {y}}\ {l}}$, (4) ${{{{\mathsf{gcd}}^{\sharp}}\ {m}}\
{n}}\Rightarrow{{{{\mathsf{gcd}}^{\sharp}}\ {(-m)}}\ {n}}\ [m<0]$, (5)
${{{{\mathsf{gcd}}^{\sharp}}\ {m}}\
{n}}\Rightarrow{{{{\mathsf{gcd}}^{\sharp}}\ {m}}\ {(-n)}}\ [n<0]$, and (6)
${{{{\mathsf{gcd}}^{\sharp}}\ {m}}\
{n}}\Rightarrow{{{{\mathsf{gcd}}^{\sharp}}\ {n}}\ {(m\bmod n)}}\ [m\geq
0\wedge n>0]$. Note that in (3.3), $m^{\prime}$ and $n^{\prime}$ occur on the
right-hand side of $\Rightarrow$ but not on the left while they are _not_
required to be instantiated to ground theory terms ($L=\emptyset$). This is
normal for SDPs [6, 21].

Termination analysis via SDPs is based on the notion of a chain:

######  Definition 3.4.

Given a set $\mathcal{P}$ of SDPs and a set $\mathcal{R}$ of rewrite rules, a
_$(\mathcal{P},\mathcal{R})$ -chain_ is a (finite or infinite) sequence
$({{s_{0}}^{\sharp}}\Rightarrow{{t_{0}}^{\sharp}}\ [\varphi_{0}\mid
L_{0}],\sigma_{0}),({{s_{1}}^{\sharp}}\Rightarrow{{t_{1}}^{\sharp}}\
[\varphi_{1}\mid L_{1}],\sigma_{1}),\ldots$ such that for all $i$,
${{s_{i}}^{\sharp}}\Rightarrow{{t_{i}}^{\sharp}}\ [\varphi_{i}\mid
L_{i}]\in\mathcal{P}$, $\sigma_{i}$ is a substitution which respects
${{s_{i}}^{\sharp}}\Rightarrow{{t_{i}}^{\sharp}}\ [\varphi_{i}\mid L_{i}]$,
and
${t_{i-1}}^{\sharp}\sigma_{i-1}\rightarrow_{\mathcal{R}}^{*}{s_{i}}^{\sharp}\sigma_{i}$
if $i>0$. The above $(\mathcal{P},\mathcal{R})$-chain is called _computable_
if $u\sigma_{i}$ is $\mathbb{C}$-computable for all $i$ and $u$ such that
$t_{i}\vartriangleright u$.

######  Example 3.5.

Following Example 3.3,
$(\text{\ref{itm:gcdlistGcdlGcdf}},[{l}\coloneq{\mathsf{nil}},{m}\coloneq{42},{n}\coloneq{24}]),(\text{\ref{itm:gcdlistGcdfGcdfMod}},[{m}\coloneq{42},{n}\coloneq{24}]),(\text{\ref{itm:gcdlistGcdfGcdfMod}},[{m}\coloneq{24},{n}\coloneq{18}]),(\text{\ref{itm:gcdlistGcdfGcdfMod}},[{m}\coloneq{18},{n}\coloneq{6}])$
is a computable $(\operatorname{SDP}(\mathcal{R}),\mathcal{R})$-chain.

The key to establishing termination is the following result (see Section A.1):

######  Theorem 3.6.

An AFP system $\mathcal{R}$ is terminating if there exists no infinite
computable $(\operatorname{SDP}(\mathcal{R}),\mathcal{R})$-chain.

##  4 The Constrained DP Framework

In this section, we present several techniques based on SDPs, each as a class
of _DP processors_ ; formally, we call this collection of DP processors the
_constrained (static) DP framework_. In general, a DP framework [8, 6]
constitutes a broad method for termination and non-termination. The
presentation here is not complete—for example, we do not consider non-
termination—and a complete one is beyond the scope of this paper. We rather
focus on the most essential DP processors and those newly designed to handle
logical constraints.

For presentation, we fix an LCSTRS $\mathcal{R}$.

######  Definition 4.1.

A _DP problem_ is a set $\mathcal{P}$ of SDPs. A DP problem $\mathcal{P}$ is
called _finite_ if there exists no infinite computable
$(\mathcal{P},\mathcal{R})$-chain. 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 a DP problem $\mathcal{P}$ is finite whenever
$\rho(\mathcal{P})$ consists only of finite DP problems.

Following Theorem 3.6, in order to establish the termination of an AFP system
$\mathcal{R}$, it suffices to show that $\operatorname{SDP}(\mathcal{R})$ is a
finite DP problem. Given a collection of sound DP processors, we have the
following procedure: (1) $Q\coloneq\\{\,\operatorname{SDP}(\mathcal{R})\,\\}$;
(2) while $Q$ contains a DP problem $\mathcal{P}$ to which some sound DP
processor $\rho$ is applicable,
$Q\coloneq(Q\setminus\\{\,\mathcal{P}\,\\})\cup\rho(\mathcal{P})$. If this
procedure ends with $Q=\emptyset$, we can conclude that $\mathcal{R}$ is
terminating.

###  4.1 The DP Graph and Its Approximations

The interconnection of SDPs via chains gives rise to a graph, namely, the DP
graph [1], which models the reachability between dependency pairs. Since this
graph is not computable in general, we follow the usual convention and
consider its (over-)approximations:

######  Definition 4.2.

Given a set $\mathcal{P}$ of SDPs, a _graph approximation_
$(G_{\theta},\theta)$ for $\mathcal{P}$ consists of a finite directed graph
$G_{\theta}$ and a mapping $\theta$ which assigns to each SDP in $\mathcal{P}$
a vertex of $G_{\theta}$ so that there is an edge from $\theta(p_{0})$ to
$\theta(p_{1})$ whenever $(p_{0},\sigma_{0}),(p_{1},\sigma_{1})$ is a
$(\mathcal{P},\mathcal{R})$-chain for some substitutions $\sigma_{0}$ and
$\sigma_{1}$.

Here $(G_{\theta},\theta)$ over-approximates the DP graph because there can be
an edge from $\theta(p_{0})$ to $\theta(p_{1})$ even if $p_{0}$ and $p_{1}$
are not connected by any $(\mathcal{P},\mathcal{R})$-chain. In practice, we
typically deal with only a finite set $\mathcal{P}$ of SDPs, in which case we
usually take a bijection for $\theta$.

This graph structure is useful because we can leverage it to decompose the DP
problem.

######  Definition 4.3.

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

######  Example 4.4.

Following Example 3.3, a (tight) graph approximation for
$\operatorname{SDP}(\mathcal{R})$ is given on the right. If a graph processor
produces this graph as the graph approximation, it will return the set of DP
problems
$\\{\,\\{\,\text{\ref{itm:gcdlistFoldFold}}\,\\},\\{\,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{\ref{itm:gcdlistGcdfGcdfN}}\,\\},\\{\,\text{\ref{itm:gcdlistGcdfGcdfMod}}\,\\}\,\\}$.

3.33.33.33.33.33.3

#### Implementation.

To compute a graph approximation, we adapt the common Cap approach [9, 31] and
take theories into account. Considering theories allows us, for example, _not_
to have an edge from (3.3) to (3.3) in the above graph.

We assume given a finite set of SDPs and let $\theta$ be a bijection. Whether
there is an edge from $\theta({{s_{0}}^{\sharp}}\Rightarrow{{t_{0}}^{\sharp}}\
[\varphi_{0}\mid L_{0}])$ to
$\theta({{s_{1}}^{\sharp}}\Rightarrow{{t_{1}}^{\sharp}}\ [\varphi_{1}\mid
L_{1}])$—we rename variables if necessary to avoid name collisions between the
two SDPs—is determined by the satisfiability (which we check by an SMT solver)
of
$\varphi_{0}\wedge\varphi_{1}\wedge\zeta({t_{0}}^{\sharp},{s_{1}}^{\sharp})$
where $\zeta(u,v)$ is defined as follows:

  * •

If $u={f}\ {{u}_{1}\cdots{u}_{n}}$ where $f\in{\mathcal{F}}^{\sharp}$ and no
rewrite rule in $\mathcal{R}$ takes the form ${{f}\
{{\ell}_{1}\cdots{\ell}_{k}}}\rightarrow{r}\ [\varphi]$ for $k\leq n$, we
define $\zeta(u,v)$ in two cases: (1)
$\zeta(u,v)=\zeta(u_{1},v_{1})\wedge\cdots\wedge\zeta(u_{n},v_{n})$ if $v={f}\
{{v}_{1}\cdots{v}_{n}}$. (2) $\zeta(u,v)=\mathfrak{f}$ if $v={g}\
{{v}_{1}\cdots{v}_{m}}$ for some function symbol $g$ other than $f$ and either
$f$ is not a theory symbol or $g$ is not a value.

  * •

Suppose $\zeta(u,v)$ is not defined above; $\zeta(u,v)=(u\equiv v)$ if $u\in
T({{\mathcal{F}}_{\vartheta}},{L_{0}})$ and $v$ is a theory term in which the
type of each variable is a theory sort, and $\zeta(u,v)=\mathfrak{t}$
otherwise.

For example, since $(m_{0}\geq 0\wedge n_{0}>0)\wedge
m_{1}<0\wedge(n_{0}\equiv m_{1}\wedge m_{0}\bmod n_{0}\equiv n_{1})$ is
unsatisfiable, there is no edge from (3.3) to (3.3).

Then strongly connected components can be computed by Tarjan’s algorithm [30].

###  4.2 The Subterm Criterion

The subterm criterion [11, 21] handles structural recursion and allows us to
remove decreasing SDPs without considering rewrite rules in $\mathcal{R}$. We
start with defining projections:

######  Definition 4.5.

Let $\operatorname{heads}(\mathcal{P})$ denote the set of function symbols
heading either side of an SDP in $\mathcal{P}$. 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({f}^{\sharp})\leq n$ if
${f}^{\sharp}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow\mathsf{dp}$.
Let $\bar{\nu}({{f}^{\sharp}}\ {{t}_{1}\cdots{t}_{n}})$ denote
$t_{\nu({f}^{\sharp})}$.

A projection chooses an argument position for each relevant function symbol so
that arguments at those positions do not increase in a chain.

######  Definition 4.6.

Given a set $\mathcal{P}$ of SDPs, 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\mid
L]\in\mathcal{P}^{\prime}$ and
$\bar{\nu}({s}^{\sharp})=\bar{\nu}({t}^{\sharp})$ for all
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid
L]\in\mathcal{P}\setminus\mathcal{P}^{\prime}$. A _subterm criterion
processor_ assigns to a DP problem $\mathcal{P}$ the singleton
$\\{\,\mathcal{P}\setminus\mathcal{P}^{\prime}\,\\}$ for some non-empty subset
$\mathcal{P}^{\prime}$ of $\mathcal{P}$ such that there exists a projection
for $\mathcal{P}$ which $\vartriangleright$-orients $\mathcal{P}^{\prime}$.

######  Example 4.7.

Following Example 4.4, a subterm criterion processor is applicable to
$\\{\,\text{\ref{itm:gcdlistFoldFold}}\,\\}$. Let
$\nu({\mathsf{fold}}^{\sharp})$ be $3$ so that
$\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})$. The processor
returns $\\{\,\emptyset\,\\}$, and the empty DP problem can (trivially) be
removed by a graph processor.

#### Implementation.

The search for a suitable projection can be done through SMT and is standard:
we introduce an integer variable $N_{{f}^{\sharp}}$ that represents
$\nu({f}^{\sharp})$ for each
${f}^{\sharp}\in\operatorname{heads}(\mathcal{P})$, and a boolean variable
$\mathsf{strict}_{p}$ for each $p\in\mathcal{P}$; then we encode the
requirement per SDP.

###  4.3 Integer Mappings

The subterm criterion deals with recursion over the structure of terms, but
not recursion over, say, integers, which requires us to utilize the
information in logical constraints. In this subsection, we assume that
$\mathsf{int}\in{\mathcal{S}}_{\vartheta}$ and
${\mathcal{F}}_{\vartheta}\supseteq\\{\,{\geq},{>},{\wedge}\,\\}$, where
${\geq}:\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{bool}$,
${>}:\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{bool}$ and
${\wedge}:\mathsf{bool}\rightarrow\mathsf{bool}\rightarrow\mathsf{bool}$ are
interpreted in the standard way.

######  Definition 4.8.

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

With integer mappings, we can handle decreasing integer values.

######  Definition 4.9.

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\mid
L]\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\mid
L]\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
values. An _integer mapping processor_ assigns to a DP problem $\mathcal{P}$
the singleton $\\{\,\mathcal{P}\setminus\mathcal{P}^{\prime}\,\\}$ for some
non-empty subset $\mathcal{P}^{\prime}$ of $\mathcal{P}$ such that there
exists an integer mapping for $\mathcal{P}$ which $>$-orients
$\mathcal{P}^{\prime}$.

######  Example 4.10.

Following Example 4.4, an integer mapping processor is applicable to
$\\{\,\text{\ref{itm:gcdlistGcdfGcdfMod}}\,\\}$. Let
$\mathcal{J}({\mathsf{gcd}}^{\sharp})$ be $x_{{\mathsf{gcd}}^{\sharp},2}$ so
that $\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$. The processor returns
$\\{\,\emptyset\,\\}$, and the empty DP problem can (trivially) be removed by
a graph processor.

#### Implementation.

We generate a number of “interpretation candidates” and use an SMT encoding to
select for each ${f}^{\sharp}\in\operatorname{heads}(\mathcal{P})$ one
candidate that satisfies the requirements. Candidates include forms such as
$\mathcal{J}({f}^{\sharp})=x_{{f}^{\sharp},i}$ and those that are generated
from the SDPs’ logical constraints—e.g., given ${{{{f}^{\sharp}}\ {x}}\
{y}}\Rightarrow{{{{g}^{\sharp}}\ {x}}\ {(y+1)}}\ [y<x]$, we generate
$\mathcal{J}({f}^{\sharp})=x_{{f}^{\sharp},1}-x_{{f}^{\sharp},2}-1$ because
$y<x$ implies $x-y-1\geq 0$.

###  4.4 Theory Arguments

Integer mapping processors have a clear limitation: what if some key variables
do not occur in the set $L$? This is observed in the remaining DP problem
$\\{\,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{\ref{itm:gcdlistGcdfGcdfN}}\,\\}$
from Example 3.3. It is clearly finite but no integer mapping processor is
applicable since $\iota({\mathsf{gcd}}^{\sharp})=\emptyset$.

This restriction exists for a reason. Variables that are not guaranteed to be
instantiated to theory terms may be instantiated to _non-deterministic_
terms—e.g., $\\{\,{{{{{f}^{\sharp}}\ {x}}\ {y}}\
{z}}\Rightarrow{{{{{f}^{\sharp}}\ {x}}\ {(x+1)}}\ {(x-1)}}\ [y<z]\,\\}$ is not
a finite DP problem if $\mathcal{R}\supseteq\\{\,{{\mathsf{c}}\ {x}}\
{y}\rightarrow x,{{\mathsf{c}}\ {x}}\ {y}\rightarrow y\,\\}$.

The problem of
$\\{\,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{\ref{itm:gcdlistGcdfGcdfN}}\,\\}$
arises because each SDP focuses on only one argument: for example, the logical
constraint (with the component $L$) of (3.3) only concerns $n$ so in principle
we cannot assume anything about $m$. Yet, if (3.3) follows (3.3) in a chain,
we _can_ derive that $m$ must be instantiated to a ground theory term (we call
such an argument a _theory argument_). We explore a way of propagating this
information.

######  Definition 4.11.

A _theory argument (position) mapping_ $\tau$ for a set $\mathcal{P}$ of SDPs
is a mapping from $\operatorname{heads}(\mathcal{P})$ (see Definition 4.5) to
subsets of $\mathbb{Z}$ such that $\tau({f}^{\sharp})\subseteq\\{\,1\leq i\leq
m\,|\,A_{i}\in{\mathcal{S}}_{\vartheta}\,\\}$ if
${f}^{\sharp}:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow\mathsf{dp}$,
$s_{i}$ is a theory term and the type of each variable in
$\operatorname{Var}(s_{i})$ is a theory sort for all ${{{f}^{\sharp}}\
{{s}_{1}\cdots{s}_{m}}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid
L]\in\mathcal{P}$ and $i\in\tau({f}^{\sharp})$, and $t_{j}$ is a theory term
and $\operatorname{Var}(t_{j})\subseteq
L\cup\bigcup_{i\in\tau({f}^{\sharp})}\operatorname{Var}(s_{i})$ for all
${{{f}^{\sharp}}\ {{s}_{1}\cdots{s}_{m}}}\Rightarrow{{{g}^{\sharp}}\
{{t}_{1}\cdots{t}_{n}}}\ [\varphi\mid L]\in\mathcal{P}$ and
$j\in\tau({g}^{\sharp})$. Let $\bar{\tau}({{{f}^{\sharp}}\
{{s}_{1}\cdots{s}_{m}}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid L])$ denote
${{{f}^{\sharp}}\ {{s}_{1}\cdots{s}_{m}}}\Rightarrow{{t}^{\sharp}}\
[\varphi\mid L\cup\bigcup_{i\in\tau({f}^{\sharp})}\operatorname{Var}(s_{i})]$.

By a theory argument mapping, we choose a subset of the given set of SDPs from
which the theory argument information is propagated.

######  Definition 4.12.

Given a set $\mathcal{P}$ of SDPs, a theory argument mapping $\tau$ is said to
_fix_ a subset $\mathcal{P}^{\prime}$ of $\mathcal{P}$ if
$\bigcup_{i\in\tau({f}^{\sharp})}\operatorname{Var}(t_{i})\subseteq L$ for all
${{s}^{\sharp}}\Rightarrow{{{f}^{\sharp}}\ {{t}_{1}\cdots{t}_{n}}}\
[\varphi\mid L]\in\mathcal{P}^{\prime}$. A _theory argument processor_ assigns
to a DP problem $\mathcal{P}$ the pair
$\\{\,\\{\,\bar{\tau}(p)\,|\,p\in\mathcal{P}\,\\},\mathcal{P}\setminus\mathcal{P}^{\prime}\,\\}$
for some non-empty subset $\mathcal{P}^{\prime}$ of $\mathcal{P}$ such that
there exists a theory argument mapping for $\mathcal{P}$ which fixes
$\mathcal{P}^{\prime}$.

######  Example 4.13.

Following Example 4.4, a theory argument processor is applicable to
$\\{\,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{\ref{itm:gcdlistGcdfGcdfN}}\,\\}$.
Let $\tau({\mathsf{gcd}}^{\sharp})$ be $\\{\,1\,\\}$ so that $\tau$ fixes
$\\{\,\text{\ref{itm:gcdlistGcdfGcdfM}}\,\\}$. The processor returns the pair
$\\{\,\\{\,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{(7)
}{{{{\mathsf{gcd}}^{\sharp}}\ {m}}\
{n}}\Rightarrow{{{{\mathsf{gcd}}^{\sharp}}\ {m}}\ {(-n)}}\
[n<0\mid\\{\,m,n\,\\}]\,\\},\\{\,\text{\ref{itm:gcdlistGcdfGcdfN}}\,\\}\,\\}$.
The integer mapping processor with
$\mathcal{J}({\mathsf{gcd}}^{\sharp})={-x_{{\mathsf{gcd}}^{\sharp},1}}$
removes (3.3) from $\\{\,\text{\ref{itm:gcdlistGcdfGcdfM}},\text{7}\,\\}$.
Then $\\{\,\text{7}\,\\}$ and $\\{\,\text{\ref{itm:gcdlistGcdfGcdfN}}\,\\}$
can be removed by graph processors.

#### Implementation.

To find a valid theory argument mapping, we simply start by setting
$\tau({f}^{\sharp})=\\{\,1,\ldots,m\,\\}$ for all ${f}^{\sharp}$, and choose
one SDP to fix. Then we iteratively remove arguments that do not satisfy the
condition until no such argument is left.

###  4.5 Reduction Pairs

Although it is not needed by the running example, we present a constrained
variant of _reduction pair processors_ , which are at the heart of most
unconstrained termination analyzers.

######  Definition 4.14.

A _constrained relation_ $R$ is a set of quadruples $(s,t,\varphi,L)$ where
$s$ and $t$ are terms which have the same type, $\varphi$ is a logical
constraint and $L\supseteq\operatorname{Var}(\varphi)$ is a set of variables
whose types are theory sorts. We write ${s}\mathrel{R}_{\varphi}^{L}{t}$ if
$(s,t,\varphi,L)\in R$. A binary relation $R^{\prime}$ over terms is said to
_cover_ a constrained relation $R$ if ${s}\mathrel{R}_{\varphi}^{L}{t}$
implies that
$(s\sigma)\,{\downarrow}_{\kappa}\mathrel{R^{\prime}}(t\sigma)\,{\downarrow}_{\kappa}$
for each substitution $\sigma$ such that $\sigma(x)$ is a ground theory term
for all $x\in L$ and $[\\![\varphi\sigma]\\!]=1$.

A _constrained reduction pair_ $(\succeq,\succ)$ is a pair of constrained
relations such that $\succeq$ is covered by some reflexive relation
$\sqsupseteq$ which includes $\rightarrow_{\kappa}$ and is monotonic (i.e.,
$s\sqsupseteq t$ implies ${C}[s]\sqsupseteq{C}[t]$), $\succ$ is covered by
some well-founded relation $\sqsupset$, and
${\sqsupseteq}\mathrel{;}{\sqsupset}\subseteq{\sqsupset^{+}}$.

######  Definition 4.15.

A _reduction pair processor_ assigns to a DP problem $\mathcal{P}$ the
singleton $\\{\,\mathcal{P}\setminus\mathcal{P}^{\prime}\,\\}$ for some non-
empty subset $\mathcal{P}^{\prime}$ of $\mathcal{P}$ such that there exists a
constrained reduction pair $(\succeq,\succ)$ where (1)
${{s}^{\sharp}}\mathrel{\succ}_{\varphi}^{L}{{t}^{\sharp}}$ for all
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid
L]\in\mathcal{P}^{\prime}$, (2)
${{s}^{\sharp}}\mathrel{\succeq}_{\varphi}^{L}{{t}^{\sharp}}$ for all
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid L]\in\mathcal{P}$, and
(3)
${\ell}\mathrel{\succeq}_{\varphi}^{\operatorname{Var}(\varphi)\cup(\operatorname{Var}(r)\setminus\operatorname{Var}(\ell))}{r}$
for all ${\ell}\rightarrow{r}\ [\varphi]\in\mathcal{R}$.

While a variety of reduction pairs have been proposed for unconstrained
rewriting, it is not yet the case in a higher-order and constrained setting:
so far the only one is a limited version of HORPO [10], which is adapted into
a weakly monotonic reduction pair [16] and then implemented in the DP
framework. This is still a prototype definition.

We have included reduction pair processors here because their definition
allows us to start designing constrained reduction pairs. In particular, as
unconstrained reduction pairs can be used as the covering pair
$(\sqsupseteq,\sqsupset)$, it is likely that many of them (such as variants of
HORPO and weakly monotonic algebras) can be adapted.

######  Theorem 4.16 (see Section A.2).

All the DP processors defined in Section 4 are sound.

##  5 Universal Computability

Termination is not a _modular_ property: given terminating systems
$\mathcal{R}_{0}$ and $\mathcal{R}_{1}$, we cannot generally conclude that
$\mathcal{R}_{0}\cup\mathcal{R}_{1}$ is also terminating. As computability is
based on termination, it is not modular either. For example, both
$\\{\,\mathsf{a}\rightarrow\mathsf{b}\,\\}$ and $\\{\,{\mathsf{f}}\
{\mathsf{b}}\rightarrow{\mathsf{f}}\ {\mathsf{a}}\,\\}$ are terminating, and
$\mathsf{f}:\mathsf{o}\rightarrow\mathsf{o}$ is computable in the second
system; yet, combining the two yields ${\mathsf{f}}\
{\mathsf{a}}\rightarrow{\mathsf{f}}\ {\mathsf{b}}\rightarrow{\mathsf{f}}\
{\mathsf{a}}\rightarrow\cdots$, which refutes the termination of the
combination and the computability of $\mathsf{f}$.

On the other hand, functions like $\mathsf{map}$ and $\mathsf{fold}$ are
prevalently used; the lack of a modular principle for the termination analysis
of higher-order systems involving such functions is painful. Moreover, if such
a system is non-terminating, this is seldom attributed to those functions,
which are generally considered “terminating” regardless of how they may be
called.

In this section, we propose _universal computability_ , a concept which
corresponds to the termination of a function in all “reasonable” uses. First,
we rephrase the notion of a hierarchical combination [25, 26, 27, 5] in terms
of LCSTRSs:

######  Definition 5.1.

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. This forms the basis of the
modular programming scenario we are interested in: think of the base system as
a library containing the definitions of, say, $\mathsf{map}$ and
$\mathsf{fold}$. We further define a class of extensions to take information
hiding into account:

######  Definition 5.2.

Given an LCSTRS $\mathcal{R}_{0}$ and a set of function symbols—called _hidden
symbols_ —in $\mathcal{R}_{0}$, an extension $\mathcal{R}_{1}$ of
$\mathcal{R}_{0}$ is called a _public extension_ if hidden symbols do not
occur in any rewrite rule in $\mathcal{R}_{1}$.

Now we present the central definitions of this section:

######  Definition 5.3.

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}$; if a set of hidden symbols in $\mathcal{R}_{0}$ is also
given and the above universal quantification of $\mathcal{R}_{1}$ is
restricted to _public_ extensions, such a term $t$ is called _publicly
computable_.

The base system $\mathcal{R}_{0}$ is called universally computable if all its
terms are; it is called publicly computable if all its _public_ terms—terms
that contain no hidden symbol—are.

With an empty set of hidden symbols, the two notions—universal computability
and public computability—coincide. Below we state common properties in terms
of public computability.

In summary, we consider passing $\mathbb{C}$-computable arguments to a defined
symbol in $\mathcal{R}_{0}$ the “reasonable” way of calling the function. To
establish the universal computability of higher-order functions such as
$\mathsf{map}$ and $\mathsf{fold}$—i.e., to prove that they are
$\mathbb{C}$-computable in _all_ relevant hierarchical combinations—we will
use SDPs, which are about $\mathbb{C}$-computability.

######  Example 5.4.

The system $\\{\,{\mathsf{app}}\ {({\mathsf{lam}}\ {f})}\rightarrow f\,\\}$ in
Section 1 is not universally computable due to the extension
$\\{\,{\mathsf{w}}\ {x}\rightarrow{{\mathsf{app}}\ {x}}\ {x}\,\\}$.

###  5.1 The DP Framework Revisited

To use SDPs for universal—or public—computability, we need a more general
version of Theorem 3.6. We start with defining public chains:

######  Definition 5.5.

An SDP ${{{f}^{\sharp}}\ {{s}_{1}\cdots{s}_{m}}}\Rightarrow{{t}^{\sharp}}\
[\varphi\mid L]$ is called public if $f$ is not a hidden symbol. A
$(\mathcal{P},\mathcal{R})$-chain is called public if its first SDP is public.

Now we state the main result of this section:

######  Theorem 5.6.

An AFP system $\mathcal{R}_{0}$ with sort ordering $\succsim$ is publicly
computable with respect to a set of hidden symbols in $\mathcal{R}_{0}$ if
there exists no infinite computable
$(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$-chain
that is _public_ for each public 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}$.

While this result itself is not surprising and its proof (see Section A.3) is
standard, it is not so obvious how it can be used. The key observation which
enables us to use the DP framework for public computability is that among the
DP processors in Section 4, only reduction pair processors rely on the rewrite
rules of the underlying system $\mathcal{R}$ (depending on how it computes a
graph approximation, a graph processor does not have to know the rewrite
rules). Henceforth, we fix a base system $\mathcal{R}_{0}$, a set of hidden
symbols in $\mathcal{R}_{0}$ and an arbitrary, unknown public extension
$\mathcal{R}_{1}$ of $\mathcal{R}_{0}$. Now $\mathcal{R}$ is the hierarchical
combination $\mathcal{R}_{0}\cup\mathcal{R}_{1}$.

First, we generalize the definition of a DP problem:

######  Definition 5.7.

A _(universal) DP problem_ $(\mathcal{P},\mathtt{p})$ consists of a set
$\mathcal{P}$ of SDPs and a flag
$\mathtt{p}\in\\{\,\mathfrak{an},\mathfrak{pu}\,\\}$ (for _any_ or _public_).
A DP problem $(\mathcal{P},\mathtt{p})$ is called _finite_ if either (1)
$\mathtt{p}=\mathfrak{an}$ and there exists no infinite computable
$(\mathcal{P},\mathcal{R}_{0}\cup\mathcal{R}_{1})$-chain, or (2)
$\mathtt{p}=\mathfrak{pu}$ and there exists no infinite computable
$(\mathcal{P},\mathcal{R}_{0}\cup\mathcal{R}_{1})$-chain which is _public_.

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}),\mathfrak{pu})$ is finite, and the
procedure for termination in Section 4 also works here if we change the
initialization of $Q$ accordingly.

Next, we review the DP processors presented in Section 4. For each $\rho$ of
the original graph, subterm criterion and integer mapping processors, the
processor $\rho^{\prime}$ such that
$\rho^{\prime}(\mathcal{P},\mathtt{p})=\\{\,(\mathcal{P}^{\prime},\mathfrak{an})\,|\,\mathcal{P}^{\prime}\in\rho(\mathcal{P})\,\\}$
is sound for universal DP problems. For theory argument processors, we can do
better when the input flag is $\mathfrak{pu}$ (when it is $\mathfrak{an}$, we
just handle $\mathcal{P}$ in the same way as we do in Section 4 and the output
flags are obviously $\mathfrak{an}$): if the subset $\mathcal{P}^{\prime}$ of
$\mathcal{P}$ fixed by a theory argument mapping $\tau$ contains all the
public SDPs in $\mathcal{P}$, the processor should return the singleton
$\\{\,(\\{\,\bar{\tau}(p)\,|\,p\in\mathcal{P}\,\\},\mathfrak{pu})\,\\}$;
otherwise, the pair
$\\{\,(\\{\,\bar{\tau}(p)\,|\,p\in\mathcal{P}\,\\},\mathfrak{an}),(\mathcal{P}\setminus\mathcal{P}^{\prime},\mathfrak{pu})\,\\}$.
Reduction pair processors require knowledge of the extension $\mathcal{R}_{1}$
so we do not adapt them.

#### New Processors.

Last, we propose two classes of DP processors that are useful for public
computability. Processors of the first class do not actually simplify DP
problems; they rather alter their input to allow other DP processors to be
applied subsequently.

######  Definition 5.8.

Given sets $\mathcal{P}_{1}$ and $\mathcal{P}_{2}$ of SDPs, $\mathcal{P}_{2}$
is said to _cover_ $\mathcal{P}_{1}$ if for each SDP
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi_{1}\mid
L_{1}]\in\mathcal{P}_{1}$ and each substitution $\sigma_{1}$ which respects
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi_{1}\mid L_{1}]$, there
exist an SDP ${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi_{2}\mid
L_{2}]\in\mathcal{P}_{2}$ and a substitution $\sigma_{2}$ such that
$\sigma_{2}$ respects ${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\
[\varphi_{2}\mid L_{2}]$, $s\sigma_{1}=s\sigma_{2}$ and
$t\sigma_{1}=t\sigma_{2}$. A _constraint modification processor_ assigns to a
DP problem $(\mathcal{P},\mathtt{p})$ the singleton
$\\{\,(\mathcal{P}^{\prime},\mathtt{p})\,\\}$ for some $\mathcal{P}^{\prime}$
which covers $\mathcal{P}$.

Now combined with the information of hidden symbols, the DP graph allows us to
remove SDPs that are unreachable from any public SDP.

######  Definition 5.9.

A _reachability processor_ assigns to a DP problem
$(\mathcal{P},\mathfrak{pu})$ the singleton
$\\{\,(\\{\,p\in\mathcal{P}\,|\,\theta(p)\text{ is reachable from
}\theta(p_{0})\text{ for some public SDP }p_{0}\,\\},\mathfrak{pu})\,\\}$,
given a graph approximation $(G_{\theta},\theta)$ for $\mathcal{P}$.

These two classes of DP processors are often used together: a constraint
modification processor can split an SDP into simpler ones, some of which may
be removed by a reachability processor. In our implementation, a constraint
modification processor is particularly used to break an SDP
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [u\neq v\mid L]$ into two SDPs with
logical constraints $u<v$ and $u>v$, respectively (see Example 5.10);
similarly for $u\vee v$.

######  Example 5.10.

Consider an alternative implementation of the factorial function from Example
2.2, which has SDPs (1) ${{{{}^{\sharp}}\ {n}}\
{k}}\Rightarrow{{{{{\mathsf{comp}}^{\sharp}}\ {k}}\ {({(*)}\ {n})}}\
{x^{\prime}}}\ [n\neq 0]$, (2) ${{{{}^{\sharp}}\ {n}}\
{k}}\Rightarrow{{{{}^{\sharp}}\ {(n-1)}}\ {({{\mathsf{comp}}\ {k}}\ {({(*)}\
{n})})}}\ [n\neq 0]$, and (3) ${{{\mathsf{init}}^{\sharp}}\
{k}}\Rightarrow{{{{}^{\sharp}}\ {42}}\ {k}}$. Assume that is a hidden symbol.
Note that
$(\\{\,\text{\ref{itm:constraintFactComp}},\text{\ref{itm:constraintFactFact}},\text{\ref{itm:constraintInitFact}}\,\\},\mathfrak{pu})$
is not finite without this assumption. A constraint modification processor can
replace (5.10) with (4) ${{{{}^{\sharp}}\ {n}}\
{k}}\Rightarrow{{{{}^{\sharp}}\ {(n-1)}}\ {({{\mathsf{comp}}\ {k}}\ {({(*)}\
{n})})}}\ [n<0]$, and (5) ${{{{}^{\sharp}}\ {n}}\
{k}}\Rightarrow{{{{}^{\sharp}}\ {(n-1)}}\ {({{\mathsf{comp}}\ {k}}\ {({(*)}\
{n})})}}\ [n>0]$. A reachability processor can then remove (5.10). The
remaining DP problem
$(\\{\,\text{\ref{itm:constraintFactComp}},\text{\ref{itm:constraintInitFact}},\text{\ref{itm:constraintFactFactGt}}\,\\},\mathfrak{pu})$
can easily be handled by a graph processor and an integer mapping processor.

######  Theorem 5.11 (see Section A.4).

All the DP processors defined in Section 5 are sound.

##  6 Experiments and Future Work

All the results in this paper have been implemented in our open-source tool
Cora, available at

https://github.com/hezzel/cora

The version of this paper is available in [19]. We have evaluated Cora on
three groups of experiments, the results of which are given below.

| Custom | STRS | ITRS
---|---|---|---
Termination | 20/28 | 72/140 | 69/117
Computability | 20/28 | 66/140 | 68/117
Wanda | – | 105/140 | –
AProVE | – | – | 102/117

The first test considers the examples from this paper and several other
LC(S)TRS benchmarks we have collected. The second test considers all
$\lambda$-free problems from the higher-order category of the TPDB [4]. The
third test considers problems from the first-order “integer TRS innermost”
category. The computability test analyzes public computability; since there
are no hidden symbols in the TPDB, the main difference with the termination
check is that the reduction pair processor is disabled. A full evaluation page
is available at

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

Unsurprisingly, Cora is substantially weaker than Wanda [14] on unconstrained
higher-order benchmarks, or AProVE [7] on first-order integer TRSs: this work
aims to be a starting point for _combining_ higher-order term analysis and
theory reasoning, and cannot yet compete with tools that have had years of
development. However, for having only a handful of simple techniques, we
believe that these results show a solid foundation.

#### Future Work.

Moreover, much of the existing techniques used in the analysis of integer TRSs
and higher-order TRS are likely to be adaptable to our setting, leaving many
encouraging avenues for further development. We highlight the most important
ones.

  * •

Usable rules with respect to an argument filtering [9, 15]: to effectively use
reduction pairs, being able to discard some rules is essential (especially for
universal computability, if we can discard the unknown rules). Closely
related, there is a clear benefit to extending more reduction pairs such as
weakly monotonic algebras [33, 24], tuple interpretations [18, 32] and more
sophisticated path orderings [3], all of which have higher-order definitions.

  * •

Transformation techniques, such as narrowing, or chaining DPs together (as
used for instance for integer transition systems, [7, Secion 3.1]). This could
also be a step towards using the constrained DP framework for non-termination.

  * •

Handling innermost or call-by-value reduction strategies. Several functional
programming languages use call-by-value evaluation, and using this restriction
may allow for a more powerful analysis. In the first-order DP framework there
is ample work on the innermost strategy to build on (see, e.g., [8, 9]).

  * •

Theory-specific processors for popular theories other than integers; e.g.,
bitvectors [22].

## References

  * [1] 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.
  * [2] F. Blanqui.  Higher-order dependency pairs.  In A. Geser and H. Søndergaard, editors, Proc. WST, pages 22–26, 2006.  doi:10.48550/arXiv.1804.08855.
  * [3] F. Blanqui, J.-P. Jouannaud, and A. Rubio.  The computability path ordering: the end of a quest.  In M. Kaminski and S. Martini, editors, Proc. CSL, pages 1–14, 2008.  doi:10.1007/978-3-540-87531-4_1.
  * [4] Community.  Termination Problem DataBase.  2023\.  URL: https://github.com/TermCOMP/TPDB.
  * [5] 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.
  * [6] 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.
  * [7] 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.  Journal of Automated Reasoning, 58(1):3–31, 2017.
  * [8] 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.
  * [9] J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke.  Mechanizing and improving dependency pairs.  JAR, 37:155–203, 2006.  doi:10.1007/s10817-006-9057-7.
  * [10] 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.
  * [11] N. Hirokawa and A. Middeldorp.  Dependency pairs revisited.  In V. van Oostrom, editor, Proc. RTA, pages 249–268, 2004.  doi:10.1007/978-3-540-25979-4_18.
  * [12] J.-P. Jouannaud and A. Rubio.  The higher-order recursive path ordering.  In G. Longo, editor, Proc. LICS, pages 402–411, 1999.  doi:10.1109/LICS.1999.782635.
  * [13] C. Kop.  Termination of LCTRSs.  In J. Waldmann, editor, Proc. WST, pages 59–63, 2013.  doi:10.48550/arXiv.1601.03206.
  * [14] C. Kop.  WANDA – a higher-order termination tool.  In Proc. FSCD, pages 36:1–36:19, 2020.  doi:10.4230/LIPIcs.FSCD.2020.36.
  * [15] C. Kop.  Cutting a proof into bite-sized chunks: Incrementally proving termination in higher-order term rewriting.  In A. Felty, editor, Proc. FSCD, pages 1:1–1:17, 2022.  doi:10.4230/LIPIcs.FSCD.2022.1.
  * [16] C. Kop.  A weakly monotonic, logically constrained, HORPO-variant.  Technical report, Radboud University, 2024.  URL: https://arxiv.org/abs/2406.18493.
  * [17] 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.
  * [18] C. Kop and D. Vale.  Tuple interpretations for higher-order complexity.  In Proc. FSCD, pages 31:1–31:22, 2021.  doi:10.4230/LIPIcs.FSCD.2021.31.
  * [19] C. Kop and D. Vale.  hezzel/cora: Artifact for MFCS 2024, 2024.  doi:10.5281/zenodo.12551027.
  * [20] C. Kop and F. van Raamsdonk.  Dynamic dependency pairs for algebraic functional systems.  LMCS, 8(2):10:1–10:51, 2012.  doi:10.2168/lmcs-8(2:10)2012.
  * [21] 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.
  * [22] A. Matsumi, N. Nishida, and D. Shin.  On singleton self-loop removal for termination of lctrss with bit-vector arithmetic.  In A. Yamada, editor, Proc. WST, 2023.  doi:10.48550/arXiv.2307.14094.
  * [23] P. W. O’Hearn.  Continuous reasoning: scaling the impact of formal methods.  In A. Dawar and E. Grädel, editors, Proc. LICS, pages 13–25, 2018.  doi:10.1145/3209108.3209109.
  * [24] J.C. van de Pol.  Termination of Higher-order Rewrite Systems.  PhD thesis, University of Utrecht, 1996.  URL: https://www.cs.au.dk/~jaco/papers/thesis.pdf.
  * [25] M. R. K. K. 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.
  * [26] M. R. K. K. 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.
  * [27] M. R. K. K. 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.
  * [28] M. Sakai and K. Kusakari.  On dependency pair method for proving termination of higher-order rewrite systems.  IEICE Trans. Inf. Syst., E88-D(3):583–593, 2005.  doi:10.1093/ietisy/e88-d.3.583.
  * [29] M. Sakai, Y. Watanabe, and T. Sakabe.  An extension of the dependency pair method for proving termination of higher-order rewrite systems.  IEICE Trans. Inf. Syst., E84-D(8):1025–1032, 2001.  URL: https://search.ieice.org/bin/summary.php?id=e84-d_8_1025.
  * [30] R. Tarjan.  Depth-first search and linear graph algorithms.  SICOMP, 1(2):146–160, 1972.  doi:10.1137/0201010.
  * [31] R. Thiemann.  The DP Framework for Proving Termination of Term Rewriting.  PhD thesis, RWTH Aachen University, 2007.  URL: http://cl-informatik.uibk.ac.at/users/thiemann/paper/diss.pdf.
  * [32] A. Yamada.  Tuple interpretations for termination of term rewriting.  J. Automated Reasoning, 66(4):667–688, 2022.  doi:10.1007/s10817-022-09640-4.
  * [33] H. Zantema.  Termination of term rewriting: interpretation and type elimination.  J. Symbolic Computation, 17:23–50, 1994.  doi:10.1006/jsco.1994.1003.

##  Appendix A Proofs of the Results

###  A.1 The Proof of Theorem 3.6

See 3.6

######  Proof A.1.

Assume that $\mathcal{R}$ is not terminating. By definition, there exists a
non-terminating term $u$, which cannot be $\mathbb{C}$-computable. Take a
minimal subterm $s$ of $u$ such that $s$ is not $\mathbb{C}$-computable, then
$s$ must take the form ${f}\ {{s}_{1}\cdots{s}_{k}}$ where $f$ is a defined
symbol and $s_{i}$ is $\mathbb{C}$-computable for all $i$. Let the type of $f$
be denoted by ${A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow B$ where
$B$ is a sort. Because $s={f}\ {{s}_{1}\cdots{s}_{k}}$ is not
$\mathbb{C}$-computable, there exist $\mathbb{C}$-computable terms
${s}_{k+1},\ldots,{s}_{m}$ such that ${s}\ {{s}_{k+1}\cdots{s}_{m}}={f}\
{{s}_{1}\cdots{s}_{m}}$ is not $\mathbb{C}$-computable.

Now due to Corollary A.19 (with $\mathcal{R}_{0}=\mathcal{R}$ and
$\mathcal{R}_{1}=\emptyset$), there exists an infinite computable
$(\operatorname{SDP}(\mathcal{R}),\mathcal{R})$-chain. The non-existence of
such a chain implies the termination of $\mathcal{R}$.

###  A.2 The Proof of Theorem 4.16

We split up the proof of Theorem 4.16 into proofs for the individual
processors.

######  Theorem A.2.

Graph processors are sound.

######  Proof A.3.

By definition of DP graph, any $(\mathcal{P},\mathcal{R})$-chain induces a
path in the DP graph $G$ of $\mathcal{P}$. By definition of graph
homomorphism, this is directly mapped to a path in the approximation
$G_{\theta}$. Since the approximation only has finitely many vertices, the
path of an infinite $(\mathcal{P},\mathcal{R})$-chain must touch at least some
vertices infinitely often.

Let $v_{1},\dots,v_{n}$ be these dependency pairs. Since all other vertices
are only touched finitely often, eventually the path _only_ touches these
vertices; that is, the chain has an infinite tail containing only DPs $p$ with
$\theta(p)\in\\{v_{1},\dots,v_{n}\\}$.

Since each $v_{i}$ occurs infinitely often, there is a path from each $v_{i}$
to each $v_{j}$ in $G_{\theta}$. Thus, all $v_{i}$ must be in the same
strongly connected component.

We did not formally state the following result in the text, but it is implied:

######  Lemma A.4.

The Cap-based approach described in the implementation part of Section 4.1
indeed yields an approximation of DP graph of $\mathcal{P}$. This holds
whether we consider the graph for $\mathcal{R}$, or for any extension
$\mathcal{R}\cup\mathcal{R}_{1}$.

######  Proof A.5.

Let ${t}\Rightarrow{s}\ [\varphi\mid L]$ and ${t}\Rightarrow{s}\ [\varphi\mid
L]$ be DPs with no shared variables. There should be an edge from
${t}\Rightarrow{s}\ [\varphi\mid L]$ to ${t}\Rightarrow{s}\ [\varphi\mid L]$
in a graph approximation if there exists a substitution $\sigma$ such that (a)
$\sigma$ maps all variables in $L$ and $L^{\prime}$ to ground theory terms,
(b) $[\\![\varphi\sigma]\\!]=[\\![\varphi^{\prime}\sigma]\\!]=1$, and (c)
$s\sigma\rightarrow_{\mathcal{R}}^{*}t^{\prime}\sigma$. As we only need an
approximation, false positives are allowed. Thus we must see, if such $\sigma$
exists, then $\varphi\wedge\varphi^{\prime}\wedge\zeta(s,t)$ is satisfiable.
We claim that it is satisfiable by the valuation that maps $x$ to
$[\\![\sigma(x)]\\!]$ whenever $\sigma(x)$ is a ground theory term. With this
valuation, certainly $\varphi$ and $\varphi^{\prime}$ are satisfied. To
complete the proof, we show by induction on $u$ that if
$u\sigma\rightarrow_{\mathcal{R}\cup\mathcal{R}_{1}}^{*}v\sigma$ then this
valuation satisfies $\zeta(u,v)$.

  * •

If $u={f}\ {{u}_{1}\cdots{u}_{n}}$ and there is a rule in $\mathcal{R}$ that
could potentially reduce $u\sigma$ at the top, then the left-hand side of such
a rule must apply $f$ to at most $n$ arguments. In this case, $\zeta(u,v)$
yields $\mathfrak{t}$, so there is nothing to prove (recall that false
positives are allowed).

  * •

If $u={f}\ {{u}_{1}\cdots{u}_{n}}$ with $f$ not a theory symbol, and there is
no rule in $\mathcal{R}$ that can reduce $u\sigma$ at the top, then since $f$
occurs in the original signature, there is no rule in $\mathcal{R}_{1}$ that
can reduce $u$ at the top either (by definition of an extension). Hence,
$v\sigma$ must have a shape ${f}\ {{t}_{1}\cdots{t}_{n}}$. So, the case
$v={g}\ {{u}_{1}\cdots{u}_{m}}$ with $f\neq g$ cannot occur, and if $v={f}\
{{v}_{1}\cdots{v}_{n}}$ then by the induction hypothesis the valuation must
satisfy $\zeta(u_{i},v_{i})$ for all $i$. In all other cases, $\zeta(u,v)$
yields $\mathfrak{t}$, so again, there is nothing to prove.

  * •

If $u={f}\ {{u}_{1}\cdots{u}_{n}}$ with $f$ a theory symbol, and there is a
rule in $\mathcal{R}$ that could potentially reduce $u\sigma$ at the top, then
$\zeta(u,v)$ yields $\mathfrak{t}$ as in the first case. If there is not, then
the only way to reduce $u\sigma$ at the top is using a calculation rule.
Hence, $v\sigma$ must have a shape ${f}\ {{t}_{1}\cdots{t}_{n}}$, or be a
value.

    * –

If $v$ is not a value, but does have a form ${g}\ {{u}_{1}\cdots{u}_{m}}$ (or
${f}\ {{v}_{1}\cdots{v}_{n}}$), then $v\sigma$ is not a value, so we complete
as we did in the second case.

    * –

If $v$ is a value or variable, and all variables in $u$ occur in $L$, then
note that $u\sigma$ is a ground theory term, and as left-hand sides of rules
cannot be theory terms, the only way to reduce a ground theory term uses the
calculation rules, which preserves the value of the term. Hence, $u=v$ must
hold in the given valuation.

    * –

In all other cases, $\zeta(u,v)$ yields $\mathfrak{t}$, so there is nothing to
prove.

  * •

If $u$ is a variable in $L$, then $u\sigma$ is a ground theory term. As above,
we conclude that $u=v$ must hold in the given valuation.

  * •

If $u$ is a variable not in $L$ then $\zeta(u,v)$ yields $\mathfrak{t}$, so
there is nothing to prove. The same holds if $u={x}\ {{u}_{1}\cdots{u}_{n}}$
with $n>0$, since in this case $x$ cannot occur in $L$ by definition of a
constraint.

######  Remark A.6.

We do not have any clever logic for the case where $v={x}\
{{v}_{1}\cdots{v}_{m}}$, because this case does not occur in practice (as
left-hand sides of DPs are in practice always patterns). It would not be hard
to add additional cases for this if new DP processors were to be defined that
broke the pattern property, however.

######  Theorem A.7.

Subterm criterion processors are sound.

######  Proof A.8.

We first observe: if $u\trianglerighteq\cdot\rightarrow_{\mathcal{R}}^{*}v$
then $u\rightarrow_{\mathcal{R}}^{*}{C}[v]$ for some context $C$. Hence, if
$t_{i}\trianglerighteq\cdot\rightarrow_{\mathcal{R}}^{*}t_{i+1}$ for all $i$
but $t_{1}$ is terminating, then eventually this sequence stops using
$\rightarrow_{\mathcal{R}}$ steps: there exists $N$ such that for all $i>N$:
$t_{i}\trianglerighteq t_{i+1}$. But _strict_ subterm steps are also
terminating, since they decrease the size of the term. So, eventually all
$\trianglerighteq$ steps are really equalities. Thus, there exists $M$ such
that for all $i>M$: $t_{i}=t_{i+1}$.

Now, any infinite computable $\mathcal{P}$-chain yields an infinite sequence
of steps
$\bar{\nu}({s_{i}}^{\sharp}\sigma_{i})\trianglerighteq\bar{\nu}({t_{i}}^{\sharp}\sigma_{i})\rightarrow^{*}\bar{\nu}({s_{i+1}}^{\sharp}\sigma_{i+1})$.
Since the immediate arguments of all ${t_{i}}^{\sharp}\sigma_{i}$ are
computable, and therefore terminating, such a sequence can only have finitely
many steps where the $\trianglerighteq$ step is strict (as we observed above).
Thus, there is an infinite tail of the chain using only SDPs that are not in
$\mathcal{P}^{\prime}$.

######  Theorem A.9.

Integer mapping processors are sound.

######  Proof A.10.

We first observe: if $i\in\iota({g}^{\sharp})$ and $\sigma$ respects an SDP
${{{f}^{\sharp}}\ {{s}_{1}\cdots{s}_{m}}}\Rightarrow{{{g}^{\sharp}}\
{{t}_{1}\cdots{t}_{n}}}\ [\varphi\mid L]$, then by definition of $\iota()$ and
“respect”, $t_{i}\sigma$ is a ground theory term, and since the left-hand
sides of rules in $\mathcal{R}$ cannot be theory terms, any
$\rightarrow_{\mathcal{R}}^{*}$ reduct of $t_{i}\sigma$ can only be obtained
with $\rightarrow_{\kappa}$, which does not change the value.

Hence, in an infinite chain $[{{s_{j}}^{\sharp}}\Rightarrow{{t_{j}}^{\sharp}}\
[\varphi_{j}\mid L_{j}]\mid j\in\mathbb{N}]$, for all $j$ we have that
$\bar{\mathcal{J}}({s_{j}}^{\sharp})\sigma_{j}$ and
$\bar{\mathcal{J}}({t_{j}}^{\sharp})\sigma_{j}$ are necessarily ground theory
terms, and
$[\\![\bar{\mathcal{J}}({t_{j}}^{\sharp})\sigma_{j}]\\!]=[\\![\bar{\mathcal{J}}({t_{j+1}}^{\sharp})\sigma_{j+1}]\\!]$

Let $\sigma_{j}^{\downarrow}$ be the substitution that maps each $x$ in the
domain of $\sigma_{j}$ to $\sigma_{j}(x)\\!\downarrow_{\kappa}$. Then
$\sigma_{j}$ maps the variables in each constraint and in
$\bar{\mathcal{J}}({s_{j}}^{\sharp})$ and
$\bar{\mathcal{J}}({t_{j}}^{\sharp})$ to values (all these variables occur in
$L_{j}$, so have a theory sort).

Since $\sigma_{j}$ respects $\varphi_{j}$, we have that
$[\\![\varphi_{j}\sigma_{j}]\\!]=[\\![\varphi_{j}\sigma_{j}^{\downarrow}]\\!]=1$,
so by assumption
$[\\![\bar{\mathcal{J}}({s_{j}}^{\sharp})\sigma_{j}]\\!]=[\\![\bar{\mathcal{J}}({s_{j}}^{\sharp})\sigma_{j}^{\downarrow}]\\!]\geq[\\![\bar{\mathcal{J}}({t_{j}}^{\sharp})\sigma_{j}^{\downarrow}]\\!]=[\\![\bar{\mathcal{J}}({t_{j}}^{\sharp})\sigma_{j}]\\!]$
for all ${{s_{j}}^{\sharp}}\Rightarrow{{t_{j}}^{\sharp}}\ [\varphi_{j}\mid
L_{j}]\in\mathcal{P}\setminus\mathcal{P}^{\prime}$, and for
${{s_{j}}^{\sharp}}\Rightarrow{{t_{j}}^{\sharp}}\ [\varphi_{j}\mid
L_{j}]\in\mathcal{P}^{\prime}$ we even have both
$[\\![\bar{\mathcal{J}}({s_{j}}^{\sharp})\sigma_{j}]\\!]>[\\![\bar{\mathcal{J}}({t_{j}}^{\sharp})\sigma_{j}]\\!]$
and $[\\![\bar{\mathcal{J}}({s_{j}}^{\sharp})\sigma_{j}]\\!]>0$.

Since only finitely many decreasing steps can be done before reaching $0$, any
infinite $\mathcal{P}$-chain must have an infinite tail not using the elements
of $\mathcal{P}^{\prime}$.

######  Theorem A.11.

Theory argument processors are sound.

######  Proof A.12.

Let us say that a term ${{f}^{\sharp}}\ {{s}_{1}\cdots{s}_{m}}$ respects
$\tau$ if $s_{i}$ is a ground theory term for every $i\in\tau({f}^{\sharp})$.
Note that:

  1. 1.

If $t$ respects $\tau$ and $t\rightarrow_{\mathcal{R}}s$ then also $s$
respects $\tau$, because ground theory terms can only be rewritten using
$\rightarrow_{\kappa}$ (since left-hand sides of rules may not be theory
terms).

  2. 2.

For any dependency pair ${{{f}^{\sharp}}\
{{s}_{1}\cdots{s}_{n}}}\Rightarrow{{{g}^{\sharp}}\ {{t}_{1}\cdots{t}_{m}}}\
[\varphi\mid L]$ and substitution $\sigma$ that respects this DP: if
${{f}^{\sharp}}\ {{s}_{1}\cdots{s}_{n}}\sigma$ respects $\tau$ then
$\sigma(x)$ is a ground theory term for any $x\in
L\cup\\{y\in\operatorname{Var}(s_{i})\mid i\in\tau(f)$. Therefore, by
definition of a theory arguments mapping, also $t_{j}\sigma$ is a ground
theory term for any $j\in\tau(g)$, so ${{g}^{\sharp}}\ {{t}_{1}\cdots{t}_{m}}$
respects $\tau$ as well.

  3. 3.

If $\tau$ fixes a dependency pair ${s}\Rightarrow{t}\ [\varphi\mid L]$, then
for any substitution $\sigma$ that respects this DP, $t\sigma$ respects
$\tau$.

Hence, in an infinite $(\mathcal{P},\mathcal{R})$-chain
$[({s_{i}}\Rightarrow{t_{i}}\ [\varphi_{i}\mid L_{i}],\sigma_{i})\mid
i\in\mathbb{N}]$, if any DP ${s_{i}}\Rightarrow{t_{i}}\ [\varphi_{i}\mid
L_{i}]$ fixes $\tau$, then by (3) $t_{i}\sigma_{i}$ respects $\tau$, so by (1)
$s_{i+1}\sigma_{i+1}$ respects $\tau$, and by (2) also $t_{i+1}\sigma_{i+1}$
respects $\tau$. Hence, the chain has an infinite tail such that each
$\sigma_{j}$ ($j>i$) respects the SDP $\bar{\tau}({s_{j}}\Rightarrow{t_{j}}\
[\varphi_{j}\mid L_{j}])$.

Thus, if $\tau$ fixes $\mathcal{P}^{\prime}$ there are two possibilities to
create an infinite $(\mathcal{P},\mathcal{R})$-chain: either the chain does
not use any DP in $\mathcal{P}^{\prime}$—so it is a
$(\mathcal{P}\setminus\mathcal{P}^{\prime},\mathcal{R})$-chain—or it has an
infinite tail that is a $(\\{\bar{\tau}(p)\mid
p\in\mathcal{P}\\},\mathcal{R})$-chain.

Moreover, if it is given that the first DP in the chain is an element of
$\mathcal{P}^{\prime}$ (which is the case in the public computability setting
if $\mathcal{P}^{\prime}$ includes all public dependency pairs) then the chain
_is_ a $(\\{\bar{\tau}(p)\mid p\in\mathcal{P}\\},\mathcal{R})$-chain.

######  Theorem A.13.

Reduction pair processors are sound.

######  Proof A.14.

Suppose a reduction pair with the given properties is given, and let
$(\sqsupseteq,\sqsupset)$ be the covering pair. We observe:

  * •

If $s\rightarrow_{\mathcal{R}}t$ then
$s\downarrow_{\kappa}\sqsupseteq^{*}t\downarrow_{\kappa}$.

_Proof:_ by induction on the form of $s$.

    * –

If $s$ is a ground theory term, then note that no rule from $\mathcal{R}$
applies, since rules may not be theory terms. Hence, the reduction is with a
$\rightarrow_{\kappa}$ step, and we have
$s\downarrow_{\kappa}=t\downarrow_{\kappa}$.

    * –

Otherwise, if $s=\ell\sigma$ and $t=r\sigma$ for some rule
${\ell}\rightarrow{r}\ [\varphi]$ and substitution $\sigma$ that respects this
rule, then by (c) and the assumption that $\sqsupseteq$ covers $\succeq$ we
have $s\downarrow_{\kappa}\sqsupseteq t\downarrow_{\kappa}$.

    * –

Otherwise, $s={s_{1}}\ {s_{2}}$, and either $t={s_{1}}\ {t_{2}}$ with
$s_{2}\rightarrow_{\mathcal{R}}t_{2}$ or $t={t_{1}}\ {s_{2}}$ with
$s_{1}\rightarrow_{\mathcal{R}}t_{1}$. We consider only the second option; the
first is similar. Since we excluded the case that $s$ is a ground theory term,
$s$ does not $\rightarrow_{\kappa}$-reduce at the top, so
$s\downarrow_{\kappa}={(s_{1}\downarrow_{\kappa})}\
{(s_{2}\downarrow_{\kappa})}$. By the induction hypothesis,
$s_{1}\downarrow_{\kappa}\sqsupseteq^{*}t_{1}\downarrow_{\kappa}$. Thus, by
monotonicity of $\sqsupseteq$ we have
$s\downarrow_{\kappa}\sqsupseteq{(t_{1}\downarrow_{\kappa})}\
{(s_{2}\downarrow_{\kappa})}$, which
$\sqsupseteq^{*}({(t_{1}\downarrow_{\kappa})}\
{s_{2}\downarrow_{\kappa})})\downarrow_{\kappa}=t\downarrow_{\kappa}$ because
$\sqsupseteq$ includes $\rightarrow_{\kappa}$ (this covers the case where $t$
is a ground theory term even though $s$ is not).

  * •

If ${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid
L]\in\mathcal{P}^{\prime}$, and $\sigma$ is a substitution that respects
${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid L]$, then
$(s\sigma)\downarrow_{\kappa}\sqsupset(t\sigma)\downarrow_{\kappa}$, and
similarly, if ${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid
L]\in\mathcal{P}\setminus\mathcal{P}^{\prime}$, and $\sigma$ is a substitution
that respects ${{s}^{\sharp}}\Rightarrow{{t}^{\sharp}}\ [\varphi\mid L]$, then
$(s\sigma)\downarrow_{\kappa}\sqsupseteq(t\sigma)\downarrow_{\kappa}$.

_Proof:_ immediately by (a), (b) and the definition of “covers”.

Hence, any infinite $(\mathcal{P},\mathcal{R})$-chain induces an infinite
sequence of $\sqsupseteq^{*}$ and $\sqsupset$ steps, and if any step in
$\mathcal{P}^{\prime}$ occurs infinitely often, then $\sqsupset$ occurs
infinitely often. Since $\sqsupseteq\cdot\sqsupset$ is included in
$\sqsupset^{+}$, this yields an infinitely decreasing $\sqsupset^{+}$
sequence, which contradicts well-foundedness of $\sqsupset$. Hence, we see
that the steps in $\mathcal{P}^{\prime}$ can occur at most finitely often, and
there is an infinite tail of the dependency chain using only pairs in
$\mathcal{P}\setminus\mathcal{P}^{\prime}$.

###  A.3 The Proof of Theorem 5.6

For the properties of $\mathbb{C}$-computability, see Appendix
A111https://doi.org/10.48550/arXiv.1902.06733 of [6]. In order to prove
Theorem 5.6, we first present two lemmas.

######  Lemma A.15.

Undefined function symbols are $\mathbb{C}$-computable.

######  Proof A.16.

Given an LCSTRS $\mathcal{R}$ and an undefined function symbol
$f:{A}_{1}\rightarrow\cdots\rightarrow{A}_{n}\rightarrow B$ where $B$ is a
sort, take arbitrary $\mathbb{C}$-computable terms ${t}_{1},\ldots,{t}_{n}$
such that $t_{i}:A_{i}$ for all $i$. Consider the reducts of ${f}\
{{t}_{1}\cdots{t}_{n}}$, each of which must be either ${f}\
{{t^{\prime}}_{1}\cdots{t^{\prime}}_{n}}$ where
$t_{i}\rightarrow_{\mathcal{R}}t_{i}^{\prime}$ for all $i$ or a value (when
$f$ is a theory symbol) because $f$ is undefined. By definition, ${f}\
{{t}_{1}\cdots{t}_{n}}\in\mathbb{C}$, and therefore $f$ is
$\mathbb{C}$-computable.

######  Lemma A.17.

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
$f:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow B$ in
$\mathcal{R}_{0}$ where $B$ is a sort, if ${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$, there exist an SDP
${{{f}^{\sharp}}\
{{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}}\Rightarrow{{{g}^{\sharp}}\
{{t}_{1}\cdots{t}_{n}}}\ [\varphi\mid
L]\in\operatorname{SDP}(\mathcal{R}_{0})$ and a substitution $\sigma$ such
that (1)
$s_{i}\rightarrow_{\mathcal{R}_{0}\cup\mathcal{R}_{1}}^{*}s_{i}^{\prime}\sigma$
for all $i$, (2) $\sigma$ respects ${{{f}^{\sharp}}\
{{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}}\Rightarrow{{{g}^{\sharp}}\
{{t}_{1}\cdots{t}_{n}}}\ [\varphi\mid L]$, and (3) $({g}\
{{t}_{1}\cdots{t}_{n}})\sigma={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 ${g}\
{{t}_{1}\cdots{t}_{n}}$.

######  Proof A.18.

We consider $\mathbb{C}$-computability in $\mathcal{R}_{0}\cup\mathcal{R}_{1}$
with $\succsim^{\prime}$. If all the reducts of ${f}\ {{s}_{1}\cdots{s}_{m}}$
were either ${f}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}$ where
$s_{i}\rightarrow_{\mathcal{R}_{0}\cup\mathcal{R}_{1}}^{*}s_{i}^{\prime}$ for
all $i$ or a value (when $f$ is a theory symbol), ${f}\
{{s}_{1}\cdots{s}_{m}}$ would be computable. Hence, there exist a rewrite rule
${{f}\ {{s^{\prime}}_{1}\cdots{s^{\prime}}_{p}}}\rightarrow{r}\
[\varphi]\in\mathcal{R}_{0}$ ($f$ cannot be defined in $\mathcal{R}_{1}$) and
a substitution $\sigma^{\prime}$ such that
$s_{i}\rightarrow_{\mathcal{R}_{0}\cup\mathcal{R}_{1}}^{*}s_{i}^{\prime}\sigma^{\prime}$
for all $i\leq p$ and $\sigma^{\prime}$ respects the rewrite rule;
${(r\sigma^{\prime})}\ {{s}_{p+1}\cdots{s}_{m}}$ is thus a reduct of ${f}\
{{s}_{1}\cdots{s}_{m}}$. There is at least one such reduct that is
uncomputable—otherwise, ${f}\ {{s}_{1}\cdots{s}_{m}}$ would be computable. Let
${(r\sigma^{\prime})}\ {{s}_{p+1}\cdots{s}_{m}}$ be uncomputable, and
therefore so is $r\sigma^{\prime}$.

Take a minimal subterm $t$ of $r$ such that $t\sigma^{\prime}$ is
uncomputable. If $t={x}\ {{t}_{1}\cdots{t}_{q}}$ for some variable $x$,
$\sigma^{\prime}(x)$ is either a value or an accessible subterm of
$s_{k}^{\prime}\sigma^{\prime}$ for some $k$ because $\mathcal{R}_{0}$ is AFP.
Either way, $\sigma^{\prime}(x)$ is computable. Due to the minimality of $t$,
$t_{i}\sigma^{\prime}$ is computable for all $i$, which implies the
computability of $t\sigma^{\prime}={\sigma^{\prime}(x)}\
{(t_{1}\sigma^{\prime})\cdots(t_{q}\sigma^{\prime})}$. This contradiction
shows that $t={g}\ {{t}_{1}\cdots{t}_{q}}$ for some function symbol $g$ in
$\mathcal{R}_{0}$. And $g$ must be a defined symbol.

Now we have an SDP ${{{{f}^{\sharp}}\
{{s^{\prime}}_{1}\cdots{s^{\prime}}_{p}}}\
{{x}_{p+1}\cdots{x}_{m}}}\Rightarrow{{{{g}^{\sharp}}\ {{t}_{1}\cdots{t}_{q}}}\
{{y}_{q+1}\cdots{y}_{n}}}\
[\varphi\mid\operatorname{Var}(\varphi)\cup(\operatorname{Var}(r)\setminus\operatorname{Var}({f}\
{{s^{\prime}}_{1}\cdots{s^{\prime}}_{p}}))]\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}}={{g}\
{(t_{1}\sigma^{\prime})\cdots(t_{q}\sigma^{\prime})}}\
{{t^{\prime}}_{q+1}\cdots{t^{\prime}}_{n}}$ is uncomputable. Let $\sigma$ be
the substitution 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 variable $z$. Let
$s_{i}^{\prime}$ denote $x_{i}$ for all $i>p$, let $t_{i}$ denote $y_{i}$ for
all $i>q$, and let $L$ denote
$\operatorname{Var}(\varphi)\cup(\operatorname{Var}(r)\setminus\operatorname{Var}({f}\
{{s^{\prime}}_{1}\cdots{s^{\prime}}_{p}}))$, then ${{{f}^{\sharp}}\
{{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}}\Rightarrow{{{g}^{\sharp}}\
{{t}_{1}\cdots{t}_{n}}}\ [\varphi\mid L]$ and $\sigma$ satisfy all the
requirements.

######  Corollary A.19.

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
$f:{A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow B$ in
$\mathcal{R}_{0}$ where $B$ is a sort, if ${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$, there exists an infinite
computable
$(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$-chain
$({{{f}^{\sharp}}\
{{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}}\Rightarrow{{t}^{\sharp}}\
[\varphi\mid L],\sigma),\ldots$

######  Proof A.20.

Repeatedly applying Lemma A.17—first on ${f}\ {{s}_{1}\cdots{s}_{m}}$, then on
${g}\ {(t_{1}\sigma)\cdots(t_{n}\sigma)}$ and so on—we thus get such an
infinite computable
$(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$-chain.

See 5.6

######  Proof A.21.

Assume that $\mathcal{R}_{0}$ is not publicly computable. By definition, there
exist a public extension $\mathcal{R}_{1}$ of $\mathcal{R}_{0}$, a sort
ordering $\succsim^{\prime}$ which extends $\succsim$ over sorts in
$\mathcal{R}_{0}\cup\mathcal{R}_{1}$ and a public term $u$ of
$\mathcal{R}_{0}$ such that $u$ 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}$ with
$\succsim^{\prime}$. Take a minimal uncomputable subterm $s$ of $u$, then $s$
must take the form ${f}\ {{s}_{1}\cdots{s}_{k}}$ where $f$ is a defined symbol
in $\mathcal{R}_{0}$ and $s_{i}$ is computable for all $i$. Let the type of
$f$ be denoted by ${A}_{1}\rightarrow\cdots\rightarrow{A}_{m}\rightarrow B$
where $B$ is a sort. Because $s={f}\ {{s}_{1}\cdots{s}_{k}}$ is uncomputable,
there exist computable terms ${s}_{k+1},\ldots,{s}_{m}$ of
$\mathcal{R}_{0}\cup\mathcal{R}_{1}$ such that ${s}\
{{s}_{k+1}\cdots{s}_{m}}={f}\ {{s}_{1}\cdots{s}_{m}}$ is uncomputable.

Now due to Corollary A.19, there exists an infinite computable
$(\operatorname{SDP}(\mathcal{R}_{0}),\mathcal{R}_{0}\cup\mathcal{R}_{1})$-chain
$({{{f}^{\sharp}}\
{{s^{\prime}}_{1}\cdots{s^{\prime}}_{m}}}\Rightarrow{{t}^{\sharp}}\
[\varphi\mid L],\sigma),\ldots$, which is public because $f$ is not a hidden
symbol by construction. The non-existence of such a chain implies the public
computability of $\mathcal{R}_{0}$.

###  A.4 The Proof of Theorem 5.11

We split up the proof of Theorem 5.11 into proofs for the individual
processors.

######  Theorem A.22.

The modified theory argument processors are sound.

######  Proof A.23.

We refer to the proof of Theorem A.11, and in particular the final
observation: “if it is given that the first DP in the chain is an element of
$\mathcal{P}^{\prime}$ (which is the case in the public computability setting
if $\mathcal{P}^{\prime}$ includes all public dependency pairs) then the chain
_is_ a $(\\{\bar{\tau}(p)\mid p\in\mathcal{P}\\},\mathcal{R})$-chain.” As the
root symbol of the first DP in the chain is unchanged, the chain is still
public.

######  Theorem A.24.

Constraint modification processors are sound.

######  Proof A.25.

If $\mathcal{P}^{\prime}$ covers $\mathcal{P}$, every computable
$(\mathcal{P},\mathcal{R}_{0}\cup\mathcal{R}_{1})$-chain corresponds to a
computable $(\mathcal{P}^{\prime},\mathcal{R}_{0}\cup\mathcal{R}_{1})$-chain
which has the same length and the same heading symbol.

######  Theorem A.26.

Reachability processors are sound.

######  Proof A.27.

Approximations over-approximate the DP graph and SDPs that are unreachable
from any public SDP cannot contribute to public chains.