Representing Nonterminating Rewriting with $\mathbf{F}_2^\mu$

TL;DR

This paper introduces a second-order type system, $ extbf{F}_2^$, for representing and deciding nontermination in rewriting systems, with a focus on productivity and a practical type checker implementation.

Contribution

The paper defines $ extbf{F}_2^$, proves decidability of productivity checking via a lambda-Y calculus mapping, and develops a type checker based on second-order matching.

Findings

Productivity checking in $ extbf{F}_2^$ is decidable.

A type checking algorithm for $ extbf{F}_2^$ is developed and implemented.

The system effectively represents nonterminating rewrite traces.

Abstract

We specify a second-order type system $\mathbf{F}_2^\mu$ that is tailored for representing nonterminations. The nonterminating trace of a term $t$ in a rewrite system $\mathcal{R}$ corresponds to a productive inhabitant $e$ such that $\Gamma_{\mathcal{R}} \vdash e : t$ in $\mathbf{F}_2^\mu$, where $\Gamma_{\mathcal{R}}$ is the environment representing the rewrite system. We prove that the productivity checking in $\mathbf{F}_2^\mu$ is decidable via a mapping to the $\lambda$-Y calculus. We develop a type checking algorithm for $\mathbf{F}_2^\mu$ based on second-order matching. We implement the type checking algorithm in a proof-of-concept type checker.

Equations

$$T::=A|\forall \underline{x}.T\Rightarrow ...\Rightarrow T\Rightarrow A$$

Full text

1 Introduction

Nontermination has been an active research area in the term rewriting community. Early studies includes classifying nonterminations based on the concept of looping reduction [6], i.e. a reduction of the shape $t\to^{+}C[\sigma t]$ for some substitution $\sigma$. More recently, many nontermination detection techniques are proposed and implemented. Emmes et. al. [8] considered a generalized notion of looping reduction, e.g. $\sigma_{2}\sigma_{1}^{n}t\to^{+}C[\sigma_{3}\sigma_{2}\sigma_{1}^{f(n)}t]$ for some substitutions $\sigma_{1},\sigma_{2},\sigma_{3}$ and some ascending linear function $f$. Endrullis and Zantema [9] used a SAT solver to search for a non-empty regular language of terms such that it is closed under reduction and does not contain normal forms.

The nonterminating reductions are usually described using mathematical notations and abbreviations. In this paper, we consider a novel representation using a relatively simple type system. In particular, a nonterminating reduction of a term will be encoded as a proof evidence in a type system called $\mathbf{F}_{2}^{\mu}$. Representing nonterminating reduction is closely related to proving nontermination, but they have some subtle differences. For proving nontermination, it is enough to exibit a nonterminating reduction for a term, while a term can admit multiple nonterminating reduction traces, with each trace exibits a different kind of reduction pattern.

Example 1.1**.**

Consider the following two string rewriting rules: $A\to_{a}AB,B\to_{b}A$. It is nonterminating by the observation that it contains the rule $A\to_{a}AB$, which means there is a nonterminating reduction of the form $A\to_{a}AB\to_{a}ABB\to_{a}ABBB\to_{a}...$. We can also use a L-system111See https://en.wikipedia.org/wiki/L-system. like parallel reduction strategy to reduce $A$, this gives rise to the nonterminating reduction: ${{A}}\Longrightarrow{{A}B}\Longrightarrow{{A}BA}\Longrightarrow{{A}BAAB}\Longrightarrow{{A}BAABABA}\Longrightarrow{{A}BAABABAABAAB}\Longrightarrow...$. Note that all the redexes at each step are reduced simultaneously and each word in the sequence is a concatenation of the previous two. The aforementioned two reduction sequences are fundamentally different. The first one exibits a regular property, i.e. each string at each step can be described by the regular expression $AB^{*}$. In the second reduction sequence, each string is called a Fibonacci word, and the set of all such words is known to be context-free free, i.e. any infinite subset can not be described by a context-free language [25]. We will show how to represent the second reduction sequence in Section 6.

The main contributions of the paper are the following ones.

• •

Inspired by Leibniz equality, we represent a rewrite rule $l\to r$ as a typing environment $\kappa:\forall p.\forall\underline{x}.p\ r\Rightarrow p\ l$, where the type variable $p$ of kind $*\Rightarrow*$ represents a reduction context, $\kappa$ is a fresh constant evidence and $\underline{x}$ denotes the set of variables in $l$. A specialized kind system is used to ensure the type variable of kind $*\Rightarrow*$ represents a reduction context. We call this representation of rewrite rule Leibniz representation in Section 3.

• •

Nonterminating reductions would result in infinite proof evidence, we use the fixed point typing rule to represent the reductions finitely. Thus a nonterminating reduction of $t$ in $\mathcal{R}$ can be represented as $\Gamma_{\mathcal{R}}\vdash e:t$, where $e$ is an evidence containing a fixed point and $\Gamma_{\mathcal{R}}$ is the Leibniz representation of $\mathcal{R}$. We called the resulting type system $\mathbf{F}_{2}^{\mu}$ (Section 3).

• •

We prove that if $\Gamma_{\mathcal{R}}\vdash e:t$ and $e$ is hereditary head normalizing(HHN), then we can recover from the evidence $e$ a nonterminating reduction of $t$ (Section 4). We also prove that the hereditary head normalization is decidable in $\mathbf{F}_{2}^{\mu}$. The decidability result is obtained via a mapping from $\mathbf{F}_{2}^{\mu}$ to $\lambda$-Y calculus, for which HHN is decidable.

• •

It is more convenient to write the unannotated proof evidence and let the type checker fill in the annotations. For this purpose we develop a second-order type checking algorithm in Section 5 and Section 6. It simplifies the process of representing nonterminations in $\mathbf{F}_{2}^{\mu}$. We implement a prototype type checker222The prototype type checker is available at https://github.com/Fermat/FCR based on this algorithm and give some nontrivial examples in the Appendix.

All the examples and the missing proofs in this paper may be found in the Appendix.

2 The Main Idea

First, let us consider how to represent a rewrite system in a type system. We could model the rewrite rule $l\to r$ as a typing environment $\kappa:l\Rightarrow r$, like many proof systems for rewriting ([22], [20]). However, modeling the rewrite rule $l\to r$ as an implication type $l\Rightarrow r$ will make it difficult to observe the proof evidence. For example, suppose we have a set of ground rewrite rules $A_{i}\to A_{i+1}$ modelled by $\kappa_{i}:A_{i}\Rightarrow A_{i+1}$ for $0\leq i\leq n$ for some $n$, where $\kappa_{i}$ is a constant. Then the evidence for the reduction $A_{0}\to^{*}A_{n}$ would be $\lambda\alpha.(\kappa_{n}\ ...\ (\kappa_{0}\ \alpha)\ ...):A_{0}\Rightarrow A_{n}$. Informally, we can see that the evidence $\lambda\alpha.(\kappa_{n}\ ...\ (\kappa_{0}\ \alpha)\ ...)$ grows outward as the number $n$ gets larger. When the reduction is nonterminating, it would be difficult to observe the very first step of the reduction ($\kappa_{0}$). Fortunately, this difficulty can be overcome by representing $l\to r$ as $r\Rightarrow l$. Thus we have the evidence $\lambda\alpha.(\kappa_{0}\ ...\ (\kappa_{n}\ \alpha)\ ...):A_{n}\Rightarrow A_{0}$, with $\kappa_{i}:A_{i+1}\Rightarrow A_{i}$ for all $0\leq i\leq n$. So we can easily observe the first step of the reduction $\kappa_{0}$ at the outermost position.

Next, we need to model the reduction context in rewriting. Given a rewrite rule $l\to r$, we have a one-step reduction $C[l]\to C[r]$ for any first-order term context $C$. Inspired by Leibniz equality, we use the type $\forall p.p\ r\Rightarrow p\ l$ to model the rewrite rule $l\to r$. The intended reading for this type is that $l$ can be replaced by $r$ under any first-order term context $p$. Note that $p$ is a second-order type variable of kind $*\Rightarrow*$. So we can obtain $C[r]\Rightarrow C[l]$ by instantiating $p$ with $\lambda x.C[x]$ in $\forall p.p\ r\Rightarrow p\ l$. This motivates our definition of Leibniz representation for the rewrite rules in Section 3 and the use of the type system $\mathbf{F}_{2}^{\mu}$, as its kind system enforces that one can only instantiate type variable of kind $*\Rightarrow*$ with a type that represents a term context.

Last but not least, we need a mechanism to handle the nonterminating reductions. Consider the cycling rewrite rules: $A\to B$ and $B\to A$, which are represented as two axioms $\Gamma=\kappa_{A}:B\Rightarrow A,\kappa_{B}:A\Rightarrow B$. There is a cyclic reduction for $A$: $A\to B\to A\to B\to...$. Using the Leibniz representation, the corresponding proof evidence for this reduction would be an infinite proof evidence $\kappa_{A}\ (\kappa_{B}\ (\kappa_{A}\ (\kappa_{B}\ ...\ )))$. But we want to use a finite evidence $e$ to represent this nonterminating reduction. The solution here is to use a fixpoint operator. We can represent the infinite proof evidence finitely as $\mu\alpha.\kappa_{A}\ (\kappa_{B}\ \alpha)$, where the $\mu$ is a fixpoint binder with the operational meaning of $\mu\alpha.e\leadsto[\mu\alpha.e/\alpha]e$. This motivates the following fixed point typing rule for $\mathbf{F}_{2}^{\mu}$.

[TABLE]

So $\Gamma\vdash\mu\alpha.\kappa_{A}\ (\kappa_{B}\ \alpha):A$ represents a nonterminating reduction of the shape $A\to B\to A\to B\to...$, since the unfolding of the evidence $\mu\alpha.\kappa_{A}\ (\kappa_{B}\ \alpha)$ gives the sequence of rules that we are going to apply. Note that not all evidence of type $A$ are representing nonterminating reductions. For example, according to the typing rule Mu, we have $\Gamma\vdash\mu\alpha.\alpha:A$, but $\mu\alpha.\alpha$ does not give any information to reconstruct a nonterminating reduction. We show in Section 4 that only the hereditary head normalizing evidence are representing the nonterminating reductions.

We conclude this section by recasting our idea in the following example.

Example 2.1**.**

Consider the following rewrite rule.

$F\ x\to G\ (F\ (G\ x))$**

The term $F\ x$ admits a reduction sequence $F\ x\to G\ (F\ (G\ x))\to G^{2}\ (F\ (G^{2}\ x))\to G^{3}\ (F\ (G^{3}\ x))\to...$, where $G^{i}\ x$ is a shorthand for $\underbrace{G\ (G\ ...(G}_{i}\ x)...)$ for any $i>1$. Using the Leibniz representation, the rewrite system is represented by the following $\mathbf{F}_{2}^{\mu}$ environments:

$\Delta=F:*\Rightarrow*,G:*\Rightarrow*$**

$\Gamma=\kappa:\forall p.\forall x.p\ (G\ (F\ (G\ x)))\Rightarrow p\ (F\ x)$**

Note that $\kappa:\forall p.\forall x.p\ (G\ (F\ (G\ x)))\Rightarrow p\ (F\ x)$ corresponds to the rewrite rule $F\ x\to G\ (F\ (G\ x))$, where $p$ of kind $*\Rightarrow*$ corresponds to a reduction context.

We will first construct a hereditary head normalizing (productive) evidence $e$ such that $\Gamma\vdash e:F\ x$. Then we will show how to check whether such $e$ is indeed representing the nonterminating reduction above. It is enough to derive $\Gamma\vdash e^{\prime}:\forall p.\forall x.p\ (F\ x)$ for some $e^{\prime}$. Consider the following judgement.

(1) $\Gamma,\alpha:\forall p.\forall x.p\ (F\ x)\vdash\lambda p.\lambda x.\alpha\ (\lambda y.p\ (G\ y))\ (G\ x):\forall p.\forall x.p\ (G\ (F\ (G\ x)))$

In (1), we instantiate the type of $\alpha$ as follows: $p$ is instantiated by $\lambda y.p\ (G\ y)$ and $x$ is instantiated by $G\ x$. Since we know that $(\lambda y.p\ (G\ y))\ (F\ (G\ x))=p\ (G\ (F\ (G\ x)))$, thus $\alpha\ (\lambda y.p\ (G\ y))\ (G\ x)$ has the type $p\ (G\ (F\ (G\ x)))$. The lambda-abstractions $\lambda p.\lambda x.$ is used to quantify over $p$ and $x$ in the type of $\alpha\ (\lambda y.p\ (G\ y))\ (G\ x)$.

From $\forall p.\forall x.p\ (G\ (F\ (G\ x)))\Rightarrow p\ (F\ x)$ and $\forall p.\forall x.p\ (G\ (F\ (G\ x)))$, we can deduce the following.

(2) $\Gamma,\alpha:\forall p.\forall x.p\ (F\ x)\vdash\lambda p.\lambda x.\kappa\ p\ x\ (\alpha\ (\lambda y.p\ (G\ y))\ (G\ x)):\forall p.\forall x.p\ (F\ x)$

We now can apply Mu rule to (2) and obtain the following:

(3) $\Gamma\vdash e^{\prime}\equiv\mu\alpha.\lambda p.\lambda x.\kappa\ p\ x\ (\alpha\ (\lambda y.p\ (G\ y))\ (G\ x)):\forall p.\forall x.p\ (F\ x)$

Thus by instantiation we have $\Gamma\vdash e^{\prime}\ (\lambda y.y)\ x:F\ x$. Observe the following unfolding of $e^{\prime}\ (\lambda y.y)\ x$ (we use beta-reduction and $\mu\alpha.e\leadsto[\mu\alpha.e/\alpha]e$ to perform reduction):

e^{\prime}\ (\lambda y.y)\ x\leadsto^{*}\hbox{\pagecolor{light-gray}\kappa\ (\lambda y.y)\ x}\ (e^{\prime}\ (\lambda y.G\ y)\ (G\ x))\leadsto^{*}\kappa\ (\lambda y.y)\ x\ (\hbox{\pagecolor{light-gray}\kappa\ (\lambda y.G\ y)\ (G\ x)}\ (e^{\prime}\ (\lambda y.G\ (G\ y))\ (G\ (G\ x))))\leadsto^{*}...**

As $\kappa$ takes a reduction context and an instantiation as its first two arguments, the gray subterms $\kappa\ (\lambda y.y)\ x$ and $\kappa\ (\lambda y.G\ y)\ (G\ x)$ can be read as: the first step of the reduction for $F\ x$ is under the empty context $\bullet$ using $\kappa$ with the instantation $[x/x]$. The second step is also using the $\kappa$ rule, reducing the redex under the term context $G\ \bullet$, with the instantiation $[G\ x/x]$. As $e^{\prime}\ (\lambda y.y)\ x$ is hereditary head normalizing (productive), the exact reduction information for $F\ x$ can be obtained from the unfolding.

With the help of the prototype type checker for $\mathbf{F}_{2}^{\mu}$, the construction of the fully annotated evidence $e^{\prime}\ (\lambda y.y)\ x$ can be semi-automated. For this example, the user will need to provide the following.

K : forall p x . p (G (F (G x))) => p (F x) h : forall p x . p (F x) h = K h e : F x e = h *

The corecursive equation h = K h can be viewed as a proof sketch for

forall p x . p (F x)**, it reflects the observation that the rule K is repeatedly applied in the reduction for F x. The declaration e : F x = h means that in this case we are providing an evidence for the nonterminating reduction of the term F x under the empty term context. The type checker will try to fill in the exact term contexts and instantiations using the type checking algorithm we developed. It gives the following output (no existing first-order type checking algorithm can type check the above code).

e : F x = h (\ x1’ . x1’) x h : forall p x . p (F x) = \ p0’ x1’. K (\ m1’ . p0’ m1’) x1’ (h (\ m1’ . p0’ (G m1’)) (G x1’)) *

3 Modeling First-order Term Rewriting System in $\mathbf{F}_{2}^{\mu}$

To model term rewriting, we define the type system $\mathbf{F}_{2}^{\mu}$, which restricts the type abstraction of $\mathbf{F}_{\omega}$ [11] to second-order. We define Leibniz representation of rewrite rules (Definition 3.15) and show how it can model rewriting via Theorem 3.16.

Definition 3.1** (Syntax of $\mathbf{F}_{2}^{\mu}$).**

[TABLE]

Note that $\kappa$ denotes an evidence constant and is used to label rewrite rules (see Definition 3.15). The letters such as $F,G$ is used to denote constant types. We use letters such as $\alpha,\beta$ to denote evidence variables, and $x,y$ to denote type variables. We use $\lambda x.e$ to denote type-abstraction on the evidence. Fixed point abstraction $\mu$ in $\mu\alpha.e$ binds the variable $\alpha$ in $e$. Operationally, $\mu\alpha.e$ behaves in the same was as the lambda term $\mathbf{Y}\ (\lambda\alpha.e)$, where $\mathbf{Y}$ is a fixpoint combinator. In our paper $\mu f.\lambda\alpha_{1}....\lambda\alpha_{n}.e$ is also represented by the corecursive equation $f\ \alpha_{1}\ ...\ \alpha_{n}=e$. We use $\forall\underline{x}.T$ as a shorthand for $\forall x_{1}....\forall x_{n}.T$, and $e\ \underline{e^{\prime}}$ for $e\ e_{1}^{\prime}\ ...\ e_{n}^{\prime}$, where the number $n$ is not important.

We distinguish two notions of kinds: kind $o$ is intended to classify types that are of formula nature, while kind $K$ is intended to classify types that are of first-order term nature. Observe that we only allow quantification over the variables of kind $K$ for a type. We use $*^{n}\Rightarrow*$ as a shorthand for $\underbrace{*\Rightarrow...\Rightarrow*}_{n}\Rightarrow*$.

Comparing to $\mathbf{F}_{\omega}$, the following kinding rules of $\mathbf{F}_{2}^{\mu}$ restrict the level of type abstraction to second-order, and stratify the types into two kinds.

Definition 3.2** (Kinding Rules).**

$\Delta\vdash T:k$**

[TABLE]

We use $(x|F:K)\in\Delta$ to abbreviate $x:K\in\Delta$ or $F:K\in\Delta$. And $\Delta\vdash T:o|*$ means $\Delta\vdash T:o$ or $\Delta\vdash T:*$. The kinding rule for $\lambda x.T$ is relevant, i.e. the lambda bound variable $x$ must be used in $T$. We have this requirement is because we want types of kind $*\Rightarrow*$ to represent a first-order term context with at least a hole, as the proof of Theorem 4.8 needs this. Given an environment $\Delta$, it is decidable whether a type $T$ is well-kinded. Given a type $T$, it is also decidable to check if there is a $\Delta$ such that $\Delta\vdash T:k$ for some kind $k$. We use $\forall x.T$ instead of $\forall x:K.T$ in our examples. The kind system allows us to separate two different kinds of types in $\mathbf{F}_{2}^{\mu}$: types that will be used to represent first-order terms and types that allow variable instantiation and modus ponens.

Definition 3.3**.**

We define a reduction relation $T\to_{o}T^{\prime}$ on types, it is the compatible closure of type level beta reduction $(\lambda x.T)\ T^{\prime}\to_{o}[T^{\prime}/x]T$.

Proposition 3.4**.**

If $\Delta\vdash T:k$, then $T$ is strongly normalizing with respect to $\to_{o}$, and $\to_{o}$ is confluent.

Let $\mathrm{FV}(T)$ denote the set of free variables occuring in $T$. The following theorem shows that the kind system satisfies the subject reduction property and the set of free type variables is invariant under the $\to_{o}$-reduction.

Theorem 3.5** (Subject Reduction for Kinding).**

If $\Delta\vdash T:k$ and $T\to_{o}T^{\prime}$, then $\mathrm{FV}(T)=\mathrm{FV}(T^{\prime})$ and $\Delta\vdash T^{\prime}:k$.

Definition 3.6** (Second-order Types).**

A type $T$ is flat iff it is one of the following forms: (1) $T\equiv x$ or $T\equiv F$. (2) $T\equiv T_{1}\ T_{2}$, where $T_{1},T_{2}$ are flat. We say a type $T$ is second-order if $T$ is flat or $T\equiv\lambda x_{1}....\lambda x_{n}.T^{\prime}$, where $T^{\prime}$ is flat and $x_{i}\in\mathrm{FV}(T^{\prime})$ forall $x_{i}\in\{x_{1},...,x_{n}\}$.

