BRICS RS-96-49 Andersen et al.: Objects, Types and Modal Logics

BRICS

Basic Research in Computer Science

Objects, Types and Modal Logics

Dan S. Andersen Lars H. Pedersen Hans H� uttel Josva Kleist

BRICS Report Series RS-96-49

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/pub/BRICS

This document in subdirectory RS/96/49/

Objects, Types and Modal Logics^{∗}

Dan S. Andersen  Lars H. Pedersen  Hans Hüttel

Josva Kleist^{†}

December 1996

Abstract

In this paper we present a modal logic for describing properties of terms in the object calculus of Abadi and Cardelli [AC96]. The logic is essentially the modal mu-calculus of [Koz83]. The fragment allows us to express the temporal modalities of the logic CTL [BAMP83]. We investigate the connection between the type system Ob_{1<:μ} and the mu-calculus, providing a translation of types into modal formulae and an ordering on formulae that is sound w.r.t. to the subtype ordering of Ob_{1<:μ}.

1 Introduction

In [AC94a, AC94b, AC94c, AC96] Abadi and Cardelli present and investigate several versions of the ς-calculus, a calculus for describing central features of object-oriented programs, with particular emphasis on various type systems.

In this paper we present a modal logic for describing dynamic properties of terms in the object calculus. By dynamic properties we mean properties specifically related to the behaviour over time of a term. We also examine the relation between the type system with recursive types Ob_{1<:μ} for the ς-calculus and the modal mu-calculus [Koz83]. It turns out that there are close correspondences between the type system and a fragment of the mu-calculus using maximal fixedpoints. In particular, there is a sound and complete translation from types to logical formulae preserving typability and the subtype ordering, when we interpret subtyping as containment. Phrased differently, the translation establishes a Curry-Howard-style result in that it allows us to view ς-calculus terms as realizers of certain mu-calculus formulae.

∗To be presented at FOOL4 (Workshop on the Foundations of Object-Oriented Languages), La Sorbonne, Paris, January 18, 1997

†Address: Dep. of Computer Science, Aalborg University, Frederik Bajersvej 7, 9220 Aalborg, Denmark. Email: {hans,kleist}@cs.auc.dk

2 The ς-calculus and its reduction semantics

There are various versions of the ς-calculus. In this paper we shall consider what is essentially the simple object calculus of [AC94b] with booleans added. The set of object terms, Obj, is defined by the following abstract syntax:

a ::= [l_{i} = ς(x_{i}:A_{i})b_{i}]_{i∈I}  objects
| x  self variables
| a.l  method activation
| a.l ⇐ ς(x:A)b  method override
| fold(A, a) | unfold(a) recursive fold/unfold
| if(a, a, a) | true | false booleans

Here x_{i} ∈ SVar range over self variables, l_{i} ∈ MNames range over method names and A_{i} ∈ Types. We let m(a) denote the set of method names and fv(a) the set of free self variables in a.

The original presentation of the ς-calculus uses a small-step reduction semantics, which is also used in the labelled transition semantics in the following section.

Let a = [l_{i} = ς(x_{i}:A_{i})b_{i}]_{i∈I}. Then the reduction rules are given by

a.l_{k} ⇝ b_{k}{^{a}/_{x_{k}}} (k ∈ I)

a.l_{k} ⇐ ς(x:A)b ⇝ [l_{i} = ς(x_{i}:A_{i})b_{i}, l_{k} = ς(x:A)b]_{i∈I\{k}}(k ∈ I)

if(true, a_{1}, a_{2}) ⇝ a_{1} if(false, a_{1}, a_{2}) ⇝ a_{2}

unfold(fold(A, a)) ⇝ a

The activation of the method l_{k} results in the method body being activated with the self variable being bound to the original object. Method override results in an object with the overridden method exchanged with the new method.

The reduction order is leftmost; this we express through evaluation contexts (C[·]) which have the following abstract syntax (with [·] denoting the hole of the context):

C[·] ::= [·].l | [·].l ⇐ ς(x:A)b | unfold(·) | fold(·) | if(·, a_{1}, a_{2})

and an evaluation strategy given by the transition rule

\frac{a ⇝ b}{C[a] ⇝ C[b]}

In the labelled transition semantics we will need to talk about objects converging to a value. This notion is of course defined modulo some notion of value; suppose that we have a well-defined notion of value, that a is an object and v a value. We then write a ⇓ v (“a converges to the value v”) if there is a terminating reduction sequence a ⇝ a_{1} ⇝ ⋯ v. We write a ⇑ (“a diverges”) if there is no v such that a ⇓ v.

3 Types

One of the main motivation for the ς-calculus is that of studying various type systems of object-oriented programming languages within a unified framework. In this paper we shall consider the type system Ob_{1<:μ} from [AC94b] as presented in [GR96].

