A Constructor- and Destructor-based Framework for Monotonic (Co-) Inductive

Specification

Claus-Peter Wirth

Brandenburger Str. 42, D-65582 Diez, Germany

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

!!! !!! !!! !!! preliminary version !!! !!! !!! !!! !!! July 23, 2008

Abstract: ???

Contents

1 Plan 1 1.1 Title . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 What the paper is about . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.4 What the paper is NOT about . . . . . . . . . . . . . . . . . . . . . . . 1 1.5 Admissibility condition . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Matter 3

3 Modeling Partial Functions with Total Structures 7

4 Basic Notions for Σ-Structures 10

5 Four Notions of Validity 11

6 Data Universes 13 6.1 Visible Sorts and Constructors . . . . . . . . . . . . . . . . . . . . . . . 13 6.2 Hidden Sorts and Destructors . . . . . . . . . . . . . . . . . . . . . . . . 14

7 Fulfilledness and Rewriting 23

Notes 25

1 Plan

1.1 Title

Notions of (Co) Inductive Validity for Constructor- and Destructor-based Specifications with Partially Defined Operations

1.2 Structure

Part 1 Introduction + (co-) inductive validities + example. 15 p..

Part 2 Monotonicity. 5 p..

Part 3 Relatedness of notions + Discussion + Meta-physics. 15 p..

Follow-up Paper Criteria for the confluence required in part 2. 40 p..

1.3 What the paper is about

CADE’94 paper + co inductive data domains.

1.4 What the paper is NOT about

1.4.1 On purpose

Co-Signatures This is fucking in the presence of terms because it renders the notion of a well-formed term to be a semantical one.

Co-Algebras

Finality

• The final objects can be proper classes and thus cannot provide something like a computational model.

• Congruence modulo bisimularity is not always given, e.g. for labeled state transition systems, for a choice-function on sets, or for some funny stacks of Joseph Goguen.

μ- and ν-Predicates

Termination and Sufficient Completeness Not intended as admissibility conditions.

Sorts that have constructors and destructors By this I mean sorts that have inductive as well as co-inductive objects and where the constructors are having no confusion. (I would not call the constructors of hidden sort of Peter Padawitz constructors because they have confusion.) Sorts in this sense, which are both visible and hidden may be nice in practice but theoretically hard to treat and not really necessary.

2 July 23, 2008

1.4.2 Due to lack of space Proving Higher-Order

1.5 Admissibility condition

The heads of the positive/negative-conditional rules may have the forms 𝔻∗𝕂ℂ ∗ where 𝔻 are the destructor function symbols of the hidden sorts, ℂ the constructors for the visible sorts, and 𝕂 the other function symbols.

2 Matter

We assume the reader to be familiar with the basics of term rewriting (cf. e.g. Avenhaus & Madlener (1990), Klop (1992)) and algebraic specification (cf. e.g. Ehrig & Mahr (1985)).

Since our approach is based on the rigorous syntactic distinction of constructors and destructors, we have to be quite explicit about signatures, terms, substitutions, and algebras.

Definition 2.1 (Variable-System, V()) A variable-system for a set 𝕊 of sorts and a set 𝕂 of function symbols is a {GEN, DAT}×𝕊sorted family V = (V_{ς,s})_{(ς,s)∈{GEN,DAT}×𝕊} of classes V_{ς,s} that are mutually disjoint and disjoint from 𝕂. The variables from V_{DAT,s} and V_{GEN,s} are called the data and general variables of sort s, resp.. By abuse of notation we write V to denote ⋃_{(ς,s)∈{GEN,DAT}×𝕊} V_{ς,s}, &c.. For k being any of these kinds of variables and for a term, formula Γ &c., ‘V_{k}(Γ)’ denotes the set of variables from V_{k} occurring in Γ.

Definition 2.2 (Signature) A signature

Σ = (𝕊, 𝕍, ℍ, 𝕂, ℂ , 𝔻, α, V, •, C, ≲)

consists of

• a set 𝕊 of sorts that partitions (i.e. 𝕊 = 𝕍⊎ℍ) into two disjoint sets 𝕍 and ℍ of visible and hidden sorts, resp.,

• a set 𝕂 of function symbols with two disjoint subsets ℂ and 𝔻 of constructors and destructors, resp.,

• an arity function α : 𝕂 → 𝕊^{+},

• a variable-system V for 𝕊 and 𝕂 where V_{ς,s} is infinite for each (ς, s) ∈ {GEN}×𝕊 ∪ {DAT}×ℍ and V_{DAT,s} = ∅ for each s ∈ ℍ,

and of the following items that will be further explained later, cf. Definition 6.3,

• a function • with dom(•) = ℍ and •_{s} ∈ V_{GEN,s} for all s ∈ ℍ,

• a set C of destructor patterns,

• and a wellfounded quasi-ordering ≲ on 𝕊.

When α is clear from the context, we write f : s_{0} → ⋯ → s_{n} to denote α(f) = s_{0} … s_{n} for f ∈ 𝕂, n ∈ N, and s_{0}, …, s_{n} ∈ 𝕊.

Example 2.3 (Signature) Let bool be the visible sort of Boolean values, nat be the visible sort of natural numbers, stream the hidden sort of finite and infinite streams of natural numbers, and set and list be the sorts of sets and finite lists of these streams, resp.. The constructors for bool are true, false : bool. The constructors for nat are 0 : nat and s : nat → nat. The constructors for list are nil : list and cons : stream → list → list. We have the destructors null : stream → bool, hd : stream → nat, tl : stream → stream, and in : stream → set → bool. We have the three destructor patterns (S ∈ V_{GEN,stream})

null(•_{stream})
hd(•_{stream}) ⟵ null(•_{stream})=false
tl(•_{stream}) ⟵ null(•_{stream})=false
in(S, •_{set}) ⟵ Def S

They say that the behavior of a stream object is given by its value under null and, if this is false (i.e. the stream is not empty), also by its value under hd (returning the first element) and tl (returning the tail of the stream beyond that element). The behavior of a set is given the elements it contains; more precisely, by the value of the functions in(S) : set → bool for S ∈ V_{GEN,stream}. Now, if S is a partially defined or undefined stream, we cannot expect in(S) to return a defined value, which we need, however, e.g. in order to find out that two singleton sets containing the same defined stream are behaviorally equal. Therefore, we have added the condition Def S to the above destructor pattern. Finally, for our wellfounded quasi-ordering we take bool ≲ stream because the first destructor pattern has sort bool and also because the condition literal of the second and third destructor pattern has visible sort bool, we take nat ≲ stream because the head of the second destructor pattern has sort nat, we take stream < set because stream is the sort of the condition literal of the fourth destructor pattern, and stream < list because the constructor cons has hidden argument sort stream. Note that the quasi-ordering ≲ will be used to guarantee that visible sorts are not constructed from hidden sorts whose behavior they define, which would be a vicious circle.

Definition 2.4 (Terms) Let Σ = (𝕊, 𝕍, ℍ, 𝕂, ℂ , 𝔻, α, V, •, C, ≲) be a signature, X be a variable-system for 𝕊 and 𝕂, and s ∈ 𝕊. The set T (Σ, X)_{GEN,s} of terms of sort s denotes the well-sorted first-order terms of fixed arity α over 𝕂 and X of sort s. This means that T (Σ, X)_{GEN,s} are the smallest classes such that X_{GEN,s}⊎X_{DAT,s} ⊆ T (Σ, X)_{GEN,s} and if f : s_{0} → ⋯ → s_{n} (n ∈ N) and, for each i ≺ n, t_{i} ∈ T (Σ, X)_{GEN,s_{i}} then f(t_{0}, …, t_{n−1}) ∈ T (Σ, X)_{GEN,s_{n}}. If s ∈ 𝕍, then the terms in T (Σ, X)_{GEN,s} are called visible. Otherwise, if s ∈ ℍ, they are hidden. The set T (Σ, X)_{DAT,s} of data terms of sort s denotes the subset of terms from T (Σ, X)_{GEN,s} that only contain function symbols from ℂ and variables from (X_{DAT,s})_{s∈𝕊}. The set VGT (Σ, X)_{s} of visible-ground terms of sort s denotes the subset of terms from T (Σ, X)_{GEN,s} that only contain function symbols from ℂ and variables of hidden sort.

Note that the visible-ground terms generalize the constructor ground terms of the constructorbased approach. The difference is that we cannot disallow hidden variables because there are no hidden constructor function symbols that could take their place.

Definition 2.5 (Condition Literal) Let Σ = (𝕊, 𝕍, ℍ, 𝕂, ℂ , 𝔻, α, V, •, C, ≲) be a signature, X be a variable-system for 𝕊 and 𝕂, and s ∈ 𝕊. A condition literal over Σ, X of sort s has one of the three forms ‘Def u’, ‘u=u′’, or ‘u≠u′’ with u, u′ ∈ T (Σ, X)_{s}.

Definition 2.6 (Sensible Signature, Destructor Pattern, ⊲) Let Σ = (𝕊, 𝕍, ℍ, 𝕂, ℂ , 𝔻, α, V, •, C, ≲) be a signature. Let < be the ordering of ≲. We define the wellfounded ordering ⊲ on 𝕊 by (s, s′ ∈ 𝕊):

s⊲s′ if s<s′ or s≲s′ ∧ s ∈ 𝕍 ∧ s′ ∈ ℍ.

Now, Σ is sensible if

• for each constructor c ∈ ℂ with say c : s_{0} → ⋯ → s_{n} (n ∈ N) we have s_{n} ∈ 𝕍 and for each i ≺ n we have (s_{i} ∈ 𝕍 ⇒ s_{i}≲s_{n}) and (s_{i} ∈ ℍ ⇒ s_{i}<s_{n}).

• for each destructor d ∈ 𝔻 with say d : s_{0} → ⋯ → s_{n} (n ∈ N) there is some i ≺ n with s_{i} ∈ ℍ and for each j ≺ n with s_{j} ∈ 𝕍 we have s_{j}≲s_{i}; and

