LFCS

Laboratory for Foundations of Computer Science

Department of Computer Science — The University of Edinburgh

Relative Equational Specification and Semantics

by

Jo Erskine Hannay

LFCS Report Series ECS–LFCS–97–366 LFCS October 1997

Department of Computer Science University of Edinburgh The King’s Buildings Edinburgh EH9 3JZ

Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, LFCS

Relative Equational Specification and Semantics

Jo Erskine Hannay

Technical Report ECS–LFCS–97–366 Department of Computer Science University of Edinburgh

October 7, 1997

Abstract: Standard concepts of initial and final algebra semantics are generalised in a modular hierarchical manner. The resulting relative formalism allows a unified view on the relationship between initial and final algebra semantics and gives a dualised notion of consistency. Using this, a modular hierarchical approach to proof by consistency is taken by which only top-level equations need be considered at any level. The formalism also allows non-homogeneous specification schemes and different proof methods at each level.

Contents

1 Introduction 2

2 Preliminaries 3

3 Equational Specification and Semantics 7

4 Relative Specification and Semantics 9 4.1 Relative Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.2 Relative Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

5 Modularity under Consistency 14 5.1 Kernel Preservation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 5.2 Separability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.3 Inconsistency revealed as referential opacity . . . . . . . . . . . . . . . . . 20

6 Proof by Kernel Preservation 22

7 Non-homogeneous hierarchies 25

8 Concluding Remarks 26

1 Introduction

One incentive for equational (algebraic) specification of abstract data types is its aptness for a variety of simple and efficient methods of formal semi-mechanised proof. A particularly immediate family of proof methods are those based on term rewriting techniques. Two choices of semantics dealt especially with by rewrite based methods are initial and final/terminal (algebra) semantics. Roughly, two terms are semantically equal according to initial algebra semantics only if their equality can be proven in the equational calculus. Final algebra semantics on the other hand, determine two terms equal unless proven otherwise in the calculus. In a purely equational language, to prove an “inequation” is to show distinguishability of the two terms involved w.r.t. a given basic (primitive) semantics, i.e. s cannot be equivalent to t if there is a context c such that c[s] and c[t] are not equivalent according to the primitive/basic semantics. Hence, final semantics is observational and behavioural in that two terms are equivalent if they “behave” equivalently when used in observable (relevant) contexts. Besides being able to easily describe data types which are cumbersome to describe directly (maps, infinite data types, processes [Pad95]), final semantics also provides abstraction up to equivalent observable behaviour as described by behavioural and observational semantics, e.g. [ST87, BHW94].

Proof by consistency is a general method for proving/refuting equations according to initial or final semantics. The idea pioneered by Musser [Mus80], is that when adding a hypothesis to a specification, Knuth-Bendix completion [KB70] may be applied for detecting inconsistencies refuting the hypothesis. The method also goes by the name “induction-less induction”, the ‘induction’ in question being the structural induction of [Bur69, Gut75]. For the initial case, the general method has been elaborated by many authors e.g. [Gog80, HH82, JK89, Küc89, Fri86, Bac88]. In [LPL96] proof by consistency is adapted to higher-order term-rewriting.

A method for proof by consistency in final semantics was described in [Pue84]. Structural context induction [Hen91, Hen92] has been developed for proofs according to behavioural and observational semantics, hence one might call proof by consistency in final semantics “induction-less” context induction. Lysne in [Lys92, Lys94] observes that proof by consistency is inherently close in spirit to reasoning according to final semantics, since explicit output is a witness of distinguishability. Lysne describes an approach to proof by consistency according to final semantics which subsumes, fully or partly, several of the approaches designated for initial semantics.

This note elaborates on the relationship between initial and final semantics. Final semantics are defined relatively to an underlying initial semantics in which inequalities are observed. Also, consistency in the initial sense can be seen as relative to a “kernel” semantics. These evident notions of relativity are made explicit by presenting a formalism, relative semantics, which provides a common vantage point for initial and final semantics. The formalism expresses consistency more explicitly, and enables a nice dualised understanding of different concepts of consistency. Explicit mention of a “kernel”, displays a link with hierarchical specification as in [WPP^{+}83]. The formalism of relative semantics thus suggests a modular hierarchical style of specification linked directly to modular level-wise proof by consistency. Early ideas of a hierarchical approach to consistency and inductive completion for initial semantics appear in [Kir84].

Relative semantics is a generalisation in several respects. Firstly, it generalises standard initial and final semantics into one common framework. Secondly, it generalises initial and final semantics to arbitrary level hierarchies of semantics. Thirdly, whereas other methods yield hierarchical constructs which always can be viewed monolithically, relative semantics also cater for non-homogeneous situations where one cannot reduce a hierarchy to a monolithic heap. Indeed, by catering for non-homogeneous specification the relative construction supports different proof methods at each level.

The formalism of relative semantics presented here first appeared in [Han95]. In [Pad95] a similar formalism is presented in the context of general inductive and co-inductive definitions of relations and functions with corresponding initial (least fixed-point) and final (greatest fixed-point) semantics (e.g. [Gor94]). The way in [Pad95] of dealing with proofs according to final semantics is by explicitly converting co-inductive definitions to inductive ones using finite approximants thereby making inductive proof techniques applicable in the final case. This is somewhat different from the approach described in the present note, where the observation that proof by consistency is inherently co-inductive in nature is used for doing proofs directly according to final semantics. Also, emphasis is on notions of consistency which we find useful for understanding more of the common nature of initial and final semantics, and on modularity of structures and proofs in such a way as to allow different proof methods at each level.

Section 2 reviews basic notions, section 3 reviews definitions of initial and final semantics, sections 4 & 5 introduce relative semantics and notions of consistency, section 6 describes modular level-wise proof by consistency and section 7 illustrates non-homogeneous specification and reasoning.

2 Preliminaries

This section gives some basic notions of algebraic specification and term rewriting that are used directly in this note. They are to be found in greater detail for algebraic specification in [Wir90] or [EM85], and for rewriting in [Klo92] or [DJ90].

We will be dealing with many-sorted specifications whose semantics will be given as classes of total many-sorted algebras with non-empty carriers.

A signature Σ = ⟨S, F ⟩ consists of a set of sorts and a set of function symbol profiles of the form f : s_{1} × ⋯ × s_{n} → s for s_{1}, …, s_{n}, s ∈ S giving a function symbol along with its arity and sort. A function symbol with arity 0 is called a constant. A sensible signature has at least one constant of every sort in S. Without further mention all signatures in this note are assumed sensible. A total heterogeneous Σ-algebra A = ⟨⟨A_{s}⟩_{s∈S}, ⟨f^{A}⟩_{f∈F} ⟩ consists of an S-indexed family ⟨A_{s}⟩_{s∈S} of non-empty carriers and an F -indexed ⟨f^{A}⟩_{f∈F} family of total functions containing an f^{A} ∈ (A_{s_{1}}×⋯×A_{s_{n}} → A_{s}) for every f : s_{1}×⋯×s_{n} → s ∈ F. All algebras in this note are assumed to be total. A Σ-term algebra T_{Σ}(X) for a set of variables X is the free algebra generated from X over the signature Σ, any carrier T_{Σ}(X)_{s} containing exactly the terms of sort s generated from X and Σ. The ground-term Σ-algebra T_{Σ}(∅) is denoted by G_{Σ}.

In the following, let Σ = ⟨S, F ⟩ be fixed. A homomorphism ϕ : A → B is a family ⟨ϕ_{s} ∈ (A_{s} → B_{s})⟩_{s∈S} of mappings such that for all f : s_{1} × ⋯ × s_{n} → s ∈ F and all a_{1} ∈ A_{s_{1}}, …, a_{n} ∈ A_{s_{n}}: ϕ_{s}(f^{A}(a_{1}, …, a_{n})) = f^{B}(ϕ_{s_{1}}(a_{1}), …, ϕ_{s_{n}}(a_{n})).

A substitution is a homomorphism σ : T_{Σ}(X) → T_{Σ}(X). A context c[□] is a term with a single place holder or hole □. We write c ∈ T_{Σ}(X) for c[□] ∈ T_{Σ∪{□ }}(X). Context application is a context with a term substituted for its place holder, e.g. c[s];

An interpretation ϕ_{T_{Σ}(X)}^{A} : T_{Σ}(X) → A is a homomorphism from a term-algebra to an algebra in which one can think of the terms as being interpreted. A computation structure is an algebra A such that ϕ_{G_{Σ}}^{A} is surjective, i.e. all carrier elements are denotable by ground terms.

A congruence ∼ on an algebra A is a family ⟨∼_{s}⟩_{s∈S} such that each ∼_{s} is an equivalence relation on A_{s} and if f : s_{1} × ⋯ × s_{n} → s ∈ F then for all a_{1}, b_{1} ∈ A_{s_{1}}, …, a_{n}, b_{n} ∈ A_{s_{n}}: a_{1} ∼_{s_{1}} b_{1}, …, a_{n} ∼_{s_{n}} b_{n} ⇒ f^{A}(a_{1}, …, a_{n}) ∼_{s} f^{A}(b_{1}, …, b_{n}). The quotient A/∼ w.r.t. an algebra A and congruence ∼ is the algebra with carriers A_{s}/∼_{s} for each s ∈ S and functions defined by f^{A/∼}([a_{1}]_{∼_{s_{1}}}, …, [a_{n}]_{∼_{sn}}) = [f(a_{1}, …, a_{n})]_{∼_{s}}, for every f : s_{1}×⋯×s_{n} → s ∈ F.

An algebra A is initial in a class K of Σ-algebras if A ∈ K and for every B in K there exists exactly one homomorphism from A to B. Conversely A is final in K if A ∈ K and for every B in K there exists exactly one homomorphism from B to A.

A (Σ-)equation is an element in T_{Σ}(X)_{s} × T_{Σ}(X)_{s}, written u = v, for u, v ∈ T_{Σ}(X)_{s}; s ∈ S, and is valid in a Σ-algebra A, written A ⊧ u = v, iff ϕ_{T_{Σ}(X)}^{A}(u) = ϕ_{T_{Σ}(X)}^{A}(v) for all interpretations ϕ_{T_{Σ}(X)}^{A}. A Σ-algebra A is a model for a set of Σ-equations E if every equation in E is valid in A. The class of all Σ-algebras which are models for E is denoted by Mod_{Σ}(E). The following is an important fact relating initiality and finality to validity.

Fact 1. For any g, g′ ∈ G_{Σ}

1. A Σ-computation structure I is initial in a class K of Σ-algebras iff I ⊧ g = g′ ⇔ for all A ∈ K : A ⊧ g = g′.