Note that types such as $\lambda x.F\ x\ x$, $\lambda x.\lambda y.F\ x\ y,\lambda x.x$ are second-order, but $\lambda x.\lambda y.F\ x\Rightarrow F\ y$ are not second-order. We use second-order types to model both first-order term contexts and terms. The following theorem shows that the kind system stratifies types into two kinds.

Theorem 3.7** (Properties of Kinding).**

If $\Delta\vdash T:o$, then $T$ is of the form $\forall x.T^{\prime}$ or $T_{1}\Rightarrow T_{2}$. 2. 2.

If $\Delta\vdash T:*^{n}\Rightarrow*$, then the $\to_{o}$-normal form of $T$ is second-order.

We define reduction rules for the evidence in the following.

Definition 3.8** (Evidence Reduction).**

Head reduction context $\mathcal{H}\ ::=\ \bullet\ |\ \mathcal{H}\ e\ |\ \lambda\alpha.\mathcal{H}\ |\ \lambda x.\mathcal{H}$

*General reduction context $\mathcal{C}\ ::=\ \bullet\ |\ \mathcal{C}\ e\ |\ \mathcal{C}\ T\ |\ \lambda\alpha.\mathcal{C}\ |\ \lambda x.\mathcal{C}\ |\ e\ \mathcal{C}\ |\ \mu\alpha.\mathcal{C}$ *

$\mathcal{H}[\mu\alpha.e]\leadsto_{h}\mathcal{H}[[\mu\alpha.e/\alpha]e]\quad\mathcal{H}[(\lambda\alpha.e)\ e^{\prime}]\leadsto_{h}\mathcal{H}[[e^{\prime}/\alpha]e]\quad\mathcal{C}[(\lambda x.e)\ T]\leadsto_{\tau}\mathcal{C}[[T/x]e]$**

$\mathcal{C}[\mu\alpha.e]\leadsto_{\mu}\mathcal{C}[[\mu\alpha.e/\alpha]e]\quad\mathcal{C}[(\lambda\alpha.e)\ e^{\prime}]\leadsto_{\beta}\mathcal{C}[[e^{\prime}/\alpha]e]$*  $\mathcal{C}[T]\leadsto_{o}\mathcal{C}[T^{\prime}]$ if $T\to_{o}T^{\prime}$*

We call the one step reduction $\leadsto_{h}\cup\leadsto_{\tau}\cup\leadsto_{o}$ a one step head reduction333This definition is following Barendregt [3], Page 173., denoted by $\leadsto_{h\tau o}$. The head reduction is lazy, i.e., $\mu\alpha.\kappa\ \alpha$ is normalizing with head reduction. We call an evidence a head normal form if it can not be one step reduced by $\leadsto_{h\tau o}$.

Theorem 3.9**.**

$\leadsto_{\beta\mu\tau o}$* and $\leadsto_{h\tau o}$ are confluent, and $\leadsto_{\tau}$ is strongly normalizing.*

We specify the typing rules for $\mathbf{F}_{2}^{\mu}$ in the following.

Definition 3.10** (Typing of $\mathbf{F}_{2}^{\mu}$).**

[TABLE]

In the Abs rule, only the types of kind $K$ are quantified. We use $\mathrm{FV}(\Gamma)$ to denote the set of free type variables occurs in $\Gamma$. We require that all the types are well-kinded. Since $\to_{o}$ is strongly normalizing and confluent, we will work with types in $\to_{o}$-normal form in this paper. The rule Conv is used implicitly.

The followings theorems shows that the type system $\mathbf{F}_{2}^{\mu}$ has the usual inversion and subject reduction properties.

Theorem 3.11** (Selected Inversion Theorems).**

If $\Gamma\vdash e\ e^{\prime}:T$, then $\Gamma\vdash e:T_{1}\Rightarrow T_{2}$, $\Gamma\vdash e^{\prime}:T_{1}$ and $T_{2}\leftrightarrow_{o}^{*}T$. 2. 2.

If $\Gamma\vdash e\ T_{1}:T$, then $\Gamma\vdash e:\forall x:K.T^{\prime}$ and $[T_{1}/x]T^{\prime}\leftrightarrow_{o}^{*}T$.

Theorem 3.12** (Subject Reduction).**

If $\Gamma\vdash e:T$ and $e\leadsto_{h\tau o}e^{\prime}$, then $\Gamma\vdash e^{\prime}:T$.

Due to Mu rule, $\mathbf{F}_{2}^{\mu}$ allows diverging evidence with respect to $\leadsto_{\beta\mu}$. We will focus on the hereditary head normalizing evidence (Definition 4.2), which will be discussed in Section 4.

Definition 3.13** (Terms and Contexts).**

First-order term $t,l,r\ ::=\ x\ |\ F^{n}\ t_{1}\ ...\ t_{n}$

Term context $C\ ::=\ \bullet\ |\ x\ |\ F^{n}\ C_{1}\ ...\ C_{n}$

Note that the term context can contains multiple $\bullet$ and we use the the notation $C[t_{1},...,t_{n}]$ to denote the result of replacing $\bullet$ from left to right in $C$ by $t_{1},...,t_{n}$. A special case is $C[t]$, it means there is exactly one $\bullet$ in $C$, which is replaced by $t$. The function symbol $F$ of arity $n$ is denoted by $F^{n}$. We work with applicative first-order terms in this paper, and we assume all function symbols are fully applied, thus we often write $F\ t_{1}\ ...\ t_{n}$ instead of $F^{n}\ t_{1}\ ...\ t_{n}$. We reuse $\mathrm{FV}(t)$ to mean the set of free variables in $t$.

Definition 3.14** (Rewrite Rules).**

Suppose $l$ and $r$ are first-order terms, where $l$ is not a variable and $\mathrm{FV}(r)\subseteq\mathrm{FV}(l)$, then $l\to r$ is a first-order rewrite rule. A rewriting system is a set $\mathcal{R}$ of rewrite rules. We write $C[t]\to C[t^{\prime}]$ if there exists $l\to r\in\mathcal{R}$ such that $\sigma l\equiv t$ and $\sigma r\equiv t^{\prime}$ for some substitution $\sigma$.

Important Notation Convention. We use the notation $t$ to denote a first-order type in $\mathbf{F}_{2}^{\mu}$ that represents the first-order term $t$. The term context $C$ containing one $\bullet$ can be represented as $\lambda x.C[x]$, a second-order type of kind $*\Rightarrow*$ in $\mathbf{F}_{2}^{\mu}$. We use letters $F,G,D,S,Z$ to denote type constants as well as function symbols. Note that for any first-order term $t$, it is always a well-kinded first-order type, since for any function symbol $F^{n}$ in $t$, we can assign the kind $*^{n}\Rightarrow*$ for $F$ and first-order term variable is of kind $*$. The following definition illustrates our use of this notation convention.

Definition 3.15** (Leibniz representation).**

Given a set of rewrite rules $\mathcal{R}$, we define the Leibniz representation of $\mathcal{R}$ as $\mathbf{F}_{2}^{\mu}$-environments $\Gamma_{\mathcal{R}},\Delta_{\mathcal{R}}$, as follows:

• •

$\kappa:\forall p.\forall\underline{x}.p\ r\Rightarrow p\ l\in\Gamma_{\mathcal{R}}$* whenever $l\to r\in\mathcal{R}$, and where $\kappa$ is a fresh evidence constant and $\underline{x}$ are the free variables in $l$.*

• •

$F:*^{n}\Rightarrow*\in\Delta_{\mathcal{R}}$* if $F^{n}$ is a function symbol in $\mathcal{R}$.*

Leibniz representation allows us to represent a first-order term rewriting system as a typing environment in $\mathbf{F}_{2}^{\mu}$, together with the typing rules, finite reductions can be represented by a typing judgement in $\mathbf{F}_{2}^{\mu}$.

Theorem 3.16**.**

Let $\mathcal{R}$ be a set of rewrite rules.

If $C[t]\to C[t^{\prime}]$ by $l\to r\in\mathcal{R}$, then $\Gamma_{\mathcal{R}}\vdash e:C[t^{\prime}]\Rightarrow C[t]$ for some $e$. 2. 2.

If $t_{1}\to t_{2}\to t_{3}$ is a reduction using $\mathcal{R}$, then $\Gamma_{\mathcal{R}}\vdash e:t_{3}\Rightarrow t_{1}$ for some $e$.

Proof 3.17**.**

By Definition 3.15, we have $\kappa:\forall p.\forall\underline{x}.p\ r\Rightarrow p\ l\in\Gamma_{\mathcal{R}}$. We instantiate $p$ with $\lambda y.C[y]$, by rule Conv, we get $\Gamma_{\mathcal{R}}\vdash\kappa\ (\lambda y.C[y]):\forall\underline{x}.C[r]\Rightarrow C[l]$. Since $\sigma l\equiv t,\sigma r\equiv t^{\prime}$, let $\underline{t}$ be the codomain of $\sigma$, we have $\Gamma_{\mathcal{R}}\vdash\kappa\ \ (\lambda y.C[y])\ \underline{t}:C[t^{\prime}]\Rightarrow C[t]$. 2. 2.

By (1), we have $\Gamma_{\mathcal{R}}\vdash e_{1}:t_{2}\Rightarrow t_{1}$ and $\Gamma_{\mathcal{R}}\vdash e_{2}:t_{3}\Rightarrow t_{2}$, so $\Gamma_{\mathcal{R}}\vdash\lambda\alpha.e_{1}\ (e_{2}\ \alpha):t_{3}\Rightarrow t_{1}$.

4 Hereditary Head Normalization and Faithfulness

In this section we define the hereditary head normalization for an evidence (Definition 4.2). The role of hereditary head normalization is similar to productivity, i.e. a hereditary head normalizing evidence can be associated with a computational tree (Böhm tree without bottom [3]). In $\mathbf{F}_{2}^{\mu}$, hereditary head normalization implies faithfulness. Informally, an evidence is faithful if we can recover a nonterminating reduction from it.

To define hereditary head normalization, we first define an erasure that maps $\mathbf{F}_{2}^{\mu}$-evidence to pure lambda term with fixed point operator.

Definition 4.1** (Erasure).**

We define erasure $|\cdot|$ on evidence as follows.

|\alpha|=\alpha\quad|\kappa|=\kappa\quad|\lambda\alpha.e|=\lambda\alpha.|e|\quad|\mu\alpha.e|=\mu\alpha.|e|\quad|e\ e^{\prime}|=|e|\ |e^{\prime}|\quad\hbox{\pagecolor{light-gray}|\lambda x.e|=|e|}\quad\hbox{\pagecolor{light-gray}|e\ T|=|e|}* *

We call the erased evidence $|e|$ Curry-style evidence. The following definition follows the same formulation by Raffalli [17] and Tatsuta [21].

Definition 4.2** (Hereditary Head Normalization).**

Let $\Lambda$ be the set of Curry-style evidence. We say $e$ is hereditary head normalizing (denoted by $e\in\mathrm{HHN}$) iff $|e|\in\mathrm{HN}_{n}$ for all $n\geq 0$. We define $\mathrm{HN}_{n}$ as follows.

• •

$e\in\mathrm{HN}_{0}$* iff $e\in\Lambda$.*

• •

$e\in\mathrm{HN}_{n+1}$* iff $e\leadsto_{\beta\mu}^{*}\lambda\underline{\alpha}.e^{\prime}\ e_{1}\ ...\ e_{m}$, where $e^{\prime}$ is a variable or a constant and $e_{i}\in\mathrm{HN}_{n}$ for all $i$.*

We are going to show in Theorem 4.8 that if $\Gamma_{\mathcal{R}}\vdash e:t$ in $\mathbf{F}_{2}^{\mu}$ and $e$ is hereditary head normalizing, then we can reconstruct a nonterminating reduction of $t$ by following the unfolding of $e$. First we define the notion of trace. The position of a trace is described as follows: Let $o$ denote the origin of a trace and $s\cdot m$ denote the next position after $m$. For a trace $\mathcal{T}$, we use $\mathcal{T}_{m}$ to refer to the node at position $m$ in the trace. The following formalization of evidence trace is a degenerate case of Böhm tree ([4], [3, §10]).

Definition 4.3** (Evidence Trace).**

Suppose $e\leadsto_{h\tau o}^{*}\kappa\ T_{1}...\ T_{n}\ e^{\prime}$, with $T_{1},...,T_{n}$ in $\to_{o}$-normal form. The evidence trace of $e$, denoted by $[e]$, is defined as:

• •

$[e]_{o}=\kappa\ T_{1}...\ T_{n}$.

• •

$[e]_{s\cdot m}=[e^{\prime}]_{m}$.

In the above definition, since $\kappa\ T_{1}...\ T_{n}\ e^{\prime}$ is a head normal form, by the confluence of $\leadsto_{h\tau o}$ (Theorem 3.9), we know that $[e]$ is referring to at most one trace. When $e\not\leadsto_{h\tau o}^{*}\kappa\ T_{1}...\ T_{n}\ e^{\prime}$, we say $[e]$ is undefined. For an example of finite evidence trace, consider $e\equiv\kappa\ (\lambda y.y)\ (\kappa^{\prime}\ (\lambda y.y))$, in this case $[e]_{o}=\kappa\ (\lambda y.y),[e]_{s\cdot o}=\kappa^{\prime}\ (\lambda y.y)$. For an example of an infinite evidence trace, consider $e\equiv\mu\alpha.\kappa\ (\lambda y.y)\ \alpha$, we have $[e]_{m}=\kappa\ (\lambda y.y)$ for any position $m$.

Intuitively, an evidence trace can be viewed as a sequence of instructions (in the form of evidence constants) that we are going to follow in order to rewrite a term. The following definitions of action and faithful action on a first-order term reflects this intuition. Suppose $C[\sigma l,...,\sigma l]\to^{*}C[\sigma r,...,\sigma r]$ by $l\to r\in\mathcal{R}$. We record the term context and the instantiation information along the reduction, i.e. $C[\sigma l,...,\sigma l]\to_{(\kappa,C,\sigma)}^{*}C[\sigma r,...,\sigma r]$.

Definition 4.4** (Action on First-Order Term).**

Suppose $[e]_{m}=\kappa\ (\lambda x.C[x,...,x])\ t_{1}...\ t_{n}$ for some position $m$ and $\kappa:\forall p.\forall\underline{x}.p\ r\Rightarrow p\ l$. An action of $[e]_{m}$ on the first-order term $t$ (denoted by $[e]_{m}(t)$) is defined as follows.

• •

$[e]_{m}(t)=t^{\prime}$* if $t\to_{(\kappa,C,\sigma)}^{*}t^{\prime}$, where $\sigma=[t_{1}/x_{1},...,t_{n}/x_{n}]$.*

• •

otherwise $[e]_{m}(t)$ is undefined.

Note that we write $t\to^{*}[e]_{m}(t)$ when $[e]_{m}(t)$ is defined. The following definition of faithful action shows how one follows a potentially infinite evidence trace to reduce a term.

Definition 4.5** (Faithful Action).**

The evidence trace $[e]$ acts on $t$ faithfully, if we have a reduction sequence $t\to^{*}[e]_{o}(t)\to^{*}[e]_{s\cdot o}([e]_{o}(t))\to^{*}[e]_{s\cdot s\cdot o}([e]_{s\cdot o}([e]_{o}(t)))\to^{*}...\to^{*}[e]_{m}(...[e]_{o}(t)...)$ for any position $m$.

Example 4.6**.**

To illustrate the intuition behind Definitions 4.3, 4.4, 4.5, let us consider the one rule rewriting system: $F\ x\to G\ (F\ (G\ x))$ in Example 2.1. The Leibniz representation is $\Delta=F:*\Rightarrow*,G:*\Rightarrow*,\Gamma=\kappa:\forall p.\forall x.p\ (G\ (F\ \ (G\ x)))\Rightarrow p\ (F\ x)$. Recall that we had the following judgement.

(1) $\Gamma\vdash e^{\prime}\equiv\mu\alpha.\lambda p.\lambda x.\kappa\ p\ x\ (\alpha\ (\lambda y.p\ (G\ y))\ (G\ x)):\forall p.\forall x.p\ (F\ x)$

*(2) $\Gamma\vdash e^{\prime}\ (\lambda y.y)\ x:F\ x$

---

We observed the following unfolding of $e^{\prime}\ (\lambda y.y)\ x$ (below $\mathcal{C}\equiv\kappa\ (\lambda y.y)\ x\ (\kappa\ (\lambda y.G\ y)\ (G\ x)\ \bullet)$):

e^{\prime}\ (\lambda y.y)\ x\leadsto_{\beta\mu\tau o}^{*}\hbox{\pagecolor{light-gray}\kappa\ (\lambda y.y)\ x}\ (e^{\prime}\ (\lambda y.G\ y)\ (G\ x))\leadsto_{\beta\mu\tau o}^{*}\kappa\ (\lambda y.y)\ x\ (\hbox{\pagecolor{light-gray}\kappa\ (\lambda y.G\ y)\ (G\ x)}\ (e^{\prime}\ (\lambda y.G\ (G\ y)))\ (G\ (G\ x)))\leadsto_{\beta\mu\tau o}^{*}\mathcal{C}[(\hbox{\pagecolor{light-gray}\kappa\ (\lambda y.G\ (G\ y))\ (G\ (G\ x))}\ (e^{\prime}\ (\lambda y.G\ (G\ (G\ y))))\ (G\ (G\ (G\ x))))]\leadsto_{\beta\mu\tau o}^{*}...**

It gives rise to the following evidence trace: $[e]_{o}=\kappa\ (\lambda y.y)\ x$, $[e]_{s\cdot o}=\kappa\ (\lambda y.G\ y)\ (G\ x)$, $[e]_{s\cdot s\cdot o}=\kappa\ (\lambda y.G\ (G\ y))\ (G\ (G\ x))$, etc. Moreover $[e]$ acts faithfully on $F\ x$ (by Theorem 4.8). For example, we observe that $F\ x\to[e]_{o}(F\ x)\to[e]_{s\cdot o}([e]_{o}(F\ x))\to[e]_{s\cdot s\cdot o}([e]_{s\cdot o}([e]_{o}(F\ x)))$, which is the following reduction trace.

$F\ x\to_{(\kappa,\bullet,[x/x])}G\ (F\ (G\ x))\to_{(\kappa,G\ \bullet,[(G\ x)/x])}G\ (G\ (F\ (G\ (G\ x))))\to_{(\kappa,G\ (G\ \bullet),[(G\ (G\ x))/x])}G\ (G\ (G\ (F\ (G\ (G\ (G\ x))))))$**

Lemma 4.7**.**

Suppose $\Gamma_{\mathcal{R}}\vdash e:t$ for some first-order term $t$ and $e$ is head normalizing. We have $e\leadsto_{h\tau o}^{*}\kappa\ (\lambda x.C[x,...,x])\ t_{1}...\ t_{n}\ e^{\prime}$ for some $\kappa:\forall p.\forall\underline{x}.p\ r\Rightarrow p\ l\in\Gamma_{\mathcal{R}}$. Furthermore, we have $\Gamma_{\mathcal{R}}\vdash e^{\prime}:C[\sigma r,...,\sigma r]$ and $C[\sigma l,...,\sigma l]=t$, where $\mathrm{codom}(\sigma)=\{t_{1},...,t_{n}\}$ and $\mathrm{dom}(\sigma)=\mathrm{FV}(l)$.

Theorem 4.8** (Faithfulness of Corecursive Evidence).**

Suppose $\Gamma_{\mathcal{R}}\vdash e:t$ in $\mathbf{F}_{2}^{\mu}$ and $e\in\mathrm{HHN}$. We have $t\to^{*}[e]_{o}(t)\to^{*}...\to^{*}[e]_{m}(...[e]_{o}(t)...)$ for any position $m$, i.e. $e$ acts faithfully on $t$.

Proof 4.9**.**