• each destructor pattern from C has the form d(x_{0}, …, x_{n}) ⟵ L_{0}, …, L_{m−1} where n, m ∈ N (for m = 0 we omit the ‘⟵’), d ∈ 𝔻 is a destructor with d : s_{0} → ⋯ → s_{n+1}, {x_{0}, …, x_{n}} ⊆ V, d(x_{0}, …, x_{n}) is a linear term, there is exactly one i ⪯ n with x_{i} ∈ ran(•) (we speak of a destructor pattern for the sort s_{i} and of sort s_{n+1}), and for this i we have s_{n+1}≲s_{i} and for each j ≺ m, L_{j} is a condition literal over Σ, V of sort l_{j} with V(L_{j}) ⊆ {x_{0}, …, x_{n}} and l_{j}⊲s_{i}, and

• for each s ∈ 𝕊 we have VGT (Σ, V)_{s} ≠ ∅.

Note that the quasi-ordering ≲ guarantees that visible sorts are not constructed from hidden sorts whose behavior they define, which would be a vicious circle. Thus, the result sort of a constructor must be visible and its argument sorts must be somehow smaller, whereas the hidden argument sorts of a destructor must be somehow bigger than its result sort, the sorts of its visible arguments, and the sorts of the condition literals of its destructor patterns. Note that in the absence of hidden sorts we can choose ≲ to be 𝕍×𝕍. This renders the conditions imposed on a sensible signature to be satisfied, so that Definition 2.6 is really a generalization of the standard constructor-based notion of a sensible (or inhabited) manysorted signature to one with hidden sorts and destructors.

Furthermore, note that the signature of Example 2.3 is sensible.

Definition 2.7 (Substitutions) Let Σ = (𝕊, 𝕍, ℍ, 𝕂, ℂ , 𝔻, α, V, •, C, ≲) be a signature. Let X be a variable-system for 𝕊 and 𝕂. Let T = (T_{ς,s})_{(ς,s)∈{GEN,DAT}×𝕊} be any {GEN, DAT}×𝕊-sorted family of classes. With X → T we denote the {GEN, DAT}×𝕊-sorted (total) functions from X to T. If T is a family of terms, then X → T is a class of substitutions. E.g., if σ ∈ X → T (Σ, X) (or simply written σ : X → T (Σ, X)), then, for any X ∈ X_{GEN,s}, σ(X) is a term of sort s, and for any x ∈ X_{DAT,s}, σ(x) is a data term of sort s. For a substitution σ we denote with ‘Γ σ’ the result of replacing in Γ each occurrence of a variable x ∈ dom(σ) with σ(x).

6 July 23, 2008

3 Modeling Partial Functions with Total Structures

Traditionally, algebras or structures are total in the sense that they assign total functions to the function symbols of their signature.

Contrary to this, most working mathematicians would be very unhappy if they were not able to use partial functions. Similarly, some people working on algebraic specification are very fond of partial functions: The idea that a function symbol denotes a partial function results in so-called partial algebras, cf. the fascinating book of Reichel (1987), which, however, already makes clear that partial algebras are not as simple as total ones. Similarly, category theorists deal with co algebras, where partiality can easily be modeled because the co domain of a function symbol of a co signature is a sum into that 1 = {⊥} can nicely be included without the usual inconvenience of an extra sort for possibly erroneous values, cf. e.g. Jacobs & Rutten (1997), Padawitz (2000).

Again contrary to this, total algebras are preferred by computer scientists working on theorem proving and algebra in implementations that deal with a very big number of terms. This is because the soundness of these implementations requires that each occurring term object really is a term, and it is practically not possible to prove this again and again. Note that e.g. in a partial or co algebra containing the natural numbers nat and the predecessor function p : nat ⇝ nat or p : nat → nat + 1, resp., and a ground term t of sort nat, whether p(t) is defined and whether p(p(t)) is a term or not depends on the evaluation of t in the algebra and therefore is a semantical notion instead of a purely syntactical one.

Our solution to this dilemma is to model partial functions with total algebras, cf. Wirth & Gramlich (1994b). In this paper, we also include predicates besides (characteristic) functions because they play an essential role as destructors of co inductive data domains. For a predicate p : s_{0}, …, s_{n−1} (with s_{0}, …, s_{n−1} ∈ 𝕊 being sorts of the signature Σ) we, however, will write p : s_{0}, …, s_{n−1} ⇝ pred (with pred ∉ 𝕊) and include it into the set 𝕂 of constant (= non-variable) function and predicate symbols of the signature Σ, i.e. p ∈ 𝕂.

Consider a partial algebra D that satisfies pred^{D} = {TRUE} and assigns to each sort s ∈ 𝕊 and each constant f : s_{0}, …, s_{n−1} ⇝ s_{n} of its signature Σ a non-empty set say s^{D} and a (strict) (possibly) partial function f^{D} : s_{0}^{D}× ⋯ ×s_{n−1}^{D} ⇝ s_{n}^{D}, resp.. We model this partial algebra with a class K of (total) Σ-structures A of the following form: A assigns to each sort s ∈ 𝕊 and each constant f : s_{0}, …, s_{n−1} ⇝ s_{n} of Σ, resp., two non-empty sets say (DAT, s)^{A} and (GEN, s)^{A} with (DAT, s)^{A} = s^{D} and (DAT, s)^{A} ⊆ (GEN, s)^{A}, and in case of s_{n} ≠ pred a total function

f^{A} : (GEN, s_{0})^{A}× ⋯ ×(GEN, s_{n−1})^{A} → (GEN, s_{n})^{A}

with f^{D} ⊆ f^{A}, and in case of s_{n} = pred a relation

f^{A} ⊆ (GEN, s_{0})^{A}× ⋯ ×(GEN, s_{n−1})^{A}

with dom(f^{D}) ⊆ f^{A}. We call (GEN, s)^{A} the general universe of A for the sort s, whereas (DAT, s)^{A} is called the data universe of A for the sort s.

Let us define a variable-system for a set 𝕊 of sorts and a set 𝕂 of constants (= nonvariables) to be a {GEN, DAT}×𝕊-sorted family V = (V_{ς,s})_{(ς,s)∈{GEN,DAT}×𝕊} of sets V_{ς,s} that are mutually disjoint and disjoint from 𝕂. The variables from V_{DAT,s} and V_{GEN,s} are called the data and general variables of sort s, resp.. By abuse of notation we sometimes write V to denote ⋃_{(ς,s)∈{GEN,DAT}×𝕊} V_{ς,s}, &c.. For k being any of these kinds of variables and for a term, formula Γ &c., ‘V_{k}(Γ)’ denotes the set of variables from V_{k} occurring in Γ. The set T (Σ, V)_{GEN,s} of terms of sort s denotes the well-sorted first-order terms of fixed arity over 𝕂 and V of sort s ∈ 𝕊, where 𝕊 and 𝕂 are the set of sorts and the set of constants given by Σ, resp.. This means that, for s ∈ 𝕊, the T (Σ, V)_{GEN,s} are the smallest sets such that V_{GEN,s} ⊎ V_{DAT,s} ⊆ T (Σ, V)_{GEN,s} and if f : s_{0}, …, s_{n−1} ⇝ s_{n} (n ∈ N; s_{0}, …, s_{n} ∈ 𝕊) and, for each i ≺ n, t_{i} ∈ T (Σ, V)_{GEN,s_{i}} then f(t_{0}, …, t_{n−1}) ∈ T (Σ, V)_{GEN,s_{n}}. The set T (Σ, V)_{DAT,s} of data terms of sort s denotes the subclass of terms from T (Σ, X)_{GEN,s} that only contain variables from V_{DAT} and constants from a special set ℂ ⊆ 𝕂 of constructors that is given by the signature Σ. For such a constructor c ∈ ℂ with c : s_{0}, …, s_{n−1} → s_{n} we require s_{n} ≠ pred and any Σ-structure A must satisfy

∀i ≺ n. d_{i} ∈ (DAT, s_{i})^{A} ⇒ c^{A}(d_{0}, …, d_{n−1}) ∈ (DAT, s_{n})^{A}.

Let T = (T_{ς,s})_{(ς,s)∈{GEN,DAT}×𝕊} be any {GEN, DAT}×𝕊-sorted family of sets. With V → T we denote the ({GEN, DAT}×𝕊-sorted) (total) functions from V to T. On the one hand, if T is a family of sets of terms, then the elements of V → T are substitutions. E.g., if σ : V → T (Σ, V), then, for any X ∈ V_{GEN,s}, σ(X) is a term of sort s, and for any x ∈ V_{DAT,s}, σ(x) is a data term of sort s. For a substitution σ we denote with ‘Γ σ’ the result of replacing in Γ each occurrence of any variable x ∈ dom(σ) with σ(x). On the other hand, if T is a Σ-structure A, then we use A to denote ((ς, s)^{A})_{(ς,s)∈{GEN,DAT}×𝕊} and the elements of V → A are the (total) valuations from V to A.

For τ : V → A we denote with ‘A⊎τ’ the extension of A to the variables of V which are then treated as nullary constants. More precisely, we assume the existence of some evaluation function ‘eval’ such that eval(A⊎τ) maps any term over Σ⊎V into the universe of A (respecting kinds) such that for all x ∈ V: eval(A⊎τ)(x) = τ(x). Moreover, eval(A⊎τ) maps any formula B over Σ⊎V to TRUE or FALSE, such that B is valid in A⊎τ iff eval(A⊎τ)(B) = TRUE. We assume that the Substitution-Lemma (cf. e.g. Enderton (1973), p. 127, or Fitting (1996), p. 120) holds in the sense that, for any substitution σ, Σ-struc-ture A, valuation τ : V → A, and term or formula B over Σ⊎V:

eval(A⊎τ)(Bσ) = eval( A ⊎ ( σ ⊎ _{V\dom(σ)}↿id ) ∘ eval(A⊎τ) )( B ).

Note that we assume the operator ‘∘’ to have higher priority than the operators ‘∪’ and ‘⊎’.

Now, when the partial algebra D satisfies a first-order specification where all terms are defined and when we consider all variables occurring in this specification to be from V_{DAT}, then the specification is satisfied by each Σ-structure A in our above class K. Note that the variables from V_{GEN} are useful for specifying non-strict partial functions:

Example 3.1 Let true, false : bool be the constructors for the sort bool of Boolean values. Let or : bool, bool → bool be from 𝕂\ℂ. Let X : V_{GEN,bool} and x : V_{DAT,bool}. Let t be a ground term of sort bool that does not evaluate to the data universe of sort bool given by the values of true and false under the evaluation function. Now specifying or via or(x, false)=x and or(x, true)=true has the same syntactical and semantical effect as specifying it via or(true, true)=true, or(false, true)=true, or(true, false)=true, or(false, false)=false. Moreover, adding or(true, x)=true has no effect anymore. Contrariwise, or(X, false)=X, or(X, true)=true also specifies that or(t, true)=t and adding or(true, X)=true has the additional effect of implying or(true, t)=true. By the way, the readers familiar with rewriting systems may note that all these equations do not produce a single proper critical pair.

Continuing our modeling of partiality, we add a predicate Def_{s} : s ⇝ pred (index omitted when clear from context) for each sort s of Σ that is interpreted by any Σ-structure A as (DAT, s)^{A}. Now, if a ground term t over Σ is defined w.r.t. D, then Def t holds in each Σ-structure A of our above class K. The converse is also true, provided that K contains all possible Σ-structures of the above kind. To wit, include the Σ-structure given by (GEN, s)^{A} = (DAT, s)^{A} ⊎ {⊥} and the functions evaluating to ⊥ when undefined in D or when applied to ⊥. Considering this Σ-structure, the question arises what the possibility to choose (GEN, s)^{A} different from (DAT, s)^{A} ⊎{⊥} is good for. The simple answer is that, on one hand, we want to be able to model non-strict functions like or in Example 3.1 above and, on the other hand, we do not want silly theorems to hold, like \frac{0}{0}=p(0) (due to ⊥=⊥) that becomes invalid when we add p(0) = 0 to the specification of natural numbers.

Well-known equality notions like (in order of increasing logical strength) weak, strong, and existential equality of two terms t, t′ can now be expressed via t=t′ ⇐ (Def t ∧ Def t′), (t=t′ ∧ Def t ∧ Def t′) ∨ (¬Def t ∧ ¬Def t′), and t=t′ ∧ Def t ∧ Def t′, resp., but this is not our subject here.

Since, in our modeling, the notion of a term is a purely syntactical one and for reasons we will see later, this modeling of partial functions with total Σ-structures makes the computer scientists perfectly happy. People working on partial or co algebras in practice should also be interested in it. Finally, the working mathematicians are confident with our modeling because they are not really interested in the logical formalization of partial functions, at least as long as there is one and someone who could principally formalize the proofs containing partial functions.

4 Basic Notions for Σ-Structures

Definition 4.1 (Enrichment, Reduct) Let Σ be a signature with 𝕊, 𝕂, ℂ as sets of sorts, constants, and constructors, resp.. Σ′ is a an enrichment of Σ if Σ′ is a signature whose sets of sorts, constants, and constructors are a superclasses of the resp. sets of Σ and the arities of the common constants are identical in both signatures. When Σ′ is an enrichment of Σ and B is a Σ′-structure, then the Σ-reduct of B is the Σ-structure A given by (ς, s)^{A} = (ς, s)^{B} for all (ς, s) ∈ {GEN, DAT}×𝕊 and f^{A} = f^{B} for all f ∈ 𝕂. When Σ′′ is the sub-signature of Σ that contains only the constants from ℂ and A is a Σ-structure, then the data reduct of A is the standard total algebra D for Σ′′ given by s^{D} = (DAT, s)^{A} for all s ∈ 𝕊 and c^{D} = c^{A} for all c ∈ ℂ.

Note that the following definition differs from the standard one.

Definition 4.2 (Σ-Homomorphism) Let Σ be a signature, with 𝕊 and 𝕂 as sets of sorts and constants, resp.. A Σ-homomorphism from A to B is a triple written h::A→B of two Σ-structures A and B whose data reducts are equal (!!!) and an 𝕊-sorted family h = (h_{s})_{s∈𝕊} of functions h_{s} : (GEN, s)^{A} → (GEN, s)^{B} that is compatible with Σ in the following sense: For f∈ 𝕂 with f : s_{0}, …, s_{n−1} ⇝ s_{n} and for a_{0} ∈ (GEN, s_{0})^{A}, …, a_{n−1} ∈ (GEN, s_{n−1})^{A} in case of s_{n} ≠ pred we have h_{s_{n}}(f^{A}(a_{0}, …, a_{n−1})) = f^{B}(h_{s_{0}}(a_{0}), …, h_{s_{n−1}}(a_{n−1})), and in case of s_{n} = pred we have (a_{0}, …, a_{n−1}) ∈ f^{A} ⇒ (h_{s_{0}}(a_{0}), …, h_{s_{n−1}}(a_{n−1})) ∈ f^{B}, and for all s ∈ 𝕊 and d ∈ (DAT, s)^{A} we have h_{s}(d) = d.

Definition 4.3 (Initial, Free) Let X be a variable-system for 𝕊 and 𝕂 of the signature Σ. Let A be a Σ-structure and K a class of Σ-structures. A is initial in K if A is in K and, for each B in K, there is a unique Σ-homomorphism h::A→B. A is free in K over X if there is some ι : X → A such that A is free in K over X w.r.t. ι. A is free in K over X w.r.t. ι if A is in K and A is free for K over X w.r.t. ι. A is free for K over X w.r.t. ι if for each B in K and τ : X → B there is a unique Σ-homomorphism h::A→B with τ_{ς,s} = ι_{ς,s}∘h_{s} for each (ς, s) ∈ {GEN, DAT}×𝕊.

5 Four Notions of Validity

Please! Never again write a paper with seven notions of validity! — Deepak Kapur, 1996

[figure: no confusion & no junk; no confusion & and no junk for DAT,; for DAT; no confusion for GEN, and A = GT /⟷^{∗}_{R,∅}; and (GEN, s)^{A} = (DAT, s)^{A}; no confusion & no junk for DAT,; A; B′; B; C; D; D′; E; no confusion; for DAT; no junk for DAT,; no confusion &; A = T (V_{GEN})/⟷^{∗}_{R,V_{GEN}}; no confusion for GEN, and; no junk; for DAT]

In Wirth & Gramlich (1994b) and still in Wirth (1997), we had seven notions of (inductive) validity. After application and consideration for years, we would now say that one or two (type C and maybe type D) are really useful, two more are important because they are still common (type E, D′), and the remaining three (type A, B, and B′) are only interesting for the history of inductive validity and will not be treated in this paper, although they were once used by other authors as in Kounalis & Rusinowitch (1990) and Bouhoula &al. (1992). The names of the types were chosen such that, roughly speaking, if T precedes T′ in the alphabet, then type-T validity of a formula implies type-T′ validity of it.

Specifications should express only what is important for the specifier. A proper semantics for such partial specifications must be based on

a class of different models instead of a single one.

A free or initial model can serve for a minimal implementation but is not adequate for defining the semantics of partial specifications.

— Robert Bookhade, 1999

Definition 5.1 (Specification, Validity) Let Σ be a signature with 𝕊 and 𝕂 as sets of sorts and constants, resp.. Let D be the data reduct of some Σ-structure. Let R be a set of formulas over Σ. We will call (Σ, D, R) a specification. Let A be a Σ-structure such that R is valid in A. Now, A is a model of (Σ, D, R) of type

C if the data reduct of A is D.

D if for some variable-system X for 𝕊, 𝕂 with ∀s ∈ 𝕊. X_{DAT,s} = ∅, A is free in the class of models of (Σ, D, R) of type C over X.

E if A is initial in the class of models of (Σ, D, R) of type C.

D′ if A is a model of (Σ, D, R) of type C, and (DAT, s)^{A} = (GEN, s)^{A} for each s ∈ 𝕊; i.e. the general universes coincide with the data universes.

Finally, for T being any of the above types, a formula is type-T valid w.r.t. (Σ, D, R) if it is valid in all models of (Σ, D, R) of type T.

Corollary 5.2 If a formula is type-C valid w.r.t. (Σ, D, R), then it is also type-D, type-E, and type-D′ valid w.r.t. (Σ, D, R).

Definition 5.3 (Extension) (Σ′, D′, R′) is an extension of of the specification (Σ, D, R) if (Σ′, D′, R′) is a specification such that Σ′ is a an enrichment of Σ, s^{D′} = s^{D} and c^{D′} = c^{D} for all s ∈ 𝕊 and c ∈ ℂ where 𝕊 and ℂ are the sets of sorts and constructor symbols of Σ, resp., and R⊆R′. Such an extension is called type-T consistent if the Σ-reduct of any model of (Σ′, D′, R′) of type-T is a model of (Σ, D, R) of type-T.

Note that consistent extensions (where the reducts of new models must be old ones) are somehow the converse of the well-known conservative extensions, where old models must be extensible to new models.

6 Data Universes

In this section we discuss two ways of establishing the data universes of the common data reduct D of the Σ-structures of our classes of models. In order to do this, we first add some more slots to our signature objects. We assume that each signature Σ contains a wellfounded quasi-ordering ≲ on 𝕊 ⊎ {pred} with pred as strict minimum (i.e. ∀s ∈ 𝕊. pred<s, where < := ≲\≳ is the (strict) ordering of ≲), and two disjoint sets 𝕍 and ℍ of visible and hidden sorts, resp., that partition the set of sorts 𝕊, i.e. 𝕊 = 𝕍⊎ℍ. The set ℍ of hidden sorts again partitions into the sets ℍ_{≠} and ℍ_{pred} because we cannot use both inequality and predicates for defining a hidden sort, cf. § 6.2.

