Monotonicity of (Co-) Inductive Validity in Conditional Equational Specifications

Claus-Peter Wirth

SEKI-Report SR–2008–01

SEKI-Report ISSN 1437-4447 ^{UNIVERSITÄT DES SAARLANDES FACHRICHTUNG INFORMATIK D–66123 SAARBRÜCKEN GERMANY WWW: http://www.ags.uni-sb.de/}

This SEKI-Report was internally reviewed by: Peter Padawitz FR Informatik, Universität des Saarlandes, D–66123 Saarbrücken, Germany

E-mail: melis@activemath.org
WWW: http://www.activemath.org/~melis

Editor of SEKI series:

Claus-Peter Wirth Brandenburger Str. 42, D–65582 Diez, Germany

E-mail: wirth@logic.at
WWW: http://www.ags.uni-sb.de/~cp

Monotonicity of (Co-) Inductive Validity in Conditional Equational Specifications

Claus-Peter Wirth

November 23, 2008

Abstract

Voodoo man can.

Keywords: German Idealism, Dyslexia, Kissing, Angels, Angles, Kant, MSC 03D20, MSC 68Q42, MSC 16S15

1 Specifications with Constructors and Destructors

Let ‘C’, ‘D’, ‘E’, ‘G’, and ‘P’ be different symbols.

1.1 Sorts and Constructors

In this paper, we are mainly concerned with specification of inductive and co-inductive data types.

As nicely described in [Kühler & Wirth, 1996], we present our results in an extended many-sorted framework, where each sort s ∈ 𝕊 of a given many-sorted signature S gives rise to a general sort (G, s) with an additional constructor sub-sort (C, s), which is related to a set Σ_{C} of constructor (constant) (function) symbols, which is a subset of the set 𝔽 of constant (function) symbols of the signature: Σ_{C} ⊆ 𝔽. In the signature S, each function symbol f ∈ 𝔽 must receive a declaration of the form

f : s_{0} → ⋯ → s_{n}

with n ∈ N and s_{i} ∈ 𝕊 for all i ∈ {0, …, n}.

Let V = (V_{s})_{s∈𝕊} and V_{C} = (V_{C,s})_{s∈𝕊} be 𝕊-sorted families such that V_{C,s} ⊆ V_{s} and any of the sets V_{C,s} of constructor variables of sort s and V_{s′}\V_{C,s′} of general variables of sort s′ are infinite and mutually disjoint for all s, s′ ∈ 𝕊.

1.2 Visible Sorts vs. Hidden Sorts

Any sort s ∈ 𝕊 will be either • a visible sort (i.e. s ∈ 𝕊_{C}),

• a hidden sort (i.e. s ∈ 𝕊_{D}), or

• an experimental sort (i.e. s ∈ 𝕊_{E}).

Visible sorts are to specify inductive data types, built-up by constructors. Theoretically, any built-in data type may be included as a visible sort by adding all its elements as nullary constructors. Practically, it is important, however, that it is easily possible to specify many data types with a finite set of constructors, such as natural numbers, lists, and trees. The major exception to this possibility are co-inductive data types such as streams, sets, and functions. Such data types, however, can be conveniently specified as hidden sorts in our framework.

As inductive theorem proving requires the on-going extension of specifications during proofs, our (partial) algebraic specifications are subject to consistent extension, As the already established lemmas have to stay valid in such an extension, the notions of validity established by the theorem prover have to be monotonic w.r.t. consistent extension.

Regarding the intended monotonic behavior of our notions of validity w.r.t. consistent extension of our specifications, it is crucial that the already given data types do no change, at least not in their constructor sub-domains, i.e. the domains of what is sometimes called defined terms, data objects, or really existing objects of the data type. For the involved motivations behind this cf. [Padawitz, 1988, § 6], [Padawitz, 2000], [Kühler & Wirth, 1996], and [Hobbs, 1996].

For visible sorts, this invariance of constructor sub-domains is simply achieved by fixing the set of constructors once and forever, and by requiring the constructor subuniverses (C, s)^{A} of the algebraic models A of a specification to be isomorphic to the initial term algebra of the constructors Σ_{C}.

For hidden sorts, however, constructors do not define the co-inductive data types, but only explore them. While the number of constructors of a hidden sort will typically grow over time, a hidden sort comes with a set ? ⊆ 𝔽 of destructors which are fixed once and forever. Note that there are no destructors of visible sorts.

Thus, the data type of a visible sort is actually given by its destructors, whereas we can only access it with the help of the constructors for the hidden sort. The first idea on what a constructor sub-universe of a hidden sort could be is that of a final algebra. But this approach has several problems:

Foundational: The theories of sets and classes preferred today do not have a universal set, i.e. a set of all sets (and urelements). They support the inductive definition of sets as least fixpoints of monotonic operators, starting from the empty set, but they do not offer a good support for the co-inductive definition of sets as greatest fixpoints starting from the universal set. To the best of our knowledge, foundational frameworks based on category theory have similar problems.

Practical: For denoting a given object of a hidden sort, we need constructors in addition to destructors anyway.

Conceptual: The construction history of objects of hidden sorts may be intensionally relevant, for instance in the following cases:

• If we consider the objects of a functional data type to be given only up to extensional equality, we cannot treat the intensional properties of functions in the quotient w.r.t. to behavioral equivalence in a final algebra.

• If we want to specify a choice function on the data type of unordered sets, we can only do this with the help of the construction history of sets, e.g. by taking the first element of the list from which the set was constructed. Cf. [Roşu, 2004, § 3.7] for further discussion of this subject.

Due to theses problems we prefer to represent a co-inductive data type by a hidden sort whose constructor sub-universe is an initial term algebra again, but now of all possible constructors for that sort (whatever that means, cf. below). Following [Roşu, 2004], the destructors of that hidden sort will implicitly define the constructors of additional experimental sorts from a set 𝕊_{E}, which come with an application function mapping any experiment and any object of hidden sort to a visible sort. Thus, two hidden objects are behaviorally equal iff the results of all their experiments are equal.

The question, however, is what the term “all possible constructors” means. Practically, we may be content with all constructors that we will need in the future. Theoretically, this demand can be satisfied as follows. We assume that the sets 𝕊 of sorts of any possible signature S is a subset of some infinite set, say the set N_{+} of the positive natural numbers. Then the triples consisting of

• the symbol C,

• a natural number m ∈ N, and

• a tuple (or non-empty list) (s_{0}, …, s_{n}) with s_{i} ∈ N_{+} (for i ∈ {0, …, n} and n ∈ N)

can serve as a never to be exhausted reservoir of constructor symbols, simply by declaring

(C, n, (s_{0}, …, s_{n})) : s_{0} → ⋯ → s_{n}.

Note that this construction does not admit us to have sorts that are visible (constructor generated) and hidden (with behavioral equality) in parallel, such as in [Bidoit & Hennicker, 2006]: While it is consistent to assume all possible constructor symbols to be given from the very beginning, it is not consistent to assume all possible specifications for constructors of hidden sorts to given in advance, because they — and especially their behavior — may depend on visible sorts not yet existing.

As we must guarantee that visible sorts are not constructed from hidden sorts whose behavior they again define, we need some we well-founded quasi-ordering ≲ on the sorts 𝕊; i.e. an 𝕊-reflexive and transitive binary relation on 𝕊. As usual, its (partial) ordering < is given as ≲ \ ≳, and its equivalence ∼ is given as ≲ ∩ ≳. A data domain of sort s may depend on on the data domain of sort s′ only if s′≲s. They may be constructed mutually only if s′∼s. Data domains of a visible sort cannot be constructed mutually with those of hidden or experimental sorts.

4 November 23, 2008

2 Basic Notions and Notation

We follow standard mathematical writing style, cf. [Gillman, 1987].

We try to be self-contained in this paper. In case we should omit some required information, we refer the reader to the extensive surveys on term rewriting of [Avenhaus & Madlener, 1990], [Dershowitz & Jouannaud, 1990], [Klop, 1992], and [Plaisted, 1993]. Moreover, the introduction to positive/negative-conditional TRSs of [Wirth & Gramlich, 1994a] may be helpful.

‘N’ denotes the set of natural numbers and ‘<’ the ordering on N. The reflexive, symmetric, transitive, and reflexive & transitive closure of a (binary) relation ⟶ will be denoted by ⟶^{=}, ⟷, ⟶^{+}, and ⟶^{∗}, respectively. v and w are called joinable w.r.t. ⟶

if v↓w, i.e. if v⟶^{∗} ∘ ⟵^{∗}w.

The domain of ⟶ is  dom(⟶) := { s | ∃t. s⟶t }
The image of a class A under ⟶ is  ⟨A⟩⟶ := { b | ∃a ∈ A. a⟶b }

The notation for relations is precisely reused for functions, which are considered to be right-unique binary relations. We use ‘⊎’ for the union of disjoint classes.

2.1 Signatures and [Constructor] Terms

Definition 2.1 (Signature)

A signature is an 8-tuple (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻) of a set of sorts 𝕊, a set of no-junk sorts 𝕊_{NJ} ⊆ 𝕊, a set of no-confusion sorts 𝕊_{NC} ⊆ 𝕊, a set of experimental sorts 𝕊_{E} ⊆ 𝕊_{NJ} ∩ 𝕊_{NC}, a relation ≲ on 𝕊, a set of constant function symbols 𝔽, a set of constant predicate symbols ℙ with 𝔽∩ℙ = ∅, and a set of declarations 𝔻, such that:

1. ≲ is a quasi-ordering on 𝕊, with ordering < and equivalence ∼, such that:

(a) < is well-founded.

(b) If s ∼ s′ ∈ 𝕊_{NJ}, then s ∈ 𝕊_{NJ}.

(c) If s ∼ s′ ∈ 𝕊_{NC}, then s ∈ 𝕊_{NC}.

2. For each f ∈ 𝔽, there is at least one declaration in 𝔻 of the form

f : s_{0} → ⋯ s_{n−1} → s_{n}, ς

with n ∈ N, with s_{i} ∈ 𝕊 for each i ∈ {0, …, n}, and with ς ∈ {C,G} ∪ {D}×N.

(a) In this case, for each declaration

f : s_{0} → ⋯ s_{n−1} → s′, ς′

in 𝔻, we require (ς′, s′) = (ς, s_{n}). ^{1}

(b) For each declaration of the form c : s_{0} → ⋯ s_{n−1} → s_{n}, C, we require^{2} s_{n} ∈ 𝕊_{NJ} ⇒ ∀i ∈ {0, …, n}. (s_{n} ≳ s_{i}). We speak of a declaration of c_{s_{0},...,s_{n−1}} as a constructor for the sort s_{n}.

1This means that even in the presence of overloaded constant function symbols, each disambiguated function symbol has a unique declaration and each term has a unique sort.

(c) For each declaration of the form d : s_{0} → ⋯ s_{n−1} → s_{n}, D, j,

we require^{3} j ∈ {0, …, n−1} and ∀i ∈ {0, …, n}. (s_{j} ≳ s_{i}).

We speak of a declaration of d_{s_{0},...,s_{n−1}} as a destructor of the sort s_{j}.

3. For each P ∈ ℙ, there is at least one declaration in 𝔻 of the form

P : s_{1}, …, s_{n}

with n ∈ N, and with s_{i} ∈ 𝕊 for each i ∈ {1, …, n}.

Definition 2.2 (Variable-System, V, X, V_{k}(⋯))

A variable-system for a signature (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻) is a {C,G}×𝕊-sorted family

V = (V_{ς,s})_{(ς,s) ∈ {C,G}×𝕊}

of infinite sets V_{ς,s} that are mutually disjoint and disjoint from 𝔽. The variables from V_{C,s} and V_{G,s} are called the constructor variables and the general variables of sort s, respectively.

By abuse of notation we sometimes write V to denote ⋃_{(ς,s) ∈ {C,G}×𝕊} V_{ς,s} and

V_{ς}

to denote ⋃_{s ∈ 𝕊} V_{ς,s}.

And when we speak of a set of variables X ⊆ V, we mean a {C,G}×𝕊-sorted family X = (X_{ς,s})_{(ς,s) ∈ {C,G}×𝕊} with X_{ς,s} ⊆ V_{ς,s} for all (ς, s) ∈ {C,G}×𝕊.

For k ∈ {C,G}×𝕊 and for Γ being a term, formula, sequent, &c., we use

V_{k}(Γ)

to denote the set of variables from V_{k} occurring in Γ.

2The idea is that the constructors of no-junk sorts equivalent via ∼ construct their domains in parallel on the basis of the domains of those of their arguments whose sort is smaller w.r.t. <. Constructors of a junk sort s ∈ 𝕊\𝕊_{NJ}, however, may have arguments of a sort s′ defined later than s, where even s<s′ may be the case.

3 s_{j}>s_{n} means that s_{n} serves as a visible sort for experiments on the sort s_{j} via d. And s_{j}∼s_{n} means that experiments on the sort s_{n} result in experiments on the sort s_{j} via d. The reason for taking the same hierarchy for hidden and visible sorts is that we do not want to have a visible sort depending on a hidden sort whose visibility it defines. The reason for requiring s_{j}≳s_{i} also for i ≺ n is the constructor hierarchy of the experimental sorts.

Definition 2.3 ([Constructor] Terms, Top(⋯), Length, Groundness, Linearity)

Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻). Let X ⊆ V. Let s ∈ 𝕊. The set

