BRICS RS-96-52 Hintermeier et al.: Combining Algebraic and Set-Theoretic Speci�cations

BRICS

Basic Research in Computer Science

Combining Algebraic and Set-Theoretic Speci�cations

(Extended Version)

Claus Hintermeier H� el� ene Kirchner Peter D. Mosses

BRICS Report Series RS-96-52 ISSN 0909-0878 December 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through World Wide Web and anonymous FTP:

http://www.brics.dk/
ftp://ftp.brics.dk/

This document in subdirectory RS/96/52/

Combining Algebraic and Set-Theoretic Specifications. (Extended version)^{∗}

Claus Hintermeier, Hélène Kirchner

CRIN-CNRS/INRIA Lorraine B.P. 239

F-54506 Vandœuvre-lès-Nancy Cedex

email: hinterme,hkirchne@loria.fr

Peter D. Mosses BRICS^{†}, University of Aarhus Ny Munkegade, bldg. 540 DK-8000 Aarhus C

                                        email: pdmosses@brics.dk

Abstract

Specification frameworks such as B and Z provide power sets and cartesian products as built-in type constructors, and employ a rich notation for defining (among other things) abstract data types using formulae of predicate logic and lambda-notation. In contrast, the so-called algebraic specification frameworks often limit the type structure to sort constants and first-order functionalities, and restrict formulae to (conditional) equations. Here, we propose an intermediate framework where algebraic specifications are enriched with a set-theoretic type structure, but formulae remain in the logic of equational Horn clauses. This combines an expressive yet modest specification notation with simple semantics and tractable proof theory.

1 Introduction

As is well known, there are two main schools of thought regarding the formal specification of abstract data types: the model-oriented [1, 18, 3], and the property-oriented [5, 20]. Let us briefly recall the main features of these two approaches.

Model-oriented specifications. The emphasis is on specifying data types as set-theoretic structures (products, power sets, etc.), the operations of the data types then being defined as particular functions on these structures. For example, to specify a simple abstract data type of sequences, one defines the type as a set of functions, represents a sequence ⟨x_{1}, …, x_{n}⟩ by the function mapping i to x_{i} for each i ∈ {1, …, n}, and defines concatenation using function abstraction and application. The underlying logic for reasoning about such a specification is a powerful higher-order logic, e.g., based on ZF set theory.

∗This work was partially supported by Compass (Esprit Basic Research Working Group 6112).

†Centre for Basic Research in Computer Science

Property-oriented specifications. Here one generally tries to avoid choosing an explicit representation: types are left abstract as so-called sorts— sometimes equipped with a subsort inclusion relation, but otherwise unstructured. The operations are specified by axioms that relate them to each other, often including the main intended algebraic properties. For example, sequences could be specified by axioms asserting that concatenation is associative, with the empty sequence as unit. The underlying logic is often a modest Horn-clause fragment of equational first-order logic—supplemented by an induction rule when dealing with initial algebra semantics rather than loose semantics.

Combinations. In practice, some model-oriented specification languages (such as Z) do allow types to be left abstract (or ‘given’), with the operations on them specified by axioms. Moreover, the use of auxiliary (‘hidden’) sorts and operations in property-oriented specifications can give these a model-oriented flavour. There are also some wide-spectrum languages (e.g., RSL, Spectrum) which encompass both approaches, allowing model- and property-oriented specifications to be mixed together.

It seems to us that both the model- and property-oriented approaches have their advantages and disadvantages. In particular, we regard the restriction to Horn-clause logic in the latter as beneficial, since not only are the consequences of a specification much more obvious than in full higher-order logic, but also automated reasoning and prototyping are feasible. The restriction of types to unstructured sorts in property-oriented specifications, however, we regard as a definite disadvantage.

This has led us to investigate an intermediate or hybrid approach, combining the better features of the model- and property-oriented approaches:

• Types include abstract types (of individuals) as well as product, power set, and function types.

• Operations may be higher-order and partial.

• The only built-in relations are equality, set membership and the existential predicate (the latter merely abbreviates an equality).

• Formulae are restricted to Horn-clauses (no disjunction, no explicit negation, variables are universally quantified).

• Models have quite straightforward set-theoretic foundations.

• Specifications have initial models (when consistent).

• Specifications are amenable to prototyping and reasoning using rewriting and saturation techniques.

We hope that the illustrations given in Section 2 will convince the reader that this framework is rather expressive, at least for specifying abstract data types. The foundations laid in Section 3 are reasonably simple, and Section 4 demonstrates the tractability of the logic. Finally, Section 5 concludes by comparing the proposed framework with related approaches.

This paper is an extended version of [7]. We present proofs of the results, and improve some technical details in the definitions.

2 Illustrations of Specifications

Before we take a closer look at the foundations of our proposed framework, let us illustrate its expressiveness, which approaches that of model-oriented frameworks such as B and Z, and far exceeds that of conventional algebraic specifications. The examples given correspond to fragments of the standard Mathematical Toolkit for Z: abstract data types of numbers and sequences.

We have chosen to format our specifications in the style normally used for Z in the literature, because the symbols here mostly have roughly the same intended interpretation as that indicated in the Z standard. However, one should bear in mind that our specifications are not actually in Z itself, and the formal details of interpretations here are different. Moreover, we want the possibility of initial algebra semantics for our specifications. For those readers not familiar with Z, a few extra words of explanation of the examples will be given below.

NaturalNumbers

ℕ : ℙ(𝕀)

0 : ℕ

succ : ℕ \underrightarrow{}ℕ

≤ , < : ℕ ↔ ℕ

∀ x, y : ℕ • 0 ≤ x

x ≤ y ⇒ succ(x) ≤ succ(y)

0 < succ(x)

x < y ⇒ succ(x) < succ(y)

All constants used in the axioms in the lower part of the specification are declared, with their types, in the upper part. The type 𝕀 is that of all individuals, and ℙ forms the type of sets with elements from its argument type, thus ℕ is specified to be a set of individuals. Sets may be used to indicate types in declarations: since ℕ : ℙ(𝕀) is a set of individuals, 0 : ℕ declares the type of 0 to be 𝕀. Moreover, for any constant c declared to have type T , there is an implicit axiom c ∈ T , where the type T is now interpreted as a set.

The remaining constants declared above are all first-order: succ has the type of a partial function on ℕ, and ≤ and < are typed as binary relations. (We could have declared succ to have total function type ℕ → ℕ, giving a slightly stronger theory, but we prefer to keep this example minimal to facilitate the discussion of its operationalization in Section 4.)

The axioms above consist of two unconditional and two conditional Hornclauses—we leave their conjunction implicit. The universal quantification of the variables used in the clauses is given explicitly, so that all notation used has been declared, and to avoid the need for type inference.

Our next example is a generic data type of sequences. X is a type variable, determining the type of elements in the sequences, and the constants declared have polymorphic types: they may be used with X instantiated by any ground (monomorphic) type, e.g., 𝕀 × 𝕀. The reference to the NaturalNumbers specification makes the notation declared there available locally, for use in the specification of the length operation. The constant seq is supposed to denote a function that maps any subset S of X to the set seq(S) of sequences whose elements are all in S.

The type specified for ⌢ illustrates the use of product types when specifying operations of more than one argument. Note also that we use the place-holder symbol ‘ ’ to indicate where the arguments go when an operation is applied: we allow not only ordinary prefix notation, but also infix, postfix, outfix, and general mixfix notation for applications. The place-holder may be omitted in prefix symbols.

GenericSequences [X ] NaturalNumbers

seq : ℙ(X ) \underrightarrow{}ℙ(𝕀)

⟨ ⟩ : seq(X )

⟨ ⟩ : X \underrightarrow{}seq(X )

⌢ : seq(X ) × seq(X ) \underrightarrow{}seq(X ) length : seq(X ) \underrightarrow{}ℕ

∀ x : X • ∀ s, t, u : seq(X ) •

⟨ ⟩ ⌢ s = s

s ⌢ ⟨ ⟩ = s

s ⌢ (t ⌢ u) = (s ⌢ t) ⌢ u

length(⟨ ⟩) = 0

length(⟨x⟩ ⌢ s) = succ(length(s))

Let us consider now a higher-order example. The notation t ↓ is read as “t exists” (or “t is defined”).

MappingSequences [X , Y ] GenericSequences mapseq : (X \underrightarrow{}Y ) \underrightarrow{}(seq(X ) \underrightarrow{}seq(Y ))

∀ x : X • ∀ s, t : seq(X ) • ∀ f : X \underrightarrow{}Y •

mapseq(f )(⟨ ⟩) = ⟨ ⟩

f (x) ↓ ⇒ mapseq(f )(⟨x⟩) = ⟨f (x)⟩ mapseq(f )(s) ↓ ∧ mapseq(f )(t) ↓ ⇒