Moreover, we require that the equivalence classes of the quasi-ordering ≲ (i.e. those of the equivalence ∼ := ≲ ∩ ≳) are subclasses of 𝕍, ℍ_{≠}, ℍ_{pred}, or {pred}. Now, the data universes of such an equivalence class of sorts are built up in parallel, assuming that the data universes for all sorts strictly smaller in the ordering < have already been established. The manner in that this is done depends on whether the equivalence class is a subclass of 𝕍 or of ℍ, as discussed in the following two subsections. While visible sorts are standard, hidden sorts are still not generally understood.

6.1 Visible Sorts and Constructors

For any constructor c ∈ ℂ with say c : s_{0}, …, s_{n−1} → s_{n} (n ∈ N) we require that s_{n} ∈ 𝕍 and ∀i ≺ n. s_{i}≲s_{n}, and call c a constructor for s_{n}. Let V be the equivalence class of s_{n} w.r.t. ∼. For any d_{i} ∈ s_{i}^{D} (i ≺ n), the term c(d_{0}, …, d_{n−1}) becomes an element in s_{n}^{D}. While the s_{i}^{D} with s_{i} < s_{n} are assumed to be already given, all v^{D} with v ∈ V are being defined as the smallest sets closed under the above term construction with all constructors for v. Moreover, in order to avoid empty data universes, we require that, for each v ∈ V, there is a term of sort v that only consists of constructors for the sorts in V and variables of sorts say s′ with s′<s_{n}. Finally, in the above context, we define c^{D}(d_{0}, …, d_{n−1}) := c(d_{0}, …, d_{n−1}), which immediately gives us the required c^{D}(d_{0}, …, d_{n−1}) ∈ s_{n}^{D}.

Example 6.1 The and/or and or/and trees over bool can be realized with the visible sorts and and or, resp., when we set bool < or ∼ and and take as constructors

[ ]_{bool}^{or} : bool → or, [ ]_{and}^{or} : and → or, cons_{or} : and, or → or,
[ ]_{bool}^{and} : bool → and, [ ]_{or}^{and} : or → and, cons_{and} : or, and → and.

An and/or tree like ∧(a, ∨(b, c, ∧(d, ∨(e)), f)) is then represented as the term

cons_{and}([a]_{bool}^{or}, [cons_{or}([b]_{bool}^{and}, cons_{or}([c]_{bool}^{and}, cons_{or}(cons_{and}([d]_{bool}^{or}, [[e]_{bool}^{or}]_{or}^{and}), [f]_{bool}^{or})))]_{or}^{and}).

While the presentation of this term to human beings cries for some syntactic sugaring, the term can well serve as an implementation and has the advantage that all children of the root of an and/or-tree are guaranteed to be or/and-trees, provided that the term is well-sorted.

Note that, theoretically, any data universe can be established with a visible sort simply by introducing a nullary constructor symbol for exactly each element of the intended data universe.

Summing up, the data universes for visible sorts are built up the following way:

No Junk

One starts with the empty set and keeps adding terms that apply a constructor. This process will come to an end at level ω. Another way to say this is that the data universes are the least fixpoints of the finitary and monotonic functor that returns the set of terms that apply a constructor to its argument set. The buzzword “no junk” emphasizes that the data universes contain nothing but what is generated by the constructors as useful data.

No Confusion

All elements that have a different construction process are considered to be different. The buzzword “no confusion” actually only means that there is as little equality between the elements as possible or, stated differently, that the universe can be homomorphically mapped to any other universe that satisfies some required axioms. E.g., when we used lists to represent finite sets, we would need the axioms of associativity, commutativity, and idempotence. In former papers we used to allow such axioms in the form of positive conditional constructor equations. Since these constructor equations produced a lot of trouble regarding consistency and theorem proving we did not include them in the implementation of the tactic-based inductive theorem prover QuodLibet, cf. Kühler (2000), and by now we also do not want to have them in our theoretical considerations anymore because we can have sets as a hidden sort and the finite sets are simply those where the function card : set ⇝ nat is defined.

In Wirth & Gramlich (1994b) we even had types of validity where junk or confusion could occur in the data universes for visible sorts. Today we do not consider this to be appropriate anymore.

6.2 Hidden Sorts and Destructors

Definition 6.2 (Condition Literal) Let Σ be a signature, X be a variable-system for 𝕊,𝕂, and s ∈ 𝕊⊎{pred}. A condition literal over Σ,X of sort s has one of the four forms

Def_{s}u where u ∈ T (Σ, X)_{GEN,s} and s ∈ 𝕊.

This literal is not conjugatible and its terms are the single term u. u_{0}=_{s}u_{1} where u_{0}, u_{1} ∈ T (Σ, X)_{GEN,s} and s ∈ 𝕊.

This literal is conjugatible to its conjugate u_{0}≠_{s}u_{1} if s ∈ 𝕍⊎ℍ_{≠}. Its terms are u_{0}, u_{1}.

u_{0}≠_{s}u_{1} where u_{0}, u_{1} ∈ T (Σ, X)_{GEN,s} and s ∈ 𝕍⊎ℍ_{≠}.

This literal is conjugatible to its conjugate u_{0}=_{s}u_{1}. Its terms are u_{0}, u_{1}. p(u_{0}, …, u_{n−1})

with s = pred, p ∈ 𝕂 with p : s′_{0}, …, s′_{n−1} ⇝ pred, and ∀i ≺ n. u_{i} ∈ T (Σ, X)_{GEN,s′_{i}}. This literal is not conjugatible and its terms are u_{0}, …, u_{n−1}.

The sort indices are omitted when clear from the context. The conjugate of a conjugatible condition literal is denoted by \overline{L}.

Let H ⊆ ℍ be the equivalence class of hidden sorts whose data universes we want to establish and O the set of sorts from 𝕊 whose data universes we assume to be already established because they are smaller than the sorts in H w.r.t. <.

We first add some more slots to our signature objects. We assume that each signature Σ contains a set 𝔻 ⊆ 𝕂\ℂ of destructors, a function • with dom(•) = ℍ and •_{h} ∈ V_{GEN,h} for all h ∈ ℍ, and a set ℙ of destructor patterns.

Definition 6.3 (Destructor Pattern) Each destructor pattern from ℙ has the form d(x_{0}, …, x_{n}) ⟵ L_{0}, …, L_{m−1} where n, m ∈ N (for m = 0 we omit the ‘⟵’); d ∈ 𝔻 is a destructor with d : s_{0}, …, s_{n} ⇝ s_{n+1}; x_{0}, …, x_{n} ∈ V_{DAT} are mutually different data variables; and there is an i ⪯ n with ran(•) ∩ {x_{0}, …, x_{n}} = {•_{s_{i}}}, s_{n+1} = pred ⇒ s_{i} ∈ ℍ_{pred}, and ∀k ⪯ n+1. s_{k}≲s_{i}, and for each j ≺ m, L_{j} is a conjugatible condition literal over the constructors and destructors for sorts from O⊎H and over x_{0}, …, x_{n} and of a sort from O⊎{pred}. In this case, we speak of a destructor pattern for s_{i} and of sort s_{n+1}, denote the set of these patterns with ℙ_{s_{i}}^{s_{n+1}}, and call d a destructor for s_{i} and of sort s_{n+1}.

While a destructor pattern can be for only one sort, a destructor can be for different sorts (in different patterns), but we require that these sorts are congruent w.r.t. ∼.

Note that the wellfounded quasi-ordering ≲ guarantees that visible sorts are not constructed from hidden sorts whose behavior they define, which would be a vicious circle. Thus, the result sort of a constructor must be visible and its argument sorts must be smaller, whereas the hidden argument sorts of a destructor must be somehow bigger than its result sort, the sorts of its arguments, and the sorts of the condition literals of its destructor patterns. Note that in the absence of hidden sorts we can choose ≲ to be 𝕍×𝕍. This renders the conditions imposed on a signature to be satisfied, so that our signatures really are a generalization of the standard constructor-based notion of a sensible (or inhabited) many-sorted signature to one with hidden sorts and destructors.

Assume that D assigns to each sort in O and its constructors the already established universes and total functions. Moreover, assume that D assigns to any destructor for hidden sorts in O already established partial functions. The step we have to perform is to let D assign a data universe to each sort in H and a partial function to each destructor for a sort in H. Suppose we have a candidate D for such an assignment.

Firstly, we need three requirements for D. The first is needed soon, the other two must be formulated later.

Requirement 6.4 (Definedness) For each destructor pattern ( d(x_{0}, …, x_{n}) ⟵ L_{0}, …, L_{m−1} ) ∈ ℙ_{h}^{s} (h ∈ H) we require that for each valuation τ : {x_{0}, …, x_{n}} → D,

• for each j ≺ m the terms of L_{j} are defined w.r.t. D⊎τ if the literals L_{0}, …, L_{j−1} are true w.r.t. D⊎τ and

• d(x_{0}, …, x_{n}) is defined w.r.t. D⊎τ if the literals L_{0}, …, L_{m−1} are true w.r.t. D⊎τ and s ≠ pred.

Secondly, we define the following:

Definition 6.5 (Bisimulation) A ℙ-bisimulation for D is an O⊎H-sorted family ≈ = (≈_{s})_{s∈O⊎H} of binary relations ≈_{s} on s^{D} that has the following properties:

1. For o ∈ O we have a ≈_{o} a′ iff a = a′ ∈ o^{D}.

2. For h ∈ H, if a ≈_{h} a′ and ( t ⟵ L_{0}, …, L_{m−1} ) ∈ ℙ_{h}^{s}, for Y := V(t)\{•_{h}} and ∀y ∈ Y. y ∈ V_{DAT,s′_{y}},