T (S, X)_{G,s}

of (general) terms of sort s denotes the disambiguated well-sorted first-order terms of over S and X of sort s. This means that, for all s′ ∈ 𝕊, the sets T (S, X)_{G,s′} are the smallest sets such that

1. for x ∈ X_{C,s′} ⊎ X_{G,s′} we have

x ∈ T (S, X)_{G,s′}

with top symbol

Top(x) = x,

and,

2. for each declaration f : s_{0} → ⋯ s_{n−1} → s′, ς in 𝔻, and for each t_{0}, …, t_{n−1} with t_{i} ∈ T (S, X)_{G,s_{i}} for each i ∈ {0, …, n−1}, we have

f_{s_{0},...,s_{n−1}}(t_{0}, …, t_{n−1}) ∈ T (S, X)_{G,s′},

with top symbol

Top(f_{s_{0},...,s_{n−1}}(t_{0}, …, t_{n−1})) = f_{s_{0},...,s_{n−1}}.

T (S, X)_{C,s} , however, is the set of constructor terms of sort s. This means that, for all s′ ∈ 𝕊, the sets T (S, V)_{C,s′} are the smallest sets such that

1.  X_{C,s′} ⊆ T (S, X)_{C,s′}

and,

2. for each declaration c : s_{0} → ⋯ s_{n−1} → s′, C in 𝔻, and for each t_{0}, …, t_{n−1} with t_{i} ∈ T (S, X)_{C,s_{i}} for each i ∈ {0, …, n−1}, we have

c_{s_{0},...,s_{n−1}}(t_{0}, …, t_{n−1}) ∈ T (S, X)_{C,s′}.

All in all, they form the term-system

T (S, X) = (T (S, X)_{ς,s})_{(ς,s) ∈ {C,G}×𝕊} .

We apply the abuses of notation for variable-systems also to term-systems.

The length of a term is |x| = 1 for x ∈ V, and |f(t_{1}, …, t_{m})| = 1 + |t_{1}| + ⋯ + |t_{m}|.

A term is ground if no variable occurs in it.

A term is linear if each variable occurs at most once in it.

Definition 2.4 (Positions POS(⋯))

The set of positions of a term t is denoted by POS(t), and inductively defined as follows. Positions are lists of positive natural numbers.

The root or top position is the empty list ∅, i.e.

∅ ∈ POS(t),
t/∅ = t,

and

t[ ∅ ← s] = s.

Moreover, for i ∈ {1, …, n},

ip ∈ POS(f(t_{1}, …, t_{n})) if p ∈ POS(t_{i})
f(t_{1}, …, t_{n})/ip = t_{i}/p,

and

f(t_{1}, …, t_{n})[ ip ← s] = f(t_{1}, …, t_{i−1}, t_{i}[ p ← s], t_{i+1}, …, t_{n}).

Definition 2.5 (Constant-Equality) Two terms t_{0}, t_{1} ∈ T (S, V) are constant-equal if we have POS(t_{0}) = POS(t_{1}) and for all p ∈ POS(t_{1}):

1. If Top(t_{0}/p) = f_{s_{0},...,s_{n−1}} for some constant symbol f ∈ 𝔽 and some sorts s_{i} ∈ 𝕊 for each i ∈ {0, …, n−1}; then Top(t_{0}/p) = Top(t_{1}/p).

2. If Top(t_{0}) ∈ V_{G,s}⊎V_{C,s} for some s ∈ 𝕊, then Top(t_{1}) ∈ V_{G,s}⊎V_{C,s} as well.

Note that Item 2 of Definition 2.5 could be omitted because we have used disambiguated constant function symbols in Item 1.

2.2 Substitutions

Definition 2.6 (Substitution) Let σ be a substitution, i.e. a function from variables to terms. We say that σ is a substitution on Y if dom(σ) ⊆ Y. Note that for σ := {x↦x}, we have dom(σ) = {x} instead of dom(σ) = ∅. If we declare a substitution as σ : Y → T (S, X), this means that dom(σ) = Y and that T (S, X) is the co-domain of σ. With ‘Γ σ’ we denote the result of replacing each occurrence of a variable x ∈ dom(σ) in Γ with σ(x).

Requirement 2.7 (V_{C}) Any substitution σ respects sorts and subsorts: ⟨V_{ς,s}⟩σ ⊆ T (S, V)_{ς,s} for each ς ∈ {C,G} and each s ∈ 𝕊.

Corollary 2.8 For u ∈ T (S, V)_{C,s} and σ : V(u) → T (S, X), we have uσ ∈ T (S, X)_{C,s}.

A substitution σ is a most general unifier of two terms u_{0}, u_{1} on Y if u_{0}σ = u_{1}σ and, for all μ : V → T (S, V) with u_{0}μ = u_{1}μ, there is a ν : V → T (S, V) such that (xσ)ν = xμ for all x ∈ Y. Note that a most general unifier always exists for unifiable terms, although each of our types has a single constructor subtype. Indeed, in the subsuming framework of order-sorted signatures, our signatures are “downward unique” and thus admit unitary unification according to Theorem 9.5 of [Waldmann, 1989b]. Our framework may be indeed represented as an instance of the order-sorted framework of [Gogolla, 1983; 1984], [Smoka &al., 1989], and [Waldmann, 1989a], roughly as follows (cf. Definition 2.1 for more details):

No other sub-sort relations are given but

(C, s) ≺ (G, s)

for each s ∈ 𝕊.

A declaration of a constant symbol f according to

f : s_{0} → ⋯ s_{n−1} → s_{n}, ς

is to result in the declaration

f : (G, s_{0}) → ⋯ (G, s_{n−1}) → (G, s_{n}).

Moreover, if f_{s_{0},...,s_{n−1}} is a constructor symbol (i.e. if ς = C), this is to be expressed in the order-sorted framework with the additional declaration

f : (C, s_{0}) → ⋯ (C, s_{n−1}) → (C, s_{n}).

A constructor variable x ∈ V_{C,s′} is declared as x : (C, s′). And a general variable Y ∈ V_{G,s} is declared as Y : (G, s).

Let X ⊆ V. Then T (S, X)_{G,s} is the set of terms of the sort (G, s) in the order-sorted framework, where T (S, X)_{C,s} is just the subset of terms t : (C, s).

Cf. [Wirth, 2009, Note 8] for a general way to model our framework with many-sorted specifications without constructor variables, which uses additional sorts with embedding functions for the constructor sub-sorts, but results in less readable terms.

Replacing all variables from V_{C,s}⊎V_{G,s} with the same chosen variable x_{s} ∈ V_{C,s}, we get:

Corollary 2.9 If t_{0}, t_{1} are constant-equal, then there is some μ : V(t_{0}, t_{0}) → T (S, V) such that t_{0}μ = t_{1}μ.

2.3 Pre-Structures, Valuations, Evaluation

Definition 2.10 (S-Pre-Structure) Let S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻) be a signature. An S-pre-structure S is a function with the following properties:

1. For each s ∈ 𝕊, S is defined on (C, s) and on (G, s). The values (C, s)^{S} and (G, s)^{S} are called the constructor universe and the (general) universe of the sort s, respectively, two sets that satisfy

∅ ≠ (C, s)^{S} ⊆ (G, s)^{S}.

2. For each declaration f : s_{0} → ⋯ s_{n−1} → s_{n}, ς in 𝔻, S is defined on f_{s_{0},...,s_{n−1}}.

The value is a function f_{s_{0},...,s_{n−1}}^{S} such that • f_{s_{0},...,s_{n−1}}^{S} : (G, s_{0})^{S}× ⋯ ×(G, s_{n−1})^{S} → (G, s_{n})^{S};

• and, in case of ς = C, also

⟨(C, s_{0})^{S}× ⋯ ×(C, s_{n−1})^{S}⟩f_{s_{0},...,s_{n−1}}^{S} ⊆ (C, s_{n})^{S}.

3. For each declaration P : s_{0}, …, s_{n−1} in 𝔻, S is defined on P_{s_{0},...,s_{n−1}}. The value is

a set P_{s_{0},...,s_{n−1}}^{S} such that

P_{s_{0},...,s_{n−1}}^{S} ⊆ (G, s_{0})^{S}× ⋯ ×(G, s_{n−1})^{S}.

Definition 2.11 (S-Valuation) Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻). Let S be a S-pre-structure. An S-valuation τ [on X] is a (possibly) partial function on V with [ dom(τ) = X and] τ(x) ∈ (ς, s)^{S} for each x ∈ V_{ς,s} ∩ dom(τ) and each (ς, s) ∈ {C,G}×𝕊. We denote with τ : X → S an S-valuation τ on X, and with τ : X ⇝ S an S-valuation τ on some Y with Y ⊆ X.

Definition 2.12 (Evaluation Function “eval”) Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻). Let S be an S-pre-structure. Let τ be an S-valuation. The evaluation function “eval” is defined as follows:

• For x ∈ V we have eval(S⊎τ)(x) = τ(x).

• For f ∈ 𝔽 with a declaration of the form f : s_{0} → ⋯ → s_{n−1} → s′′, ς in 𝔻, and for terms t′_{0}, …, t′_{n−1} with t′_{i} ∈ T (S, V)_{G,s_{i}} and s_{i} ∈ 𝕊 for each i ∈ {0, …, n−1}:

eval( S⊎τ )( f_{s_{0},...,s_{n−1}}(t′_{0}, …, t′_{n−1}) ) = f_{s_{0},...,s_{n−1}}^{S}( \begin{matrix}eval(S⊎τ)(t′_{0}) & , \\ … & , \\ eval(S⊎τ)(t′_{n−1}) \end{matrix} ).

