On behavioural abstraction and behavioural satisfaction in higher-order logic ⋆

Martin Hofmann^{1} and Donald Sannella^{2}

Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh EH9 3JZ, United Kingdom

Abstract

The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, which is due to Reichel and was recently generalized to the case of first-order logic by Bidoit et al, is further generalized to this case. The fact that higher-order logic is powerful enough to express the indistinguishability relation is used to characterize behavioural satisfaction in terms of ordinary satisfaction, and to develop new methods for reasoning about specifications under behavioural semantics.

1 Introduction

An important ingredient in the use of algebraic specifications to describe data abstractions is the concept of behavioural equivalence between algebras, which seems to appropriately capture the “black box” character of data abstractions, see e.g. [GGM76], [GM82], [ST87] and [ST95]. Roughly speaking (since there are different choices of definition), two algebras A, B over a signature Σ are behaviourally equivalent with respect to a distinguished set OBS of observable types if all computations that can be expressed using the functions in Σ and

⋆ A condensed version of this paper appeared in: Proc. 20th Colloq. on Trees in Algebra and Programming, Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Aarhus. Springer LNCS 915, 247–261 (1995). 1 E-mail mxh@dcs.ed.ac.uk. Supported by a Human Capital and Mobility fellowship, contract number ERBCHBICT930420. 2 E-mail dts@dcs.ed.ac.uk. Supported by an EPSRC Advanced Fellowship and EPSRC grants GR/H73103 and GR/J07303.

To appear in Theoretical Computer Science 23 July 1996

that yield a result of a type in OBS produce the same result in both A and B. (The set OBS is typically taken to include primitive types like Booleans and natural numbers.) A specification of a data abstraction should characterize a class of algebras that is closed under behavioural equivalence; otherwise it forbids some realizations that are indistinguishable from acceptable ones. Closure can be ensured by the specification framework (by making all specificationbuilding operations deliver closed classes, see e.g. [NO88]) or by the specifier (by applying a specification-building operation, sometimes known as behavioural abstraction, to form the closure, see e.g. [SW83], [ST87]). The term “behavioural semantics” is sometimes used to characterize approaches that take the need for behavioural closure into account. Behavioural abstraction seems to be an implicit ingredient of model-oriented approaches to specification such as VDM and Z, where a specification spells out one or more concrete models but any program that delivers the same results is regarded as an acceptable realization.

An unfortunate problem with behavioural semantics in general and the behavioural abstraction operation in particular is that it complicates the task of reasoning about specifications. For example, if a specification SP satisfies a formula φ then the behavioural abstraction of SP need not satisfy φ. Reasoning methods that are appropriate in the context of behavioural semantics have been developed, but these are either insufficiently powerful (e.g. [ST87], cf. Section 5 of [Sch92]) or tend to be too complicated for convenient use in practice (e.g. [Hen91], [Far92]). One avenue of attack on this problem is to consider the relationship between the class of algebras produced by applying the behavioural abstraction operation to a specification ⟨Σ, Φ⟩, and the class of algebras obtained by simply interpreting equality in the axioms Φ as indistinguishability rather than as identity. The latter approach, sometimes known as behavioural satisfaction, was pioneered by Reichel [Rei85] who showed that these two classes coincide when the axioms involved are conditional equations, provided that the conditions used are equations between terms of types in OBS. This yields a reasoning method for specifications involving behavioural abstraction: given a sound proof system for behavioural satisfaction, any consequence φ of a specification ⟨Σ, Φ⟩ that can be proved in that system will hold in the behavioural abstraction of ⟨Σ, Φ⟩, provided Φ and φ have the required form.

The usefulness of this reasoning method is limited by the fact that conditional equations are not powerful enough for convenient practical use in writing specifications (see e.g. [SW96]). But in a recent development, Bidoit et al have generalized Reichel’s result to the case of specifications with infinitary firstorder equational formulae as axioms, and to arbitrary relations of behavioural equivalence and indistinguishability. In [BHW95] they show that the coincidence of classes described above holds in this context as well, whenever the class of models of ⟨Σ, Φ⟩ (under ordinary satisfaction) is closed under quotienting with respect to indistinguishability of values, provided that indistinguishability is weakly regular and that behavioural equivalence is factorizable by indistinguishability. Subsequently, [BH95] and [BH96] use this characterization as the basis for reasoning methods.

In this paper we examine these issues for the case of (flat) specifications with higher-order logical formulae as axioms. Our first main contribution is a generalization^{3} of the framework and results of [BHW95]. Although it is not made explicit there, the main results in [BHW95] including the characterization theorem do not strongly depend on the form of axioms. The same result holds for any logical system for which behavioural satisfaction of a formula φ in A coincides with ordinary satisfaction of φ in the quotient of A w.r.t. indistinguishability and for which isomorphisms preserve and reflect satisfaction. In Sections 2 and 3 we give syntax and semantics for higher-order formulae and show that these properties hold for such formulae (Theorem 3.35 and Corollary 3.14 respectively). In Section 4 we formulate definitions of behavioural equivalence and indistinguishability, and we show that the former is factorizable by the latter (Theorem 5.21) and that indistinguishability is regular (Proposition 4.7) and hence weakly regular (Proposition 4.9). This leads directly to a characterization result analogous to the one in [BHW95] (Theorem 6.7). Although the generalization to higher-order logic results in certain complications, it also yields a simplification: since equality may be expressed directly in higher-order logic, it need not be given specialized treatment, and the rôle of equality in the context of behavioural semantics is revealed as a special case of something more general.

Higher-order logic provides sufficient power to express the indistinguishability relation as a predicate (Theorem 5.4, cf. [Sch94]). A second main contribution is the application of this fact to develop methods for reasoning about specifications under behavioural semantics. In Section 5 we characterize behavioural satisfaction in terms of ordinary satisfaction, by giving a translation that takes any formula φ to a “relativized” formula ⌜φ⌝ such that the latter is satisfied exactly when the former is behaviourally satisfied (Corollary 5.10). This translation plays an important rôle in the comparison of various alternative definitions of behavioural equivalence, differing in the set of “experiments” used to test algebras, which leads to the conclusion that the three definitions considered yield the same relation (Corollary 5.22). These results, together with the characterization theorem of Section 6, lead directly to various proof methods that are summarized in Section 7.

3 [BHW95] uses the infinitary logic L_{ω_{1}ω}, so strictly speaking our framework is not a generalization. The extension to infinitary logic is easy and raises no interesting issues, and it also seems gratuitous in the context of higher-order logic, so we omit it. Also, unlike [BHW95] we do not handle structured specifications, for reasons explained in Section 8.2.

2 The language of higher-order logic

The syntax of the typed variant of higher-order logic we will use is described below. The logic is higher-order because quantification over predicates (i.e. sets) is allowed in addition to the usual quantification over individuals. For the sake of simplicity, functions are not “first-class citizens”, so there is no quantification over function types or use of functions as arguments to predicates or functions, but see Section 8.1 for comments on a possible extension.

Definition 2.1 A signature Σ consists of a set B of base types and a set C of constants such that each c ∈ C has an arity n ≥ 0, an n-tuple of argument types b_{1}, …, b_{n} ∈ B and a result type b ∈ B, which we abbreviate c : b_{1} × ⋯ × b_{n} → b.

Let Σ = ⟨B, C⟩ be a signature.

Definition 2.2 The types over Σ are given by the following grammar:

τ ::= b | [τ_{1}, …, τ_{n}]

where b ∈ B and n ≥ 0. Types(Σ) denotes the set of all types over Σ.

A type of the form [τ_{1}, …, τ_{n}] may be regarded as the type of n-ary predicates taking arguments of types τ_{1}, …, τ_{n}. For example, is-even : [int], <: [int, int], has-property : [int, [int]], where is-even(3) does not hold but has-property(2, is-even) does. A more suggestive syntax for a type [τ_{1}, …, τ_{n}] might be τ_{1} × ⋯ × τ_{n} → Prop, where Prop is the type of propositions; in particular, the type [ ] may be thought of as Prop. However, since λ-abstraction can be used to form predicates but not ordinary functions (see below), we need to distinguish between the arrow used to write the types of constants and the arrow in τ_{1} × ⋯ × τ_{n} → Prop.

Let X be a fixed infinite set of variables, ranged over by x.

Definition 2.3 The terms over Σ are given by the following grammar:

t ::= x | c(t_{1}, …, t_{n}) | λ(x_{1}:τ_{1}, …, x_{n}:τ_{n}).t | t(t_{1}, …, t_{n}) | t ⇒ t′ | ∀x:τ.t

where c ∈ C and n ≥ 0. Parentheses may be used for grouping as usual; in the absence of parentheses, ⇒ associates to the right. As usual, we regard α-convertible terms as equal, where the binding constructs are λ and ∀. We write c as an abbreviation for c() when c : → b, and ∀x_{1}, …, x_{n}:τ.t as an abbreviation for ∀x_{1}:τ. · · · .∀x_{n}:τ.t.

\overline{Γ ⊢ x : Γ(x)}  (var)
\frac{Γ, x_{1} : τ_{1}, …, x_{n} : τ_{n} ⊢ t : [ ]}{Γ ⊢ λ(x_{1}:τ_{1}, …, x_{n}:τ_{n}).t : [τ_{1}, …, τ_{n}]}  (λ)
\frac{c : b_{1} × ⋯ × b_{n} → b Γ ⊢ t_{1} : b_{1} ⋯ Γ ⊢ t_{n} : b_{n}}{Γ ⊢ c(t_{1}, …, t_{n}) : b}  (fun)
\frac{Γ ⊢ t : [τ_{1}, …, τ_{n}] Γ ⊢ t_{1} : τ_{1} ⋯ Γ ⊢ t_{n} : τ_{n}}{Γ ⊢ t(t_{1}, …, t_{n}) : [ ]}  (pred)
\frac{Γ ⊢ t : [ ] Γ ⊢ t′ : [ ]}{Γ ⊢ t ⇒ t′ : [ ]}  (⇒)
\frac{Γ, x : τ ⊢ t : [ ]}{Γ ⊢ ∀x:τ.t : [ ]}  (∀)

Fig. 1. Typing rules

Function application (written c(t_{1}, …, t_{n})) is distinguished from predicate application (written t(t_{1}, …, t_{n})) although both notations are similar. λ-abstraction is for forming predicates; implication (⇒) and universal quantification are for forming propositions. There is just one syntax class for terms: terms that denote individuals (e.g. +(3, 2)) are not distinguished syntactically from terms denoting predicates (e.g. λ(x:int, y:int).prime(+(x, y))) or propositions (e.g. ∀P:[int].(∀x:int.P (x)) ⇒ P (3)). But in order for a term to denote anything at all, it has to be typable according to the following definitions.

Definition 2.4 A context Γ is a sequence of the form x_{1} : τ_{1}, …, x_{n} : τ_{n} where x_{i} ≠ x_{j} for all i ≠ j. We write Γ(x_{j}) for τ_{j} and Vars(Γ) for {x_{1}, …, x_{n}}, and we identify Γ with the Types(Σ)-sorted set of variables such that Γ_{τ} = {x ∈ Vars(Γ) | Γ(x) = τ} for all τ ∈ Types(Σ). Concatenation of contexts, written Γ, Γ′, is required to yield a context, i.e. it is required that Vars(Γ)∩Vars(Γ′) = ∅. Let T ⊆ Types(Σ) be a subset of the set of types over Σ; then Γ is called a T -context if Γ(x) ∈ T for all x ∈ Vars(Γ).

Definition 2.5 We write Γ ⊢ t : τ if this judgement is derivable using the rules in Figure 1, and then we call t a term in context Γ. A term t is closed if it is typable in the empty context, i.e. if ⊢ t : τ. A predicate (in context Γ) is a term t such that Γ ⊢ t : [τ_{1}, …, τ_{n}]. A formula (in context Γ) is a term φ such that Γ ⊢ φ : [ ].

Proposition 2.6 The following weakening and permutation rules are admissible in the system of rules given in Figure 1:

\frac{Γ ⊢ t : τ}{Γ, x : τ′ ⊢ t : τ}  (weak)

\frac{Γ, Γ′ ⊢ t : τ}{Γ′, Γ ⊢ t : τ}  (perm)

Proof: Obvious. □

There is no need to include equality as a built-in predicate, since it is expressible using higher-order quantification. That is, suppose Γ ⊢ t : τ and Γ ⊢ t′ : τ; then

t =_{τ} t′ abbreviates ∀P:[τ].P (t) ⇒ P (t′)

where P is chosen arbitrarily such that P ∉ Vars(Γ).

Existential quantification and the missing connectives are expressible as usual in terms of ∀ and ⇒:

true abbreviates ∀P:[ ].P ⇒ P
false abbreviates ∀P:[ ].P
¬φ abbreviates φ ⇒ false
φ ∨ φ′ abbreviates (¬φ) ⇒ φ′
φ ∧ φ′ abbreviates ¬(¬φ ∨ ¬φ′)
∃x:τ.φ abbreviates ¬∀x:τ.¬φ

Alternatively, the higher-order encodings of ∨, ∧ and ∃ could be used. In contrast to those above, these do not presuppose a classical setting, but otherwise there is no essential difference.

φ ∨ φ′ abbreviates ∀P:[ ].(φ ⇒ P) ⇒ (φ′ ⇒ P) ⇒ P
φ ∧ φ′ abbreviates ∀P:[ ].(φ ⇒ φ′ ⇒ P) ⇒ P
∃x:τ.φ abbreviates ∀P:[ ].(∀x:τ.φ ⇒ P) ⇒ P

Finally, there is no need to treat reachability constraints as a special case, since induction principles are expressible — see Example 2.7 below.

The following will be used as a running example to illustrate various definitions and results below. It is chosen for the sake of simplicity and because it was employed in [Sch92] to exhibit a weakness in existing methods for reasoning about specifications involving behavioural abstraction — see Example 7.6.

Example 2.7 We specify a counter which can be set to zero, incremented, decremented (stopping at zero), and tested to see if it is zero. The signature Σ_{ctr} has base types bool and ctr (counter), and constants zero :→ ctr, inc : ctr → ctr, dec : ctr → ctr, is-zero : ctr → bool, true :→ bool and ¬(true =_{bool} false)

∀b:bool.(b =_{bool} true ∨ b =_{bool} false)

dec(zero) =_{ctr} zero

∀c:ctr.dec(inc(c)) =_{ctr} c

is-zero(zero) =_{bool} true

∀c:ctr.is-zero(inc(c)) =_{bool} false

∀P:[ctr].( P (zero) ∧ ∀c:ctr.(P (c) ⇒ P (inc(c))) ) ⇒ ∀c:ctr.P (c)

(GENCTR)

Fig. 2. The axioms Φ_{ctr}

false :→ bool (not to be confused with the formulae true : [ ] and false : [ ]!). These constants are required to satisfy the axioms Φ_{ctr} given in Figure 2. The last axiom (labelled GENCTR) expresses a reachability constraint for ctr, requiring that all values of type ctr are generated by zero and inc. The second axiom expresses reachability for bool.

The only explicit higher-order aspect of this example is in the formula GENCTR (there is implicit higher-order quantification in each of the equations) but this will suffice for our purposes. □

The following example gives a better demonstration of the expressive power of the language.

Example 2.8 Consider the signature with base types sched (schedule) and proc (process) and constants start :→ sched, step : sched → sched and who : sched → proc. We would like to require that start is a fair schedule, i.e. that it schedules each process infinitely often. The following is essentially a translation of a formula in the modal mu-calculus [Sti92] into higher-order logic.

We begin with the least and greatest fixed point operators, which can be expressed directly as follows:

μ =_{def} λ(Φ:[[sched], sched] , s:sched).

∀P:[sched].(∀s′:sched.Φ(P, s′) ⇒ P (s′)) ⇒ P (s)

ν =_{def} λ(Φ:[[sched], sched] , s:sched).

∃P:[sched].(∀s′:sched.P (s′) ⇒ Φ(P, s′)) ∧ P (s)

The predicate always (a given predicate holds at every step in a given schedule) is expressed as a greatest fixed point, and the predicate eventually is expressed as a least fixed point:

always =_{def} λ(P:[sched], s:sched).

ν(λ(always-P:[sched], s′:sched).

P (s′) ∧ always-P(step(s′)) , s)

eventually =_{def} λ(P:[sched], s:sched).

μ(λ(eventually-P:[sched], s′:sched).

P (s′) ∨ eventually-P(step(s′)) , s)

These are used to code a predicate which checks that a given predicate holds infinitely often in a given schedule:

infinitely-often =_{def}

λ(P:[sched], s:sched). always((λ(s′:sched).eventually(P, s′)) , s)

Then the required fairness property is fair(start), where fair is expressed in terms of infinitely-often as follows:

fair =_{def} λ(s:sched). ∀p:proc.infinitely-often((λ(s′:sched).who(s′) = p) , s)

Expanding fair(start) gives a single formula expressing the required property. □

The language defined above is a trimmed version of the “classical theory of simple types” as introduced by Henkin in [Hen50]. Henkin considers nonstandard models for which a natural Gentzen-style proof system is sound and complete. A good reference is also Chapter 4 of Schütte’s monograph [Sch77] where cut-elimination for this system is established.

3 Semantics of higher-order logic

Let Σ = ⟨B, C⟩ be a signature.

Terms over Σ are interpreted in the context of a Σ-algebra which gives meaning to the base types and the constants in Σ.

Definition 3.1 A Σ-algebra A consists of a carrier set [[b]]_{A} for every b ∈ B, and interpretations of constants [[c]]_{A}∈ ([[b_{1}]]_{A}× ⋯ × [[b_{n}]]_{A}→ [[b]]_{A}) for every c : b_{1} × ⋯ × b_{n} → b in C. The class of all Σ-algebras is denoted Alg(Σ). Σhomomorphisms and Σ-isomorphisms are as usual; we write A ≅ A′ if there is a Σ-isomorphism h : A → A′.

Let A be a Σ-algebra.

We define two interpretations for terms. The first is the obvious “standard” interpretation with respect to an environment mapping free variables to values. The second interpretation is modulo a partial congruence relation on A. In the latter interpretation, quantification (and λ-abstraction) is over only those elements of types that respect the congruence; as a result, equality in formulae refers to the congruence rather than to identity of values. The particular partial congruence of interest will be a relation of indistinguishability with respect to a given set of observable base types, to be defined in Section 4. Theorem 3.35 below demonstrates a relationship between the two interpretations that will be crucial in the sequel.

Our use of partial congruences in Section 3.2 below stems from the need to establish an appropriate relationship between indistinguishability and behavioural equivalence, see Theorem 5.21, in order to apply the characterization theorems in Section 6. If the indistinguishability relation were not defined as a partial congruence, the desired relationship with the behavioural equivalence relation would not hold.

3.1 Standard interpretation

Definition 3.2 Types of the form [τ_{1}, …, τ_{n}] are interpreted as follows:

[[[τ_{1}, …, τ_{n}]]]_{A}= Pow([[τ_{1}]]_{A}× ⋯ × [[τ_{n}]]_{A}).

Thus, [[[ ]]]_{A} is {{}, {∗}} where ∗ is the empty tuple. Recalling that [ ] means Prop, {} may be thought of as denoting falsity and {∗} as denoting truth, so we will use the abbreviation ff for {} and tt for {∗}.

Let Γ be a context.

Definition 3.3 A Γ-environment (on A) is a Types(Σ)-sorted function ρ = ⟨ρ_{τ} : Γ_{τ} → [[τ]]_{A}⟩_{τ∈Types(Σ)}. We write [x_{1} ↦ v_{1}, …, x_{n} ↦ v_{n}] to denote the evident environment, and the notation ρ[x_{1} ↦ v_{1}, …, x_{n} ↦ v_{n}] denotes the environment ρ superseded at x_{1}, …, x_{n} by v_{1}, …, v_{n} respectively. When x ∈ Vars(Γ) we write ρ(x) for ρ_{Γ(x)}(x). Let T ⊆ Types(Σ); a Γ-environment ρ is T -surjective if ρ_{τ} : Γ_{τ} → [[τ]]_{A} is surjective for each τ ∈ T.

Definition 3.4 Let ρ be a Γ-environment. The interpretation of constants is extended to terms in context Γ as follows:

[[x]]_{ρ,A} = ρ(x)
[[c(t_{1}, …, t_{n})]]_{ρ,A} = [[c]]_{A}([[t_{1}]]_{ρ,A}, …, [[t_{n}]]_{ρ,A})

[[λ(x_{1}:τ_{1}, …, x_{n}:τ_{n}).t]]_{ρ,A} = {(v_{1}, …, v_{n}) | v_{1} ∈ [[τ_{1}]]_{A} and ⋯ and v_{n} ∈ [[τ_{n}]]_{A}

and [[t]]_{ρ[x_{1}↦v_{1},...,x_{n}↦v_{n}],A}= tt}
[[t(t_{1}, …, t_{n})]]_{ρ,A} = if ([[t_{1}]]_{ρ,A}, …, [[t_{n}]]_{ρ,A}) ∈ [[t]]_{ρ,A} then tt else ff
[[t ⇒ t′]]_{ρ,A} = if [[t]]_{ρ,A}= tt then [[t′]]_{ρ,A} else tt
[[∀x:τ.t]]_{ρ,A} = if [[t]]_{ρ[x↦v],A}= tt for all v ∈ [[τ]]_{A} then tt else ff

It is easy to see that the interpretation [[t]]_{ρ,A} of a term t does not depend on ρ when t is closed. We may therefore omit ρ and use the notation [[t]]_{A} in this case.

The following substitution property will be handy in proofs in later sections. As usual, s[x := t] denotes the result of simultaneously replacing all occurrences of the variable x in the term s by the term t, with appropriate changes of bound variable names to avoid variable capture.

Proposition 3.5 For any Γ ⊢ t : τ and Γ, x : τ ⊢ s : τ′ and any Γenvironment ρ, [[s]]_{ρ[x↦[[t]]_{ρ,A}],A}= [[s[x := t]]]_{ρ,A}.

Proof: By induction on the structure of s. □

The following shows that the above interpretation of terms and types is sound with respect to the typing relation.

Proposition 3.6 If Γ ⊢ t : τ and ρ is a Γ-environment then [[t]]_{ρ,A}∈ [[τ]]_{A}.

Proof: By induction on the structure of the derivation of Γ ⊢ t : τ. □

The following proposition demonstrates that =_{τ} really is equality (i.e. identity of values).

Proposition 3.7 Suppose v, v′ ∈ [[τ]]_{A} for some type τ. Then for any environment ρ, [[x =_{τ} y]]_{ρ[x↦v,y↦v′],A}= tt iff v = v′.

Proof:

⟸: Obvious.

⟹: Suppose [[∀P:[τ].P (x) ⇒ P (y)]]_{ρ[x↦v,y↦v′],A}= tt and consider the predicate {v} ∈ [[[τ]]]_{A}. We have [[P (x)]]_{ρ[x↦v,P ↦{v}],A}= tt and so [[P (y)]]_{ρ[y↦v′,P ↦{v}],A}= tt; thus v′ ∈ {v}, i.e. v = v′. □

This entitles us to use φ ⇔ φ′ as an abbreviation for φ =_{[ ]} φ′ instead of the equivalent but longer (φ ⇒ φ′) ∧ (φ′ ⇒ φ).

It is easy to see that the abbreviations defined for the connectives ¬, ∨, ∧ and for ∃ and true have the expected meaning. The following shows that the abbreviation defined for false is also correct.

Proposition 3.8 For any environment ρ, [[false]]_{ρ,A}= ff .

Proof: Recall that false is ∀P:[ ].P and take P = ff ∈ [[[ ]]]_{A}. □

Definition 3.9 Let φ be a formula in context Γ. Suppose ρ is a Γ-environment; then we write A ⊧_{ρ} φ if [[φ]]_{ρ,A}= tt. We write A ⊧ φ (A satisfies φ) if A ⊧_{ρ} φ for all Γ-environments ρ. If φ′ is also a formula in context Γ, we write φ ⊧| φ′ (φ is equivalent to φ′) if for all A ∈ Alg(Σ) and all Γ-environments ρ, A ⊧_{ρ} φ iff A ⊧_{ρ} φ′. Finally, if Φ is a set of formulae in context Γ then we write A ⊧ Φ if A ⊧ φ for all φ ∈ Φ.

Example 3.10 A Σ_{ctr}-algebra Nat is defined by taking [[ctr]]_{Nat}= ω (the set of natural numbers) and [[bool]]_{Nat}= {T, F } (not to be confused with tt and ff !) with the evident interpretation of the constants. This satisfies all of the axioms in Φ_{ctr}; see below for comments concerning GENCTR. Another Σ_{ctr}- algebra is the term algebra Term, defined by taking [[ctr]]_{Term}= {t | ⊢ t : ctr} and [[bool]]_{Term}= {T, F } with [[is-zero]]_{Term}(t) = [[is-zero(t)]]_{Nat} for t ∈ [[ctr]]_{Term}. The only axioms in Φ_{ctr} that Term satisfies are is-zero(zero) =_{bool} true, ∀c:ctr.is-zero(inc(c)) =_{bool} false, ¬(true =_{bool} false) and ∀b:bool.(b =_{bool} true ∨ b =_{bool} false). □

Definition 3.11 Let B′ ⊆ B be a subset of the set of base types in Σ, and let b ∈ B. A value v ∈ [[b]]_{A} is B′-reachable if there is a B′-context Γ, a term t with Γ ⊢ t : b, and a Γ-environment ρ, such that [[t]]_{ρ,A}= v.

Intuitively, v is B′-reachable if v can be obtained by application of constants to values of types in B′.

Example 3.12 Let Σ′_{ctr} be Σ_{ctr} without the constant dec : ctr → ctr. For any Σ_{ctr}-algebra A, A ⊧ GENCTR iff every value of type ctr in A is ∅-reachable with respect to the reduced signature Σ′_{ctr}. (The “if” direction is obvious; to see that the “only if” direction holds, simply instantiate GENCTR with the predicate P = {v ∈ [[ctr]]_{A}| v is ∅-reachable in Σ′_{ctr}} ∈ [[[ctr]]]_{A}.) Then Nat ⊧ GENCTR and Term |̸= GENCTR (since dec(zero) ∈ [[ctr]]_{Term} is not ∅-reachable in Σ′_{ctr}). □

The following proposition is used to show that isomorphisms preserve and reflect satisfaction, as in almost any conceivable logical system.

Proposition 3.13 Let h : A → A′ be an isomorphism. Extend h to bracket types by taking h_{[τ_{1},...,τ_{n}]}(p) = {(h_{τ_{1}}(v_{1}), …, h_{τ_{n}}(v_{n})) | (v_{1}, …, v_{n}) ∈ p} ∈ [[[τ_{1}, …, τ_{n}]]]_{A′} for p ∈ [[[τ_{1}, …, τ_{n}]]]_{A}. Let t be a term in context Γ and let ρ be a Γ-environment; then h([[t]]_{ρ,A}) = [[t]]_{h∘ρ,A′}.

Proof: By induction on the structure of t. □

Corollary 3.14 If A ≅ A′ then A ⊧ φ iff A′ ⊧ φ.

Proof: By Proposition 3.13, since h_{[ ]} is the identity and since h_{τ} is a bijection for every type τ. □

3.2 Interpretation w.r.t. a partial congruence

Definition 3.15 A partial congruence ≈ on A is a family of partial equivalence relations (i.e., symmetric and transitive relations) ⟨≈_{b} ⊆ [[b]]_{A}×[[b]]_{A}⟩_{b∈B} such that for all c : b_{1} × ⋯ × b_{n} → b in C and all v_{1}, v′_{1} ∈ [[b_{1}]]_{A}, …, v_{n}, v′_{n} ∈ [[b_{n}]]_{A}, if v_{1} ≈_{b_{1}} v′_{1} and ⋯ and v_{n} ≈_{b_{n}} v′_{n} then [[c]]_{A}(v_{1}, …, v_{n}) ≈_{b} [[c]]_{A}(v′_{1}, …, v′_{n}). A (total) congruence is a reflexive partial congruence.

Example 3.16 Equality is a total congruence on Nat. A total congruence on Term is given by t ≈_{ctr} t′ ⇔ [[t]]_{Nat}= [[t′]]_{Nat} for all t, t′ ∈ [[ctr]]_{Term} (so we have e.g. dec(inc(zero)) ≈_{ctr} zero) and b ≈_{bool} b′ ⇔ b = b′. This is a partial congruence on the Σ_{ctr}-algebra Term^{∞} defined by taking [[ctr]]_{Term}_{∞}= [[ctr]]_{Term}∪{∞} and [[bool]]_{Term}_{∞}= [[bool]]_{Term}, with interpretation of constants as in Term augmented by [[inc]]_{Term}_{∞}(∞) = [[dec]]_{Term}_{∞}(∞) = ∞ and [[is-zero]]_{Term}_{∞}(∞) = F. Another total congruence on Term, which is again a partial congruence on Term^{∞}, is obtained by taking t ≈′_{ctr} t′ ⇔ [[t]]_{Nat}≡ [[t′]]_{Nat} (mod 2) for all t, t′ ∈ [[ctr]]_{Term} and b ≈′_{bool} b′ for all b, b′ ∈ {T, F } (this is forced by the fact that inc(inc(zero)) ≈′_{ctr} zero). □

Let ≈ be a partial congruence on A. As suggested at the beginning of Section 3, the partial congruence of interest will be a relation of indistinguishability to be defined later. The reader may find it helpful to keep this in mind in order to understand the motivation behind some of the definitions and results below. We do not restrict attention to this particular partial congruence at this point because much of the sequel does not depend on the special features of this relation, and because there are several different indistinguishability relations of potential interest (although we will consider only one).

The idea behind the development which follows is to generalize the usual definition of satisfaction up to a partial congruence in first-order equational logic to higher-order logic. Whereas in the first-order case it is enough to interpret the primitive equality symbol as the partial congruence and to restrict all quantifiers to values lying in the domain of the partial congruence, the situation is more complicated here. We must make sure that the predicate variables only range over predicates which “respect” the partial congruence. What this means exactly is not entirely obvious for types with nested brackets. That the definition we give is indeed the right generalization of the first-order case is shown by Proposition 3.29 and Theorem 3.35. In the first-order case, Proposition 3.29 is obvious from the definition of satisfaction.

The following definition explains how to extend the partial congruence ≈, which relates values of base types only, to a so-called logical relation (see e.g. [Mit90]) over all types. The resulting relation will be used below to give an interpretation of bracket types.

Definition 3.17 We extend ≈ to “bracket” types by taking p ≈_{[τ_{1},...,τ_{n}]} p′ for p, p′ ∈ [[[τ_{1}, …, τ_{n}]]]_{A} iff for all v_{1}, v′_{1} ∈ [[τ_{1}]]_{A}, …, v_{n}, v′_{n} ∈ [[τ_{n}]]_{A}, if v_{1} ≈_{τ_{1}} v′_{1} and ⋯ and v_{n} ≈_{τ_{n}} v′_{n} then (v_{1}, …, v_{n}) ∈ p iff (v′_{1}, …, v′_{n}) ∈ p′. We say that v ∈ [[τ]]_{A} respects ≈ if v ≈_{τ} v.

A predicate p ∈ [[[τ_{1}, …, τ_{n}]]]_{A} respects ≈ if it does not differentiate between values that are related by ≈. Note that trivially ∅ ≈_{[τ_{1},...,τ_{n}]} ∅, and that v ≈_{[ ]} v′ iff v = v′.

Example 3.18 Consider ≈ on Term and Term^{∞} given in Example 3.16. Let P = {t ∈ [[ctr]]_{Term}| t does not contain dec} and P′ = {t ∈ [[ctr]]_{Term}| [[t]]_{Nat}≡ 0 (mod 2)}, so P, P′ ∈ [[[ctr]]]_{Term}⊂ [[[ctr]]]_{Term}_{∞}; then P does not respect ≈ (since dec(inc(zero)) ≈_{ctr} zero and zero ∈ P but dec(inc(zero)) ∉ P) but P′ does. Since ≈ is a partial congruence on Term^{∞}, its extension to bracket types may identify distinct values. For instance, {∞} ≈_{[ctr]} ∅ since v ≈_{ctr} v implies that v ≠ ∞. This in turn directly implies that {{∞}} ≉_{[[ctr]]} {{∞}} (note that {{∞}} ∈ [[[[ctr]]]]_{Term}_{∞} is the predicate that holds only for the predicate {∞} ∈ [[[ctr]]]_{Term}_{∞}). Finally, for an example of identification of distinct values at third-order types, consider {P } ≈_{[[ctr]]} ∅. □

Proposition 3.19 ≈_{τ} is a partial equivalence relation for any type τ.

Proof: Obvious. □

Note that extending a (total) congruence to bracket types does not in general yield a (total) equivalence relation.

Corollary 3.20 If v ≈_{τ} v′ then v and v′ respect ≈.

Proof: Apply symmetry and transitivity. □

The difference between the standard interpretation of terms and their interpretation with respect to a partial congruence stems from the following definition.

Definition 3.21 Interpretation of types w.r.t. ≈ is defined as follows:

[[b]]_{A}^{≈} = {v ∈ [[b]]_{A}| v respects ≈}
[[[τ_{1}, …, τ_{n}]]]_{A}^{≈} = {p ∈ Pow([[τ_{1}]]_{A}^{≈}× ⋯ × [[τ_{n}]]_{A}^{≈}) | p respects ≈}

We have [[[ ]]]_{A}^{≈}= [[[ ]]]_{A}= {ff , tt}. Note that if ≈ is a congruence, then [[b]]_{A}^{≈}= [[b]]_{A}. The second clause of the above definition is well-formed because of the following proposition.

Proposition 3.22 [[τ]]_{A}^{≈}⊆ [[τ]]_{A} for any type τ.

Proof: By induction on the structure of τ. (Thus the proof that [[[τ_{1}, …, τ_{n}]]]_{A}^{≈} is well-defined depends on [[τ_{1}]]_{A}^{≈}, …, [[τ_{n}]]_{A}^{≈}, which have been shown to be welldefined at a previous stage.) □

Example 3.23 Consider ≈ on Term^{∞} given in Example 3.16. We have ∞ ∉ [[ctr]]_{Term^{∞}}^{≈} but v ∈ [[ctr]]_{Term^{∞}}^{≈} for all other v ∈ [[ctr]]_{Term}_{∞}. From Example 3.18 we have P ∉ [[[ctr]]]_{Term^{∞}}^{≈}, P′ ∈ [[[ctr]]]_{Term^{∞}}^{≈} and {{∞}} ∉ [[[[ctr]]]]_{Term^{∞}}^{≈}.

□

The following proposition shows that the extension of ≈ to bracket types, restricted to type interpretations [[[τ_{1}, …, τ_{n}]]]_{A}^{≈}, is trivial in the sense that it does not identify distinct values.

Proposition 3.24 For all p, p′ ∈ [[[τ_{1}, …, τ_{n}]]]_{A}^{≈}, if p ≈_{[τ_{1},...,τ_{n}]} p′ then p = p′.

Proof: Let v_{1} ∈ [[τ_{1}]]_{A}^{≈}, …, v_{n} ∈ [[τ_{n}]]_{A}^{≈}; then v_{1} ≈_{τ_{1}} v_{1} and ⋯ and v_{n} ≈_{τ_{n}} v_{n}. If p ≈_{[τ_{1},...,τ_{n}]} p′ then (v_{1} …, v_{n}) ∈ p iff (v_{1} …, v_{n}) ∈ p′, i.e. p = p′. □

Returning to Example 3.18, we see that {∞} ∉ [[[ctr]]]_{Term^{∞}}^{≈} and {P } ∉ [[[[ctr]]]]_{Term^{∞}}^{≈} and thus these do not provide counterexamples to Proposition 3.24.

Let Γ be a context.

Definition 3.25 A Γ-environment (w.r.t. ≈, on A) is a Types(Σ)-sorted function ρ = ⟨ρ_{τ} : Γ_{τ} → [[τ]]_{A}^{≈}⟩_{τ∈Types(Σ)}. We adopt the previously-explained notations for environments.

Definition 3.26 Let ρ be a Γ-environment w.r.t. ≈. The interpretation w.r.t. ≈ of terms that are typable in context Γ is defined as follows:

[[x]]_{ρ,A}^{≈} = ρ(x)
[[c(t_{1}, …, t_{n})]]_{ρ,A}^{≈} = [[c]]_{A}([[t_{1}]]_{ρ,A}^{≈}, …, [[t_{n}]]_{ρ,A}^{≈})

[[λ(x_{1}:τ_{1}, …, x_{n}:τ_{n}).t]]_{ρ,A}^{≈} = {(v_{1}, …, v_{n}) | v_{1} ∈ [[τ_{1}]]_{A}^{≈} and ⋯ and v_{n} ∈ [[τ_{n}]]_{A}^{≈}

and [[t]]_{ρ[x_{1}↦v_{1},...,x_{n}↦v_{n}],A}^{≈}= tt}
[[t(t_{1}, …, t_{n})]]_{ρ,A}^{≈} = if ([[t_{1}]]_{ρ,A}^{≈}, …, [[t_{n}]]_{ρ,A}^{≈}) ∈ [[t]]_{ρ,A}^{≈} then tt else ff
[[t ⇒ t′]]_{ρ,A}^{≈} = if [[t]]_{ρ,A}^{≈}= tt then [[t′]]_{ρ,A}^{≈} else tt
[[∀x:τ.t]]_{ρ,A}^{≈} = if [[t]]_{ρ[x↦v],A}^{≈}= tt for all v ∈ [[τ]]_{A}^{≈} then tt else ff

A comparison of the above definition with the corresponding definition for the standard interpretation (Definition 3.4) reveals that the only difference is the change to the meaning of λ-abstraction and universal quantification induced by the different interpretation of types.

The proof of soundness does not go through directly; a stronger induction hypothesis is required.

Proposition 3.27 Suppose Γ ⊢ t : τ and ρ, ρ′ are Γ-environments w.r.t. ≈ such that ρ(x) ≈_{Γ(x)} ρ′(x) for each x ∈ Vars(Γ). Then:

(i) If τ is a base type b, then [[t]]_{ρ,A}^{≈}, [[t]]_{ρ′,A}^{≈}∈ [[b]]_{A} (ii) If τ is [τ_{1}, …, τ_{n}], then [[t]]_{ρ,A}^{≈}, [[t]]_{ρ′,A}^{≈}∈ Pow([[τ_{1}]]_{A}^{≈}× ⋯ × [[τ_{n}]]_{A}^{≈})

and [[t]]_{ρ,A}^{≈}≈_{τ} [[t]]_{ρ′,A}^{≈}.

Proof: By induction on the structure of the derivation of Γ ⊢ t : τ. □

Corollary 3.28 If Γ ⊢ t : τ and ρ is a Γ-environment w.r.t. ≈ then [[t]]_{ρ,A}^{≈}∈ [[τ]]_{A}^{≈}.

Proof: Apply Proposition 3.27 with ρ′ = ρ. □

The following proposition shows that =_{τ} refers to the partial congruence ≈ under interpretation of terms w.r.t. ≈. This is due to the fact that the quantifier in the formula ∀P:[τ].P (t) ⇒ P (t′) (which t =_{τ} t′ abbreviates) ranges over predicates that respect ≈.

Proposition 3.29 Suppose v, v′ ∈ [[τ]]_{A}^{≈} for some type τ. Then for any environment ρ w.r.t. ≈, [[x =_{τ} y]]_{ρ[x↦v,y↦v′],A}^{≈}= tt iff v ≈_{τ} v′.

Proof:

⟸: Suppose v ≈_{τ} v′. Any predicate p ∈ [[[τ]]]_{A}^{≈} respects ≈, i.e. v ∈ p iff v′ ∈ p.

⟹: Suppose that [[∀P:[τ].P (x) ⇒ P (y)]]_{ρ[x↦v,y↦v′],A}^{≈}= tt and consider the predicate p = {w | w ≈_{τ} v} ∈ [[[τ]]]_{A}^{≈}. We have [[P (x)]]_{ρ[x↦v,P ↦p],A}^{≈}= tt so [[P (y)]]_{ρ[y↦v′,P ↦p],A}^{≈}= tt; thus v′ ∈ p, i.e. v′ ≈_{τ} v. □

Definition 3.30 Let φ be a formula in context Γ. Suppose ρ is a Γ-environment w.r.t. ≈; then we write A ⊧_{ρ}^{≈} φ if [[φ]]_{ρ,A}^{≈}= tt. We write A ⊧^{≈} φ (A satisfies φ w.r.t. ≈) if A ⊧_{ρ}^{≈} φ for all Γ-environments ρ w.r.t. ≈. If Φ is a set of formulae in context Γ then we write A ⊧^{≈} Φ if A ⊧^{≈} φ for all φ ∈ Φ.

When ≈ is the indistinguishability relation (see Definition 4.1 below), ⊧^{≈} is known as behavioural satisfaction.

Example 3.31 The Σ_{ctr}-algebra Nat satisfies all of the axioms in Φ_{ctr} with respect to equality, since it satisfies them in the standard sense (Example 3.10). The algebras Term and Term^{∞} satisfy all of these axioms with respect to the congruence ≈ given in Example 3.16; see below for comments concerning GENCTR. They satisfy all of them with respect to ≈′ with the exception of the axiom ¬(true =_{bool} false).

For any Σ_{ctr}-algebra A and any partial congruence ≈ on A, A ⊧^{≈} GENCTR iff every value in [[ctr]]_{A}^{≈} is congruent to a value that is ∅-reachable with respect to the reduced signature Σ′_{ctr} from Example 3.12. (The “if” direction depends on the requirement that P ∈ [[[ctr]]]_{A}^{≈} rather than P ∈ [[[ctr]]]_{A}; to see that the “only if” direction holds, instantiate GENCTR with P = {v ∈ [[ctr]]_{A}^{≈}| ∃v′ ∈ [[ctr]]_{A}^{≈}.v ≈_{ctr} v′ and v′ is ∅-reachable in Σ′_{ctr}} ∈ [[[ctr]]]_{A}^{≈}. Note that there are A and ≈ for which {v ∈ [[ctr]]_{A}^{≈}| v is ∅-reachable in Σ′_{ctr}} ∉ [[[ctr]]]_{A}^{≈}.) This shows that Term ⊧^{≈} GENCTR and Term^{∞} ⊧^{≈} GENCTR for ≈ as given in Example 3.16. □

3.3 Relating ⊧ and ⊧^{≈}

Let ≈ be a partial congruence on A.

Definition 3.32 Suppose v ∈ [[b]]_{A} for b ∈ B such that v ≈_{b} v; then the congruence class of v w.r.t. ≈ is defined as [v]_{≈_{b}} = {v′ ∈ [[b]]_{A}| v ≈_{b} v′}. The quotient of A by ≈, written A/≈, is then defined as follows:

[[b]]_{A/≈}= {[v]_{≈_{b}} | v ∈ [[b]]_{A} and v ≈_{b} v} for all b ∈ B
[[c]]_{A/≈}([v_{1}]_{≈_{b_{1}}}, …, [v_{n}]_{≈_{bn}}) = [[[c]]_{A}(v_{1}, …, v_{n})]_{≈_{b}}

for all c : b_{1} × ⋯ × b_{n} → b in C.

Since ≈ is a partial congruence, the choice of representatives v_{1}, …, v_{n} in the definition of [[c]]_{A/≈} doesn’t matter. Note that if ≈ is a congruence, then A/≈ is the usual quotient algebra, with [[b]]_{A/≈}= [[b]]_{A}/≈_{b}.

Proposition 3.33 A/≈ is a Σ-algebra, that is [[c]]_{A/≈}∈ ([[b_{1}]]_{A/≈}× ⋯×[[b_{n}]]_{A/≈}→ [[b]]_{A/≈}) for every c : b_{1} × ⋯ × b_{n} → b in C.

Proof: Easy, since if v_{1} ∈ [[b_{1}]]_{A/≈}, …, v_{n} ∈ [[b_{n}]]_{A/≈} then v_{1} ≈_{b_{1}} v_{1} and ⋯ and v_{n} ≈_{b_{n}} v_{n} so [[c]]_{A}(v_{1}, …, v_{n}) ≈_{b} [[c]]_{A}(v_{1}, …, v_{n}). □

Example 3.34 Nat ≅ Term/≈ ≅ Term^{∞}/≈ for ≈ as given in Example 3.16. □

The following theorem demonstrates a fundamental relationship between the two interpretations defined above. In the first-order case, it says that standard satisfaction of a formula φ in a quotient algebra A/≈ is equivalent to satisfaction of φ, with the symbol = interpreted as ≈, in A itself.

Theorem 3.35 A/≈ ⊧ φ iff A ⊧^{≈} φ.

Proof: Define two families of functions ⟨ψ_{τ} : [[τ]]_{A}^{≈}→ [[τ]]_{A/≈}⟩_{τ∈Types(Σ)} and ⟨χ_{τ} : [[τ]]_{A/≈}→ [[τ]]_{A}^{≈}⟩_{τ∈Types(Σ)} by induction on τ as follows:

for all v ∈ [[b]]_{A}^{≈},
ψ_{b}(v) = [v]_{≈_{b}}
for all v ∈ [[b]]_{A/≈},
χ_{b}(v) = some arbitrary element of v
for all p ∈ [[[τ_{1}, …, τ_{n}]]]_{A}^{≈},
ψ_{[τ_{1},...,τ_{n}]}(p) = {(v_{1}, …, v_{n}) ∈ [[τ_{1}]]_{A/≈}× ⋯ × [[τ_{n}]]_{A/≈}| (χ_{τ_{1}}(v_{1}), …, χ_{τ_{n}}(v_{n})) ∈ p}
for all p ∈ [[[τ_{1}, …, τ_{n}]]]_{A/≈},
χ_{[τ_{1},...,τ_{n}]}(p) = {(v_{1}, …, v_{n}) ∈ [[τ_{1}]]_{A}^{≈}× ⋯ × [[τ_{n}]]_{A}^{≈}| (ψ_{τ_{1}}(v_{1}), …, ψ_{τ_{n}}(v_{n})) ∈ p}

These functions are well-defined. First, ψ and χ_{[τ_{1},...,τ_{n}]} are not affected by the choice of χ_{b}. Second, for all v ∈ [[τ]]_{A/≈}, χ_{τ}(v) respects ≈ (for base types b, we have v ≈_{b} v for v ∈ [[b]]_{A/≈}; for bracket types, it follows from the fact that v ≈_{τ} v′ implies ψ_{τ}(v) = ψ_{τ}(v′)). We have for all v ∈ [[τ]]_{A/≈}, ψ_{τ}(χ_{τ}(v)) = v and for all v ∈ [[τ]]_{A}^{≈}, χ_{τ}(ψ_{τ}(v)) ≈_{τ} v, both by induction on the structure of τ (the latter uses again the fact that v ≈_{τ} v′ implies ψ_{τ}(v) = ψ_{τ}(v′)). The former implies that ψ_{τ} is onto for all τ. Note that ψ_{[ ]} is the identity.

The remainder of the proof relies on the following:

Lemma For any Γ ⊢ t : τ and Γ-environment ρ w.r.t. ≈, [[t]]_{ψ∘ρ,A/≈}= ψ_{τ}([[t]]_{ρ,A}^{≈}).

Proof: By induction on the structure of the derivation of Γ ⊢ t : τ. For function application, we use the fact that for c : b_{1} × ⋯ × b_{n} → b in C we have ψ_{b}([[c]]_{A}(v_{1}, …, v_{n})) = [[c]]_{A/≈}(ψ_{b_{1}}(v_{1}), …, ψ_{b_{n}}(v_{n})). For universal quantification, we use the fact that ψ is onto. □ (lemma)

This gives A/≈ ⊧ φ ⇒ A ⊧^{≈} φ, as follows. Suppose that A/≈ ⊧ φ, i.e. Γ ⊢ φ : [ ] and for all Γ-environments ρ on A/≈, A/≈ ⊧_{ρ} φ. Then suppose ρ is a Γ-environment on A w.r.t. ≈. We need to show that A ⊧_{ρ}^{≈} φ. But ψ ∘ ρ is a Γ-environment on A/≈, and so [[φ]]_{ρ,A}^{≈}= ψ_{[ ]}([[φ]]_{ρ,A}^{≈}) = [[φ]]_{ψ∘ρ,A/≈}= tt.

For A/≈ ⊧ φ ⇐ A ⊧^{≈} φ, suppose that A ⊧^{≈} φ, i.e. Γ ⊢ φ : [ ] and for all Γ-environments ρ w.r.t. ≈, A ⊧_{ρ}^{≈} φ. Then suppose ρ is a Γ-environment on A/≈. We need to show that A/≈ ⊧_{ρ} φ. Since ψ is onto, ρ factors through ψ: ρ = ψ∘ρ′ for some Γ-environment ρ′ w.r.t. ≈. Thus [[φ]]_{ψ∘ρ′,A/≈}= ψ_{[ ]}([[φ]]_{ρ′,A}^{≈}) = ψ_{[ ]}(tt) = tt, i.e. A/≈ ⊧_{ρ} φ. □

A trivial consequence of Theorem 3.35 is the fact that when ≈ is equality, ⊧^{≈} coincides with ⊧. Theorem 3.35 for the case of infinitary first-order equational logic is Theorem 3.11 of [BHW95], where the proof method is analogous.

Example 3.36 From Example 3.10 we know that Nat ⊧ Φ_{ctr}, and then Corollary 3.14 and the fact (Example 3.34) that Nat ≅ Term^{∞}/≈ for ≈ as given in Example 3.16 gives Term^{∞}/≈ ⊧ Φ_{ctr}. Then Theorem 3.35 tells us that Term^{∞} ⊧^{≈} Φ_{ctr}, which is what we concluded in Example 3.31. (And vice versa.) □