if s ≠ pred, then

• for any π : Y → D such that all literals in L_{0}, …, L_{m−1} are true w.r.t. D ⊎ {•_{h}↦a} ⊎ π there is a π′ : Y → D with ∀y ∈ Y. π(y) ≈_{s′_{y}} π′(y) such that all literals in L_{0}, …, L_{m−1} are true w.r.t. D ⊎ {•_{h}↦a′} ⊎ π′ and eval(D⊎{•_{h}↦a}⊎π)(t) ≈_{s} eval(D⊎{•_{h}↦a′}⊎π′)(t), and

• for any π′ : Y → D such that all literals in L_{0}, …, L_{m−1} are true w.r.t. D ⊎ {•_{h}↦a′} ⊎ π′ there is a π : Y → D with ∀y ∈ Y. π(y) ≈_{s′_{y}} π′(y) such that all literals in L_{0}, …, L_{m−1} are true w.r.t. D ⊎ {•_{h}↦a} ⊎ π and eval(D⊎{•_{h}↦a}⊎π)(t) ≈_{s} eval(D⊎{•_{h}↦a′}⊎π′)(t), and

if s = pred, then

• for any π : Y → D such that all literals in L_{0}, …, L_{m−1}, t are true w.r.t. D ⊎ {•_{h}↦a} ⊎ π there is a π′ : Y → D with ∀y ∈ Y. π(y) ≈_{s′_{y}} π′(y) such that all literals in L_{0}, …, L_{m−1}, t are true w.r.t. D ⊎ {•_{h}↦a′} ⊎ π′, and

• for any π′ : Y → D such that all literals in L_{0}, …, L_{m−1}, t are true w.r.t. D ⊎ {•_{h}↦a′} ⊎ π′ there is a π : Y → D with ∀y ∈ Y. π(y) ≈_{s′_{y}} π′(y) such that all literals in L_{0}, …, L_{m−1}, t are true w.r.t. D ⊎ {•_{h}↦a} ⊎ π.

Definition 6.6 (Experiment) Let Σ be a signature. For h ∈ ℍ and s ∈ 𝕍 ⊎ {pred} the sets 𝔼_{h}^{s} of experiments over Σ for h of sort s are inductively defined as follows:

1. ℙ_{h}^{s} ⊆ 𝔼_{h}^{s}.

2. If, for h′ ∈ ℍ,

( e ⟵ L_{0}, …, L_{m−1} ) ∈ 𝔼_{h′}^{s},

( e′ ⟵ L′_{0}, …, L′_{m′−1} ) ∈ ℙ_{h}^{h′},

σ : V(e) → T (Σ, V) satisfies σ(•_{h′}) = e′ and renames V(e) \ {•_{h′}} away from V(e′) and ran(•) (i.e. _{V(e)\{•_{h′}}}↿σ : (V(e)\{•_{h′}}) → (V\V(e′)\ran(•)) is injective), then

( eσ ⟵ L′_{0}, …, L′_{m′−1}, L_{0}σ, …, L_{m−1}σ ) ∈ 𝔼_{h}^{s}.

Note that for any experiment e ⟵ L_{0}, …, L_{m−1} for h of sort s the following holds: s = pred ⇒ h ∈ ℍ_{pred}, the term e is linear, V(L_{0}, …, L_{m−1}) ⊆ V(e), and there is a unique path from the root of e to the variable •_{h}. On this path, all proper subterms are hidden and all symbols are destructors, whereas all symbols not on this path are variables. Furthermore, s<h and l_{j}<h for the sorts l_{j} of L_{j}.

Now, an 𝔼-bisimulation can be defined just like a ℙ-bisimulation in Definition 6.5 and the following corollary holds for ℙ- as well as for 𝔼-bisimulations.

Corollary 6.7 Let D satisfy Requirement 6.4. Now:

1. (_{s^{D}}↿id)_{s∈O⊎H} is a bisimulation for D.

2. If (A_{s})_{s∈O⊎H} and (B_{s})_{s∈O⊎H} are bisimulations for D, then (A_{s}^{−1})_{s∈O⊎H} and (A_{s}∘B_{s})_{s∈O⊎H} are bisimulations for D, too.

3. A non-empty union over bisimulations for D is a bisimulation for D.

4. There is a maximum bisimulation for D, which is given as the union over all bisimulations for D and which is a D-equivalence.

Corollary 6.8 If D satisfies Requirement 6.4, then every ℙ-bisimulation is an 𝔼-bisimulation.

As the maximum 𝔼-bisimulation can easily be shown to satisfy the contrapositive of condition (2) of the definition of a ℙ-bisimulation, we get:

Corollary 6.9 If D satisfies Requirement 6.4, then the maximum 𝔼-bisimulation for D is the maximum ℙ-bisimulation for D and will be denoted with ≈_{D}.

The second requirement on D is the opposite of “no confusion”:

Requirement 6.10 (Extensionality) For any two elements a, a′ ∈ h^{D} of a data universe for a sort h ∈ H, if a≈_{D,h} a′ then a = a′.

The third requirement on D is quite the opposite of “no junk”:

Requirement 6.11 (Maximality) If we extend the data universes for H and the partial functions for the destructors for H, yielding a new structure D′ for that Requirement 6.4 is satisfied, then for each new element a ∈ h^{D′}\h^{D} of a data universe for h ∈ H, we have a ≈_{D′,h} a′ for some old element a′ ∈ h^{D}.

Now it is time to see some examples.

Example 6.12 (Infinite Streams) The infinite streams over some sort s can be established as follows. Let infstream ∈ ℍ with s < infstream and hd, tl ∈ 𝔻 with hd : infstream ⇝ s and tl : infstream ⇝ infstream. Set ℙ := {hd(•_{infstream}), tl(•_{infstream})}. We get 𝔼 = { hd(tl^{k}(•_{infstream})) | k ∈ N }. The above definedness requirement says that hd^{D} and tl^{D} must be total on infstream^{D}. The condition (2) of Definition 6.5 says (due to Y = ∅) that a ≈_{D,infstream} a′ implies hd^{D}(a) = hd^{D}(a′) and tl^{D}(a) ≈_{D,infstream} tl^{D}(a′).

Thus, the above extensionality requirement says that the data universe for infstream can be viewed as a subset of 𝔼 → s^{D} (with simple changes for more general experiments (cf. Example 6.17), this is always the case if the experiments are unconditional and do not include variables of sorts from H besides ran(•)) or as a subset of N → s^{D}. Indeed, the infinite streams are isomorphic to this set of functions. Finally, the maximality requirement says that we need all functions from N → s^{D} in the data universe for infstream, or at least those we can talk about. By this we mean that we only need those streams that can be comprehended with our language, logic, and (co) recursive definition mechanism. Such a “Henkin” or “general” model can usually be guaranteed to exist, to be countable, and to have the same theory as the standard model (here: of all streams) by a proof similar to the completeness proof for Q_{0} in Andrews (1986). While countable data universes may be preferred for philosophical reasons, for infinite streams there seems to be no real need to deviate from the standard model. This will be different in Example 6.16 below. The co algebraic view on infinite streams is the destructor

(hd, tl) : infstream → s × infstream

and the set of infinite streams is the greatest fixpoint of the monotonic functor F (X) = s^{D}×X in the non-wellfounded set theory of Aczel (1988).

Example 6.13 (Streams) The (finite and infinite) streams over some sort s can be established as follows. Let stream ∈ ℍ with s < stream and null, hd, tl ∈ 𝔻 with null : stream ⇝ bool, hd : stream ⇝ s, and tl : stream ⇝ stream. Set

ℙ := \{ \begin{matrix}null(•_{stream}); \\ hd(•_{stream}) & ⟵ & null(•_{stream})=false; \\ tl(•_{stream}) & ⟵ & null(•_{stream})=false \end{matrix} \} .

We get 𝔼 :=

\left\{{null(tl^{k}(•_{stream})) ⟵ null(tl^{0}(•_{stream}))=false, …, null(tl^{k−1}(•_{stream}))=false; \atop hd(tl^{k}(•_{stream})) ⟵ null(tl^{0}(•_{stream}))=false, …, null(tl^{k}(•_{stream}))=false k ∈ N}\right\} .

The above definedness requirement says that null^{D} must be total on stream^{D} and that hd^{D} and tl^{D} must be defined on any non-null stream. The condition (2) of Definition 6.5 says that a ≈_{D,stream} a′ implies null^{D}(a) = null^{D}(a′) and if null^{D}(a) = false^{D} then hd^{D}(a) = hd^{D}(a′) and tl^{D}(a) ≈_{D,stream} tl^{D}(a′). Thus, the above extensionality requirement says that the data universe for stream can be viewed as a subset of ⋃_{α⪯ω} (α → s^{D}). Indeed, the streams are isomorphic to this set of functions. Finally, the maximality requirement says that we need all functions from this set in the data universe for stream, or at least those we can talk about. The co algebraic view on infinite streams is the destructor

(hd, tl) : stream → s × (stream + 1)

and the set of streams minus the empty stream is the greatest fixpoint of the monotonic functor F (X) = s^{D} × (X ⊎ 1) in the non-wellfounded set theory of Aczel (1988).

Example 6.14 (Characteristic Functions) The characteristic functions over some sort s can be established as follows. Let chara ∈ ℍ with s < chara and in ∈ 𝔻 with in : s, chara ⇝ bool. Set ℙ := {in(e, •_{chara})}. We get 𝔼 = ℙ. The above definedness requirement says that in^{D} must be total on s^{D}×chara^{D}. The condition (2) of Definition 6.5 says that a ≈_{D,chara} a′ implies in^{D}(e, a) = in^{D}(e, a′) for any e ∈ s^{D}. Thus, the above extensionality requirement says that the data universe for chara can be viewed as a subset of s^{D} → bool^{D}. Indeed, the characteristic functions are isomorphic to this set of functions. Finally, the maximality requirement says that we need all functions from this set in the data universe for chara, or at least those we can talk about. The co algebraic view on characteristic functions is the destructor in : chara → s → 2 and the set of characteristic functions is the greatest fixpoint of the monotonic functor F (X) = s^{D} → bool^{D}.