• For P ∈ ℙ with a declaration of the form P : s_{1}, …, s_{n} in 𝔻, and for terms t′_{1}, …, t′_{n} with t′_{i} ∈ T (S, V)_{G,s_{i}} and s_{i} ∈ 𝕊 for each i ∈ {1, …, n}:

eval( S⊎τ )( P_{s_{1},...,s_{n}}(t′_{1}, …, t′_{n}) ) =

\{ \begin{matrix}TRUE & if ( \begin{matrix}eval(S⊎τ)(t′_{1}) & , \\ … & , \\ eval(S⊎τ)(t′_{n}) \end{matrix} ) ∈ P_{s_{1},...,s_{n}}^{S} \\ FALSE & otherwise \end{matrix} \} .

• For s ∈ 𝕊 and for t_{0}, t_{1} ∈ T (S, V)_{G,s}:

eval(S⊎τ)(t_{0}=t_{1}) = \{ \begin{matrix}TRUE & if eval(S⊎τ)(t_{0}) = eval(S⊎τ)(t_{1}) \\ FALSE & otherwise \end{matrix} \} .

2.4 Constructing Terms

Definition 2.13 ([Extended] Constructing Terms CT(S,V), ECT(S,V))

Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻). Let s′ ∈ 𝕊.

The set CT(S,V)_{s′} of constructing terms of the sort s′ (or else: the set ECT(S,V)_{s′} of extended constructing terms of the sort s′) is given as follows:

t ∈ CT(S,V)_{s′} (or else: t ∈ ECT(S,V)_{s′}) if t ∈ T (S, V)_{G,s′} and, for each p ∈ POS(t), the following holds:

• If Top(t/p) = f_{s_{0},...,s_{n−1}} for some constant symbol f ∈ 𝔽 and some sorts s_{i} ∈ 𝕊 for each i ∈ {0, …, n−1}; then, for the unique (ς, s′′) such that 𝔻 contains a declaration of the form

f : s_{0} → ⋯ → s_{n−1} → s′′, ς,

we have s′′ ∼ s′ and ς = C (or else: s′′ ∈ 𝕊 and ς = C).

• If Top(t/p) = x for some variable x ∈ V; then, for the unique (ς, s′′) such that x ∈ V_{ς,s′′}, we have s′′ < s′ and ς = C (or else: s′′ ∈ 𝕊 and ς ∈ {C,G}).

2.5 Built-In Terms and Predicates

As the constructor terms of a sort s ∈ 𝕊_{NJ} ∩𝕊_{NC} are to be identical to their constructor subuniverses up to isomorphism, with the exception of their sub-terms of sorts not in 𝕊_{NJ} ∩𝕊_{NC}, these “built-in terms” already represent their constructor sub-universes one-to-one and may be used to define “built-in” predicates that can be guaranteed to be somehow the same in all possible structures.

Definition 2.14 ([Extended] Built-In Terms BT(S,V))

Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻). Let s′ ∈ 𝕊.

The set BT(S,V)_{s′} of build-in terms of the sort s′ (or else: the set EBT(S,V)_{s′} of extended build-in terms of the sort s′) is given as follows:

t ∈ BT(S,V)_{s′} (or else: t ∈ EBT(S,V)_{s′}) if t ∈ T (S, V)_{G,s} and, for each p ∈ POS(t), the following holds:

• If Top(t/p) = f_{s_{0},...,s_{n−1}} for some constant symbol f ∈ 𝔽 and some sorts s_{i} ∈ 𝕊 for each i ∈ {0, …, n−1}; then, for the unique (ς, s′′) such that 𝔻 contains a declaration of the form

f : s_{0} → ⋯ → s_{n−1} → s′′, ς,

we have s′′ ∈ 𝕊_{NJ} ∩𝕊_{NC} (or else: s′′ ∈ 𝕊_{NC}) and ς = C.

• If Top(t/p) = x for some variable x ∈ V; then, for the unique (ς, s′′) such that x ∈ V_{ς,s′′}, we have s′′ ∉ 𝕊_{NJ} ∩𝕊_{NC} (or else: s′′ ∉ 𝕊_{NC}) and ς = G.

Note that we have CT(S,V) ⊆ ECT(S,V), BT(S,V) ⊆ ECT(S,V), and EBT(S,V) ⊆ ECT(S,V), but not other subset relations hold in general for these sets. As the sorts of the variables are different from the sorts of the function symbols for any T with T ∈ {CT(S,V), BT(S,V), EBT(S,V)}, we get the following corollary, which, however, does not hold for ECT(S,V) in general.

Corollary 2.15 Let T ∈ {CT(S,V), BT(S,V), EBT(S,V)}. We have:

1. T ⊆ ECT(S,V).

2. If, for each i ∈ {0, 1}, we have û_{i} ∈ T and ϱ_{i} : V(û_{i}) → T (S, V), and if û_{0}ϱ_{0} = û_{1}ϱ_{1}; then û_{0}, û_{1} are constant-equal.

Note that Item 2 of Corollary 2.15 serves as a strengthened converse of Corollary 2.9.

Definition 2.16 (Built-In Predicates)

Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻).

Let P ∈ ℙ with declaration P : s_{1}, …, s_{n} in 𝔻.

Now the disambiguated predicate symbol P_{s_{1},...,s_{n}} is a built-in predicate for S if there is associated with it a fixed subset of BT(S,V)_{s_{1}}× ⋯ ×BT(S,V)_{s_{n}}, which is closed under constant-equality. By abuse of notation we denote this set with P_{s_{1},...,s_{n}} as well.

2.6 Structures

Definition 2.17 (S-structure) Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻). An S-structure S is an S-pre-structure that satisfies following properties:

1. In case of s ∈ 𝕊_{NJ}:

(C, s)^{S} = { eval(S⊎τ)(t) | t ∈ CT(S,V)_{s} ∧ τ : V(t) → S }.

2. In case of s ∈ 𝕊_{NC}, t_{i} ∈ CT(S,V)_{s}, τ_{i} : V(t_{i}) → S for i ∈ {0, 1}, and

eval(S⊎τ_{0})(t_{0}) = eval(S⊎τ_{1})(t_{1}); then we t_{0}, t_{1} are constant-equal, and if Top(t_{0}/p) ∈ V, then τ_{0}(t_{0}/p) = τ_{1}(t_{1}/p).

3. Let P ∈ ℙ with declaration P : s_{1}, …, s_{n} in 𝔻. If P_{s_{1},...,s_{n}} is a built-in predicate,

then we require for o_{1}, …, o_{n} with o_{i} ∈ (G, s_{i})^{S} for each i ∈ {1, …, n}:

(o_{0}, …, o_{n−1}) ∈ P_{s_{1},...,s_{n}}^{S} iff

there are an index set I ⊆ {1, …, n} and some terms t_{i} ∈ BT(S,V)_{s_{i}} and some valuations τ_{i} : V(t_{i}) → S, such that eval(S⊎τ_{i})(t_{i}) = o_{i} for each i ∈ I and

A_{1}× ⋯ ×A_{n} ⊆ P_{s_{1},...,s_{n}},

where A_{i} := \{ \begin{matrix}\{t_{i}\} & if i ∈ I \\ BT(S,V)_{s_{i}} & if i ∈ \{1, …, n\}\I \end{matrix} \}.

3 Conditional Term Rewriting Systems

3.1 Motivation

Recursion is a form of programming or definition where a newly defined notion may even occur in its definientia. Contrary to explicit definitions, where we can always get rid of the new notions by reduction, i.e. by rewriting the definienda (left-hand sides of the defining equations) to the definientia (right-hand sides), reduction with recursive definitions may run forever.

By formalizing recursive definitions with left-linear \underline{t}erm \underline{r}ewriting \underline{s}ystems (TRSs) we can stay very close to the original intuition.

• From a theoretical point of view, recursion can be modeled with unconditional TRSs. Indeed, each Turing machine (including a universal one) can easily be programmed as a monadic, left-linear, unconditional TRS whose critical overlaps are trivial selfoverlays; cf. [Huet & Lankford, 1978].

• From a practical point of view, however, left-linear positive/negative-conditional TRSs with non-trivial critical overlaps are more convenient and in great demand; cf. [Kaplan, 1988], [Bachmair & Ganzinger, 1991], [Becker, 1993], [Wirth & Lunde, 1994], [Wirth & Gramlich, 1994a], and § 4 of [Wirth, 1997].

The problems in finding a meaningful semantics for recursion modeled in the framework of TRSs may seem just as difficult as for untyped λ-calculus, cf. [Barendregt, 1984]. To state our case clearly, let us name these problems for the instance of first-order arithmetic of natural numbers, assuming the consistency of arithmetic on the meta-level in the sense of [Gentzen, 1938]. The consistency of arithmetic might be destroyed on the object-level by the following two dangers:

Non-Termination: Even if we require that each new term is reducible, some non-termi-nating recursions (such as a = a+1) may introduce error objects which cannot be consistently identified with any natural number.

Inconsistent Identification: A function-call may evaluate non-confluently to two different natural numbers, resulting in their equality, such as for a = 0 and a = 1.

On the one hand, programming languages — such as Haskell (cf. e.g. [Hudlak &al., 1999]) or Curry (cf. e.g. [Hanus, 2006]) — circumvent these dangers by tailored semantics, such as priority rewriting and “non-deterministic functions”. Theoreticians, on the other hand, tend to avoid these dangers by proving some recursion theorems, saying that certain restricted forms of recursive equations have unique solutions in terms of total functions for the recursive operators. These unique solutions can then be thought to define these operators explicitly, and dangers cannot occur. For instance, Slind [1996] presents the idea that recursive functions must not be specified without a well-founded ordering, and that the non-decreasing calls in the function definition’s right-hand sides are to be immediately evaluated to ⊥ and not rewritten recursively.

• From a conceptual point of view, recursion theorems are counterintuitive because rewriting with the defining equations is not modeled at all. We believe that the recursive process of rewriting definienda to definientia is the conceptual basis for both recursive specification and computation. Indeed, for studying what could go wrong with recursive definitions, we have to model this recursive rewriting explicitly.

• From a practical point of view, recursion theorems such as the one of Slind [1996] are infeasible because many recursive programs (such as interpreters) — by their very nature — do not terminate on all input and have undecidable termination problems; and even if they do terminate, neither the termination nor the well-founded ordering to show it may be known at definition time.

Note that the recursion theorem of Slind [1996] is not a poor instance of a recursion theorem, but — to the best of our knowledge — one of the strongest and practically most adequate approaches to admit recursive definitions via recursion theorems. It is implemented e.g. in Isabelle/HOL, cf. e.g. [Nipkow &al., 2000; 2002].

In this paper we are interested in a conceptually and practically adequate treatment of recursion via rewriting.

The state of the art of controlling the danger of inconsistent identification are the confluence criteria of [Wirth, 2009]. In this paper we will simply assume confluence to be given.

Our answer to the danger of non-termination is simple: Don’t worry, be happy! Indeed, an arbitrary number of error objects is beneficial to the semantics of so-called data models. Kühler & Wirth [1996] describe this semantics under a practical aspect. Under a more theoretical and general aspect, Wirth & Gramlich [1994b] study this and other possible semantics for partially specified functions. These studies are extended in § 10 of [Wirth, 1997]. Validity in all data models, however, still appears as the most natural semantical answer to the danger of non-termination. But we will add a lot to that answer in this paper.

3.2 Basic Notions and Notation