By Lemma 4.7, we know that $e\leadsto_{h\tau o}^{*}\kappa\ (\lambda x.C[x,...,x])\ t_{1}...\ t_{n}\ e^{\prime}$ for some $\kappa:\forall p.\forall\underline{x}.p\ r\Rightarrow p\ l$, $\Gamma_{\mathcal{R}}\vdash e^{\prime}:C[\sigma r,...,\sigma r]$, $C[\sigma l,...,\sigma l]=t$, where $\mathrm{codom}(\sigma)=\{t_{1},...,t_{n}\}$ and $\mathrm{dom}(\sigma)=\mathrm{FV}(l)$. Thus $t=C[\sigma l,...,\sigma l]\to_{(\kappa,C,\sigma)}^{*}\ C[\sigma r,...,\sigma r]$. We prove the theorem by induction on $m$.

• •

$m=o$. We have $[e]_{o}=\kappa\ (\lambda x.C[x,...,x])\ t_{1}...\ t_{n}$, since $t\to_{(\kappa,C,\sigma)}^{*}\ C[\sigma r,...,\sigma r]$, so $t\to^{*}[e]_{o}(t)$.

• •

$m=s\cdot m^{\prime}$. We need to show $t\to^{*}[e]_{o}(t)\to^{*}...\to^{*}[e]_{s\cdot m^{\prime}}(...[e]_{o}(t)...)$. Since $\Gamma_{\mathcal{R}}\vdash e^{\prime}:C[\sigma r,...,\sigma r]$ and $e^{\prime}\in\mathrm{HHN}$, by IH, we have $C[\sigma r,...,\sigma r]\to^{*}[e^{\prime}]_{o}(C[\sigma r,...,\sigma r])\to^{*}...\to^{*}[e^{\prime}]_{m^{\prime}}(...[e^{\prime}]_{o}(C[\sigma r])...)$. Thus $t\to^{*}[e]_{o}(t)=C[\sigma r,...,\sigma r]\to^{*}[e^{\prime}]_{o}([e]_{o}(t))\to^{*}...\to^{*}[e^{\prime}]_{m^{\prime}}(...[e^{\prime}]_{o}([e]_{o}(t))...)$. Since $[e^{\prime}]_{a}=[e]_{s\cdot a}$ for any position $a$, we have $t\to^{*}[e]_{o}(t)\to^{*}[e]_{s\cdot o}([e]_{o}(t))\to^{*}...\to^{*}[e]_{s\cdot m^{\prime}}(...[e]_{s\cdot o}([e]_{o}(t))...)$.

Now we are going to show the hereditary head normalization for $\mathbf{F}_{2}^{\mu}$ is decidable by mapping a typable evidence in $\mathbf{F}_{2}^{\mu}$ to a typable evidence in $\lambda$-Y caculus (simply typed lambda calculus with fixpoint typing rule [19])444Please see Appendix F for full details..

Definition 4.10**.**

We define a function $\theta$ that maps $\mathbf{F}_{2}^{\mu}$ types to $\lambda$-Y types.

$\theta(x|F)=B$*  $\theta(\lambda x.T)=\theta(T)$  $\theta(T\ T^{\prime})=\theta(T)$  $\theta(T\Rightarrow T^{\prime})=\theta(T)\Rightarrow\theta(T^{\prime})$  $\theta(\forall x.T)=\theta(T)$*

We write $\theta(\Gamma)$ to mean applying the function $\theta$ to all the types in $\Gamma$. Type $B$ is the based type in $\lambda$-Y.

Theorem 4.11**.**

If $\Gamma\vdash e:T$ and $\Delta\vdash T:*|o$ in $\mathbf{F}_{2}^{\mu}$, then $\theta(\Gamma)\vdash|e|:\theta(T)$ in $\lambda$-Y.

Theorem 4.11 implies that the hereditary head normalization for $\mathbf{F}_{2}^{\mu}$ is decidable, since it is well-known that hereditary head normalization for $\lambda$-Y is decidable ([5], [18], [13]).

5 Type Checking $\mathbf{F}_{2}^{\mu}$ Based on Resolution with Second-order Matching

Modeling first-order term contexts is one of the reasons we use second-order types. Quantification over second-order type variables also enables us to represent some nonlooping nonterminations in $\mathbf{F}_{2}^{\mu}$.

Example 5.1**.**

Consider the following rewrite rules [10].

$D\ (S\ x)\ y\to_{a}D\ x\ (S\ y)$**

$D\ Z\ y\to_{b}D\ (S\ y)\ Z$**

The term $D\ Z\ Z$ will give rise to the following nonlooping nonterminating reduction, where no cycle or loop can be observed:

$D\ Z\ Z\to_{b}D\ (S\ Z)\ Z\to_{a}D\ Z\ (S\ Z)\to_{b}D\ (S\ (S\ Z))\ Z\to_{a}D\ (S\ Z)\ (S\ Z)\to_{a}D\ Z\ (S\ (S\ Z))\to_{b}D\ (S\ (S\ (S\ Z)))\ Z\to_{a}D\ (S\ (S\ Z))\ (S\ Z)\to_{a}D\ (S\ Z)\ (S\ (S\ Z))\to_{a}D\ Z\ (S\ (S\ (S\ Z)))\to...$*

---

The rule sequence for this reduction exhibits the pattern: “$ba,baa,baaa,...$”, which can be represented by the corecursive function $f\ \alpha\ \beta=(\beta\cdot\alpha)\ (f\ \alpha\ (\beta\cdot\alpha))$(here $\cdot$ denotes functional composition), as $f\ a\ b$ would give rise to the following reduction (we omit the compositional symbols):

$f\ a\ b\leadsto(ba)(f\ a\ (ba))\leadsto(babaa)(f\ a\ (baa))\leadsto(babaabaaa)(f\ a\ (baaa))$**

Let the Leibniz representation of the rewriting system be as follows:

$\Delta=D:*^{2}\Rightarrow*,Z:*,S:*\Rightarrow*$*

$\Gamma=\kappa_{a}:\forall p.\forall x.\forall y.p\ (D\ x\ (S\ y))\Rightarrow p\ (D\ (S\ x)\ y),\kappa_{b}:\forall p.\forall y.p\ (D\ (S\ y)\ Z)\Rightarrow p\ (D\ Z\ y)$***

We would like to provide a type annotation for $f$ such that $\Gamma\vdash f\ \kappa_{a}\ \kappa_{b}:D\ Z\ Z$. But it is not obvious as we cannot type check $f\ \kappa_{a}\ \kappa_{b}$ with $D\ Z\ Z$ using any first-order type checking algorithm (e.g. the one in Haskell). We will show how to type check $f$ using the type checking algorithm we introduce in this section.

By type checking, we mean the following problem: given an environment $\Gamma$, a Curry-style evidence $e$ and a type $T$, construct a fully annotated evidence $e^{\prime}$ such that $\Gamma\vdash e^{\prime}:T$ and $|e^{\prime}|=e$. We use the terminology proof checking to mean the following: given an environment $\Gamma$, a fully annotated evidence $e$ and a type $T$, check if $\Gamma\vdash e:T$. The type checking problem for Curry-style System $\mathbf{F}$ and $\mathbf{F}_{\omega}$ are well-known to be undecidable ([24], [23]). The type system $\mathbf{F}_{2}^{\mu}$ appears to be a much weaker system compared to System $\mathbf{F}$ and $\mathbf{F}_{\omega}$ (HHN is decidable in $\mathbf{F}_{2}^{\mu}$), we will show a type checking algorithm for $\mathbf{F}_{2}^{\mu}$ inspired by SLD-resolution [16]. We will work on types that are kindable by our decidable kind system (Definition 3.2). Moreover, we will consider the following reformulation of type $T$ from Definition 3.1:

[TABLE]

Here $A$ is of kind $*$. We use $T_{1},...,T_{n}\Rightarrow A$ as a shorthand for $T_{1}\Rightarrow...\Rightarrow T_{n}\Rightarrow A$ and we call $A$ the head of $T_{1},...,T_{n}\Rightarrow A$. These types are a generalized version of Horn formulas, called hereditary Harrop formula in the literature [15].

In this section we use $A,B$ to denote a type of kind $*$, and we use $a,b$ to denote a type variable or a type constant. The following definition of second-order matching follows Dowek’s treatment [7] of Huet’s algorithm [14].

Definition 5.2** (Second-order Matching).**

Let $E$ be a set of second-order matching problems $\{A_{1}\mapsto B_{1},...,A_{n}\mapsto B_{n}\}$. The following rules (intended to apply top-down) show how to transform $E$.

[TABLE]

Note that $\bot$ denotes a failure in matching. In the Imi rule, the variables $y_{1},...,y_{m}$ are fresh type variables. The Proj and Imi rules introduce nondeterminism, so there may be multiple matchers for a matching problem $A\mapsto B$. We write $A\mapsto_{\sigma}B$ to mean there is a derivation from $A\mapsto B$ to $\emptyset$ using rules in the above definition with a second-order matcher $\sigma$. The second-order matching is decidable (all derivations are finite using Definition 5.2) and all the resulted matchers are finite, but second-order unification is not decidable [12].

The standard second-order matching algorithm usually generates many vacuous substitutions, we can exclude them by kinding, as we work with kindable types. For example, when we match $d\ Z\ Z$ against $D\ Z\ (S\ Z)$, the second-order matching algorithm would generate matchers such as $[\lambda x.\lambda y.D\ Z\ (S\ Z)/d]$ and $[\lambda x.\lambda y.D\ y\ (S\ y)/d]$, which are not kindable.

Let $T=\forall x_{1}....\forall x_{m}.T_{1},...,T_{n}\Rightarrow A$, the set of variables $\{x_{i}\ |\ x_{i}\notin\mathrm{FV}(A),1\leq i\leq m\}\cup\mathrm{FV}(T)$ are called existential variables. In this section, we work with types that do not have any existential variables, we will show how to handle existential variables in the next section. We use $\Phi$ to denote a set of tuples of the form $(\Gamma,e,T)$. We define resolution by second-order matching as a transition system from $\Phi$ to $\Phi^{\prime}$ as follows:

Definition 5.3** (Resolution by Second-order Matching (RSM)).**

$\Phi\longrightarrow\Phi^{\prime}$**

$\{(\Gamma,(\kappa|\alpha)\ e_{1}\ ...\ e_{n},A),\Phi\}\longrightarrow_{a}\{(\Gamma,e_{1},\sigma T_{1}),...,(\Gamma,e_{n},\sigma T_{n}),\Phi\}$* if $\kappa|\alpha:\forall\underline{x}.T_{1},...,T_{n}\Rightarrow B\in\Gamma$ with $B\mapsto_{\sigma}A$.* 2. 2.

$\{(\Gamma,\lambda\alpha_{1}....\lambda\alpha_{n}.e,T_{1},...,T_{n}\Rightarrow A),\Phi\}\longrightarrow_{i}\{([\Gamma,\alpha_{1}:T_{1},...,\alpha_{n}:T_{n}],e,A),\Phi\}$. 3. 3.

$\{(\Gamma,e,\forall x_{1}...\forall x_{n}.T),\Phi\}\longrightarrow_{\forall}\{(\Gamma,e,T),\Phi\}$. 4. 4.

$\{(\Gamma,\mu\alpha.e,T),\Phi\}\longrightarrow_{c}\{([\Gamma,\alpha:T],e,T),\Phi\}$.

As before, $\kappa|\alpha$ means “$\kappa$ or $\alpha$”. The rule (1) allow the the size of $\{e_{1},...,e_{n}\}$ to be zero. We require the sizes of $\{\alpha_{1},...,\alpha_{n}\}$ and $\{x_{1},...,x_{n}\}$ both to be nonzero for rules (2) and (3). Rule (3) also introduces fresh eigenvariables $\{x_{1},...,x_{n}\}$ for $T$, they behave the same as constants during RSM. In rule (1), when perform matching $B\mapsto_{\sigma}A$, we rename the bound variables $\underline{x}$ in $T_{1},...,T_{n},B$ to fresh variables. The $T$ in the tuple $(\Gamma,e,T)$ intuitively corresponds to the current goal for the resolution and $e$ is a Curry-style evidence that can be understood as a list of instructions for the resolution algorithm. The resolution is defined by case analysis on the Curry-style evidence and the current goal $T$ and it is terminating. If it terminates with the empty set, then we say the resolution succeeds, otherwise it fails. The following theorem shows that if the resolution succeeds, then the type checking succeeds, i.e. we can obtain the corresponding fully annotated evidence.

Theorem 5.4** (Soundness of RSM).**

If $\{(\Gamma,e,T)\}\longrightarrow^{*}\emptyset$, then there exists an evidence $e^{\prime}$ such that $\Gamma\vdash e^{\prime}:T$ in $\mathbf{F}_{2}^{\mu}$ and $|e^{\prime}|=e$.

The proof of Theorem 5.4 gives us an algorithm to compute the annotated evidence $e^{\prime}$. This algorithm is implemented in our prototype.

Example 5.5**.**

Continuing the Example 5.1, let us illustrate how to use RSM to type check the function $f$. Consider the long form of $f$, namely, $f=\mu f.\lambda\alpha.\lambda\beta.\beta(\alpha\ (f\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})\ (\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime})))$ and the Leibniz representation:

$\Delta=D:*^{2}\Rightarrow*,Z:*,S:*\Rightarrow*$**

$\Gamma=\kappa_{a}:\forall p.\forall x.\forall y.p\ (D\ x\ (S\ y))\Rightarrow p\ (D\ (S\ x)\ y),\kappa_{b}:\forall p.\forall y.p\ (D\ (S\ y)\ Z)\Rightarrow p\ (D\ Z\ y)$.**

As we want $\Gamma\vdash f\ \kappa_{a}\ \kappa_{b}:D\ Z\ Z$, the most intuitive type that we can assign to $f$ is the following.

$T\equiv(\forall p.\forall x.\forall y.p\ (D\ x\ (S\ y))\Rightarrow p\ (D\ (S\ x)\ y))\Rightarrow(\forall p.\forall y.p\ (D\ (S\ y)\ Z)\Rightarrow p\ (D\ Z\ y))\Rightarrow D\ Z\ Z$**

But $f$ can not be type checked with $T$ by RSM. The solution is abstracting $D$ to a second-order variable $d$ and assigning the following type to $f$:

$T^{\prime}\equiv\forall d.\underbrace{(\forall p.\forall x.\forall y.p\ (d\ x\ (S\ y))\Rightarrow p\ (d\ (S\ x)\ y))\Rightarrow(\forall p.\forall y.p\ (d\ (S\ y)\ Z)\Rightarrow p\ (d\ Z\ y))\Rightarrow d\ Z\ Z}_{T^{\prime\prime}}$**

This change yields the following successful RSM resolution trace.

$\{(\Gamma,\mu f.\lambda\alpha.\lambda\beta.\beta(\alpha\ (f\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})\ (\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime})))),T^{\prime})\}\longrightarrow_{c}$**

$\{([\Gamma,f:T^{\prime}],\lambda\alpha.\lambda\beta.\beta(\alpha\ (f\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})\ (\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime})))),T^{\prime})\}\longrightarrow_{\forall}$**

\{([\Gamma,f:T^{\prime}],\lambda\alpha.\lambda\beta.\beta(\alpha\ (f\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})\ (\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime})))),[d_{1}/d]T^{\prime\prime})\}\longrightarrow_{i}\{(\Gamma^{\prime\prime},\beta(\alpha\ (f\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})\ (\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime})))),d_{1}\ Z\ Z)\}\longrightarrow_{a}\{(\Gamma^{\prime\prime},\alpha\ (f\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})\ (\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime}))),d_{1}\ (S\ Z)\ Z)\}\longrightarrow_{a}\{(\Gamma^{\prime\prime},f\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})\ (\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime})),d_{1}\ Z\ (S\ Z))\}\hbox{\pagecolor{light-gray}\longrightarrow_{a}}**

$\{(\Gamma^{\prime\prime},\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime},\forall p.\forall x.\forall y.p\ (d_{1}\ x\ (S\ (S\ y)))\Rightarrow p\ (d_{1}\ (S\ x)\ (S\ y))),\Phi_{1}\equiv(\Gamma^{\prime\prime},\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime}),\forall p.\forall y.p\ (d_{1}\ (S\ y)\ (S\ Z))\Rightarrow p\ (d_{1}\ Z\ (S\ y)))\}\longrightarrow_{\forall}$**

$\{(\Gamma^{\prime\prime},\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime},p_{1}\ (d_{1}\ x_{1}\ (S\ (S\ y_{1})))\Rightarrow p_{1}\ (d_{1}\ (S\ x_{1})\ (S\ y_{1}))),\Phi_{1}\}\longrightarrow_{i}$**

$\{([\Gamma^{\prime\prime},\alpha^{\prime}:p_{1}\ (d_{1}\ x_{1}\ (S\ (S\ y_{1})))],\alpha\ \alpha^{\prime},p_{1}\ (d_{1}\ (S\ x_{1})\ (S\ y_{1}))),\Phi_{1}\}\longrightarrow_{a}$**

$\{([\Gamma^{\prime\prime},\alpha^{\prime}:p_{1}\ (d_{1}\ x_{1}\ (S\ (S\ y_{1})))],\alpha^{\prime},p_{1}\ (d_{1}\ x_{1}\ (S\ (S\ y_{1})))),\Phi_{1}\}\longrightarrow_{a}\{(\Gamma^{\prime\prime},\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime}),\forall p.\forall y.p\ (d_{1}\ (S\ y)\ (S\ Z))\Rightarrow p\ (d_{1}\ Z\ (S\ y)))\}\longrightarrow_{\forall}$**

$\{(\Gamma^{\prime\prime},\lambda\alpha^{\prime}.\beta(\alpha\ \alpha^{\prime}),p_{2}\ (d_{1}\ (S\ y_{2})\ (S\ Z))\Rightarrow p_{2}\ (d_{1}\ Z\ (S\ y_{2})))\}\longrightarrow_{i}$**

$\{([\Gamma^{\prime\prime},\alpha^{\prime}:p_{2}\ (d_{1}\ (S\ y_{2})\ (S\ Z))],\beta(\alpha\ \alpha^{\prime}),p_{2}\ (d_{1}\ Z\ (S\ y_{2})))\}\longrightarrow_{a}$**

$\{([\Gamma^{\prime\prime},\alpha^{\prime}:p_{2}\ (d_{1}\ (S\ y_{2})\ (S\ Z))],\alpha\ \alpha^{\prime},p_{2}\ (d_{1}\ (S\ (S\ y_{2}))\ Z))\}\longrightarrow_{a}$**

$\{([\Gamma^{\prime\prime},\alpha^{\prime}:p_{2}\ (d_{1}\ (S\ y_{2})\ (S\ Z))],\alpha^{\prime},p_{2}\ (d_{1}\ (S\ y_{2})\ (S\ Z)))\}\longrightarrow_{a}\emptyset$**

Note that $\Gamma^{\prime\prime}=\Gamma,f:T^{\prime},\alpha:\forall p.\forall x.\forall y.p\ (d_{1}\ x\ (S\ y))\Rightarrow p\ (d_{1}\ (S\ x)\ y),\beta:\forall p.\forall y.p\ (d_{1}\ (S\ y)\ Z)\Rightarrow p\ (d_{1}\ Z\ y)$. At the third $\longrightarrow_{a}$-step, by second-order matching, we instantiate the $d$ in the type of $f$ to $\lambda x.\lambda y.d_{1}\ x\ (S\ y)$. Now that $f$ is typable with $T^{\prime}$, we have $\Gamma\vdash f\ D\ \kappa_{a}\ \kappa_{b}:D\ Z\ Z$. Since the rewriting system is non-overlapping and $f$ is hereditary head normalizing, by Theorem 4.8 we know $f\ D\ \kappa_{a}\ \kappa_{b}$ represents the nonterminating reduction of $D\ Z\ Z$.

Representing nonterminations in general follows the same method as the above example: one first writes down a corecursive function that represents the rule sequence in a nonterminating reduction, and then provides the proper type signature for such function. Once the function is type checked, a finite representation can be obtained. We illustrate how the prototype works for this example and some other challenging examples in the Appendix H, J.

6 RSM Algorithm with Existential Variables

The RSM algorithm in Definition 5.3 fails to type check some judgements in presence of existential variables. In this section, we extend RSM to cope with existential variables. As a result, the nontermination reduction in the Example 1.1 can also be type checked.

We consider the following sequential reduction that simulates the parallel reduction sequence in the Example 1.1. At each reduction step, we underline the chosen redex.