mapseq(f )(s ⌢ t) = mapseq(f )(s) ⌢ mapseq(f )(t)

In this example we have to be a bit careful about existence: equations are interpreted as ‘existential’, so x = y asserts the existence of both x and y. Since f ranges over partial functions, f (x) may not exist for some x. If f were restricted to being a total function, we could replace all the \underrightarrow{}’s by →’s above, and drop the existence conditions from the axioms altogether.

3 Foundations

Here we provide the formal foundations for our specification language. For perspicuity, we treat first a simpler kernel language, giving syntax, semantics, proof rules, and various results; in particular, we show how to decide whether a term is well-typed, as soon as each constant and variable has a type. Models for specifications in the kernel language are defined in a set theoretic framework. Sound proof rules are given for this class of models, which has an initial model. The construction of this initial model is a key point to prove completeness of deduction, more precisely that any atomic formula valid in all models is deducible with these proof rules. At the end of this section we define the syntax of our complete language, and indicate how it can be reduced to the kernel language. First, we make some general remarks about the novel aspects of our work.

Compared to conventional algebraic specification languages, the type system of our language is very rich, being close to that of Z. We follow Z in interpreting types as sets, and in allowing them to be used as values in terms too. However, we take a slightly intensional view of sets: two sets that have the same values as members are not necessarily equal! This is achieved by what amounts to a labelling of sets, provided by a choice function (denoted by choose) which gives a unique element for any set given as argument. This provides the key to the completeness of our logic.

The motivation for not using extensional equality on sets is twofold. First, an axiom in a specification could have an equality between sets as a condition. If two differently-specified sets (say, subsets of the natural numbers) happened to have the same members, unexpected consequences might follow. By insisting that two sets are only regarded as equal when this follows by algebraic reasoning, rather than by membership equivalence, we remove this (admittedly minor) danger. Second, for tractability and operationalization of reasoning, we wish to remain in Horn-clause logic (with equality), and it is well-kown that extensionality cannot be axiomatized in (finitary) Horn-clause logic. Adding a choice function, freely interpreted, allows formulating a deduction rule for an extensional equality on sets with non-standard elements. Our treatment of higher-order operations is similarly intensional: two operations do not get equated just because they give the same results on the same arguments. We claim that this kind of intensional equality of sets and functions is necessary to keep our framework truly ‘algebraic’. Other frameworks for higher-order algebraic specification, e.g., that of [11], provide extensionality and term-models, but the proof theory seems less tractable.

For expressing types, we propose, in addition to the constant 𝕀 for the builtin type of individuals^{1} and variables, several type constructors: partial power set operator ℙ and cartesian product ×, and partial function space constructor \underrightarrow{}and relation space constructor ↔. Furthermore, we introduce the termgenerated subset constructor 𝕋 that extracts from any set its term-generated part; this is needed by our choice to consider also non-standard (i.e. non termgenerated) models. Finally, for technical reasons, we include in our type system a universal type 𝕌.

In Z, the function space S \underrightarrow{}T and relation space S ↔ T are both interpreted as subtypes of ℙ(S × T ). This may seem rather natural, but it has some unfortunate pragmatic consequences in connection with overloading and subtype polymorphism: specifying f : S \underrightarrow{}T restricts the graph of f to be a subset of S × T , preventing f from being extended to give results on arguments not in S! For example, in the Z framework specifying succ : ℕ \underrightarrow{}ℕ implies succ ⊆ ℕ × ℕ , which prevents an extension to succ : ℤ \underrightarrow{}ℤ with succ(−1) = 0. (According to the Z Draft Standard, ℕ is not a type, but merely a subset of ℤ. The constant succ thus gets a unique interpretation on ℤ, and (−1, 0) ∉ ℕ × ℕ.) Similarly, in Z a relation p : S ↔ T cannot be extended to other types, so specifying e.g. ≤ : ℕ × ℕ prevents overloading with ≤ : seq(ℕ) × seq(ℕ).

Here, in contrast to Z, our interpretation of S \underrightarrow{}T is as a set of partial functions which always (when defined) give results in T when applied to arguments in S! Thus specifying f : S \underrightarrow{}T does not say anything at all about what might result when f is applied to arguments outside S. An axiom f ∈ S \underrightarrow{}T here corresponds to S ◁ f ∈ S \underrightarrow{}T in Z, where S ◁ f denotes the restriction of f to domain S (but our type assertion f : S \underrightarrow{}T appears to have no exact counterpart in Z). Similarly, we interpret S ↔ T as a set of binary relations that may relate other pairs than those in S × T .

By this means, we are able to avoid a significant danger of accidental inconsistency in specifications, and permit the use of subtype polymorphism and overloading, as common in some algebraic specification frameworks. Notice that our change of interpretation does not prevent type-checking: f (s) is only considered type-correct when f : S \underrightarrow{}T and s : S hold for some S and T .

1For simplicity in this paper, we do not consider further ‘given’ types of individuals.

3.1 Syntax

A presentation P in our kernel language consists of a set of declarations of typed constants (including 𝕀, ℙ, 𝕋, choose, ×, \underrightarrow{}, ↔) and variables, together with a set of Horn-clauses built from terms over the declared items using three built-in predicates: equality =, membership ∈ and existence ↓. The fixed notation is indicated by the following BNF-like grammar:

CLAUSE ::= ATOMS ⇒ ATOM | ATOMS ⇒
ATOMS ::= ATOM ∧ ATOMS | ATOM
ATOM ::= TERM = TERM | TERM ∈ TERM | TERM ↓
TERM ::= CONST | VAR | TERM (TERM ) | TERM , TERM
CONST ::= 𝕀 | ℙ | 𝕋 | choose | × | \underrightarrow{}| ↔ | …
VAR  ::= …

where the ‘… ’s indicate declared constants and variables. Place-holders ‘ ’ in constant symbols indicate that these are to denote functions, and that applications are to be written concretely with the argument(s) in the position of the place-holder(s). Parentheses are allowed for disambiguating the grouping. Thus the application of ℙ to 𝕀 may be written ℙ 𝕀 or ℙ(𝕀), and that of × to (𝕀, 𝕀) as 𝕀 × 𝕀. The syntax for pairs TERM , TERM and applications of product TERM × TERM is assumed to be left-associative. Note that a list of ATOMS may be empty.

Types are denoted by type terms generated by the following grammar:

TYPE ::= VAR | 𝕀 | 𝕌 | TYPE × TYPE
| ℙ(TYPE) | TYPE \underrightarrow{}TYPE | TYPE ↔ TYPE
RTYPE ::= 𝕋(VAR) | 𝕋(𝕀) | 𝕋(𝕌) | 𝕋(TYPE × TYPE)
STYPE ::= 𝕋(ℙ(TYPE)) | 𝕋(TYPE \underrightarrow{}TYPE) | 𝕋(TYPE ↔ TYPE)
TTYPE ::= RTYPE | STYPE

Type terms will be interpreted as sets of values (when defined), with variables VAR indicating polymorphism. We shall regard TYPE, RTYPE, STYPE, and TTYPE as kinds, writing T : K to assert that T is a well-formed type term of kind K . Intuitively, values of types in TTYPE are generated by ‘standard’ terms, excluding the use of choose; the types in STYPE are simply those that are interpreted as sets of sets, so that choose may be used on their elements. For example, the types 𝕀 × ℙ(𝕀), ℙ(𝕀) \underrightarrow{}ℙ(𝕀) and ℙ(ℙ(𝕀)) are of kind TYPE and 𝕋(𝕀 × ℙ(𝕀) × ℙ(ℙ(𝕀))) is of kind TTYPE.

Type terms are partially ordered by a subtype inclusion ordering ≤. The cartesian product constructor is monotone in both arguments, as are ℙ and 𝕋 in their only argument. The function space constructor is anti-monotone in the first argument and monotone in the second. The relation space constructor is anti-monotone in both arguments, just as if it were a boolean function. So the subtype inclusion ordering ≤ on type terms satisfies the following assertions, where S, T , V , W range over well-formed type terms of kind TYPE only:

S ≤ V ⇒ ℙ(S) ≤ ℙ(V ) S ≤ V ∧ T ≤ W ⇒ S × T ≤ V × W V ≤ S ∧ T ≤ W ⇒ S \underrightarrow{}T ≤ V \underrightarrow{}W V ≤ S ∧ W ≤ T ⇒ S ↔ T ≤ V ↔ W S ≤ 𝕌 V \underrightarrow{}W ≤ ℙ(𝕌 × 𝕌) V ↔ W ≤ ℙ(𝕌 × 𝕌) S ≤ V ⇒ 𝕋(S) ≤ 𝕋(V ) 𝕋(S) ≤ S