3.1 The type language

The set of Ob_{1<:μ} type expressions Type is defined via the following abstract syntax:

A ::= Bool | [l_{i}:A_{i}] | Top | μ(X)A | X

Here Bool denotes the only ground type, namely that of truth values. [l_{i}:A_{i}] denotes an object record type, where the method l_{i} has type A_{i}. Top denotes the most general or unspecified type, μ(X)A is a recursive type and X ranges over TypeVar, the set of type variables.

3.2 Assigning types to objects

Ob_{1<:μ} has two kinds of judgments. Type judgments on the form Γ ⊢ a : A, state that the object a has type A under the assumptions in Γ, where Γ describes typing assumptions of self variables. For instance, Γ(x) = A states that we assume that the free self variable x has type A.

The type system Ob_{1<:μ} also incorporates a notion of subtyping, whose intended informal interpretation is that of capturing some types being more general than others. The expression A <: B denotes that A is a subtype of B and thus that objects of type A may be used instead of objects of type B.

Subtyping judgments Γ ⊢ A <: B state that the type A is a subtype of B, given the subtyping assumptions in Γ. Here the typing assumptions in Γ describe subtyping constraints on type variables. Γ(X) = E states that we assume X <: E.

In order to ensure uniqueness of recursively defined types Abadi and Cardelli define a syntactic predicate of formal contractivity on type variables. A ≻ Y should be read as ‘variable Y is formally contractive in type expression A’. Informally, this means that any occurrence of Y occurs within the scope of a method label in the type expression E. The rules defining the predicate are shown in Table 1.

\frac{X ≠ Y}{X ≻ Y}  \overline{Top ≻ Y}  \overline{[l_{i}:A_{i}] ≻ Y}  \frac{A ≻ Y}{μ(X)A ≻ Y}

Table 1: Formal contractivity

A type of Ob_{1<:μ} is well-formed if it can be formed using the inference rules of Table 2.

The subtyping relation is expressed in the inference rules of Table 3. Finally, an object a has type A under assumptions Γ if Γ ⊢ a:A can be

inferred by the type assignment rules in Table 4. An object term a is said to be typable if for some type A we can infer that ∅ ⊢ a:A.

4 A labelled transition semantics

The correspondence between object types and modal logic is based on the labelled transition semantics used to interpret logical formulae. As our labelled transition semantics, we shall use that proposed by Gordon and Rees in [GR96]. The syntax has been altered very slightly in that boolean values

[Type Object] \frac{Γ ⊢ A_{i} ∀i ∈ I}{Γ ⊢ [l_{i}:A_{i}]_{i∈I}}  [Type top] \overline{Γ ⊢ Top}
[Type X]  \frac{X ∈ dom(Γ)}{Γ ⊢ X}  [Type Rec] \frac{Γ[X <: Top] ⊢ A A ≻ X}{Γ ⊢ μ(X)A}

Table 2: Well-formed types

[Sub Refl] \frac{Γ ⊢ A}{Γ ⊢ A <: A}  [Sub Trans] \frac{Γ ⊢ A_{1} <: A_{2} Γ ⊢ A_{2} <: A_{3}}{Γ ⊢ A_{1} <: A_{3}}
[Sub X] \frac{Γ(X) = A}{Γ ⊢ X <: A} [Sub top] \frac{Γ ⊢ A}{Γ ⊢ A <: Top}
[Sub obj] \frac{K ⊆ L i ∈ L j ∈ K Γ ⊢ A_{i}}{Γ ⊢ [l_{i}:A_{i}]_{i∈L} <: [l_{j}:A_{j}]_{j∈K}}
[Sub rec] \frac{Γ ⊢ μ(X_{1})A_{1} Γ ⊢ μ(X_{2})A_{2} Γ[X_{2} <: Top, X_{1} <: X_{2}] ⊢ A_{1} <: A_{2}}{Γ ⊢ μ(X_{1})A_{1} <: μ(X_{2})A_{2}}

Table 3: The subtyping relation

[Var]  \frac{Γ(x) = A}{Γ ⊢ x:A}  [Select]  \frac{Γ ⊢ b:[l_{i}:B_{i}]_{i∈I} j ∈ I}{Γ ⊢ b.l_{j}:B_{j}}

[Object] \frac{Γ[x_{i}:A] ⊢ b_{i}:B_{i} ∀i ∈ I A ≡ [l_{i}:B_{i}]_{i∈I}}{Γ ⊢ [l_{i} = ς(x_{i}:A)b_{i}]_{i∈I} : A}

[Update] \frac{Γ ⊢ a:A Γ[x:A] ⊢ b:B_{j} j ∈ I A ≡ [l_{i}:B_{i}]_{i∈I}}{Γ ⊢ a.l_{j} ⇐ ς(x:A)b : A}