\hbox{\pagecolor{light-gray}\underline{A}}\to_{a}\hbox{\pagecolor{light-gray}\underline{A}B}\to_{a}AB\underline{B}\to_{b}\hbox{\pagecolor{light-gray}\underline{A}BA}\to_{a}AB\underline{B}A\to_{b}ABA\underline{A}\to_{a}\hbox{\pagecolor{light-gray}\underline{A}BAAB}\to_{a}AB\underline{B}AAB\to_{b}ABA\underline{A}AB\to_{a}ABAAB\underline{A}B\to_{a}ABAABAB\underline{B}\to_{b}\hbox{\pagecolor{light-gray}\underline{A}BAABABA}\to_{a}AB\underline{B}AABABA\to_{b}ABA\underline{A}ABABA\to_{a}ABAAB\underline{A}BABA\to_{a}ABAABAB\underline{B}ABA\to_{b}ABAABABA\underline{A}BA\to_{a}ABAABABAAB\underline{B}A\to_{b}ABAABABAABA\underline{A}\to_{a}\hbox{\pagecolor{light-gray}\underline{A}BAABABAABAAB}\to...

Observe that the length of the gray strings grows according to the Fibonacci sequence, and each gray string is a result of concatenation of the previous two.

The rule sequence in the above reduction is “$a,ab,aba,abaab,abaababa$” (each word in the rule sequence is a concatenation of the previous two). We can use the corecursive function $f\alpha\ \beta=\alpha\ (f\ (\alpha\cdot\beta)\ \alpha)$ to generate such sequences.

$f\ a\ b\leadsto a(f\ (ab)\ a)\leadsto(aab)(f\ (aba)\ (ab))\leadsto(aababa)(f\ (abaab)\ (aba))$

We can use a standard method [22] to represent string rewriting systems as first-order term rewriting systems. In this case, the corresponding rules would be $A\ x\to_{a}A\ (B\ x)$ and $B\ x\to_{b}A\ x$. The reduction would begin with $A\ x$. The Leibniz representation for this rewrite system is the following:

$\Delta=A:*\Rightarrow*,B:*\Rightarrow*$

$\Gamma=\kappa_{a}:\forall p.\forall x.p\ (A\ (B\ x))\Rightarrow p\ (A\ x),\kappa_{b}:\forall p.\forall x.p\ (A\ x)\Rightarrow p\ (B\ x)$

To represent the rewriting sequence above, we need to give a type to the function $f$ such that $\Gamma\vdash f\ \kappa_{a}\ \kappa_{b}:A\ x$. The most intuitive type we can assign to the corecursive function $f\alpha\ \beta=\alpha\ (f\ (\alpha\cdot\beta)\ \alpha)$ is the following:

(I) $\forall x.(\forall p_{2}.\forall y_{2}.p_{2}\ (A\ (B\ y_{2}))\Rightarrow p_{2}\ (A\ y_{2}))\Rightarrow(\forall p_{1}.\forall y_{1}.p_{1}\ (A\ y_{1})\Rightarrow p_{1}\ (B\ y_{1}))\Rightarrow A\ x$

Then we would have $\Gamma\vdash f\ x\ \kappa_{a}\ \kappa_{b}:A\ x$. Unfortunately this will not be type checked by RSM (the resolution will fail). We need to perform abstraction on type (I), here we abstract the function symbol $B$ to a functional variable $b:*\Rightarrow*$, and $A$ to a functional variable $a:*\Rightarrow*$, obtaining the following type for $f$.

(II) T\equiv\forall{a}.\forall b.\forall x.\underbrace{(\forall p.\forall y.p\ ({a}\ (\hbox{\pagecolor{light-gray}b}\ y))\Rightarrow p\ ({a}\ y))\Rightarrow(\forall p.\forall y.p\ ({a}\ y)\Rightarrow p\ (\hbox{\pagecolor{light-gray}b}\ y))\Rightarrow a\ x}_{T^{\prime}}

Note that the quantified variable $b$ in (II) is an existential variable. If $f$ is typable with (II), then we know that $\Gamma\vdash f\ A\ B\ x\ \kappa_{a}\ \kappa_{b}:A\ x$, which encodes the nonterminating reduction starting from $A\ x$. But RSM will fail again in this case, due to the appearance of the existential variable $b$.

Ideally, the best way to deal with existential variables is by unification, we would need to replace rule (1) in RSM with the following:

$\{(\Gamma,(\kappa|\alpha)\ e_{1}\ ...\ e_{n},A),\Phi\}\longrightarrow_{a}\{(\sigma\Gamma,e_{1},\sigma T_{1}),...,(\sigma\Gamma,e_{1},\sigma T_{n}),\sigma\Phi\}$ if $\kappa|\alpha:\forall\underline{x}.T_{1},...,T_{n}\Rightarrow B\in\Gamma$ with $B\sim_{\sigma}A$

Here $B\sim_{\sigma}A$ means $A$ and $B$ are second-orderly unifiable by $\sigma$. And $\sigma\Gamma,\sigma\Phi$ means applying the substitution $\sigma$ to all the types in $\Gamma,\Phi$. But second-order unification is not decidable and we need a finite set of unifiers. Thus we replace $B\sim_{\sigma}A$ with $B\mapsto_{\sigma}A$.

Definition 6.1** (Existential RSM (ERSM)).**

We replace (1) in Definition 5.3 to the following (Keeping rules (2), (3), (4) unchanged):

(1’) $\{(\Gamma,(\kappa|\alpha)\ e_{1}\ ...\ e_{n},A),\Phi\}\longrightarrow_{a}\{(\sigma\Gamma,e_{1},\sigma T_{1}),...,(\sigma\Gamma,e_{n},\sigma T_{n}),\sigma\Phi\}$

if $\kappa|\alpha:\forall x_{1}....\forall x_{m}.T_{1},...,T_{n}\Rightarrow B\in\Gamma$ with $B\mapsto_{\sigma}A$.

Note that the formula $\forall x_{1}....\forall x_{m}.T_{1},...,T_{n}\Rightarrow B$ in rule (1’) may contain existential variables. The idea of this change is that by reordering the $(\Gamma,e,T)$ pairs, we give priority to resolve the pair $(\Gamma,e,T)$ where the head of $T$ does not contain any existential variables. If the $A$ in (1’) does not contain existential variables, we can use rule (1’) to eliminate the existential variables in $\forall x_{1}....\forall x_{m}.T_{1},...,T_{n}\Rightarrow B$. This extension allows us to avoid using the undecidable second-order unification, and it is good enough to handle all of our examples involving existential variables555There is a well-known scope problem [7, Section 5], we show how to solve it for ERSM and prove the soundness of ERSM in Appendix I..

With the Definition 6.1, we can obtain the following successful ERSM reduction, where $\mu f.\lambda\alpha.\lambda\beta.\alpha\ (f\ (\lambda\alpha^{\prime}.(\alpha\ (\beta\ \alpha^{\prime})))\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime}))$ is the long form of $f\ \alpha\ \beta=\alpha\ (f(\alpha\cdot\beta)\ \alpha)$.

$\{(\Gamma,\mu f.\lambda\alpha.\lambda\beta.\alpha\ (f\ (\lambda\alpha^{\prime}.(\alpha\ (\beta\ \alpha^{\prime})))\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})),T\}\longrightarrow_{c}$

$\{([\Gamma,f:T],\lambda\alpha.\lambda\beta.\alpha\ (f\ (\lambda\alpha^{\prime}.(\alpha\ (\beta\ \alpha^{\prime})))\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})),T)\}\longrightarrow_{\forall}$

\{([\Gamma,f:T],\lambda\alpha.\lambda\beta.\alpha\ (f\ (\lambda\alpha^{\prime}.(\alpha\ (\beta\ \alpha^{\prime})))\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})),[a_{1}/a,b_{1}/b,x_{1}/x]T^{\prime})\}\longrightarrow_{i}\{(\Gamma^{\prime},\alpha\ (f\ (\lambda\alpha^{\prime}.(\alpha\ (\beta\ \alpha^{\prime})))\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime})),a_{1}\ x_{1})\}\longrightarrow_{a}\{(\Gamma^{\prime},f\ (\lambda\alpha^{\prime}.(\alpha\ (\beta\ \alpha^{\prime})))\ (\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime}),a_{1}\ (b_{1}\ x_{1})\}\hbox{\pagecolor{light-gray}\longrightarrow_{a}}

\{(\Gamma^{\prime},\lambda\alpha^{\prime}.\alpha\ (\beta\ \alpha^{\prime}),\forall p.\forall y.p\ (a_{1}\ (b_{1}\ (\hbox{\pagecolor{light-gray}b_{2}}\ y)))\Rightarrow p\ (a_{1}\ (b_{1}\ y))),\Phi\equiv(\Gamma^{\prime},\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime},(\forall p.\forall y.p\ (a_{1}\ (b_{1}\ y))\Rightarrow p\ (\hbox{\pagecolor{light-gray}b_{2}}\ y)))\}\longrightarrow_{\forall}

\{(\Gamma^{\prime},\lambda\alpha^{\prime}.\alpha\ (\beta\ \alpha^{\prime}),p_{2}\ (a_{1}\ (b_{1}\ (\hbox{\pagecolor{light-gray}b_{2}}\ y_{2})))\Rightarrow p_{2}\ (a_{1}\ (b_{1}\ y_{2}))),\Phi\}\longrightarrow_{i}

\{([\Gamma^{\prime},\alpha^{\prime}:p_{2}\ (a_{1}\ (b_{1}\ (\hbox{\pagecolor{light-gray}b_{2}}\ y_{2})))],\alpha\ (\beta\ \alpha^{\prime}),p_{2}\ (a_{1}\ (b_{1}\ y_{2})))),\Phi\}\longrightarrow_{a}

\{([\Gamma^{\prime},\alpha^{\prime}:p_{2}\ (a_{1}\ (b_{1}\ (\hbox{\pagecolor{light-gray}b_{2}}\ y_{2})))],\beta\ \alpha^{\prime},p_{2}\ (a_{1}\ (b_{1}\ (b_{1}\ y_{2})))),\Phi\}\longrightarrow_{a}

\{([\Gamma^{\prime},\alpha^{\prime}:p_{2}\ (a_{1}\ (b_{1}\ (\hbox{\pagecolor{light-gray}b_{2}}\ y_{2})))],\alpha^{\prime},p_{2}\ (a_{1}\ (b_{1}\ (a_{1}\ y_{2})))),\Phi\}\hbox{\pagecolor{light-gray}\longrightarrow_{a}}

[(\lambda y.a_{1}\ y)/\hbox{\pagecolor{light-gray}b_{2}}]\Phi\equiv\{(\Gamma^{\prime},\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime},\forall p.\forall y.p\ (a_{1}\ (b_{1}\ y))\Rightarrow p\ (a_{1}\ y))\}\longrightarrow_{\forall}

$\{(\Gamma^{\prime},\lambda\alpha^{\prime}.\alpha\ \alpha^{\prime},p_{3}\ (a_{1}\ (b_{1}\ y_{3}))\Rightarrow p_{3}\ (a_{1}\ y_{3}))\}\longrightarrow_{i}$

$\{([\Gamma^{\prime},\alpha^{\prime}:p_{3}\ (a_{1}\ (b_{1}\ y_{3}))],\alpha\ \alpha^{\prime},p_{3}\ (a_{1}\ y_{3}))\}\longrightarrow_{a}$

$\{([\Gamma^{\prime},\alpha^{\prime}:p_{3}\ (a_{1}\ (b_{1}\ y_{3}))],\alpha^{\prime},p_{3}\ (a_{1}\ (b_{1}\ y_{3})))\}\longrightarrow_{a}\emptyset$

Note that $\Gamma^{\prime}=\Gamma,f:T,\alpha:\forall p.\forall y.p\ (a_{1}\ (b_{1}\ y))\Rightarrow p\ (a_{1}\ y),\beta:\forall p.\forall y.p\ (a_{1}\ y)\Rightarrow p\ (b_{1}\ y)$. At the second $\longrightarrow_{a}$-step, by second-order matching, variable $a$ is instantiated with $\lambda y.a_{1}\ (b_{1}\ y)$ for the type of $f$ and the existential variable $b$ is instantiated with fresh variable $b_{2}$. At the fifth $\longrightarrow_{a}$-step, the existential variable $b_{2}$ is instantiated with $\lambda y.a_{1}\ y$, and there is a substitution for $b_{2}$ applying to $\Phi$. But RSM will not perform this substitution, as a result, RSM cannot resolve $\Phi$ to $\emptyset$.

7 Conclusion and Future Work

We present a novel method to represent nonterminating reductions in $\mathbf{F}_{2}^{\mu}$, where the rewrite rules and first-order terms are modeled by types, and the nonterminations are modeled by the hereditary head normalizing evidence. We prove that the hereditary head normalizing evidence for a first-order term is faithful, i.e. it represents a nonterminating reduction. We also prove the hereditary head normalization property for $\mathbf{F}_{2}^{\mu}$ is decidable. To ease the representation process, we develop a type checking algorithm based on second-order matching, where fully annotated evidence can be generated from Curry-style evidence with only top-level type annotations.

Future work. We would like to investigate the nonterminating reductions that are currently outside the scope of $\mathbf{F}_{2}^{\mu}$ and study the expressitivity of $\mathbf{F}_{2}^{\mu}$ in terms of representing nonterminations. The RSM/ERSM type checking algorithm is not very flexible. For example the Curry style evidence currently has to be in long form. We plan to relax this restriction.

Acknowledgement

I would like to thank Tom Schrijvers for coming up with Example 5.1 and showing me a solution in Haskell using type family (See Fu et. al. [10]), at a time when I thought this whole thing is impossible. I also like to thank Ekaterina Komendantskaya for many helpful discussions, which leads me to consider the automation aspect, eventually I discover that quantification over higher-order variables leads to another solution for Example 5.1 without using type family, hence this paper. Reviewer 1 from FSCD 2016 discovered an error in an ealier version of the paper, which leads to a more rigid formulation of $\mathbf{F}_{2}^{\mu}$. Reviewer A from POPL 2017 suggests a possible simplification of productivity checking by mapping $\mathbf{F}_{2}^{\mu}$ to $\lambda$-Y, which I carried out in this paper, and it greatly simplifies and strengthens the paper. Leibniz representation in this paper is inspired by Stump and Schürmann [20]’s treatment on rewriting and Girard’s recent criticism about Leibniz equality 666J.Y. Girard, Transcendental syntax III: equality. I would also like to thank the School of Computing at University of Dundee, and my mother Chen Xingzhen for generously providing a working space for me when I was in transitions between Postdocs.

Appendix A Proof of Theorem 3.5

Theorem A.1**.**

If $\Delta\vdash T:k$ and $T\to_{o}T^{\prime}$, then $\mathrm{FV}(T)=\mathrm{FV}(T^{\prime})$ and $\Delta\vdash T^{\prime}:k$

Proof A.2**.**

By induction on the derivation of $\Delta\vdash T:k$.

Case*.*

$\Delta\vdash x|F:K(x|F:K)\in\Delta$**

Obvious.

Case*.*

$\Delta\vdash\lambda x.T:*\Rightarrow K\lx@proof@logical@and\Delta,x:*\vdash T:Kx\in\mathrm{FV}(T)$**

We have $T\to_{o}T^{\prime}$. By IH, we have $\Delta,x:*\vdash T^{\prime}:K$ and $\mathrm{FV}(T)=\mathrm{FV}(T^{\prime})$. Thus $x\in\mathrm{FV}(T^{\prime})$. So $\Delta\vdash\lambda x.T^{\prime}:*\Rightarrow K$.

Case*.*

$\Delta\vdash(\lambda x.T_{2})\ T_{1}:K\lx@proof@logical@and\Delta\vdash T_{1}:*\Delta\vdash\lambda x.T_{2}:*\Rightarrow K$**

We have $(\lambda x.T_{2})\ T_{1}\to_{o}[T_{1}/x]T_{2}$. Since $\Delta\vdash\lambda x.T_{2}:*\Rightarrow K$, by inversion we know that $\Delta,x:*\vdash T_{2}:K$ and $x\in\mathrm{FV}(T_{2})$. So $\mathrm{FV}((\lambda x.T_{2})\ T_{1})=\mathrm{FV}([T_{1}/x]T_{2})$ and $\Delta\vdash[T_{1}/x]T_{2}:K$.

Case*.*

$\Delta\vdash\forall x.T:o\Delta,x:K\vdash T:o|*$**

Suppose $\forall x.T\to_{o}\forall x.T^{\prime}$ by $T\to_{o}T^{\prime}$. By IH, $\Delta,x:K\vdash T^{\prime}:o|*$ and $\mathrm{FV}(T)=\mathrm{FV}(T^{\prime})$. Thus $\Delta\vdash\forall x.T^{\prime}:o$ and $\mathrm{FV}(\forall x.T)=\mathrm{FV}(\forall x.T^{\prime})$.

All the other cases are similar.

Appendix B Proof of Theorem 3.7

Theorem B.1**.**

If $\Delta\vdash T:o$, then $T$ is of the form $\forall x.T^{\prime}$ or $T_{1}\Rightarrow T_{2}$. 2. 2.

If $\Delta\vdash T:*^{n}\Rightarrow*$, then the normal form of $T$ is second-order.

Proof B.2**.**

(1) Obvious.

(2). By induction on the derivation of $\Delta\vdash T:*^{n}\Rightarrow*$.

Case*.*

$\Delta\vdash x|F:K(x|F:K)\in\Delta$**

Obvious.

Case*.*

$\Delta\vdash T_{2}\ T_{1}:K\lx@proof@logical@and\Delta\vdash T_{1}:*\Delta\vdash T_{2}:*\Rightarrow K$**

We need to show the normal form of $T_{2}\ T_{1}$ is second-order. By IH, we know the normal form of $T_{1},T_{2}$ are second-order, moreover, $T_{1}$ is flat since $\Delta\vdash T_{1}:*$. Suppose $T_{2}\equiv F$ or $T_{2}\equiv x$, then by definition we know $T_{2}\ T_{1}$ is second-order. Suppose $T_{2}\equiv\lambda x.T^{\prime}$, where $x\in\mathrm{FV}(T^{\prime})$ and $T^{\prime}$ is second-order. Then $(\lambda x.T^{\prime})\ T_{1}\to_{o}[T_{1}/x]T^{\prime}$ and $[T_{1}/x]T^{\prime}$ is second-order.

Case*.*

$\Delta\vdash\lambda x.T:*\Rightarrow K\lx@proof@logical@and\Delta,x:*\vdash T:Kx\in\mathrm{FV}(T)$**

Let $[T]$ be the normal form of $T$. By IH, we know that $[T]$ is second-order. By Theorem 3.5, we know that $x\in\mathrm{FV}([T])$. Thus $\lambda x.[T]$ is second-order.

Appendix C Proof of Theorem 3.9

Theorem C.1**.**

$\leadsto_{\beta\mu\tau o}$* and $\leadsto_{h\tau o}$ are confluent, and $\leadsto_{\tau}$ is strongly normalizing.*

Proof C.2**.**

Note that $\leadsto_{\tau}$ commutes with $\leadsto_{o}$, $\leadsto_{h}$ and $\leadsto_{\beta\mu}$. Also $\leadsto_{o}$ commutes with $\leadsto_{h}$ and $\leadsto_{\beta\mu}$. Thus it is enough to show that $\leadsto_{h}$ and $\leadsto_{\beta\mu}$ are confluent. For $\leadsto_{h}$, we just need to check $\mathcal{H}_{1}[(\lambda x.(\mathcal{H}_{2}[\mu\alpha.e^{\prime}]))\ e]$, as it is the only critical pair. We know that:

$\mathcal{H}_{1}[(\lambda\alpha.(\mathcal{H}_{2}[\mu\beta.e^{\prime}]))\ e]\leadsto_{h}\mathcal{H}_{1}[([e/\alpha]\mathcal{H}_{2})[\mu\beta.[e/\alpha]e^{\prime}]]\leadsto_{h}\mathcal{H}_{1}[([e/\alpha]\mathcal{H}_{2})[[\mu\beta.[e/\alpha]e^{\prime}/\beta][e/\alpha]e^{\prime}]]$**

$\mathcal{H}_{1}[(\lambda\alpha.(\mathcal{H}_{2}[\mu\beta.e^{\prime}]))\ e]\leadsto_{h}\mathcal{H}_{1}[(\lambda\alpha.\mathcal{H}_{2}[[\mu\beta.e^{\prime}/\beta]e^{\prime}])\ e]\leadsto_{h}\mathcal{H}_{1}[([e/\alpha]\mathcal{H}_{2})[[\mu\beta.[e/\alpha]e^{\prime}/\beta][e/\alpha]e^{\prime}]]$*