2. A Σ-computation structure F is final in a class C of Σ-computation structures iff F |̸= g = g′ ⇔ for all A ∈ C : A |̸= g = g′.

A term rewrite system (TRS) ⟨Σ, R⟩ consist of a signature and a set R of rewrite rules v → h over T_{Σ}(X). A TRS is often simply denoted by its set of rules R. For any s, t ∈ T_{Σ}(X), s rewrites in R to t in one step, written s →_{R} t, if there is a v → h ∈ R and a substitution σ such that s = c[vσ] and t = c[hσ], for some context c[□]. The task of finding such a σ and c[□] is called matching and is algorithmic. The relation →_{R} is a rewrite relation, meaning it fulfils s →_{R} t ⇒ c[sσ] →_{R} c[tσ] for all contexts c[□] and substitutions σ. Moreover it is the least such rewrite relation, meaning that →_{R} is the rewrite closure of R.

The transitive closure of →_{R} is denoted by →_{R}^{+} , the reflexive-transitive closure by →_{R}^{∗} and the symmetric closure by ↔_{R}.

The equational calculus will be dealt with in the equivalent form of symmetric TRSs; i.e. we consider as provability relation for a given set of equations E, the relation ↔_{E}^{∗}; i.e. the rewrite, reflexive, symmetric, transitive closure of E. For any terms s and t and set of equations E, we then have E ⊢ s = t ⇔ s ↔_{E}^{∗} t. For any set of rules or equations E, the closure ↔_{E}^{∗} is a congruence, and quotients w.r.t. ↔_{E}^{∗} are usually written A/E.

For any relation ℜ a derivation in ℜ is a possibly infinite sequence ⟨t_{0}, t_{1}, …, t_{i}, …⟩ such that for every 1 ≤ j ≤ n, t_{j} ℜ t_{j+1}.

A TRS ⟨Σ, R⟩ is terminating if there is no infinite derivation in →_{R}. It is confluent if

s ←_{R}^{∗} w →_{R}^{∗} t ⇒ ∃u | s →_{R}^{∗} u ←_{R}^{∗} t

If both these properties are present the TRS is complete. One then has a rewrite driven decision procedure for the relation ↔_{R}^{∗}, if R has finitely many rules: Completeness gives that every term t ∈ T_{Σ}(X) has a unique normal form t!, i.e. a unique t! such that t →_{R}^{∗} t! and ∄u | t! →_{R}^{∗} u, which can be computed in finitely many steps.

Knuth-Bendix completion [KB70] was originally designed to generate a complete R with the same equational theory as a given set of equations E. However, in the attempt of generating such a TRS, the procedure derives new theorems in a certain manner which can be useful for other purposes even if it doesn’t succeed in its completion task. The method of proof by consistency thus uses the completion process to derive certain inconsistency witnesses generated if an added equation is not an inductive consequence of the equations already present. This checks hypotheses according to the initial model, but as mentioned in the introduction the method can also be used according to other semantics, e.g. final algebra semantics.

Completion is usually described by a set of inference rules manipulating a pair ⟨E, R⟩ (see any of the two references above) and the relation ⊢_{KB} is defined such that ⟨E, R⟩ ⊢_{KB} ⟨E′, R′⟩ if ⟨E′, R′⟩ is obtainable from ⟨E, R⟩ in one step by applying any of the inference rules. A possibly infinite completion sequence ⟨⟨E_{0}, R_{0}⟩, …, ⟨E_{i}, R_{i}⟩, …⟩ is then such that for every i, ⟨E_{i}, R_{i}⟩ ⊢_{KB} ⟨E_{i+1}, R_{i+1}⟩. Running completion in the original sense means ideally hoping for the following property: ⟨E, ∅⟩ ⊢_{KB}^{∗} ⟨∅, R⟩ and no inference rule is applicable. Then R is complete and has the same equational theory as E. Since the starting point is a set of unordered equations, and since termination is in general undecidable, a completion process is equipped with a user defined term ordering so that equations, original or generated, may be oriented into rewrite rules in such a way that every R_{i} is terminating.

The driving force in completion is the elimination of non-confluence (this view is due to Bachmair [Bac91]). Any derivation of s ↔_{R}^{∗} t for a non-confluent R might have peaks s_{i−1} ←_{R}s_{i} →_{R}s_{i+1} as well as valleys s_{j−1} →_{R}s_{j} ←_{R}s_{j+1}. A completion process may be viewed as a peak elimination process, ultimately seeking to produce a set of rules such that a rewrite proof s →_{R}^{∗} u ←_{R}^{∗} t is possible for every s, t s.t. s ↔_{R}^{∗} t. We have:

Fact 2. (Bachmair [Bac87]) Suppose a possibly infinite completion sequence

⟨⟨E_{0}, R_{0}⟩, …, ⟨E_{i}, R_{i}⟩, …⟩

is fair w.r.t. inferences, i.e. no possible inference is overlooked infinitely often and every equation generated is orientable. Then for any s and t:

s ↔_{E_{0}}^{∗} t ⇔ ∃j | s!R_{j} = t!R_{j}

It is this property that we will be using for our version of proof by consistency.

One standard form of proof by consistency is based on inductive completion. A term t is said to be ground reducible in R if for all ground substitutions σ ∈ (T_{Σ}(X) → G_{Σ}), there exists a u such that tσ →_{R}^{+} u. Ground reducibility is decidable. We have:

Fact 3 (Inductive completion). Let R be complete and having the same equational theory as E. For any equation s = t consider a completion sequence

⟨⟨E_{0}, R_{0}⟩, …, ⟨E_{i}, R_{i}⟩, …⟩

which is fair w.r.t. inferences, and where every equation generated is orientable. Then:

G_{Σ}/E |̸= H
⇕

a rule ⟨l, r⟩ is generated during the process s.t. l is not ground reducible in R.

Constructive function specification suggests viewing a signature Σ as disjointly divided into Σ_{c} consisting of constructors and Σ_{d} consisting of defined operators. Essential syntactic qualities are then captured as follows:

Definition 1. (Guttag [Gut77]) A set of equations or rules E is sufficiently complete w.r.t. Σ_{c} if for every g ∈ G_{Σ} there exists a g_{c} ∈ G_{Σ_{c}} such that g ↔_{E}^{∗} g_{c}.

Definition 2. (Guttag [Gut77]) Let E_{c} be the Σ_{c}-equations in E. Then, E is consistent

w.r.t. Σ_{c} if g_{c} ↔_{E}^{∗} g′_{c} ⇔ g_{c} ↔_{Ec}^{∗} g′_{c} for arbitrary g_{c}, g′_{c} ∈ G_{Σ_{c}}.

Suppose now that the term ordering given for completion is such that every u ∈ T_{Σ_{d}∪Σ_{c}}(X)\ T_{Σ_{c}}(X) is greater in the ordering than all v ∈ T_{Σ_{c}}(X)., and that R is sufficiently complete w.r.t. Σ_{c}. Then a refuting witness l = r for inductive completion will be a rule purely over T_{Σ_{c}}(X), and moreover for some ground substitution σ, lσ↮_{R}^{∗} rσ. Thus, a refuting witness is a rule which collapses R-equivalence classes, i.e. E-equivalence classes in G_{Σ}/E. Moreover, since R is complete, R is consistent w.r.t. Σ_{c}: Suppose g_{c} ↔_{R}^{∗} g′_{c}. Then by completeness we have g_{c} →_{R}^{∗}g_{c}!←_{R}^{∗}g′_{c}, and by the term ordering g_{c} →_{Rc}^{∗}g_{c}!←_{Rc}^{∗}g′_{c}. A refuting witness is therefore a witness of inconsistency in the sense of definition 2, resulting from adding the hypothesis s = t.

There are essentially two things that can go wrong in any completion based process. One is non-termination of the process. There are however results [Her92] that can be used in some cases to determine whether an infinite sequence will bring anything essentially new, or not, in which case the remaining sequence can be neglected. The more annoying thing that may happen is inability to orient some equation, either because the given term ordering is too weak, or because it is fundamentally impossible to orient the equation without giving a non-terminating set of rules. There are extensions to standard rewriting and completion which try to deal with the latter case. Ordered rewriting and completion exploit the possibility that all ground instances of equations may be orientable. Extended or class rewriting puts all non-orientable equations in a separate set and does rewriting and completion modulo the equational theory of this set. The appropriate versions of facts 2 and 3 hold for these variants.

3 Equational Specification and Semantics

In proof technical considerations as those done for e.g. proof by consistency, the models directly involved are syntax dependent term models of specifications or equations. These are typically, and naturally, initial or final in character. The semantics defined in the following two sections for the specification formalisms presented there all give term models generated directly from the syntax and the equations involved. In section 4, the semantics of relative specifications is generated this way relative to a kernel semantics.

Initial and final semantics represent monomorphic interpretation schemes in that model classes for specifications consist of exactly one algebra (up to isomorphism). In a refinement setting [ST97, Mor94] monomorphic semantics are directly relevant at final stages of development, but due to fact 1, these semantics also represent larger model classes and are thus relevant at earlier development stages as well.

This section reviews standard notions of equational specification and initial and final semantics. The next section introduces relative equational specification and initial and final semantics thereof.

Definition 3. An (equational) specification SP is a pair SP = ⟨Σ, E⟩ consisting of a signature Σ and a set of Σ-equations E.

Initial and final semantics are described as follows:

Definition 4. For SP = ⟨Σ, E⟩ a specification, the restriction ↔_{E}^{∗} _{G_{Σ}} of ↔_{E}^{∗} to G_{Σ} is the initial semantics specified by SP.

Definition 5. (e.g. Lysne [Lys92]) For SP = ⟨Σ, E⟩ a specification, the congruence

g ∼^{Q} g′ ⇔ ¬∃c ∈ G_{Σ}; g_{c} ∈ G_{Σ_{c}} | (c[g] ↔_{E}^{∗} g_{c} ↮_{E}^{∗} c[g′] or c[g′] ↔_{E}^{∗} g_{c} ↮_{E}^{∗} c[g])

is the final semantics specified by SP.

Since for any congruence ∼ on G_{Σ}, g ∼ g′ ⇔ G_{Σ}/∼ ⊧ g = g′, we here deliberately confuse the semantical model G_{Σ}/∼ with the underlying ∼.

An algebra’s property of being initial or final in some interesting class of algebras may reveal information as to how well the corresponding interpretation scheme fulfils the intentions of specification. The monomorphic intention behind the specification formalisms dealt with here would be that one specifies all there is, i.e. all intended semantic equalities are specified (initial intention), or that all semantic inequalities are specified (final intention).