We believe that the above development would go through, mutatis mutandis, for Henkin models [Hen50] as well as in a constructive framework like that of topos theory [Pho92], see Section 3.9 of [TvD88]. In the absence of the axiom of choice, e.g. in topos theory, one must replace the function χ in the proof of Theorem 3.35 by a relation which is functional up to ≈.

4 Behavioural equivalence and indistinguishability

We now consider specific definitions of indistinguishability and behavioural equivalence. Let Σ = ⟨B, C⟩ be a signature, and let OBS, the observable base types of Σ, be a subset of B. The intention is that OBS includes just those base types that are directly visible to clients; typically this would include types like bool and nat. All other types, including all bracket types, are hidden in the sense that their values may only be inspected indirectly by performing experiments (i.e. evaluating terms) that yield a result of a type in OBS.

The following defines the indistinguishability relation used in [NO88]. Two values v, v′ are indistinguishable if no experiment of observable type with additional observable inputs is able to distinguish between them.

Definition 4.1 Let the family of partial congruences ≈_{OBS} = ⟨≈_{OBS,A}⟩_{A∈Alg(Σ)} be such that for any Σ-algebra A, base type b ∈ B and v, v′ ∈ [[b]]_{A}, v ≈_{OBS,A,b} v′ (v and v′ are indistinguishable) iff v and v′ are OBS-reachable, and for any OBS-context Γ, variable x ∉ Vars(Γ), term t with Γ, x : b ⊢ t : b′ for b′ ∈ OBS, and Γ-environment ρ, [[t]]_{ρ[x↦v],A}= [[t]]_{ρ[x↦v′],A}.

Example 4.2 The partial congruence ≈_{{bool},Nat} is equality, while ≈_{{bool},Term^{∞}}, which is the same as ≈_{{bool},Term}, is ≈ from Example 3.16. Making all base types observable, as in ≈_{{bool,ctr},Term}, yields equality. The partial congruence ≈_{{ctr},Term} is equality on ctr but is the total relation on bool since there are no terms over Σ_{ctr} of type ctr containing a variable of type bool. Providing no observable types, as in ≈_{∅,Term}, yields the total relation for similar reasons.

□

Proposition 4.3 For any Σ-algebra A, ≈_{OBS,A} is a partial congruence on A.

Proof: Symmetry and transitivity are obvious. Suppose c : b_{1} × ⋯ × b_{n} → b in C and v_{1} ≈_{OBS,A,b_{1}} v′_{1} and ⋯ and v_{n} ≈_{OBS,A,b_{n}} v′_{n}; we have to show that [[c]]_{A}(v_{1}, …, v_{n}) ≈_{OBS,A,b} [[c]]_{A}(v′_{1}, …, v′_{n}). Since v_{i}, v′_{i} are OBS-reachable for all 1 ≤ i ≤ n, there is an OBS-context Γ, Γ-environment ρ and terms t_{i}, t′_{i} in context Γ such that v_{i} = [[t_{i}]]_{ρ,A} and v′_{i} = [[t′_{i}]]_{ρ,A}, for all 1 ≤ i ≤ n. (There is no loss of generality in taking the same Γ and ρ for all of these terms.) Now, let Γ′ be an OBS-context, suppose that Γ′, x : b ⊢ s : b′ for b′ ∈ OBS and x ∉ Vars(Γ′), and let ρ′ be a Γ′-environment. W.l.o.g. we may assume that Vars(Γ) and Vars(Γ′) are disjoint and that x ∉ Vars(Γ). We then calculate as follows:

[[s]]_{ρ′[x↦[[c]]_{A}(v_{1},...,v_{n})],A}
= [[s]]_{(ρ′+ρ)[x↦[[c(t_{1},...,t_{n})]]_{ρ′+ρ,A}],A}  (using disjointness)
= [[s[x := c(t_{1}, …, t_{n})]]]_{ρ′+ρ,A}  (by Proposition 3.5)
= [[s[x := c(y, t_{2}, …, t_{n})]]]_{(ρ′+ρ)[y↦v_{1}],A} (using Proposition 3.5)
= [[s[x := c(y, t_{2}, …, t_{n})]]]_{(ρ′+ρ)[y↦v′_{1}],A} (since v_{1} ≈_{OBS,A,b_{1}} v′_{1})
= [[s[x := c(t′_{1}, t_{2}, …, t_{n})]]]_{ρ′+ρ,A}  (using Proposition 3.5)
= [[s[x := c(t′_{1}, …, t′_{n})]]]_{ρ′+ρ,A}  (iterating the above three steps)
= [[s]]_{ρ′[x↦[[c]]_{A}(v′_{1},...,v′_{n})],A}  (reversing the first two steps).

Since [[c]]_{A}(v_{1}, …, v_{n}) and [[c]]_{A}(v′_{1}, …, v′_{n}) are clearly OBS-reachable, the claim follows. □

Note that the above proof makes essential use of the fact that OBS-reachability of v and v′ is required for v ≈_{OBS,A,b} v′ in Definition 4.1. This is no accident, as the following counterexample shows.

Counterexample 4.4 Let the signature Σ have base types b and bool and constants f : b → bool and c : b×b → b, and take OBS = {bool}. Consider the Σ-algebra A such that [[b]]_{A}= {0, 1, 2}, [[bool]]_{A}= {T, F }, [[f]]_{A}(0) = [[f]]_{A}(1) = T, [[f]]_{A}(2) = F, and