---

Thus $\leadsto_{h}$ is confluent. For the confluence of $\leadsto_{\beta\mu}$, we refer to the existing literature (e.g. [1, §7.1]). Finally, $\leadsto_{\tau}$ is strongly normalizing because the number of $\leadsto_{\tau}$-redex is strictly decreasing.

Appendix D Proof of Theorem 3.12

Theorem D.1** (Inversion).**

If $\Gamma\vdash x:T$, then there exists $(x:T^{\prime})\in\Gamma$ and $T\leftrightarrow_{o}^{*}T^{\prime}$. 2. 2.

If $\Gamma\vdash\kappa:T$, then there exists $(\kappa:T^{\prime})\in\Gamma$ and $T\leftrightarrow_{o}^{*}T^{\prime}$. 3. 3.

If $\Gamma\vdash\lambda\alpha.e:T$, then $\Gamma,\alpha:T_{1}\vdash e:T_{2}$ and $T_{1}\Rightarrow T_{2}\leftrightarrow_{o}^{*}T$. 4. 4.

If $\Gamma\vdash e\ e^{\prime}:T$, then $\Gamma\vdash e:T_{1}\Rightarrow T_{2}$, $\Gamma\vdash e^{\prime}:T_{1}$ and $T_{2}\leftrightarrow_{o}^{*}T$. 5. 5.

If $\Gamma\vdash\lambda x.e:T$, then $\Gamma\vdash e:T^{\prime}$, $x\notin\mathrm{FV}(\Gamma)$ and $\forall x.T^{\prime}\leftrightarrow_{o}^{*}T$. 6. 6.

If $\Gamma\vdash e\ T_{1}:T$, then $\Gamma\vdash e:\forall x.T^{\prime}$ and $[T_{1}/x]T^{\prime}\leftrightarrow_{o}^{*}T$. 7. 7.

If $\Gamma\vdash\mu\alpha.e:T$, then $\Gamma,\alpha:T^{\prime}\vdash e:T^{\prime}$ and $T^{\prime}\leftrightarrow_{o}^{*}T$.

Proof D.2**.**

By induction on derivation.

Lemma D.3**.**

$\Gamma,\alpha:T\vdash e:T^{\prime}$* and $\Gamma\vdash e^{\prime}:T$, then $\Gamma\vdash[e^{\prime}/\alpha]e:T^{\prime}$.* 2. 2.

$\Gamma\vdash e:T^{\prime}$, then $[T_{1}/x]\Gamma\vdash[T_{1}/x]e:[T_{1}/x]T^{\prime}$.

Proof D.4**.**

By induction on the derivation.

Theorem D.5**.**

If $\Gamma\vdash e:T$ and $e\leadsto_{h\tau o}e^{\prime}$, then $\Gamma\vdash e^{\prime}:T$.

Proof D.6**.**

By induction on the derivation of $\Gamma\vdash e:T$.

Case*.*

$\Gamma\vdash\mu\alpha.e:T\Gamma,\alpha:T\vdash e:T$**

We know $\mu\alpha.e\leadsto_{h}[\mu\alpha.e/\alpha]e$. By lemma D.3 (1), we know that $\Gamma\vdash[\mu\alpha.e/\alpha]e:T$.

Case*.*

$\Gamma\vdash(\lambda\alpha.e)\ e_{1}:T\lx@proof@logical@and\Gamma\vdash e_{1}:T^{\prime}\Gamma\vdash\lambda\alpha.e:T^{\prime}\Rightarrow T$**

Suppose $(\lambda\alpha.e)\ e_{1}\leadsto_{h}[e_{1}/\alpha]e$. By Theorem D.1 (4), we have $\Gamma,\alpha:T_{1}\vdash e:T_{2}$ and $T_{1}\Rightarrow T_{2}\leftrightarrow_{o}^{*}T^{\prime}\Rightarrow T$. Since $\to_{o}$ is confluent, we have $T_{1}\leftrightarrow_{o}^{*}T^{\prime}$ and $T_{2}\leftrightarrow_{o}^{*}T$. Thus $\Gamma\vdash e_{1}:T_{1}$. By Lemma D.3 (1), we know $\Gamma\vdash[e_{1}/\alpha]e:T_{2}$. Thus $\Gamma\vdash[e_{1}/\alpha]e:T$.

Case*.*

$\Gamma\vdash(\lambda x.e)\ T^{\prime}:[T^{\prime}/x]T\Gamma\vdash\lambda x.e:\forall x:K.T$**

Suppose that $(\lambda x.e)\ T^{\prime}\leadsto_{\tau}[T^{\prime}/x]e$. By Theorem D.1 (5), we have $\Gamma\vdash e:T_{1}$, $x\notin\mathrm{FV}(\Gamma)$ and $\forall x.T_{1}\leftrightarrow^{*}_{o}\forall x.T$. By Lemma D.3 (2), we have $\Gamma\vdash[T^{\prime}/x]e:[T^{\prime}/x]T_{1}$. Since $\forall x.T_{1}\leftrightarrow^{*}_{o}\forall x.T$ implies $[T^{\prime}/x]T_{1}\leftrightarrow^{*}_{o}[T^{\prime}/x]T$, we have $\Gamma\vdash[T^{\prime}/x]e:[T^{\prime}/x]T$.

Suppose that $(\lambda x.e)\ T^{\prime}\leadsto_{o}(\lambda x.e)\ T^{\prime\prime}$ with $T^{\prime}\to_{o}T^{\prime\prime}$. So by App rule, we have $\Gamma\vdash(\lambda x.e)\ T^{\prime\prime}:[T^{\prime\prime}/x]T$. By Conv rule, we have $\Gamma\vdash(\lambda x.e)\ T^{\prime\prime}:[T^{\prime}/x]T$.

For all the other cases are easy.

Appendix E Proof of Theorem 4.7

Lemma E.1**.**

Suppose $\Gamma_{\mathcal{R}}\vdash e:t$ for some first-order term $t$ and $e$ is head normalizing. We have $e\leadsto_{h\tau}^{*}\kappa\ (\lambda x.C[x,...,x])\ t_{1}...\ t_{n}\ e^{\prime}$ for some $\kappa:\forall p.\forall\underline{x}.p\ r\Rightarrow p\ l\in\Gamma_{\mathcal{R}}$. Furthermore, we have $\Gamma_{\mathcal{R}}\vdash e^{\prime}:C[\sigma r,...,\sigma r]$ and $C[\sigma l,...,\sigma l]=t$, where $\mathrm{codom}(\sigma)=\{t_{1},...,t_{n}\}$ and $\mathrm{dom}(\sigma)=\mathrm{FV}(l)$.

Proof E.2**.**

Since $e$ is head normalizing and $\Gamma_{\mathcal{R}}\vdash e:t$, its head normal form must be of the $\kappa\ T\ T_{1}...\ T_{n}\ e^{\prime}$ for some $\kappa:\forall p.\forall\underline{x}.p\ r\Rightarrow p\ l\in\Gamma_{\mathcal{R}}$. By subject reduction (Theorem 3.5, Theorem 3.12), we have $\Gamma_{\mathcal{R}}\vdash\kappa\ T\ T_{1}...\ T_{n}\ e^{\prime}:t$. By inversion Theorem 3.11 (1) on $\Gamma_{\mathcal{R}}\vdash\kappa\ T\ T_{1}...\ T_{n}\ e^{\prime}:t$, we know that $\Gamma_{\mathcal{R}}\vdash\kappa\ T\ T_{1}...\ T_{n}:T_{1}^{\prime}\Rightarrow T_{2}^{\prime}$, $\Gamma_{\mathcal{R}}\vdash e^{\prime}:T_{1}^{\prime}$ and $T_{2}^{\prime}\leftrightarrow_{o}t$. By inversion Theorem 3.11 (2) on $\Gamma_{\mathcal{R}}\vdash\kappa\ T\ T_{1}...\ T_{n}:T_{1}^{\prime}\Rightarrow T_{2}^{\prime}$, we have $\sigma(p\ r)\Rightarrow\sigma(p\ l)\leftrightarrow^{*}_{o}T_{1}^{\prime}\Rightarrow T_{2}^{\prime}$, where $\sigma=[T/p,T_{1}/x_{1},...,T_{n}/x_{n}]$. Since we are working with well-kinded types, we know that $\Gamma_{\mathcal{R}}\vdash T:*\Rightarrow*$ and $\Gamma_{\mathcal{R}}\vdash T_{i}:*$ for all $i$. By Theorem 3.7, we know $T=\lambda x.C[x,...,x]$ and $T_{i}$ is flat for all $i$. By confluence of $\leftrightarrow_{o}$, we have $\sigma(p\ r)\leftrightarrow_{o}^{*}T_{1}^{\prime}$ and $\sigma(p\ l)\leftrightarrow_{o}^{*}T_{2}^{\prime}\leftrightarrow_{o}^{*}t$. Thus $\sigma(p\ l)\equiv[T/p,T_{1}/x_{1},...,T_{n}/x_{n}](p\ l)\equiv(\lambda x.C[x,...,x])\ (\sigma l)\to_{o}^{*}t$. So $C[\sigma l,...,\sigma l]=t$. Since $\sigma(p\ r)\leftrightarrow_{o}^{*}T_{1}^{\prime}$, we have $\Gamma_{\mathcal{R}}\vdash e^{\prime}:C[\sigma r,...,\sigma r]$.

Appendix F Mapping $\mathbf{F}_{2}^{\mu}$ to $\lambda$-Y

Definition F.1** ($\lambda$-Y calculus).**

$\lambda$-Y terms $e::=\alpha\ |\ \kappa\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \lambda\alpha.e\leavevmode\nobreak\ \mid\leavevmode\nobreak\ e\ e^{\prime}\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \mu\alpha.e$

$\lambda$-Y types $T::=B\ |\ T\Rightarrow T^{\prime}$

$\lambda$-Y environment $\Gamma::=\cdot\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \alpha:T,\Gamma\ |\ \kappa:T$

Note that $B$ denotes a constant type in $\lambda$-Y.

Definition F.2** (Typing of $\lambda$-Y).**

[TABLE]

Definition F.3**.**

We define a function $\theta$ that maps $\mathbf{F}_{2}^{\mu}$ types to $\lambda$-Y types.

$\theta(F)=B$**

$\theta(x)=B$**

$\theta(\lambda x.T)=\theta(T)$**

$\theta(T\ T^{\prime})=\theta(T)$**

$\theta(T\Rightarrow T^{\prime})=\theta(T)\Rightarrow\theta(T^{\prime})$**

$\theta(\forall x.T)=\theta(T)$**

Lemma F.4**.**

If $\Delta\vdash T:K$ in $\mathbf{F}_{2}^{\mu}$, then $\theta(T)=B$.

Proof F.5**.**

By induction on the derivation of $\Delta\vdash T:K$.

Lemma F.6**.**

If $\Delta\vdash T^{\prime}:K$ in $\mathbf{F}_{2}^{\mu}$, then $\theta([T^{\prime}/x]T)\equiv\theta(T)$ for any $T$ in $\mathbf{F}_{2}^{\mu}$.

Proof F.7**.**

Using Lemma F.4 and induction on the structure of $T$.

Lemma F.8**.**

If $T_{1}\leftrightarrow_{o}^{*}T_{2}$ and $\Delta\vdash T_{1}|T_{2}:k$ in $\mathbf{F}_{2}^{\mu}$, then $\theta(T_{1})\equiv\theta(T_{2})$.

Proof F.9**.**

By induction on the derivation of $T_{1}\leftrightarrow_{o}^{*}T_{2}$.

Definition F.10**.**

$\theta(.)=.$**

$\theta(\Gamma,\alpha:T)=\theta(\Gamma),\alpha:\theta(T)$**

$\theta(\Gamma,\kappa:T)=\theta(\Gamma),\kappa:\theta(T)$**

Theorem F.11**.**

If $\Gamma\vdash e:T$ and $\Delta\vdash T:*|o$ in $\mathbf{F}_{2}^{\mu}$, then $\theta(\Gamma)\vdash|e|:\theta(T)$ in $\lambda$-Y.

Proof F.12**.**

By induction on derivaton of $\Gamma\vdash e:T$ in $\mathbf{F}_{2}^{\mu}$.

• •

Case:

[TABLE]

We just need to show $\theta(\Gamma)\vdash\alpha|\kappa:\theta(T)$ in $\lambda$-Y, which we know is the case by definition of $\theta(\Gamma)$.

• •

Case:

[TABLE]

We need to show $\theta(\Gamma)\vdash|e_{2}\ e_{1}|:\theta(T)$ in $\lambda$-Y. By induction, we know that $\theta(\Gamma)\vdash|e_{1}|:\theta(T^{\prime})$ and $\theta(\Gamma)\vdash|e_{2}|:\theta(T^{\prime})\Rightarrow\theta(T)$ in $\lambda$-Y. Thus we have $\theta(\Gamma)\vdash|e_{2}|\ |e_{1}|:\theta(T)$.

• •

Case:

[TABLE]

We need to show $\theta(\Gamma)\vdash\lambda\alpha.|e|:\theta(T^{\prime})\Rightarrow\theta(T)$ in $\lambda$-Y. By induction, we know that $\theta(\Gamma),\alpha:\theta(T^{\prime})\vdash|e|:\theta(T)$ in $\lambda$-Y.

• •

Case:

[TABLE]

We need to show $\theta(\Gamma)\vdash\mu\alpha.|e|:\theta(T)$ in $\lambda$-Y. By induction, we know that $\theta(\Gamma),\alpha:\theta(T)\vdash|e|:\theta(T)$ in $\lambda$-Y.

• •

Case:

[TABLE]

We need to show $\theta(\Gamma)\vdash|e|:\theta(T)$ in $\lambda$-Y, which is the case by induction.

• •

Case:

[TABLE]

We need to show $\theta(\Gamma)\vdash|e|:\theta([T^{\prime}/x]T)$ in $\lambda$-Y. By induction, we know that $\theta(\Gamma)\vdash|e|:\theta(T)$. By Lemma F.6, we know that $\theta([T^{\prime}/x]T)\equiv\theta(T)$.

• •

Case:

[TABLE]

We need to show $\theta(\Gamma)\vdash|e|:\theta(T^{\prime})$ in $\lambda$-Y. By induction, we know that $\theta(\Gamma)\vdash|e|:\theta(T)$. By Lemma F.8, we know that $\theta(T^{\prime})\equiv\theta(T)$.

Appendix G Proof of Theorem 5.4

Lemma G.1**.**

If $\{(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{n},e_{n},T_{n})\}\longrightarrow^{*}\emptyset$, then there exists an evidence $e^{\prime}_{1},...,e^{\prime}_{n}$ such that $\Gamma_{i}\vdash e^{\prime}_{i}:T_{i}$ and $|e^{\prime}_{i}|=e_{i}$ for all $i$.

Proof G.2**.**

By induction on the length of $\{(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{n},e_{n},T_{n})\}$ $\longrightarrow^{*}\emptyset$.

• •

Case $\{(\Gamma,\alpha|\kappa,A)\}\longrightarrow_{a}\emptyset$.

In this case $\alpha|\kappa:\forall\underline{x}.B\in\Gamma$ and $B\mapsto_{\sigma}A$. Since $\forall\underline{x}.B$ does not contain existential variables, by Inst, we have $\Gamma\vdash(\alpha|\kappa)\ \underline{T}:A$, where $\{\underline{T}\}=\mathrm{codom}(\sigma)$ and $|(\alpha|\kappa)\ \underline{T}|=\alpha|\kappa$.

• •

Case

$\{(\Gamma,(\alpha|\kappa)\ e^{\prime\prime}_{1}\ ...e_{m}^{\prime\prime},A),(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{n},e_{n},T_{n})\}\longrightarrow_{a}$**

$\{(\Gamma,e_{1}^{\prime\prime},\sigma T_{1}^{\prime}),...,(\Gamma,e_{m}^{\prime\prime},\sigma T_{m}^{\prime}),(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{n},e_{n},T_{n})\}\longrightarrow^{*}\emptyset$, where $\kappa|\alpha:\forall\underline{x}.T_{1}^{\prime},...,T_{n}^{\prime}\Rightarrow B\in\Gamma$ with $B\mapsto_{\sigma}A$.

By IH, we know that $\Gamma\vdash e_{1}^{\prime\prime\prime}:\sigma T_{1}^{\prime},...,\Gamma\vdash e_{m}^{\prime\prime}:\sigma T_{m}^{\prime},\Gamma_{1}\vdash e_{1}^{\prime}:T_{1},...,\Gamma_{n}\vdash e_{n}^{\prime}:T_{n}$ and $|e_{1}^{\prime\prime\prime}|=e_{1}^{\prime\prime},...,|e_{m}^{\prime\prime\prime}|=e_{m}^{\prime\prime},|e_{1}^{\prime}|=e_{1},...,|e_{n}^{\prime}|=e_{n}$. Let $\mathrm{codom}(\sigma)=\underline{T}$, since $\forall\underline{x}.T_{1}^{\prime},...,T_{n}^{\prime}\Rightarrow B$ does not contain existential variables, we have $\Gamma\vdash(\alpha|\kappa)\ \underline{T}:\sigma T_{1}^{\prime},...,\sigma T_{n}^{\prime}\Rightarrow\sigma B$. Thus $\Gamma\vdash(\alpha|\kappa)\ \underline{T}\ e_{1}^{\prime\prime\prime}\ ...\ e_{m}^{\prime\prime\prime}:\sigma B$. By Conv, we have $\Gamma\vdash(\alpha|\kappa)\ \underline{T}\ e_{1}^{\prime\prime\prime}\ ...\ e_{m}^{\prime\prime\prime}:A$. Moreover, $|(\alpha|\kappa)\ \underline{T}\ e_{1}^{\prime\prime\prime}\ ...\ e_{m}^{\prime\prime\prime}|=(\alpha|\kappa)\ |e_{1}^{\prime\prime\prime}|\ ...\ |e_{m}^{\prime\prime\prime}|=(\alpha|\kappa)\ e_{1}^{\prime\prime}\ ...\ e_{m}^{\prime\prime}$.

• •

*Case

$\{(\Gamma,\lambda\alpha_{1}....\lambda\alpha_{n}.e,T_{1},...,T_{n}\Rightarrow A),(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{l},e_{l},T_{l})\}$ $\longrightarrow_{i}\{([\Gamma,\alpha_{1}:T_{1},...,\alpha_{n}:T_{n}],e,A),(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{l},e_{l},T_{l})\}\longrightarrow^{*}\emptyset$*

By IH, we have $\Gamma,\alpha_{1}:T_{1},...,\alpha_{n}:T_{n}\vdash e^{\prime}:A,\Gamma_{1}\vdash e_{1}^{\prime}:T_{1},...,\Gamma_{l}\vdash e_{l}^{\prime}:T_{l}$ with $|e^{\prime}|=e,|e_{1}^{\prime}|=e_{1},...,|e_{l}^{\prime}|=e_{l}$. Thus by Lam rule, we have $\Gamma\vdash\lambda\alpha_{1}....\lambda\alpha_{n}.e^{\prime}:T_{1},...,T_{n}\Rightarrow A$ and $|\lambda\alpha_{1}....\lambda\alpha_{n}.e^{\prime}|=\lambda\alpha_{1}....\lambda\alpha_{n}.e$.

• •

*Case

$\{(\Gamma,e,\forall x_{1}....\forall x_{m}.T),(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{l},e_{l},T_{l})\}\longrightarrow_{\forall}$*

$\{(\Gamma,e,T),(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{l},e_{l},T_{l})\}\longrightarrow^{*}\emptyset$**

By IH, we have $\Gamma\vdash e^{\prime}:A,\Gamma_{1}\vdash e_{1}^{\prime}:T_{1},...,\Gamma_{l}\vdash e_{l}^{\prime}:T_{l}$ with $|e^{\prime}|=e,|e_{1}^{\prime}|=e_{1},...,|e_{l}^{\prime}|=e_{l}$. Since $\{x_{1},...,x_{m}\}\cap\mathrm{FV}(\Gamma)=\emptyset$, by Abs rules, we have $\Gamma\vdash\lambda x_{1}....\lambda x_{m}.e^{\prime}:\forall x_{1}....\forall x_{m}.T$ and $|\lambda x_{1}....\lambda x_{m}.e^{\prime}|=e$.