together with reflexivity and transitivity of ≤. Note that the omission of the inclusions S \underrightarrow{}T ≤ S ↔ T ≤ ℙ(S × T ) is deliberate, to allow overloading, as discussed at the start of Section 3. The inclusion V \underrightarrow{}W ≤ ℙ(𝕌×𝕌) reflects the fact that a partial function (graph) is a set of pairs, without restriction on the components of the pairs; similarly for binary relations in V ↔ W ≤ ℙ(𝕌 × 𝕌).

Proposition 3.1 The validity of formulae ∃ … ∀ … (S_{1} ≤ T_{1} ∧ … ∧ S_{n} ≤ T_{n}) where S_{i}, T_{i} for i ∈ {1, …, n} are of kind TYPE or TTYPE, is decidable.

Proof: Given a type inclusion problem of the form ∃ ∀(S_{1} ≤ T_{1} ∧ … ∧ S_{n} ≤ T_{n}), we start with the replacement of universally quantified type variables by new constants of the same type. Let the so obtained purely existentially quantified problem C be ∃(S′_{1} ≤ T′_{1} ∧ … ∧ S′_{n} ≤ T′_{n}).

The conjunction is then rewritten using the following set of rewrite rules, closely corresponding to subtyping assertions above, and taking into account in the last additional rule that an inequation with the 𝕋 operator, that can only occur at the top of type terms, can be weakened.

ℙ(S) ≤ ℙ(V ) → S ≤ V
S × T ≤ V × W → S ≤ V ∧ T ≤ W
S \underrightarrow{}T ≤ V \underrightarrow{}W → V ≤ S ∧ T ≤ W
S ↔ T ≤ V ↔ W → V ≤ S ∧ W ≤ T
S ≤ 𝕌 → true
V \underrightarrow{}W ≤ ℙ(𝕌 × 𝕌) → true
V ↔ W ≤ ℙ(𝕌 × 𝕌) → true
𝕋(S) ≤ 𝕋(V ) → S ≤ V
𝕋(S) ≤ S → true
𝕋(T ) ≤ S → T ≤ S

if S ∉ VAR, S not of kind TTYPE.

This system terminates since each rewrite step strictly decreases the number of symbols ℙ, ×, \underrightarrow{}, ↔, 𝕌, 𝕋 in the conjunction. After simplifying with respect to the usual properties of conjunction, the result C′ is either true or a conjunction of inequations in which one side is a variable or the constant 𝕀. Clearly, if C →^{∗} C′, then C′ ⇒ C logically. In particular if C →^{∗} true, then C is true. Otherwise, the resulting set of inequations has a solution if and only if the left and right-hand sides of the inequations are unifiable with respect to kinds (which is decidable in this order-sorted regular signature of type terms of kinds {TYPE, RTYPE, STYPE, TTYPE}). □

Finally, we define type membership for terms (potentially) denoting values, writing s : T to assert that s is a well-formed term of type T . Let X , Y be type variables of kind TYPE, and let f , s, t range over arbitrary terms. Then we assert:

s : S ∧ S ≤ T ⇒ s : T f : 𝕋(S \underrightarrow{}T ) ∧ s : 𝕋(S) ⇒ f (s) : 𝕋(T ) s : 𝕋(S) ∧ t : 𝕋(T ) ⇒ (s, t) : 𝕋(S × T ) 𝕀 : 𝕋(ℙ(𝕀)) ℙ : 𝕋(ℙ(X ) \underrightarrow{}ℙ(ℙ(X ))) 𝕋 : 𝕋(ℙ(X ) \underrightarrow{}𝕋(ℙ(X ))) choose : 𝕋(ℙ(X )) \underrightarrow{}X × : 𝕋(ℙ(X ) × ℙ(Y ) \underrightarrow{}ℙ(X × Y )) choose : 𝕋(X \underrightarrow{}Y ) \underrightarrow{}(X × Y ) \underrightarrow{}: 𝕋(ℙ(X ) × ℙ(Y ) \underrightarrow{}ℙ(X \underrightarrow{}Y )) choose : 𝕋(X ↔ Y ) \underrightarrow{}(X × Y ) ↔ : 𝕋(ℙ(X ) × ℙ(Y ) \underrightarrow{}ℙ(X ↔ Y ))

Observe that in general, constants are declared to have types of kind TTYPE, the exception being choose.

Proposition 3.2 Assuming that the declarations in a presentation provide types for each constant and variable used, it is decidable to check that each term is well-typed.

Proof: From constant and variable types, it is possible to determine in a bottomup process a type for any term built from these constants and variables with the pairing and function application operators. Because of subtyping and overloading, a term may have several types.

In order to type f (a) knowing a : A and f : F , we solve

∃ S, T (F ≤ 𝕋(S \underrightarrow{}T ) ∧ A ≤ 𝕋(S)).

Let μ be a solution. Then f (a) : 𝕋(μ(T )).

In order to type (a_{1}, a_{2}) knowing a_{1} : A_{1} and a_{2} : A_{2}, we solve

∃ S, T (A_{1} ≤ 𝕋(S) ∧ A_{2} ≤ 𝕋(T )).

Let μ be a solution. Then (a_{1}, a_{2}) : 𝕋(μ(S) × μ(T )). □

For example, if ℕ : 𝕋(ℙ(𝕀)), then we can form the term ℙ(ℕ), which is of type 𝕋(ℙ(ℙ(𝕀))) since ℙ : 𝕋(ℙ(X ) \underrightarrow{}ℙ(ℙ(X ))) and the system

∃ S, T (𝕋(ℙ(X ) \underrightarrow{}ℙ(ℙ(X ))) ≤ 𝕋(S \underrightarrow{}T ) ∧ 𝕋(ℙ(𝕀)) ≤ 𝕋(S))

has a solution with X = 𝕀, S = ℙ(𝕀)) and T = ℙ(ℙ(𝕀)).

In the following sections, for an arbitrary presentation P, we write F, X for the declared type constructors and variables (with their respective kinds), F, X for the remaining constants and variables (with their respective types), \overline{Σ} for (F, F, X), and Σ for \overline{Σ} without the constant choose (which plays a special role in our framework). A \overline{Σ}-presentation is given by a signature (\overline{Σ}, X) and a set of (\overline{Σ}, X)-Horn-clauses. In the following, (Σ, X)-terms are called standard terms and (\overline{Σ}, X)-terms are called non-standard terms.

3.2 Semantics

The semantics for our formulae are structural set theoretic models. We therefore start with the definition of an interpretation for the type constructors (from F) and other constants (from F). These interpretations are not given separately, since both can be used in terms. Remark that we use a classical notion of set in the definition, as e.g. in [19].

Note furthermore that typing and membership are not to be confused: except for declared constants, deriving t : T does not imply that t ∈ T holds. This difference comes from the use of partial functions. E.g., div(1, 0) may be of type 𝕀, but may fail to exist, i.e. div(1, 0) does not denote a member of the set 𝕀.

Definition 3.3 A standard set-theoretic Σ-interpretation I is a pair (U_{I} , .^{I} ) of a universe U_{I} and an interpretation function .^{I} , such that:

• U_{I} is a set of atomic objects (individuals and pairs) and sets (the special constant 𝕌 is not interpreted as an element of U_{I} , to avoid foundational problems—conceptually, it may be interpreted as the entire universe U_{I} );

• 𝕀^{I} is a set of individuals;

• ℙ^{I} is a partial function such that ℙ^{I} (S), when defined, is a subset of the ordinary powerset of S;

• ×^{I} is a partial function yielding, when defined, the cartesian product of its arguments;

• \underrightarrow{}^{I} is a partial function yielding, when defined, a set of (graphs of) partial functions such that when g ∈ S \underrightarrow{}^{I} T then (s, t) ∈ g and s ∈ S imply t ∈ T ;

• ↔^{I} is a partial function yielding, when defined, a set of (graphs of) binary relations;

• ( , )^{I} is a partial function yielding, when defined, the pair of its arguments; • f (s)^{I} is t when f is a function graph and (s, t) ∈ f ;

• for all constants c in F ∪ F (other than 𝕌, 𝕋 and choose), c^{I} ∈ α^{I} (T ) when c : T for all (X, I )-variable assignments α (i.e. a mapping from type variables to (F, ∅)-type term interpretations), and where α^{I} is the natural extension of α to terms under interpretation .^{I} . When α is ∅, α^{I} (T ) is written as T^{I} .

Note that 𝕋^{I} is left unrestricted above. Now we relax the notion of interpretation to allow non-standard elements (i.e. not denoted by a Σ-term) that represent (but are not themselves) sets. These non-standard elements may be regarded as ‘labels’ that distinguish between sets which include the same standard elements.

Definition 3.4 A (non-standard) \overline{Σ}-interpretation I is a standard set-theoretic Σ-interpretation with the following differences:

• The sets in ℙ^{I} (S) may include non-standard elements that represent (but are not themselves) subsets of S;

• 𝕋^{I} is a partial function such that, when defined, 𝕋^{I} (S) is the Σ-term-generated subset of S (excluding all non-standard elements);

• choose^{I} is a partial function which gives a unique arbitrary element from any non-empty set S ∈ U_{I} , and is otherwise undefined.

A \overline{Σ}-interpretation where 𝕀^{I} is a set of \overline{Σ}-terms is called a \overline{Σ}-term interpretation.

Let us illustrate Definition 3.4 with an example.

Example 3.5 Let F = \{s, 0, ≤ \} with 0 : 𝕀, s : 𝕀 \underrightarrow{}𝕀, ≤ : 𝕀 ↔ 𝕀. Let furthermore Nat and Even be of type ℙ(𝕀). Then I defined as follows is a \overline{Σ}-interpretation:

• U_{I} is a set containing all natural numbers, the set of even natural numbers, the set of all natural numbers, the graph of the successor function, the graph of the less or equal relation, and all pairs of natural numbers. Moreover, 𝕌_{I} has to contain the denotations of all the built-in constants (other than 𝕌), i.e., 𝕀, ℙ, ×, \underrightarrow{}, ↔, 𝕋, and choose.

• 𝕀^{I} is the set of natural numbers,

• ℙ^{I} maps 𝕀^{I} to {Nat^{I} , Even^{I} } and is undefined for all other arguments.

• ×^{I} is the empty partial function graph;

• \underrightarrow{}^{I} maps (𝕀^{I} , 𝕀^{I} ) to the singleton containing the graph of the successor function only; it is undefined for all other arguments.

• ↔^{I} maps (𝕀^{I} , 𝕀^{I} ) to the singleton containing the graph of the less or equal relation; it is undefined for all other arguments.

• ( )^{I} is defined as required for \overline{Σ}-interpretations.

• ( , )^{I} maps any two natural numbers to their pair, and is otherwise undefined;

• 0^{I} is zero, s^{I} is the (graph of the) successor function on natural numbers, ≤^{I} is less or equal on natural numbers, Nat^{I} is the set of natural numbers and Even^{I} is the set of even natural numbers.

• 𝕋^{I} is the identity on 𝕀^{I} , ℙ^{I} (𝕀^{I} ), 𝕀^{I} \underrightarrow{}^{I} 𝕀^{I} , and 𝕀^{I} ↔^{I} 𝕀^{I} ; and all their cartesian products built with ×; it is undefined otherwise.

• The choice function choose^{I} gives^{2} zero for Even^{I} , one for Nat^{I} (and hence for 𝕀^{I} ), the graph of the successor function for (𝕀 \underrightarrow{}𝕀)^{I} and the less or equal relation for (𝕀 ↔ 𝕀)^{I} .

Hence, we get for example, 0^{I} ∈ 𝕀^{I} , Nat^{I} ∈ ℙ^{I} (𝕀^{I} )), Even^{I} ∈ ℙ^{I} (𝕀^{I} )), and s(0)^{I} = one as expected. Remark that 𝕋(ℙ(𝕀))^{I} is the set containing only the set of natural numbers and the set of even natural numbers but not the set of odd natural numbers.

However, since we also consider non-standard interpretations, any interpretation J defined as I , except that 𝕀^{J} is the set of (positive and negative) integers, is another \overline{Σ}-interpretation. Then, 𝕀^{I} and 𝕀^{J} differ, but all other interpretations remain unchanged, since the term generated part of I and J is equal. Here 𝕋^{J} on 𝕀^{J} cuts out the negative integers.

Definition 3.6 Let I , J be \overline{Σ}-interpretations.

A \overline{Σ}-homomorphism h : I → J is a (total) function h : U_{I} → U_{J} satisfying:

• for all (F, ∅)-terms T , t ∈ T^{I} implies h(t) ∈ T^{J} ;

• for all constants c ∈ F ∪ F (apart from 𝕌), h(c^{I} ) = c^{J} ;

• for all (F, ∅)-terms T_{1}, T_{2} of kind TTYPE, for all t_{1} ∈ T_{1}^{I} , t_{2} ∈ T_{2}^{I} , h((t_{1}, t_{2})^{I} ) = (h(t_{1}), h(t_{2}))^{J} whenever (t_{1}, t_{2}) exists;

• for all (F, ∅)-terms T , T′ of kind TYPE, for all t_{2} ∈ 𝕋(T )^{I} and for all t_{1} ∈ 𝕋(T \underrightarrow{}T′)^{I} , h(t_{1}(t_{2})^{I} ) = h(t_{1})(h(t_{2}))^{J} whenever t_{1}(t_{2}) exists.

Definition 3.7 A (X∪X , I )-variable assignment α is a mapping from variables in X ∪ X to (F, ∅)-type terms and elements of 𝕀^{I} respectively, such that α |_{X} is a (X, I )-variable assignment and α(x) ∈ (α(T ))^{I} if x : T , where T is a (F, X)- type term. The assignment α is extended to a partial function α^{I} mapping terms (possibly containing variables) to their interpretations.

2Remark that the interpretation of choose is not restricted—it may be any interpretation realising a choice.

\overline{Σ}-substitutions are defined as usual as (X ∪ X , I )-variable-assignments α in \overline{Σ}-term interpretations I , such that \{x ∈ X ∪ X | α(x) ≠ x\} is finite. The set {x ∈ X ∪ X | α(x) ≠ x} is then called the domain of α, written Dom(α). The set of \overline{Σ}-substitutions with domain included in X is written SUBST_{Σ}(X ∪ X).

Now, given a \overline{Σ}-interpretation I , we can define the truth value of a formula by universal quantification over all (X ∪ X , I )-variable assignments.

Definition 3.8 Let I be a \overline{Σ}-interpretation and α be a (X ∪ X , I )-variable assignment.

• An existential formula T ↓ holds in I under α if α^{I} (T ) is defined.

• An equality S = T holds in I under α if α^{I} (S) and α^{I} (T ) are both defined and are identical.

• A membership formula S ∈ T holds in I under α if α^{I} (S) and α^{I} (T ) are both defined and α^{I} (S) is an element of α^{I} (T ).

• An implication A_{1} ∧…∧A_{n} ⇒ A holds in I under α if A holds in I under α whenever all of A_{1}, …, A_{n} hold in I under α. A negative implication A_{1} ∧ … ∧ A_{n} ⇒ holds in I under α if A_{1}, …, A_{n} never hold together in I under α. A trivial implication ⇒ A holds in I under α if A holds in I under α.

A (\overline{Σ}, X)-Horn clause holds in I if it holds in I for all (X ∪ X , I )-variable assignments α. I is a model of a presentation P if all Horn clauses in P hold in I .

Formula satisfaction is written I ⊧ Φ, or P ⊧ Φ in case all models of P satisfy the formula Φ. P is consistent if it has a model.

3.3 Proof Rules

From this section on, we restrict the possible sets of formulas, such that some atoms, trivially unsatisfiable due to type mismatches, are eliminated.

Definition 3.9 A standard \overline{Σ}-presentation is a \overline{Σ}-presentation P, where:

• All non-variable terms occurring in P belong to a type of kind TTYPE.

• If a constant c (other than 𝕌) is declared to be of type T , then c ∈ T is a fact in P.

• choose does not occur in the conclusion of any clause in P.

• All variables of type T with T : TYPE in P occur only as the left-hand-side of a membership relation ‘∈’.

• All equalities s = t satisfy that the sets of types of σ(s) and σ(t) are the same for every \overline{Σ}-substitution σ.

• All membership formulas s ∈ t satisfy that σ(t) is of type 𝕋(S \underrightarrow{}T ), 𝕋(S ↔ T ) or 𝕋(ℙ(S × T )), if σ(s) is of type S × T , and of type 𝕋(ℙ(T )) if σ(s) is of any other type, for every \overline{Σ}-substitution σ.

The proof rules shown in Table 1 are for a deduction relation ⊢ taking two arguments. The first argument is a standard \overline{Σ}-presentation. The second argument is a \overline{Σ}-formula Φ. These rules are divided into four groups: the upper one is for the embedding of typing into set theory, and uses the subtype inclusion defined in Section 3.1. Then there are rules handling function and relation graphs. Note that z is here intended to be of type 𝕌 \underrightarrow{}𝕌, which is a subtype of ℙ(𝕌 × 𝕌). These are followed by general set theoretic rules, which correspond to the axiom of choice and the axiom of (non-standard) extensionality. Last but not least, there are the logic inference rules; the meta-variables G, G′ range over possibly-empty conjunctions of atomic formulae, and L, L′ may be a single atomic formula or empty.