[Fold]  \frac{A ≡ μ(X)A Γ ⊢ a:A\{A/X\}}{Γ ⊢ fold(A, a) : A} [Unfold]  \frac{A ≡ μ(X)A Γ ⊢ a:A}{Γ ⊢ unfold(a) : A\{A/X\}}
[If]  \frac{Γ ⊢ a:Bool Γ ⊢ a_{1}, a_{2} : A}{Γ ⊢ if(a, a_{1}, a_{2}) : A}  [Subsump] \frac{Γ ⊢ a:A_{1} Γ ⊢ A_{1} <: A_{2}}{Γ ⊢ a : A_{2}}

Table 4: Type assignment

can now appear. Transitions are on the form a ^{\overline{}^{α}} b — this transition describes that the object term a admits the observation α and then becomes the object term b.

In the labelled transition semantics, terms are always annotated with their type. The types of Ob_{1<:μ} are divided into two classes, active and passive. Active types are the types of values. Only Bool is active, so in our presentation all values are booleans. Recursive types, object types and Top are passive types. At active types a program must converge to a value before it can be observed; at passive types a program performs observable actions unconditionally, whether or not it converges.

The observations, α ∈ Obs, take the following forms:

α ::= true | false | l | l ⇐ ς(x)e | unfold

These observations should be interpreted as follows: An object term allows the observation true (resp. false) if the term is of type Bool and has the value true (resp. false.) An object term allows the observation l if it has a method labelled l. An object term allows the observation l ⇐ ς(x)e if the object can have its method labelled l redefined as ς(x)e. And finally, an object term always allows the observation unfold – intuitively, this corresponds to ‘unfolding’ the object by substituting self variables by their corresponding objects.

The labelled transition semantics is defined by the minimal family of relations

\{ ^{\overline{}^{α}} | α ∈ Act\}

closed under the rules in Table 5.

[Trans Bool]  \frac{a ⇓ v ∈ \{true,false\}}{a_{Bool} ^{\overline{}^{v}} 0}

[Trans Select] \frac{A ≡ [l_{i}:A_{i}]_{i∈I} j ∈ I}{a_{A} ^{\overline{}^{l_{j}}} a.l_{j} _{A_{j}}}

[Trans Update] \frac{A ≡ [l_{i}:A_{i}]_{i∈I} j ∈ I x:A ⊢ e:A_{j}}{a_{A} ^{\overline{}^{l_{j}⇐ς(x)e}} a.l_{j} ⇐ ς(x:A)e_{A}}

[ Trans Unfold] \frac{A ≡ μ(X)A B ≡ A[A/X]}{a_{A}  ^{\overline{}^{unfold}} unfold(a)_{B}}

Table 5: The rules of the labelled transition semantics

The notion of bisimulation equivalence ∼ is defined as usual [Par81, Mil89]. Definition 1 (Bisimulation) Bisimilarity ∼ is the greatest binary relation on ς-calculus terms that satisfies the following:

a ∼ b if and only if

1. a ^{\overline{}^{α}} a′ ⇒ ∃ b′ s.t. (b ^{\overline{}^{α}} b′ ∧ a′ ∼ b′)

2. b ^{\overline{}^{α}} b′ ⇒ ∃ a′ s.t. (a ^{\overline{}^{α}} a′ ∧ a′ ∼ b′).

If a ∼ b we say that a and b are bisimilar.

We sometimes index bisimilarity w.r.t. types, writing a ∼_{A} b if a:A and b:A and a and b are bisimilar. It should be noted, though, that Definition 1 not only relates terms a_{A} and b_{A} on their type A, but also on all of their supertypes. That is, if the subtype relation

A <: B_{1} <: B_{2} <: ⋯ <: B_{n}

holds, then Definition 1 states that the following must hold:

a_{A} ∼ b_{A} ⇒ a_{B_{1}} ∼ b_{B_{1}}, …, a_{B_{n}} ∼ b_{B_{n}}

In the following we refer to the bisimulation of Definition 1 as Gordon-Rees bisimulation or bisimulation in the sense of Gordon and Rees.

5 A logic for objects

The logic we shall use is a version of the modal mu-calculus [Koz83] interpreted over the labelled transition system defined in the previous section. This logic also corresponds to the Hennessy-Milner logic of [HM85] extended with (local) recursive definitions [Lar90].

5.1 Syntax of formulae

The set of mu-calculus formulae is given by

F ::= F_{1} ∨ F_{2} | F_{1} ∧ F_{2} | ⟨α⟩F | [α]F | X | νX.F | μX.F
| ⟨true⟩tt | ⟨false⟩tt | tt | ff
α ::= l | unfold | l ⇐ ς(x)e