• •

Case $\{(\Gamma,\mu\alpha.e,T),(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{n},e_{n},T_{n})\}\longrightarrow_{c}\{([\Gamma,\alpha:T],e,T),(\Gamma_{1},e_{1},T_{1}),...,(\Gamma_{n},e_{n},T_{n})\}$

$\longrightarrow^{*}\emptyset$**

By IH, we know that $\Gamma,\alpha:T\vdash e^{\prime}:T,\Gamma_{1}\vdash e_{1}^{\prime}:T_{1},...,\Gamma_{n}\vdash e_{n}^{\prime}:T_{n}$ and $|e_{i}^{\prime}|=e_{i}$ for all $i$. By Mu rule, we have $\Gamma\vdash\mu\alpha.e^{\prime}:T$. Thus $|\mu\alpha.e^{\prime}|=\mu\alpha.e$.

Appendix H Examples in the Paper

In this section we show how to represent nonterminations for all the examples in the paper using the prototype FCR (for Functional Certification of Rewriting), the prototype is available at https://github.com/Fermat/FCR. It tries to generate typable $\mathbf{F}_{2}^{\mu}$ evidence from the corecursive equations and the type declarations.

H.1 Example in Section 5

The following is the input file for FCR.

A : forall p x y . p (D x (S y)) => p (D (S x) y) B : forall p y . p (D (S y) Z) => p (D Z y)

g : forall d . (forall p x y . p (d x (S y)) => p (d (S x) y)) => (forall p y . p (d (S y) Z) => p (d Z y)) => d Z Z

g a1 a2 = a2 (a1 (g (\ v . a1 v) (\ v . a2 (a1 v))))

e : D Z Z e = g (\ v . A v) (\ v . B v)

The capitalized words for FCR are intended to denote both type and evidence constant, uncapitalized words are intended to denote both type and evidence variables. In the definition of corecursive function g, “\” denotes the $\lambda$ binder, its type declaration is discussed in the paper. FCR currently uses long normal form to make variable instantiation, so we have to use (I) instead of (II).

(I) g a1 a2 = a2 (a1 (g (\v . a1 v) (\v . a2 (a1 v))))

(II) g a1 a2 = (a2 . a1) (g a1 (a2 . a1))

Evidence such as $\mu f.\lambda a.e$ is represented as equation f a = e, so there is no explicit $\mu$ binder in the input file. The corecursive evidence for D Z Z is e. The following is the output by the type checker.

rewrite rules kinds D : * => * => * S : * => * Z : * axioms A : forall p x y . p (D x (S y)) => p (D (S x) y) B : forall p y . p (D (S y) Z) => p (D Z y) proof declarations g : forall d . (forall p x y . p (d x (S y)) => p (d (S x) y)) => (forall p y . p (d (S y) Z) => p (d Z y)) => d Z Z = \ a1 a2 . a2 (a1 (g (\ v . a1 v) (\ v . a2 (a1 v)))) e : D Z Z = g (\ v . A v) (\ v . B v) lemmas e : D Z Z = g (\ m1’ m2’ . D m1’ m2’) (\ p1’ x2’ y3’ (v : p1’ (D x2’ (S y3’))) . A (\ m1’ . p1’ m1’) x2’ y3’ v) (\ p7’ y8’ (v : p7’ (D (S y8’) Z)) . B (\ m1’ . p7’ m1’) y8’ v) g : forall d . (forall p x y . p (d x (S y)) => p (d (S x) y)) => (forall p y . p (d (S y) Z) => p (d Z y)) => d Z Z = \ d0’ (a1 : forall p x y . p (d0’ x (S y)) => p (d0’ (S x) y)) (a2 : forall p y . p (d0’ (S y) Z) => p (d0’ Z y)) . a2 (\ x1’ . x1’) Z (a1 (\ x1’ . x1’) Z Z (g (\ m1’ m2’ . d0’ m1’ (S m2’)) (\ p7’ x8’ y9’ (v : p7’ (d0’ x8’ (S (S y9’)))) . a1 (\ m1’ . p7’ m1’) x8’ (S y9’) v) (\ p13’ y14’ (v : p13’ (d0’ (S y14’) (S Z))) . a2 (\ m1’ . p13’ m1’) (S y14’) (a1 (\ m1’ . p13’ m1’) (S y14’) Z v)))) steps automated proof reconstruction success!

The lemmas section contains the annotated evidence. All variables generated by FCR are variables end with “ ’ ”. All lambda-bound evidence variables are annotated with the type information. This is needed for decidable proof checking, we do not need to annotate lambda-bound type variables. The annotated evidence generated by our type checker is checked by a separate $\mathbf{F}_{2}^{\mu}$ proof checker.

We can translated the input file into the following Haskell code, but it will not pass Haskell’s type checker.

data D :: * -> * -> * data S :: * -> * data Z :: * a :: forall p x y . p (D x (S y)) -> p (D (S x) y) a = undefined b :: forall p y . p (D (S y) Z) -> p (D Z y) b = undefined g :: forall d . (forall p x y . p (d x (S y)) -> p (d (S x) y)) -> (forall p y . p (d (S y) Z) -> p (d Z y)) -> d Z Z g a1 a2 = a2 (a1 (g (\ v -> a1 v) (\ v -> a2 (a1 v))))

e :: D Z Z e = g (\ v -> a v) (\ v -> b v)

H.2 Example in Section 6

The following is the input file for FCR.

Ka : A x <= A (B x) Kb : B x <= A x

g : forall a b x . (forall p y . p (a (b y)) => p (a y)) => (forall p y . p (a y) => p (b y)) => a x

g a b = a (g (\ v . a (b v)) (\ v . a v))

h : A x h = g (\ v . Ka v) Kb

step h 20

We use the alternative notation A x <= A (B x) to represent the rewrite rule from A x to A (B x), it will be translated to its Leibniz representation by FCR. And step h 20 is a command telling FCR to output the 20th first-order term in the reduction h began with term A x. The following is the output information.

rewrite rules Ka : A x <= A (B x) Kb : B x <= A x kinds A : * => * B : * => * axioms Ka : forall p x . p (A (B x)) => p (A x) Kb : forall p x . p (A x) => p (B x) proof declarations g : forall a b x . (forall p y . p (a (b y)) => p (a y)) => (forall p y . p (a y) => p (b y)) => a x = \ a b . a (g (\ v . a (b v)) (\ v . a v)) h : A x = g (\ v . Ka v) Kb lemmas h : A x = g (\ m1’ . A m1’) (\ m1’ . B m1’) x (\ p3’ y4’ (v : p3’ (A (B y4’))) . Ka (\ m1’ . p3’ m1’) y4’ v) Kb g : forall a b x . (forall p y . p (a (b y)) => p (a y)) => (forall p y . p (a y) => p (b y)) => a x = \ a0’ b1’ x2’ (a : forall p y . p (a0’ (b1’ y)) => p (a0’ y)) (b : forall p y . p (a0’ y) => p (b1’ y)) . a (\ x1’ . x1’) x2’ (g (\ m1’ . a0’ (b1’ m1’)) (\ m1’ . a0’ m1’) x2’ (\ p8’ y9’ (v : p8’ (a0’ (b1’ (a0’ y9’)))) . a (\ m1’ . p8’ m1’) (b1’ y9’) (b (\ m1’ . p8’ (a0’ (b1’ m1’))) y9’ v)) (\ p14’ y15’ (v : p14’ (a0’ (b1’ y15’))) . a (\ m1’ . p14’ m1’) y15’ v)) steps step h 20 automated proof reconstruction success! steps results A (B (A (A (B (A (B (A (A (B (A (A (B x))))))))))))

We can check that the term A (B (A (A (B (A (B (A (A (B (A (A (B x)))))))))))) represents the string we obtain in the very end of the string reduction trace in Section 6. Note that this term is obtained directly from the unfolding of the reduction trace without invoking any term rewriting reduction.

Appendix I Solving the Scope Problem in ERSM and the Soundness of ERSM

Due to lack of space, we did not explain nor discuss the soundness of ERSM in Section 6. In fact, the ERSM is not sound in its current form due to a subtle scope problem. We will show how to solve this soundness problem in this section. To explain the scope problem, let us consider the following two formulas.

(I) forall p x y . p (G (F Z x (S y)) (F x y (S (S Z)))) => p (F Z (S x) y)

(II) forall p x y . p (qa (F Z x (S y))) => p (F Z (S x) y)

It may appear that these two formulas are second-orderly unifiable if we instantiate qa in (II) to \m . G m (F x y (S (S Z))). But this instantiation assumes the variable x, y in \m . G m (F x y (S (S Z))) can be automatically captured by the forall binder in (II), this is not a correct assumption. In fact (I) and (II) are not unifiable, this kind of problem is called scope problem by Dowek [7, Section 5].

The solution of the scope problem is conceptually simple, i.e. we just need to prevent the instantiation of the existential variables when there is such a scope problem. However, to implement this solution within the ERSM framework requires some efforts.

We works with idempotent substitution, i.e. for a substitution $\sigma$, we require that $\sigma\cdot\sigma=\sigma$. Idemptentness is easy to check, due to the following property [2]: $\sigma$ is idempotent iff $\mathrm{dom}(\sigma)\cap\mathrm{FV}(\mathrm{codom}(\sigma))=\emptyset$. This requirement is needed in order to prove the soundness theorem.

Definition I.1**.**

Let $L$ denote a list of variables. We define $y\sqsubset_{L}x$ if $L=L_{1},y,L_{2},x,L_{3}$ for some $L_{1},L_{2},L_{3}$. We define $\mathsf{scope}(L,\sigma)$ to be the conjunction of the following two predicates: (1) $\forall x\in\mathrm{dom}(\sigma)\cap L,\forall y\in\mathrm{FV}(\sigma{x}),y\sqsubset_{L}{x}$. (2) $\forall x\in\mathrm{dom}(\sigma)-L,\mathrm{FV}(\sigma x)\cap L=\emptyset$.

Let $\Phi$ denotes a set of tuple $(L,\Gamma,e,T)$. We use $\sigma L$ to denote $L-\mathrm{dom}(\sigma)$ and we use $L+L^{\prime}$ to mean appending $L,L^{\prime}$.

Definition I.2**.**

$\sigma\Gamma,\sigma\Phi$**

$\sigma\cdot=\cdot$**

$\sigma[\alpha:T,\Gamma]=\alpha:\sigma T,\sigma\Gamma$**

$\sigma[\kappa:T,\Gamma]=\kappa:\sigma T,\sigma\Gamma$**

$\sigma\{\}=\{\}$**

$\sigma\ \{(L,\Gamma,e,T),\Phi\}=\{(\sigma L,\sigma\Gamma,e,\sigma T),\sigma\Phi\}$, where $\mathsf{scope}(L,\sigma)$.

Let $S$ be a set of variables, we write $\sigma/S=[t/x\ |\ x\in(\mathrm{dom}(\sigma)-S)]$.

Definition I.3** (ERSM with Scope Check).**

$(\Phi,\sigma)\longrightarrow(\Phi^{\prime},\sigma^{\prime})$**

$(\{(L,\Gamma,(\kappa|\alpha)\ e_{1}\ ...\ e_{n},A),\Phi\},\sigma)\longrightarrow_{a}(\{(L^{\prime},\sigma^{\prime\prime}\Gamma,e_{1},\sigma^{\prime}T_{1}),...,(L^{\prime},\sigma^{\prime\prime}\Gamma,e_{1},\sigma^{\prime}T_{n}),\sigma^{\prime\prime}\Phi\},\sigma^{\prime\prime}\cdot\sigma)$**

if $\kappa|\alpha:\forall x_{1}....\forall x_{m}.T_{1},...,T_{n}\Rightarrow B\in\Gamma$ with $B\mapsto_{\sigma^{\prime}}A$. Moreover, $\sigma^{\prime\prime}=\sigma^{\prime}/\{x_{1},...,x_{m}\}$, $\mathsf{scope}(L,\sigma^{\prime\prime})$ and $L^{\prime}=\sigma^{\prime\prime}L+[x_{i}\ |\ x_{i}\notin\mathrm{FV}(B),1\leq i\leq m]$. 2. 2.

$(\{(L,\Gamma,\lambda\alpha_{1}....\lambda\alpha_{n}.e,T_{1},...,T_{n}\Rightarrow A),\Phi\},\sigma)\longrightarrow_{i}(\{(L,[\Gamma,\alpha_{1}:T_{1},...,\alpha_{n}:T_{n}],e,A),\Phi\},\sigma)$. 3. 3.

$(\{(L,\Gamma,e,\forall x_{1}...\forall x_{n}.T),\Phi\},\sigma)\longrightarrow_{\forall}(\{([L,x_{1},...,x_{n}],\Gamma,e,T),\Phi\},\sigma)$. 4. 4.

$(\{(L,\Gamma,\mu\alpha.e,T),\Phi\},\sigma)\longrightarrow_{c}(\{(L,[\Gamma,\alpha:T],e,T),\Phi\},\sigma)$.

We can see if we eliminate $L$ and $\mathsf{scope}(L,\sigma)$, we can obtain ERSM described in the paper.

Lemma I.4**.**

If $\Gamma\vdash e:T$, then $\sigma\Gamma\vdash\sigma e:\sigma T$.

If $S$ is a set of variables, we define $\sigma S:=\{\sigma x|\ x\in S\}$. Moreover, we extend $\mathrm{FV}$ function to obtain all the free variables of a set of terms. Note that all the substitutions are idempotent and disjoint , i.e. $\mathrm{FV}(\mathrm{codom}(\sigma))\cap\mathrm{dom}(\sigma)=\emptyset$ for any $\sigma$ and $\mathrm{dom}(\sigma_{1})\cap\mathrm{dom}(\sigma_{2})=\emptyset,$ for any $\sigma_{1},\sigma_{2}$.

Lemma I.5** (Scope Check Composition).**

Suppose $\mathrm{FV}(\mathrm{codom}(\sigma_{2}))\cap\mathrm{dom}(\sigma_{1})=\emptyset$. If $\mathsf{Scope}(L,\sigma_{1})$ and $\mathsf{Scope}(\sigma_{1}L+L^{\prime},\sigma_{2})$ for some fresh $L^{\prime}$, then $\mathsf{Scope}(L,\sigma_{2}\cdot\sigma_{1})$.

Proof I.6**.**

• •

Case $y\in\mathrm{dom}(\sigma_{2}\cdot\sigma_{1})-L$.

We need to show $\mathrm{FV}(\sigma_{2}\sigma_{1}y)\cap L=\emptyset$, i.e. $\mathrm{FV}(\sigma_{2}(\mathrm{FV}(\sigma_{1}y)))\cap L=\emptyset$. We know that $\mathrm{dom}(\sigma_{2}\cdot\sigma_{1})=\mathrm{dom}(\sigma_{2})\uplus\mathrm{dom}(\sigma_{1})$. Suppose $y\in\mathrm{dom}(\sigma_{1})$, we know that $\mathrm{FV}(\sigma_{1}y)\cap L=\emptyset$. For any $z\in\mathrm{FV}(\sigma_{1}y)\cap\mathrm{dom}(\sigma_{2})$, we have $\mathrm{FV}(\sigma_{2}z)\cap(\sigma_{1}L+L^{\prime})=\emptyset$, which implies $\mathrm{FV}(\sigma_{2}z)\cap L=\emptyset$. For any $z\in\mathrm{FV}(\sigma_{1}y)-\mathrm{dom}(\sigma_{2})$, we have $\mathrm{FV}(\sigma_{2}z)=\{z\},\{z\}\cap L=\emptyset$. Suppose $y\in\mathrm{dom}(\sigma_{2})$, we need to show $\mathrm{FV}(\sigma_{2}y)\cap L=\emptyset$, this is the case since $\mathrm{FV}(\sigma_{2}y)\cap(\sigma_{1}L+L^{\prime})=\emptyset$ and $\mathrm{FV}(\mathrm{codom}(\sigma_{2}))\cap\mathrm{dom}(\sigma_{1})=\emptyset$.

• •

Case. $y\in\mathrm{dom}(\sigma_{2}\cdot\sigma_{1})\cap L$.

We need to show for any $z\in\mathrm{FV}(\sigma_{2}(\mathrm{FV}(\sigma_{1}y)))\cap L$, $z\sqsubset_{L}y$. Let $x\in\mathrm{FV}(\sigma_{1}y)$, we just need to show for any $z\in\mathrm{FV}(\sigma_{2}x)\cap L$, $z\sqsubset_{L}y$. Suppose $x\notin\mathrm{dom}(\sigma_{2})$. Then $\mathrm{FV}(\sigma_{2}x)=\{x\}$. So $x\sqsubset_{L}y$ if $x\in L$. Suppose $x\in\mathrm{dom}(\sigma_{2})\cap L$, we know that $(\mathrm{FV}(\sigma_{2}x)\cap(\sigma_{1}L+L^{\prime}))\sqsubset_{\sigma_{1}L+L^{\prime}}x$. Since $z\in\mathrm{FV}(\sigma_{2}x)\cap L$ implies $z\in\mathrm{FV}(\sigma_{2}x)\cap(\sigma_{1}L+L^{\prime})$, we have $z\sqsubset_{\sigma_{1}L+L^{\prime}}x\sqsubset_{L}y$. Since $x\notin L^{\prime}$ and $x\notin\mathrm{dom}(\sigma_{1})$, we have $z\sqsubset_{L}x\sqsubset_{L}y$. Suppose $x\in\mathrm{dom}(\sigma_{2})-L$, then $x\in\mathrm{dom}(\sigma_{2})-(\sigma_{1}L+L^{\prime})$, thus $\mathrm{FV}(\sigma_{2}x)\cap(\sigma_{1}L+L^{\prime})=\emptyset$, which implies $\mathrm{FV}(\sigma_{2}x)\cap L=\emptyset$.

Suppose $y\in\mathrm{dom}(\sigma_{2})$, we just need to show for any $z\in\mathrm{FV}(\sigma_{2}y)\cap L$, $z\sqsubset_{L}y$. Since $z\notin\mathrm{dom}(\sigma_{1})$, we have $z\in\mathrm{FV}(\sigma_{2}y)\cap(\sigma_{1}L+L^{\prime})$. Thus $z\sqsubset_{\sigma_{1}L+L^{\prime}}y$, which implies $z\sqsubset_{L}y$.

Lemma I.7** (Scope Invariant).**

If $(\{(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{n},\Gamma_{n},e_{n},T_{n})\},\sigma)\longrightarrow(\{(L_{1}^{\prime},\Gamma_{1}^{\prime},e_{1}^{\prime},T_{1}^{\prime}),...,(L_{m}^{\prime},\Gamma_{m}^{\prime},e_{m}^{\prime},T_{m}^{\prime})\},\sigma^{\prime}\cdot\sigma)$, then $\mathsf{Scope}(L_{i},\sigma^{\prime})$ for all $i$. 2. 2.

If $(\{(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{n},\Gamma_{n},e_{n},T_{n})\},\sigma)\longrightarrow^{*}(\{(L_{1}^{\prime},\Gamma_{1}^{\prime},e_{1}^{\prime},T_{1}^{\prime}),...,(L_{m}^{\prime},\Gamma_{m}^{\prime},e_{m}^{\prime},T_{m}^{\prime})\},\sigma^{\prime}\cdot\sigma)$, then $\mathsf{Scope}(L_{i},\sigma^{\prime})$ for all $i$.

Proof I.8**.**

By Lemma I.5 and induction.

Lemma I.9**.**

If $(\{(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{n},\Gamma_{n},e_{n},T_{n})\},\sigma)\longrightarrow^{*}(\emptyset,\sigma^{\prime}\cdot\sigma)$ for some $\sigma^{\prime}$, then $\sigma^{\prime}\Gamma_{i}\vdash e_{i}^{\prime}:\sigma^{\prime}T_{i}$ and $|e_{i}^{\prime}|=e_{i}$ for all $i$.

Proof I.10**.**

By induction on the length of $(\{(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{n},\Gamma_{n},e_{n},T_{n})\},\sigma)$ $\longrightarrow^{*}(\sigma^{\prime}\cdot\sigma,\emptyset)$.

• •