Let ∼ be any congruence on G_{Σ}. Consider the class

⌊∼⌋_{Σ} = {A | g ∼ g′ ⇒ A ⊧ g = g′}

of Σ-computation structures. An algebra in ⌊∼⌋_{Σ} satisfies all the equalities (and perhaps more) induced by ∼. For example, the restriction of Mod_{Σ}(E) to computation structures is by completeness (Birkhoff) the class ⌊↔_{E}^{∗}⌋_{Σ}. On the other hand, the algebras in the class of Σ-computation structures

⌈∼⌉_{Σ} = {A | g ≁ g′ ⇒ A |̸= g = g′}

satisfy no equality which is not induced by ∼.^{1}

The quotient G_{Σ}/E (G_{Σ}/↔_{E}^{∗}) is initial in ⌊↔_{E}^{∗}⌋_{Σ}, meaning that it is the computation structure model for E satisfying fewest equations, i.e. no equation holds unless explicitly entailed in the equational calculus from E. Conversely, G_{Σ}/∼^{Q} is final in ⌈↔_{Ec}^{∗}⌉_{Σ_{c}} ∩ ⌊↔_{E}^{∗}⌋_{Σ}, meaning that G_{Σ}/∼^{Q} is the computation structure model for E satisfying the greatest amount of equations, but satisfying no more equations over G_{Σ_{c}} than those explicitly entailed by E_{c}, i.e. satisfying the “inequations” of the initial semantics on G_{Σ_{c}}. Further inequalities are derived from these basic inequalities by the congruence principle:

c[g] ≁ c[g′] ⇒ g ≁ g′  (1)

(In contrast, the final model of only ⌊↔_{E}^{∗}⌋_{Σ} contains one element and is generally not very interesting.) These two extremal modes of semantics (initial and final) are the results of two natural ways of generating term models from syntax and equations.

Specific specifications will be written in a syntax suggested in the following examples. Specification names will coincide with signature names:

Example 1. The following specification just specifies integers generated by 0 and the two operators successor and predecessor, together with two operations for addition and subtraction:

spec Int_{op} sorts int constructors 0 : int, succ, pred : int → int defined oprs +, – : int × int → int axioms E_{Int_{op}} : succ(pred(x)) = x, pred(succ(x)) = x, x+0 = x, x+succ(y) = succ(x+y), x+pred(y) = pred(x+y), x – 0 = x, x–succ(y) = pred(x–y), x–pred(y) = succ(x–y)

The initial semantics ⟷_{E_{Intop}}^{∗}_{G_{Intop}} consists of all inductive consequences of E_{Int_{op}}, i.e. all equations whose ground instantiations are logical consequences of E_{Int_{op}}. ^{} Example 2. This specification specifies an operator altsum that takes as input a sequence of integers and produces the alternating sum of the sequence. Here the alternating sum of e.g. ⟨x_{0}, x_{1}, x_{2}, x_{3}, x_{4}⟩ is (x_{0} − x_{1}) + (x_{2} − x_{3}) + x_{4}.

1or satisfy all inequalities (or more) induced by ∼, but strictly speaking this formulation presumes ‘inequality’ expressible in the formula language.

spec AltSumList–Int_{op} sorts int, list constructors 0 : int, succ, pred : …, ε : list, ⊣ : int × list → list defined oprs altsum : list → int axioms E_{Int_{op}} ∪ E_{AltSumList} : altsum(ε) = 0, altsum(x ⊣ ε) = x, altsum(x ⊣ (y ⊣ q)) = (x – y) + altsum(q)

The final semantics ∼^{Q} on G_{AltSumList−Int_{op}_{c}} gives by the observer altsum that list constructor terms are semantically equal if and only if they represent integer sequences whose alternating sums are equal. ^{}

The method of this example of specifying semantics on one type based upon the initial semantics of another is studied and used in [Kam83, Les83, GHJ85, DO91].

We might bias specifications by indicating what sort of semantics we want. For example, the initially and finally biased specifications of example 1 would have the headings spec Int_{op} initial, and spec AltSumList–Int_{op} final respectively.^{2}

4 Relative Specification and Semantics

We now define relative specification and semantics. A relative semantics is defined w.r.t. a given kernel semantics, and is thus hierarchical in nature. Making a kernel explicit in specification and semantics will allow us to discuss consistency in relation to notions of conservative extensions of specifications. We also find that the definition of final semantics is a bit more intuitive when expressed relatively to an explicit kernel.

Definition 6. An (equational) relative specification is either an equational specification or a pair RSP = ⟨SP, SP^{κ}⟩ consisting of an equational specification SP = ⟨Σ, E⟩ and a relative specification SP^{κ} = ⟨Σ^{κ}, E^{κ}⟩, such that Σ^{κ} ⊆ Σ, but E ∩ E^{κ} = ∅. The specification SP^{κ} is called the kernel of RSP.

This is slightly different from the definition of hierarchical specification in [WPP^{+}83] and extension in [Pad95] where SP always includes SP^{κ}, and in particular the upper level equations of SP always include the equations of SP^{κ}. Our intention is that the two sets of equations are disjoint. This lets us reason modularly, actually disregarding details of the primitive specification. Whereas hierarchical specifications treated in e.g. [WPP^{+}83] can always be seen as non-hierarchical ones, we wish to be able to treat also non-homogeneous situations in which a hierarchy can not be viewed as a monolith (section 7). The formalism of relative specification reflects this.

2The notion of ‘bias’ here is not that discussed in connection to VDM.

A biased relative specification is a relative specification with a bias on each component SP and SP^{κ}.

4.1 Relative Semantics

We now focus on the semantics of biased relative specifications. We start with the final case. As seen in the previous section, final semantics depend upon basic inequalities in a kernel semantics in order to give new inequalities. Semantics specified in this manner are therefore inherently hierarchical. Relative semantics makes this explicit:

Definition 7. Let RSP = ⟨SP, SP^{κ}⟩ with SP = ⟨Σ, E⟩ and biased SP^{κ} = ⟨Σ^{κ}, E^{κ}⟩ be a relative specification, such that ∼^{κ} on G_{Σ^{κ}} is the semantics specified by SP^{κ}. Define the following relation ∼^{ζ}= ⟨∼_{s}^{ζ}⟩_{s∈S} on G_{Σ}: For any s ∈ S and all g, g′ ∈ G_{Σ}_{s}

g∼_{s}^{ζ}g′ ⇔ ¬∃c ∈ G_{Σ}; g_{1}, g_{2} ∈ G_{Σ^{κ}} | c[g] ↔_{E}^{∗} g_{1}≁_{s′}^{κ}g_{2} ↔_{E}^{∗} c[g′]

for some sort s′ ∈ S. We call ∼^{ζ} the final semantics relative to ∼^{κ} specified by RSP. We refer to ∼^{κ} as the kernel of ∼^{ζ}.

Example 3. The specification of example 1 can now be rephrased hierarchically:

spec AltSumList final relative to Int-op initial sorts list constructors ε : list, ⊣ : int × list → list defined oprs altsum : list → int axioms E_{AltSumList} : altsum(ε) = 0, altsum(x ⊣ ε) = x, altsum(x ⊣ (y ⊣ q)) = (x – y) + altsum(q)

The final semantics ∼^{ζ} on G_{AltSumList_{c}} relative to the initial semantics on G_{Int−op} is identical to ∼^{Q} of example 1. ^{}

Now, ∼^{Q}=∼^{ζ} is not true in general, but the identity does hold under certain sound conditions and consistency. We will return to this issue after introducing relative semantics in fuller depth.

The relation ∼^{ζ} in definition 7 is not necessarily a congruence. It is always symmetric and satisfies the congruence principle, but reflexivity and transitivity may be not satisfied: Let ∼^{κ} be the identity congruence on G_{{a,b}} for constants a, b. Let E = {a = b}. We then have a ↔_{E}^{∗} a ≁^{κ} b ↔_{E}^{∗} a, so a ≁^{ζ} a. To demonstrate lack of transitivity, let ∼^{κ} on G_{{a,b,c,d}} be such that a ≁^{κ} b, c ∼^{κ} d and d ∼^{κ} e. Let E = {f(c) = a, f(e) = b}. Then we have

f(c) ↔_{E}^{∗} a ≁^{κ} b ↔_{E}^{∗} f(e), giving c ≁^{ζ} e, in spite of c ∼^{ζ} d and d ∼^{ζ} e.

Hence, this relation is strictly speaking not worthy of being called a semantics. However it is reasonable to impose the following restrictions on definition 7:

KC: E is kernel conservative: ↔_{E}^{∗} _{G_{Σ^{κ}}} ⊆ ∼^{κ}

SC: E is sufficiently complete w.r.t. Σ_{c}^{κ}.

KC asserts that all equalities on Σ^{κ}-terms explicitly entailed by E are (already) specified by SP^{κ}. This technically resembles the notion of ‘hierarchy conservative’ in [WPP^{+}83], the difference being again that here E does not (necessarily) contain the equations of SP^{κ}. SC’s reference to sufficient completeness w.r.t. the constructors of Σ^{κ} is a slight generalisation of the notion in definition 1, also extended naturally to many-sorted situations. Regarding ∼^{κ} as constructor semantics, focusing on constructive function specification would require that SC is fulfilled.

Theorem 1. Given KC and SC, the relation ∼^{ζ} in definition 7 is a congruence.

Now we state a result of finality for ∼^{ζ} defined above as we did in the previous section for ∼^{Q}. The following lemmas are easily proven:

Lemma 2. g ≁^{κ} g′ ⇒ g ≁^{ζ} g′: all inequalities in ∼^{κ} are preserved in ∼^{ζ}.

Lemma 3. Assume KC and SC. Then G_{Σ}/∼^{ζ} ∈ Mod_{Σ}(E)

And then we have:

Theorem 4. Assume KC and SC. Then G_{Σ}/∼^{ζ} is final in ⌈∼^{κ}⌉_{Σ^{κ}} ∩ ⌊↔_{E}^{∗}⌋_{Σ}.

Proof: By lemma 2 G_{Σ}/∼^{ζ} is in ⌈∼^{κ}⌉_{Σ^{κ}}. By lemma 3 G_{Σ}/∼^{ζ} is in ⌊↔_{E}^{∗}⌋_{Σ}. Now, suppose

g ≁^{ζ} g′ for some g, g′ ∈ G_{Σ}, i.e. c[g] ↔_{E}^{∗} g_{1} ≁^{κ} g_{2} ↔_{E}^{∗} c[g′] for some c ∈ G_{Σ}, g_{1}, g_{2} ∈ G_{Σ^{κ}}.