One of the inference rules (SubstConform) uses P-conform \overline{Σ}-substitutions. These are defined as follows:

Definition 3.10 Let σ ∈ SUBST_{Σ}(X ∪ X) and P be a \overline{Σ}-presentation. Then σ is P-conform if for any variable x in Dom(σ) ∩ X, P ⊢ σ(x) ↓. The set of all P-conform substitutions is denoted by P-SUBST_{Σ}(X ∪ X).

P-conform substitutions have the nice property that they behave like \overline{Σ}- substitutions for composition with general variable assignments.

3.4 Results

We first address correctness of the deduction rules.

Theorem 3.11 Let P be a standard \overline{Σ}-presentation. Then, all deduction rules in PL are sound, i.e. if P ⊢ Φ then P ⊧ Φ.

Proof: We have to check that each rule is sound in any \overline{Σ}-interpretation which is a model of P.

• SubType: if t ∈ S holds in a \overline{Σ}-interpretation I , for any assignment α, α^{I} (t) ∈ α^{I} (S). Then if S ≤ T , α^{I} (S) ⊆ α^{I} (T ) (since when both t ∈ S and T ↓ hold, neither S nor T can involve 𝕌 at all, hence either S = T or S = 𝕋(T )). So it is sound to deduce that α^{I} (t) ∈ α^{I} (T ) for any assignment α, thus t ∈ T holds in the \overline{Σ}-interpretation I ,

• PairType1, PairType2, AppTyp, FApply, FGraph, RApply, RGraph: these axioms are valid in any \overline{Σ}-interpretation by construction.

• SubSet, Choice are sound due to the interpretation of ℙ as a partial power set function and of choose as a choice function (defined on all non-empty sets) in every \overline{Σ}-interpretation.

SubType:  \frac{t ∈ S, T ↓}{t ∈ T} if S ≤ T
PairType1:  x ∈ X ∧ y ∈ Y ∧ (x, y) ↓∧ (X × Y ) ↓⇒ (x, y) ∈ (X × Y )
PairType2:  (x, y) ∈ (X × Y ) ⇒ x ∈ X ∧ y ∈ Y
AppType:  x ∈ X ∧ z ∈ (X \underrightarrow{}Y ) ∧ z(x) ↓ ⇒ z(x) ∈ Y
FApply:  x ∈ X ∧ y ∈ Y ∧ z ∈ (X \underrightarrow{}Y ) ∧ (x, y) ∈ z ⇒ z(x) = y
FGraph:  x ∈ X ∧ y ∈ Y ∧ z ∈ (X \underrightarrow{}Y ) ∧ z(x) = y ⇒ (x, y) ∈ z
RApply:  x ∈ X ∧ y ∈ Y ∧ z ∈ (X ↔ Y ) ∧ (x, y) ∈ z ⇒ z(x, y)
RGraph:  x ∈ X ∧ y ∈ Y ∧ z ∈ (X ↔ Y ) ∧ z(x, y) ⇒ (x, y) ∈ z
SubSet:  x ∈ y ∧ y ∈ ℙ(z) ⇒ x ∈ z
Choice:  \frac{s ∈ t}{choose(t) ∈ t} if t : T for some T : STYPE
Ext:  \frac{choose(x) ∈ y, choose(y) ∈ x}{x = y} if x, y : T for some T : STYPE
WellDef:  \frac{Φ[t]}{t ↓} if Φ[t] is a (\overline{Σ}, X)-atom containing t
PartialReflex:  \frac{t ↓}{t = t}
Axioms:  G ⇒ L if (G ⇒ L) ∈ P is a (\overline{Σ}, X)-clause
SubstConform: \frac{G ⇒ L}{σ(G) ⇒ σ(L)} if σ ∈ P-SUBST_{Σ}(X ∪ X)
Cut:  \frac{G ∧ L′ ⇒ L, G′ ⇒ L′}{G ∧ G′ ⇒ L}
Paramodulation: \frac{G ⇒ L[s], G′ ⇒ (s = t)}{G ∧ G′ ⇒ L[t]}

Table 1: PL – Deduction Rules for P ⊢ Φ • Ext is sound and expresses extensional equality on non-standard sets,

due to the fact that choose is free in every \overline{Σ}-interpretation. Extensional equality of two sets can only be deduced when the premisses hold for all interpretations of the choose function, i.e. for any element in the sets. This amounts to check that both sets have the same elements.

• WellDef is sound since if an atom Φ[t] is valid in every model of P, any term t in this atom should denote an element in the model. This is due to the fact that atoms only hold when their argument terms denote elements—in particular, our equality is existential.

• PartialReflex is the restriction of reflexivity to well-defined terms, so is sound.

• Axioms is trivially sound in every model of P.

• SubstConform, Cut, Paramodulation are standard sound rules for Horn clause logic with equality.

□

The following lemma is needed in order to show that the initial model defined below actually is a model. It can be proved by simple composition of P-conform substitutions with variable assignments:

Lemma 3.12 Let \overline{Σ} be a signature, P a presentation, I a \overline{Σ}-interpretation, G a conjunction of (\overline{Σ}, X)-atoms, σ ∈ P-SUBST_{Σ}(X) and δ be a variable assignment for X ∪ X in I . Then σ(G) holds in I under δ iff G holds in I under δ ∘ σ.

Proof: Let us first prove that if σ ∈ P-SUBST_{Σ}(X) and δ is a variable assignment for X ∪ X in I , δ ∘ σ(x) is also a variable assignment of X ∪ X in I . This amounts to prove that for all x ∈ X with x : T , δ ∘ σ(x) ∈ δ ∘ σ(T )^{I} . If x ∉ Dom(σ), then this is implied by δ being a (X ∪ X , I )-variable assignment. Otherwise, we know that δ(σ(x)) ∈ 𝕋(U_{I} ), since P ⊧ σ(x) ↓. Moreover σ(x) ∈ σ(T ) by definition of a substitution as a special variable assignment in a term interpretation. Hence, δ(σ(x)) ∈ δ(σ(T ))^{I} .

Then let us denote I , δ ⊧ σ(G) the statement σ(G) holds in I under δ. Assume that G is a conjunction of atoms p(…, t, …). Then

I , δ ⊧ σ(p(…, t, …)) iff I , δ ⊧ p(…, σ(t), …)
iff (…, δ(σ(t)), …) ∈ p^{I}
iff I , δ ∘ σ ⊧ p(…, t, …).

□

The initial model constructed in the next definition interprets individuals (t of type 𝕋(𝕀)), pairs (t of type 𝕋(S × T )) and non-standard terms (t of type T : TYPE) as representative of their equivalence class (written [t]), whenever they exist. Sets t (of type 𝕋(ℙ(T ))) and graphs of functions and relations are interpreted such that they contain exactly those term interpretations [u] with u being provably in t, also only if t exists. Remark that this includes the interpretation of terms built from type constructors. Var(t) denotes the set of variables of t.

Definition 3.13 Let P be a standard \overline{Σ}-interpretation and V ⊆ X ∪ X. We define I_{P}(V ) to be the \overline{Σ}-interpretation I whose universe U_{I} is the set of all [t] where t is a (\overline{Σ}, V )-term with P ⊢ t ↓, and where [.] is defined as follows:

• ∀ t with Var(t) ⊆ V , such that t : T where T : RTYPE or T : TYPE, [t] is a representative of {u | u : T , Var(u) ⊆ V and P ⊢ u = t} if P ⊢ t ↓;

• ∀ t with Var(t) ⊆ V , such that t : T with T : STYPE, [t] = {[u] | u : U , Var(u) ⊆ V and P ⊢ u ∈ t} ∪ {[choose(t)]} if P ⊢ t ↓, where U is S when T is 𝕋(ℙ(S)), and R × S when T is 𝕋(R \underrightarrow{}S) or 𝕋(R ↔ S).

For all constants c, let c^{I} = [c]. Finally, for any [t_{1}], [t_{2}] ∈ U_{I} : let ([t_{1}], [t_{2}])^{I} = [(t_{1}, t_{2})] if P ⊢ (t_{1}, t_{2}) ↓, otherwise undefined; and let [t_{1}]([t_{2}])^{I} = [t_{1}(t_{2})] if P ⊢ t_{1}(t_{2}) ↓, otherwise undefined.

One may check that this definition is a \overline{Σ}-interpretation in the sense of Definitions 3.3 and 3.4.

The difficulty in the initiality proof is hidden in the extensionality of sets. The following lemma is crucial for the interpretation of equality and membership. It decomposes into three steps: (1) Equality on individuals (type 𝕋(𝕀)), pairs (type 𝕋(S × T )) and non-standard elements (type T : TYPE) coincides with deductive equality. (2) The same holds for the membership atoms in standard presentations. (3) This is true for equality of sets represented by standard terms.