A (conditional) equation is a triple l=r⟵C consisting of two terms of the same sort, namely the left-hand side l and the right-hand side r, and the condition C. It is to be interpreted as: “For all variables from V(l=r⟵C), the left-hand side l is equal to the right-hand side r if the condition C holds.” Cf. [Kühler & Wirth, 1996], [Wirth, 1997], and [Wirth & Gramlich, 1994b] for more on semantics. If the condition is empty, i.e. if C = ∅, the equation is unconditional and we simply write l=r instead of l=r⟵C. An (unconditional) TRS is a set of unconditional equations. A \underline{c}onditional TRS (CTRS) is a set of (conditional) equations.

A CTRS is ground if all its terms are ground. A CTRS is left-linear if all its left-hand sides are linear terms.

We are going to define a term rewrite or reduction relation for a CTRS R and a set of variables X ⊆ V. As we will not instantiate the variables from X in the reduction relation (as would be required for considering stability under substitution), the elements of X are to be considered as unknowns, parameters, or free generators. For instance, in Quod-Libet, the set X is set to V\V_{C} for semantical reasons described by [Kühler & Wirth, 1996] (⟷^{∗}_{R,X} becomes equality in all data models), and T (S, X)_{C} becomes the set of constructor ground terms.

Definition 3.1 (Reduction Relation, ⟶_{R,X,i,p}) Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻). Let R be a CTRS. Let X ⊆ V. Let us define our reduction relation ⟶_{R,X} top-down, inductively over the condition-recursion depth i, and modulo the property of fulfilledness of Definition 3.10.

⟶_{R,X} := ⋃_{i∈N} ⟶_{R,X,i}.

For s, t ∈ T (S, X) and i ∈ N, we define s⟶_{R,X,i}t if s⟶_{R,X,i,p}t for some p ∈ POS(s).

⟶_{R,X,0,p} := ∅.

s⟶_{R,X,i+1,p}t if there are (l=r⟵C) ∈ R and a substitution μ : V(l=r⟵C) → T (S, X), such that s/p = lμ and t = s[ p ← rμ] and Cμ is fulfilled w.r.t. ⟶_{R,X,i} and S.

The notion of fulfilledness may remain abstract up to § 3.3. The only thing we need right now is that the operator that maps a relation ⟶ to the conditions fulfilled w.r.t. ⟶ and S is monotonic, i.e. that a bigger ⟶ results in more conditions being fulfilled w.r.t. ⟶ and S. Then a trivial induction shows:

Corollary 3.2 For i, j ∈ N with i ≤ j we have ⟶_{R,X,i} ⊆ ⟶_{R,X,j} ⊆ ⟶_{R,X}.

Corollary 3.3 (Destructing Derivations)

If s⟶_{R,X,n,pq}t, then s/p⟶_{R,X,n,q}t/p and t = s[ p ← t/p].

Corollary 3.4 (Constructing Derivations)

1. If t/p⟶_{R,X,n,q}u, then we have t⟶_{R,X,n,pq}t[ p ← u].

2. Let Π ⊆ POS(t) be a parallel set of positions.

If t/p⟶^{∗}_{R,X,n}u_{p} for each p ∈ Π, then we have t⟶^{∗}_{R,X,n}t[ p ← u_{p} | p ∈ Π].

A variable in V(r, C)\V(l) is called an extra variable of the equation l=r⟵C. According to the occurrences of extra variables in their equations, the following taxonomy of CTRSs (restricting all their equations) is not mnemonic but folklore, cf. e.g. [Hanus, 1994; Suzuki &al., 1995]:

1-CTRS No extra variables: V(r, C) ⊆ V(l).

2-CTRS Extra variables only in the conditions: V(r) ⊆ V(l).

3-CTRS Extra variables must occur in the condition of their equation: V(r) ⊆ V(l, C).

4-CTRS No restriction on extra variables.

We will use n-CTRS both as a noun and as an adjective.

Definition 3.5 (Normality; [Bergstra & Klop, 1986]) A CTRS R is normal if the right-hand sides u_{2} of the equations (u_{1}=u_{2}) listed in the conditions C of the conditional equations (l=r⟵C) ∈ R are ground terms which are irreducible w.r.t. R. (For decidability reasons, this irreducibility requirement is typically strengthened to irreducibility w.r.t. the associated unconditional TRS, which has all conditions removed, assuming them to be always fulfilled.)

While the requirement of normality (cf. Definition 3.5) is a strong restriction on the form of CTRSs (cf. the discussions in §§ 6 and 7.3 of [Wirth, 2009]), its weak form of quasinormality only disallows that both the left-hand side and the right-hand side of an equation in a condition are undefined objects in the sense of Definition 3.10. Quasi-normality can easily be achieved for constructor-based specifications in practice. Indeed, all confluent example specifications in this paper are quasi-normal.

Definition 3.6 ([Weak-] Quasi-Normality) Let V be a variable-system for the signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻). Let R be a CTRS and X ⊆ V. A condition C is [weak-] quasi-normal w.r.t. R, X if for all (u_{0}=u_{1}) listed in C:

• [V(u_{0}, u_{1}) ⊆ V_{C} or]

• for all μ : V(C) → T (S, X) for which Cμ is fulfilled w.r.t. ⟶_{R,X} and S, there is an i ∈ {0, 1} such that (Def u_{i}μ) occurs in Cμ or that u_{i}μ ∈ T (S, V)_{C}.

R, X is [weak-] quasi-normal if C is [weak-] quasi-normal w.r.t. R, X for all (l=r⟵C) ∈ R.

3.3 Constructors and Fulfilledness

Let us describe the special settings of this paper which are presupposed in the following; namely the irreducibility of constructor terms and the possible conditions of conditional equations and their fulfilledness.

Operationally, the set T (S, X)_{C} of constructor terms guarantees irreducibility also in future consistent extensions of the specification. Semantically, T (S, X)_{C} is intended to denote the defined terms, data objects, or really existing objects. For the involved motivations behind this cf. [Hobbs, 1996], [Kühler & Wirth, 1996], [Padawitz, 1988, § 6], and [Padawitz, 2000].

Requirement 3.7 (Requirements 20 and 43 (Σ_{C} and Σ_{N T}) of [Wirth, 2009]) For any signature S = (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻), and for any CTRS R and each (l=r⟵C) ∈ R we require Top(l) = f_{s_{0},...,s_{n−1}}, for some f ∈ 𝔽 with declaration f : s_{0} → ⋯ → s_{n−1} → s′′, ς in 𝔻 and with ς ≠ C.

By Requirement 3.7, no left-hand side can match a term from T (S, V)_{C}, nor from ECT(S,V). Thus we have:

Corollary 3.8 dom(⟶_{R,X}) ⊆ T (S, X) \ T (S, X)_{C}.

Corollary 3.9 Let û ∈ ECT(S,V), and ϱ : V(û) → T (S, V). If ûϱ⟶^{∗}_{R,X}v, then there is

a ϱ′ : V(û) → T (S, V) with v = ûϱ′ and ∀x ∈ V(û). (xϱ⟶^{∗}_{R,X}xϱ′).

We assume that our conditions are conjunctive lists of literals of the following five forms: (u_{1}=u_{2}), (u_{1}≠u_{2}), (Def u), P (u_{1}, …, u_{n}), ¬P (u_{1}, …, u_{n}), where P is an n-ary built-in predicate on BT(S,V), cf. § 2.5. As these predicates are not specified by the CTRSs but must be given by additional means, we have one more reason to call them built-in predicates.

As already explained in § 2.5, by abuse of notation, each P has a syntactical and a semantical aspect, which can easily be distinguished in our context even without a different notation: the symbol P : s_{1}, …, s_{n} in our formal language (forming the literal P (u_{1}, …, u_{n}) for any terms u_{i} ∈ T (S, X)_{s_{i}}); and the relation P ⊆ BT(S,V)_{s_{1}} × ⋯ × BT(S,V)_{s_{n}} in the BT(S,V)-reduct of the (sorted) free term algebra over X.

We may have arbitrarily many such predicates P on BT(S,V) of arbitrary arity, cf. [Wirth, 2009, Note 2].

Definition 3.10 (Fulfilledness)

1. A condition is fulfilled w.r.t. ⟶ and S if all its literals are fulfilled w.r.t. ⟶ and S.

2. (u_{1}=u_{2}) is fulfilled w.r.t. ⟶ and S if u_{1}↓u_{2}.

3. (u_{1}≠u_{2}) is fulfilled w.r.t. ⟶ and S if for each i ∈ {0, 1}, there are û_{i} ∈ EBT(S,V) and ϱ_{i} : V(û_{i}) → T (S, V), such that u_{i}⟶^{∗}û_{i}ϱ_{i}, and û_{0}, û_{1} are not constant-equal.^{4}

4. (Def u) is fulfilled w.r.t. ⟶ and S if there is a û ∈ T (S, X)_{C} such that u⟶^{∗}û. ^{5}

5. P (u_{1}, …, u_{n}) is fulfilled w.r.t. ⟶ and S if there is an index set I ⊆ {1, …, n} such that, setting J := {1, …, n}\I, for each i ∈ I, there are û_{i} ∈ BT(S,V) and ϱ_{i} : V(û_{i}) → T (S, V) with u_{i}⟶^{∗}û_{i}ϱ_{i} such that, for all (û_{j})_{j∈J} with ∀j ∈ J. (û_{j} ∈ BT(S,V)), it is the case that P (û_{1}, …, û_{n}) is effectively known to hold.

6. ¬P (u_{1}, …, u_{n}) is fulfilled w.r.t. ⟶ and S if there is an index set I ⊆ {1, …, n} such that, setting J := {1, …, n}\I, for each i ∈ I, there are û_{i} ∈ BT(S,V) and ϱ_{i} : V(û_{i}) → T (S, V) with u_{i}⟶^{∗}û_{i}ϱ_{i}, such that, for all (û_{j})_{j∈J} with ∀j ∈ J. (û_{j} ∈ BT(S,V)), it is the case that P (û_{1}, …, û_{n}) is effectively known not to hold.

4Note that, contrary to Item 3 of Definition 22 of [Wirth, 2009], ≠ can be seen as the built-in [constant-] inequality predicate on BT(S,V). Indeed, ≠ may exploit inequality of the matching terms from EBT(S,V), even if matching terms from BT(S,V) are equal.

5Note that, contrary to Item 4 of Definition 22 of [Wirth, 2009], Def (“definedness”) cannot be seen as the built-in universal predicate on BT(S,V). Again, however, but now for a different reason, namely because its negation is not consistent w.r.t. consistent extension, ¬(Def u) is not admitted as a condition literal.

The reason why we admit I to be a proper subset of {1, …, n} is that, e.g. for

P (u_{1}, u_{2}, u_{3}, u_{4})

being a lexicographic ordering such as

(u_{1}, u_{2}) < (u_{3}, u_{4}),

it should be sufficient that u_{1} reduces to a shorter term in T (S, X)_{C} than u_{3}, even if u_{2} does not reduce to any term of T (S, X)_{C} at all. Choose I := {1, 3}. Then

(0, 0 − s(0)) < (s(0), 0 − s(s(0)))

is fulfilled, disregarding the undefined terms in the second elements of the pairs, simply because we have

(0, û_{2}) < (s(0), û_{4})

for all (û_{j})_{j∈{2,4}} with ∀j ∈ {2, 4}. (û_{j} ∈ T (S, X)_{C}).

Let us assume that ⟶ is confluent. Then u_{1}↓u_{2} iff u_{1}⟷^{∗}u_{2}. Thus, equality literals are tested for equality in the quotient modulo ⟷^{∗}. Moreover, P (u_{1}, …, u_{n}) and ¬P (u_{1}, …, u_{n}) cannot both be fulfilled w.r.t. a confluent ⟶ and S, because an argument with an index in the intersection of the two index sets would have to have two different normal forms; cf. the proof of Lemma 3.15 for more details. But fulfilledness of P (u_{1}, …, u_{n}) and ¬P (u_{1}, …, u_{n}) does not have to satisfy tertium non datur, cf. [Wirth, 2009, Note 3].