Consider any A ∈ ⌈∼^{κ}⌉_{Σ^{κ}} ∩ ⌊↔_{E}^{∗}⌋_{Σ}, and assume A ⊧ g = g′. Since A ∈ ⌊↔_{E}^{∗}⌋_{Σ}, we have A ⊧ c[g] = g_{1} and A ⊧ c[g′] = g_{2}. But then A ⊧ g_{1} = g_{2} contradicting A ∈ ⌈∼^{κ}⌉_{Σ}. So A |̸= g = g′, and the theorem follows by fact 1. □

This result shows that this semantics does indeed match our intention: G_{Σ}/∼^{ζ} is the least computational model of E satisfying the inequations in ∼^{κ}, meaning that ∼^{ζ} is the congruence on G_{Σ} inducing two terms as semantically equal unless their inequality follows with necessity from principle (1) using E and ∼^{κ}.

We now generalise initial semantics to relative initial semantics.

Definition 8. Let RSP = ⟨SP, SP^{κ}⟩ with SP = ⟨Σ, E⟩ and biased SP^{κ} = ⟨Σ^{κ}, E^{κ}⟩ be a relative specification, such that ∼^{κ} on G_{Σ^{κ}} is the semantics specified by SP^{κ}. Consider the rewrite relation ℜ on G_{Σ} such that for all g, g′ ∈ G_{Σ}