Lemma 3.14 Consider [.] as defined in Definition 3.13.

1. For all s, t : T with T : TYPE or T : RTYPE, P ⊢ s = t iff [s] = [t].

2. For all s : S with S : TYPE or S : RTYPE, and t : T with T : STYPE, P ⊢ s ∈ t iff [s] ∈ [t].

3. And for all s, t : S with S : STYPE, P ⊢ s = t iff [s] = [t].

Proof: The left-to-right direction is trivial by definition and the reflexivity, paramodulation, well-definedness rules of our logic. From right-to-left, let us assume s : S and t : T .

1. [s] is a representative of {u | u : T , Var(u) ⊆ V and P ⊢ u = s} and [t] is a representative of {v | v : T , Var(v) ⊆ V and P ⊢ v = t}. If [s] = [t], there exists w such that P ⊢ w = s and P ⊢ w = t. So P ⊢ s = t.

2. Assume that P ⊢ t ↓ and P ⊢ s ↓. [s] is a representative of {u | u : S, Var(u) ⊆ V and P ⊢ u = s\}, T is of the form 𝕋(ℙ(S)), 𝕋(R \underrightarrow{}S), or 𝕋(R ↔ S), and [t] = {[w] | w : W , Var(w) ⊆ V and P ⊢ w ∈ t}. W is S when T is 𝕋(ℙ(S)), and R × S in the other two cases. If [s] ∈ [t], there exists [w] such that [s] = [w] and P ⊢ w ∈ t. Since s : S and w : W (where W cannot be of kind STYPE, since S is not, and [s] and [w] must therefore both be representative terms rather than actual sets) from (1) we get P ⊢ s = w. Hence, Paramodulation gives us P ⊢ s ∈ t.

3. If [s] = [t], then [choose(s)] ∈ [t], since [choose(s)] ∈ [s] by Choice. Using (2), we know now that we can derive choose(s) ∈ t from P. Analogously, we can derive choose(t) ∈ s and therefore by Ext also s = t.

□

Now, we can prove that our candidate for an initial model is actually a model in our logics.

Theorem 3.15 Let P be a consistent standard \overline{Σ}-presentation and V ⊆ X ∪ X. Then I_{P}(V ) is a model of P.

Proof: Let I stand for I_{P}(V ) in the following.

Lemma 3.14 guarantees that the relations ∈ and = are interpreted correctly. Remark that Paramodulation and PartialReflex guarantee that the relation = is a congruence. The satisfaction of existential formulas ‘t ↓’ follows from the definition of the interpretation: by construction of I , [t] is defined if and only if t ↓.

In order to prove that I is a model of P, we prove that all clauses in P are valid in I . Suppose G ⇒ L is in P and δ is a (I , X ∪ X)-variable assignment, such that I ⊧ δ(G). Let us define the \overline{Σ}-substitution δ′, such that [δ′(x)] = δ(x) for all x ∈ X ∪ X, i.e. I ⊧ δ′(G) by Lemma 3.12 (use δ′ as σ and δ defined by δ(x) = [x] for all x ∈ X). So I ⊧ δ′(A) for any atom A in the conjuction of atoms G. By definition of I and Lemma 3.14 P ⊢ δ′(A) and so P ⊢ δ′(G). Then we can use the SubstConform rule on G ⇒ L, followed immediately by k times Cut (where k is the number of atoms in G), in order to get P ⊢ δ′(L). Hence, I ⊧ δ(L) by definition of I . □

There remains to show completeness of deduction and initiality. Both proofs are in fact similar to those for G^{n}-logics [6].

Theorem 3.16 Let P be a consistent standard \overline{Σ}-presentation and L a (\overline{Σ}, X)- atom. P ⊧ L if and only if P ⊢ L.

Proof: Since the rules in PL are correct we already know that if P ⊢ L, then P ⊧ L. Conversely if P ⊧ L, since 𝕀^{I_{P} (V )} is a model of P, we know that under any assignment α, 𝕀^{I_{P} (V )}, α ⊧ L. Applying this to the assignment δ defined by δ(x) = [x] for any x in V , we get that δ(L) is valid in 𝕀^{I_{P} (V )}. δ(L) is of one of the following forms: [s] = [t], [s] ∈ [t], or [s] ↓. From 𝕀^{I_{P} (V )} ⊧ [s] = [t], 𝕀^{I_{P} (V )} ⊧ [s] ∈ [t], 𝕀^{I_{P} (V )} ⊧ [s] ↓, we get by definition of 𝕀^{I_{P} (V )}, P ⊢ s = t, P ⊢ s ∈ t, P ⊢ s ↓. So P ⊢ L. □

Theorem 3.17 Let P be a consistent standard \overline{Σ}-presentation. For all models J of P, there is a unique \overline{Σ}-homomorphism h : I_{P}(∅) → J .

Proof: The homomorphism is defined by h([t]) = t^{J} for any \overline{Σ}-term t. Let us check that it satisfies Definition 3.6. Let I be I_{P}(∅), J be any \overline{Σ}- interpretation, and h : I → J be the function h : U_{I} → U_{J} defined by h([t]) = t^{J} . It satisfies:

• for all (F, ∅)-terms T , [t] ∈ [T ] implies P ⊢ t ∈ T , so t^{J} ∈ T^{J} . Then h([t]) = t^{J} ∈ h([T ]) = T^{J} ;

• for all constants c ∈ F ∪ F other than 𝕌, h([c]) = c^{J} ;

• for all (F, ∅)-terms T_{1}, T_{2} of kind TTYPE, for all [t_{1}] ∈ [T_{1}] and [t_{2}] ∈ [T_{2}], h(([t_{1}], [t_{2}])^{I} ) = h([(t_{1}, t_{2})]) = (t_{1}, t_{2})^{J} = (t_{1}^{J} , t_{2}^{J} )^{J} = (h([t_{1}]), h([t_{2}]))^{J} whenever ([t_{1}], [t_{2}]) exists;

• for all (F, ∅)-terms T , T′ of kind TYPE, for all [t] ∈ 𝕋(T )^{I} and for all [f ] ∈ 𝕋(T \underrightarrow{}T′)^{I} , h([f ]([t])^{I} ) = h([f (t)]) = f (t)^{J} = f^{J} (t^{J} )^{J} = h([f ])(h([t]))^{J} whenever [f ]([t]) exists.

Unicity of the homomorphism h from I to J is proved as usual by structural induction on t. □

3.5 Pragmatics

The following extension to the grammar given in Section 3.1 covers the entire specification language used in the illustrations in Section 2:

SPEC  ::= NAME DECLS CLAUSE | NAME [VARS] DECLS CLAUSE
DECLS ::= DECL | DECL, DECLS
DECL ::= NAME | CONST : TERM
CLAUSE ::= … | ATOMS ⇒ CLAUSE | CLAUSE ∧ CLAUSE
| ATOMS ⇔ ATOMS | ATOMS | ∀ VARS : TYPE • CLAUSE
CONST ::= … | →
VARS  ::= VAR | VAR, VARS
TYPE ::= TERM

The main points to note in the transformation from the above into the kernel language defined in Section 3.1 are these: a name used in a declaration is replaced by the declarations to which it refers, the associated variables and clauses being incorporated too; set-valued terms used as types in declarations have to be replaced by their element types (cf. Z); the same holds for types of quantified variables in clauses; each constant declaration c : T generates a clause c ∈ T ; each quantified variable declaration x : T generates an atom x ∈ T in the premiss of the clause where x occurs; declarations of total functions f : S → T generate f : S \underrightarrow{}T and a clause s ∈ S ⇒ f (s) ∈ T ; and clauses have to be converted to Horn form.

4 Illustrations of Proofs

Compared to Z specifications, our framework has some restrictions: we do not allow arbitrary quantifications, nor explicit negation. However this is a deliberate decision, since restricting our presentations to Horn clauses with equalities and membership atoms gives three great advantages:

• The operational semantics of our presentations is given by conditional rewriting. Our specifications are actually programs executable with an interpretor of rewrite rules.

• We claim that we can provide an automatic tool for building a conditional term rewriting system equivalent to a given presentation using a saturation technique.

• We also think possible to obtain with the same technique, a refutationally complete procedure for proving a theorem in the initial model of a presentation. This proof procedure uses an ordering on terms and atoms to apply inference rules only on maximal literals in the clauses, which reduces the search space.

Using the saturation procedure or the refutational theorem prover we have in mind, requires to be in equational Horn clause logic. So the first step is to establish a correspondance between deduction with rules in PL written P ⊢ Φ, and deduction in Horn clause logic written P ⊢_{HCL} Φ.

Let us replace SubType, Choice and Ext by Horn clause axioms and consider the set HA of Horn axioms described in Table 2.