As the reference to the reduction relation ⟶ will vary a lot, whereas S will be more constant or clear from the context, in what follows we will often speak of “fulfilledness w.r.t. ⟶” where we would actually have to speak of “fulfilledness w.r.t. ⟶ and S”.

Finally, note that fulfilledness is monotonic, indeed, as presupposed for the validity of Corollary 3.2.

3.4 Compatibility with [Wirth, 2009]

Although, as already said, we will simply assume confluence in this paper, our treatment here would be meaningless in practice unless we show that our new notions of fulfilledness here is compatible with the results of [Wirth, 2009]. Contrary to the notion of fulfilledness of [Wirth, 2009], our notion of fulfilledness here also applies to sorts s with s ∉ 𝕊_{NJ} ∩𝕊_{NC}, and is identical to the one of [Wirth, 2009] only for the case of 𝕊 = 𝕊_{NJ} ∩𝕊_{NC}. Luckily, the whole treatment of fulfilledness in [Wirth, 2009] (with the exception of equality literals) is confined to two lemmas, which we have to re-proof now.

As a corollary of Corollary 3.9 we get:

Corollary 3.11 Let n_{0}, n_{1} ∈ N. Assume that R, X is shallow confluent up to n_{0}+n_{1}. Let u, v ∈ T (S, V), û ∈ ECT(S,V), and ϱ : V(û) → T (S, V).

If v⟵^{∗}_{R,X,n_{0}}u⟶^{∗}_{R,X,n_{1}} ûϱ, then there is a ϱ′ : V(û) → T (S, V) with v⟶^{∗}_{R,X,n_{1}} ûϱ′.

As a corollary of Corollaries 3.9 and 2.15 we get:

Corollary 3.12 Let T ∈ {BT(S,V), EBT(S,V)}. For each i ∈ {0, 1}, let û_{i} ∈ T and ϱ_{i} : V(û_{i}) → T (S, V). If û_{0}ϱ_{0}↓_{R,X} û_{1}ϱ_{1}, then û_{0}, û_{1} are constant-equal.

Lemma 3.13 (Variable-Overlap Lemma [Wirth, 2009, Lemma 24]) Let n_{0}, n_{1} ∈ N. Let (l=r⟵C) ∈ R. Let μ, ν : V(l=r⟵C) → T (S, X). If R, X is shallow confluent up to n_{0}+n_{1}, C is weak-quasi-normal w.r.t. R, X, Cμ is fulfilled w.r.t. ⟶_{R,X,n_{1}} and S, and ∀x ∈ V(C). (xμ⟶^{∗}_{R,X,n_{0}}xν); then lν⟶_{R,X,n_{1}+1}rν and Cν is fulfilled w.r.t. ⟶_{R,X,n_{1}} and S.

Proof of Lemma 3.13 It suffices to show, for each literal L in C, that Lν is fulfilled w.r.t. ⟶_{R,X,n_{1}} under the assumption that Cμ is fulfilled w.r.t. ⟶_{R,X,n_{1}}; cf. Definition 3.10.

\underline{L = (u_{0}=u_{1}):} By ∀x ∈ V(C). xμ⟶^{∗}_{R,X,n_{0}}xν and Corollary 3.4, we get

u_{0}ν⟵^{∗}_{R,X,n_{0}}u_{0}μ↓_{R,X,n_{1}}u_{1}μ⟶^{∗}_{R,X,n_{0}}u_{1}ν.

As C is assumed to be weak-quasi-normal w.r.t. R, X, we have to distinguish the following cases: Firstly, in the case of V(u_{0}, u_{1}) ⊆ V_{C}, by Corollary 2.8 we have for all x ∈ V(u_{0}, u_{1}): xμ ∈ T_{C}(X). Then, by Corollaries 3.2 and 3.8, we have u_{0}ν = u_{0}μ↓_{R,X,n_{1}}u_{1}μ = u_{1}ν.

Secondly, if there is is an i ∈ {0, 1} such that (Def u_{i}μ) occurs in Cμ or that u_{i}μ ∈ T (S, V)_{C}, then there is a v̂ ∈ T (S, V)_{C} with u_{i}μ⟶^{∗}_{R,X,n_{1}} v̂. By Corollary 3.8 and [Wirth, 2009, Lemma 15(4)], we get the desired u_{0}ν↓_{R,X,n_{1}}u_{1}ν again.

\underline{L = (u_{0}≠u_{1}):} For i ∈ \{0, 1\}, there are û_{i} ∈ EBT(S,V) and ϱ_{i} : V(û_{i}) → T (S, V) with

u_{i}ν⟵^{∗}_{R,X,n_{0}}u_{i}μ⟶^{∗}_{R,X,n_{1}} û_{i}ϱ_{i} and û_{0} ≠ û_{1}. By Corollary 3.11, there are

ϱ′_{i} : V(û_{i}) → T (S, V) with u_{i}ν⟶^{∗}_{R,X,n_{1}} û_{i}ϱ′_{i}.

\underline{L = (Def u):} Then there is a v̂ ∈ T (S, V)_{C} with uν⟵^{∗}_{R,X,n_{0}}uμ⟶^{∗}_{R,X,n_{1}} v̂. By Corollary 3.8 and [Wirth, 2009, Lemma 15(3)], we get uν⟶^{∗}_{R,X,n_{1}} v̂.

\underline{L = [¬]P (u_{1}, …, u_{k}):} For i ∈ I, there are û_{i} ∈ BT(S,V) and ϱ_{i} : V(û_{i}) → T (S, V)

with u_{i}ν⟵^{∗}_{R,X,n_{0}}u_{i}μ⟶^{∗}_{R,X,n_{1}} û_{i}ϱ_{i} and P (û_{1}, …, û_{k}) [not] holding for

all (û_{j})_{j∈J} with ∀j ∈ J. (û_{j} ∈ BT(S,V)). By Corollary 3.11, there are ϱ′_{i} : V(û_{i}) → T (S, V) with u_{i}ν⟶^{∗}_{R,X,n_{1}} û_{i}ϱ′_{i} for all i ∈ I. Q.e.d. (Lemma 3.13)

Definition 3.14 (Complementarity of Condition Lists) Two condition lists D_{0} and D_{1} are complementary if for a permutation k of {0, 1}, for each i ∈ {0, 1}, D_{k_{i}} lists a literal L_{i}, such that at least one of the following cases holds:

1. L_{0} has the form P (u_{1}, …, u_{m}) and L_{1} has the form ¬P (u_{1}, …, u_{m}) for some built-in predicate P on BT(S,V).

2. L_{0} has the form (u_{1}=u_{2}) and L_{1} has the form (u_{1}≠u_{2}); and there is an l ∈ {1, 2} such that u_{l} ∈ T (S, V)_{C} or D_{k_{0}} lists (Def u_{l}).

3. Let T ∈ {T (S, V)_{C}, BT(S,V), EBT(S,V)} be fixed.

Now, for each i ∈ {0, 1}, L_{i} has the form (p=c_{i}) with c_{i} ∈ T, such that c_{0}φ ≠ c_{1}φ for all μ : V(c_{0}, c_{1}) → T (S, X).

4. L_{i} has the form P_{i}(y_{i,1}, …, y_{i,m′_{i}})σ for distinct variables y_{i,1}, …, y_{i,m′_{i}} ∈ V for each i ∈ {0, 1} and some σ : V → T (S, V) such that

¬∃y_{0,1}, …, y_{0,m′_{0}}, y_{1,1}, …, y_{1,m′_{1}} ∈ BT(S,V). \binom{P_{0}(y_{0,1}, …, y_{0,m′_{0}})}{∧ P_{1}(y_{1,1}, …, y_{1,m′_{1}})}

is an element of a fixed decidable set of theorems of the built-in predicates P_{0} and P_{1} on BT(S,V).

5. L_{0} has the form (y_{0,1}=y_{0,2})σ and L_{1} has the form P (y_{1,1}, …, y_{1,m′_{1}})σ for variables y_{i,j} ∈ V and σ : V → T (S, V) such that y_{1,1}, …, y_{1,m′_{1}} are distinct and

¬∃y_{0,1}, y_{0,2}, y_{1,1}, …, y_{1,m′_{1}} ∈ BT(S,V). \binom{(y_{0,1}=y_{0,2})}{∧ P (y_{1,1}, …, y_{1,m′_{1}})}

is an element of a fixed decidable set of theorems of the built-in predicate P on BT(S,V); and there is an l ∈ {1, 2} such that

y_{0,l}σ ∈ T (S, V)_{C} or D_{k_{0}} lists (Def y_{0,l}σ).

Lemma 3.15 ([Wirth, 2009, Lemma 62]) Each binding-complementary critical peak is shallow trivial.

Proof of Lemma 3.15

We omit the subscript R, X in this proof. Assume the situation and notation of Definition 3.14 and [Wirth, 2009, Definition 58]. To show shallow triviality, we assume that the condition of [Wirth, 2009, Definition 30] is satisfied for some φ : V → T (S, X) and some n_{0}, n_{1} ∈ N, and will derive a contradiction. Under this assumption, (Cξ_{i})φ, (D′_{i}ξ_{i})φ is fulfilled w.r.t. ⟶_{n_{i}}, and R, X is shallow confluent up to n_{0}+n_{1}. Define ψ_{i} : V → T (S, X) by yψ_{i} := yξ_{i}φ for y ∈ {x_{1}, …, x_{m}}∪Z, and yψ_{i} := yφ for y ∈ V \ ({x_{1}, …, x_{m}}∪Z). Then Cψ_{i}, D′_{i}ψ_{i} is fulfilled w.r.t. ⟶_{R,X,n_{i}}, and yψ_{0} = yψ_{1} for y ∈ V \ ({x_{1}, …, x_{m}}∪Z). As C contains binding equations for the variables x_{1}, …, x_{m} whose left-hand sides do not contain variables from the set Z, by [Wirth, 2009, Lemma 47] we get x_{j}ψ_{0} = x_{j}ψ_{1} for all j ∈ {1, …, m}. Thus, due to Z ∩ V(D′_{i}) = ∅, D′_{i}ψ_{1} is fulfilled w.r.t. ⟶_{R,X,n_{i}}. By the assumed complementarity there must be complementary literals in D′_{0} and D′_{1}. Thus, assume k to be a permutation of {0, 1} as described in Definition 3.14. We distinguish the cases of Definition 3.14:

\underline{Case 1:} When we consider ¬P as the name of the built-in predicate on BT(S,V) complementary to P, by Definition 3.10 this is a subcase of Case 4 for y_{0,j} = y_{1,j} and y_{0,j}σ = u_{j}.

\underline{Case 2:} In this case we have (u_{1}=u_{2}) in D′_{k_{0}} and (u_{1}≠u_{2}) in D′_{k_{1}} and there is an l ∈ \{1, 2\}

such that (Def u_{l}) is in D′_{k_{0}} unless u_{l} ∈ T (S, V)_{C}. By Corollaries 2.8 and 3.8, we get y_{0,l}ψ_{1}⟶^{∗}_{n_{k_{0}}} û ∉ dom(⟶) for some û. Moreover, for each i ∈ {0, 1}, there are v̂_{i} ∈ EBT(S,V) and ϱ_{i} : V(v̂_{i}) → T (S, V), such that v̂_{0} ≠ v̂_{1} are not constant-equal and