g ℜ g′ ⇔ \{ \begin{matrix}g ↔_{E} g′ or \\ ∃g_{1}, g_{2} ∈ G_{Σ^{κ}}; c ∈ G_{Σ} | g = c[g_{1}], g′ = c[g_{2}], g_{1} ∼^{κ} g_{2} \end{matrix}

Define ∼^{α} on G_{Σ} by ∼^{α}= ℜ^{∗} We call ∼^{α} the initial semantics relative to ∼^{κ} specified by RSP. We refer to ∼^{κ} as the kernel of ∼^{α}.

The relation ∼^{α} in definition 8 is clearly a congruence. The case Σ^{κ} =∼^{κ}= ∅ and the case ∼^{κ}= ↔_{E}^{∗}_{G_{Σ^{κ}}} yield the initial semantics as defined in definition 4.

The way relative initial specification will be utilised in our examples is by giving semantics to constructors by way of a kernel and letting the axioms E give semantics to defined operators.

Example 4. We add a concatenation operator to AltSumList:

spec AltSumList_{op} initial relative to AltSumList final defined oprs ⊢⊣ : list × list → list axioms E_{AltSumList_{op}} : \begin{matrix}ε ⊢⊣ r = ε, \\ (x ⊣ q) ⊢⊣ r = x ⊣ (q ⊢⊣ r) \end{matrix}

Example 5. The specification Int_{op} from example 1 can be rephrased thus:

spec Int_{op} initial relative to Int initial sorts int defined oprs +, – : int × int → int axioms x+0 = x, x – 0 = x, x+succ(y) = succ(x+y), x–succ(y) = pred(x–y), x+pred(y) = pred(x+y), x–pred(y) = succ(x–y)

spec Int initial sorts int constructors 0 : int, succ, pred : int → int axioms succ(pred(x)) = x, pred(succ(x)) = x

In both initial and final generalisations the kernel may be final, initial, or even of some other bias or mode (see section 7). This accommodates the use of different strategies for defining equality over constructor terms. We have the initial dual of lemma 2:

Lemma 5. g ∼^{κ} g′ ⇒ g ∼^{α} g′, i.e. all equalities in ∼^{κ} are preserved in ∼^{α}.

And then it is straight forward to show:

Theorem 6. The quotient G_{Σ}/∼^{α} is initial in ⌊↔_{E}^{∗}⌋_{Σ} ∩ ⌊∼^{κ}⌋_{Σ}.

So relative initial semantics specifies terms as semantically unequal unless their equality follows with necessity from E in conjunction with ∼^{κ}.

4.2 Relative Consistency

The postulate that a mathematical proposition cannot simultaneously be true and false is mirrored in predicate calculus by referring to a set of axioms as inconsistent when the predicate true = false is deducible from the axioms. In a generalised view, consistency is related to basic understandings of the semantic domain which are expressed as requirements to the involved axioms and calculus. Guttag’s notion of consistency in definition 2 thus presupposes the semantics of constructors specified by the designated set E_{c}, calling the whole set E inconsistent if E breaches these semantics. This act of viewing consistency always relatively to such presuppositions is made explicit by a notion of consistency in relative specification relative to the kernel specification.

Definition 9. A relative specification RSP is initially kernel preserving relative to ∼^{κ} if

∼^{κ} = ∼_{G_{Σ^{κ}}}^{α}

where ∼^{α} is the initial semantics specified by RSP relative to ∼^{κ}.

The definition of consistency in [Gut77] is the special case of definition 9 where ∼^{κ} is a congruence on constructors specified base initially by some E_{c} ⊆ E.

Definition 10. A relative specification RSP is finally kernel preserving relative to ∼^{κ} if

∼_{G_{Σ^{κ}}}^{ζ} = ∼^{κ}

where ∼^{ζ} is the final semantics specified by RSP relative to ∼^{κ}.

Failure of kernel preservation will be called kernel corruption.

In the final case, several other notions related to consistency are feasible. It is for example natural to identify a signature Σ_{o} ⊆ Σ of designated observers meant to specify final semantics by principle (1). Final inconsistency w.r.t. Σ_{o} would then mean there are defined operators in Σ \ Σ_{o} whose specification in E gives further inequalities by principle (1) than intended. This is dealt with in [Han97].

A defined operator whose specification gives kernel corruption w.r.t. some presupposed semantics ∼^{κ} on constructors cannot be interpreted as a function in any algebra containing G_{Σ^{κ}}/∼^{κ} as a sub-algebra. In this manner the notion of relative consistency generalises the notion of consistency in predicate logic which is equivalent to the nonexistence of any model for any inconsistent set of predicates. In predicate logic, the predefined semantics on {true,false} is true≠false. In relative equational semantics, the kernel plays the role of predefined semantics.

However, note that a relative specification does have a model even if the specification is kernel corrupting. In order to investigate notions of consistency it is essential that there are semantics to be discussed in the event of inconsistency as well. This is safe as long as the semantics of an inconsistent specification bears witness of the inconsistency. Relative semantics supports this by its explicit kernel.

5 Modularity under Consistency

A crucial assumption of modular programming is the context independency of modules, in the sense that properties of submodules should be unaffected by their use in some larger context. In algebraic specification this is mirrored by the notion of ‘conservative extension’. Algebras characterised by complex specifications should have models of the constituent subspecifications as (intact) sub-algebras. Such algebras are dubbed “hierarchical models” in [WPP^{+}83]. The analogue for relative specification are initial or final models which have the model of the kernel specification G_{Σ^{κ}}/∼^{κ} as a sub-algebra. This end is fulfilled by kernel preservation (two analogues, and analogues only, in [WPP^{+}83] being ‘hierarchyconservativeness’ and ‘hierarchy-faithfulness’).

This section investigates kernel preservation and modularity in some depth, resulting in the partial equivalence of generalised initial and final semantics.

5.1 Kernel Preservation

We start by showing the coincidence of initial and final kernel preservation.

Theorem 7. Assume SC. Let RSP be a relative specification whose biased kernel has semantics ∼^{κ}. We have relatively to ∼^{κ}, that RSP is finally kernel preserving if and only if RSP is initially kernel preserving.

Before proving this we make a few observations. The result is independent of KC, but note that the assumption of KC excludes a particularly blatant cause of kernel corruption different from the type caused by principle (1) on page 8.

Example 6. Consider the following specification:

spec CorruptInt1 initial relative to Int initial sorts int defined oprs f : int → int

axioms \begin{matrix}f(0) = 0, \\ f(0) = succ(0) \end{matrix}

or even:

spec CorruptInt2 initial relative to Int initial sorts int axioms 0 = succ(0)

Both specifications give initial-semantically succ(0) ∼^{α} 0. The assumption of KC rules out such specifications as CorruptInt and CorruptInt2. ^{} Note also that the coincidence in theorem 7 cannot be shown simply by establishing ∼_{G_{Σ^{κ}}}^{ζ} = ∼_{G_{Σ^{κ}}}^{α}, because initial and final corrupted kernel semantics do not coincide. This fact is the counterpart of lemmas 5 and 2. Final kernel corruption means

∼_{G_{Σ^{κ}}}^{ζ} ⊂ ∼^{κ}

whereas initial kernel corruption amounts to

∼^{κ} ⊂ ∼_{G_{Σ^{κ}}}^{α}

The two forms of kernel corruption are duals of each other—initial kernel corruption collapsing the kernel’s congruence classes, and final kernel corruption composing new ones.

Example 7. Consider the specification

spec CorruptInt3

relative to Int initial sorts int defined oprs f : int → int axioms f(0) = 0, f(succ(x)) = succ(f(x)), f(pred(x)) = f(x)

Relative to the initial semantics given by Int, the specification CorruptInt3 is both initially and finally kernel corrupting. Initially we have succ(0) ∼^{α} 0 and final-semantically we have succ(pred(0)) ≁^{ζ} 0. The relations ∼^{α} and ∼^{ζ} are not identical. We have succ(0) ≁^{ζ} 0, and also succ(pred(0)) ∼^{α} 0. ^{}

Now for the proof:

Proof of Lemma 7: Let ∼^{α} be the initial semantics relative to ∼^{κ}.

Assume RSP is not finally kernel preserving relative to ∼^{κ}. By lemma 2 there must exist c ∈ G_{Σ} and g_{κ}, g′_{κ}, g_{1}, g_{2} ∈ G_{Σ^{κ}} such that

c[g_{κ}] ↔_{E}^{∗} g_{1} ≁^{κ} g_{2} ↔_{E}^{∗} c[g′_{κ}] but g_{κ} ∼^{κ} g′_{κ}

Since g_{κ} ∼^{κ} g′_{κ} we have g_{κ} ∼^{α} g′_{κ} by lemma 5, giving c[g_{κ}] ∼^{α} c[g′_{κ}]. Since c[g_{κ}] ↔_{E}^{∗} g_{1} and g_{2} ↔_{E}^{∗} c[g′_{κ}], we then get g_{1} ∼^{α} g_{2}. But g_{1} ≁^{κ} g_{2}, so E cannot be initially kernel preserving relative to ∼^{κ}.

For the converse implication, suppose first that KC does not hold. Then there are g_{κ}, g′_{κ} ∈ G_{Σ^{κ}} such that

g_{κ} ↔_{E}^{∗} g′_{κ} but g_{κ} ≁^{κ} g′_{κ}

But then we have g_{κ} ≁^{κ} g′_{κ} ↔_{E}^{∗} g_{κ}, and E is trivially finally kernel corrupting.

So, assume KC. Suppose RSP is initially kernel corrupting relative to ∼^{κ}. By lemma 5 there are g_{κ}, g′_{κ} ∈ G_{Σ^{κ}} such that

g_{κ} ∼^{α} g′_{κ} but g_{κ} ≁^{κ} g′_{κ}

We now define

g ↔_{κ} g′ ⇔ \{ \begin{matrix}g↮_{E}^{∗} g′ and \\ ∃c ∈ G_{Σ}; g_{1}, g_{2} ∈ G_{Σ^{κ}} | g = c[g_{1}], g′ = c[g_{2}], g_{1} ∼^{κ} g_{2} \end{matrix}

Consider an arbitrary ∼^{α}-derivation ⟨g_{κ}, …, g′_{κ}⟩ in G_{Σ}. By KC we must have g_{κ} ↮_{E}^{∗} g′_{κ}, so there must be at least one ↔_{κ} -step in the derivation, and since g_{κ} ≁^{κ} g′_{κ}, there must also be at least one ↔_{E} -step in the derivation. We may assume that this latter step is such that g ↔_{E} g′ where at least one of g, g′ is not in G_{Σ^{κ}}; otherwise this step would by KC be a ↔_{κ} -step. There is, then, a term g ∉ G_{Σ^{κ}} in the derivation. But then there must exist two ↔_{E} -steps; since a ↔_{κ} -step cannot link a term in G_{Σ^{κ}} with a term not in G_{Σ^{κ}} (and g_{κ} ≠ g′_{κ}, since ∼^{κ} is reflexive). Both these two ↔_{E} -steps must be linking terms in G_{Σ^{κ}} with terms not in G_{Σ^{κ}}. The derivation must therefore be of the form:

g_{κ} ↔_{κ}^{∗} g_{κ}_{0} ↔_{E}^{+} c_{1}[g_{1}] ↔_{κ}^{∗} c_{1}[g′_{1}] ↔_{E}^{∗} ⋯

:

⋯ ↔_{E}^{∗} c_{k}[g_{k}] ↔_{κ}^{+} c_{k}[g′_{k}] ↔_{E}^{∗} c_{k+1}[g_{k+1}] ↔_{κ}^{+} c_{k+1}[g′_{k+1}] ↔_{E}^{∗} ⋯

:

⋯ ↔_{E}^{∗} c_{n}[g_{n}] ↔_{κ}^{∗} c_{n}[g′_{n}] ↔_{E}^{+} g_{κ}_{n} ↔_{κ}^{∗} g′_{κ}

for g_{κ}_{0}, g_{κ}_{n}, g_{i}, g′_{i} ∈ G_{Σ^{κ}} and c_{i} ∈ G_{Σ}; 1 ≤ i ≤ n. By SC we have

c_{i}[g′_{i}] ↔_{E}^{∗} g_{κ}_{i} ↔_{E}^{∗} c_{i+1}[g_{i+1}]

for some g_{κ}_{i} ∈ G_{Σ^{κ}}; 1 ≤ i ≤ n. Now, we cannot have g_{κ}_{0} ∼^{κ} ⋯ ∼^{κ} g_{κ}_{k} ∼^{κ} ⋯ ∼^{κ} g_{κ}_{n}, since this would entail g_{κ} ∼^{κ} g′_{κ}. Therefore there must exist a 0 ≤ l < n such that g_{κ}_{l} ≁^{κ} g_{κ}_{l+1}. But then we have

c_{l+1}[g_{l+1}] ↔_{E}^{∗} g_{κ}_{l} ≁^{κ} g_{κ}_{l+1} ↔_{E}^{∗} c_{l+1}[g′_{l+1}]

Since g_{l+1} ∼^{κ} g′_{l+1}, RSP is finally kernel corrupting relative to ∼^{κ}. □

Based on proposition 7, the relationship between final and initial kernel preservation under KC (and for the case ‘n = 1’ in the proof) is illustrated in figure 1.

Final kernel preservation is trivial relative to an identity kernel:

Observation 8. If a final semantics is a congruence and its kernel ∼^{κ} is an identity relation then lemma 2 gives final kernel preservation relative to ∼^{κ}.

Hence we get the following perhaps obvious corollary from proposition 7 and observation

\begin{aligned}g_{1} & c[g_{κ}] & c[g′_{κ}] & g_{2} & g_{1} & g_{2} & ∗ & E & ⟷_{κ}^{∗} & ∗ & E & ∗ & E & ∗ & E & ≁^{κ} \\ & & & (a) \\ c[g_{κ}] & c[g_{κ}] & c[g′_{κ}] & c[g′_{κ}] & g_{1} & g_{2} \\ ∗ & E & ⟷_{κ}^{∗} & ∗ & E & ∗ & E & ∗ & E & ≁^{κ} & (b) \end{aligned}

Figure 1: Duality. Kernel corruption from two points of view. Final and initial kernel preservation are under KC two manifestations of the same phenomenon. In (a) inconsistency declares itself as initial kernel corruption, in that g_{1} ≁^{κ} g_{2}, but g_{1} ∼^{α} g_{2}. In (b) inconsistency manifests itself in final kernel corruption, in that g_{κ} ≁^{ζ} g′_{κ}, but g_{κ} ∼^{κ} g′_{κ}.

Corollary 9. Assume SC. If the final semantics is a congruence and its kernel ∼^{κ} is the identity relation then we also have initial kernel preservation relative to ∼^{κ}.

That is, a specification cannot corrupt a kernel without the kernel providing a situation where the term-universe is in a many-to-one correspondence with the semantic value space.

Although the matter is not pursued further here, the above results based upon sufficient completeness have interesting formulations as partial results corresponding to assumptions of partial sufficient completeness. Such partial results are interesting e.g. in connection with hidden sorts and symbols and also in connection with partial specifications.

5.2 Separability

Kernel preservation ensures conservativeness in a hierarchical sense. Relative semantics arise from two component semantics—the kernel and that given by some equation set E. Under KC and SC, kernel preservation also ensures the preservation of the semantics on all terms of kernel sorts, i.e. also the part specified by E. Consider the following relation:

(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗} [i.e. the reflexive-transitive closure of the union]  (2)

The closure under monotonicity (context application) of this relation is just the relative initial semantics of definition 8. However with monotonicity stripped away, there is no “interaction” between the two components ∼^{κ} and ↔_{E}^{∗}_{G_{Σ}}. Intuitively then, under SC and KC, (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗} is separable, i.e. gives precisely the pure sum of the semantics of its two components. More precisely, it is straight-forward to prove the separability of (∼^{κ} ∪

↔_{E}^{∗}_{G_{Σ}})^{∗}:

Lemma 10. Assume SC and KC. For a congruence ∼^{κ} on G_{Σ^{κ}} and a set of equations E, we have

1. (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{G_{Σ^{κ}}}^{∗} = ∼^{κ} (preservation of ∼^{κ})

2. ↔_{E}^{∗}_{G_{Σ}} ⊆ (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗} (preservation of ↔_{E}^{∗}. Completeness)

3. g(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g_{κ} ⇒ g ↔_{E}^{∗} g′_{κ} (preservation of ↔_{E}^{∗}. Soundness 1) for any g ∈ G_{Σ} and g_{κ} ∈ G_{Σ^{κ}}, for some g′_{κ} ∈ G_{Σ^{κ}} such that g_{κ} ∼^{κ} g′_{κ}.

4. g(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′ ⇒ g ↔_{E}^{∗} g′ (preservation of ↔_{E}^{∗}. Soundness 2) for any g, g′ ∈ G_{Σ} of sorts not in Σ^{κ}.

Proof: 1 : Suppose (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{G_{Σ^{κ}}}^{∗} ≠ ∼^{κ}. Since it is evident that ∼^{κ}⊆ (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{G_{Σ^{κ}}}^{∗}, there must exist g_{κ}, g′_{κ} ∈ G_{Σ^{κ}} such that g_{κ} ≁^{κ} g′_{κ}, in spite of g_{κ}(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′_{κ}. But then we must have

g_{κ} ∼^{κ} g_{1} ↔_{E}^{∗} g′_{1} ∼^{κ} g_{2} ↔_{E}^{∗} g′_{2} ∼^{κ} ⋯ ∼^{κ} g_{i} ↔_{E}^{∗} g′_{i} ∼^{κ} ⋯ ∼^{κ} g_{n} ↔_{E}^{∗} g′_{n} ∼^{κ} g′_{κ}

for some g_{i}, g′_{i} ∈ G_{Σ^{κ}}; 1 ≤ i ≤ n. By KC g_{i} ∼^{κ} g′_{i} for every 1 ≤ i ≤ n, and then g_{κ} ∼^{κ} g′_{κ}, which is a contradiction.

2 : Obvious.

3 : Suppose g(∼^{κ} ∪↔_{E}^{∗}_{G_{Σ}})^{∗}g_{κ} for some g ∈ G_{Σ}, g_{κ} ∈ G_{Σ^{κ}}. Observe that g must be of the same sort as g_{κ}. By SC we then have g ↔_{E}^{∗} g′_{κ} for a g′_{κ} ∈ G_{Σ^{κ}}. Then

g_{κ}(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g ↔_{E}^{∗} g′_{κ}

i.e. g_{κ}(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′_{κ}. And then (1) gives g_{κ} ∼^{κ} g′_{κ}.

4 : Suppose g(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′ for some g, g′ ∈ G_{Σ}. Observe that g must be of the same sort as g′, and that every component in any (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}-derivation ⟨g, …, g′⟩ is of the same sort as g, g′.

Observe also that every (∼^{x} ∪↔_{E}^{∗}_{G_{Σ}})^{∗}-derivation step has the form g_{i} = g_{x} ∼^{κ} g′_{x} = g_{i+1},

for g_{κ}, g′_{κ} ∈ G_{Σ^{κ}}; or the form g_{i} ↔_{E} g_{i+1} (for g_{i}, g_{i+1} ∈ G_{Σ}).

Let S^{κ} denote the set of sorts of terms occurring in G_{Σ^{κ}}. Suppose g, g′ are not of any type in S^{κ}. But then we cannot have g_{i} ∼^{κ} g_{i+1} for any components g_{i}, g_{i+1} in any (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}-derivation ⟨g, …, g′⟩. Consequently g ↔_{E}^{∗} g′, and the theorem follows. □

Now we may use (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗} to show that initial and final semantics are separable in kernel sorts under kernel preservation; i.e. the components of relative semantics in kernel sorts are untouched. The following two theorems are easily proven:

Theorem 11. Assume KC and SC. Let RSP = ⟨SP, SP^{κ}⟩ be a relative specification with SP = ⟨Σ, E⟩ and biased SP^{κ} = ⟨Σ^{κ}, E^{κ}⟩, such that ∼^{κ} on G_{Σ^{κ}} is the semantics specified by SP^{κ}. Then for S^{κ} the sorts in Σ^{κ} we have:

(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} = ∼_{S^{κ}}^{α}

⇕ RSP is initially kernel preserving relative to ∼^{κ}

Proof: If RSP is initially kernel corrupting relative to ∼^{κ} then (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} ≠ ∼_{S^{κ}}^{α} by proposition 10(1).

So, assume initial kernel preservation. Clearly (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} ⊆ ∼_{S^{κ}}^{α}, so we concentrate on showing (∼^{κ}∪↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} ⊇ ∼_{S^{κ}}^{α}. We induce on the length n of an arbitrary ∼_{S^{κ}}^{α}-derivation ⟨g, …, g′⟩ in G_{Σ} for g, g′ ∈ G_{Σ}_{S^{κ}}:

n = 1: Trivially g(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g.

n = k + 1; k ≥ 1: We then have a derivation ⟨g, …, g_{k}, g′⟩. Since g, g_{k} must be of a sort in S^{κ}, the induction hypothesis gives g(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g_{k}. Suppose g_{k} ↔_{E} g′. Then g_{k}(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′ and the theorem follows. Suppose g_{k} = c[g′_{k}] and c[g′′] = g′ and g′_{k} ∼^{κ} g′′, for some g′_{k}, g′′ ∈ G_{Σ^{κ}}. Since c[g′_{k}] and c[g′′] are of some sort in S^{κ}, SC gives c[g′_{k}] ↔_{E}^{∗} g_{κ} and c[g′′] ↔_{E}^{∗} g′_{κ} for some g_{κ}, g′_{κ} ∈ G_{Σ^{κ}}. Assuming initial kernel preservation or the equivalent notion of final kernel preservation (proposition 7) we have

¬∃c′ ∈ G_{Σ}; g_{1}, g_{2} ∈ G_{Σ^{κ}} | c′[g′_{k}] ↔_{E}^{∗} g_{1} ≁^{κ} g_{2} ↔_{E}^{∗} c′[g′′]

But then g_{k} = c[g′_{k}] ↔_{E}^{∗} g_{κ} ∼^{κ} g′_{κ} ↔_{E}^{∗} c[g′′] = g′, i.e. g_{k}(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′. □

Theorem 12. Assume KC and SC. Let RSP = ⟨SP, SP^{κ}⟩ be a relative specification with SP = ⟨Σ, E⟩ and biased SP^{κ} = ⟨Σ^{κ}, E^{κ}⟩, such that ∼^{κ} on G_{Σ^{κ}} is the semantics specified by SP^{κ}. Then for S^{κ} the sorts in Σ^{κ} we have:

(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} = ∼_{S^{κ}}^{ζ}

⇕ RSP is finally kernel preserving relative to ∼^{κ}

Proof: If RSP is finally kernel corrupting relatively to ∼^{κ} then (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} ≠ ∼_{S^{κ}}^{ω} by proposition 10(1).

Assume final kernel preservation. Suppose g(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′ for arbitrary g, g′ ∈ G_{Σ}_{S^{κ}}. We show g∼^{ω}g′ by induction on the length n of an arbitrary (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗}-derivation ⟨g, …, g′⟩.

n = 1: By KC and SC and fact 1 ∼^{ω} is reflexive, so g ∼^{ω} g.

n = k + 1; k ≥ 1: We then have a derivation ⟨g, …, g_{k}, g′⟩. Since g, g_{k} must be of a sort in S^{κ}, the induction hypothesis gives g∼^{ω}g_{k}. Any (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}-derivation step has

the form g_{i} = g_{κ} ∼^{κ} g′_{κ} = g_{i+1}, for g_{κ}, g′_{κ} ∈ G_{Σ^{κ}}; or the form g_{i} ↔_{E} g_{i+1} (for g_{i}, g_{i+1} ∈ G_{Σ}_{S^{κ}}).

Suppose g_{k} = g_{κ} ∼^{κ} g′_{κ} = g′ for g_{κ}, g′_{κ} ∈ G_{Σ^{κ}}: Since SP is finally kernel preserving we have g_{k} = g_{κ}∼_{S^{κ}}^{ω}g′_{κ} = g′, and the theorem follows. Suppose g_{k} ↔_{E} g′: By lemma 3 g_{k} ∼^{ω} g′ and since g, g_{k} are of some sort in S^{κ}, we get g_{k}∼^{ω}g′.

Now suppose g∼^{ω}g′ for arbitrary g, g′ ∈ G_{Σ}_{S^{κ}}. By SC we have g ↔_{E}^{∗} g_{κ} and g′ ↔_{E}^{∗} g′_{κ} for g_{κ}, g′_{κ} ∈ G_{Σ^{κ}}. Since g ∼^{ω} g′, we have

¬∃c ∈ G_{Σ}; g_{1}, g_{2} ∈ G_{Σ^{κ}} | c[g] ↔_{E}^{∗} g_{1} ≁^{κ} g_{2} ↔_{E}^{∗} c[g′]

In particular we have g ↔_{E}^{∗} g_{κ} ∼^{κ} g′_{κ} ↔_{E}^{∗} g′ thus giving g(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′. □

Finally, we get the following essential property as a corollary of theorems 11 and 12:

Theorem 13. Assume KC and SC. Under kernel preservation we have that initial and final semantics coincide in kernel sorts:

∼_{S^{κ}}^{α} = ∼_{S^{κ}}^{ζ}

Before ending this section let us return briefly to the non-relative final semantics of definition 5. The analogue of this corollary for a standard non-relative specification SP = ⟨Σ, E⟩, is that for E convergent and sufficiently complete

∼_{S^{κ}}^{Q} = ↔_{E}^{∗} _{S^{κ}}

where S^{κ} denotes designated initial sorts [Lys92]. This holds regardless of inconsistency. This is roughly because in a monolithic definition such as definition 5, at finality the implicit “kernel” is corrupted in the initial direction (see fig. 1) before the mechanism of extracting inequalities sets in. In contrast, the relative definition corrupts the kernel in the process of extracting inequalities, hence corrupting the kernel in the final direction. In the relative case, inconsistency reveals itself in the exact symmetrical duals of kernel corruption. So on a higher level, proposition 7 and theorem 13 give the equivalence of initial and final semantics on kernel sorts, also for relative semantics.

Under kernel preservation/consistency one can show ∼^{Q} = ∼^{ζ} (where the kernel of ∼^{ζ} is the implicit ↔_{Ec}^{∗} _{G_{Σc}}), by using the separable relation ( ↔_{Ec}^{∗} _{G_{Σc}} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}.

5.3 Inconsistency revealed as referential opacity

According to proposition 10(1) it may seem that the relation (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗} is in a sense insensitive to inconsistency. However, even though (∼^{κ} ∪ ↔_{E}^{∗} _{G_{Σ}})^{∗} always preserves its components, inconsistency now reveals itself through other symptoms; namely lack of monotonicity under context application, in other words (∼^{κ} ∪↔_{E}^{∗}_{G_{Σ}})^{∗} becomes referentially opaque.

Theorem 14. Assume KC and SC. Let ∼^{ζ} be the final semantics specified by a relative biased specification RSP relative to ∼^{κ} on G_{Σ^{κ}}. We then have for S^{κ} the sorts in Σ^{κ}:

RSP is finally kernel corrupting relative to ∼^{κ} ⇕

(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} is not monotone w.r.t. context application

Proof: Suppose RSP is finally kernel corrupting. By observation 2 there must be c ∈ G_{Σ} and g_{κ}, g′_{κ}, g_{1}, g_{2} ∈ G_{Σ^{κ}} such that

c[g_{κ}] ↔_{E}^{∗} g_{1} ≁^{κ} g_{2} ↔_{E}^{∗} c[g′_{κ}] but g_{κ} ∼^{κ} g′_{κ}

Since g_{κ} ∼^{κ} g′_{κ} proposition 10(1) gives g_{κ}(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′_{κ}. Now, suppose

c[g_{κ}](∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}c[g′_{κ}]

It cannot be the case that c[g_{κ}] ↔_{E}^{∗} c[g′_{κ}] since this would give g_{1} ↔_{E}^{∗} g_{2} which contradicts KC. Any (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}-derivation ⟨c[g_{κ}], …, c[g′_{κ}]⟩ in G_{Σ} must therefore have the form

\begin{matrix}c[g_{κ}] ↔_{E}^{∗} g_{κ}_{1} ∼^{κ} g_{κ}′_{1} ↔_{E}^{∗} g_{κ}_{2} ∼^{κ} g_{κ}′_{2} ↔_{E}^{∗} ⋯ \\ : \\ ⋯ ↔_{E}^{∗} g_{κ}_{i} ∼^{κ} g_{κ}′_{i} ↔_{E}^{∗} ⋯ \\ : \\ ⋯ ↔_{E}^{∗} g_{κ}_{n} ∼^{κ} g_{κ}′_{n} ↔_{E}^{∗} c[g′_{κ}] \end{matrix}  (3)

for n ≥ 2 and g_{κ}_{i}, g_{κ}′_{i} ∈ G_{Σ^{κ}}; 1 ≤ i ≤ n. By KC g_{κ}′_{i} ∼^{κ} g_{κ}_{i+1} for 1 ≤ i ≤ n. But since g_{1} ↔_{E}^{∗} c[g_{κ}] and c[g′_{κ}] ↔_{E}^{∗} g_{2} we get g_{1} ∼^{κ} g_{2} which is a contradiction. Consequently, and since c[g_{κ}], c[g′_{κ}] must be of type S^{κ}, c[g_{κ}](∼^{κ} ∪̸ ↔_{E}^{∗} _{G_{Σ}})_{S^{κ}}^{∗}c[g′_{κ}], so (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} is not monotone w.r.t. context application.

Conversely, suppose that g(∼^{κ} ∪↔_{E}^{∗}_{G_{Σ}})^{∗}g′ but c[g](∼^{κ} ∪̸↔_{E}^{∗}_{G_{Σ}})^{∗}c[g′] for some c[g], c[g′] ∈

G_{Σ}_{S^{κ}}. By SC we have g ↔_{E}^{∗} g_{κ} and g′ ↔_{E}^{∗} g′_{κ} for g_{κ}, g′_{κ} ∈ G_{Σ^{κ}}. Hence, g_{κ}(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}g′_{κ} and

by proposition 10(1)

g_{κ} ∼^{κ} g′_{κ}

By SC we also have c[g]↔_{E}^{∗}g_{1} and c[g′]↔_{E}^{∗}g_{2} for g_{1}, g_{2} ∈ G_{Σ^{κ}}. Now, we cannot have g_{1} ∼^{κ} g_{2}, because then c[g](∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}c[g′]. Accordingly,

c[g] ↔_{E}^{∗} g_{1} ≁^{κ} g_{2} ↔_{E}^{∗} c[g′]

and then also

c[g_{κ}] ↔_{E}^{∗} c[g] ↔_{E}^{∗} g_{1} ≁^{κ} g_{2} ↔_{E}^{∗} c[g′] ↔_{E}^{∗} c[g′_{κ}]

So, g_{x} ≁^{ω} g′_{x}, but g_{κ} ∼^{κ} g′_{κ}, thus RSP is finally kernel corrupting. □

And of course we have the dual by proposition 7:

Corollary 15. Assume KC and SC. Let ∼^{α} be the initial semantics specified by a biased relative specification RSP relative to ∼^{κ} on G_{Σ^{κ}}. We then have for S^{κ} the sorts in Σ^{κ}:

RSP is initially kernel corrupting relative to ∼^{κ} ⇕

(∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})_{S^{κ}}^{∗} is not monotone w.r.t. context application

Example 8. For the specification CorruptInt3 from example 7 we had initial-semantically f(succ(pred(0))) ∼^{α} succ(0) and f(0) ∼^{α} 0 giving initial kernel corruption by succ(0) ∼^{α} 0. Consider the associated relation (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗}. We have

succ(pred(0)) (∼^{κ} ∪ ↔_{E}^{∗}_{G_{Σ}})^{∗} 0,

but

f(succ(pred(0))) (∼^{κ} ∪̸↔_{E}^{∗}_{G_{Σ}})^{∗} f(0).

6 Proof by Kernel Preservation

The formalism of relative semantics can now be utilised to describe a modular hierarchical approach to proof by consistency, in which at each stage, only the uppermost equations in the hierarchy need be considered for completion. So, given a relative semantics ∼^{r} we pose the problem of determining whether G_{Σ}/∼^{r} ⊧ u = v for any given equation u = v (which is undecidable in general, of course). Although the following result is stated for standard completion and assumes orientability, it also holds for ordered completion assuming only orientability of ground instances. This is evident by examining the proof, since peak elimination is done w.r.t. ground-term derivations. It also holds for extended completion if all unorientable equations are in kernel terms, i.e. over T_{Σ^{κ}}(X).

Theorem 16. Let ∼^{ζ} be the final semantics specified by a relative biased specification RSP relative to ∼^{κ} on G_{Σ^{κ}} under assumption of KC and SC. Let H be a set of equational hypotheses. Suppose a completion sequence ⟨⟨E ∪ H, ∅⟩, …, ⟨E_{i}, R_{i}⟩, …⟩ is fair w.r.t. inferences and is s.t. every equation generated is orientable. Assume furthermore that every term in T_{Σ}(X) \ T_{Σ^{κ}}(X) is greater in the completion process’s term ordering than all terms in T_{Σ^{κ}}(X). Then:

G_{Σ}/∼^{ζ} |̸= H
⇕

an equation or rule ⟨l, r⟩ over T_{Σ^{κ}}(X) is generated during the process s.t. G_{Σ^{κ}}/∼^{κ} |̸= l = r Proof: Assume G_{Σ}/∼^{ζ} |̸= H, i.e. there is some u = v ∈ H, ground-instantiation τ and context c such that c[uτ] ↔_{E}^{∗} g_{1} ≁^{κ} g_{2} ↔_{E}^{∗} c[vτ]. But then, g_{1} ⟷_{E∪{u= v}}^{∗}g_{2}. Regarding completion processes as derivation transforming processes in the style of Bachmair [Bac91], any derivation ⟨g_{1}, …, g_{2}⟩ may be transformed into a derivation ⟨g_{1}, …, g_{2}⟩′ where every component is a term in G_{Σ^{κ}} (otherwise, by assumption of the term ordering, there would be peak in the derivation). This entails the generation of a set E_{j} ∪ R_{j} purely over T_{Σ^{κ}}(X) such that g_{1} ⟷_{E_{j} ∪R_{j}}^{∗} g_{2}. But then at least one of ⟨l, r⟩ ∈ E_{j} ∪ R_{j} must be s.t. G_{Σ^{κ}}/∼^{κ} |̸= l = r, or else g_{1} ∼^{κ} g_{2}, contradicting our assumption.

Conversely, assume an equation or rule ⟨l, r⟩ over T_{Σ^{κ}}(X) is generated during the process s.t. for some instantiation σ_{κ}, lσ_{κ} ≁^{κ} rσ_{κ}. By KC, lσ_{κ}↮_{E}^{∗} rσ_{κ}. Then, every E ∪H-derivation must be of the form

lσ_{κ} ↔_{E}^{∗} c_{1}[u_{1}σ_{1}], c_{1}[v_{1}σ_{1}] ↔_{E}^{∗} ⋯ ↔_{E}^{∗} c_{n}[u_{n}σ_{n}], c_{n}[v_{n}σ_{n}] ↔_{E}^{∗} rσ_{κ}

(or any u_{i}, v_{i}-symmetrical form), for ⟨u_{i}, v_{i}⟩ ∈ H; 1 ≤ i ≤ n. By SC, for every i there

are g_{i}, g′_{i} ∈ G_{Σ^{κ}} s.t. c_{i}[u_{i}σ_{i}] ↔_{E}^{∗} g_{i} and c_{i}[v_{i}σ_{i}] ↔_{E}^{∗} g′_{i}. There must be some 1 ≤ l ≤ n s.t.

g_{l} ≁^{κ} g′_{l}, or else lσ_{κ} ∼^{κ} rσ_{κ} (since lσ_{κ} ∼ g_{1}, g_{i} ∼ g_{i+1} and g′_{n} ∼ rσ_{κ} by KC). But then

c_{l}[u_{l}σ_{l}] ↔_{E}^{∗} g_{l} ≁^{κ} g′_{l} ↔_{E}^{∗} c_{l}[v_{l}σ_{l}], so u_{l}σ_{l} ≁^{ζ} v_{l}σ_{l}, hence G_{Σ}/∼^{ζ} |̸= H. □

According to theorem 16, equational hypotheses H_{0} may be resolved according to a relative hierarchical data-type G_{Σ}/∼^{r} composed of final modules, by running completion w.r.t. the top-level (n’th-level) equations E_{n} and extracting a set of new hypotheses H_{1} in kernel terms. These new hypotheses are in turn given to completion together with the level n − 1 equations E_{n−1}, and so on, until some atomic module is encountered, which if standard initial can be dealt with by standard methods. Note how reasoning about G_{Σ}/∼^{r} is done modularly w.r.t. current top-level equations only. This lightens the burden of having to consider for completion a large monolithic set of equations for the whole hierarchical data-type.

What about initial modules? Assuming that all relative initial modules only have kernel-sorts, corollary 13 states that under kernel preservation, initial modules may be treated as final. If kernel preservation is not guaranteed, then by duality, initial kernel corruption will manifest itself in final kernel corruption. Viewing any kernel corruption as simply a sign of wrongful specification, initial and final specification may be viewed as equivalent in kernel sorts, and theorem 16 applies.

Theorem 16 says that a kernel corrupting witness will reveal itself if and only if the set of hypotheses are not valid in the data-type. Hence, proof by kernel preservation is a generalised relative version of proof by consistency. By the equivalence in kernel sorts, this is also a generalised relative version of proof by consistency methods designated for standard initial semantics.

Example 9. Consider the following specification:

spec FlatTree final relative to AltSumList_{op} initial sorts tree constructors ϵ : tree, leaf : int → tree, node : tree × tree → tree defined oprs flatten : tree → list axioms E_{FlatTree} : flatten(ϵ) = 0, flatten(leaf(x)) = x ⊣ε, flatten(node(l,r)) = flatten(l) ⊢⊣ flatten(r)

The observer flatten should give final-semantically that two G_{FlatTree_{c}}-terms are semantically equal if and only if they represent trees which, when flattened (infix) give semantically equal sequences according to AltSumList_{op} initial. To check whether

h_{0}: node(node(leaf(x),leaf(y)),leaf(z)) = node(leaf(x),node(leaf(y),leaf(z)))

is valid in the relative datatype G_{FlatTree}/∼^{ζ} specified by FlatTree final, the set {h_{0}} ∪ E_{FlatTree} is subjected to completion with a term-ordering in which every term in T_{FlatTree}(X)\ T_{AltSumList_{op}}(X) is greater than all terms in T_{AltSumList_{op}}(X). This yields a single equation

h_{1}: ((x⊣ε) ⊢⊣ (y⊣ε)) ⊢⊣ (z⊣ε) = (x⊣ε) ⊢⊣ ((y⊣ε) ⊢⊣ (z⊣ε))

over T_{AltSumList_{op}}(X). Completion of {h_{1}} ∪ E_{AltSumList_{op}} does not yield any hypotheses over T_{AltSumList}(X), so according to theorem 16, h_{0} is valid in G_{FlatTree}/∼^{ζ}.

Completion of

h′_{0}: node(leaf(x),node(leaf(y),ϵ)) = node(ϵ,ϵ)

together with E_{FlatTree} yields the new hypothesis

h′_{1}: (x ⊣ ε) ⊢⊣ ((y ⊣ ε) ⊢⊣ ε) = ε ⊢⊣ ε

which completed with E_{AltSumList_{op}} yields

y ⊣ (x ⊣ (x ⊣ q)) = y ⊣ q

which completed with E_{AltSumList} produces

0 = x

which can be refuted as an inductive consequence of E_{Int_{op}} by standard methods. Hence h′_{1} is not valid in G_{FlatTree}/∼^{ζ}. ^{}

Theorem 16 also shows how one might discover kernel corruption. If the procedures refutes a hypothesis which is known to hold in the kernel, then the specification is not kernel preserving. Similar ideas occur in [Kir84].

7 Non-homogeneous hierarchies

In this section two sources of non-homogeneouity to a specification hierarchy are briefly sketched. The key point being that relative specification admits non-homogeneouity and supports different proof methods at each level. Auxiliary functions may give unintended semantics:

spec AltSumList’ final relative to Int_{op} initial sorts list constructors ε : list, ⊣ : int × list → list defined oprs altsum, alt1, alt2 : list → int axioms E_{AltSumList′} : altsum(q) = alt1(q), alt1(ε) = 0, alt2(ε) = 0, alt1(x ⊣ q) = x – alt2(q), alt2(x ⊣ q) = x + alt1(q)

The operators alt1 (handling the subtraction part) and alt2 (handling the additition part) are auxiliary to altsum, and the intended final semantics is that of AltSumList final of example 3. However, this specification is finally inconsistent w.r.t. Σ_{o} = {altsum}: Letting g = succ(0)⊣(succ(0)⊣(pred(0)⊣ε)) and g′ = pred(0)⊣ε, we have

alt2(g) ⟷_{E_{AltSumList′}}^{∗} succ(succ(succ(0))) ≁^{κ} pred(0) ⟷_{E_{AltSumList′}}^{∗} alt2(g′)

giving g ≁^{ζ} g′ (while altsum(g) ⟷_{E_{AltSumList′}}^{∗} pred(0) ⟷_{E_{AltSumList′}}^{∗} altsum(g′), so the only intended distinguisher altsum does not distinguish g and g′). It is possible to make private, or protect auxiliary operators from unauthorised external use, i.e. alt2 should only be accessed within the data-type by the main operator altsum, by restricting the monotonicity axiom in equational logic to allow context application of non-private symbols only. (A similar restriction is also applied for proving refinement of non-deterministic data-types in [QG93].) Proof by consistency may be adapted to this modified equational logic [Han97]. Relative semantics then cater firstly for the definition of semantics according to this modified logic, and secondly by supporting modified versions of proof by consistency at each level.

Another source of non-homogeneouity is the following: Due to un-orientability, no complete pure term-rewrite system exists for the characteristic equations for sets (of natural numbers) {add(add(s,x),x) = add(s,x), add(add(s,x),y) = add(add(s,y),x)}. However, it is possible to write a convergent specification of a function computing canonical representatives for the classes specified by the characteristic axioms, e.g. in the form of sorted non-repeating lists. So if E_{s} specifies a canonical representatives function crep, this gives rise to indirect specification of the form g ∼^{s} g′ ⇔ s(g)⟷_{Es}^{∗}s(g′), where s represents crep. The issue of convergence is crucial for rewrite related reasoning, and by specifying a function inducing a semantics, rather than the semantics itself directly, one may thus indirectly convergently specify semantics for which no direct convergent set of equations exist.

Now, s is not a symbol intended to represent a genuine function in a data-type. In the case of an indirectly specified module occurring in a larger context, one would not want to view the entire entity monolithically. Proof by consistency adapted to indirect semantics would have to be treated as a separate process, making monolithic completion unsuitable. Relative specification and semantics provide the formalism for incorporating this kind of incompatible specification as a module of a larger hierarchical specification.

In certain cases it is possible to reduce indirect semantics to final semantics, and also to initial semantics by introducing the equation s(x) = x. Proving this benefits greatly from formulation in the relative constructs.

8 Concluding Remarks

The notions of relative specification and semantics were presented in order to (1) make explicit the notion of a kernel in existing notions of initial and final semantics. This provides (2) a uniform view of initial and final semantics and dualised notions of consistency as kernel preservation, and also provides (3) a modular hierarchical generalisation of initial and final semantics admitting a corresponding modular hierarchical method of proof by consistency where at each level the kernel may be disregarded. This extends to the “meta-theory” also—results in this note are stated and proved disregarding details of the kernel. Making the kernel explicit in the formalisms also (4) permits non-homogeneous specification and semantics schemes, admitting diverse proof methods at each level of the hierarchy.

This work on extremal monomorphic semantics is a basic step: It lays a basis on which investigation into relative loose semantics may be done. Given a loose kernel semantics consisting of a class of congruences, there are several ways of defining a next relative layer. One option is to extend in a point-wise fashion and consider a class of monomorphic relative models as the next layer semantics. Each member of this class will be extremal in some class of their own so one might also consider the union of all these classes to be the relative loose semantics.

Much investigation has been invested into modularity and compositionality properties of rewrite systems [Ohl95]. The approach in this note tends to decomposition in the sense that only modular parts of an entire specification should be treated at a time. In particular, an analysis of the effects of running completion on parts of an equation set compared to those of completing the entire set, would seem interesting.

Acknowledgements

Thanks to Don Sannella and Olav Lysne for valuable comments, and to the makers of Re-DuX, Reinhard Bündgen and Jochen Walter. This research is sponsored by the Norwegian Research Council, grant no. 110904/41

References

[Bac87] L. Bachmair. Proof methods for equational theories. PhD thesis, University of Illinois, Urbana-Champaign, 1987.

[Bac88] L. Bachmair. Proof by consistency in equational theories. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK), pages 228– 233, 1988.

[Bac91] L. Bachmair. Canonical equational proofs. Computer Science Logic, Progress in Theoretical Computer Science. Birkhäuser Verlag AG, 1991.

[BHW94] M. Bidoit, R. Hennicker, and M. Wirsing. Behavioural and abstractor specifications. Res. Rep. 9414, Ludwig-Maximilians-Universität München, August 1994.

[Bur69] R. Burstall. Proving properties of programs by structural induction. Computer Journal, 12(1):41–48, 1969.

[DJ90] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6. Elsevier, 1990.

[DO91] O.-J. Dahl and O. Owe. Formal development with ABEL. Forskningsraport 552, Institutt for informatikk, Universitetet i Oslo, 1991.

[EM85] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications I, Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer, 1985.

[Fri86] L. Fribourg. A strong restriction on the inductive completion procedure. In Proceedings 13th International Colloquium on Automata, Languages and Programming, volume 226 of LNCS, pages 105–115. Springer, 1986.

[GHJ85] J.V. Guttag, J.J. Horning, and J.M.Wing. Larch in five easy pieces. Technical report, Digital Systems Research Center, 1985.

[Gog80] J.A. Goguen. How to prove inductive hypotheses without induction. In Proceedings 5th International Conference on Automated Deduction, volume 87 of LNCS, pages 356–373. Springer, 1980.

[Gor94] A. Gordon. A tutorial on co-induction and functional programming. In Proceedings 1994 Glasgow Workshop on Functional Programming, pages 78–95. Springer, 1994.

[Gut75] J.V. Guttag. The Specification and Application to Programming of Abstract Data Types. PhD thesis, Computer Science Department, University of Toronto, [Gut77] J.V. Guttag. Abstract datatypes and the development of data structures. Com-

munications of the ACM, 20(6):396–404, 1977.

[Han95] J.E. Hannay. Generalised algebraic specification with an application to indirect semantics. Cand. Scient. Thesis, Inst. for informatikk, Universitetet i Oslo, May 1995.

[Han97] J.E. Hannay. Proof by consistency for data-types with hidden operators.

Available by http://www.dcs.ed.ac.uk/home/joh/LogicHiding.ps, Janu-

ary 1997.

[Hen91] R. Hennicker. Context induction: A proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing, 3:326–345, 1991.

[Hen92] R. Hennicker. A semi-algorithm for algebraic implementation proofs. Theoretical Computer Science, 104:53–87, 1992.

[Her92] M. Hermann. On the relation between primitive recursion, schematization, and divergence. In Proceedings of the 3rd International Conference on Algebraic and Logic Programming, volume 632 of LNCS, pages 115–127. Springer, Sept. 1992.

[HH82] G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, pages 239–266, 1982.

[JK89] J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1–33, July 1989.

[Kam83] S. Kamin. Final data types and their specification. ACM Transactions on Programming Languages and Systems, 5(1):97–123, January 1983.

[KB70] D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, 1970.

[Kir84] H. Kirchner. A general inductive completion algorithm and application to abstract data types. In cade7, volume 170 of LNCS, pages 282–302. Springer, 1984.

[Klo92] J.W. Klop. Term rewriting systems. In S. Abramsky, D.M. Gabbai, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 1–116. Oxford University Press, 1992.

[Küc89] W. Küchlin. Inductive completion by ground proof transformation. In H. Aït-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2 of Rewriting Techniques, chapter 7. Academic Press, 1989.

[Les83] P. Lescanne. Behavioural categoricity of abstract data type specifications. The Computer Journal, 26(4):289–292, 1983.

[LPL96] H. Linnestad, C. Prehofer, and O. Lysne. Higher-order proof by consistency. In Proceedings 16th International Conference FSTTCS, India, volume 1180 of LNCS, pages 274–285, 1996.

[Lys92] O. Lysne. Proof by consistency in constructive systems with final algebra semantics. In Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa, volume 632 of LNCS, pages 276–290. Springer, 1992.

[Lys94] O. Lysne. Extending Bachmair’s method for proof by consistency to the final algebra. Information Processing Letters, 51:303–310, 1994.

[Mor94] C. Morgan. Programming from Specifications, 2nd ed. Prentice Hall International Series in Computer Science; C.A.R. Hoare, Series Editor. Prentice-Hall, UK, 1994.

[Mus80] D.L. Musser. On proving inductive properties in abstract data types. In Proceedings 7th Annual ACM Symposium on Principles of Programming Languages, pages 154–162, January 1980.

[Ohl95] E. Ohlebusch. Modular properties of composable term rewriting systems. Journal of Symbolic Computation, 20(1):1–41, 1995.

[Pad95] P. Padawitz. Swinging datatypes. In Recent Trends in Data Type Specification, Proceedings 11th workshop on Specification of Abstract Data types, volume 1130 of LNCS, pages 409–435, Oslo, September 1995. Springer.

[Pue84] L. Puel. Proof in the final algebra. In B. Courcelle, editor, Proceedings 9th Colloquium on Trees in Algebra and Programming, pages 227–242. Cambridge University Press, 1984.

[QG93] X. Qian and A. Goldberg. Referential opacity in nondeterministic data refinement. LoPLaS, 2, 1993.

[ST87] D. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences, 34:150–178, 1987.

[ST97] D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing, 1997. To appear. Avail-

able by http://www.dcs.ed.ac.uk/home/dts/alf/concepts.ps.

[Wir90] M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 13, pages 675–788. Elsevier, 1990.

[WPP^{+}83] M. Wirsing, P. Pepper, H. Partsch, W. Dosch, and M. Broy. On hierarchies of abstract data types. Acta Informatica, 20:1–33, 1983.