Now deduction rules WellDef, PartialReflex, Axioms, SubstConform, Cut and Paramodulation are deduction rules for partial Horn deduction. A little more work must be done for eliminating WellDef, PartialReflex, that requires to transform atoms t ↓ into t ∈ 𝕌 (see [6]). Eventually every predicate different from equality has to be turned into a boolean function. Let us call Θ these two transformations. Then one can prove as in [6] that for any ground atom L, P ⊢ L if and only if Θ(P ∪ HA) ⊢_{HCL} Θ(L).

However, for a better readability, in the examples below, we do not perform the transformation Θ.

Let us now briefly recall the saturation procedure as described for instance in [2, 16]. The three main inference rules are superposition into conclusion, superposition into premisses and equality resolution. Subsumption by another clause and elimination of tautologies are also used to eliminate redundant clauses.

SubType-H:  t ∈ S ∧ T ↓∧ S ≤ T ⇒ t ∈ T
PairType1:  x ∈ X ∧ y ∈ Y ∧ (x, y) ↓∧ (X × Y ) ↓⇒ (x, y) ∈ (X × Y )
PairType2:  (x, y) ∈ (X × Y ) ⇒ x ∈ X ∧ y ∈ Y
AppType:  x ∈ X ∧ z ∈ (X \underrightarrow{}Y ) ∧ z(x) ↓ ⇒ z(x) ∈ Y

FApply:  x ∈ X ∧ y ∈ Y ∧ z ∈ (X \underrightarrow{}Y ) ∧ (x, y) ∈ z ⇒ z(x) = y
FGraph:  x ∈ X ∧ y ∈ Y ∧ z ∈ (X \underrightarrow{}Y ) ∧ z(x) = y ⇒ (x, y) ∈ z
RApply:  x ∈ X ∧ y ∈ Y ∧ z ∈ (X ↔ Y ) ∧ (x, y) ∈ z ⇒ z(x, y)
RGraph:  x ∈ X ∧ y ∈ Y ∧ z ∈ (X ↔ Y ) ∧ z(x, y) ⇒ (x, y) ∈ z

SubSet:  x ∈ y ∧ y ∈ ℙ(z) ⇒ x ∈ z
Choice-H:  s ∈ t ⇒ choose(t) ∈ t
Ext-H:  choose(x) ∈ y ∧ choose(y) ∈ x ⇒ x = y

Table 2: HA –Horn axioms

An ordered strategy is used for reducing the search space by using only maximal terms and literals w.r.t. a given ordering for inference computation. A saturation process is a sequence of presentations (P_{0}, P_{1}, …), also called a derivation, where P_{i} is deduced from P_{i−1} by application of one inference rule. This derivation must be fair in the intuitive sense that no clause is forgotten in the process of generating consequences. P_{0} is consistent if and only if the empty clause does not belong to any P_{i}. Moreover if P_{∞} is the set of persisting clauses in this fair derivation and does not contain the empty clause, then one can construct from P_{∞} a conditional term rewriting system which is terminating and confluent in the initial model of P_{0}. This indeed provides a way to compute in a finite and unambiguous way the normal form of any expression in P_{0}. The complete description of the process and its proof can be found in [6].

For understanding the proof tools proposed below, we first show the transformation of the initial Z-style specification NaturalNumbers given in Section 2 into a presentation in our logic, according to Section 3.5. Note that specifying succ to be a total function would amount to adding to the following presentation the clause: x ∈ ℕ ⇒ succ(x) ∈ ℕ.

NaturalNumbers

ℕ : 𝕋(ℙ(𝕀))

0 : 𝕋(𝕀)

succ : 𝕋(𝕀 \underrightarrow{}𝕀)

≤ , < : 𝕋(𝕀 ↔ 𝕀)

∀ x, y : 𝕋(𝕀) •

0 ∈ ℕ

succ ∈ ℕ \underrightarrow{}ℕ

≤ ∈ ℕ ↔ ℕ

< ∈ ℕ ↔ ℕ

x ∈ ℕ ⇒ 0 ≤ x

x ∈ ℕ ∧ y ∈ ℕ ∧ x ≤ y ⇒ succ(x) ≤ succ(y)

x ∈ ℕ ⇒ 0 < succ(x)

x ∈ ℕ ∧ y ∈ ℕ ∧ x < y ⇒ succ(x) < succ(y)

Considering this last set of clauses, with an adequate ordering on terms and formulas, and an ordered strategy, there is no possible superposition into the conclusions, neither into premises, so the presentation is saturated, hence consistent. The ordering may be built with a lexicographic path ordering (see for instance [4]) from a precedence ≻ including ≤, <, succ ≻ ℕ. To order formulas, we may ignore the membership and equality relations, map atoms and terms to multisets of sequences, and compare sequences with the multiset extension of the lexicographic extension of ≻. For instance to compare the two atomic formulas x ≤ y and x ∈ ℕ, we compare {(≤, x, y)} and {(ℕ, x)}. Since ≤ ≻ ℕ, we get (≤, x, y) ≻_{lex} (ℕ, x), {(≤, x, y)} ≻_{lex}^{mult} {(ℕ, x)}, and thus x ≤ y greater than x ∈ ℕ. It may be worth emphasising that with this saturation technique, we can handle a limited form of negative assertion. Assume for example that we want to state in our presentation that ∀ x ∈ ℕ • ¬(x = succ(x)). The negative clause (x ∈ ℕ) ∧ (x = succ(x)) ⇒ is added to the presentation and superpositions are performed. With an ordered strategy, the saturation process terminates and proves the consistency of the whole presentation. Here to compare the two atomic formulas x = succ(x) and x ∈ ℕ, we compare {(x), (succ, x)} and {(ℕ, x)}. Since succ ≻ ℕ, we get (succ, x) ≻_{lex} (ℕ, x), {(x), (succ, x)} ≻_{lex}^{mult} {(ℕ, x)}, and thus x = succ(x) greater than x = succ(x) and x ∈ ℕ.

Then we can prove by refutation ∃ x ∈ ℕ • ¬(x = succ(0)). In this case, the clause ⇒ (x ∈ ℕ) ∧ (x = succ(0)) is added, and superposition is performed with a renaming of (x ∈ ℕ) ∧ (x = succ(x)) ⇒ and generates ⇒ (0 ∈ ℕ) ∧ (0 ∈ ℕ), then the empty clause.

Taking ℕ for X in GenericSequences, the specification gets transformed into the following one:

NaturalSequences NaturalNumbers

seq : 𝕋(ℙ(𝕀) \underrightarrow{}ℙ(𝕀))

⟨ ⟩ : 𝕋(ℙ(𝕀))

⟨ ⟩ : 𝕋(𝕀 \underrightarrow{}ℙ(𝕀))

⌢ : 𝕋((ℙ(𝕀) × ℙ(𝕀)) \underrightarrow{}ℙ(𝕀))

length : 𝕋(ℙ(𝕀) \underrightarrow{}𝕀)

∀ x : 𝕋(𝕀) • ∀ s, t, u : 𝕋(ℙ(𝕀)) •

seq ∈ ℙ(ℕ) \underrightarrow{}ℙ(𝕀)

⟨ ⟩ ∈ seq(ℕ)

⟨ ⟩ ∈ ℕ \underrightarrow{}seq(ℕ)

⌢ ∈ seq(ℕ) × seq(ℕ) \underrightarrow{}seq(ℕ)

length ∈ seq(ℕ) \underrightarrow{}ℕ

s ∈ seq(ℕ) ⇒ ⟨ ⟩ ⌢ s = s

s ∈ seq(ℕ) ⇒ s ⌢ ⟨ ⟩ = s

s ∈ seq(ℕ) ∧ t ∈ seq(ℕ) ∧ u ∈ seq(ℕ)

⇒ s ⌢ (t ⌢ u) = (s ⌢ t) ⌢ u

length(⟨ ⟩) = 0

x ∈ ℕ ∧ s ∈ seq(ℕ) ⇒ length(⟨x⟩ ⌢ s) = succ(length(s))

Extending the previous precedence with length ≻ seq, 0, succ, this presentation is proved consistent. With similar arguments as previously, one can prove that it remains consistent if we add the following statement:

∄x ∈ ℕ, s ∈ seq(ℕ) • length(s) = length(⟨x⟩ ⌢ s).

The technique extends to the higher-order example of MappingSequences in Section 2. The difficulty again is to compare the terms mapseq(f )(s ⌢ t) and mapseq(f )(s) ⌢ mapseq(f )(t) with a suitable ordering. This can be done also by mapping each term to a sequence and comparing them with a lexicographic path ordering. The sequence corresponding with the first term is, e.g., (mapseq, f , (⌢, s, t)). The sequence corresponding with the second term is (⌢, (mapseq, f , s), (mapseq, f , t)). Assuming mapseq ≻ ⌢ in the precedence, mapseq(f )(s ⌢t) is greater than mapseq(f )(s)⌢mapseq(f )(t), and superposition can be applied only on the first term. Then it is not difficult to see that the whole presentation is saturated, thus consistent.