[[c]]_{A}(x, y) = \{ \begin{matrix}x & if x = y \\ 2 & if x ≠ y \end{matrix}

Now suppose that the requirement of OBS-reachability were removed from Definition 4.1. Then 0 ≈_{OBS,A,b} 0 and 0 ≈_{OBS,A,b} 1 but [[c]]_{A}(0, 0) ≉_{OBS,A,b} [[c]]_{A}(0, 1) since [[f]]_{A}([[c]]_{A}(0, 0)) ≠ [[f]]_{A}([[c]]_{A}(0, 1)). □

By analogy with the terminology of denotational semantics (see e.g. [Win93]), a Σ-algebra A is called fully abstract when the indistinguishability relation on A is simply equality. Such an A is called an algebra of minimal redundancy in [Rei85].

Definition 4.5 ([BHW95]) Let ≈ = ⟨≈_{A}⟩_{A∈Alg(Σ)} be a family such that each ≈_{A} is a partial congruence on A. A Σ-algebra A is ≈-fully abstract when ≈_{A} is the equality in A, that is, when for all b ∈ B and v, v′ ∈ [[b]]_{A} we have v ≈_{A} v′ iff v = v′. For any class A ⊆ Alg(Σ) of Σ-algebras, FA_{≈}(A) ⊆ A is the subclass of ≈-fully abstract algebras, that is:

FA_{≈}(A) = {A ∈ A | A is ≈-fully abstract}.

The family ≈ is regular if A/≈_{A} is ≈-fully abstract for every A ∈ Alg(Σ).

Example 4.6 Nat is ≈_{{bool}}-fully abstract, while Term and Term^{∞} are not. □

Regularity ensures that the partial congruences which ≈ associates with different algebras are related in a natural way.

Proposition 4.7 ≈_{OBS} is regular.

Proof: We have to show that for all b ∈ B and for all v, v′ ∈ [[b]]_{A/≈_{OBS,A}}, v ≈_{OBS,A/≈_{OBS,A}} v′ iff v = v′.

⟸: We only need to show that v(= v′) is OBS-reachable. This follows from the lemma in the proof of Theorem 3.35 and the fact that v is a congruence class of OBS-reachable values in A.

⟹: Suppose that v ≈_{OBS,A/≈_{OBS,A}} v′. Then for any OBS-context Γ, x ∉ Vars(Γ), term t such that Γ, x : b ⊢ t : b′ for b′ ∈ OBS and Γ-environment ρ on A/≈_{OBS,A}, [[t]]_{ρ[x↦v],A/≈_{OBS,A}}= [[t]]_{ρ[x↦v′],A/≈_{OBS,A}}. Let v̂, v̂′ ∈ [[b]]_{A} be such that [v̂]_{≈_{OBS,A}} = v and [v̂′]_{≈_{OBS,A}} = v′; by the lemma in the proof of Theorem 3.35, it follows that [[[t]]_{ρ′[x↦_{v}],A}]_{≈_{OBS,A}} = [[[t]]_{ρ′[x↦_{v′}],A}]_{≈_{OBS,A}} for any Γ-environment ρ′ on A, because for any ρ there is a ρ′ such that ρ = [·]_{≈_{OBS,A}} ∘ ρ′, and vice versa since Γ is an OBS-context so ρ′(x) is trivially OBS-reachable for any x ∈ Vars(Γ). But ≈_{OBS,A} on b′ ∈ OBS is equality so v̂ ≈_{OBS,A} v̂′, i.e. v = v′.

□

A slightly weaker property than regularity is required to state the main characterization theorem from [BHW95].

Definition 4.8 ([BHW95]) Let ≈ = ⟨≈_{A}⟩_{A∈Alg(Σ)} be a family such that each ≈_{A} is a partial congruence on A. The family ≈ is weakly regular if A/≈_{A} ≅ (A/≈_{A})/≈_{(A/≈_{A})} for every A ∈ Alg(Σ).

Proposition 4.9 ([BHW95]) If ≈ is regular then it is weakly regular.

Proof: From the definitions. □

We will now define what it means for two Σ-algebras to be behaviourally equivalent. The definition resembles that of indistinguishability in the sense that it is based on the idea of performing experiments to probe for differences between the two algebras. But in this case performing an experiment means testing satisfaction of a formula rather than evaluating a term of base type, and here we are comparing algebras rather than values within a single algebra. The formulae of importance are equations between terms of observable type, with variables of observable type.

Definition 4.10 Let Γ be an OBS-context. An observable equation is a formula in context Γ of the form t =_{b} t′ where b ∈ OBS. Let ObsEq_{Γ}(Σ) be the set of observable equations in context Γ.

Definition 4.11 Let A, A′ ∈ Alg(Σ). A is behaviourally equivalent to A′ (via equations), written A ≡_{OBS} A′, if there is an OBS-context Γ and Γenvironments ρ_{A} on A and ρ_{A′} on A′ that are OBS-surjective (see Definition 3.3) such that for any equation φ ∈ ObsEq_{Γ}(Σ), A ⊧_{ρ_{A}} φ iff A′ ⊧_{ρ_{A′}} φ.

Example 4.12 Nat ≡_{{bool}} Term ≡_{{bool}} Term^{∞}. □

Proposition 4.13 ≡_{OBS} ⊆ Alg(Σ) × Alg(Σ) is an equivalence relation.

Proof: Reflexivity and symmetry are obvious. Transitivity follows from the observation that the choice of variable names in the context Γ is arbitrary.

□

It might seem surprising that the definition of ≡_{OBS} does not make use of the higher-order features of the language, except as a result of the way that equality is expressed via quantification over predicates. So ≡_{OBS} is just the same as in e.g. [SW83], [MG85], [NO88]. The reason for this choice is that the natural modification of the definition of ≡_{OBS} to make use of higher-order formulae (Definition 5.19) gives exactly the same relation, see Corollary 5.22.

The following definition is the key to understanding the relationship between indistinguishability of values on the one hand and behavioural equivalence of algebras on the other. The idea is that a family of partial congruences naturally induces an equivalence on Alg(Σ). If behavioural equivalence is the relation that is induced by indistinguishability (as will turn out to be the case, see Theorem 5.21) then it is possible to translate constructions phrased in terms of behavioural equivalence into constructions phrased in terms of indistinguishability, and vice versa. There is a close analogy with the case of finite state machines, where two machines M, M′ are equivalent if quotienting M and M′ by the so-called Nerode equivalence on states yields isomorphic machines.

Definition 4.14 ([BHW95]) Let ≈ = ⟨≈_{A}⟩_{A∈Alg(Σ)} be a family such that each ≈_{A} is a partial congruence on A, and let ≡ ⊆ Alg(Σ) × Alg(Σ) be an equivalence relation. Then ≡ is factorizable by ≈ if for any A, A′ ∈ Alg(Σ), A ≡ A′ iff A/≈_{A} ≅ A′/≈_{A′}. (Factorizability can be decomposed as follows: ≡ is left-factorizable by ≈ if for any A, A′ ∈ Alg(Σ), A ≡ A′ ⇐ A/≈_{A} ≅ A′/≈_{A′}, and it is right-factorizable by ≈ if for any A, A′ ∈ Alg(Σ), A ≡ A′ ⇒ A/≈_{A} ≅ A′/≈_{A′}.)

The following proposition gives right-factorizability of ≡_{OBS} by ≈_{OBS}. Leftfactorizability can be proved directly, but we obtain it instead by applying a more general result, see Corollary 5.16 below.

Proposition 4.15 For any A, A′ ∈ Alg(Σ), if A ≡_{OBS} A′ then A/≈_{OBS,A} ≅ A′/≈_{OBS,A′}.

Proof: Suppose that A ≡_{OBS} A′ via OBS-context Γ and Γ-environments ρ_{A} on A and ρ_{A′} on A′. The proof uses the following:

Lemma Let t, t′ be terms such that Γ ⊢ t : b and Γ ⊢ t′ : b. Then [[t]]_{ρ_{A},A}≈_{OBS,A,b} [[t′]]_{ρ_{A},A} iff [[t]]_{ρ_{A′},A′}≈_{OBS,A′,b} [[t′]]_{ρ_{A′},A′}.

Proof:

⟹: Suppose that [[t]]_{ρ_{A},A}≈_{OBS,A,b} [[t′]]_{ρ_{A},A}. We know that [[t]]_{ρ_{A′},A′} and [[t′]]_{ρ_{A′},A′} are OBS-reachable since Γ is an OBS-context. Let Γ′ be an OBS-context, x ∉ Vars(Γ′) be a variable, s be a term with Γ′, x : b ⊢ s : b′ for b′ ∈ OBS, and ρ be a Γ-environment on A′. We need to show that [[s]]_{ρ[x↦[[t]]_{ρ_{A′} ,A′}],A′}=

[[s]]_{ρ[x↦[[t′]]_{ρ_{A′} ,A′}],A′}. W.l.o.g. (since ρ_{A′} is OBS-surjective) we can restrict at-

tention to the case where Γ = Γ′ and ρ = ρ_{A′}; then by Proposition 3.5 it suffices to show that [[s[x := t]]]_{ρ_{A′},A′}= [[s[x := t′]]]_{ρ_{A′},A′}. Now consider the observable equation φ =_{def} s[x := t] =_{b′} s[x := t′]. We have A ⊧_{ρ_{A}} φ since [[t]]_{ρ_{A},A}≈_{OBS,A,b} [[t′]]_{ρ_{A},A}; then A′ ⊧_{ρ_{A′}} φ since A ≡_{OBS} A′. Hence [[s[x := t]]]_{ρ_{A′},A′}= [[s[x := t′]]]_{ρ_{A′},A′} by Proposition 3.7. ⟸: Similarly. □ (lemma)

Now define a function h : A/≈_{OBS,A} → A′/≈_{OBS,A′} by taking h([v]_{≈_{OBS,A}}) = [[[t]]_{ρ_{A′},A′}]_{≈_{OBS,A′}} for b ∈ B and v ∈ [[b]]_{A}, where t is a term in context Γ such that [[t]]_{ρ_{A},A}= v. We know that such a t exists because v is OBS-reachable by definition of ≈_{OBS,A} and because ρ_{A} is OBS-surjective. To see that the choice of the term t and the representative v don’t matter, suppose we have terms t, t′ in context Γ such that [[t]]_{ρ_{A},A}= v ≈_{OBS,A,b} v′ = [[t′]]_{ρ_{A},A}; then [[t]]_{ρ_{A′},A′}≈_{OBS,A′,b} [[t′]]_{ρ_{A′},A′} by the lemma. Thus h is well-defined, and it is easy to see that h is a Σ-homomorphism. Since our signatures do not contain predicate symbols, h is a Σ-isomorphism if we can prove that it is bijective.

To see that h is surjective, consider any b ∈ B and representative v of any congruence class in [[b]]_{A′/≈_{OBS,A′}}. Pick a term t in context Γ such that [[t]]_{ρ_{A′},A′}= v; we know that such a t exists because v is OBS-reachable (since v ≈_{OBS,A′} v) and because ρ_{A′} is OBS-surjective. Then [v]_{≈_{OBS,A′}} = h([[[t]]_{ρ_{A},A}]_{≈_{OBS,A}}).

To see that h is injective, suppose there are b ∈ B and v, v′ ∈ [[b]]_{A} such that h([v]_{≈_{OBS,A}}) = h([v′]_{≈_{OBS,A}}), where t, t′ are terms in context Γ such that [[t]]_{ρ_{A},A}= v and [[t′]]_{ρ_{A},A}= v′. Then [[t]]_{ρ_{A′},A′}≈_{OBS,A′} [[t′]]_{ρ_{A′},A′}, so by the lemma we have [[t]]_{ρ_{A},A}≈_{OBS,A} [[t′]]_{ρ_{A},A}, i.e. [v]_{≈_{OBS,A}} = [v′]_{≈_{OBS,A}}.

Thus we have shown that h : A/≈_{OBS,A} → A′/≈_{OBS,A′} is a Σ-isomorphism. Note that its inverse can be obtained from the proof of surjectivity. □

Example 4.16 Since Nat ≡_{{bool}} Term ≡_{{bool}} Term^{∞} (Example 4.12), by Proposition 4.15 Nat/≈_{{bool},Nat} ≅ Term/≈_{{bool},Term} ≅ Term^{∞}/≈_{{bool},Term^{∞}} (Example 3.34, see also Example 4.2). □

Proposition 4.15 essentially amounts to one direction of Example 5.4 of [BHW95], where the proof method is the same.

In this paper, we consider only the particular definitions of indistinguishability (Definition 4.1) and behavioural equivalence (Definition 4.11) given above. There are at least two other candidates for each of these definitions, as described in [BHW95]. The first variant, which has been studied by [Rei85], is obtained by allowing Γ to be an arbitrary B-context in both definitions, removing the requirement of OBS-reachability in Definition 4.1, and changing the requirement of OBS-surjectivity to B-surjectivity in Definition 4.11. The second variant is obtained by eliminating the context Γ and environments from both definitions, and changing the requirement of OBS-reachability to ∅-reachability in Definition 4.1; the resulting definition of behavioural equivalence has been studied in Section 2 of [ST87]. These alternatives are not studied here, although all of the proofs required should be similar to those given here. In our opinion, the first variant is simply wrong because the resulting behavioural equivalence relation fails to identify algebras that differ only in their behaviour on values of non-observable types that are not OBS-reachable: see [ONS91] for an example. The second variant seems to be unnecessarily restrictive in the presence of parameterised specifications, since (as discussed in [ST89]) OBS will normally include the parameter types and these types typically lack generators; this leads to a behavioural equivalence relation that is too coarse.

Schoett [Sch90] has shown that A ≡_{OBS} A′ iff there exists an OBS-correspondence between A and A′ (a family of relations ⟨↔_{b} ⊆ [[b]]_{A}×[[b]]_{A′}⟩_{b∈B} such that for all c : b_{1} × ⋯ × b_{n} → b in C and all v_{1} ∈ [[b_{1}]]_{A}, …, v_{n} ∈ [[b_{n}]]_{A} and v′_{1} ∈ [[b_{1}]]_{A′}, …, v′_{n} ∈ [[b_{n}]]_{A′}, if v_{1} ↔_{b_{1}} v′_{1} and ⋯ and v_{n} ↔_{b_{n}} v′_{n} then [[c]]_{A}(v_{1}, …, v_{n}) ↔_{b} [[c]]_{A′}(v′_{1}, …, v′_{n}), and such that ↔_{b} is a bijection for b ∈ OBS).^{4} This characterization is useful for proving that specific algebras are

4 In fact, the definition of A ≡_{OBS} A′ in [Sch90] requires [[b]]_{A}= [[b]]_{A′} for all b ∈

behaviourally equivalent. Very recently, [BT96] has generalized this result. First, they consider an arbitrary concrete category of models, rather than that of ordinary algebras, and study the concepts of behavioural satisfaction and behavioural equivalence in this context. They then generalize the characterization theorem of [Sch90] to the case of arbitrary ≈ and ≡ (satisfying certain technical conditions) such that ≡ is factorizable by ≈. They also generalize the characterization theorem of [BHW95] to this context.

5 Expressible congruences and relativization

The language of higher-order logic is powerful enough to express the indistinguishability relation ≈_{OBS} by means of a family of predicates, i.e. terms in the language (cf. [Sch94]). We can use this fact to characterize behavioural satisfaction of a formula φ in terms of ordinary satisfaction of a “relativized” version of φ.

Let Σ = ⟨B, C⟩ be a signature for which B and C are finite and let OBS ⊆ B. The assumption of finiteness is required to obtain finite terms in Proposition 5.1 and Theorem 5.4 below.

Notations like ∀_{b∈B}x_{b}:b.t and λ(⟨P_{b}:[b, b]⟩_{b∈B}).t will be used below to abbreviate obvious (finite) terms. The latter assumes some fixed enumeration of the elements of B; this is not needed for the former since a sequence of universal quantifiers can be permuted without affecting meaning.

Proposition 5.1 Let A be a Σ-algebra and suppose v̂ ∈ [[b̂]]_{A} for b̂ ∈ B. Then A ⊧_{[x↦_{v}]} REACH_{b}(x) iff v̂ is OBS-reachable, where REACH_{b} is defined as follows:

If b̂ ∈ OBS then REACH_{b} =_{def} λ(x:b̂).true.

OBS, and so there ↔_{b} is required to be equality for b ∈ OBS. Moreover, Schoett uses partial algebras where the definition of ≡_{OBS} is a little more complicated and correspondences are required to satisfy additional conditions.

If b̂ ∉ OBS then

REACH_{b} =_{def}

λ(x:b̂). ∀_{b∉OBS}P_{b} : [b].

( ∧_{{c:b_{1}×···×b_{n}→b′ in C \atop b′∉OBS}} ∀_{1≤i≤n}x_{i} : b_{i}. ( ∧_{{1≤j≤n \atop b_{j}∉OBS}}P_{b_{j}}(x_{j})) ⇒ P_{b′}(c(x_{1}, …, x_{n})))

⇒ P_{b}(x)

Proof: If b̂ ∈ OBS then the proof is trivial. So suppose that b̂ ∉ OBS.

⟹: Instantiate REACH_{b}(x) with P_{b} = {v ∈ [[b]]_{A}| v is OBS-reachable} ∈ [[[b]]]_{A} for all b ∉ OBS. It then suffices to show that the closure property on the left-hand side of the main implication is satisfied. This is easy: for each c : b_{1} × ⋯ × b_{n} → b′ in C, the required term is simply the application of c to the terms that witness the OBS-reachability of x_{1}, …, x_{n}.

⟸: Suppose that v̂ is OBS-reachable; then there is an OBS-context Γ, term t with Γ ⊢ t : b̂, and Γ-environment ρ such that [[t]]_{ρ,A}= v̂. We need to show that A ⊧_{[x↦_{v}]} REACH_{b}(x); by Proposition 3.5 it suffices to show that A ⊧_{ρ} REACH_{b}(t). This follows by induction on the structure of t. □

Example 5.2 Consider the signature Σ_{ctr} and let OBS = {bool}; then REACH_{bool} is λ(x:bool).true and REACH_{ctr} is:

λ(x:ctr).∀P:[ctr].
(P (zero) ∧ ∀y:ctr.P (y) ⇒ P (inc(y)) ∧ ∀z:ctr.P (z) ⇒ P (dec(z)))
⇒ P (x)
□

Definition 5.3 Let ≈ = ⟨≈_{A}⟩_{A∈Alg(Σ)} be a family of partial congruences, and let ∼ = ⟨∼_{b}⟩_{b∈B} be a family of closed predicates such that ⊢ ∼_{b} : [b, b] for every base type b ∈ B. Then ≈ is expressible by ∼ if [[∼_{b}]]_{A}= ≈_{A,b} for every b ∈ B.

The formulae in the following theorem do not make easy reading. INDIST_{b} characterizes ≈_{OBS} as the greatest (∃_{b∈B}P_{b}:[b, b].P_{b}(x, y) ∧ ⋯) partial congruence (CONG(⟨P_{b}⟩_{b∈B})) that is equality on OBS (OBSEQ(⟨P_{b}⟩_{b∈B})) and is defined only for OBS-reachable values (REACH_{b}(x) ∧ REACH_{b}(y)).

Theorem 5.4 The indistinguishability relation ≈_{OBS} is expressible by the family of predicates ⟨INDIST_{b}⟩_{_{b}∈B}, defined as follows:

CONG =_{def}
λ(⟨P_{b}:[b, b]⟩_{b∈B}).

∧_{c:b_{1}×···×b_{n}→b in C} ∀_{1≤i≤n}x_{i}, x′_{i}:b_{i}.\begin{matrix}( ∧_{1≤j≤n}P_{b_{j}}(x_{j}, x′_{j})) \\ ⇒ P_{b}(c(x_{1}, …, x_{n}), c(x′_{1}, …, x′_{n})) \end{matrix}

OBSEQ =_{def} λ(⟨P_{b}:[b, b]⟩_{b∈B}). ∧_{b∈OBS}∀x, x′:b. P_{b}(x, x′) ⇔ x =_{b} x′

INDIST_{b} =_{def}

λ(x:b̂, y:b̂).∃_{b∈B}P_{b}:[b, b].P_{b}(x, y) ∧ CONG(⟨P_{b}⟩_{b∈B}) ∧ OBSEQ(⟨P_{b}⟩_{b∈B})

∧ REACH_{b}(x) ∧ REACH_{b}(y)

Proof: Let A be a Σ-algebra. We need to prove that if v̂, v̂′ ∈ [[b̂]]_{A}, then

A ⊧_{[x↦_{v},y↦_{v′}]} INDIST_{b}(x, y) iff v̂ ≈_{OBS,A,_{b}} v̂′.

⟸: Suppose that v̂ ≈_{OBS,A,_{b}} v̂′. We claim that A ⊧_{[x↦_{v},y↦_{v′}]} INDIST_{b}(x, y) with the predicates P_{b} = ≈_{OBS,A,b} ∈ [[[b, b]]]_{A} for all b ∈ B. By the assumption we have that A ⊧_{[x↦_{v},y↦_{v′}]} P_{b}(x, y); then A ⊧ CONG(⟨P_{b}⟩_{b∈B}) since ≈_{OBS,A} is a partial congruence on A (Proposition 4.3), A ⊧ OBSEQ(⟨P_{b}⟩_{b∈B}) by the definition of ≈_{OBS,A}, and A ⊧_{[x↦_{v},y↦_{v′}]} REACH_{b}(x) ∧ REACH_{b}(y) by Proposition 5.1.

⟹: Suppose that A ⊧_{[x↦_{v},y↦_{v′}]} INDIST_{b}(x, y). Then v̂ and v̂′ are OBSreachable by Proposition 5.1. It remains to show that if Γ is an OBS-context, z ∉ Vars(Γ), s is a term such that Γ, z : b̂ ⊢ s : b′ for b′ ∈ OBS, and ρ is a Γ-environment, then [[s]]_{ρ[z↦_{v}],A}= [[s]]_{ρ[z↦_{v′}],A}. This is a consequence of the following lemma:

Lemma For any OBS-context Γ, variable z ∉ Vars(Γ), term s such that

Γ, z : b̂ ⊢ s : b′, and Γ-environment ρ, ([[s]]_{ρ[z↦_{v}],A}, [[s]]_{ρ[z↦_{v′}],A}) ∈ P_{b′}.

Proof: By induction on the structure of s. Suppose that s is a variable but not z; then b′ ∈ OBS since Γ is an OBS-context, and the required property follows from the fact that A ⊧ OBSEQ(⟨P_{b}⟩_{b∈B}). Suppose that s is z; then the required property follows directly from the fact that A ⊧_{[x↦_{v},y↦_{v′}]} P_{b}(x, y). Suppose that s is a function application; then the required property follows from the inductive assumption and the fact that A ⊧ CONG(⟨P_{b}⟩_{b∈B}). □ (lemma)

From this, together with the fact that A ⊧ OBSEQ(⟨P_{b}⟩_{b∈B}) and Proposition 3.7, it follows that [[s]]_{ρ[z↦_{v}],A}= [[s]]_{ρ[z↦_{v′}],A} when b′ ∈ OBS. □

Example 5.5 Consider the signature Σ_{ctr} and let OBS = {bool}; then INDIST_{bool} simplifies to λ(x:bool, y:bool).x =_{bool} y and INDIST_{ctr} simplifies to:

λ(x:ctr, y:ctr).
REACH_{ctr}(x) ∧ REACH_{ctr}(y)
∧ ∃P:[ctr, ctr].P (zero, zero) ∧ ∀a, b:ctr. P (a, b) ⇒ P (inc(a), inc(b)) ∧ P (dec(a), dec(b)) ∧ is-zero(a) =_{bool} is-zero(b) ∧ P (x, y)

This can be used to show that zero ≈_{{bool},Term} dec(inc(zero)) (and similarly for ≈_{{bool},Term^{∞}}) by taking

P = {(v, v′) | v = v′ ∨ ∃t. x : ctr ⊢ t : ctr ∧ v = t[zero] ∧ v′ = t[dec(inc(zero))]}.

where t[t′] is shorthand for [[t]]_{[x↦t′],Term}. This choice of P works for showing that t[zero] ≈_{{bool},Term} t[dec(inc(zero))] for any “context” t, but a different choice of P is required for showing that dec(inc(zero)) ≈_{{bool},Term} zero or zero ≈_{{bool},Term} dec(dec(inc(inc(zero)))). □

In [Sch94] an expressibility result analogous to Theorem 5.4 for the indistinguishability relation used in [Rei85] is given for a language of second-order logic. Detailed comparisons are rendered difficult by the fact that the logic used there is untyped. Very recently, [BT96] has shown that regularity (Proposition 4.7 above), among other properties of ≈_{OBS}, follows from the characterization of ≈_{OBS} as the greatest partial congruence that is equality on OBS and is defined only for OBS-reachable values.

Let ≈ = ⟨≈_{A}⟩_{A∈Alg(Σ)} be a family of partial congruences that is expressible by the family of predicates ∼ = ⟨∼_{b}⟩_{b∈B}.

Definition 3.17 showed how to extend a partial congruence to bracket types. We can express exactly the same thing for any expressible congruence.

Proposition 5.6 For any type τ there is a closed predicate ∼_{τ} such that ⊢ ∼_{τ} : [τ, τ] and [[∼_{τ}]]_{A}= ≈_{A,τ}, given by the following definition: If τ = b ∈ B then ∼_{τ} =_{def} ∼_{b}. If τ = [τ_{1}, …, τ_{n}] then

∼_{τ} =_{def}
λ(p:[τ_{1}, …, τ_{n}], p′:[τ_{1}, …, τ_{n}]).

∀_{1≤i≤n}x_{i}, x′_{i}:τ_{i}. ( ∧_{1≤j≤n}x_{j} ∼_{τ_{j}} x′_{j}) ⇒ (p(x_{1}, …, x_{n}) ⇔ p′(x′_{1}, …, x′_{n}))

(The definition of ∼_{[τ_{1},...,τ_{n}]} is recursive, but the result is a finite term for any type [τ_{1}, …, τ_{n}].) Proof: Immediate. □ This leads directly to a family of predicates characterizing the values that are in the interpretation of types w.r.t. ≈. Proposition 5.7 For any type τ there is a closed predicate DOM_{τ} such that ⊢ DOM_{τ} : [τ] and [[DOM_{τ}]]_{A}= [[τ]]_{A}^{≈_{A}}, given by the following definition: If τ = b ∈ B then DOM_{τ} =_{def} λ(x:b).x ∼_{b} x. If τ = [τ_{1}, …, τ_{n}] then

DOM_{τ} =_{def}
λ(p:[τ_{1}, …, τ_{n}]).

p ∼_{[τ_{1},...,τ_{n}]} p ∧ ∀_{1≤i≤n}x_{i}:τ_{i}. (p(x_{1}, …, x_{n}) ⇒ ∧_{1≤j≤n}DOM_{τ_{j}}(x_{j}))

(Again, this is a recursive definition that gives a finite term for any type.) Proof: By induction on the structure of τ, using Propositions 3.22 and 5.6.

□

We can use the predicates DOM_{τ} thus defined to transform any formula φ into a formula ⌜φ⌝ such that ⌜φ⌝ is satisfied exactly when φ is satisfied w.r.t. ≈. The idea is simply to “relativize” each bound variable by attaching a requirement that the value taken on by the variable is in the interpretation of its type w.r.t. ≈. Definition 5.8 Let t be a term in context Γ. The ∼-relativization of t is the term ⌜t⌝ (in context Γ) defined as follows:

⌜x⌝ = x
⌜c(t_{1}, …, t_{n})⌝ = c(⌜t_{1}⌝, …, ⌜t_{n}⌝)
⌜λ(x_{1}:τ_{1}, …, x_{n}:τ_{n}).t⌝ = λ(x_{1}:τ_{1}, …, x_{n}:τ_{n}).

DOM_{τ_{1}}(x_{1}) ∧ ⋯ ∧ DOM_{τ_{n}}(x_{n}) ∧ ⌜t⌝

⌜t(t_{1}, …, t_{n})⌝ = ⌜t⌝(⌜t_{1}⌝, …, ⌜t_{n}⌝)
⌜t ⇒ t′⌝ = ⌜t⌝ ⇒ ⌜t′⌝
⌜∀x:τ.t⌝ = ∀x:τ.DOM_{τ}(x) ⇒ ⌜t⌝

The following results relate satisfaction of a formula to satisfaction of its relativized version.

Theorem 5.9 Let A be a Σ-algebra, Γ ⊢ t : τ and let ρ be a Γ-environment w.r.t. ≈_{A} (so ρ is also an ordinary Γ-environment by Proposition 3.22). Then [[t]]_{ρ,A}^{≈_{A}}≈_{A,τ} [[⌜t⌝]]_{ρ,A}.

Proof: By induction on the structure of the derivation of Γ ⊢ t : τ. For λ-abstraction, we use Propositions 3.27 and 5.7. For universal quantification, we use Proposition 5.7. □

Corollary 5.10 Let A be a Σ-algebra, let φ be a formula in context Γ and let ρ be a Γ-environment w.r.t. ≈_{A}. Then A ⊧_{ρ}^{≈_{A}} φ iff A ⊧_{ρ} ⌜φ⌝.

Proof: Immediate from Theorem 5.9. □

Corollary 5.11 Let A be a Σ-algebra, v, v′ ∈ [[τ]]_{A}^{≈} for some τ, and ρ be an environment w.r.t. ≈_{A}. Then [[⌜x =_{τ} y⌝]]_{ρ[x↦v,y↦v′],A}= [[x ∼_{τ} y]]_{ρ[x↦v,y↦v′],A}.

Proof: [[⌜x =_{τ} y⌝]]_{ρ[x↦v,y↦v′],A}= [[x =_{τ} y]]_{ρ[x↦v,y↦v′],A}^{≈_{A}} (by Theorem 5.9, since ≈_{A,[ ]} is equality) = (v ≈_{A,τ} v′) (by Proposition 3.29) = [[x ∼_{τ} y]]_{ρ[x↦v,y↦v′],A} (by Proposition 5.6). □

Example 5.12 Let φ be the Σ_{ctr}-formula ∀c:ctr.dec(inc(c)) =_{ctr} c; then ⌜φ⌝ is ∀c:ctr.DOM_{ctr}(c) ⇒ ∀P:[ctr].DOM_{[ctr]}(P) ⇒ P (dec(inc(c))) ⇒ P (c). This is equivalent to ∀c:ctr.DOM_{ctr}(c) ⇒ INDIST_{ctr}(dec(inc(c)), c) by Corollary 5.11. Let OBS = {bool}. In Term^{∞}, the effect of restricting to values c such that DOM_{ctr}(c) is to ignore ∞, and the effect of restricting to predicates P such that DOM_{[ctr]}(P) is to consider only predicates that respect ≈_{{bool},Term^{∞}}, disregarding e.g. P in Example 3.18. Since Term^{∞} ⊧^{≈} φ (Example 3.31), Corollary 5.10 says that Term^{∞} ⊧ ⌜φ⌝. □

The definition of the ∼-relativization of a formula is closely related to the definition of “lifted” formula in [BH96], and Corollary 5.10 is a higher-order version of Theorem 4.2(i) in [BH96].

Corollary 5.13 Let A, A′ be Σ-algebras such that A/≈_{A} ≅ A′/≈_{A′}, and let φ be a closed formula. Then A ⊧ ⌜φ⌝ iff A′ ⊧ ⌜φ⌝.

Proof: A ⊧ ⌜φ⌝ iff A ⊧^{≈_{A}} φ (by Corollary 5.10, since φ is closed) iff A/≈_{A} ⊧ φ (by Theorem 3.35) iff A′/≈_{A′} ⊧ φ (by Corollary 3.14) iff A′ ⊧^{≈_{A′}} φ iff A′ ⊧ ⌜φ⌝. □

The relativization construction may be used to define another behavioural equivalence relation, in which two algebras are regarded as behaviourally equivalent provided they cannot be distinguished by relativized formulae. The motivation for this apparent departure from our earlier notion of behavioural equivalence is that it is a convenient technical device for proving left-factorizability of ≡_{OBS} by ≈_{OBS} (Corollary 5.16), since this follows directly from left-factorizability of this new relation by ≈_{OBS} (Theorem 5.15). In fact, it will turn out (Corollary 5.22) that this “new” relation coincides with ≡_{OBS}.

Definition 5.14 Let A, A′ ∈ Alg(Σ). A is behaviourally equivalent to A′ via relativized formulae, written A ≡_{RelForm} A′, if there is an OBS-context Γ and Γ-environments ρ_{A} on A and ρ_{A′} on A′ that are OBS-surjective such that for any formula φ in context Γ, A ⊧_{ρ_{A}} ⌜φ⌝ iff A′ ⊧_{ρ_{A′}} ⌜φ⌝, where ⌜φ⌝ is the ⟨INDIST_{b}⟩_{b∈B}-relativization of φ.

Theorem 5.15 For any A, A′ ∈ Alg(Σ), if A/≈_{OBS,A} ≅ A′/≈_{OBS,A′} then A ≡_{RelForm} A′.

Proof: Let h : A/≈_{OBS,A} → A′/≈_{OBS,A′} be an isomorphism. Since ≈_{OBS} is equality on b ∈ OBS, we have a bijection ĥ_{b} : [[b]]_{A}→ [[b]]_{A′} for b ∈ OBS defined by [ĥ_{b}(v)]_{≈_{OBS,A′,b}} = h_{b}([v]_{≈_{OBS,A,b}}) for v ∈ [[b]]_{A}.

Let Γ be the OBS-context such that Γ_{b} = [[b]]_{A} for every b ∈ OBS (w.l.o.g. we assume that [[b]]_{A}⊆ X and that [[b]]_{A} and [[b′]]_{A} are disjoint for b ≠ b′). Define an OBS-surjective Γ-environment ρ_{A} on A by ρ_{A}(x) = x. Define an OBS-surjective Γ-environment ρ_{A′} on A′ by ρ_{A′}(x) = ĥ(x). Since ≈_{OBS} is equality on b ∈ OBS, ρ_{A} (resp. ρ_{A′}) is also a Γ-environment w.r.t. ≈_{OBS} on A (resp. A′). Let φ be a formula in context Γ. Then A ⊧_{ρ_{A}} ⌜φ⌝ iff A ⊧_{ρ_{A}}^{≈_{OBS,A}} φ (by Corollary 5.10) iff A/≈_{OBS,A} ⊧_{ψ∘ρ_{A}} φ (by the lemma in the proof of Theorem 3.35, where ψ is the function from that proof, since ψ_{[ ]} is the identity) iff A′/≈_{OBS,A′} ⊧_{h∘ψ∘ρ_{A}} φ (by Proposition 3.13, since h_{[ ]} is the identity) iff A′/≈_{OBS,A′} ⊧_{ψ∘ρ_{A′}} φ (since h ∘ ψ ∘ ρ_{A} = ψ ∘ ĥ ∘ ρ_{A}) iff A′ ⊧_{ρ_{A′}}^{≈_{OBS,A′}} φ iff A′ ⊧_{ρ_{A′}} ⌜φ⌝. □

Corollary 5.16 For any A, A′ ∈ Alg(Σ), if A/≈_{OBS,A} ≅ A′/≈_{OBS,A′} then A ≡_{OBS} A′.

Proof: Observe that for any equation φ ∈ ObsEq_{Γ}(Σ), φ ⊧| ⌜φ⌝ since the extra premise in ⌜φ⌝ always holds, by an easy argument involving Proposition 5.7. Then just apply Theorem 5.15. □

Example 5.17 To get an example of Corollary 5.16, just turn Example 4.16 around: since Nat/≈_{{bool},Nat} ≅ Term/≈_{{bool},Term} ≅ Term^{∞}/≈_{{bool},Term^{∞}} (Example 3.34) we obtain Nat ≡_{{bool}} Term ≡_{{bool}} Term^{∞} (Example 4.12).

□

Yet another definition of behavioural equivalence is obtained by extending the definition of ≡_{OBS} to take advantage of the availability of higher-order formulae to perform experiments.

Definition 5.18 A type τ is observable if either:

– τ is a base type that is in OBS; or

– τ = [τ_{1}, …, τ_{n}] and τ_{i} is observable for all 1 ≤ i ≤ n.

Let Γ be a context. A term t in context Γ is observation-restricted if all types occurring in t (i.e. as types of bound variables in λ-abstractions and universal quantifications) are observable. If t is a formula and Γ is an OBS-context then t is called observable. Let ObsForm_{Γ}(Σ) be the set of observable formulae in context Γ.

Since predicates in formulae can only arise in two ways — via λ-abstraction and via quantification — the restrictions imposed on observable formulae ensure that predicates in such formulae always have observable type. Note that ObsEq_{Γ}(Σ) ⊂ ObsForm_{Γ}(Σ).

Definition 5.19 Let A, A′ ∈ Alg(Σ). A is behaviourally equivalent to A′ via formulae, written A ≡_{OBSForm} A′, if there is an OBS-context Γ and Γenvironments ρ_{A} on A and ρ_{A′} on A′ that are OBS-surjective such that for any formula φ ∈ ObsForm_{Γ}(Σ), A ⊧_{ρ_{A}} φ iff A′ ⊧_{ρ_{A′}} φ.

Left-factorizability of ≡_{OBSForm} by ≈_{OBS} is another direct consequence of Theorem 5.15.

Corollary 5.20 For any A, A′ ∈ Alg(Σ), if A/≈_{OBS,A} ≅ A′/≈_{OBS,A′} then A ≡_{OBSForm} A′.

Proof: For any observable type τ, v ≈_{OBS,A,τ} v for any v ∈ [[τ]]_{A}, by induction on the structure of τ using Proposition 5.6. From this it follows that for any φ ∈ ObsForm_{Γ}(Σ), φ ⊧| ⌜φ⌝. Then apply Theorem 5.15. □

Theorem 5.21 ≡_{RelForm}, ≡_{OBS} and ≡_{OBSForm} are factorizable by ≈_{OBS}.

Proof:

≡_{RelForm}: By Proposition 4.15 (since ≡_{RelForm} ⊆ ≡_{OBS} by an argument like

the one in Corollary 5.16) and Theorem 5.15. ≡_{OBS}: By Proposition 4.15 and Corollary 5.16. ≡_{OBSForm}: By Proposition 4.15 (since ≡_{OBSForm} ⊆ ≡_{OBS}) and Corollary 5.20.

□

It is an easy consequence of the above theorem that all three of our behavioural equivalence relations coincide. This demonstrates that using formulae more complex than equations as experiments does not allow finer distinctions between algebras to be made. This is not necessarily what one would expect: in the case of non-deterministic algebras, the use of more complex formulae does yield a different relation, see [Nip88].

Corollary 5.22 ≡_{RelForm} = ≡_{OBS} = ≡_{OBSForm}.

Proof: Immediate from Theorem 5.21 and the definition of factorizability. □

6 Relating abstractor specifications and behavioural specifications

As discussed in the introduction, ordinary specifications consisting of a signature together with a set of axioms are not sufficiently abstract in that they sometimes describe classes of algebras that are not closed under behavioural equivalence. Two approaches to resolving this problem have been proposed. The first, due to [SW83], is to simply close the class of models of a specification under behavioural equivalence using an operation called behavioural abstraction. The second, due to [Rei85], is to take as models of a specification all those algebras that behaviourally satisfy the axioms. We provide syntax for all three kinds of specifications here in order to study how they are related.

Definition 6.1 A (flat) specification consists of a signature Σ and a set Φ of closed Σ-formulae, called axioms. The models of a specification ⟨Σ, Φ⟩ are all the algebras in the class

Mod(⟨Σ, Φ⟩) = {A ∈ Alg(Σ) | A ⊧ Φ}.

Let ⟨Σ, Φ⟩ be a specification. Let ≈ = ⟨≈_{A}⟩_{A∈Alg(Σ)} be a family such that each ≈_{A} is a partial congruence on A, and let ≡ ⊆ Alg(Σ) × Alg(Σ) be an equivalence relation.

Definition 6.2 For any class A ⊆ Alg(Σ), the closure of A under ≡ is the class

Abs_{≡}(A) = {A ∈ Alg(Σ) | A ≡ A′ for some A′ ∈ A}.

When ≡ is the relation ≡_{OBS} for some set OBS of base types, the operator Abs_{≡} is known as behavioural abstraction.

A (flat) abstractor specification abstract ⟨Σ, Φ⟩ w.r.t. ≡ has as models all those Σ-algebras that are equivalent to models of ⟨Σ, Φ⟩:

Mod(abstract ⟨Σ, Φ⟩ w.r.t. ≡) = Abs_{≡}(Mod(⟨Σ, Φ⟩)).

Definition 6.3 A (flat) behavioural specification behaviour ⟨Σ, Φ⟩ w.r.t. ≈ has as models all those Σ-algebras that satisfy the axioms Φ w.r.t. ≈:

Mod(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) = {A ∈ Alg(Σ) | A ⊧^{≈_{A}} Φ}.

The notation used for behavioural specifications should not be confused with similar notation used in [SW83] and [ST87] for a particular special case of abstractor specifications.

Example 6.4 ⟨Σ_{ctr}, Φ_{ctr}⟩ is a specification having as models the class of all Σ_{ctr}-algebras that are isomorphic to Nat. abstract ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≡_{{bool}} is an abstractor specification having as models Nat, Term, Term^{∞}, all Σ_{ctr}-algebras that are isomorphic to one of these, and many other Σ_{ctr}-algebras besides. behaviour ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≈_{{bool}} is a behavioural specification having the same class of models. □

We have now built up enough machinery to redo the development in [BHW95] in the framework of higher-order logic. Although it is not made explicit there, their results are independent of the logic used in axioms, provided properties corresponding to Corollary 3.14 and Theorem 3.35 hold for the logic of interest. In the remainder of this section we merely state the most important theorems and indicate dependencies; for proofs, more results, and discussion, see [BHW95].

The theorems below are stated for arbitrary choices of ≈ and ≡ such that ≈ is regular or weakly regular and ≡ is factorizable by ≈. The particular case of interest is where ≈ and ≡ are ≈_{OBS} and ≡_{OBS} respectively, for an arbitrary choice OBS of observable base types, which satisfy the requirements by Propositions 4.7 and 4.9, and Theorem 5.21.

Theorem 6.5 ([BHW95]) If ≈ is regular and ≡ is factorizable by ≈, then Mod(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) = Abs_{≡}(FA_{≈}(Mod(⟨Σ, Φ⟩))).

Proof: See [BHW95]. The proof depends on Theorem 3.35 and Corollary 3.14, and the fact that regularity and factorizability implies A ≡ A/≈_{A} for any A.

□

Theorem 6.6 ([BHW95]) If ≈ is weakly regular and ≡ is factorizable by ≈, then Mod(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) ⊆ Mod(abstract ⟨Σ, Φ⟩ w.r.t. ≡).

Proof: See [BHW95]. The proof depends on Theorem 3.35. □

Note that if the requirement of weak regularity of ≈ is slightly strengthened to regularity, then Theorem 6.6 is an immediate corollary of Theorem 6.5.

The main characterization theorem is the following:

Theorem 6.7 ([BHW95]) Suppose ≈ is weakly regular and ≡ is factorizable by ≈. The following conditions are equivalent:

(i) Mod(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) = Mod(abstract ⟨Σ, Φ⟩ w.r.t. ≡) (ii) Mod(⟨Σ, Φ⟩) ⊆ Mod(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) (iii) For all A ∈ Mod(⟨Σ, Φ⟩), A/≈_{A} ∈ Mod(⟨Σ, Φ⟩)

Proof: See [BHW95]. The proof depends on Theorems 3.35 and 6.6 and Corollary 3.14. □

Example 6.8 According to Theorem 6.7, the fact that the model class Mod(abstract ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≡_{{bool}}) coincides with the model class Mod(behaviour ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≈_{{bool}}) (Example 6.4) follows from the fact that for all A ∈ Mod(⟨Σ_{ctr}, Φ_{ctr}⟩), A/≈_{A} ∈ Mod(⟨Σ_{ctr}, Φ_{ctr}⟩). The latter holds because the only model of ⟨Σ_{ctr}, Φ_{ctr}⟩ is (up to isomorphism) Nat, which is ≈_{{bool}}-fully abstract (Example 4.6) and is hence isomorphic to its quotient by ≈_{{bool},Nat}.

Now consider the signature Σ′_{ctr} obtained by adding a constant zero′ : ctr to Σ_{ctr}, and the set of axioms Φ′_{ctr} obtained by adding the formula ¬(zero =_{ctr} zero′) to Φ_{ctr} and removing the formula GENCTR. Let Nat′ be the Σ′_{ctr}- algebra consisting of “two copies of Nat”, defined by taking [[ctr]]_{Nat}_{′}= ω ⊎ ω and the obvious interpretation of the constants such that [[zero]]_{Nat}_{′}≠ [[zero′]]_{Nat}_{′} and [[is-zero(zero)]]_{Nat}_{′}= [[is-zero(zero′)]]_{Nat}_{′}= T. Then Nat′ ∈ Mod(⟨Σ′_{ctr}, Φ′_{ctr}⟩) and so Nat′ ∈ Mod(abstract ⟨Σ′_{ctr}, Φ′_{ctr}⟩ w.r.t. ≡_{{bool}}). On the other hand, Nat′ ∉ Mod(behaviour ⟨Σ′_{ctr}, Φ′_{ctr}⟩ w.r.t. ≈_{{bool}}) since Nat′ |̸=^{≈_{_{Nat}′}} ¬(zero =_{ctr} zero′), and this is because there is no context which allows us to distinguish [[zero]]_{Nat}_{′} and [[zero′]]_{Nat}_{′}. Thus we see that conditions (i) and (ii) of Theorem 6.7 are not satisfied. Condition (iii) is also not satisfied since Nat′/≈_{Nat}′ is isomorphic to Nat augmented by taking [[zero′]]_{Nat}_{′}= [[zero]]_{Nat}_{′}, which does not satisfy ¬(zero =_{ctr} zero′). □

7 Reasoning about specifications

The results presented above serve to clarify our understanding of behavioural satisfaction and behavioural equivalence and the relationship between these in the context of higher-order logic. A concrete benefit of this is a number of methods for reasoning about specifications, as will be summarized below. Some of these appear in a different form in [BH96] or elsewhere, while others (Proof Methods 7.5, 7.8 and 7.10) are new.

We begin by introducing some (mostly standard) concepts and notation. Let Σ = ⟨B, C⟩ be a signature. In this section we restrict attention to closed formulae.

Definition 7.1 A closed formula φ is a consequence of a set Φ of closed formulae, written Φ ⊧ φ, if for any Σ-algebra A, A ⊧ Φ implies A ⊧ φ.

When reasoning about a specification SP, our goal is to discover whether or not a given formula φ is satisfied by all models of SP. Let ≈ = ⟨≈_{A}⟩_{A∈Alg(Σ)} be a family of partial congruences. A related goal is that of discovering whether or not φ is satisfied w.r.t. ≈ by all models of SP. These questions amount to determining whether or not φ is in the theory (resp. theory w.r.t. ≈) of SP.

Definition 7.2 Let A ⊆ Alg(Σ) be a class of Σ-algebras. The theory w.r.t. ≈ of A is the set Th_{≈}(A) = {φ | A ⊧^{≈_{A}} φ for every A ∈ A}. The (ordinary) theory of A is the set Th(A) = {φ | A ⊧ φ for every A ∈ A}; note that Th(A) = Th_{=}(A). If SP is a specification, we write Th(SP) for Th(Mod(SP)) and Th_{≈}(SP) for Th_{≈}(Mod(SP)).

The essence of reasoning about specifications is to find a way of reducing the problems of determining φ ∈ Th(SP) and φ ∈ Th_{≈}(SP) to that of consequence (Φ ⊧ ψ for appropriate Φ and ψ); then any proof system that is sound for ⊧ may be used to finish the job. For the ordinary theory of a flat specification, the reduction is trivial: φ ∈ Th(⟨Σ, Φ⟩) iff Φ ⊧ φ. For the theory w.r.t. ≈ and for behavioural specifications and abstractor specifications, the problem is much more difficult. We consider each case below, giving proof methods that provide such reductions. Some cases have particular importance, as indicated below, while others are treated only for the sake of completeness and/or because the important cases are reducible to these under certain conditions.

Let ≈ be expressible by the family of predicates ∼ = ⟨∼_{b}⟩_{b∈B}, and let ≡ ⊆ Alg(Σ) × Alg(Σ) be an equivalence relation.

7.1 φ ∈ Th(behaviour ⟨Σ, Φ⟩ w.r.t. ≈)

This problem can be reduced to ordinary consequence by applying the following easy consequence of Corollary 5.10:

Proposition 7.3 Mod(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) = Mod(⟨Σ, ⌜Φ⌝⟩) where ⌜Φ⌝ = {⌜φ⌝ | φ ∈ Φ}. □

This leads to the following proof method:

Proof Method 7.4 φ ∈ Th(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) iff ⌜Φ⌝ ⊧ φ. □

If ≈ is weakly regular and ≡ is factorizable by ≈, then any behavioural specification is at least as restrictive as the corresponding abstractor specification by Theorem 6.6. Thus, under these conditions the proof methods in Section 7.2 below (i.e. Proof Methods 7.5–7.10) may be soundly applied to this problem.

7.2 φ ∈ Th(abstract ⟨Σ, Φ⟩ w.r.t. ≡)

This is the problem that is of importance for reasoning about specifications in a language like ASL [SW83] that includes a specification-building operation corresponding to abstract; cf. [Far92].

If Theorem 6.7 applies, this problem can be reduced to the problem treated in Section 7.1 above. Then Proof Method 7.4 is applicable.

Alternatively, if the formula to be proved is a relativized formula or is logically equivalent to such a formula, Corollary 5.13 yields the following reduction.

Proof Method 7.5 Suppose that ≡ is factorizable by ≈ and φ is equivalent to a relativized formula, i.e. φ ⊧| ⌜ψ⌝ for some (closed) formula ψ. Then Φ ⊧ φ implies φ ∈ Th(abstract ⟨Σ, Φ⟩ w.r.t. ≡).

Proof: Suppose A ∈ Mod(abstract ⟨Σ, Φ⟩ w.r.t. ≡), i.e. there is some algebra A′ such that A′ ∈ Mod(⟨Σ, Φ⟩) and A ≡ A′, and Φ ⊧ φ. But then A′ ⊧ φ, so A′ ⊧ ⌜ψ⌝, and then A ⊧ ⌜ψ⌝ (by factorizability and Corollary 5.13) so A ⊧ φ. □

This is a direct extension of the method for reasoning about abstractor specifications presented in Section 4 of [ST87], which applies only to formulae built in certain ways from observable equations. By analogy with an observation there, Proof Method 7.5 is not confined to inferring formulae that are equivalent to relativized formulae. In order to validly conclude that φ ∈ Th(abstract ⟨Σ, Φ⟩ w.r.t. ≡), it is enough to have a proof of Φ ⊧ φ for which there is a “horizontal cut” containing only formulae that are equivalent to relativized formulae. Similar remarks apply to the proof methods presented below. In applying Proof Method 7.5, we normally (as in the example below) take ψ to be φ, but this is not required. A formula that is equivalent to its own relativization is called a “≈-invariant” formula in [BH96], but this concept is not used as the basis of a reasoning method there.

Example 7.6 Suppose that ⟨Σ_{nat}, Φ_{nat}⟩ specifies the natural numbers with the usual constants (at least 0, 1 and +) and the usual axioms. Now consider the specification:

Counter =_{def} abstract ⟨Σ_{ctr} ∪ Σ_{nat}, Φ_{ctr} ∪ Φ_{nat}⟩ w.r.t. ≡_{{bool,nat}}

Our aim is to prove the property

∀n, m:nat.n < m ⇒ is-zero(mdec(n, minc(m, zero))) =_{bool} false

where the functions minc and mdec (multiple inc/dec) are defined recursively “on top of” the specification Counter by the following ML-like code:

fun minc(0, c) = c

| minc(n + 1, c) = minc(n, inc(c)) fun mdec(0, c) = c

| mdec(n + 1, c) = mdec(n, dec(c))

and < (less than) is as usual.

Our framework admits neither structured specifications nor quantification over functional types (see Section 8 for comments on both of these omissions), which rules out the obvious ways of expressing the above problem. But we can encode it using predicates as follows:

φ =_{def} ∀n, m:nat.n < m ⇒

∀c, c′:ctr.Minc(m, zero, c) ∧ Mdec(n, c, c′) ⇒ is-zero(c′) =_{bool} false where <, Minc, and Mdec are predicates defined as follows:

< =_{def} λ(n:nat, m:nat).∀P:[nat, nat].
(∀x:nat.P (0, x + 1)) ∧ (∀x, y:nat.P (x, y) ⇒ P (x + 1, y + 1))
⇒ P (n, m)
Minc =_{def} λ(n:nat, c:ctr, c′:ctr).∀P:[nat, ctr, ctr].

(∀t:ctr.P (0, t, t)) ∧ (∀x:nat.∀t, v:ctr.P (x, inc(t), v) ⇒ P (x + 1, t, v))

⇒ P (n, c, c′)
Mdec =_{def} λ(n:nat, c:ctr, c′:ctr).∀P:[nat, ctr, ctr].

(∀t:ctr.P (0, t, t)) ∧ (∀x:nat.∀t, v:ctr.P (x, dec(t), v) ⇒ P (x + 1, t, v))

⇒ P (n, c, c′)

Our goal is to establish φ ∈ T h(Counter). Proof Method 7.5 says that this follows if we can establish that Φ_{ctr} ∪Φ_{nat} ⊧ φ and φ ⊧| ⌜ψ⌝ for some formula ψ. The former follows by induction on n. For the latter we first establish that Minc and Mdec are compatible with ≈_{{bool,nat}} in the sense that whenever Minc(n, c, c′) and c ≈_{{bool,nat}} d then we can find d′ such that Minc(n, d, d′) and c′ ≈_{{bool,nat}} d′, and similarly for Mdec. Using this property we can characterize ⌜Minc⌝ and ⌜Mdec⌝ as the ≈_{{bool,nat}}-closures of Minc and Mdec respectively. φ ⊧ ⌜φ⌝ then follows from this and the compatibility property using the fact that the final conclusion of φ is observable and thus respects ≈_{{bool,nat}}. For the converse ⌜φ⌝ ⊧ φ one uses the characterization of ⌜Minc⌝ and ⌜Mdec⌝ directly.

This problem is taken from Section 5 of [Sch92] where it is shown that an infinite number of applications of the proof method in [ST87] would be required in a proof of the property given above. □

Convenient use of Proof Method 7.5 requires a syntactic criterion which enables us to conclude φ ⊧| ⌜φ⌝ directly from the form of φ rather than via a semantic argument as in the above example. It appears, however, that the above line of reasoning is independent of the particular definition of the functions minc and mdec and thus should generalize to other recursively defined local functions. Indeed, we believe that one has φ ⊧| ⌜φ⌝ for any formula φ that arises from an encoding of a formula having a form like ∀f:τ.⟨recursive definition of f⟩ ⇒ ψ where τ is a functional type and ψ ⊧| ⌜ψ⌝, but we leave this question to future research — see Section 8.1. For the time being we content ourselves with a simpler but useful syntactic criterion that does not apply directly to the above example. This is obtained by adding “respectful” abstraction λ^{r} and quantification ∀^{r} to the syntax, where:

λ^{r}(x_{1}:τ_{1}, …, x_{n}:τ_{n}).t abbreviates λ(x_{1}:τ_{1}, …, x_{n}:τ_{n}).

DOM_{τ_{1}}(x_{1}) ∧ ⋯ ∧ DOM_{τ_{n}}(x_{n}) ∧ t

∀^{r}x:τ.t abbreviates ∀x:τ.DOM_{τ}(x) ⇒ t

Definition 7.7 A respectful formula is a formula that may contain λ^{r} and/or ∀^{r} but does not contain λ or ∀.

It is easy to see that φ ⊧| ⌜φ⌝ for any respectful formula φ. This gives the following.

Proof Method 7.8 Suppose that ≡ is factorizable by ≈ and φ is a closed respectful formula. Then Φ ⊧ φ implies φ ∈ Th(abstract ⟨Σ, Φ⟩ w.r.t. ≡).

□

In the case of behavioural abstraction, note that ∀^{r} on base types corresponds exactly to reachable quantification as in [Sch92].

Example 7.9 Consider the binary predicate on ctr that determines if one value can be obtained from another by application of inc:

comes-after(x:ctr, y:ctr) = “∃n ≥ 0.inc^{n}(y) =_{ctr} x”

This can be expressed in our framework as follows:

comes-after =_{def} λ(x:ctr, y:ctr).∀P:[ctr, ctr].
(∀a:ctr.P (a, a)) ∧ (∀a:ctr.P (inc(a), a))
∧ (∀a, b, c:ctr.P (a, b) ∧ P (b, c) ⇒ P (a, c))
⇒ P (x, y)

Now consider the formula

φ =_{def} ∀x, y:ctr.comes-after(x, y) ∨ comes-after(y, x)

Then φ ∉ Th(abstract ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≡_{{bool}}), as can be seen by considering Term ∈ Mod(abstract ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≡_{{bool}}) (Example 6.4) and instantiating x to dec(inc(zero)) and y to zero.

Next, consider a respectful version of φ:

φ^{r} =_{def} ∀^{r}x, y:ctr.comes-after^{r}(x, y) ∨ comes-after^{r}(y, x)

where

comes-after^{r} =_{def} λ^{r}(x:ctr, y:ctr).∀^{r}P:[ctr, ctr].
(∀^{r}a:ctr.P (a, a)) ∧ (∀^{r}a:ctr.P (inc(a), a))
∧ (∀^{r}a, b, c:ctr.P (a, b) ∧ P (b, c) ⇒ P (a, c))
⇒ P (x, y)

Informally, the effect of the respectful quantifiers is to give

comes-after^{r}(x:ctr, y:ctr) = “∃n ≥ 0.inc^{n}(y) ≈_{ctr} x”

for x, y that respect ≈. Taking ≈ to be ≈_{{bool}}, the respectful quantifier over ctr in φ^{r} quantifies over the {bool}-reachable values of type ctr (so in Term^{∞}, the value ∞ is excluded). We can use Proof Method 7.8 to conclude φ^{r} ∈ Th(abstract ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≡_{{bool}}) from Φ_{ctr} ⊧ φ^{r}, since φ^{r} is a respectful formula. As observed above, this conclusion is not valid for the non-respectful version φ. □

Since every observable formula amounts to a respectful formulae (since respectful abstraction and quantification over observable types is equivalent to ordinary abstraction and quantification), we have the following:

Proof Method 7.10 Suppose that φ is a closed observable formula. Then Φ ⊧ φ implies φ ∈ Th(abstract ⟨Σ, Φ⟩ w.r.t. ≡_{OBS}). □

7.3 φ ∈ Th_{≈}(⟨Σ, Φ⟩)

This is the problem that is studied in [BH96], where it is argued that a solution to this problem provides the basis of a strategy for proving correctness of implementation steps in stepwise refinement of specifications (cf. [BH95] and “abstractor” implementations in [ST88b]).

The following proof method follows immediately from Corollary 5.10:

Proof Method 7.11 φ ∈ Th_{≈}(⟨Σ, Φ⟩) iff Φ ⊧ ⌜φ⌝. □

This is essentially the same as the solution proposed in [BH96], except that because the analogue of our Corollary 5.10 there involves infinitary formulae, more work is required to reduce the problem to one of consequence for finitary formulae.

If Theorem 6.7 applies then this problem is equivalent to the problem treated in Section 7.4 below according to the following result, taking ≡ to be the equivalence induced by ≈, i.e. such that A ≡ A′ iff A/≈_{A} ≅ A′/≈_{A′}. See Example 7.18.

Proposition 7.12 ([BHW95]) If ≡ is factorizable by ≈ then Th_{≈}(Abs_{≡}(A)) = Th_{≈}(A).

Proof: Straightforward, using Corollary 3.14 and two applications of Theorem 3.35. □

(In [BHW95], this result has an additional assumption, not used in the proof, that ≈ is weakly regular.)

7.4 φ ∈ Th_{≈}(behaviour ⟨Σ, Φ⟩ w.r.t. ≈)

Corollary 5.10 and Proposition 7.3 yield the following proof method:

Proof Method 7.13 φ ∈ Th_{≈}(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) iff ⌜Φ⌝ ⊧ ⌜φ⌝.

□

Another approach, which appears to be more powerful, is obtained by appealing to the following results:

Proposition 7.14 ([BHW95]) If ≡ is factorizable by ≈ then

Th_{≈}(Abs_{≡}(FA_{≈}(A))) = T h(FA_{≈}(A)).

Proof: By Proposition 7.12 and the definition of fully abstract algebra. □

Proposition 7.15 ([BH96])

FA_{≈}(Mod(⟨Σ, Φ⟩)) = Mod(⟨Σ, Φ ∪ {∀x, y:b.(x ∼_{b} y ⇔ x =_{b} y) | b ∈ B}⟩).

Proof: Directly from the definition of fully abstract algebra. □

These together with Theorem 6.5 (taking ≡ to be the equivalence induced by ≈) yield the following:

Proof Method 7.16 Suppose that ≈ is regular. Then φ ∈ Th_{≈}(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) iff Φ ∪ {∀x, y:b.(x ∼_{b} y ⇔ x =_{b} y) | b ∈ B} ⊧ φ. □

This is essentially the same as the method proposed in [BH96], with the proviso concerning infinitary formulae mentioned earlier.

It is worth pointing out that a weaker but very simple and potentially useful consequence of this is the following:

Proof Method 7.17 Suppose that ≈ is regular. Then φ ∈ Th_{≈}(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) if Φ ⊧ φ. □

Example 7.18 Consider the formula φ from Example 7.9. We know φ ∈ Th_{≈_{{bool}}}(behaviour ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≈_{{bool}}) by Proof Method 7.17 since Φ_{ctr} ⊧ φ. Since Theorem 6.7 applies (see Example 6.8), by Proposition 7.12 we also obtain φ ∈ Th_{≈_{{bool}}}(⟨Σ_{ctr}, Φ_{ctr}⟩). □

Finally, a more direct approach to this problem is to reduce it trivially to consequence w.r.t. ≈:

Definition 7.19 A closed formula φ is a consequence of a set Φ of closed formulae w.r.t. ≈, written Φ ⊧^{≈} φ, if for any Σ-algebra A, A ⊧^{≈_{A}} Φ implies A ⊧^{≈_{A}} φ.

Proof Method 7.20 φ ∈ Th_{≈}(behaviour ⟨Σ, Φ⟩ w.r.t. ≈) iff Φ ⊧^{≈} φ. □

Then what is required to finish the job is a proof system that is sound for ⊧^{≈}. See [Rei85], where a proof system for conditional equational logic is given that is sound for an indistinguishability relation different from ≈_{OBS}, in the context of partial algebras; see also [HW95].

7.5 φ ∈ Th_{≈}(abstract ⟨Σ, Φ⟩ w.r.t. ≡)

If ≡ is factorizable by ≈ then this problem is equivalent to the problem treated in Section 7.3 above according to Proposition 7.12. Thus Proof Method 7.11 is applicable. If Theorem 6.7 applies then Proof Methods 7.13–7.20 from Section 7.4 are applicable as well.

Example 7.21 Consider once again the formula φ from Example 7.9, and recall from Example 7.18 that φ ∈ Th_{≈_{{bool}}}(behaviour ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≈_{{bool}}) using Proof Method 7.17. Since Theorem 6.7 applies, we also obtain φ ∈ Th_{≈_{{bool}}}(abstract ⟨Σ_{ctr}, Φ_{ctr}⟩ w.r.t. ≡_{{bool}}). □

8 Further work

We consider below the treatment of functional types and structured specifications, and the potential for application of the results presented above.

8.1 Functional types

The language defined in Section 2 is higher-order because it allows quantification over predicates in addition to the usual quantification over individuals. There is however no quantification over function types or use of functions as arguments to predicates or functions, cf. e.g. [Möl87], [Mei92]. There are two reasons for wanting to include functional types. First, higher-typed functional constants in signatures permit elegant specifications both of functional data structures such as streams and λ-models, and of higher-typed constants such as map and iter. Second, (higher-typed) functions used locally in formulae allow us to express some examples in a much clearer way — compare the informal presentation in Example 7.6 with the formula that encodes it.

Higher-typed functions can be added either by encoding them in terms of what is already present in the language, or by extending the basic framework with additional primitives. A specification having a signature involving higher-typed constants can be translated into a specification with a first-order signature by closing the set of base types under a formal function space constructor ⇒, adding appropriately-typed S, K and application operators, and changing the types of constants to use ⇒ in place of → (assuming w.l.o.g. that all constants are curried). The axioms of the specification have to be translated to make the use of application explicit and to use S and K instead of λ-abstraction, and finally augmented by the usual equations constraining the interpretation of these additional operators. In addition to S and K one could also add a family of fixpoint operators (Y) to allow for recursivelydefined functions in axioms. The source language of this encoding would then resemble the framework of [Grü90], except that his logic is first-order.

Even when signatures contain only first-order constants, function types can be useful in formulae as shown by Example 7.6. Such types can be encoded using predicate types as shown there. We believe that the passage from the informal presentation to its encoding can be made more systematic, following ideas in [TvD88]; it also seems to be possible to encode uses of a description operator like Hilbert’s ι which selects values that satisfy a predicate. The interpretation we give to predicate types means that this encoding yields the full set-theoretic function space. This is in contrast to the encoding above, where carriers of “functional” types like int ⇒ int may exclude functions that are not λ-definable. We can use such types for types of variables in formulae, but the result would be different from the result of using predicate types because of this different interpretation of the function space.

Reasoning about values of functional types by explicitly expanding formulae according to an encoding is cumbersome. A more attractive alternative is to develop proof methods that work directly on the “high-level” syntax. An example would be a proof method to enable us to conclude φ ⊧| ⌜φ⌝ in Example 7.6, exploiting the fact that φ arises as the encoding of a specification involving recursively-defined functions.

Alternatively, we could extend the basic framework itself with function types. This involves giving an interpretation to such types, both in the standard case and w.r.t. a partial congruence. As we have seen above, there are different choices for the standard case. Using the full function space to interpret function types in signatures precludes examples like the specification of λ-models: postulating an injection from the full function space D → D to D admits only the trivial model. On the other hand, using the full function space to interpret functional types occurring locally in formulae seems unproblematic, and one can imagine situations in which an oracle deciding the halting problem, which would require more than just the λ-definable functions, would be useful. We might even want to provide two different function spaces, with different notations to distinguish between them. The interpretation of function types w.r.t. a partial congruence is possible but is not straightforward, since with the obvious choice, namely [[τ → τ′]]_{A}^{≈}= {f : [[τ]]_{A}^{≈}→ [[τ′]]_{A}^{≈}| ∀u, v ∈ [[τ]]_{A}^{≈}.u ≈_{A,τ} v ⇒ f(u) ≈_{A,τ′} f(v)}, Proposition 3.22 fails to hold. A solution will be presented in a future paper.

8.2 Structured specifications

We have restricted attention above to the study of flat specifications consisting of a signature together with a set of axioms. Large specifications are normally built in a structured fashion, using specification-building operations like enrich, + and derive. It is well-known that structured specifications cannot in general be reduced to equivalent flat specifications (see e.g. [ST95]), and the structure of specifications provides an interesting added dimension to the study of reasoning about specifications, implementation of specifications, etc.

An attempt to extend the characterization results to structured specifications in the context of first-order logic appears in [BHW95], where the extension of behaviour to structured specifications is a post hoc construction on the class of models of the underlying specification:

Mod(behaviour SP w.r.t. ≈) = {A ∈ Alg(Σ) | A/≈_{A} ∈ Mod(SP)}

where Σ is the signature of SP. An alternative is to interpret the specificationbuilding operations in SP in the usual way but with axioms in SP satisfied according to ⊧^{≈} rather than ⊧, along the following lines:

M̂od(behaviour SP w.r.t. ≈) = Mod_{≈}(SP)

Mod_{≈}(⟨Σ, Φ⟩) = {A ∈ Alg(Σ) | A ⊧^{≈} Φ}

Mod_{≈}(derive from SP by σ) = {A _{σ} | A ∈ Mod_{≈}(SP)}

Mod_{≈}(enrich SP by types B constants C axioms Φ) =

{A ∈ Alg(Sig(SP) ∪ ⟨B, C⟩) | A _{Sig(SP)} ∈ Mod_{≈}(SP) ∧ A ⊧^{≈} Φ}

Mod_{≈}(SP + SP′) =

{A ∈ Alg(Sig(SP) ∪ Sig(SP′)) |

A _{Sig(SP)} ∈ Mod_{≈}(SP) ∧ A _{Sig(SP′)} ∈ Mod_{≈}(SP′)}

where Sig(SP) denotes the signature of the specification SP, σ : Σ → Σ′ is a signature morphism, A′ _{σ} is the reduct of a Σ′-algebra A′ to a Σ-algebra, and A′ _{Σ} is the reduct along an inclusion Σ ↪ Σ′. If SP is a flat specification then Mod(behaviour SP w.r.t. ≈) and M̂od(behaviour SP w.r.t. ≈) coincide by Theorem 3.35. But for structured specifications they do not coincide in general. Methods for reasoning about structured specifications — see e.g. the inference rules in [ST88a] — apply to the second interpretation but appear to be inapplicable to the first. Further research is required to clarify the relationship between abstractor specifications (which generalize easily to structured specifications) and this alternative interpretation of behavioural specifications. For now, it is perhaps worth mentioning that the characterization results above should straightforwardly extend to the case of structured specifications using the extended definition of behaviour given in [BHW95].

8.3 Application of results

One of our motivations for studying behavioural semantics of specifications with higher-order formulae as axioms was a desire to apply the results in the Extended ML framework for the formal development of ML programs from specifications [ST89], [KST95]. The characterization results and reasoning methods are of direct relevance in this context: the interpretation of Extended ML interfaces involves abstractor specifications, and the logical system used for writing axioms is (a form of) higher-order logic. However, it is difficult to apply the results as they stand to Extended ML because of the lack of functional types and treatment of structured specifications discussed above.

In particular, the most obvious pertinent examples of the use of behavioural semantics in the context of higher-order logic require functional types.

Once these extensions have been carried out, we will be in a position to apply the results and proof methods to examples in Extended ML and elsewhere, which should shed considerable light on their usefulness. Without having attempted many examples, we are not yet in a position to understand the tradeoffs between the various proof methods that may be applicable in a particular situation. But in view of the size and complexity of the predicates INDIST_{b} in Theorem 5.4, it seems clear that proof methods that involve the direct manipulation of relativized formulae will not be convenient for use in practice when ≈ is the indistinguishability relation ≈_{OBS}. Here, a promising avenue is the search for more tractable predicates which correctly express ≈_{OBS} under restrictions that are acceptable in practice (cf. [BH96]). Proof methods which make no use of the predicates INDIST_{b} (e.g. Proof Methods 7.20 and 7.10) do not suffer from this problem.

Acknowledgements: Thanks to Michel Bidoit and Rolf Hennicker for many very useful comments, including an explanation of how their results relate to concepts and results in Sections 5 and 7. Proof Method 7.16 is due to them, and they pointed out that a previous version of Proof Methods 7.5 and 7.8 were unnecessarily restrictive. Thanks to Andrzej Tarlecki for many discussions on related topics and for drawing our attention to the idea behind the predicate INDIST_{b} in Theorem 5.4, and to him and Michel Bidoit for comments concerning the results in [BT96]. Thanks to David Aspinall for helpful comments on a draft of this paper, and to Wolfgang Degen for providing useful pointers to the literature.

References

[BH95] M. Bidoit and R. Hennicker. Modular correctness proofs of behavioural implementations. Report 9513, Ludwig-Maximilians-Universität Mn̈chen (1995).

[BH96] M. Bidoit and R. Hennicker. Behavioural theories and the proof of behavioural properties. To appear in Theoretical Computer Science (1996).

[BHW95] M. Bidoit, R. Hennicker and M. Wirsing. Behavioural and abstractor specifications. Science of Computer Programming 25:149–186 (1995).

[BT96] M. Bidoit and A. Tarlecki. Behavioural satisfaction and equivalence in concrete model categories. Proc. 21st Colloq. on Trees in Algebra and Programming, Linköping. Springer LNCS 1059, 241–256 (1996).

[Far92] J. Farrés-Casals. Verification in ASL and Related Specification Languages. Ph.D. thesis, Report CSR-92-92, Univ. of Edinburgh (1992).

[GGM76] V. Giarratana, F. Gimona and U. Montanari. Observability concepts in abstract data type specification. Proc. 1976 Symp. on Mathematical Foundations of Computer Science, Gdansk. Springer LNCS 45, 567–578 (1976).

[GM82] J. Goguen and J. Meseguer. Universal realization, persistent interconnection and implementation of abstract modules. Proc. 9th Intl. Colloq. on Automata, Languages and Programming, Aarhus. Springer LNCS 140, 265–281 (1982).

[Grü90] T. Grünler. Spezifikation höherer Ordnung. Ph.D. thesis, Report MIP-9012, Universität Passau (1990).

[Hen50] L. Henkin. Completeness in the theory of types. Journal of Symbolic Logic 15:81–91 (1950).

[Hen91] R. Hennicker. Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing 4:326–345 (1991).

[HW95] R. Hennicker and M. Wirsing. Behavioural specifications. In: Proof and Computation. Marktoberdorf International Summer School, 1993. NATO ASI Series F, Vol. 139. Springer (1995).

[KST95] S. Kahrs, D. Sannella and A. Tarlecki. The definition of Extended ML: a gentle introduction. Report ECS-LFCS-95-322, Dept. of Computer Science, Univ. of Edinburgh (1995). To appear in Theoretical Computer Science.

[Mei92] K. Meinke. Universal algebra in higher types. Theoretical Computer Science 100:385–417 (1992).

[MG85] J. Meseguer and J. Goguen. Initiality, induction and computability. In: Algebraic Methods in Semantics (M. Nivat and J. Reynolds, eds.). Cambridge Univ. Press, 459–540 (1985).

[Mit90] J. Mitchell. Type systems for programming languages. In Handbook of Theoretical Computer Science, Vol. B (J. van Leeuwen, ed.), 365–458. North Holland (1990).

[Möl87] B. Möller. Higher-Order Algebraic Specifications. Habilitationsschrift, Technische Universität München (1987).

[Nip88] T. Nipkow. Observing nondeterministic data types. Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane. Springer LNCS 332, 170–183 (1988).

[NO88] P. Nivela and F. Orejas. Initial behaviour semantics for algebraic specifications. Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane. Springer LNCS 332, 184–207 (1988).

[ONS91] F. Orejas, M. Navarro and A. Sánchez. Implementation and behavioural equivalence: a survey. Selected Papers from the 8th Workshop on Specification of Abstract Data Types, Dourdan. Springer LNCS 655, 93– 125 (1991).

[Pho92] W. Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. Report ECS-LFCS-92-208, Univ. of Edinburgh (1992).

[Rei85] H. Reichel. Behavioural validity of conditional equations in abstract data types. Proc. of the Vienna Conf. on Contributions to General Algebra, 1984. Teubner-Verlag, 301–324 (1985).

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

[ST88a] D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation 76:165–210 (1988).

[ST88b] D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25:233–281 (1988).

[ST89] D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. Joint Conf. on Theory and Practice of Software Development, Barcelona. Springer LNCS 352, 375–389 (1989).

[ST95] D. Sannella and A. Tarlecki. Model-theoretic foundations for program development: basic concepts and motivation. Report 791, Institute of Computer Science, Polish Academy of Sciences (1995).

[SW83] D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. Proc. 1983 Intl. Conf. on Foundations of Computation Theory, Borgholm. Springer LNCS 158, 413–427 (1983).

[SW96] D. Sannella and M. Wirsing. Specification languages. Chapter 7 of Algebraic Foundations of Systems Specification (E. Astesiano, H.-J. Kreowski and B. Krieg-Brückner, eds.). Springer, to appear (1996).

[Sch94] P.-Y. Schobbens. Second-order proof systems for algebraic specification languages. Selected Papers from the 9th Workshop on Specification of Abstract Data Types, Caldes de Malavella. Springer LNCS 785, 321–336 (1994).

[Sch90] O. Schoett. Behavioural correctness of data representations. Science of Computer Programming 14:43–57 (1990).

[Sch92] O. Schoett. Two impossibility theorems on behavioural specification of abstract data types. Acta Informatica 29:595–621 (1992).

[Sch77] K. Schütte. Proof Theory. Springer (1977).

[Sti92] C. Stirling. Modal and temporal logics for processes. In: Logics for Concurrency: Structure versus Automata (F. Moller and G. Birtwistle, eds.). Springer LNCS 1043, 149–237 (1996).

[TvD88] A. Troelstra and D. van Dalen. Constructivism in Mathematics: An Introduction, Vol. 1. North-Holland (1988).

[Win93] G. Winskel. The Formal Semantics of Programming Languages. MIT Press (1993).