Here X ranges over the set of formula recursion variables FormVar. tt and ff are atomic formulae, not to be confused with the boolean values of the ς-calculus. The modalities of the logic are indexed by the observations from the labelled transition semantics. Intuitively, a formula ⟨α⟩F is true for an object o if o allows some observation α such that F is true for the resulting object. Similarly, a formula [α]F is true for the object o if all observations of α will result in an object for which F is true. A syntactic constraint is imposed on the form of formulae including true and false, as the only way an object can allow a boolean observation is by terminating.

5.2 Semantics of formulae

We interpret our logic over the labelled transition system of the previous section. If a formula F is true for an object a, we say that a satisfies F.

The denotation of a formula is the set of object terms that satisfy F. As formulae may contain free variables. the denotation of a formula is seen relative to an environment σ : FormVar ↪ P(Obj) which for a given variable, returns the set of objects which satisfies the formula bound to that variable.

We can extend operations and predicates on sets of objects to environments. For any two environments σ_{1}, σ_{2} we write σ_{1} ⊆ σ_{2} iff for all variables we have that σ_{1}(X) ⊆ σ_{2}(X). If S is a set of objects, we write σ ⊆ S if for all X we have that σ(X) ⊆ S. Similarly, σ_{1} ∪ σ_{2} is the environment σ such that σ(X) = σ_{1}(X) ∪ σ_{2}(X).

The semantics of formula not using the recursion operators can then be defined as:

[[tt]]σ = Obj
[[ff]]σ = ∅
[[F_{1} ∨ F_{2}]]σ = [[F_{1}]]σ ∪ [[F_{2}]]σ
[[¬F]]σ = Obj \ [[F]]σ
[[X]]σ = σ(X)
[[⟨l⟩F]]σ = \{a | ∃b : a ^{\overline{}^{l}} b and b ∈ [[F]]σ\}
[[[l]F]]σ = \{a | ∀b with a ^{\overline{}^{l}} b : b ∈ [[F]]σ\}
[[⟨l ⇐ ς(x)a⟩F]]σ = \{a | ∃b : a ^{\overline{}^{l⇐ς(x)a}} b and b ∈ [[F]]σ\}
[[[l ⇐ ς(x)a]F]]σ = \{a | ∀b with a ^{\overline{}^{l⇐ς(x)a}} b : b ∈ [[F]]σ\}

The operators νX.F and μX.F are local recursion operators. For any recursive formula νX.F or μX.F we define a declaration function

D_{F} : (FormVar ↪ P(Obj)) → P(Obj) by D_{F} (σ) = [[F]]σ

Both recursion operators denote a solution to the equation X = F, that is, we want an environment σ such that [[X]]σ = [[F]]σ. A σ with this property is called a model.

One may easily show that (FormVar ↪ P(Obj), ⊆), the set of environments ordered under inclusion, constitutes a complete lattice and that the function D_{F} is a monotonic function for any recursive formula νX.F or μX.F. Consequently, Tarski’s fixedpoint theorem [Tar55] for complete lattices and monotonic functions, guarantees that models always exist for any recursive formula. Theorem 2 (Maximal and minimal model) Given a recursive formula F of the form νX.F or μX.F, there exist models σ_{max} and σ_{min} given by:

σ_{max} = ⋃{σ | σ ⊆ D_{F} (σ)}
σ_{min} = ⋂{σ | D_{F} (σ) ⊆ σ}

σ_{max} is the maximal model w.r.t. ⊆ and σ_{min} is the minimal model w.r.t. ⊆.

The ν-operator is taken to indicate that we want the model σ_{max}, whereas the ν-operator is taken to indicate that we want the model σ_{min} and thus the semantics of the recursion operators is

[[νX.F]]σ = σ_{max}(X)
[[μX.F]]σ = σ_{min}(X)

From Theorem 2 we obtain the following definition of pre- and postmodels. Definition 3 (Pre- and post-models) Given a formula μX.F or νX.F, an environment σ is a pre-model if σ ∈ {σ | D_{F} (σ) ⊆ σ}. σ is a post-model if σ ∈ {σ | σ ⊆ D_{F} (σ)}.

Consequently, Theorem 2 says that the semantics of a ν-formula is the union of all its post-models and that the semantics of a μ-formula is the intersection of all its pre-models. When relating types and logical properties, we are primarily interested in maximal models.

6 Specifying objects

The modal mu-calculus is very powerful when used a temporal logic of labelled transition systems. It is well-known that the temporal modalities of the propositional branching time temporal logic CTL [Eme94] are expressible within the mu-calculus (in fact, it can be shown that all of CTL^{∗} [Eme94] can be expressed within the mu-calculus).

