Types, Subtypes, and ASL+

David Aspinall

Department of Computer Science, University of Edinburgh, U.K.

                  e-mail: da@dcs.ed.ac.uk

Abstract. ASL+ is a formalism for specification and programming in-the-large, based on an arbitrary institution. It has rules for proving the satisfaction and refinement of specifications, which can be seen as a type theory with subtyping, including contravariant refinement for Π-abstracted specifications and a notion of stratified equality for higher-order objects. We describe the syntax of the language and a partial equivalence relation semantics. This style of semantics is familiar from subtyping calculi, but a novelty here is the use of a hierarchy of typed domains instead of a single untyped domain. We introduce the formal system for proving satisfaction and refinement and describe how it is linked to proof systems of the underlying programming and specification languages.

1 Introduction

There is a simple correspondence between the worlds of type theory and algebraic specification:

elementhood, M : A  ⟺ satisfaction, M ∈ Mod(A)
subtyping, A ≤ A′  ⟺  refinement, A′⇝A

The elementhood of a term M in a type A is like satisfaction of a specification A by a program M; to say that a type A is a subtype of another type A′ is like saying that the specification A is a refinement of the specification A′. This connection holds because we take a model-theoretic approach to specification semantics: a specification amounts to the collection of models that are permissible implementations, and the refinement A′⇝A just means that every model of A is also a model of A′. The difference is one of syntax and semantics: type theory is a game of symbol-pushing which often begins from syntactically defined relationships, whereas in our view of algebraic specification a model-theoretic semantics is paramount, and we search for sound proof-theoretic counterparts afterward.

This paper appears in Recent Trends in Data Type Specification, Springer Lecture Notes in Computer Science 906, 1995.

An example of this is a formal system introduced by Sannella, Sokołowski, and Tarlecki [15] for proving satisfaction in ASL+, an extended version of the ASL specification language. The rules of their formal system are remarkably similar to those of a subtyping system with power types, designed by Cardelli as a programming language type-system [5]. Cardelli’s system has terms of the form Power(A), which stands for the type of all subtypes of A. He uses the elementhood A : Power(A′) to stand for the subtyping A ≤ A′. In ASL+, there is a corresponding term written Spec(A), and A : Spec(A′) is the syntactic counterpart of A′⇝A. Like Cardelli’s system, ASL+ also has λ and Π-abstractions; we use them for expressing parameterised programs and specifications, and specifications of parameterised programs (an example follows below). The similarity between the systems of Cardelli and Sannella et al. is intriguing, because they were designed in isolation and from quite different motivations. It is explained, of course, by the correspondence above.

The work reported here is part of an attempt to consciously exploit this connection, by applying recent ideas from type theory to help understand and develop ASL+. The original treatment of the language and its formal systems was restricted in scope and depth. In particular, it turns out that the satisfaction system has a surprisingly complex meta-theory due to its combination of several concepts. The main focus of this paper, however, is on a new syntax and semantics for ASL+, which extend and improve the original treatment. The remainder of this section contains a brief overview of the framework; further explanation and motivations can be found in [15]. Section 2 describes the formal syntax of ASL+ and the kind-checking system used to define the semantics. In Section 3 we describe the semantics based on partial equivalence relations. Section 4 provides only an outline of the formal system for proving satisfaction; a fuller treatment will appear in [2]. Section 5 concludes.

1.1 Overview of the ASL+ framework

ASL+ is proposed as a kernel language for writing programs and specifications in-the-large; it extends the λ-calculus parameterisation mechanism of ASL. Suppose we wish to specify symbol tables for various kinds of lookup key: let KEY be a specification of a datatype of keys. A parameterised specification of symbol tables has the form:

SYMTAB =_{def} λ X ≤ KEY ….

Here the actual parameter that instantiates the variable X is required to be a specification that is a refinement of KEY . The body of the abstraction (indicated by dots) is a specification written using the parameter X. We can also write a parameterised program implementing symbol tables, parameterised on a program that implements the datatype KEY (this is like a functor in Standard ML):

SymTab =_{def} λ X : KEY ….

But SymTab isn’t directly an implementation of SYMTAB (even if it is correct); this is because SYMTAB is a mapping from specifications to specifications, not a specification itself. To write a specification of a parameterised program (a functor signature in Extended ML), we use Π-abstraction:

SYMTAB^{#} =_{def} Π X : KEY ….

The denotation of SYMTAB^{#} is a collection of functions from algebras to algebras, which might include the function denoted by SymTab. Some parameterised specifications may be viewed as specifications of corresponding parameterised programs, but in general we need both; see [15] for further details, including an explanation of a meaning for ‘^{#}’ (which we use here simply as a part of the names for Π-abstractions).

ASL+ is a higher-order framework, so we may freely write higher-order specifications parameterised on SYMTAB, as well as specifications parameterised on KEY or SYMTAB^{#}, and also higher-order parameterised programs. We now highlight some aspects connected with subtyping systems which will be important later.

Subsumption and Refinement. For reference sake, we recall the characteristic rule of subtyping systems, known as subsumption:

\begin{matrix}M : A & A ≤ B \\ M : B \end{matrix}  (sub)

It expresses the idea that if A is a subtype of B, then every term of type A also has type B. In our setting, this rule is sound because of the definition of specification refinement.

Refinement of Π-specifications. There are two ways to refine specifications like SYMTAB^{#}. First, we can make design decisions by imposing further constraints on the body. Alternatively, we can remove constraints from the argument specification KEY . Both result in a smaller class of models. A simple example is to imagine that KEY includes axioms that specify an ordering on keys. But we may wish to use an implementation SymFinMap of finite maps from some type ELT to symbols, which is surely good enough for the job, and satisfies a more general specification:

SYMFINMAP^{#} =_{def} Π X : ELT ….

If KEY ≤ ELT, we have that SYMFINMAP^{#} ≤ SYMTAB^{#} and so via (sub), SymFinMap : SYMTAB^{#} too (modulo some renaming, perhaps). The principle is captured by this rule (where Γ is a list of assumptions about variables):

\begin{matrix}Γ ⊢ A′ ≤ A & Γ, X : A′ ⊢ B ≤ B′ \\ Γ ⊢ ΠX:A.B ≤ ΠX:A′.B′ \end{matrix}  (sub-Π)

This demonstrates the contravariance of the domain of function spaces. We might call this the rule of contravariant refinement, as its counterpart is known colloquially as the “contravariant rule” amongst subtyping enthusiasts.

Equality of models of Π-specifications. We would like to have a simple notion of equality on the terms of our calculus which entitles us to substitute like for like. Accepting (sub-Π), we can go further than the usual β-conversion equalities. Suppose that we have two implementations SymTab and SymFinMap, and moreover, that these are equal as functions when restricted to the domain KEY . Then they are indistinguishable when used as implementations of SYMTAB^{#}, and we write SymTab = SymFinMap : SYMTAB^{#} to mean that we may replace one for the other in any context which expects an implementation of SYMTAB^{#}. The rule for equality of λ-terms is:

\begin{matrix}Γ ⊢ A′ ≤ A & Γ, X : A′ ⊢ M = M′ : B′ \\ Γ ⊢ λX:A.M = λX:A′.M′ : ΠX:A′.B′ \end{matrix}  (eq-λ)

When terms have several types, it is possible to have different equality relations at different types. The rule (eq-λ) demonstrates that viewing terms in larger types can allow more terms to be considered equal; informally this is because there are fewer ways of distinguishing them. In general equalities become finer as the subtype hierarchy is descended. Conversely, moving from type to supertype equality is preserved; this monotonicity property that can be derived via (sub) and the rules for β-conversion. These aspects of a stratified equality (stratified over a subtyping relation) are well known in subtyping type-systems.

2 The Formalism ASL+

ASL+ is based on an arbitrary institution [12], together with an associated programming language and specification language. This means we are given a collection of signatures Σ ∈ Sign, and for each signature a collection of algebras Alg(Σ). The denotation of a program is an element of Alg(Σ) for some Σ, and the denotation of a specification is a collection of algebras, an element of Spec(Σ), writing Spec(Σ) as a shorthand for Pow(Alg(Σ)). The underlying programming language is formalized as a collection of operations for putting together programs. An arity is an element of Sign^{⋆} × Sign. A program building operator (PBO) p with arity (Σ_{1} ⋯ Σ_{k}, Σ) is a mapping Alg(Σ_{1}) × ⋯ × Alg(Σ_{k}) → Alg(Σ). Similarly, a specification building operator (SBO) s with the same arity is a mapping Spec(Σ_{1}) × ⋯ × Spec(Σ_{k}) → Spec(Σ).

The set T of terms of ASL+ is the least set such that:

1. X ∈ T;

2. If M_{1} ∈ T … M_{k} ∈ T then p[M_{1} ⋯ M_{k}] ∈ T;

3. If A_{1} ∈ T … A_{k} ∈ T then s[A_{1} ⋯ A_{k}] ∈ T;

4. If A ∈ T and M ∈ T then λX:A.M ∈ T and {M}_{A} ∈ T;

5. If M ∈ T and N ∈ T then MN ∈ T;

6. If A ∈ T and B ∈ T then ΠX:A.B ∈ T, A & B ∈ T, and Spec(A) ∈ T.

where X ranges over a fixed set of variables. The meta-variables A, B, M, N and variants range over T; the intuition is that A and B stand for terms which are specifications (also called types because of the parallels drawn in Section 1). We write λX ≤ A. M as shorthand for λX: Spec(A).M, and omit the empty bracket pairs from terms like s[ ] and p[ ].

A couple of term constructors were not mentioned in the previous section. A & B is the conjunction of the specifications A and B: this can be thought of taking the union of the requirements of A with those of B, which corresponds to the intersection of model classes in the semantics; for this reason A & B behaves as an intersection type. The singleton type {M}_{A} provides a way of linking the levels of programs and specifications which is useful for writing Π-specifications. When {M}_{A} ≤ B we know that M is an implementation of B. We treat the singleton type as the equivalence class of terms equal to M at the type A; the tag A is needed to keep track of which type we wish to think of M as inhabiting.

A context Γ is a list of declarations X_{1} : A_{1}, …, X_{n} : A_{n} in which no variable X_{i} is declared more than once. We write ⟨⟩ for the empty context, Dom(Γ) for the set {X_{i} | 1 ≤ i ≤ n}, and define the projection Γ(X_{i}) to be A_{i}. A context Γ′ extends another context Γ, written Γ ⊆ Γ′, if every declaration X_{i} : A_{i} in Γ also appears in Γ′. The free and bound variables of a term are defined as expected. Syntactical identity is modulo alphaconvertibility, and M[X := N] denotes the capture-avoiding substitution of the term N for the variable X inside the term M. Substitution extends to contexts pointwise on the A_{i}. There are three varieties of reduction on terms: β-reduction and η-reduction are as usual; additionally we use Γ-reduction, defined relative to a context Γ, as C[X] ⟶_{Γ} C[M] provided, for some M and A, Γ(X) ≡ {M}_{A} (C[−] indicates a term with a hole in it). The idea behind Γ-reduction is that if we know a variable X inhabits a type {M}_{A}, then X must be equal to M.

Example 2.1 ASL+ is intended to be instantiated with the institution independent SBOs of ASL described in [16]. These include families of operators such as the simple specification constructor ⟨Σ, Φ⟩ which has arity (ϵ, Σ) where Φ is a set of Σ-sentences, and the hiding and renaming operator D_{σ} ≡ derive from − by σ which has arity (Σ′, Σ) for each signature morphism σ : Σ → Σ′. If we use the institution of equational logic EQ, then signatures and algebras are the usual algebraic notions and sentences are equations; an orthogonal term rewriting system [9] is a suitable notion of program. PBOs might include RΦ⃗ with arity (ϵ, Σ) for a set of (oriented) Σ-equations Φ⃗ that define an orthogonal term rewriting system, and +_{Σ_{1},Σ_{2}} with arity (Σ_{1} Σ_{2}, Σ_{1} ⊎ Σ_{2}), for creating disjoint unions of rewrite systems.

2.1 Kind checking

The set T contains many nonsensical terms. Some of them are eliminated by kind checking, a syntax examination process that ensures structural wellformedness (kindability) of terms and contexts, by attaching a kind to each term according to the rules in Table 1. Kinds play a dual role, in fact; they are also used to define the semantic domains over which terms are interpreted. The kinds, ranged over by K, are formal expressions generated by the grammar:

K ::= Σ | K → K | Spec(K)

where Σ ranges over Sign. Intuitively, a base kind Σ classifies terms that denote algebras with signature Σ; the arrow kind K → K′ classifies mappings from terms with kind K to terms with kind K′, and the specification kind Spec(K) classifies collections of terms of kind K. Kind-checking involves two judgements:

Γ K-context  Γ is a kindable context.
Γ ⊢ M : K  In context Γ, M has kind K.

In the case that the second judgement holds, we say that M is kindable in Γ.

We briefly describe the system. The rules (k-empty) and (k-extend) manage contexts. Each declaration in a context must have a Spec-kind, so X : A means that X has kind K when A has kind Spec(K). The rule (k-var) derives this. The rules for PBOs (k-pbo) and SBOs (k-sbo) are similar: in each case, we must check that the operator is correctly instantiated and the final premise ensures that Γ is a kindable context in case k = 0. The rule (k-λ) gives an arrow kind to λ-abstractions; it should be compared with (k-Π) which shows that Π-abstractions stand for collections of mappings. The rule (k-app) is the obvious rule for function application. A singleton term {M}_{A} has kind Spec(K) by (k-{}) when M : K and A : Spec(K), so A stands for a collection of terms with the same kind as M. By (k- & ), we can only form conjunctions of specifications that have the same Spec kind. Finally, (k-Spec) characterises the Spec term constructor as forming collections of collections.

Example 2.2 Suppose (for simplicity) that KEY is a nullary SBO s_{k}, with arity (ϵ, Σ_{K}). Let s_{s} be an SBO that builds symbol table specifications and p_{s} a PBO that builds symbol table implementations, with Arity(s_{s}) = Arity(p_{s}) = (Σ_{K}, Σ_{S}). Now we have the following kindings:

⟨⟩ ⊢ SYMTAB : Spec(Σ_{K}) → Spec(Σ_{S}) SYMTAB ≡ λX ≤ s_{k}. s_{s}[X]
⟨⟩ ⊢ SymTab : Σ_{K} → Σ_{S}  SymTab ≡ λX:s_{k}.p_{s}[X]
⟨⟩ ⊢ SYMTAB^{#} : Spec(Σ_{K} → Σ_{S})  SYMTAB^{#} ≡ ΠX:s_{k}.s_{s}[{X}_{s_{k}}]

Properties of kind-checking. The kind-checking system is well-behaved. The rules are syntax-directed by the term M and context Γ and so the kind of M is unique. The proposition below states desirable properties of the kindchecking system; the proofs are routine inductions on kinding derivations.

Proposition 2.3 (Kind-checking) 1. Suppose Γ K-context, where Γ ≡ X_{1} : A_{1}, …, X_{n} : A_{n}. Then for all m such that 0 ≤ m < n, X_{1} : A_{1}, …, X_{m} : A_{m} is also a kindable context and for some K_{m+1}, we have X_{1} : A_{1}, …, X_{m} : A_{m} ⊢ A_{m+1} :

Spec(K_{m+1}).

⟨⟩ K-context  (k-empty)
Γ ⊢ A : Spec(K)  X ∉ Dom(Γ)

Γ, X : A K-context

(k-extend)

Γ K-context Γ ≡ Γ_{1}, X : A, Γ_{2} Γ_{1} ⊢ A : Spec(K)

Γ ⊢ X : K (k-var)

Arity(p) = (Σ_{1} ⋯ Σ_{k}, Σ) for 1 ≤ i ≤ k, Γ ⊢ M_{i} : Σ_{i} Γ K-context

Γ ⊢ p[M_{1} ⋯ M_{k}] : Σ (k-pbo)

Arity(s) = (Σ_{1} ⋯ Σ_{k}, Σ) for 1 ≤ i ≤ k, Γ ⊢ A_{i} : Spec(Σ_{i}) Γ K-context

Γ ⊢ s[A_{1} ⋯ A_{k}] : Spec(Σ)

(k-sbo)

\begin{matrix}Γ ⊢ A : Spec(K) & Γ, X : A ⊢ M : K′ \\ Γ ⊢ λX:A.M : K → K′ \end{matrix}  (k-λ)
\begin{matrix}Γ ⊢ M : K → K′ & Γ ⊢ N : K \\ Γ ⊢ M N : K′ \end{matrix}  (k-app)
Γ ⊢ M : K  Γ ⊢ A : Spec(K)

Γ ⊢ {M}_{A} : Spec(K) (k-{})

Γ ⊢ A : Spec(K)  Γ ⊢ B : Spec(K)

Γ ⊢ A & B : Spec(K) (k-&)

Γ ⊢ A : Spec(K)  Γ, X : A ⊢ B : Spec(K′)

Γ ⊢ ΠX:A.B : Spec(K → K′)

(k-Π)

Γ ⊢ A : Spec(K) Γ ⊢ Spec(A) : Spec(Spec(K))

(k-Spec)

Table 1: Kind checking in ASL+ 2. Suppose Γ ⊢ M : K. Then (a) Γ K-context, and (b) FV (()M) ⊆

Dom(Γ).

3. Weakening. If Γ ⊢ M : K, Γ ⊆ Γ′ and Γ′ K-context, then Γ′ ⊢ M : K.

4. Kind unicity. If Γ ⊢ M : K, then K is the unique such kind.

5. Decidability. It is decidable whether Γ ⊢ M : K for any given Γ, M, and K; furthermore, given just Γ and M, it is decidable whether there is such a K.

6. Substitution. If Γ, X : A, Γ′ ⊢ M : K, Γ ⊢ A : Spec(K′) and Γ ⊢ N : K′, then Γ, Γ′[X := N] ⊢ M[X := N] : K.

7. Single-step subject reduction. Suppose Γ ⊢ M : K. If any of M ⟶_{β} M′, M ⟶_{η} M′ or M ⟶_{Γ} M′, then Γ ⊢ M′ : K too.

It is important to realise that kind checking is a necessary, but not sufficient condition to ensure that a term has a well-defined meaning. There are several ways that a kindable term may fail to have a denotation in the semantics given later:

• We can write λ-abstractions over specifications. In general, we have to check that a program satisfies a specification to see that an application of such a term is defined. For example, if s_{0} is an inconsistent Σspecification, and p denotes a Σ-algebra, so Arity(s_{0}) = Arity(p) = Σ, then ⊢ (λX:s_{0}.X) p : Σ holds in the kind-checking system, but we choose to regard (λX:s_{0}.X) p as meaningless since p cannot satisfy s_{0}.

• A singleton specification {M}_{A} denotes the collection of algebras equal to M which satisfy the specification A. Again, for this to be defined, we must check that M satisfies A, which is a stronger condition than the rule (k-{}) ensures.

• We allow for partiality of PBOs and SBOs so that some instantiations of an operator may fail to denote an algebra or collection of algebras. Whilst for specifications we might instead suppose that the operator returned the inconsistent specification, it is necessary for PBOs. For example, if we wished to allow a general union operation ∪ of term rewriting systems in EQ, it may be that P_{1} ∪ P_{2} is not confluent (hence not orthogonal); so ∪ is at best a partial operator.

3 Semantics of ASL+

The semantics presented here is an altered form of the set-theoretic semantics in [15]. Along lines suggested there, we use the institution to construct a hierarchy of set-like domains D_{K}, indexed by kinds K. Programs built using PBOs have kind Σ for some specification Σ, and are interpreted as elements of D_{K} = Alg(Σ). Rather than sets, specifications with kind Spec(K) for some K are interpreted as partial equivalence relations (PERs) over D_{K} (for specifications built using SBOs, we have PERs over Alg(Σ) for some Σ). Parameterised terms with kind K → K′ are interpreted as set-theoretic partial functions in D_{K} ⇀ D_{K′}. We pause to explain these choices before presenting the definitions.

Partial equivalences. The use of partial equivalence relation models for interpreting subtyping and polymorphic type-systems is well-known (e.g., [6]). Recall that a partial equivalence relation R is a set |R| (the carrier) together with a symmetric and transitive relation −R− ⊆ |R| × |R|. The reason why we use PERs is that they model the typed equational theory of λ-calculi, and in a simple way that works well with subtyping. A type is interpreted as a PER over a set of values which are denotations of terms. Subtyping is just inclusion of PERs; if A ≤ B then for all a, b, a ⟦A⟧ b ⟹ a ⟦B⟧ b should hold. It follows that if two terms are equal at A, they are also equal at B. Typically, PER models follow an “untyped” approach, based on a global value space (e.g., the domain D of a model of the untyped λcalculus) from which all types are carved out. Here we use the hierarchy D_{K}, retaining a “typed” aspect; this is because algebras over different signatures live in different categories, so it seems natural to preserve the different value spaces in the semantics.

Partial functions. Partial functions are used because, as explained above, the true domain of a function with kind K → K′ may be smaller than K. Their use also allows a neat way of capturing the rule (sub-Π) shown in Section 1.1, via inclusion. If ΠX:A.B has kind K → K′, then we let ⟦ΠX:A.B⟧ stand for the collection of partial functions in D_{K→K′} which are total at least on ⟦A⟧, and map elements a ∈ ⟦A⟧ to elements of ⟦B⟧_{[X→a]}. So the inclusion ⟦ΠX:A.B⟧ ⊆ ⟦ΠX:A′.B′⟧ holds provided ⟦A′⟧ ⊆ ⟦A⟧ and ⟦B⟧_{[X→a]} ⊆ ⟦B′⟧_{[X→a]} for all a ∈ ⟦A′⟧. Notice that this does not work if we define ⟦ΠX:A.B⟧ as a set of total functions defined on exactly ⟦A⟧.

3.1 The semantic interpretation

We recall some nomenclature: the domain of a PER is dom(R) = {a | a R a} and a ∈ R abbreviates a ∈ dom(R). If a ∈ R then the equivalence class of a in R is [a]_{R} = {b | a R b}. Inclusion of PERs R ⊆ R′ is defined for PERs with the same carrier by a R b ⟹ a R′ b for all a, b. PER[A] stands for the set of all PERs with carrier A.

Domains for kinds and contexts. The semantic domain D_{K} associated to each kind K is a set defined by induction on the structure of K:

D_{Σ}  = Alg(Σ)
D_{K→K′} = D_{K} ⇀ D_{K′}
D_{Spec(K)} = PER[D_{K}]

where A ⇀ B is the set of partial functions from A to B. We assume that for each Σ ∈ Sign, the collection of algebras over Σ is built within some fixed universe, and so Alg(Σ) is a set; this provides a simplistic justification of the existence of the hierarchy D_{K}.

Contexts are interpreted by PERs over products of sets: A × B is the set of all ordered pairs ⟨a, b⟩ with a ∈ A, b ∈ B and π_{1}, π_{2} are the projections. Let 1 =_{def} {∗} be a single point set. The domain D_{Γ} for a kindable context Γ is defined by induction on a kinding derivation:

D_{⟨⟩}  = 1
D_{Γ,X:A} = D_{Γ} × D_{K}, where Γ ⊢ A : Spec(K)

The free variables in a term will be interpreted by projection from an environment, which is a tuple g in the domain of some context. The projections along g corresponding to a context Γ are given by:

g^{⟨⟩}(Y)  undefined, for all Y.
g^{Γ, X:A}(Y) = \{ \begin{matrix}π_{2}(g), & if Y ≡ X, \\ (π_{1}(g))^{Γ}(Y) & if Y ≢ X. \end{matrix}

We write g_{1}^{Γ_{1}} ⊆ g_{2}^{Γ_{2}} if g_{1}^{Γ_{1}}(X) = g_{2}^{Γ_{2}}(X) for all X ∈ Dom(Γ_{1}).

Semantic constructions. Here are the semantic constructions used in the interpretation. The interpretation is partial (some terms fail to denote even if they are kindable, as we have explained), so we adopt the convention that the application of any of the constructions below to an undefined argument gives an undefined result.

Let A and B be sets; R, R′ and R′′ elements of PER[A], F ∈ dom(R) → B and G ∈ dom(R) → PER[B] such that a R b implies G(a) = G(b). Then:

• Id(A, A′) ∈ PER[A] provided A′ ⊆ A and where:

a Id(A, A′) a for all a ∈ A′

• {}(R, a) ∈ PER[A] provided a ∈ A, and where:

b {}(R, a) c  iff  b R c and b R a

• λ(R, F) ∈ A ⇀ B is the partial function f defined by:

f(a) = \{ \begin{matrix}F (a) & for all a ∈ R \\ undefined & otherwise. \end{matrix}

• Π(R, G) ∈ PER[A ⇀ B] where:

f Π(R, G) g  iff  ∀a, b.a R b ⟹ f(a) G(a) g(b)

• Σ(R, G) ∈ PER[A × B] where:

c Σ(R, G) d iff π_{1}(c) R π_{1}(d) and π_{2}(c) G(π_{1}(c)) π_{2}(d)

• ∩(R, R′) ∈ PER[A] where:

a ∩(R, R′) b  iff  a R b and a R′ b

• P(R) ∈ PER[PER[A]] where:

R′ P(R) R′′  iff  R′ = R′′ and R′ ⊆ R

Constructions such as λ, Π, Σ and ∩ are well-known. For example, Π(R, G) is a PER in which two partial functions are related if they map related arguments to related results (and both must be defined on at least dom(R)). Less familiar ones include Id(A, B), which is simply a PER over elements of A with domain B on which the equivalence relation is just identity; the PER {}(R, a) which is the equivalence class of a in R, and P(R) in which two PERs are equivalent if they are equal as PERs and included in R. It is a simple matter to check that the constructions lead to values in the domains claimed, given defined arguments in the domains stated.

⟦⟨⟩⟧  = Id(1, 1)
⟦Γ, X : A⟧  = Σ(⟦Γ⟧, ⟦Γ ⊢ A : Spec(K)⟧)
⟦Γ ⊢ X : K⟧g  = g^{Γ}(X)
⟦p[M_{1} ⋯ M_{k}] : Σ⟧  = ⟦p⟧ (⟦M_{1} : Σ_{1}⟧, …, ⟦M_{k} : Σ_{k}⟧)
⟦s[A_{1} ⋯ A_{k}] : Spec(Σ)⟧  = Id( D_{Σ}, ⟦s⟧ \begin{matrix}(dom(⟦A_{1} : Spec(Σ_{1})⟧), \\ …, dom(⟦A_{k} : Spec(Σ_{k})⟧) ) ) \end{matrix}
⟦{M}_{A} : Spec(K)⟧  = {}(⟦A : Spec(K)⟧, ⟦M : K⟧)
⟦A & B : Spec(K)⟧  = ∩(⟦A : Spec(K)⟧, ⟦B : Spec(K)⟧)
⟦Spec(A) : Spec(Spec(K))⟧ = P(⟦A : Spec(K)⟧)
⟦M N : K′⟧  = ⟦M : K → K′⟧ (⟦N : K⟧)

⟦Γ ⊢ λX:A.M : K → K′⟧g

= λ(⟦Γ ⊢ A : Spec(K)⟧g, a ↦ ⟦Γ, X : A ⊢ M : K′⟧⟨g, a⟩) ⟦Γ ⊢ ΠX:A.B : Spec(K → K′)⟧g

= Π(⟦Γ ⊢ A : Spec(K)⟧g, a ↦ ⟦Γ, X : A ⊢ B : Spec(K′)⟧⟨g, a⟩)

Table 2: Semantics of ASL+ Definition of semantics. The interpretation of contexts and terms is defined in Table 2 by induction on kind-checking derivations. The interpretation of a context ⟦Γ⟧ is a PER over D_{Γ}, and the interpretation of a term, ⟦Γ ⊢ M : K⟧, is a map from dom(⟦Γ⟧) to D_{K}. If g ∉ dom(⟦Γ⟧), then ⟦Γ ⊢ M : K⟧g is undefined by convention. There is an equation in the table for each kinding rule; for readability Γ and g are omitted when they don’t play a part. We shall sometimes also omit K when it is clear from the context, writing just ⟦M⟧.

We rely upon an externally defined semantics for PBOs and SBOs: as mentioned before, ⟦p⟧ and ⟦s⟧ are partial maps between algebras or classes of algebras. SBOs ignore the equivalence relation on their arguments, and the instantiation of an SBO is interpreted as an identity PER. This means that two terms with kind Σ are equal just when they denote exactly the same algebra. (It would be interesting to extend this to allow coarser institutiondependent equalities, such as isomorphism, or even to allow ⟦s⟧ to be a PER constructor).

Example 3.1 We calculate the meaning of the closed term SYMTAB^{#}:

R =_{def} ⟦s_{k}[ ]⟧ = Id(D_{Σ_{K}}, ⟦s_{k}⟧)
⟦SYMTAB^{#}⟧ = ⟦ΠX:s_{k}.s_{s}[{X}_{s_{k}}]⟧
= Π(R, a ↦ Id(D_{Σ_{S}}, ⟦s_{s}⟧(dom({}(R, ⟦X⟧⟨⋆, a⟩))) ))
= Π(R, a ↦ Id(D_{Σ_{S}}, ⟦s_{s}⟧({a})))

By the definition of Π, ⟦SYMTAB^{#}⟧ is interpreted as the set of partial functions f from Alg(Σ_{K}) to Alg(Σ_{S}) such that ∀a ∈ ⟦s_{k}⟧. f(a) ∈ ⟦s_{s}⟧({a}). Two such functions f and f′ are equivalent if they are equal as functions when restricted to ⟦s_{k}⟧.

Properties of the semantics. It would be nice to establish that the interpretation is well-defined in the sense that whenever ⟦M : K⟧ is defined, then ⟦M⟧ ∈ D_{K}. Unfortunately, this isn’t true! The reason is that, because of the use of partial functions, a function application f(a) in the semantics may be defined “by accident” without a being in the domain of the PER that f is assumed to inhabit. This isn’t ensured by kind-checking or definedness of the interpretation function, but it is ensured by the stronger formal system of the next section. Some useful properties of the semantics can be established at this stage, nevertheless, under the assumption that everything we deal with is defined and in the domains required.

Lemma 3.2 (Semantic properties for well-defined interpretations) 1. Weakening. Let Γ, Γ′ be kindable contexts with Γ ⊆ Γ′. Let g ∈ ⟦Γ⟧ and g′ ∈ ⟦Γ′⟧ where g^{Γ} ⊆ g^{′Γ′}. Then ⟦Γ ⊢ M : K⟧g = ⟦Γ′ ⊢ M : K⟧g′.

2. Semantic contexts. Let Γ be a kindable context and Γ ⊢ X : K. Then: ∀g_{1}, g_{2}. g_{1} ⟦Γ⟧ g_{2} ⟹ g_{1}^{Γ}(X) ⟦Γ ⊢ Γ(X) : Spec(K)⟧g_{1} g_{2}^{Γ}(X)

3. Semantic substitution. Let Γ, X : A, Γ′ ⊢ M : K′, Γ ⊢ A : Spec(K), g ∈ ⟦Γ⟧, and let n = ⟦Γ ⊢ N : K⟧g. If g_{1} ∈ ⟦Γ, Γ′[X := N]⟧, and g_{2} ∈ ⟦Γ, X : A, Γ′⟧, then:

⟦Γ, Γ′[X := N] ⊢ M[X := N] : K′⟧g_{1} = ⟦Γ, X : A, Γ′ ⊢ M : K′⟧g_{2} provided g^{Γ} ⊆ g_{1}^{Γ,Γ′[X:=N]} ⊆ g_{2}^{Γ,X:SP,Γ′} and g_{2}^{Γ,X:SP,Γ′}(X) = n.

4. β and η-reduction. Suppose Γ ⊢ M : K and g ∈ ⟦Γ⟧. If either M ⟶_{β} N or M ⟶_{η} N, then ⟦M⟧g = ⟦N⟧g.

4 Satisfaction in ASL+

So far we have a formal syntax of terms, and a semantics for the kindable terms. However, not all kindable terms have a denotation in the semantics, and we have no way of proving when a program satisfies a specification (elementhood in the semantics). We now introduce the system of rules^{1} in Table 3 for proving satisfaction. Two judgements are defined:

Γ Context  Γ is a denoting context.
Γ ⊢ M : A  In context Γ, M satisfies A.

and we use some derived judgements:

Γ ⊢ A ≤ B  =_{def} Γ ⊢ A : Spec(B)
Γ ⊢ M = N : A  =_{def} Γ ⊢ M : {N}_{A}
Γ ⊢ A  =_{def} Γ ⊢ A ≤ B for some B

We have explained the “subtyping” abbreviation already. A relation of typedequality Γ ⊢ M = N : A is included in the calculus via singleton types; this has been investigated elsewhere [1].

The judgement Γ ⊢ A asserts that A is a denoting type. More generally, a denoting term M is one for which there exists an A such that Γ ⊢ M : A. Thus the rules in Table 3 can also be used to establish that a term has a denotation in the semantics. From the viewpoint of ASL+, a program term is meaningful just in case there is some specification that it satisfies, and similarly a specification is meaningful if there is another which it refines. This may seem like an odd way of determining which terms are well-formed, but typically the SBOs include operators for constructing trivial specifications, which for example may amount to some simple type-checking requirements. So if M is built from PBOs, it is natural to expect there to be some A built from SBOs such that M : A. Furthermore, we would expect A ≤ A if A is a well-formed specification. We examine this more closely next.

1These are a re-design of those in [15], which had several omissions.

Basic programs and specifications. To do anything useful, we must first have some way to prove things about the underlying programming language and specification language. A basic program P is a term built using only PBOs and basic program variables from a Sign-sorted set V_{prog}; similarly a basic specification S (or T) is built using only SBOs and variables from a Sign-sorted set V_{spec}. We abstract away from the details of the underlying proof systems and assume that there are two consequence relations [3] which describe the properties of interest:

Δ |−_{V}^{sat} P : S  basic satisfaction;
Δ |−_{V}^{ref} S ≤ T  basic refinement.

In each case, V is the set of variables (from V_{prog} and V_{spec}) free in the program or specification terms and Γ is a finite set of statements with the same form as the right hand side. Variables are needed because it is essential to have schematic assertions that allow us to deal with SBOs and PBOs applied to ASL+ terms, and in particular, ASL+ variables. The rules (pbo) and (sbo) formalize this.^{2} To apply one of these rules (backwards), one must find appropriate substitutions θ from variables in V to ASL+ terms which unify the right hand side of a sequent with the desired conclusion in ASL+. If the left hand side of the sequent Δ is non-empty, this leads to further statements to be proved in ASL+. (Of course, the substitutions θ must respect the sorts of the variables; we omit details here).

Example 4.1 In EQ, we would expect the consequence relations to include, for sets of sentences Φ_{1}, Φ_{2} over signatures Σ_{1}, Σ_{2}: |−_{{ }}^{sat} RΦ⃗_{1} + RΦ⃗_{2} : ⟨Σ_{1} ⊎ Σ_{2}, Φ_{1} ∪ Φ_{2}, ⟩ (the union of two rewrite systems satisfies a specification consisting of a union of the equations), and Rσ⃗(Φ) : S |−_{{S}}^{sat} RΦ⃗ : D_{σ}(S) (which allows renaming), where σ : Σ → Σ′ is a signature morphism, Φ is

2The vector notation P̄, etc. abbreviates vectors of arguments to PBOs and SBOs.

We have glossed over some details: there should be extra premises to ensure that the arguments are denotable: Γ ⊢ Ā etc., and we should ensure that the arity of the operators is respected.

⟨⟩ Context  (empty)
Γ ⊢ A  X ∉ Dom(Γ)

Γ, X : A Context

(extend)

Γ Context

Γ ⊢ X : Γ(X) (var)

Δ |−_{V}^{sat} p[P̄] : s[S̄] θ_{p}(P̄) = M̄, θ_{s}(S̄) = Ā Γ ⊢ θ_{p}(θ_{s}(Δ)) Γ Context

Γ ⊢ p[M̄] : s[Ā] (pbo)

Δ |−_{V}^{ref} s[S̄] ≤ t[T̄] θ_{s}(S̄) = Ā, θ_{s}(T̄) = B̄ Γ ⊢ θ_{s}(Δ) Γ Context

Γ ⊢ s[Ā] : Spec(t[B̄])

(sbo)

{Γ, X : A ⊢ M : B \atop Γ ⊢ λX:A.M : ΠX:A.B}  (Π-I)
\begin{matrix}Γ ⊢ M : ΠX:A.B & Γ ⊢ N : A \\ Γ ⊢ M N : B[X := N] \end{matrix}  (Π-E)
\begin{matrix}Γ ⊢ M : A_{1}, A_{2} & Γ ⊢ A_{1}, A_{2} : Spec(B) \\ Γ ⊢ M : A_{1} & A_{2} \end{matrix}  (&-I)
\begin{matrix}Γ ⊢ M : A_{1} & A_{2} & j = 1, 2 \\ Γ ⊢ M : A_{i} \end{matrix}  (&-E)
\begin{matrix}Γ, X : A ⊢ X : B & Γ ⊢ B \\ Γ ⊢ A : Spec(B) \end{matrix}  (Spec-I)
\begin{matrix}Γ ⊢ M : A & Γ ⊢ A : Spec(B) \\ Γ ⊢ M : B \end{matrix}  (Spec-E)
\begin{aligned}Γ ⊢ M : A & Γ ⊢ N : A & M =_{βηΓ} N \\ & Γ ⊢ M : \{N\}_{A} \end{aligned}  (\{\}-I)
{Γ ⊢ M : \{N\}_{A} \atop Γ ⊢ M : A}  (\{\}-E)

Table 3: Satisfaction Rules of ASL+ 17 a set of Σ-sentences and S stands for a basic Σ′-specification. Examples of proof rules which generate a consequence relation for |−^{ref} on the institution independent operators of ASL can be found in [11].

Some assumptions must be made of |−^{sat} and |−^{ref} , the most important of which is that they are sound with respect to the semantics of basic programs and specifications. For example, whenever P_{1} : S_{1} … P_{n} : S_{n} |−_{V}^{sat} P : S then

∀ρ, γ. ⟦P_{1}⟧ρ ∈ ⟦S_{1}⟧γ ⋀ ⋯ ⋀ ⟦P_{n}⟧ρ ∈ ⟦S_{n}⟧γ ⟹ ⟦P ⟧ρ ∈ ⟦S⟧γ

where ρ and γ are evaluations mapping Σ-variables from V_{prog} to Σ-algebras and Σ-variables from V_{spec} to sets of Σ-algebras. There are other requirements which reflect the ideas above: there should always be an S such that |−_{{ }}^{sat} P : S whenever P is a well-formed basic program with a denotation, and in this case we should have |−_{{ }}^{ref} S ≤ S to indicate that S too is well-formed and has a denotation.

Higher-order constructors. In Table 3 there is a rule of introduction and a rule of elimination for each of the higher-order term constructors.

The rules for λ-introduction (Π-I) and elimination (Π-E) are usual in all type systems with dependent Π types. For conjunction the rules are also well-known, except that the introduction rule ( & -I)^{3} restricts intersections to being formed over types which have a common supertype. This reflects the semantics: we only form collections within the same value space.

The elimination rule (Spec-E) for the Spec operator is simply the subsumption rule in a different guise. The introduction rule (Spec-E) is rather unusual: it has a simple reading (if whenever X is assumed to inhabit A, it can be shown to also inhabit B, then deduce A ≤ B), but its simplicity belies its power when combined with the other introduction and elimination rules. It is common in subtyping systems to axiomatise a separate subtyping relation with rules for each type constructor; this one rule captures the full relation. In particular, the (derived) relation ≤ is easily shown to be reflexive and transitive on denoting types, and familiar rules for subtyping intersection types follow. Also, the rule (sub-Π) shown in Section 1.1 is admissible when we close the system under a rule of η-subject reduction.

The meaning of the singleton terms is captured by ({}-I). Whenever M is convertible to N via β,η or Γ reductions, and both satisfy S, we assert that M inhabits the singleton {N}_{S}: intuitively, M is in the equivalence class of terms equal to N when considered at S. The elimination rule is weaker, it just says that when M : {N}_{A}, then M must also satisfy A.

3Notice that it has four premises, abbreviated in a hopefully obvious way.

Example 4.2 As a simple example, we can show that SymTab : SYMTAB^{#}:

P : s_{k}, P : S |−_{{S,P}}^{sat} p_{s}[P] : s_{s}[S]

⋮ ; X : s_{k} ⋮ ; X : {X}_{s_{k}} {|−_{\{ \}}^{ref} s_{k} ≤ s_{k} \atop ⊢ s_{k} ≤ s_{k}}

X : s_{k} Context
X : s_{k} ⊢ p_{s}[X] : s_{s}[{X}_{s_{k}}]
⟨⟩ ⊢ λX:s_{k}.p_{s}[X] : ΠX:s_{k}.s_{s}[{X}_{s_{k}}]

(the dots are filled by repeating the few rules on the right, and using the rule ({}-I) in the second case; we omitted the context X : s_{k} in these branches too).

This example serves to show how the proof theoretic side of the ASL+ framework is glued together, rather than illustrate the power of the language. We assumed that the main proof arises from a single sequent in |−^{sat}; in reality s_{k} and p_{s} would probably be composed of several SBOs and PBOs, and this proof could involve several invocations of the underlying proof systems.

Properties of satisfaction. Unlike the kind-checking system, it is not obvious how to apply the rules in the satisfaction system: for a given conclusion, several rules may be able to derive it. It would be interesting to examine ways of directing proof search in this system; this corresponds to looking for a type-checking algorithm for the related subtyping system. Of course, theorem proving is almost always needed at the level of basic programs and specifications anyway, so we can’t hope for a complete algorithm.

Space precludes any treatment of the meta-theory of the rules here. We mention only the crucial aspect of the system mentioned at the outset: soundness with respect to the semantics defined in Section 3. This also establishes the well-definedness of the interpretation on denotable terms and contexts.

Proposition 4.3 (Soundness and Definedness properties) 1. Agreement with kind-checking.

If Γ Context, then Γ K-context.

If Γ ⊢ M : A then for some (unique) kind K, Γ ⊢ M : K and Γ ⊢ A : Spec(K).

2. Definedness. If Γ Context, then ⟦Γ⟧ ∈ PER[D_{Γ}]. If Γ ⊢ M : A and g ∈ ⟦Γ⟧, then ⟦M : K⟧g ∈ D_{K}.

3. Γ-reduction. Suppose Γ ⊢ M : A and g ∈ ⟦Γ⟧. Then M ⟶_{Γ} N implies ⟦M⟧g ⟦A⟧g ⟦N⟧g.

4. Soundness. If Γ ⊢ M : A and g ⟦Γ⟧ g′, then ⟦M⟧g ⟦A⟧g ⟦M⟧g′

The proofs proceed by induction on derivations in the satisfaction system. Part 1 uses Proposition 2.3; parts 2–4 are proved together, using Proposition 3.2. Now we have established:

Theorem 4.4 (Soundness of Satisfaction) Γ ⊢ M : A implies ⟦Γ ⊢ M : K⟧g ∈ ⟦Γ ⊢ A : Spec(K)⟧g for all g ∈ ⟦Γ⟧. Proof A corollary of the final part of Proposition 4.3, taking g = g′. □

5 Conclusions

ASL+ provides a unified framework for programming and specification inthe-large which seems powerful. Some larger and more detailed examples than those shown here have been studied in [17, 15, 2] but work is still needed to appreciate the practical merits of the different mechanisms of parameterisation. Real specification languages built on ASL+ might not use all of the parameterisation possibilities (Extended ML, for example, lacks parameterised specifications), but it makes sense to study a complete kernel formalism to see that the distinct mechanisms can be safely combined.

There are many avenues to be explored starting from the satisfaction system of Section 4. We would like to be able to characterise the relationship between the consequence relations for PBOs and SBOs and their corresponding fragments inside ASL+. The best case would be if the extension is conservative, and complete (i.e., a converse of Theorem 4.4 holds) when the underlying relations are complete. As mentioned, we should try to find ways of directing proof search in the system, so that showing satisfaction in ASL+ is reduced to showing underlying consequences in a canonical way. Unfortunately, similar things can be tricky to show for related subtyping systems [8, 14], and the added complication of dependent Π-types makes things harder still. Also, the concise presentation of the rules shown here is somewhat provisional; although it is nice to describe, it may prove more fruitful to study a longer equivalent version where more of the rules are spelled out.

Certain extensions of the satisfaction system would be interesting. One is to allow subtyping between signatures: whenever ι : Σ_{1} ↪ Σ_{2} is an inclusion in a sub-category of signature inclusions, we can consider Σ_{2} ≤ Σ_{1} by virtue of the reduct functor. This would allow many renamings to be avoided at the level of syntax; in the semantics, we would have to reconstruct them. The subtyping semantics in [4] uses a similar technique.

As well as subtyping parallels, there are some specification languages related to ASL+. Cengarle and Wirsing [7] describe a language with higherorder parameterisation, including parameterisation on signatures. Drossopoulou and Paterson [10] have explored similar type theory connections when designing a language for writing parameterised programs and their interfaces. SPECTRAL in [13] is a design for a rich language that combines an institution-level language that has subtyping, polymorphism and dependent types with a module-level language similarly endowed for specifications and programs.

Acknowledgements. I would like to sincerely thank Don Sannella, Benjamin Pierce and Andrzej Tarlecki for their coaching and encouragement during the course of this work. Thanks are also due to Claudio Russo and Martin Hofmann for discussions about ASL+, and to the anonymous referees of ADT’94 for suggestions to improve the presentation. I was supported by a UK EPSRC postgraduate studentship.

References

[1] David R. Aspinall. Subtyping with singleton types. In Proc. Computer Science Logic, CSL’94, Kazimierz, Poland, Lecture Notes in Computer Science 933. Springer-Verlag, 1995.

[2] David R. Aspinall. Type systems for algebraic specification in-the-large. Forthcoming PhD thesis, Department of Computer Science, University of Edinburgh, 1996.

[3] Arnon Avron. Simple consequence relations. Information and Computation, 92:105–139, 1991.

[4] Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172–221, 1991.

[5] Luca Cardelli. Structural subtyping and the notion of power type. In Fifteenth Annual ACM Symposium on Principles of Programming Languages, 1988.

[6] Luca Cardelli and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417–458, 1991.

[7] María Victoria Cengarle and Martin Wirsing. A calculus of parameterization for algebraic specifications. Technical Report 94/198, Department of Computer Science, Monsahs University, 1994.

[8] Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[9] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In van Leeuwen et.al., editor, Handbook of Theoretical Computer Science, chapter 6. North-Holland, 1990.

[10] Sophia Drossopoulou and Ross Paterson. Higher order module parameterization. Technical report, Department of Computing, Imperial College, October 1993.

[11] Jorge Farrés-Cassals. Verification in ASL and related Specification Languages. PhD thesis, Edinburgh University, 1992.

[12] J. A. Goguen and R. M. Burstall. Institutions: abstract model theory for specification and programming. Journal of the ACM, 39:95–146, 1992.

[13] Bernd Krieg-Brückner and Donald Sannella. Structuring specifications inthe-large and in-the-small: Higher-order functions, dependent types and inheritance in SPECTRAL. In TAPSOFT ’91: Proc. Joint Conf. on Theory and Practice of Software Development, Brighton, 1991.

[14] Benjamin C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1), July 1994.

[15] Donald T. Sannella, Stefan Sokołowski, and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: Parameterisation revisited. Acta Informatica, 29:689–736, 1992.

[16] Donald T. Sannella and Andrzej Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76(2/3):165–210, 1988.

[17] Stefan Sokołowski. Parametricity in algebraic specifications: A case study. Technical report, Institute of Computer Science, Polish Academy of Sciences, Gdańsk, 1989.