Case $(\{(L,\Gamma,\alpha|\kappa,A)\},\sigma)\longrightarrow_{a}(\emptyset,\sigma^{\prime\prime}\cdot\sigma)$.

In this case $\alpha|\kappa:\forall\underline{x}.B\in\Gamma$, $\sigma^{\prime\prime}=\sigma^{\prime}/\{\underline{x}\}$, $\mathsf{scope}(L,\sigma^{\prime\prime})$ and $B\mapsto_{\sigma^{\prime}}A$. By Inst rule and the idempotentness of $\sigma^{\prime}$, we have $\sigma^{\prime\prime}\Gamma\vdash(\alpha|\kappa)\ (\sigma^{\prime}\underline{x}):\sigma^{\prime}B\equiv\sigma^{\prime\prime}\sigma^{\prime}B=\sigma^{\prime\prime}A$, where $|(\alpha|\kappa)\ (\sigma^{\prime}\underline{x})|=\alpha|\kappa$.

• •

Case $(\{(L,\Gamma,(\alpha|\kappa)\ e^{\prime\prime}_{1}\ ...e_{m}^{\prime\prime},A),(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{n},\Gamma_{n},e_{n},T_{n})\},\sigma)\longrightarrow_{a}$

$(\{(L^{\prime},\sigma^{\prime}\Gamma,e_{1}^{\prime\prime},\sigma_{1}T_{1}^{\prime}),...,(L^{\prime},\sigma^{\prime}\Gamma,e_{m}^{\prime\prime},\sigma_{1}T_{m}^{\prime}),(\sigma^{\prime}L_{1},\sigma^{\prime}\Gamma_{1},e_{1},\sigma^{\prime}T_{1}),...,(\sigma^{\prime}L_{n},\sigma^{\prime}\Gamma_{n},e_{n},\sigma^{\prime}T_{n})\},\sigma^{\prime}\cdot\sigma)\longrightarrow^{*}(\emptyset,\sigma^{\prime\prime}\cdot\sigma^{\prime}\cdot\sigma)$,

where $\kappa|\alpha:\forall\underline{x}.T_{1}^{\prime},...,T_{n}^{\prime}\Rightarrow B\in\Gamma$ with $B\mapsto_{\sigma_{1}}A$, $\sigma^{\prime}=\sigma_{1}/\{\underline{x}\}$, $\mathsf{scope}(L,\sigma^{\prime})$ and $L^{\prime}=\sigma^{\prime}L+[x_{i}\ |\ x_{i}\notin\mathrm{FV}(B),1\leq i\leq m]$.

By IH, we know that $\sigma^{\prime\prime}\sigma^{\prime}\Gamma^{\prime}\vdash e_{1}^{\prime\prime\prime}:\sigma^{\prime\prime}\sigma_{1}T_{1}^{\prime},...,\sigma^{\prime\prime}\sigma^{\prime}\Gamma^{\prime}\vdash e_{m}^{\prime\prime\prime}:\sigma^{\prime\prime}\sigma_{1}T_{m}^{\prime},\sigma^{\prime\prime}\sigma^{\prime}\Gamma_{1}\vdash e_{1}^{\prime}:\sigma^{\prime\prime}\sigma^{\prime}T_{1},...,\sigma^{\prime\prime}\sigma^{\prime}\Gamma_{n}\vdash e_{n}^{\prime}:\sigma^{\prime\prime}\sigma^{\prime}T_{n}$ and $|e_{1}^{\prime\prime\prime}|=e_{1}^{\prime\prime},...,|e_{m}^{\prime\prime\prime}|=e_{m}^{\prime\prime},|e_{1}^{\prime}|=e_{1},...,|e_{n}^{\prime}|=e_{n}$. We have $\sigma^{\prime\prime}\sigma^{\prime}\Gamma\vdash(\alpha|\kappa)\ (\sigma^{\prime\prime}\sigma^{\prime}\underline{x}):\sigma^{\prime\prime}\sigma_{1}T_{1}^{\prime},...,\sigma^{\prime\prime}\sigma_{1}T_{n}^{\prime}\Rightarrow\sigma^{\prime\prime}\sigma_{1}B$. By Conv, App and idempotentness, we have $\sigma^{\prime\prime}\sigma^{\prime}\Gamma\vdash(\alpha|\kappa)\ (\sigma^{\prime\prime}\sigma^{\prime}\underline{x})\ e_{1}^{\prime\prime\prime}\ ...\ e_{m}^{\prime\prime\prime}:\sigma^{\prime\prime}\sigma_{1}B=\sigma^{\prime\prime}\sigma^{\prime}A$. Moreover, $|(\alpha|\kappa)\ (\sigma^{\prime\prime}\sigma^{\prime}\underline{x})\ e_{1}^{\prime\prime\prime}\ ...\ e_{m}^{\prime\prime\prime}|=(\alpha|\kappa)\ |e_{1}^{\prime\prime\prime}|\ ...\ |e_{m}^{\prime\prime\prime}|=(\alpha|\kappa)\ e_{1}^{\prime\prime}\ ...\ e_{m}^{\prime\prime}$.

• •

*Case

$(\{(L,\Gamma,\lambda\alpha_{1}....\lambda\alpha_{n}.e,T_{1},...,T_{n}\Rightarrow A),(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{l},\Gamma_{l},e_{l},T_{l})\},\sigma)$ $\longrightarrow_{i}(\{(L,[\Gamma,\alpha_{1}:T_{1},...,\alpha_{n}:T_{n}],e,A),(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{l},\Gamma_{l},e_{l},T_{l})\},\sigma)\longrightarrow^{*}(\emptyset,\sigma^{\prime}\cdot\sigma)$*

By IH, we have $\sigma^{\prime}\Gamma,\alpha_{1}:\sigma^{\prime}T_{1},...,\alpha_{n}:\sigma^{\prime}T_{n}\vdash e^{\prime}:\sigma^{\prime}A,\sigma^{\prime}\Gamma_{1}\vdash e_{1}^{\prime}:\sigma^{\prime}T_{1},...,\sigma^{\prime}\Gamma_{l}\vdash e_{l}^{\prime}:\sigma^{\prime}T_{l}$ with $|e^{\prime}|=e,|e_{1}^{\prime}|=e_{1},...,|e_{l}^{\prime}|=e_{l}$. Thus by Lam rule, we have $\sigma^{\prime}\Gamma\vdash\lambda\alpha_{1}....\lambda\alpha_{n}.e^{\prime}:\sigma^{\prime}T_{1},...,\sigma^{\prime}T_{n}\Rightarrow\sigma^{\prime}A$ and $|\lambda\alpha_{1}....\lambda\alpha_{n}.e^{\prime}|=\lambda\alpha_{1}....\lambda\alpha_{n}.e$.

• •

*Case

$(\{(L,\Gamma,e,\forall x_{1}....\forall x_{m}.T),(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{l},\Gamma_{l},e_{l},T_{l})\},\sigma)\longrightarrow_{\forall}$*

$(\{([L,x_{1},...,x_{m}],\Gamma,e,T),(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{l},\Gamma_{l},e_{l},T_{l})\},\sigma)\longrightarrow^{*}(\emptyset,\sigma^{\prime}\cdot\sigma)$**

By IH, we have $\sigma^{\prime}\Gamma\vdash e^{\prime}:\sigma^{\prime}T,\sigma^{\prime}\Gamma_{1}\vdash e_{1}^{\prime}:\sigma^{\prime}T_{1},...,\sigma^{\prime}\Gamma_{l}\vdash e_{l}^{\prime}:\sigma^{\prime}T_{l}$ with $|e^{\prime}|=e,|e_{1}^{\prime}|=e_{1},...,|e_{l}^{\prime}|=e_{l}$. By Lemma I.7 (2), $\mathsf{scope}([L,x_{1},...,x_{m}],\sigma^{\prime})$. So $\mathrm{FV}(\mathrm{codom}(\sigma^{\prime}))\cap\{x_{1},...,x_{m}\}=\emptyset$. Thus by Abs rule, we have $\sigma^{\prime}\Gamma\vdash\lambda x_{1}....\lambda x_{m}.e^{\prime}:\forall x_{1}....\forall x_{m}.\sigma^{\prime}T=\sigma^{\prime}(\forall x_{1}....\forall x_{m}.T)$ and $|\lambda x_{1}....\lambda x_{m}.e^{\prime}|=e$.

• •

Case $(\{(L,\Gamma,\mu\alpha.e,T),(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{n},\Gamma_{n},e_{n},T_{n})\},\sigma)\longrightarrow_{c}$

$(\{(L,[\Gamma,\alpha:T],e,T),(L_{1},\Gamma_{1},e_{1},T_{1}),...,(L_{n},\Gamma_{n},e_{n},T_{n})\},\sigma)\longrightarrow^{*}(\emptyset,\sigma^{\prime}\cdot\sigma)$**

By IH, we know that $\sigma^{\prime}\Gamma,\alpha:\sigma^{\prime}T\vdash e^{\prime}:\sigma^{\prime}T,\sigma^{\prime}\Gamma_{1}\vdash e_{1}^{\prime}:\sigma^{\prime}T_{1},...,\sigma^{\prime}\Gamma_{n}\vdash e_{n}^{\prime}:\sigma^{\prime}T_{n}$ and $|e_{i}^{\prime}|=e_{i}$ for all $i$. By Mu rule, we have $\sigma^{\prime}\Gamma\vdash\mu\alpha.e^{\prime}:\sigma^{\prime}T$. Thus $|\mu\alpha.e^{\prime}|=\mu\alpha.e$.

Theorem I.11** (Soundness of ERSM).**

If $(\{([],\Gamma,e,T)\},\mathrm{id})\longrightarrow^{*}(\emptyset,\sigma)$ and $\mathrm{FV}(\Gamma)=\mathrm{FV}(T)=\emptyset$, then $\Gamma\vdash e^{\prime}:T$ and $|e^{\prime}|=e$.

Proof I.12**.**

By Lemma I.9.

We now can understand the error message when we try to type check the following declarations in FCR.

K : forall p x y . p (G (F Z x (S y)) (F x y (S (S Z)))) => p (F Z (S x) y)

K2 : forall qa . (forall p x y . p (qa (F Z x (S y))) => p (F Z (S x) y)) => B

h : B h = K2 (\ c . K c)

Note that type checking h will give a scope problem as (I) and (II) above does not unify. FCR will print out the following message.

scope error when matching [p1’] (qa0’ (F Z [x2’] (S [y3’]))) against [p1’] (G (F Z [x2’] (S [y3’])) (F [x2’] [y3’] (S (S Z)))) when applying c : [p1’] (qa0’ (F Z [x2’] (S [y3’]))) when applying substitution [ qa0’ : \ m1’ . G m1’ (F [x2’] [y3’] (S (S Z))) ] current variables list: qa0’ p1’ x2’ y3’ the current mixed proof term: K2 qa0’ (\ p1’ x2’ y3’ (c : [p1’] (qa0’ (F Z [x2’] (S [y3’])))) . K (\ m1’ . [p1’] m1’) [x2’] [y3’] ([p1’] (G (F Z [x2’] (S [y3’])) (F [x2’] [y3’] (S (S Z))))))

The eigenvariables are the variables surrounded by brackets, and the substitution $[t/x]$ is represented as [x : t]. In this case the FCR will try to instantiate the existential variable qa0’ with \m1’ . G m1’ (F [x2’] [y3’] (S (S Z))). The $L$ is the current variables list for the $\mathsf{scope}$ function, we can see the substitution will not pass the scope check. Moreover, we can inspect the mix proof term, we see that qa0’ is not in the scope of [x2’], [y3’]. Thus the function h gives a typing error.

Appendix J Examples from Term Rewriting Literature

We demonstrate how to use the prototype FCR to represent some nontrivial nonterminations in this section. All of the examples in this section are from the existing term rewriting literature, and we will focus on representing nonlooping nonterminating reductions.

The general idea of representing a nonterminating reduction trace is the following: we need to see if the rule sequence can be generated by a corecursive function. Then we will try to assign a type for the corecursive function. Most of the efforts will be put on abstracting the right universal and existential type variables. Obtaining the right type for the corecursive function usually requires interactions with FCR and a good understanding of the type checking algorithm ERSM.

J.1

The following string rewriting system is from Endrullis and Zantema [9], Example 29.

$AL\to_{1}LA$  $RA\to_{2}AR$ $BL\to_{3}BR$ $RB\to_{4}LAB$

Observe the following nonlooping nonterminating reduction:

$\underline{BL}B\to_{3}B\underline{RB}\to_{4}\underline{BL}AB\to_{3}B\underline{RA}B\to_{2}BA\underline{RB}\to_{4}B\underline{AL}AB\to_{1}\underline{BL}AAB\to_{3}B\underline{RA}AB\to_{2}BA\underline{RA}B\to_{2}BAA\underline{RB}\to_{4}BA\underline{AL}AB\to_{1}B\underline{AL}AAB\to_{1}\underline{BL}AAAB\to_{3}...$

Observe that all the strings in the reduction can be described by the regular expression $BA^{*}(L|R)A^{*}B$. We focus on the rule sequence: $\underline{3}4\underline{32}41\underline{322}411....$. The rule sequence can be generated by the following corecursive function: $f\ a_{1}\ a_{2}\ a_{3}\ a_{4}=a_{3}\cdot a_{4}\cdot(f\ a_{1}\ a_{2}\ (a_{3}\cdot a_{2})\ (a_{4}\cdot a_{1}))$, i.e. $f\ 1\ 2\ 3\ 4$ gives the rule sequence.

The term rewriting system corresponds to the above string rewriting system is the following.

$A\ (L\ x)\to_{1}L\ (A\ x)$  $R\ (A\ x)\to_{2}A\ (R\ x)$ $B\ (L\ x)\to_{3}B\ (R\ x)$ $R\ (B\ x)\to_{4}L\ (A\ (B\ x))$

The following is the type assignment for the function $f$, where the variable r is an existential variable and will be instantiated by (\m1’ . A (r2’ m1’)) at the corecursive call of f.

K1 : A (L x) <= L (A x) K2 : R (A x) <= A (R x) K3 : B (L x) <= B (R x) K4 : R (B x) <= L (A (B x))

f : forall p l r y . (forall p x . p (l (A x)) => p (A (l x))) => (forall p x . p (A (r x)) => p (r (A x))) => (forall p x . p (B (r x)) => p (B (l x))) => (forall p x . p (l (A (B x))) => p (r (B x))) => p (B (l (B y)))

f a1 a2 a3 a4 = a3 (a4 (f (\ c . a1 c) (\ c . a2 c) (\ c . a3 (a2 c)) (\ c . a4 (a1 c))))

h : B (L (B y)) h = f K1 K2 (\ c . K3 c) K4

J.2

The following string rewriting system is from Endrullis and Zantema [9], Example 34.

$ZL\to_{1}LZ$  $RZ\to_{2}ZR$ $ZLL\to_{3}ZLR$ $RRZ\to_{4}LZRZ$

Observe the following nonlooping nonterminating reduction:

$\underline{ZLL}ZZRZ\to_{3}ZL\underline{RZ}ZRZ\to_{2}ZLZ\underline{RZ}RZ\to_{2}ZLZZ\underline{RRZ}\to_{4}ZLZ\underline{ZL}ZRZ\to_{1}ZL\underline{ZL}ZZRZ\to_{1}\underline{ZLL}ZZZRZ\to_{3}ZL\underline{RZ}ZZRZ\to_{2}\cdot\to_{2}\cdot\to_{2}ZLZZZ\underline{RRZ}\to_{4}ZLZZ\underline{ZL}ZRZ\to_{1}\cdot\to_{1}\cdot\to_{1}\underline{ZLL}ZZZZRZ\to_{3}...$

Observe the rule sequence: $32241132224111....$. This rule sequence can be generated by the following corecursive function: $f\ a_{1}\ a_{2}\ a_{3}\ a_{4}=a_{3}\cdot a_{2}\cdot a_{2}\cdot a_{4}\cdot a_{1}\cdot a_{1}\cdot(f\ a_{1}\ a_{2}\ (a_{3}\cdot a_{2})\ (a_{4}\cdot a_{1}))$, i.e. $f\ 1\ 2\ 3\ 4$ gives the rule sequence.

The term rewriting system corresponds to the above string rewriting system is the following.

$Z\ (L\ x)\to_{1}L\ (Z\ x)$  $R\ (Z\ x)\to_{2}Z\ (R\ x)$ $Z\ (L\ (L\ x))\to_{3}Z\ (L\ (R\ x))$ $R\ (R\ (Z\ x))\to_{4}L\ (Z\ (R\ (Z\ x)))$

The following is the type that we assign to $f$. The existential variable r is instantiated by (\m1’ . Z (r2’ m1’)) at the corecursive call of f.

K1 : Z (L x) <= L (Z x) K2 : R (Z x) <= Z (R x) K3 : Z (L (L x)) <= Z (L (R x)) K4 : R (R (Z x)) <= L (Z (R (Z x)))

f : forall p l r y . (forall p x . p (l (Z x)) => p (Z (l x))) => (forall p x . p (Z (r x)) => p (r (Z x))) => (forall p x . p (Z (L (r x))) => p (Z (L (l x)))) => (forall p x . p (l (Z (R (Z x)))) => p (r (R (Z x)))) => p (Z (L (l (Z (Z (R (Z y)))))))

f a1 a2 a3 a4 = a3 (a2 (a2 (a4 (a1 (a1 (f (\ c . a1 c) (\ c . a2 c) (\ c . a3 (a2 c)) (\ c . a4 (a1 c))))))))

h : (Z (L (L (Z (Z (R (Z y))))))) h = f K1 K2 (\ c . K3 c) K4

J.3

The following string rewriting system is from Endrullis and Zantema [9], Example 33.

$AAL\to_{1}LAA$  $RA\to_{2}AR$ $BL\to_{3}BR$ $RB\to_{4}LAB$ $RB\to_{5}ALB$

Observe the following nonlooping nonterminating reduction:

$B\underline{RB}\to_{4}\underline{BL}AB\to_{3}B\underline{RA}B\to_{2}BA\underline{RB}\to_{5}B\underline{AAL}B\to_{1}\underline{BL}AAB\to_{3}B\underline{RA}AB\to_{2}\cdot\to_{2}BAA\underline{RB}\to_{4}B\underline{AAL}AB\to_{1}\underline{BL}AAAB\to_{3}B\underline{RA}AAB\to_{2}\cdot\to_{2}\cdot\to_{2}BAAA\underline{RB}\to_{5}BAA\underline{AAL}B\to_{1}\cdot\to_{1}\underline{BL}AAAAB\to_{3}B\underline{RA}AAAB\to_{2}\cdot\to_{2}\cdot\to_{2}\cdot\to_{2}BAAAA\underline{RB}\to_{4}...$

Observe the rule sequence: $43251322,41322251132222,41132222251113222222....$ This rule sequence can be generated by the following corecursive function: $f\ a_{1}\ a_{2}\ a_{3}\ a_{4}\ a_{5}=a_{4}\cdot a_{3}\cdot a_{2}\cdot a_{5}\cdot a_{1}\cdot a_{3}\cdot a_{2}\cdot a_{2}\cdot(f\ a_{1}\ a_{2}\ (a_{3}\cdot a_{2}\cdot a_{2})\ (a_{4}\cdot a_{1})\ (a_{5}\cdot a_{1}))$, i.e. $f\ 1\ 2\ 3\ 4\ 5$ gives the rule sequence.

The term rewriting system corresponds to the above string rewriting system is the following.

$A\ (A\ (L\ x))\to_{1}L\ (A\ (A\ x))$  $R\ (A\ x)\to_{2}A\ (R\ x)$ $B\ (L\ x)\to_{3}B\ (R\ x)$ $R\ (B\ x)\to_{4}L\ (A\ (B\ x))$ $R\ (B\ x)\to_{5}A\ (L\ (B\ x))$

We assign a type for $f$ in the following. The existential variable l is instantiated with (\m1’ . l1’ (A (A m1’))) at the corecursive call of f.

K1 : A (A (L x)) <= L (A (A x)) K2 : R (A x) <= A (R x) K3 : B (L x) <= B (R x) K4 : R (B x) <= L (A (B x)) K5 : R (B x) <= A (L (B x))