Example 6.15 (Sets) Some people would say that the characteristic functions of Example 6.14 are isomorphic to predicates or sets. Other people, however, use to think predicates as μ-predicates, i.e. sets where only positive information is given and the intended meaning is the smallest consistent set. This will be important for the labeled transition systems in the example below. We will call these μ-predicates simply “sets” in the current example. The sets over some sort s can be established as follows. Let set ∈ ℍ_{pred} with s < set and in ∈ 𝔻 with in : s, set ⇝ pred. Set ℙ := {in(e, •_{set})}. We get 𝔼 = ℙ. Note that we cannot put set into ℍ_{≠} because we have a pattern of the sort pred. Thus, we have to put it into ℍ_{pred} instead, which means that there are no inequality condition literals for the sort pred. The above definedness requirement does not say anything about the definedness of in^{D}. Definedness of predicates is no reasonable notion anyway. The condition (2) of Definition 6.5 says that a ≈_{D,set} a′ implies, for any e ∈ s^{D}, that in^{D}(e, a) iff in^{D}(e, a′). Thus, the above extensionality requirement says that the data universe for set can be viewed as a subset of 𝔓(s^{D}) or as a subset of s^{D} ⇝ {true^{D}}. Indeed, the sets over s^{D} are isomorphic to any of these sets. Moreover, they are even isomorphic to s^{D} → bool^{D} (i.e. s^{D} → {true^{D}, false^{D}}) of Example 6.14, which seems to justify the view that characteristic functions and sets are isomorphic. The last isomorphism, however, depends on two premises that both will not be satisfied in Example 6.16, namely that s^{D} is a set (i.e. not a proper class) and that s < set. Finally, the maximality requirement says that we need all elements from one of these sets in the data universe for set, or at least those we can talk about. The co algebraic view on sets is the destructor in : set → 𝔓(s) and the set of sets over s^{D} is the greatest fixpoint of the monotonic functor F (X) = 𝔓(s^{D}) .

Example 6.16 (Labeled Transition Systems)

The labeled transition systems over bool as alphabet can be established as follows. Let lts, set ∈ ℍ_{pred} with bool < lts ∼ set and next, in ∈ 𝔻 with next : lts, bool ⇝ set and in : lts, set ⇝ pred. Set ℙ := {next(•_{lts}, b), in(a, •_{set})}, where the former returns the set of all successor states labeled with b and the latter tests whether a is in the set. We get 𝔼 = {in(a, next(•_{lts}, b)), in(a, •_{set})}. The above definedness requirement says that next^{D} must be total on lts^{D}. The condition (2) of Definition 6.5 says that a ≈_{D,lts} a′ implies next^{D}(a, b) ≈_{D,set} next^{D}(a′, b) for all b ∈ bool^{D}. It also says that s ≈_{D,set} s′ implies that for any a ∈ lts^{D} with in^{D}(a, s) there is an a′ ∈ lts^{D} with a ≈_{lts} a′ and in^{D}(a′, s′).

The co algebraic view on infinite streams is the destructor next : lts → bool → 𝔓(lts) and the proper class of labeled transition systems is the greatest fixpoint of the monotonic functor F (X) = bool^{D} → 𝔓(X) in the non-wellfounded set theory of Aczel (1988). We, however, have two problems with this fixpoint: The first problem is that it is a proper class. This means we cannot work properly with it in set theory. E.g., every total function defined on it is a proper class, too, and thus any class of such functions is empty. The second problem is that for new nullary function symbols say a : lts and all : set defined by next(a, b) = all and in(a, all) we have the problem that a^{D} is not bisimular to any element of that fixpoint, simply because all^{D} functions as a proper class and therefore cannot be an element of that fixpoint. This means that that fixpoint does not satisfy our above maximality requirement. Thus, we need another fixpoint (1) in another set theory or (2) for another functor.

1. In order to be consistent, a set theory has to put some restrictions on set formation in order to avoid sets like the famous class named after Bertrand Russell, which is similar to the one below. The ingenious solution to this problem found by John von Neumann and others had been sufficient for half a century but then turned out to be not too well-suited for some tasks like ours here. While the non-wellfounded set theory of Aczel (1988) is simply an improvement of the standard one (i.e. it is just as consistent but has more sets), other set theories might deprive us of certain sets by restricting the axioms of comprehension, power-set, union, separation, subset, &c., but give us new sets that may be important for our work. The only results on new set theories I know are Forti &al. (1996) and others of the same authors who do not seem to have any interest in the practical usefulness of their theories or in explaining them to anybody interested in their practical application. It should be clear that we cannot settle these very sophisticated problems here.

2. The clearer solution is to choose a different functor. E.g., in this example, we could

use the functor

F (X) = { f : bool^{D} → 𝔓(X) | f is “definable” with the elements of X }, which is finitary and monotonic and thus will have a least fixpoint at level ω, which is countable and therefore a set. While this is not the place to define “definable”, the reader should also cf. the discussion on “Henkin” or “general” models in Example 6.12.

Note that in general it may be well the case that no such fixpoint exists in any set theory. To see this, suppose that the signature of in would be in : lts, set ⇝ bool. Now, consider next(r, b) = Russell and in(a, Russell) = true ⟵ in(a, next(a, true)) = false. This implies in(r, next(r, true)) = true ⟵ in(r, next(r, true)) = false. Since the destructor pattern for in would require totality of in^{D}, this would lead to a contradiction. Thus, in this case, there would be no data universe that satisfies our definedness and maximality requirements, unless we excluded the above definition of r from the admissible ones, which renders r “undefinable”. But of course, this destructor pattern would have completely different effects: Consider

a_{true}  _{true}  c_{true} b _{false}  d _{false}

which can be specified via in(b, next(a, true)) in(a, next(b, false)) in(d, next(a, true)) in(d, next(c, true)) in(c, next(d, false))

and renders a ≈_{D,lts} c and b ≈_{D,lts} d. For the alternative signature of in : lts, set ⇝ bool, however, the above specification would not be sufficient because in would have to be total, and we would need something like:

in(a, next(a, b))=and(or(eq(a, b), eq(a, d)), eq(b, true))
in(a, next(b, b))=and(eq(a, a), eq(b, false))
in(a, next(c, b))=and(eq(a, d), eq(b, true))
in(a, next(d, b))=and(eq(a, c), eq(b, false))

But then the maximum bisimulation would be the identity because in case of a ≈_{D,lts} c, due to in(b, next(c, true)) = false there must be some a ≈_{D,lts} b with in(a, next(a, true)) = false, but the only possible solutions a = a and a = c are contradictory.

Example 6.17 (Total Functions) The simple function spaces of simply typed higher-order logic can be established stepwise in the following fashion. For α, β ∈ 𝕊, in order to get the total functions from α to β, let (α → β) ∈ ℍ with α, β < (α → β) and app ∈ 𝔻 with app : (α → β), α ⇝ β. Set ℙ := {app(•_{(α→β)}, a)}. We get 𝔼 = ℙ. The above definedness requirement says that app^{D} and must be total on (α → β)^{D} × α^{D}. The condition (2) of Definition 6.5 says (due to Y = ∅) that f ≈_{D,(α→β)} f′ implies app^{D}(f, a) = app^{D}(f′, a) for any a ∈ α^{D}. Moreover, the extensional equality of higherorder logic is—mutatis mutandis—exactly our ≈_{D,(α→β)}. Now, the above extensionality requirement says that the data universe for (α → β) can be viewed as a subset of { app(•_{(α→β)}, a) | a ∈ α^{D} } → β^{D} or as a subset of α^{D} → β^{D}. Indeed, the total functions from α to β are isomorphic to these sets of functions. Finally, the maximality requirement says that we need all functions from α^{D} → β^{D} in the data universe for (α → β), or at least those we can talk about. The co algebraic view on infinite streams is the destructor

app : (α → β) → α → β

and the set of total functions is the greatest fixpoint of the monotonic functor F (X) = α^{D} → β^{D}.

Our pragmatic solution to the problems with the establishment of hidden sorts is simply to assume that for the destructor patterns and the admissible definitions we want to have there is a set satisfying our three requirements of definedness, extensionality, and maximality from above, and that there is a way to choose one of them as the intended one. In case that this choice should—contrary to our assumptions—turn out to be crucial for our notions of validity, then we have to add more requirements, and finally, when the field has become more common and better understood, we will have to solve the problem of whether and what data universes exist for given destructor patterns and given admissibility of definitions by some general means.

7 Fulfilledness and Rewriting

Note that the following definition is recursive on the sort of condition literals in the wellfounded ordering < introduced at the beginning of § 6.

Definition 7.1 (Fulfilledness) Let Σ be a signature with 𝕊, 𝕍, ℍ, 𝕂, ℂ as sets of sorts, visible sorts, hidden sorts, constant symbols, constructors, resp.. Let D be the data reduct of some Σ-algebra. Let X be a variable-system for 𝕊, 𝕂 with ∀s ∈ 𝕊. X_{DAT,s} = ∅. Let Σ′ denote the signature that differs from Σ insofar as that the sets 𝕂 and ℂ of constants and constructors are extended to the sets 𝕂′ and ℂ′ with a new nullary constant symbol d : → h for any hidden sort h ∈ ℍ and any d ∈ h^{D}. Note that the signature Σ′ violates the rules of § 6 because it has constructors for hidden sorts. Let ⟶ be a sort-invariant relation on T (Σ′, X) and H be a set of condition literals of sort pred over Σ′, X. A list of condition literals over Σ′, X is said to be fulfilled w.r.t. ⟶, H if each of its literals is. A condition literal over Σ′, X is said to be fulfilled w.r.t. ⟶, H if for all s ∈ 𝕊 and u, u′ ∈ T (Σ′, X)_{GEN,s} if it has the form