In this short section we shall describe how properties of ς-calculus can be described this way. We let the set Act denote the set of possible observations; we write [Act]F as an abbreviation of ⋀_{α∈Act}[α]F and similarly, we write ⟨Act⟩F as an abbreviation of ⋁_{α∈Act}⟨α⟩F.

The CTL temporal modalities can be defined as

AGF = νX.F ∧ [Act]X
EGF = νX.F ∧ ([Act]ff ∨ ⟨Act⟩X)
EFF = μX.F ∧ ⟨Act⟩X
AFF = μX.F ∧ (⟨Act⟩tt ∧ [Act]X)
U_{F,G}^{s} = μX.G ∨ (F ∧ ⟨Act⟩tt ∧ [Act]X)
U_{F,G}^{w} = νX.G ∨ (F ∧ [Act]X)

The intuitive interpretation of these modalities is

AGF: An object o satisfies AGF, a ∈ [[AG]]σ_{max}, if F is satisfied by all states of any transition path of o.

EGF: EGF is satisfied by an object o if there exists some transition path of a such that F is satisfied by all states of the path.

EFF: The dual of AGF. An object o satisfies P_{F} if F is satisfied by some state along some transition path.

AFF: Guarantees that F will sooner or later be true along any transition path.

U^{s}(F, G), U^{w}(F, G): The meanings of U^{w}(F, G) and U^{w}(F, G) only differ slightly. The idea is that an object o satisfies U^{s}(F, G) or U^{w}(F, G) if F is satisfied by o until G at some point is satisfied. The difference is that U^{w}(F, G) does not guarantee that G will ever be satisfied. U^{s}(F, G) is called strong until, and U^{w}(F, G) weak until.

So notice that invariance properties are expressed using maximal recursion, whereas eventuality properties are expressed using minimal recursion.

The following example illustrates how an object can be specified using the CTL modalities: Example 1 In [AC96] a calculator object is described. The behaviour of the calculator can informally be stated as follows: Either one of the methods enter, add or sub can be invoked, which will result in a new calculator, or the method equals can be invoked resulting in termination. In the following let Act be defined as Act = {enter, add, sub}.

The formula F shown below specifies the observations that must be allowed by a calculator object of recursive type. The formula G describes what must always hold about the methods enter, add and sub of the calculator object:

F = ⟨unfold⟩tt ∧ [unfold]tt ∧ [Act]ff,
G = ([add]tt ∧ ⟨add⟩tt) ∨ ([sub]tt ∧ ⟨sub⟩tt)
∨ ([enter]tt ∧ ⟨enter⟩tt) ∧ [unfold]ff.

To express that it holds that F is satisfied until G at some point will be satisfied we use the connective “strong until” and write:

U^{s}(F, G).

We write that U^{s}(F, G) must always hold as

AGU^{s}(F, G)

The specification of the calculator object is then a combination of AGU^{s}(F, G) and the specification for the equals method:

F_{eq} = ⟨unfold⟩([equals]tt ∧ ⟨equals⟩tt) ∧

[unfold]([equals]tt ∧ ⟨equals⟩tt)

The final correctness specification looks as follows:

AGU^{s}(F, G) ∨ F_{eq}.
□

7 Types as logical formulae

In this section we shall show an intimate correspondence between the types of Ob_{1<:μ} and the formulae of Form. Types are certain invariance properties and subtyping corresponds to inclusion between logical properties.

7.1 The translation

In order to be able to express the typings of objects in our modal logic we introduce the atomic formula isBool, which is the logical formula corresponding to Bool. isBool has the following semantics:

[[isBool]]σ = {a | a:Bool}

The reason for introducing a special atomic formula, which models the basic type Bool, is that the mu-calculus connectives alone cannot express that an object of type Bool will allow precisely the observations true or false – in order to achieve this, we would need infinite conjunctions. Further, the fact that an object of type Bool can diverge in the reduction semantics cannot be expressed. In other words, it seems reasonable that the base types should be modelled by atomic formulae.

Only certain formulae can occurs as the translations of Ob_{1<:μ} types. We shall call such formulae type formulae. The abstract syntax of type formulae is as follows:

F ::= tt | (⋀_{i∈I}⟨l_{i}⟩t(F_{i})) ∧ (⋀_{i∈I}[l_{i}]t(F_{i})) | isBool
| X | νX.⟨unfold⟩t(F) ∧ [unfold]t(F)

We denote the set of type formulae by Form_{t}.

We are now able to introduce the translation T : Type → Form_{t} from types to type formulae as follows:

T (Top) = tt
T (Bool) = isBool
T ([l_{i}:A_{i}]_{i∈I}) = (⋀_{i∈I}⟨l_{i}⟩T (A_{i})) ∧ (⋀_{i∈I}[l_{i}]T (A_{i}))
T (μ(X)A) = νX.⟨unfold⟩T (A) ∧ [unfold]T (A)
T (X) = X