v̂_{0}ϱ_{0}⟵^{∗}_{n_{k_{1}}} u_{1}ψ_{1}⟶^{∗}_{n_{k_{0}}} ∘ ⟵^{∗}_{n_{k_{0}}} u_{2}ψ_{1}⟶^{∗}_{n_{k_{1}}} v̂_{1}ϱ_{1}.

By [Wirth, 2009, Lemma 15(4)] and Corollaries 3.2 and 3.8, we get v̂_{0}ϱ_{0}↓_{n_{k_{0}}} v̂_{1}ϱ_{1}. By Corollaries 3.2 and 3.12 we get the contradictory fact that v̂_{0}, v̂_{1} are constant-equal.

\underline{Case 3:} In this case we have (p=c_{i}) in D′_{k_{i}}. Thus, for some w_{0}, w_{1}, we have

c_{0}ψ_{1}⟶^{∗}_{n_{k_{0}}} w_{0}⟵^{∗}_{n_{k_{0}}} pψ_{1}⟶^{∗}_{n_{k_{1}}} w_{1}⟵^{∗}_{n_{k_{1}}} c_{1}ψ_{1}.

By shallow confluence, there is some ŵ with

c_{0}ψ_{1}⟶^{∗}_{n_{k_{0}}} w_{0}⟶^{∗}_{n_{k_{1}}} ŵ⟵^{∗}_{n_{k_{0}}} w_{1}⟵^{∗}_{n_{k_{1}}} c_{1}ψ_{1}.

Thus, by Corollary 3.2 c_{0}ψ_{1}↓c_{1}ψ_{1}. In case of T = T (S, V)_{C}, we get the contradictory c_{0}ψ_{1} = c_{1}ψ_{1} by Corollaries 2.8 and 3.8. In case of T ∈ {BT(S,V), EBT(S,V)}, we know that c_{0}, c_{1} are constructor-equal by Corollary 3.12. By Corollary 2.9 there is some μ : V(c_{0}, c_{1}) → T (S, V) with c_{0}μ = c_{1}μ, which contradicts the case again.

\underline{Case 4:} In this case we have P_{i}(y_{i,1}, …, y_{i,m′_{i}})σ in D′_{k_{i}}. Then, for all i ∈ \{0, 1\}, there

are I_{i} ⊆ {1, …, m′_{i}} and, for all j ∈ I_{i}, there are v̂_{i,j} ∈ BT(S,V) and

ϱ_{i,j} : V(v̂_{i,j}) → T (S, V) with y_{i,j}σψ_{1}⟶^{∗}_{n_{k_{i}}} v̂_{i,j}ϱ_{i,j}, such that P_{i}(v̂_{i,1}, …, v̂_{i,m′_{i}}) is known to

hold for all v̂_{i,j} ∈ BT(S,V) (j ∈ {1, …, m′_{i}}\I_{i}). Thus, by the known theorem on P_{0} and P_{1}, namely

¬∃y_{0,1}, …, y_{0,m′_{0}}, y_{1,1}, …, y_{1,m′_{1}} ∈ BT(S,V). \binom{P_{0}(y_{0,1}, …, y_{0,m′_{0}})}{∧ P_{1}(y_{1,1}, …, y_{1,m′_{1}})},

as the variables y_{i,1}, …, y_{i,m′_{i}} are distinct, there must be n′_{0} ∈ I_{0} and n′_{1} ∈ I_{1} with y_{0,n′_{0}} = y_{1,n′_{1}}, but v̂_{0,n′_{0}}, v̂_{1,n′_{1}} are not constant-equal. Thus, we have

v̂_{0,n′_{0}}ϱ_{0,n′_{0}} ⟵^{∗}_{n_{k_{0}}} y_{0,n′_{0}}σψ_{1} = y_{1,n′_{1}}σψ_{1}⟶^{∗}_{n_{k_{1}}} v̂_{1,n′_{1}}ϱ_{1,n′_{1}}.

By shallow confluence and Corollary 3.2 we get v̂_{0,n′_{0}}ϱ_{0,n′_{0}}↓v̂_{1,n′_{1}}ϱ_{1,n′_{1}}. Thus, by Corollary 3.12 get the contradictory fact that v̂_{0,n′_{0}}, v̂_{1,n′_{1}} are constant-equal.

\underline{Case 5:} In this case we have (y_{0,1}=y_{0,2})σ in D′_{k_{0}} and P (y_{1,1}, …, y_{1,m′_{1}})σ in D′_{k_{1}} and there is

an l ∈ {1, 2} such that (Def y_{0,l}σ) is in D′_{k_{0}} unless y_{0,l}σ ∈ T_{C}(V). By Corollaries 2.8 and 3.8, we get y_{0,l}σψ_{1}⟶^{∗}_{n_{k_{0}}} û ∉ dom(⟶) for some û. There is a I ⊆ {1, …, m′_{1}} and, for all j ∈ I, there are v̂_{j} ∈ BT(S,V) and

ϱ_{j} : V(v̂_{j}) → T (S, V) with y_{1,j}σψ_{1}⟶^{∗}_{n_{k_{1}}} v̂_{j}ϱ_{j}, such that P (v̂_{1}, …, v̂_{m′_{1}}) is known to hold

for all v̂_{j} ∈ BT(S,V) (j ∈ {1, …, m′_{1}}\I). Thus, by the known theorem on P, namely

¬∃y_{0,1}, y_{0,2}, y_{1,1}, …, y_{1,m′_{1}} ∈ BT(S,V). \binom{(y_{0,1}=y_{0,2})}{∧ P (y_{1,1}, …, y_{1,m′_{1}})},

as the variables y_{1,1}, …, y_{1,m′_{1}} are distinct, there must be n′_{0}, n′_{1} ∈ I with y_{0,1} = y_{1,n′_{0}} and y_{0,2} = y_{1,n′_{1}}, but v̂_{n′_{0}}, v̂_{n′_{1}} are not constant-equal. Thus, we have

v̂_{n′_{0}}ϱ_{n′_{0}} ⟵^{∗}_{n_{k_{1}}} y_{0,1}σψ_{1}⟶^{∗}_{n_{k_{0}}} ∘ ⟵^{∗}_{n_{k_{0}}} y_{0,2}σψ_{1}⟶^{∗}_{n_{k_{1}}} v̂_{n′_{1}}ϱ_{n′_{1}}.

By [Wirth, 2009, Lemma 15(4)] and Corollaries 3.2 and 3.8, we get v̂_{n′_{0}}ϱ_{n′_{0}}↓_{n_{k_{0}}} v̂_{n′_{1}}ϱ_{n′_{1}}. By Corollaries 3.2 and 3.12 we get the contradictory fact that v̂_{n′_{0}}, v̂_{n′_{1}} are constant-equal.

Q.e.d. (Lemma 3.15)

4 Specification

Definition 4.1 (Specification)

A specification S = (𝕊, 𝔽, 𝔻, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, ℙ, R) is a 9-tuple with the following properties:

1. (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻) is a signature. We re-use our notation on signatures — such as T (S, V) — for specifications by considering the triple of the first seven elements of S as the signature referred to.

2. ℙ is a set of (constant) predicate symbols disjoint from 𝔽, such that, for each predicate symbol P ∈ ℙ, there is a declaration in 𝔻 of the form P : s_{0}, …, s_{n−1} with n ∈ N and s_{j} ∈ 𝕊 for j ∈ {0, …, n−1}.

3. R is a CTRS, i.e. a conditional term rewriting system, i.e. a set of (conditional) equations. A (conditional) equation is a triple l=r⟵C consisting of two terms of the same sort, namely the left-hand side l and the right-hand side r, and the condition C.^{6} If the condition is empty, i.e. if C = ∅, the equation is unconditional and we simply write l=r instead of l=r⟵C.

4. Let V be a variable-system for S. For each s′ ∈ 𝕊_{NJ}, we require that the set CT(S,V)_{s′} is non-empty.

5. All elements of 𝕊_{E} are of the form h⇾v for some sorts h, v ∈ 𝕊 with (h⇾v) > h > v. And if (h⇾v) ∈ 𝕊_{E}, then there is some _[_] ∈ 𝔽 such that 𝔻 contains the declaration _[_] : (h⇾v) → h → v, G.

6. For each declaration of the form

d : s_{0} → ⋯ → s_{n}, D, j,

we require that 𝔻 contains the following declarations:

(a) In case of s_{j} > s_{n}, for ŝ:= s_{n}: d_{s_{0},...,s_{n−1}}^{j} : s_{0} → ⋯ → s_{j−1} → s_{j+1} → ⋯ → s_{n−1} → (s_{j}⇾ŝ), C.

(b) In case of s_{j} ∼ s_{n}, for any ŝ ∈ 𝕊 with (s_{n}⇾ŝ) ∈ 𝕊_{E}:

_d_{s_{0},...,s_{n−1}}^{j} : (s_{n}⇾ŝ) → s_{0} → ⋯ → s_{j−1} → s_{j+1} → ⋯ → s_{n−1} → (s_{j}⇾ŝ), C.

Moreover, the declarations of constructors of all experimental sorts s_{j}⇾ŝ are minimally generated this way by some destructor of s_{j}, and the set 𝕊_{E} is the smallest set such that the sorts of the declarations of these constructor symbols belong to 𝕊.

Finally, R has to contain the following unconditional equations for some X_{k} ∈ V_{G,s_{k}} for k ∈ {0, …, n−1}:

(a) In case of s_{j} > s_{n}, for ŝ:= s_{n}:

(d_{s_{0},...,s_{n−1}}^{j}:ŝ) d_{s_{0},...,s_{n−1}}^{j}(X_{0}, …, X_{j−1}, X_{j+1}, …, X_{n−1})[X_{j}] = d(X_{0}, …, X_{n})

(b) In case of s_{j} ∼ s_{n}, for any ŝ ∈ 𝕊 with (s_{n}⇾ŝ) ∈ 𝕊_{E}, and for E ∈ V_{G,s_{n}⇾ŝ}:

(d_{s_{0},...,s_{n−1}}^{j}:ŝ) E d_{s_{0},...,s_{n−1}}^{j}(X_{0}, …, X_{j−1}, X_{j+1}, …, X_{n−1})[X_{j}] = E[d(X_{0}, …, X_{n})]

6It is to be interpreted as: “For all variables from V(l=r⟵C), the left-hand side l is equal to the right-hand side r if the condition C holds.”

Note that Items 5 and 6 of Definition 2.1 describe a generic way of extending the specification for the visible and hidden sorts that are smaller than the experimental sorts. Indeed, in [Roşu, 2004, Definition 4.1], this generic way of extension is defined as an afterthought in what is called “unhiding a signature”. The reason why we have chosen to integrate it directly into our definition of a signature is that otherwise we cannot introduce greater sorts on the basis of the experimental sorts. This does not mean that we have to specify the experimental sorts explicitly in our examples. We can use them, however, for the specification of additional sorts, such as lists or streams of experiments.

Moreover, note that — contrary to [Roşu, 2004] — we may have experimental sorts h⇾ŝ with ŝ∈ 𝕊_{D}, i.e. the results of experiments may be hidden sorts. Note that this may happen only if h>ŝ; but especially not if h∼ŝ, in which case we end up in Item 9b of Definition 2.1 analogous to [Roşu, 2004, Definition 4.1].

Definition 4.2 (Satisfaction)

Let S be an S-structure for the specification S = (𝕊, 𝔽, 𝔻, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, ℙ, R), i.e. for the signature (𝕊, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, 𝔽, ℙ, 𝔻).

S is a model of S if the following holds:

• The constructor universes (C, s)^{S} are constructed recursively over the well-founded ordering < of the quasi-ordering ≲ as follows:

– If s ∈ 𝕊_{NJ} ∩ 𝕊_{NC}, then (C, s)^{S} = { tσ | t ∈ CT(S,V) ∧ σ : V(t) → S }; and for

any declaration of the form c : s′_{0} → ⋯ s′_{n−1} → s, C in 𝔻 we have

c_{s′_{0},...,s′_{n−1}}^{S}(o_{0}, …, o_{n−1}) = c_{s′_{0},...,s′_{n−1}}(o_{0}, …, o_{n−1}).

– If s ∈ 𝕊_{NJ} \𝕊_{NC}, then (C, s)^{S} = { ⟨{tσ}⟩≈ | t ∈ CT(S,V) ∧ σ : V(t) → S }; and for any declaration of the form c : s′_{0} → ⋯ s′_{n−1} → s, C in 𝔻 we have

c_{s′_{0},...,s′_{n−1}}^{S}(o_{0}, …, o_{n−1}) = c_{s′_{0},...,s′_{n−1}}(o_{0}, …, o_{n−1}).

– If s ∈ 𝕊_{NC}\𝕊_{NJ},

– If s ∈ 𝕊\(𝕊_{NJ} ∪ 𝕊_{NC}),

– if s ∈ 𝕊_{C}, for each s′ ∈ 𝕊_{C} with s′∼s, we have that (C, s′)^{S} is the smallest set such that, for each c ∈ ℂ declared as c : s_{0} → ⋯ → s_{n−1} → s′, and for each o_{i} ∈ (C, s_{i})^{S} (i ∈ {0, …, n−1}), we have c(o_{0}, …, o_{n−1}) ∈ (C, s′)^{S}; and,

– if s ∈ 𝕊_{D}, then (C, s)^{S} is the set of functions f whose domain is the set of pairs (e, τ), where e ∈ E_{s} is an experiment of sort s, where τ is an S-valuation on V(e) \ {•_{s,0}}, and where f(e, τ) ∈ (C, s)^{S}.

• For each c ∈ Σ_{C} declared as c : s_{0} → ⋯ → s_{n} we have the following:

– In case of s_{n} ∈ Σ_{C}:

For each o_{0}, …, o_{n−1} with o_{i} ∈ (C, s_{i}) for each i ∈ {0, …, n−1}, we have

c^{S}(o_{0}, …, o_{n−1}) = c(o_{0}, …, o_{n−1}).

• For each d ∈ 𝔽 declared as d : s_{0} → ⋯ → s_{n}, D we have the following:

– In case of s_{n}<s_{0}:

For each o_{0}, …, o_{n−1} with o_{i} ∈ (C, s_{i}) for each i ∈ {0, …, n−1}, we have

d^{S}(o_{0}, …, o_{n−1}) = o_{0}(e, τ)

for

e := d(•_{s_{0},0}, •_{s_{1},1}, …, •_{s_{n−1},n−1})

and

τ := { •_{s_{j},j} ↦ o_{j} | j ∈ {1, …, n−1} }.

– In case of s_{n}∼s_{0}:

For each o_{0}, …, o_{n−1} with o_{i} ∈ (C, s_{i}) for each i ∈ {0, …, n−1}, we have

d^{S}(o_{0}, …, o_{n−1}) = f

where the function f is given as follows: For each e ∈ E_{s_{n}} and each S-valuation τ on V(e) \ {•_{s,0}}, we have

f(e, τ) := o_{0}(eσ, τ⊎τ′)

for

σ := { •_{s_{n},0} ↦ d(•_{s_{0},0}, •_{s_{1},m+1}, …, •_{s_{n−1},m+n−1}) }

for

m := |V(e)| − 1,

and

τ′ := { •_{s_{m+j},j} ↦ o_{j} | j ∈ {1, …, n−1} }.

Example 4.3 (Cf. [Wirth, 2009, Example 8]) Let S = (𝕊, 𝔽, 𝔻, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, ℙ, R) be generated from the following:

𝕊_{C} ∋ bool, nat, (nat, nat), list(term), term, (nat, set(term)) 𝕊_{D} ∋ set(term), stream((nat, set(term))) nat ≲ (nat, nat) nat ≲ term ≲ list(term) ≲ term term ≲ set(term) ≲ (nat, set(term)) ≲ stream((nat, set(term))) 𝔽 ∋ true, false, 0, s, (_, _), nil, cons, var, term, set