Def u:

If s ∈ 𝕍: There is a term t whose function symbols are constructors from ℂ′ and whose variables are of hidden sort, and a substitution σ : V(t) → T (Σ′, X) such that u⟶^{∗}tσ and Def(xσ) is fulfilled w.r.t. ⟶, H for each x ∈ V(t).

If s ∈ ℍ: For any v ∈ 𝕍, any experiment ( e ⟵ L_{0}, …, L_{m−1} ) ∈ 𝔼_{s}^{v} over Σ, V where w_{j}, w′_{j} are the terms of L_{j}, and any σ : V(e) → T (Σ′, X) with σ(•_{s}) = u and ∀x ∈ V(e)\{•_{s}}. σ(x) ∈ GT (Σ′)_{DAT}, there either is some i ≺ m such that ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{i−1}, Def w′_{i−1}, L_{i−1}, Def w_{i}, Def w′_{i}, \overline{L_{i}} )σ is fulfilled w.r.t. ⟶, H or otherwise ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{m−1}, Def w′_{m−1}, L_{m−1} )σ is fulfilled w.r.t. ⟶, H and, unless v = pred, Def(eσ) is fulfilled w.r.t. ⟶, H.

u=u′:

If s ∈ 𝕍: There is a term t whose function symbols are constructors from ℂ′ and whose variables are of hidden sort, and two substitutions σ, σ′ : V(t) → T (Σ′, X) such that u⟶^{∗}tσ, u′⟶^{∗}tσ′, and xσ=xσ′ is fulfilled w.r.t. ⟶, H for each x ∈ V(t).

If s ∈ ℍ: For any v ∈ 𝕍, any experiment ( e ⟵ L_{0}, …, L_{m−1} ) ∈ 𝔼_{s}^{v} over Σ, V where w_{j}, w′_{j} are the terms of L_{j}, and any σ, σ′ : V(e) → T (Σ′, X) with σ(•_{s}) = u, σ′(•_{s}) = u′, and ∀x ∈ V(e)\{•_{s}}. σ(x) = σ′(x) ∈ GT (Σ′)_{DAT}, there either is some i ≺ m such that ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{i−1}, Def w′_{i−1}, L_{i−1}, Def w_{i}, Def w′_{i}, \overline{L_{i}} )σ or ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{i−1}, Def w′_{i−1}, L_{i−1}, Def w_{i}, Def w′_{i}, \overline{L_{i}} )σ′ is fulfilled w.r.t. ⟶, H or otherwise ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{m−1}, Def w′_{m−1}, L_{m−1} )σ and ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{m−1}, Def w′_{m−1}, L_{m−1} )σ′ are fulfilled w.r.t. ⟶, H and, in case of v ≠ pred, eσ=eσ′ is fulfilled w.r.t. ⟶, H, and, in case of v ≠ pred, eσ, eσ′ is fulfilled w.r.t. ⟶, H.

u≠u′:

If s ∈ 𝕍: There are terms t, t′ whose function symbols are constructors from ℂ′ and whose variables are of hidden sort, and two substitutions σ : V(t) → T (Σ′, X), σ′ : V(t′) → T (Σ′, X), such that u⟶^{∗}tσ, u′⟶^{∗}t′σ′, and either t and t′ are clashing or else t and t′ are equal and there is some x ∈ V_{GEN,h}(t) such that h ∈ ℍ_{≠} and xσ≠xσ′ is fulfilled w.r.t. ⟶, H.

If s ∈ ℍ_{≠}: For any v ∈ 𝕍, any experiment ( e ⟵ L_{0}, …, L_{m−1} ) ∈ 𝔼_{s}^{v} over Σ, V where w_{j}, w′_{j} are the terms of L_{j}, and any σ, σ′ : V(e) → T (Σ′, X) with σ(•_{s}) = u, σ′(•_{s}) = u′, and ∀x ∈ V(e)\{•_{s}}. σ(x) = σ′(x) ∈ GT (Σ′)_{DAT}, there either is some i ≺ m such that ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{i−1}, Def w′_{i−1}, L_{i−1}, Def w_{i}, Def w′_{i}, \overline{L_{i}} )σ or ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{i−1}, Def w′_{i−1}, L_{i−1}, Def w_{i}, Def w′_{i}, \overline{L_{i}} )σ′ is fulfilled w.r.t. ⟶, H or otherwise ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{m−1}, Def w′_{m−1}, L_{m−1} )σ and ( Def w_{0}, Def w′_{0}, L_{0}, …, Def w_{m−1}, Def w′_{m−1}, L_{m−1} )σ′ are fulfilled w.r.t. ⟶, H and (note v ≠ pred) eσ≠eσ′ is fulfilled w.r.t. ⟶, H.

p(w_{0}, …, w_{n−1}): If there is some p(w′_{0}, …, w′_{n−1}) ∈ H such that for each j ≺ n either w_{i} is equal to w′_{i} or (w_{i}=w′_{i}) is fulfilled w.r.t. ⟶, H.

July 23, 2008 25

Notes References

Peter Aczel (1988). Non-Well-Founded Sets. CSLI Lecture Notes 14, Stanford Univ.. Peter B. Andrews (1986). An Introduction to Mathematical Logic and Type Theory. Aca-

demic Press (Elsevier). Jürgen Avenhaus, Klaus Madlener (1990). Term Rewriting and Equational Reasoning. In:

R. B. Banerji (ed.). Formal Techniques in Artificial Intelligence, pp. 1–43, Elsevier. Matthias Baaz, Christian G. Fermüller (1995). Non-elementary Speedups between Different

Versions of Tableaux. 4^{th} TABLEAUX 1995, LNAI 918, pp. 217–230, Springer. Matthias Baaz, Uwe Egly, Christian G. Fermüller (1997). Lean Induction Principles for

Tableaux. 6^{th} TABLEAUX 1997, LNAI 1227, pp. 62–75, Springer. Leo Bachmair (1988). Proof By Consistency in Equational Theories. 3^{rd} IEEE Symposium

on Logic In Computer Sci., pp. 228–233, IEEE Press. Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg (1997). Computing Answers with

Model Elimination. Artificial Intelligence 90, pp. 135–176. Bernhard Beckert, Reiner Hähnle (1998). Analytic Tableaux. In: Bibel & Schmitt (1998),

Vol. 1, pp. 11–41. Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (1993). The Even More Liberalized δ-

Rule in Free Variable Semantic Tableaux. Kurt Gödel Colloquium, LNCS 713, pp. 108-119, Springer.

Wolfgang Bibel (1987). Automated Theorem Proving. 2^{nd} rev. ed., Vieweg, Braunschweig. Wolfgang Bibel, Peter H. Schmitt (eds.) (1998). Automated Deduction — A Basis for Appli-

cations. Kluwer (Springer). Susanne Biundo, Birgit Hummel, Dieter Hutter, Christoph Walther (1986). The Karlsruhe

Induction Theorem Proving System. 8^{th} CADE 1986, LNCS 230, pp. 672–674, Springer. Adel Bouhoula, Michaël Rusinowitch (1995). Implicit Induction in Conditional Theories.

J. Automated Reasoning 14, pp. 189–235, Kluwer (Springer). Adel Bouhoula, Emmanuël Kounalis, Michaël Rusinowitch (1992). Automated Mathematical

Induction. Technical Report 1636, INRIA. Nicolas Bourbaki (1954). Livre I — Théorie des Ensembles. Hermann, Paris. Robert S. Boyer, J S. Moore (1979). A Computational Logic. Academic Press (Elsevier). Robert S. Boyer, J S. Moore (1988). A Computational Logic Handbook. Academic Press

(Elsevier). Hans-Jürgen Bürckert, Bernhard Hollunder, Armin Laux (1993). On Skolemization in Con-

strained Logics. DFKI Research Report RR–93–06, Saarbrücken. Also in: Annals of Mathematics and Artificial Intelligence 18, pp. 95-131, Balzer Sci. Publ., 1996.

Ricardo Caferra, Gernot Salzer (eds.) (2000). Automated Deduction in Classical and Non-Classical Logics. LNAI 1761, Springer.

Domenico Cantone, Marianna Nicolosi-Asmundo (2000). A Further and Effective Liberalization of the δ-Rule in Free Variable Semantic Tableaux. In: Caferra & Salzer (2000), pp. 109–125.

Hartmut Ehrig, Bernd Mahr (1985). Fundamentals of Algebraic Specification 1. Springer.

Herbert B. Enderton (1973). A Mathematical Introduction to Logic. 2^{nd} printing, Academic Press (Elsevier).

Melvin C. Fitting (1996). First-Order Logic and Automated Theorem Proving. 2^{nd} extd. ed., Springer.

Marco Forti, Furio Honsell, Marina Lenisa (1996). Axiomatic Characterizations of Hyperuniverses and Applications. Annals of the New York Academy of Sci., vol.80, pp. 140– 163.

Dov M. Gabbay, C. J. Hogger, J. A. Robinson (eds.) (1993 ff.). Handbook of Logic in Artificial Intelligence and Logic Programming. Clarendon Press.