f : forall p l r y . (forall p x . p (l (A (A x))) => p (A (A (l x)))) => (forall p x . p (A (r x)) => p (r (A x))) => (forall p x . p (B (r x)) => p (B (l x))) => (forall p x . p (l (A (B x))) => p (r (B x))) => (forall p x . p (A (l (B x))) => p (r (B x))) => p (B (r (B y)))

f a1 a2 a3 a4 a5 = a4 (a3 (a2 (a5 (a1 (a3 (a2 (a2 (f (\ c . a1 c) (\ c . a2 c) (\ c . a3 (a2 (a2 c))) (\ c . a4 (a1 c)) (\ c . a5 (a1 c))))))))))

h : B (R (B y)) h = f K1 K2 K3 (\ c . K4 c) K5

J.4

Consider the following rewriting system (from Zantema and Geser [26]) :

$F\ Z\ (S\ x)\ y\to_{a}F\ Z\ x\ (S\ y)$

$F\ Z\ (S\ x)\ y\to_{b}F\ x\ y\ (S\ (S\ Z))$

Observe the following nonlooping reduction trace.

$F\ Z\ (S\ Z)\ (S\ Z)\to_{b}F\ Z\ (S\ Z)\ (S\ (S\ Z))\to_{b}F\ Z\ (S\ (S\ Z))\ (S\ (S\ Z))\to_{a}F\ Z\ (S\ Z)\ (S\ (S\ (S\ Z)))\to_{b}F\ Z\ (S\ (S\ (S\ Z)))\ (S\ (S\ Z))\to_{a}...$

Note that the rule sequence for this reduction is: bbabaabaaab….. The nontermination can only be observed via the full reduction tree. The following partial reduction tree produced by FCR is an infinite binary tree structure with each branch finite (by issuing command :full 6 (F Z (S Z) (S Z)) to FCR). Each node is a triple (e.g. [], B, F Z (S Z) (S (S Z))), the first element denotes the redex position of the parent (which is a list of number, but all of them are at root position, hence []), second element denotes the label of the rewrite rule applied, the third element denotes the contractum.

[], _, F Z (S Z) (S Z) | +- [], B, F Z (S Z) (S (S Z)) | | | +- [], B, F Z (S (S Z)) (S (S Z)) | | | | | +- [], B, F (S Z) (S (S Z)) (S (S Z)) | | | | | ‘- [], A, F Z (S Z) (S (S (S Z))) | | | | | +- [], B, F Z (S (S (S Z))) (S (S Z)) | | | | | | | +- [], B, F (S (S Z)) (S (S Z)) (S (S Z)) | | | | | | | ‘- [], A, F Z (S (S Z)) (S (S (S Z))) | | | | | | | +- [], B, F (S Z) (S (S (S Z))) (S (S Z)) | | | | | | | ‘- [], A, F Z (S Z) (S (S (S (S Z)))) | | | | | ‘- [], A, F Z Z (S (S (S (S Z)))) | | | ‘- [], A, F Z Z (S (S (S Z))) | ‘- [], A, F Z Z (S (S Z))

Note that the rule sequence can be described by the corecursive function $f\ a_{1}\ a_{2}=a_{2}\ (f\ (\lambda c.a_{1}\ c)\ (\lambda c.a_{2}\ (a_{1}\ c)))$. We assign a type for $f$ in the following. The universal type variable $f$ is instantiated by \m1’ m2’ m3’ . f1’ m1’ m2’ (S m3’) at the corecursive call of function f. We observe step h 7 gives F Z (S Z) (S (S (S (S Z)))), which is the reducible leaf at depth 6 in the reduction tree.

A : forall p x y . p (F Z x (S y)) => p (F Z (S x) y) B : forall p x y . p (F x y (S (S Z))) => p (F Z (S x) y)

f : forall p f . (forall p x y . p (f Z x (S y)) => p (f Z (S x) y)) => (forall p y . p (f Z y (S (S Z))) => p (f Z (S Z) y)) => p (f Z (S Z) (S Z)) f a1 a2 = a2 (f (\ c . a1 c) (\ c . a2 (a1 c)))

h : F Z (S Z) (S Z) h = f A (\ c . B c) step h 7

J.5

\dbend

Consider the following one rule rewriting system (from Zantema and Geser [26]) :

$F\ Z\ (S\ x)\ y\to_{K}G\ (F\ Z\ x\ (S\ y))\ (F\ x\ y\ (S\ (S\ Z)))$

Note that the rewrite system in Section J.4 is the dummy eliminated version of this rewriting system. Issuing command :inner 6 (F Z (S Z) (S Z)) to FCR, we obtain the following reduction trace.

the execution trace is: F Z (S Z) (S Z) -K-> G (F Z Z (S (S Z))) (F Z (S Z) (S (S Z))) -K-> G (F Z Z (S (S Z))) (G (F Z Z (S (S (S Z)))) (F Z (S (S Z)) (S (S Z)))) -K-> G (F Z Z (S (S Z))) (G (F Z Z (S (S (S Z)))) (G (F Z (S Z) (S (S (S Z)))) (F (S Z) (S (S Z)) (S (S Z))))) -K-> G (F Z Z (S (S Z))) (G (F Z Z (S (S (S Z)))) (G (G (F Z Z (S (S (S (S Z))))) (F Z (S (S (S Z))) (S (S Z)))) (F (S Z) (S (S Z)) (S (S Z))))) -K-> G (F Z Z (S (S Z))) (G (F Z Z (S (S (S Z)))) (G (G (F Z Z (S (S (S (S Z))))) (G (F Z (S (S Z)) (S (S (S Z)))) (F (S (S Z)) (S (S Z)) (S (S Z))))) (F (S Z) (S (S Z)) (S (S Z))))) -K-> G (F Z Z (S (S Z))) (G (F Z Z (S (S (S Z)))) (G (G (F Z Z (S (S (S (S Z))))) (G (G (F Z (S Z) (S (S (S (S Z))))) (F (S Z) (S (S (S Z))) (S (S Z)))) (F (S (S Z)) (S (S Z)) (S (S Z))))) (F (S Z) (S (S Z)) (S (S Z)))))

In this case the rule sequence is pretty simple, so we cannot learn much from the rule sequence. But when we observe the redexes, the reduction appear to have the same patterns as the one in Section J.4. The dummy elimination technique makes the reduction pattern explicit in the rule sequence, it inspires us to arrive at the following representation.

K : F Z (S x) y <= G (F Z x (S y)) (F x y (S (S Z)))

f : forall p qa qb f . (forall p x y . p (qa (f Z x (S y)) x y) => p (f Z (S x) y)) => (forall p y . p (qb (f Z y (S (S Z))) y) => p (f Z (S Z) y)) => p (f Z (S Z) (S Z)) f a1 a2 = a2 (f (\ c . a1 c) (\ c . (a2 (a1 c))))

h : F Z (S Z) (S Z) h = f (\ c . K c) (\ c . K c)

step h 7

The function f follows the exact same pattern as in Section J.4, but its type reflect the two use case of the rule K, i.e. applying K to the left or right argument of G. For each case we use a existential variable to capture the resulting contexts. Note that the existential variable qa has arity 3 and the existential variable qb has arity 2. Let us observe the following fully annotated h and f from FCR. Notice that the third argument for f in the definition of h is \m1’ m2’ . G (F Z Z (S m2’)) m1’ (the order of m1’ and m2’ is switched in the body). And the third argument is \m1’ m2’ . qb2’ (qa1’ m1’ m2’ (S (S Z))) (S m2’) at the corecursive call of f in the definition of f (the variable m2’ is duplicated).

lemmas h : F Z (S Z) (S Z) = f (\ x1’ . x1’) (\ m1’ m2’ m3’ . G m1’ (F m2’ m3’ (S (S Z)))) (\ m1’ m2’ . G (F Z Z (S m2’)) m1’) (\ m1’ m2’ m3’ . F m1’ m2’ m3’) (\ p4’ x5’ y6’ (c : p4’ (G (F Z x5’ (S y6’)) (F x5’ y6’ (S (S Z))))) . K (\ m1’ . p4’ m1’) x5’ y6’ c) (\ p10’ y11’ (c : p10’ (G (F Z Z (S y11’)) (F Z y11’ (S (S Z))))) . K (\ m1’ . p10’ m1’) Z y11’ c) f : forall p qa qb f . (forall p x y . p (qa (f Z x (S y)) x y) => p (f Z (S x) y)) => (forall p y . p (qb (f Z y (S (S Z))) y) => p (f Z (S Z) y)) => p (f Z (S Z) (S Z)) = \ p0’ qa1’ qb2’ f3’ (a1 : forall p x y . p (qa1’ (f3’ Z x (S y)) x y) => p (f3’ Z (S x) y)) (a2 : forall p y . p (qb2’ (f3’ Z y (S (S Z))) y) => p (f3’ Z (S Z) y)) . a2 (\ m1’ . p0’ m1’) (S Z) (f (\ m1’ . p0’ (qb2’ m1’ (S Z))) (\ m1’ m2’ m3’ . qa1’ m1’ m2’ (S m3’)) (\ m1’ m2’ . qb2’ (qa1’ m1’ m2’ (S (S Z))) (S m2’)) (\ m1’ m2’ m3’ . f3’ m1’ m2’ (S m3’)) (\ p10’ x11’ y12’ (c : p10’ (qa1’ (f3’ Z x11’ (S (S y12’))) x11’ (S y12’))) . a1 (\ m1’ . p10’ m1’) x11’ (S y12’) c) (\ p16’ y17’ (c : p16’ (qb2’ (qa1’ (f3’ Z y17’ (S (S (S Z)))) y17’ (S (S Z))) (S y17’))) . a2 (\ m1’ . p16’ m1’) (S y17’) (a1 (\ m1’ . p16’ (qb2’ m1’ (S y17’))) y17’ (S (S Z)) c)))

J.6

\dbend

The following term rewriting system is adapted from a string rewriting system in [9](Section 7), no current automated termination checker can detect the nontermination for this example.

$Bl\ (B\ x)\to_{1}B\ (Bl\ x)$

$Bl\ (Cl\ (Dl\ x))\to_{2}B\ (Cl\ (D\ x))$

$D\ (Dl\ x)\to_{3}Dl\ (D\ x)$

$Al\ (X\ x)\to_{4}Al\ (Bl\ (Bl\ x))$

$B\ (X\ x)\to_{5}X\ (Cl\ (Y\ x))$

$Bl\ (Cl\ (Dl\ x))\to_{6}X\ (Cl\ (Y\ x))$

$Y\ (D\ x)\to_{7}Dl\ (Y\ x)$

$Y\ (El\ x)\to_{8}Dl\ (Dl\ (El\ x))$

Observe the following nonlooping reduction trace ($\to_{a,b}$ is a shorthand for $\to_{a}\cdot\to_{b}$):

$Al\ (Bl\ \underline{(Bl\ (Cl\ (Dl}\ (Dl\ (El\ x))))))\to_{2}Al\ (Bl\ (B\ (Cl\ (D\ (Dl\ (El\ x))))))\to_{1,3}Al\ (B\ \underline{(Bl\ (Cl\ (Dl}\ (D\ (El\ x))))))\to_{6}Al\ (B\ (X\ (Cl\ (Y\ (D\ (El\ x))))))\to_{5,7}\underline{Al\ (X}\ (Bl\ (Cl\ (Dl\ \underline{(Y\ (El}\ x))))))\to_{4,8}Al\ (Bl\ (Bl\ \underline{(Bl\ (Cl\ (Dl}\ (Dl\ (Dl\ (El\ x))))))))\to_{2}Al\ (Bl\ (Bl\ (B\ (Cl\ (D\ (Dl\ (Dl\ (El\ x))))))))\to_{1,3,1,3}Al\ (B\ (Bl\ \underline{(Bl\ (Cl\ (Dl}\ (Dl\ (D\ (El\ x))))))))\to_{2}Al\ (B\ (Bl\ (B\ (Cl\ (Dl\ (Dl\ (D\ (El\ x))))))))\to_{1,3}Al\ (B\ (B\ \underline{(Bl\ (Cl\ (Dl}\ (D\ (D\ (El\ x))))))))\to_{6}Al\ (B\ (B\ (X\ (Cl\ (X\ (D\ (D\ (El\ x))))))))\to_{5,7,5,7}\underline{Al\ (X}\ (Bl\ (Bl\ (Cl\ (Dl\ (Dl\ \underline{(Y\ (El}\ x))))))))\to_{4,8}Al\ (Bl\ (Bl\ (Bl\ (Bl\ (Cl\ (Dl\ (Dl\ (Dl\ (Dl\ (El\ x))))))))))\to...$

The rewriting system admits reductions of the form: $Al\ (Bl^{n}\ (Cl\ (Dl^{n}\ (El\ x))))))\to^{*}Al\ (Bl^{n+1}\ (Cl\ (Dl^{n+1}\ (El\ x))))))$ for any for every $n>1$. The rule sequence of the above reduction is the following: $213,657,48,21313,213,65757,48,2131313,21313,213,6575757,48,...$. We now represent this rule sequence by the following corecursive function:

$f\ a_{1}\ a_{2}\ a_{3}\ a_{4}\ a_{5}\ a_{6}\ a_{7}\ a_{8}\ b=(b\cdot a_{6}\cdot a_{5}\cdot a_{7}\cdot a_{4}\cdot a_{8})\ (f\ a_{1}\ (a_{2}\cdot a_{1}\cdot a_{3})\ a_{3}\ a_{4}\ a_{5}\ (a_{6}\cdot a_{5}\ \cdot a_{7})\ a_{7}\ a_{8}\ \ (a_{2}\cdot a_{1}\cdot a_{3}\cdot a_{1}\cdot a_{3}\cdot b))$

Note that $f\ 1\ 2\ 3\ 4\ 5\ 6\ 7\ 8\ (2\cdot 1\cdot 3)$ generates the rule sequence above. The following is the type we assign for $f$.

K1 : Bl (B x) <= B (Bl x) K2 : Bl (Cl (Dl x)) <= B (Cl (D x)) K3 : D (Dl x) <= Dl (D x) K4 : Al (X x) <= Al (Bl (Bl x)) K5 : B (X x) <= X (Bl x) K6 : Bl (Cl (Dl x)) <= X (Cl (Y x)) K7 : Y (D x) <= Dl (Y x) K8 : Y (El x) <= Dl (Dl (El x))

f : forall p0 c b d y . (forall p x . p (B (Bl x)) => p (Bl (B x))) => (forall p x . p (B ( c (D x))) => p (Bl ( c (Dl x)))) => (forall p x . p (Dl (D x)) => p (D (Dl x))) => (forall p x . p (Al (Bl (Bl x))) => p (Al (X x))) => (forall p x . p (X (Bl x)) => p (B (X x))) => (forall p x . p (X ( c (Y x))) => p ( b (Cl ( d x)))) => (forall p x . p (Dl (Y x)) => p (Y (D x))) => (forall p x . p (Dl (Dl (El x))) => p (Y (El x))) => (forall p x . p (B ( b (Cl ( d (D x))))) => p (Bl (Bl ( c (Dl (Dl x)))))) => p0 (Al (Bl (Bl ( c (Dl (Dl (El y)))))))

f a1 a2 a3 a4 a5 a6 a7 a8 b = b (a6 (a5 (a7 (a4 (a8 (f a1 (\ c1 . a2 (a1 (a3 c1))) a3 a4 a5 (\ c1. a6 (a5 (a7 c1))) a7 a8 (\ c1 . a2 (a1 (a3 (a1 (a3 (b c1))))))))))))

h : (Al (Bl (Bl ( Cl (Dl (Dl (El y))))))) h = f K1 K2 K3 K4 K5 K6 K7 K8 (\ c . K2 (K1 (K3 c)))

Note that the quantified variables b,d in the type of f are existential variables. In the corecursive call of f, the variable c will be instantiated with (\m1’ . Bl (c1’ (Dl m1’))) , b will be instantiated with (\m1’ . B (b2’ m1’)) and d will be instantiated with (\m1’ . d3’ (D m1’)).

J.7

\dbend

The following rewriting system is from Emmes et. al. [8], which according to them is outside the scope of the their nontermination detection techniques.

$G\ T\ T\ x\ (S\ y)\to_{1}G\ (N\ x)\ (N\ y)\ (S\ x)\ (D\ (S\ y))$

$N\ Z\to_{2}T$

$N\ (S\ x)\to_{3}N\ x$

$D\ Z\to_{4}Z$

$D\ (S\ x)\to_{5}S\ (S\ (D\ x))$

Observe the following nonlooping nonterminating reduction trace for $G\ T\ T\ Z\ (S\ Z)$ (using left to right, inner-most reduction strategy).

$G\ T\ T\ Z\ (S\ Z)\to_{1}G\ (N\ Z)\ (N\ Z)(S\ Z)(D\ (S\ Z))\to_{2}G\ T\ (N\ Z)(S\ Z)(D\ (S\ Z))\to_{2}G\ T\ T\ (S\ Z)(D\ (S\ Z))\to_{5}G\ T\ T\ (S\ Z)(S\ (S\ (D\ Z)))\to_{4}G\ T\ T\ (S\ Z)(S\ (S\ Z))\to_{1}G\ (N\ (S\ Z))(N\ (S\ Z))(S\ (S\ Z))(D\ (S\ (S\ Z)))\to_{3}G\ (N\ Z)(N\ (S\ Z))(S\ (S\ Z))(D\ (S\ (S\ Z)))\to_{2}G\ T\ (N\ (S\ Z))(S\ (S\ Z))(D\ (S\ (S\ Z)))\to_{3}G\ T\ (N\ Z)(S\ (S\ Z))(D\ (S\ (S\ Z)))\to_{2}G\ T\ T\ (S\ (S\ Z))(D\ (S\ (S\ Z)))\to_{5}G\ T\ T\ (S\ (S\ Z))(S\ (S\ (D\ (S\ Z))))\to_{5}G\ T\ T\ (S\ (S\ Z))(S\ (S\ (S\ (S\ (D\ Z)))))\to_{4}G\ T\ T\ (S\ (S\ Z))(S\ (S\ (S\ (S\ Z))))...$

The rule sequence is of the shape $1,22,54,1,3232,554,1,3323332,55554...$. This rule sequence can be represented by the following corecursive equation.

$f\ a_{1}\ a_{2}\ b_{2}\ a_{3}\ b_{3}\ a_{4}\ a_{5}=a_{1}\ a_{2}\ b_{2}\ a_{5}\ a_{4}\ (f\ a_{1}\ (a_{3}\cdot a_{2})\ (b_{3}\cdot b_{2})\ a_{3}\ (b_{3}\cdot b_{3})\ a_{4}\ (a_{5}\cdot a_{5}))$

Note that $f\ 1\ 2\ 2\ 3\ 3\ 4\ 5$ gives rise to the rule sequence. The following is the type that we assign to $f$.

K1 : forall p x y . p (G (N x) (N y) (S x) (D (S y))) => p (G T T x (S y)) K2 : forall p . p T => p (N Z) K3 : forall p x . p (N x) => p (N (S x)) K4 : forall p . p Z => p (D Z) K5 : forall p x . p (S (S (D x))) => p (D (S x)) f : forall p g n1 n2 s . (forall p x y . p (g (n1 x) (n2 y) (S x) (D (s y))) => p (g T T x (s y))) => (forall p . p T => p (n1 Z)) => (forall p . p T => p (n2 Z)) => (forall p x . p (n1 x) => p (n1 (S x))) => (forall p x . p (n2 x) => p (n2 (s x))) => (forall p . p Z => p (D Z)) => (forall p x . p (s (s (D x))) => p (D (s x))) => p (g T T Z (s Z))

f a1 a2 b2 a3 b3 a4 a5 = a1 (a2 (b2 (a5 (a4 (f (\ c . a1 c) (\ c . a3 (a2 c)) (\ c . (b3 (b2 c))) (\ c . a3 c) (\ c . b3 (b3 c))) a4 (\ c . a5 (a5 c))))))

h : G T T Z (S Z) h = f (\ c . K1 c) K2 K2 K3 K3 K4 K5

Note that n1, n2 in the type of f are existential variables. At the corecursive call of f, variable g is instantiated by (\m1’ m2’ m3’ m4’ . g1’ m1’ m2’ (S m3’) m4’), variable n1 is instantiated by (\m1’ . n12’ (S m1’)), variable n2 is instantiated by (\m1’ . n23’ (s4’ m1’)), variable s is instantiated by (\m1’ . s4’ (s4’ m1’)).