𝔻 ∋ \{ \begin{matrix}true, false & : & & & bool, & C \\ 0 & : & & & nat, & C \\ s & : & nat & → & nat, & C \\ (_, _) & : & nat → nat & → & (nat, nat) , & C \\ nil & : & & & list(term), & C \\ cons & : & term → list(term) & → & list(term), & C \\ var & : & nat & → & term, & C \\ term & : & nat → list(term) & → & term, & C \\ set & : & list(term) & → & set(term), & C \\ (_, _) & : & nat → set(term) & → & (nat, set(term)), & C \end{matrix}

The domains are the Boolean values bool given by the constructors true and false, the natural numbers nat given by the constructors zero 0 and successor s, pairs over natural numbers (nat, nat) given by the constructor (_, _), lists of terms list(term) given by the constructors nil and cons, and terms term given by the constructors var (mapping a natural number to a variable) term (constructing a term from a natural number encoding a function symbol and a list of terms).

𝔽 ∋ in, hd, tl

𝔻 ∋ \{ \begin{matrix}in & : & term → set(term) & → & bool, & D \\ hd & : & stream((nat, set(term))) & → & (nat, set(term)), & D \\ tl & : & stream((nat, set(term))) & → & stream((nat, set(term))), & D \end{matrix}

The domains are 𝔽 ∋ _+_, _−_, divrest, well, welltail, length, mbp, or, and, arity

𝔻 ∋ \{ \begin{matrix}or, and & : & bool → bool & → & bool, & G \\ well & : & term & → & bool, & G \\ welltail & : & list(term) & → & bool, & G \\ mbp & : & term → list(term) & → & bool, & G \\ arity & : & nat & → & nat, & G \\ _+ _, _− _ & : & nat → nat & → & nat, & G \\ length & : & list(term) & → & nat, & G \\ divrest & : & nat → nat & → & (nat, nat), & G \end{matrix}

ℙ ∋ _<_, _≤_ 𝔻 ∋ { _<_, _≤_: nat, nat V_{C,nat} ∋ x, y, z_{1}, z_{2}, r, q V_{G,bool} ∋ B_{1}, B_{2}

V_{G,term} ∋ T

V_{G,list(term)} ∋ L

Let R_{4.3} denote the CTRS consisting of the following (conditional) equations:

(in : set1) in(T , set(L)) = mbp(T , L)
(plus1) x + 0 = x
(plus2) x + s(y) = s(x+y)

(minus1) x − 0  = x
(minus2) s(x) − s(y) = x−y
(divrest1) divrest(x, y) = (0, x) ⟵ x < y
(divrest2) divrest(x, y) = (s(q), r) ⟵ y ≤ x, y ≠ 0, divrest(x−y, y) = (q, r)
(well1) well(var(x))  = true
(well2) well(term(x, L)) = false  ⟵ arity(x)=z_{1}, length(L)=z_{2}, z_{1}≠z_{2}
(well3) well(term(x, L)) = welltail(L) ⟵ arity(x)=z_{1}, length(L)=z_{2}, z_{1}=z_{2}
(welltail1) welltail(nil)  = true
(welltail2) welltail(cons(T , L)) = false  ⟵ well(T)=false
(welltail3) welltail(cons(T , L)) = welltail(L) ⟵ well(T)=true
(length1) length(nil)  = 0
(length2) length(cons(T , L)) = s(length(L))

(mbp1) mbp(T , nil) = false

(or1) or(false, B_{2}) = B_{2}
(or2) or(B_{1}, false) = B_{1}
(or3) or(true, B_{2}) = true
(or4) or(B_{1}, true) = true

(and1) and(false, B_{2}) = false
(and2) and(B_{1}, false) = false
(and3) and(true, B_{2}) = B_{2}
(and4) and(B_{1}, true) = B_{1}

There are addition _+_, minus _−_, and a division function divrest(_, _). The function divrest computes a pair consisting of the quotient and the remainder. Moreover, there is a well-formedness predicate well(_) (actually a characteristic function). well(_) checks whether the number of arguments of each function symbol in a term is equal to its arity according to the partially specified function arity(_). Furthermore, there is an incomplete definition of the member predicate mbp(_, _) on lists of terms list(term), which will be extended in what follows in different ways. Finally, there are definitions of Boolean disjunction or(_, _) and conjunction and(_, _), which are non-strict, i.e. which may return defined values (i.e. constructor terms) even when some arguments are undefined.

Notice that minus, divrest, well, and mbp are partial due to the specifying case analysis (minus and mbp syntactically, the others by their conditions). There may also be functions that are partially defined due to non-termination. Partial and lazy incremental specification is important for inductive theorem proving in practice; cf. [Löchner, 2006] and [Wirth, 2006].

Furthermore, in the equation (divrest2) we have an example of a binding equation, namely divrest(x−y, y) = (q, r), which introduces the extra variables q, r, which do not occur in the function-call divrest(x, y) of the left-hand side, but are then used to describe the return-value (s(q), r) of the right-hand side. In the equations (well2) and (well3) we find the binding equations arity(x)=z_{1} and length(L)=z_{2}, binding the extra variables z_{1} and z_{2} for later use in the same condition list.

Finally note that the predicate symbols from ℙ do not receive a specification by a CTRS. They are built-in predicates on the constructor sub-universes.

Let us see how the implicitly given experimental sorts and their constructors look like. To simplify notation let us write stream instead of stream((nat, set(term))).

𝕊_{E} ∋ set(term)⇾bool, stream⇾(nat, set(term))

V_{G,set(term)} ∋ M

V_{G,stream} ∋ S

V_{G,stream⇾(nat,set(term))} ∋ E

𝔻 ∋ \{ \begin{matrix}in_{1} & : & term & → & set(term)⇾bool \\ hd_{0} & : & & & stream⇾(nat, set(term)) \\ _tl_{0} & : & stream⇾(nat, set(term)) & → & stream⇾(nat, set(term)) \\ app & : & set(term)⇾bool → set(term) & → & bool \\ app & : & stream⇾(nat, set(term)) → stream & → & (nat, set(term)) \end{matrix}

(in_{1} : bool)  in_{1}(T)[M] = in(T , M)
(hd_{0} : (nat, set(term))) hd_{0}[S] = hd(S)
(tl_{0} : (nat, set(term))) E tl_{0}[S] = E[tl(S)]

Example 4.4 Let the CTRS R_{4.4} consist of R_{4.3} of Example 4.3 plus:

(mbp2) mbp(p_{1}, cons(p_{2}, L)) = true  ⟵ p_{1}=p_{2}
(mbp3) mbp(p_{1}, cons(p_{2}, L)) = mbp(p_{1}, L) ⟵ p_{1}≠p_{2}

Together with (mbp1) from Example 4.3, the equations (mbp2) and (mbp3) provide us with a most natural definition of membership in lists. It is also one with the minimal number of defined function symbols. Note that the addition of the equations (mbp2) and (mbp3) constitutes a consistent extension of the specification of Example 4.3. We consider it to be obvious that the exclusion of this specification of membership in lists by admissibility conditions would constrict CTRSs to be a more or less theoretical enterprise. Cf. [Wirth, 2009, § 6] for further discussion on this.

Definition 4.5 (Experiment)

Let V be a variable-system for the signature S = (𝕊, 𝔽, 𝔻, 𝕊_{NJ} , 𝕊_{NC}, 𝕊_{E}, ≲, ℙ, R).

Let • : (𝕊×N) → V be an injective function such that •_{s,n} ∈ V_{C,s} for all s ∈ 𝕊 and n ∈ N.

Let ŝ ∈ 𝕊_{D}.

Now the sets of experiments E_{s′} for the sorts s′ ∈ 𝕊_{D} with s′∼ŝ are the smallest sets such that for each d ∈ 𝔽 declared as d : s′ → s_{1} → ⋯ → s_{n}, D we have:

• In case of s_{n}<s′:

d(•_{s′,0}, •_{s_{1},1}, …, •_{s_{n−1},n−1}) ∈ E_{s′}.

• In case of s_{n}∼s′, for each e ∈ E_{s_{n}}:

eσ ∈ E_{s′}

for

σ := { •_{s_{n},0} ↦ d(•_{s′,0}, •_{s_{1},m+1}, …, •_{s_{n−1},m+n−1}) }

for

m := |V(e)| − 1.

References

[Abramsky &al., 1992] S. Abramsky, Dov Gabbay, and T. S. E. Maibaum, editors. Handbook of Logic in Computer Sci.. Clarendon Press, 1992.

[Aït-Kaci & Nivat, 1989] Hassan Aït-Kaci and Maurice Nivat, editors. Resolution of Equations in Algebraic Structures. Academic Press (Elsevier), 1989.

[Avenhaus & Madlener, 1990] JürgenAvenhaus and Klaus Madlener. Term rewriting and equational reasoning. In R. B. Banerji, editor, Formal Techniques in Artificial Intelligence, pages 1–43. Elsevier, 1990.

[Bachmair & Ganzinger, 1991] Leo Bachmair and Harald Ganzinger. Perfect model semantics for logic programs with equality. 1991. In [Furukawa, 1991, pp. 645–659].

[Barendregt, 1984] Hen(dri)k P. Barendregt. The Lambda Calculus. North-Holland (Elsevier), 1984. 2^{nd} ed..

[Becker, 1993] Klaus Becker. Semantics for Positive/Negative-Conditional Rewrite Systems. In 3^{rd} Int. Workshop on Conditional Term Rewriting Systems, Pont-à-Mousson (France), 1992, number 656 in Lecture Notes in Computer Science, pages 213–225. Springer, 1993.

[Bergstra & Klop, 1986] Jan A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluence and termination. J. Computer and System Sci., 32:323–362, 1986.

[Bidoit & Hennicker, 2006] Michel Bidoit and Rolf Hennicker. Constructor-based observational logic. J. of Logic and Algebraic Programming, 67:3–51, 2006.

[Courcelle, 1984] Bruno Courcelle, editor. Proc. 9^{th} Int. Colloquium on Trees in Algebra and Programming (CAAP 1984), Bordeaux. Cambridge Univ. Press, 1984.

[Deemter & Peters, 1996] Kees van Deemter and Stanley Peters, editors. Semantic Ambiguity and Underspecification. CLSI LN No. 55, Stanford, 1996.

[Dershowitz & Jouannaud, 1990] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. 1990. In [Leeuwen, 1990, Vol. B, pp. 243–320].

[Furukawa, 1991] Koichi Furukawa, editor. Proc. 8^{th} Int. Conf. on Logic Programming. MIT Press, 1991.

[Gabbay &al., 1993] Dov Gabbay, Christopher John Hogger, and J. Alan Robinson, editors. Handbook of Logic in Artificial Intelligence and Logic Programming. Vol. 1: Logical Foundations. Clarendon Press, 1993.

[Gentzen, 1938] Gerhard Gentzen. Die gegenwärtige Lage in der mathematischen Grundlagenforschung – Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, Neue Folge, 4:3–44, 1938. Reprinted as facsimile by Wissenschaftliche Buchgesellschaft, Darmstadt, Verlag von S. Hirzel, Stuttgart. English translation in [Gentzen, 1969].

[Gentzen, 1969] Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland (Elsevier), 1969. Ed. by Manfred E. Szabo.

[Gillman, 1987] Leonard Gillman. Writing Mathematics Well. The Mathematical Association of America, 1987.

[Gogolla, 1983] Martin Gogolla. Algebraic Specifications with Partially Ordered Sorts and Declarations. Report 169/1983, FB Informatik, Univ. Dortmund, 1983. Short version is [Gogolla, 1984].

[Gogolla, 1984] Martin Gogolla. Partially ordered sorts in algebraic specifications. 1984. In [Courcelle, 1984, pp. 139–154]. Long version is [Gogolla, 1983].

[Hanus, 1994] Michaël Hanus. On Extra Variables in (Equational) Logic Programming. MPI–I–94–2–246, Max Planck Inst. für Informatik, Saarbrücken, 1994. Short version in [Sterling, 1991, pp. 665–679].

[Hanus, 2006] Michaël Hanus. Curry — an integrated functional logic language. Web

only: http://www.informatik.uni-kiel.de/~curry/report.html, 2006.

[Hobbs, 1996] Jerry R. Hobbs. Monotone decreasing quantifiers in a scope-free logical form. 1996. In [Deemter & Peters, 1996, pp. 55–76]. http://www.isi.edu/~hobbs/

monotone-decreasing.pdf.

[Hudlak &al., 1999] Paul Hudlak, John Peterson, and Joseph H. Fasel. A gentle introduc-

tion to Haskell. Web only: http://www.haskell.org/tutorial, 1999.

[Huet & Lankford, 1978] Gérard Huet and Dallas S. Lankford. On the Uniform Halting Problem for Term Rewriting Systems. Rapport de Recherche 283,

INRIA, 1978.  http://www.ens-lyon.fr/LIP/REWRITING/OLD_PUBLICATIONS_ON_
TERMINATION/HUET_LANKFORD.

[Kaplan, 1988] Stéphane Kaplan. Positive/Negative-Conditional Rewriting. In 1^{st} Int. Workshop on Conditional Term Rewriting Systems, Orsay (France), 1987, number 308 in Lecture Notes in Computer Science, pages 129–143. Springer, 1988.

[Kühler & Wirth, 1996] Ulrich Kühler and Claus-Peter Wirth. Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. SEKI-Report SR–1996–11 (ISSN 1437–4447). SEKI Publications, Univ. Kaiserslautern, 1996. Short version in 8th RTA 1997, LNCS 1232, pp. 38–52, Springer. http:

//www.ags.uni-sb.de/~cp/p/rta97.

[Klop, 1992] Jan Willem Klop. Term rewriting systems. 1992. In [Abramsky &al., 1992, Vol. II, pp. 1–116].

[Leeuwen, 1990] Jan van Leeuwen, editor. Handbook of Theoretical Computer Sci.. MIT Press, 1990.

[Löchner, 2006] Bernd Löchner. Things to know when implementing LPO. Int. J. Artificial Intelligence Tools, 15:53–79, 2006.

[Nipkow &al., 2000] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle’s

Logics: HOL. Web only: http://isabelle.in.tum.de/PSV2000/doc/logics-HOL.

pdf, 2000.

[Nipkow &al., 2002] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Number 2283 in Lecture Notes in Computer Science. Springer, 2002.

[Padawitz, 1988] Peter Padawitz. Computing in Horn Clause Theories. Springer, 1988.

[Padawitz, 2000] Peter Padawitz. Swinging types = functions + relations + transition systems. Theoretical Computer Sci., 243:93–165, 2000.

[Plaisted, 1993] David Plaisted. Equational reasoning and term rewriting systems. 1993. In [Gabbay &al., 1993, pp. 273–364].

[Roşu, 2003] Grigore Roşu. Inductive behavioral proofs by unhiding. Electronic Notes in Theoretical Computer Sci., 82:285–302, 2003. http://dx.doi.org/10.1016/ S1571-0661(04)80645-5. Revised version is [Roşu, 2004].

[Roşu, 2004] Grigore Roşu. Behavioral abstraction is hiding information. Theoretical Com-

puter Sci., 327:197–221, 2004. http://dx.doi.org/10.1016/j.tcs.2004.07.027. Pre-

liminary version is [Roşu, 2003].

[Slind, 1996] Konrad Slind. Function definition in higher-order logic. In 9^{th} TPHOLs 1996, number 1125 in Lecture Notes in Computer Science, pages 381–397. Springer, 1996.

[Smoka &al., 1989] Gerd Smoka, Werner Nutt, Joseph Goguen, and José Meseguer. Ordersorted equational computation. 1989. In [Aït-Kaci & Nivat, 1989, Vol. 2, pp. 297–367].

[Sterling, 1991] Leon Sterling, editor. Proc. 12^{th} Int. Conf. on Logic Programming. MIT Press, 1991.

[Suzuki &al., 1995] Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In 6^{th} Int. Conf. on Rewriting Techniques and Applications, Kaiserslautern, 1995, number 914 in Lecture Notes in Computer Science, pages 179–193. Springer, 1995.

[Waldmann, 1989a] Uwe Waldmann. Semantics of Order-Sorted Specifications. Report 297/1989, FB Informatik, Univ. Dortmund, 1989. Revised version in Theoretical Computer Sci. (1992) 94, pp. 1–35, Elsevier.

[Waldmann, 1989b] Uwe Waldmann. Unification in Order-Sorted Signatures. Report 298/1989, FB Informatik, Univ. Dortmund, 1989. Revised version 1990, http://www.

mpi-sb.mpg.de/~uwe/paper/UNIDO-INF-298.dvi.gz.

[Wirth & Gramlich, 1994a] Claus-Peter Wirth and Bernhard Gramlich. A constructorbased approach for positive/negative-conditional equational specifications. J. Symbolic

Computation, 17:51–90, 1994. http://www.ags.uni-sb.de/~cp/p/jsc94.

[Wirth & Gramlich, 1994b] Claus-Peter Wirth and Bernhard Gramlich. On notions of inductive validity for first-order equational clauses. In Alan Bundy, editor, 12^{th} Int. Conf. on Automated Deduction, Nancy, 1994, number 814 in Lecture Notes in Artificial Intelligence, pages 162–176. Springer, 1994. www.ags.uni-sb.de/~cp/p/cade94.

[Wirth & Lunde, 1994] Claus-Peter Wirth and Rüdiger Lunde. Writing Positive/Negative-Conditional Equations Conveniently. SEKI-Report SR–1994–04 (ISSN 1437–4447). SEKI Publications, Univ. Kaiserslautern, 1994. http://www.ags.uni-sb.de/~cp/p/swp9404.

[Wirth, 1997] Claus-Peter Wirth. Positive/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving, volume 31 of Schriftenreihe Forschungsergebnisse zur Informatik. Verlag Dr. Kovač, Hamburg, Arnoldstr. 49, D–27763 Hamburg, 1997. ISBN 3–86064–551–X,

www.ags.uni-sb.de/~cp/p/diss.

[Wirth, 2006] Claus-Peter Wirth. Progress in Computer-Assisted Inductive Theorem Proving by Human-Orientedness and Descente Infinie? SEKI-Working-Paper SWP–2006–01 (ISSN 1860–5931). SEKI Publications, Saarland Univ., 2006. www.ags.uni-sb.de/~cp/

p/swp200601/welcome.html.

[Wirth, 2009] Claus-Peter Wirth. Shallow confluence of conditional term rewriting systems. J. Symbolic Computation, 44:69–98, 2009. http://www.ags.uni-sb.de/~cp/p/

shallow, http://dx.doi.org/10.1016/j.jsc.2008.05.005.