However, in order to prove a theorem such as ∀ f , s • length(mapseq(f )(s)) = length(s), we need an inductive theorem prover. Induction is also necessary to prove the totality of functions declared as partial, and this is certainly a domain for further investigations. This discussion leads to the conclusion that rewriting techniques offer good possibilities for (semi-)automated theorem proving in our framework. There is surely some work to adapt existing theorem provers for our logic, but the changes seem to be reasonably simple.

5 Conclusion

The framework proposed here has been largely compared to the abstract data types approach and to Z specifications in the previous sections. But other works have strong connections too.

• First of all, this work is derived from R^{n}-/G^{n}-logics presented in [8]. The construction of R^{n}-/G^{n}-logics starts with Russell’s ramified theory of types, to build a set-theoretic framework providing expressive typing, higher-order functions and initial models at the same time. The parameter n, which is a natural number, gives a bound on the nesting depth of the sets used in interpretations. The difference from Russell’s ramified theory of types is the consideration of non-term-generated models. R^{n}-logics are axiomatisable by an order-sorted equational Horn logic with a membership predicate, and G^{n}-logics provide in addition partial functions. The framework proposed in this paper is a refinement of G^{n}–logics with an extended type system. Kinds, not existing in G^{n}-logics, are added, and operators ×, \underrightarrow{}and ↔ provide further refinements of the type structure. The deduction rules are quite similar to those given for G^{n}-logics.

• ETL [10] is in fact a fragment of R^{n}-logics [6]. An ETL presentation is a triple [[Ω, V , E]], such that Ω is a set of function symbols, V is a set of unsorted variables and E is a set of Ω-Horn clauses using only equality “=” and the typing relation “:” as binary operators. The typing relation satisfies the paramodulation axiom and therefore it can be used as a new relation symbol in our logic. Remark that we cannot reuse “∈” for this purpose, since it has more properties than “:” in ETL. So it is possible to construct a presentation, such that an Ω-atom is true in our logic if and only if it holds in ETL.

• Power and unified algebras have been proposed and compared in [15] and also greatly influenced our framework. Concerning power algebras, the main difference is the absence of a predefined empty set, which corresponds to the bottom element in unified algebra, and of predefined singletons. Instead we can define empty sets and singletons in our logic. The other operators of power algebras: inclusion, intersection and union, can be axiomatized in the same way as in unified algebras [15]. Hence we can encode power algebras (apart from extensional equality of sets, of course) in our framework, and come quite close to unified algebras.

• More generally this work has similarities with higher-order functional langages. Some higher-order features are provided, since function graphs are specified as set constants, which can be passed to other functions as higherorder arguments. During the last years, a number of papers have dealt with the extension of first-order algebraic specifications to higher-order ones. Among them are [9, 17, 12, 14, 13, 11]. Our approach differs from [11] for instance in that our formal basis is set-theoretic rather than purely algebraic and provides a uniform treatment of typing and higher-order functions. Compared with λ-calculi, we have deliberately omitted the abstraction operator in order to minimize the functions in the initial model, which may be crucial for limiting the search space for automated theorem proving.

References

[1] J. R. Abrial. B-Tool Reference Manual. Edinburgh Portable Compiler, 1991.

[2] L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), pages 462–476, 1992.

[3] J. Dawes. The VDM-SL Reference Guide. Pitman, 1991.

[4] N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1 & 2):69–116, 1987.

[5] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Equations and initial semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.

[6] C. Hintermeier. Déduction avec sortes ordonnées et égalités. Thèse de Doctorat d’Université, Université Henri Poincaré – Nancy 1, Oct. 1995.

[7] C. Hintermeier, H. Kirchner, and P. D. Mosses. Combining algebraic and set theoretic specifications. In M. Haveraaen, O. Owe, and O-J. Dahl, editors, Recent Trends in Data Type Specification”, Proc. 11th Workshop on Specification of Abstract Data Types joint with the 9th general COMPASS workshop. Oslo, Norway, September 1995. Selected papers, volume 1130 of Lecture Notes in Computer Science, pages 255–273. Springer-Verlag, 1996.

[8] C. Hintermeier, H. Kirchner, and P. D. Mosses. R^{n}- and G^{n}-logics. In G. Dowek, J. Heering, K. Meinke, and B. Möller, editors, Higher-Order Algebra, Logic, and Term Rewriting, volume 1074 of Lecture Notes in Computer Science, pages 90–108. Springer-Verlag, 1996.

[9] T. S. E. Maibaum and C. J. Lucena. Higher order data types. International Journal of Computer and Information Sciences, 9:31–53, 1980.

[10] V. Manca, A. Salibra, and G. Scollo. Equational type logic. Theoretical Computer Science, 77(1-2):131–159, 1990.

[11] K. Meinke. Universal algebra in higher types. Theoretical Computer Science, 100:385–417, 1992.

[12] B. Möller. Algebraic specifications with high-order operators. In L. Meertens, editor, Proceedings IFIP TC2 Working Conf. on Program Specification and Transformation, pages 367–392. IFIP, Elsevier Science Publishers B. V. (North-Holland), 1987.

[13] B. Möller, A. Tarlecki, and M. Wirsing. Algebraic specification with built-in domain constructions. In M. Dauchet and M. Nivat, editors, Proceedings of CAAP’88, Lecture Notes in Computer Science, pages 132–148. Springer-Verlag, 1988.

[14] B. Möller, A. Tarlecki, and M. Wirsing. Algebraic specifications or reachable higher-order algebras. In D. Sannella and A. Tarlecki, editors, Recent Trends in Data Type Specification, volume 332 of Lecture Notes in Computer Science, pages 154–169. Springer-Verlag, 1988.

[15] P. D. Mosses. Unified algebras and institutions. In Proceedings 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, pages 304–312, 1989.

[16] R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In D. Kapur, editor, Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), volume 607 of Lecture Notes in Computer Science, pages 477–491. Springer-Verlag, 1992.

[17] A. Poigné. Partial algebras, subsorting and dependent types. prerequisites of error handling in algebraic specifications. In Proceedings of Workshop on Abstract Data Types, volume 332 of Lecture Notes in Computer Science. Springer-Verlag, 1988.

[18] J. M. Spivey. Understanding Z: a specification language and its formal semantics. Cambridge University Press, 1988.

[19] A. N. Whitehead and B. Russell. Principia Mathematica, volume 1. Cambridge University Press, Cambridge, MA, 1925.

[20] M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 13, pages 675–788. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1990.

Recent Publications in the BRICS Report Series

RS-96-52 Claus Hintermeier, H� el� ene Kirchner, and Peter D. Mosses. Combining Algebraic and Set-Theoretic Speci�cations (Extended Version). December 1996. 26 pp. Appears in Haveraaen, Owe and Dahl, editors, Recent Trends in Data Type Speci�cation: 11th Workshop on Speci�cation of Abstract Data Types, joint with 8th COMPASS Workshop, Selected Papers, LNCS 1130, 1996, pages 255�274.

RS-96-51 Claus Hintermeier, H� el� ene Kirchner, and Peter D. Mosses. R^{n}- and G^{n}-Logics. December 1996. 19 pp. Appears in Gilles, Heering, Meinke and M� oller, editors, Higher-Order Algebra, Logic, and Term-Rewriting: 2nd International Workshop, HOA ’95 Proceedings, LNCS 1074, 1996, pages 90�108.

RS-96-50 Aleksandar Peke� c. Hypergraph Optimization Problems: Why is the Objective Function Linear? December 1996. 10 pp.

RS-96-49 Dan S. Andersen, Lars H. Pedersen, Hans H� uttel, and Josva Kleist. Objects, Types and Modal Logics. December 1996. 20 pp. To be presented at the 4th International Workshop on the Foundations of Object-Oriented, FOOL4, 1997.

RS-96-48 Aleksandar Peke� c. Scalings in Linear Programming: Necessary and Suf�cient Conditions for Invariance. December 1996. 28 pp.

RS-96-47 Aleksandar Peke� c. Meaningful and Meaningless Solutions for Cooperative N-person Games. December 1996. 28 pp.

RS-96-46 Alexander E. Andreev and Sergei Soloviev. A Decision Algorithm for Linear Isomorphism of Types with Complexity Cn(log^{2}(n)). November 1996. 16 pp.

RS-96-45 Ivan B. Damg� ard, Torben P. Pedersen, and Birgit P�tzmann. Statistical Secrecy and Multi-Bit Commitments. November 1996. 30 pp. To appear in IEEE Transactions on Information Theory.