Gerhard Gentzen (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, pp. 176-210, 405–431.

Gerhard Gentzen (1938). 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, Folge 4, Leipzig.

Alfons Geser (1995). A Principle of Non-Wellfounded Induction. In: Tiziana Margaria (ed.). Kolloquium Programmiersprachen und Grundlagen der Programmierung, MIP–9519, pp. 117-124, Univ. Passau.

Martin Giese (1998). Integriertes automatisches und interaktives Beweisen: die Kalkülebene.

Master’s thesis, Univ. Karlsruhe. http://i11www\netdotira\netdotuka\netdotde\
netslash\~{}giese\netslashda\psgz (May09,2000).

Martin Giese, Wolfgang Ahrendt (1999). Hilbert’s ε-Terms in Automated Theorem Proving. 8^{th} TABLEAUX 1999, LNAI 1617, pp. 171–185, Springer.

Kurt Gödel (1986 ff.). Collected Works. Solomon Feferman (ed.), Oxford Univ. Press.

Bernhard Gramlich, Wolfgang Lindner (1991). A Guide to Unicom, an Inductive Theorem Prover Based on Rewriting and Completion Techniques. SEKI-Report SR–91–17 (SFB), FB Informatik, Univ. Kaiserslautern. http://agent\

netdotinformatik\netdotuni-kl\netdotde\netslashseki\netslash1991\
netslashLindner\netdotSR-91-17\psgz (May09,2000).

Reiner Hähnle, Peter H. Schmitt (1994). The Liberalized δ-Rule in Free Variable Semantic Tableaux. J. Automated Reasoning 13, pp. 211–221, Kluwer (Springer).

David Hilbert, Paul Bernays (1968/70). Grundlagen der Mathematik. 2^{nd} ed., Springer.

Paul Howard, Jean E. Rubin (1998). Consequences of the Axiom of Choice. Math. Surv. and Monographs, Vol. 58, American Math. Society.

Bart Jacobs, Jan Rutten (1997). A Tutorial on (Co)Algebras and Co(Induction). Bull.

EATCS 62, pp. 222–259. http://www\netdotcs\netdotkun\netdotnl\netslash\
~{}bart\netslashPAPERS\netslashJR\netdotps\netdotZ (Oct.15,1999).

Stig Kanger (1963). A Simplified Proof Method for Elementary Logic. In: Siekmann & Wrightson (1983), Vol. 1, pp. 364-371.

Deepak Kapur, Hantao Zhang (1989). An Overview of Rewrite Rule Laboratory ( Rrl). 3^{rd} RTA 1989, LNCS 355, pp. 559–563, Springer.

Manfred Kerber (1998). Proof Planning: A Practical Approach to Mechanized Reasoning in Mathemantics. In: Bibel & Schmitt (1998), Vol. 3, pp. 77–95.

Jan Willem Klop (1992). Term Rewriting Systems. In: S. Abramsky, Dov M. Gabbay, T. S. E. Maibaum (eds.). Handbook of Logic in Computer Science, Vol. 2, Clarendon Press.

Donald E. Knuth (1997 f.). The Art of Computer Programming. 3^{rd} ed., Addison-Wesley.

Michaël Kohlhase (1995). Higher-Order Tableaux. 4^{th} TABLEAUX 1995, LNAI 918, pp. 294– 309, Springer. Revised version is: Kohlhase (1998).

Michaël Kohlhase (1998). Higher-Order Automated Theorem Proving. In: Bibel & Schmitt (1998), Vol. 1, pp. 431–462.

Emmanuël Kounalis, Michaël Rusinowitch (1990). Mechanizing Inductive Reasoning. 8^{th} AAAI 1990, pp. 240–245, MIT Press.

Georg Kreisel (1965). Mathematical Logic. In: T. L. Saaty (ed.). Lectures on Modern Mathematics, Vol. III, pp. 95–195, John Wiley & Sons, New York.

Christoph Kreitz, Brigitte Pientka (2000). Matrix-based Inductive Theorem Proving. 9^{th} TABLEAUX 2000, LNAI 1847, pp. 294–308, Springer.

Ulrich Kühler (2000). A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Ph.D. thesis, Infix, Akademische Verlagsgesellschaft Aka GmbH, Sankt Augustin, Berlin.

Ulrich Kühler, Claus-Peter Wirth (1996). Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. SEKI-Report SR–96–11, FB Informatik, Univ. Kaiserslautern. Short version in: 8^{th} RTA 1997, LNCS 1232, pp. 38–52, Springer. http://\wwwcppubladdressrta97\

netslashwelcome\netdothtml (May09,2000).

Al(bert) C. Leisenring (1969). Mathematical Logic and Hilbert’s ε-Symbol. Gordon and Breach, New York.

Vladimir A. Lifschitz (1971). Specialization of the Form of Deduction in the Predicate Calculus with Equality and Function Symbols. In: Orevkov (1971), pp. 1-24.

Vladimir A. Lifschitz (1989). What Is the Inverse Method?. J. Automated Reasoning 5, pp. 1–23, Kluwer (Springer).

Sergey Yu. Maslov (1971). The Inverse Method for Establishing Deducibility for Logic Cal-

culi. In: Orevkov (1971), pp. 25-96. Dale A. Miller (1992). Unification under a Mixed Prefix. J. Symbolic Computation 14,

pp. 321–358, Academic Press (Elsevier). Andreas Nonnengart (1996). Strong Skolemization. MPI–I–96–2–010, Max Planck Inst. für

Informatik, Saarbrücken. Vladimir P. Orevkov (1971). The Calculi of Symbolic Logic.I. American Mathematical So-

ciety, Providence, Rhode Island. Peter Padawitz (1996). Inductive Theorem Proving for Design Specifications. J. Symbolic

Computation 21, pp. 41–99, Academic Press (Elsevier). Peter Padawitz (1998). Expander. A System for Testing and Verifying Functional Logic

   Programs. http://\wwwpadawitzpubl{ExpaTex\psgz} (Sept.14,1999).

Michaël S. Paterson, Mark N. Wegman (1978). Linear Unification. J. Computer and System

Sci. 16, pp. 158–167, Academic Press (Elsevier). Padawitz (2000). Swinging types = functions + relations + transition systems. Theoretical

Computer Sci. 243, pp. 93–165, Elsevier. Dag Prawitz (1960). An Improved Proof Procedure. In: Siekmann & Wrightson (1983),

Vol. 1, pp. 159-199. Dag Prawitz (1965). Natural Deduction. Almquist & Wiksells, Uppsala. Martin Protzen (1994). Lazy Generation of Induction Hypotheses. 12^{th} CADE 1994,

LNAI 814, pp. 42–56, Springer. Long version in: Protzen (1995). Martin Protzen (1995). Lazy Generation of Induction Hypotheses and Patching Faulty Con-

jectures. Ph.D. thesis, Infix, Akademische Verlagsgesellschaft Aka GmbH, Sankt Augustin, Berlin.

Horst Reichel (1987). Initial Computability, Algebraic Specifications, and Partial Algebras.

Clarendon Press. Grigore Roşu, Joseph Goguen (1998). Hidden Congruent Deduction. In: Caferra & Salzer

   (2000), pp. 251–266. http://www-cse\netdotucsd\netdotedu\netslashusers\
   netslashgoguen\netslashps\netslashcong\netdotps\netdotgz (Oct.20,1999).

Herman Rubin, Jean E. Rubin (1985). Equivalents of the Axiom of Choice. Elsevier. Jörg Siekmann, Graham Wrightson (eds.) (1983). Automation of Reasoning. Springer. Raymond M. Smullyan (1968). First-Order Logic. Springer. Wayne Snyder, Jean Gallier (1989). Higher-Order Unification Revisited: Complete Sets of

Transformations. J. Symbolic Computation 8, pp. 101–140, Academic Press (Elsevier). Christoph Walther (1992). Computing Induction Axioms. 3^{rd} LPAR 1992, LNAI 624,

pp. 381–392, Springer.

Christoph Walther (1994). Mathematical Induction. In: Gabbay &al. (1993 ff.), Vol. 2, pp. 127-228.

Claus-Peter Wirth (1997). Positive/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving. Ph.D. thesis, Verlag Dr. Kovač, Hamburg.

Claus-Peter Wirth (1998). Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but Without Skolemization. Report 698/1998, FB Informatik, Univ. Dortmund. Short version in: Gernot Salzer, Ricardo Caferra (eds.). Proc. 2^{nd} Int. Workshop on First-Order Theorem Proving (FTP’98), pp. 244–255, Tech. Univ. Vienna, 1998. Short version also in: Caferra & Salzer (2000), pp. 283–298.

http://\wwwcppubladdressftp98\netslashwelcome\netdothtml (May09,2000).

Claus-Peter Wirth (1999). Full First-Order Free Variable Sequents and Tableaux in Implicit Induction. 8^{th} TABLEAUX 1999, LNAI 1617, pp. 293–307, Springer. http://

\wwwcppubladdresstab99\netslashwelcome\netdothtml (May09,2000).

Claus-Peter Wirth, Klaus Becker (1995). Abstract Notions and Inference Systems for Proofs by Mathematical Induction. 4^{th} CTRS 1994, LNCS 968, pp. 353–373, Springer. http:

//\wwwcppubladdressctrs94\netslashwelcome\netdothtml (May09,2000).

Claus-Peter Wirth, Bernhard Gramlich (1994a). A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications. J. Symbolic Computation 17, pp. 51–90, Academic Press (Elsevier). http://\wwwcppubladdressjsc94\

netslashwelcome\netdothtml (May09,2000).

Claus-Peter Wirth, Bernhard Gramlich (1994b). On Notions of Inductive Validity for First-Order Equational Clauses. 12^{th} CADE 1994, LNAI 814, pp. 162–176, Springer. http:

//\wwwcppubladdresscade94\netslashwelcome\netdothtml (May09,2000).

Ludwig Wittgenstein (1922). Tractatus Logico-Philosophicus. C. K. Ogden (ed.), Rout-

ledge and Kegan Paul, London. http://www\netdotkfs\netdotorg\netslash\
~{}jonathan\netslashwitt\netslashtlph\netdothtml (Feb.09,2000).

Ludwig Wittgenstein (1939). Lectures on the Foundations of Mathematics, Cambridge. Cora Diamond (ed.), from the notes of R. G. Bosanquet, Norman Malcolm, Rush Rhees, and Yorick Smythies, Univ. of Chicago Press, 1989.