Not surprisingly, the type Top is assigned the formulae tt, since all typable objects have type (or supertype) Top. The type Bool is as a special case translated to the atomic formula isBool. The mu-calculus translation of an object type reflects the possible method invocations that can be performed with respect to objects of the object type. The specification for a recursive object type is an invariance property. It states that it must always be possible to perform a transition on unfold leading to the specification for an object type, and that we must therefore consider the maximal interpretation of the logic formula. In other words, the μ becomes a ν when passing from types to formulae.

The translation defined by T is similar to the notion of characteristic formula [IS94] for the typings of objects. It is not the case, though, that these characteristic formulae express all possible behaviours of objects. In particular, it is not possible to prove that the logic for object types fully characterizes the bisimulation of Gordon and Rees, as the types and thus the type formulae say nothing about the possibility of method overrides. (This is exemplified towards the end of this section.)

7.2 Soundness and completeness of the translation

The translation presented here is correct in a very precise sense. In order to express this, we need to formulate the logic counterparts of the typability notions. Definition 4 expresses the notion of subtyping with respect to the modal formulae for types. Definition 4 Let A, B ∈ T ype and Γ some well formed environment. We say that Γ models the subtyping relation A <: B written

Γ ⊧ A <: B

if for some post-model σ it holds that [[T (A)]]σ ⊆ [[T (B)]]σ and σ(X) ⊆ [[T (C)]]σ for all (X <: C) ∈ Γ.

Lemma 5 relates the standard subtype judgments, which are of the form Γ ⊢ A <: B, to the inclusion relation between logical properties. The lemma is interesting in its own right and is also going to be useful in the proof of Theorem 6. Lemma 5 Let A, B ∈ T ype, Γ some well formed environment and Γ ⊢ A <: B. Then Γ ⊧ A <: B. Proof. By induction in the proof tree of Γ ⊢ A <: B, that is, by inspecting the rules for subtyping.

Sub Refl: It follows directly that [[T (A)]]σ ⊆ [[T (A)]]σ.

Sub Top: Since [[T (Top)]]σ = Obj it must hold that [[T (A)]]σ ⊆ [[T (Top)]]σ for all types A ∈ Type.

Sub Object: Let [l_{i}:A_{i}]_{i∈I} <: [l_{i}:A_{i}]_{i∈J} for some indexing sets I, J for which it holds that J ⊆ I. By definition of t, T ([l_{i}:A_{i}]_{i∈I}) must impose at least the same restrictions on objects as T ([l_{i}:A_{i}]_{i∈J}). It follows that [[[l_{i}:A_{i}]_{i∈I}]]σ ⊆ [[[l_{i}:A_{i}]_{i∈J}]]σ.

Sub X: Follows from the well formedness of Γ.

Sub Rec: Assume there is a post-model σ such that σ(X) ⊆ [[T (C)]]σ for all X <: C ∈ Γ, σ(X_{1}) ⊆ σ(X_{2}) and [[T (A)]]σ ⊆ [[T (B)]]σ. We must find a post-model σ′ such that σ′(X) ⊆ [[T (A)]]σ for all X <: C ∈ Γ and [[T (μX_{1}.A)]]σ ⊆ [[T (μX_{2}.B)]]σ. Take σ′ defined by

σ′(X) = \{ \begin{matrix}σ(X_{1}) ∪ [[T (A)]]σ & if X = X_{1} \\ σ(X_{2}) ∪ [[T (B)]]σ & if X = X_{2} \\ σ(X) & otherwise \end{matrix}

By the assumptions [[T (μX_{1}.A)]]σ′ ⊆ [[T (μX_{2}.B)]]σ′. Thus, we only need to check that σ′ is a post-model, i.e. that

σ′(X_{1}) ⊆ [[T (A)]]σ′ and σ′(X_{2}) ⊆ [[T (B)]]σ′.

By definition of σ′, σ(X) ⊆ σ′(X) for all X. Then, since [[·]] is monotonic on σ it must hold that [[F]]σ ⊆ [[F]]σ′ for all F ∈ Form_{t}.

□

We want our translation to be sound and complete with respect to the usual typings of objects. In particular we wish to prove a statement resembling

Γ ⊢ a:A ⇔ a ∈ [[T (A)]]σ

for some Γ and σ. It turns out that this is possible, if we assume certain properties of the typing environment Γ. Theorem 6 gives us the soundness of our translation. Theorem 6 (Soundness) Let a ∈ Ob_{1<:μ}, A, B ∈ T ype and Γ ⊢ a:A, where Γ is some well formed environment. If it holds that (x:B) ∈ Γ implies [[x]]σ ∈ [[T (B)]]σ for all x ∈ dom(Γ) and some post-model σ, then a ∈ [[T (A)]]σ. Proof. By induction in the proof tree of Γ ⊢ a:A.

Val True: Obviously true ∈ [[T (Bool)]]σ, since by [ Trans Bool ] true ^{\overline{}^{true}} 0.

Val False: Similar. Val Subsumption: We have that a ∈ [[T (A)]]σ and [[T (A)]]σ ⊆ [[T (B)]]σ.

Then by Lemma 5 it must hold that a ∈ [[T (B)]]σ. Val Select: Assume that a ∈ [[T ([l_{i}:A_{i}]_{i∈I})]]σ. Then it is also the case that

a ∈ [[(⋀_{i∈I}⟨l_{i}⟩T (A_{i})) ∧ (⋀_{i∈I}[l_{i}]T (A_{i}))]]σ.

By the transition rule [ Trans Select ] and the semantics of ⟨l_{i}⟩F it is given that a.l_{j} ∈ [[T (A_{j})]]σ for all j ∈ I.

Val Unfold: Assume that a ∈ [[T (μ(X)A)]]σ. Then it is also the case that

a ∈ [[X ⇒ ⟨unfold⟩T (A) ∧ [unfold]T (A)]]σ.

This implies that

a ∈ [[⟨unfold⟩T (A) ∧ [unfold]T (A)]]σ.

Since σ is a post-model it must hold that unfold(a) ∈ [[T (A)]]σ, since by [ Trans Unfold ] a_{μ(X)A} ^{\overline{}^{unfold}} unfold(a)_{A}.

□

The completeness of the translation is given by Theorem 7. Theorem 7 Let a ∈ Ob_{1<:μ} and F ∈ Form_{t}. If a ∈ [[F]]σ then there exists a type A such that ∅ ⊢ a:A, where T (A) = F. Proof. By induction on the possible forms of F. Top: If F = tt then it must hold that a:Top, where T (Top) = tt. Bool. If F = isBool then, obviously, a:Bool. where T (Bool) = isBool. Object: Assume that

F = (⋀_{i∈I}⟨l_{i}⟩T (A_{i})) ∧ (⋀_{i∈I}[l_{i}]T (A_{i})).

It must be the case that a can perform the transitions a ^{\overline{}^{l_{i}}} a.l_{i}, where a.l_{i} ∈ [[T (A_{i})]]σ, for all i ∈ I. That is, a must at least have the type [l_{i}:A_{i}]_{i∈I}. We do not know if a may have further possibilities for transitions, a ^{\overline{}^{l_{j}}} a.l_{j} for j ∈ J, I ∩ J = ∅, which results in the typing

[l_{i}:A_{i}, l_{j}:A_{j}]_{i∈I∪J},

but we do not care about this, since

[l_{i}:A_{i}, l_{j}:A_{j}]_{i∈I∪J} <: [l_{i}:A_{i}]_{i∈I}.

Unfold: Assume that

F = X ⇒ ⟨unfold⟩T (A) ∧ [unfold]T (A).

Then, obviously, a:μ(X)A.

Var: Trivial.

□

As mentioned earlier, the characteristic formulae for object types do not fully characterize the bisimulation equivalence of objects due to Gordon and Rees. This is due to the fact that the typing of an object does not take into account the possible method overrides that can be performed on the object. In fact it is possible, with respect to an object, to do infinitely many method overrides. That is, the ς-calculus is not finite branching. This lack of information about the possible behaviour of an object carries through to the type formulae. Example 2 Consider the two objects:

a = [l_{1} = true, l_{2} = false]
b = [l_{1} = true, l_{2} = ς(x:A) x.l_{1}]

Both have the type

A = [l_{1}:Bool, l_{2}:Bool],

and supertypes B and C:

B = [l_{1}:Bool],
C = [l_{2}:Bool]

It can be shown that a ∼_{B} b and a ∼_{C} b but a ≁_{A} b, since after the method overrides a.l_{1} ⇐ ς(x)x.l_{2} and b.l_{1} ⇐ ς(x)x.l_{2}, a converges while b diverges.

The encodings of A,B and C look as follows

T (A) = (⟨l_{1}⟩T (Bool) ∧ ⟨l_{2}⟩T (Bool)) ∧ ([l_{1}]T (Bool) ∧ [l_{2}]T (Bool))
= (⟨l_{1}⟩isBool ∧ ⟨l_{2}⟩isBool) ∧ ([l_{1}]isBool ∧ [l_{2}]isBool)
T (B) = ⟨l_{1}⟩T (Bool) ∧ [l_{1}]T (Bool)
= ⟨l_{1}⟩isBool ∧ [l_{1}]isBool
T (C) = ⟨l_{2}⟩T (Bool) ∧ [l_{2}]T (Bool)
= ⟨l_{2}⟩isBool ∧ [l_{2}]isBool

If the type formulae should characterize Gordon-Rees bisimulation, then it should be the case that a, b ∈ [[T (B)]]σ and a, b ∈ [[T (C)]]σ, but a, b ∉ [[T (A)]]σ. Obviously this is not the case, since a, b ∈ [[T (A)]]σ. □

8 Conclusions and further work

In this paper we have described how certain properties of ς-calculus terms can be described within the modal mu-calculus. A natural next step is to investigate how one can use the mu-calculus to verify interesting properties of objects. The notion of model checking, that is, algorithmically checking whether a term satisfies a given modal formula [SW89], is already well understood in the context of process calculi. It remains to be seen how far we can proceed within the ς-calculus.

We have also shown a correspondence between the type system Ob_{1<:μ} for the ς-calculus and the modal mu-calculus, which captures both type assignment and subtyping.

A natural question is how much further we can go in this direction. We can easily deal with arrow types, if we introduce a simple notion of intuitionistic implication into our logic. Let us say that F implies G for some object o if o is an object abstraction which, whenever given an argument satisfying the property F becomes an object satisfying the property G.

[[F ⇒ G]]σ = {o | ∀o′ ∈ [[F]]σ : oo′ ∈ [[G]]σ}

We then get

T (A_{1} → A_{2}) = T (A_{1}) ⇒ T (A_{2})

It is straightforward to see that this extended interpretation is sound w.r.t. the subtyping rules for arrow types, and in particular for the rule

[Sub Arrow] \frac{Γ ⊢ A′ <: A Γ ⊢ B <: B′}{Γ ⊢ A → B <: A′ → B′}

which states that the arrow type is contravariant in its first second and covariant in its second argument.

This leads straight to the question of the possibility of dealing with the variance annotations suggested by Abadi and Cardelli in [AC96]. This seems to require the introduction of negation into the syntax of the logic and is a topic of further study.

The interpretation of types as modal formulae also suggests a somewhat alternative account of the semantics of types to that presented in [AC96], where the semantics of a type is a per (partial equivalence relation). This is a topic of ongoing work by one of the authors.

References

[AC94a] Martin Abadi and Luca Cardelli. A semantics of object types. In Proceedings of the 9th IEEE Symposium on Logics in Computer Science, pages 332–341. IEEE Computer Society Press, 1994.

[AC94b] Martin Abadi and Luca Cardelli. A theory of primitive objects – untyped and first-order systems. In Theoretical Aspects of Computer Software, pages 296–320. Springer-Verlag, 1994.

[AC94c] Martin Abadi and Luca Cardelli. A theory of primitive objects: Second-order systems. In Proceedings of European Symposium on Programming, number 788 in Lecture Notes in Computer Science, pages 1–25. Springer-Verlag, 1994.

[AC96] Martin Abadi and Luca Cardelli. A Theory of Objects. Springer-Verlag, 1996.

[BAMP83] M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica, 20:207–226, 1983.

[Eme94] E.A. Emerson. Handbook of Theoretical Computer Science, chapter Temporal and Modal Logic, pages 995–1072. Elsevier, 1994.

[GR96] Andrew D. Gordon and Gareth D. Rees. Bisimilarity for a firstorder calculus of objects with subtyping. In Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, 1996.

[HM85] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, January 1985.

[IS94] Anna Ingólfsdóttir and Bernhard Steffen. Characteristic formulae for processes with divergence. Information and Computation, 110:149–163, April 1994.

[Koz83] D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.

[Lar90] Kim G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72:265–288, 1990.

[Mil89] R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.

[Par81] D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings of 5th GI Conference LNCS 104, pages 167–183. Springer-Verlag, 1981.

[SW89] C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In LNCS 351, pages 369–383. Springer-Verlag, 1989.

[Tar55] A. Tarski. A lattice-theoretical fixpoint and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.

Recent Publications in the BRICS Report Series

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.

RS-96-44 Glynn Winskel. A Presheaf Semantics of Value-Passing Processes. November 1996. 23 pp. Extended and revised version of paper appearing in Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS 1119, 1996, pages 98�114.

RS-96-43 Anna Ing� olfsd� ottir. Weak Semantics Based on Lighted Button Pressing Experiments: An Alternative Characterization of the Readiness Semantics. November 1996. 36 pp. An extended abstract to appear in the proceedings of the 10th Annual International Conference of the European Association for Computer Science Logic, CSL ’96.

RS-96-42 Gerth St�lting Brodal and Sven Skyum. The Complexity of Computing the k-ary Composition of a Binary Associative Operator. November 1996. 15 pp.