Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages

Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages

Shin-ya Katsumata

Division of Informatics, University of Edinburgh, King’s Buildings, Edinburgh EH9 3JZ, Scotland

Abstract. We extend the study of the relationship between behavioural equiva- lence and the indistinguishability relation[4, 7] to the simply typed lambda calcu- lus, where higher-order types are available. The relationship between these two notions is established in terms of factorisability[4]. The main technical tool of this study is pre-logical relations[8], which give a precise characterisation of behavioural equivalence. We then consider a higher-order logic to reason about models of the simply typed lambda calculus, and relate the resulting standard satisfaction relation to behavioural satisfaction.

1 Introduction

This work is a contribution to the understanding of the relationship between behavioural equivalence and the indistinguishability relation. These notions arose from the study of data abstraction in the context of algebraic specifications. Behavioural equivalence identifies models which show the same behaviour for any program yielding an observ- able value. This formalises an intuitive equivalence between two programming environ- ments that show the same behaviour to programmers, regardless of differences in the representation of non-observable data types. The indistinguishability relation is a par- tial equivalence relation which identifies values in a model that are interchangeable with each other in any program context. This provides an abstract view of the programming environment based on behaviour, rather than denotation.

These two notions are useful when reasoning about specifications, and their rela- tionship has been studied in a series of papers beginning with [4] by Bidoit, Hennicker and Wirsing. They established the key idea of factorisability to relate behavioural equiv- alence and the indistinguishability relation. Their framework is infinitary first-order logic over algebras. Hofmann and Sannella[7] extended the logic over algebras to higher-order logic, which enables us to quantify over predicates and axiomatise the indistinguishability relation when the underlying signature is finite.

We further extend the target of reasoning to a language having higher-order types and functions. Higher-order functions enable us to write program-parameterised pro- grams, and are useful in program development. Thus we are interested in reasoning about specifications in such languages.

In this paper, we take the simply typed lambda calculus as the formalisation of higher-order typed languages, and give the semantics of the lambda calculus by typed combinatory algebras, which subsume a wide range of semantic frameworks including Henkin models, type frames and full-type hierarchies.

Once we introduce higher-order types, we need to consider how to extend be- havioural equivalence and the indistinguishability relation to higher-order types. In the study of the simply typed lambda calculus, there is a well-known extension method us- ing exponential relations (the following shows the case of binary relations between two combinatory algebras and ; we can extend this to -ary relations):

"!$#% '&)(* ,+.-'0/,21 "!$3 /4516"!)87

and the resulting relation is called a logical relation if it relates the interpretations in and of each constant. However, in this study, logical relations are not adequate for a couple of reasons:

1. Reachability at first-order types cannot be extended to higher-order types using the exponential relation. We see this by an example; let us consider the simply typed lambda calculus with zero and successor, namely9;:=<?> and@:=<?>

:=<?>. We give the semantics of the lambda calculus by the full-type hierarchy. A full-type hierarchy constructed from^# :=<?>

BA

. We write ^C for the set of reachable elements at type^D . We can reach any ^!EA by the term^{@ : 9} , thus^C :=<?>

F#

:=<?>. However the unary logical relation constructed from :=<?>

C :G<?> does not give reach- ability correctly at higher-order types, since :G<?>

:=<?>

H#

:=<?>

:G<?> but clearly

C :=<?>

:=<?>"I

#

:G<?>

:=<?>.

2. Logical relations are not suitable to characterise behavioural equivalence. A re- stricted notion of behavioural equivalence, called closed observational equivalence, was studied in [10]. Mitchell showed representation independence theorem; if there exists a binary logical relation between two models such that the relation is bijective on the observable types, then these two models are closed observationally equiv- alent. He showed that the converse is also true when the underlying signature has only first-order constants. However this is not satisfactory for two reasons; one is the above restriction to first-order constants, and the other is that in general log- ical relations do not compose, despite the fact that behavioural equivalence is a transitive relation.

To solve these problems, we use pre-logical relations[8] by Honsell and Sannella instead of logical relations. They are a generalisation of logical relation, and have sev- eral characterisations; a relation is pre-logical iff it satisfies the basic lemma (theorem 1 below), and a pre-logical relation can be seen as a correspondence in the sense of Schoett[12] between two combinatory algebras. Roughly, a pre-logical relation is a re- lation satisfying ^{J K} . Thus pre-logical relations allow flexibility at higher-order types while logical relations are determined uniquely at all types from the relations at base types. Of course logical relations are included in pre-logical relations, but also the reachability predicate and other relations are included in this class. Another advantage of pre-logical relations is that they are closed under composition, which is a desirable property for characterising behavioural equivalence.

This paper is organised as follows: section 2 introduces basic definitions of the sim- ply typed lambda calculus, pre-logical relations and partial equivalence relations(PERs).

Section 3 establishes a relation between behavioural equivalence and existence of pre- logical relations. We also introduce another model equivalence and show that it is equiv-

alent to behavioural equivalence. In section 4 we study properties of the indistinguisha- bility relation, which turns to be a pre-logical PER over the underlying model. In section 5 we show that behavioural equivalence is factorisable by indistinguishability. We move to higher-order logic and its semantics in section 6. We introduce two semantics; one is the standard model and the other is the relative model w.r.t. some PER. We show that the quotient model of higher-order logic by a PER and the behavioural model w.r.t.

the PER are logically equivalent. We prove this by showing that they are behaviourally equivalent w.r.t. boolean observations. In section 7 we apply these results to reasoning about specifications.

2 Preliminaries

2.1 Syntax of the Simply Typed Lambda Calculus

Definition 1 (Higher-Order Signature). Let ^L be a set. We define the set of types

M%NPO L

by BNF^{DRQSQUTV+ D D} where^{TW! L} . A higher-order signature (or simply signature) is a pair of sets ^{L YX} where^L gives the set of base types and^{X J X[Z\&}

M%NPO L

gives the set of typed constants for some universe^X]Z of constant symbols. We write^{^} for the pair^{^ D %!_X} . We fix a higher-order signature^{`FL YX} . We often write^{M%NPO 8a} for^{M%NPO L} .

We assume that readers are familiar with the simply typed lambda calculus. The cal- culus considered in this paper is the minimal fragment; it has only types. The lambda terms are built on a countably infinite set of variables ^b . We define a con- text by a partial function ^{cQdbfe MgNPO 8a}. Two contexts ^c and^h are separated

if ^{i jGk c "l i6j=k h mBn} . For ^{o J M%NPO 8a}, we say ^c is a ^o -context if for all

/p!

i jGk c

,^{c 0/V! o} . We say^cUqsrtQuD is a well-formed term if^cvqsrtQD is derived only from the inference rules of the simply typed lambda calculus.

2.2 Semantics of the Simply Typed Lambda Calculus

In this study, we take typed combinatory algebras as the basis for the semantics of the simply typed lambda calculus. The reason is twofold: one is that they are general enough to subsume other classes of models, such as Henkin models and type frames, and the other is that combinatory algebras and the notion of pre-logical relation, intro- duced later, are compatible. Indeed the class of combinatory algebras is closed under quotient by pre-logical PERs(proposition 2).

We write^X"w;x for the extension of a set of constants^X with^{C 2y} combinators:

Xzw;x{X}|~

C"

€ ‚



€0 ,+

D D6ƒ

D6ƒƒ ! MgNPO 8a?7

|]y ‚ + D D ƒ !

MgNPO

„a?7;3

Definition 2 (Typed Combinatory Algebra). A -typed combinatory algebra (or sim- ply combinatory algebra) is a tuple

…#?†ˆ‡‰5Š%5‡z

such that:

1. ^# is a^{MgNPO „a}-indexed family of sets (called carrier sets).

2. The application operator^{† ‡} is a family of functions having type^{# #}

#

for any^{D D ƒ ! M%NPO „a}. 3. ^{^ ‡ !$#} for each^{^ !$Xzw;x} .

4. The combinators satisfy equationsy{†/"†1\/

and^C †Ž"††EŽ"††'P†‘

for

any^/,1Ž,22 in appropriate carrier sets (superscripts and subscripts are omitted

for readability).

We write

† ‡

as a left-associative infix operator. We may omit superscripts and sub- scripts if they are obvious from the context. Script letters (

Œ’Œ’’

) are used to denote combinatory algebras while the carrier sets of these algebras are referred by normal letters (

#Y(“Œ’’Œ’

). We write^”V•

„a

for the collection of -combinatory algebras.

Definition 3 (Henkin Model/Type Frame/Full Type Hierarchy). A combinatory al- gebra is called:

– a -Henkin model if extensionality holds:^{-Pa!~# 3u–-/~!)# 3=“†‘‡~/_}

† ‡ /—˜™$š

.

– a -type frame if^{# ,J # #} and^{\† ‡ /›{'œ/}.

– a -full type hierarchy if^{# # #} and^{V† ‡ /›{'œ/}. We note that a full-type hierarchy is uniquely determined by the carrier sets for base types.

Example 1. The following is a higher-order signature^5ž

>

Ÿ

L

ž

>

YXz5ž

>

for the finite sets of natural numbers.

L

5ž

>

 ‘T¢¡‘¡‘£5

¤G¥

@¦¥

7

X"ž

>

 §§¨„©Y©ª«5¬

¨8©2©ª

.­®ˆ§¨8©Y©5ª€V¨„©Y©ª«2¯

:G<?>

°.±‘²Œ²

:=<?>

:G<?>

³´

:=<?>

:=<?>

¨8©Y©5ª5

n

5ž

>

.;Š7

:=<?>

5ž

>

Šs|µŠ%

ž

>

5ž

>

5ž

>

¶P·§5³ˆ¸



:=<¢>

¨8©2©ª‚0

ž

>

5ž

>

?¹°³=º»§¼

5ž

>

V¨„©Y©ª

7

The constant

¶P·§5³ˆ¸

takes a predicate

Ž

and a set^@ and yields the set which consists of the elements in^@ satisfying the predicate

Ž

. The constant

¹°³=º»§¼

judges whether a given set is empty or not.

We introduce two full-type hierarchies ^5ž

>

and ^5ž

>

over^ž

>

. In ^ž

>

, base types are interpreted as ^{# ¨8©Y©5ª5ž}

>

½G¾‚¾¢„¿m7;2#

:=<?>

5ž

>

`AsY#

5ž

>

5ž

>

FÀW0Am

. We interpret^{¶P·§5³ˆ¸} and

¹°³ˆºV»§„¼

in ^5ž

>

as follows:

¶P·§5³=¸–‡'ÁÂÃ'

b

Ä/~!

b

+'œ/[ ¾€¾?7

¹°2³ˆº»§„¼

‡ Á„Â0Ã

b

…¾‚¾sÅ\˜

b

n

The interpretation of the other constants is naturally defined.

In^(5ž

>

, base types are interpreted as^{( 5ž¨„©Y©ª}

>

Æ;¾‚¾?¿µ7GY(

:=<¢>

ž

>

vAs2(

ž

>

5ž

>

`AÇ

( ¨8©2©ª

5ž

>

. In this interpretation, a set^{b J A} is represented by its characteristic function

ÈÊÉ

Q

AË( ¨8©Y©5ª

ž

>

. We interpret^{¶P·§5³ˆ¸} and^{¹°2³ˆº»§¼} in ^ž

>

as follows:

œ¶P·§5³ˆ¸œÌ ÁÂÃ6ŽÍP,/›Ä¾€¾ÎÅa˜ÏŽ4œ/—ľ€¾Ð›'0/[…¾‚¾

¹°³=º»§„¼

Ì Á„ÂÃ

$ľ€¾ÎÅa˜ -/$!~AÑ3‘'0/[E¿

The interpretation of the other constants is naturally defined.

An environment (ranged over by ^Ò ) over a combinatory algebra is a partial function ^{bÔe Õ =Ö=×؈Ù}

SÚ

 #

. We write ^Ò

!Û#%Ü

for an environment ^Ò such that

i j=k Ò

[

i j=k c

and^{Ò œ/z!)#gÜ €Ý } for all^{/~! i j=k Ò} .

Given a combinatory algebra , we can interpret well-formed lambda terms in by the meaning function^{“Þފzßß8Š} , which maps a well-formed term^cUqsrtQuD and an environment^{Ò !R#%Ü} to a value in^# . The meaning function is defined by induction on the derivation of well-formed lambda terms, and uses a trick of compiling lambda abstraction using^C and^y in a combinatory algebra when interpreting^{à / 3 r} . For details, see [2, 11].

Proposition 1. (Semantic Substitution Lemma) Let^c and^h be separated contexts,

c

2/

QuDµqÎrÏQuD

ƒ and^h½qÎáâQD be well-formed terms,

Ó_!ã#gÜ

and^Ò

!s#ä

. Then

“ÞÞr ßߖÓu/›å

“ÞÞá ßßÒ 7

“ÞÞr`Þá“æ /6ßSßßSÓ|

Ò .

Definition 4 ( -homomorphism). A -homomorphism is a^MgNPO

„a

-indexed family of functions ^{ç Q # K( 7 =Ö=×؈Ù}

SÚ

 such that for all^{^ ! XzwGx} , ^{ç ^ ‡ Í ^ Ì} and for all^{D D ƒ ! M%NPO „a./{!}#} and^1R!}# ,^ç œ/$†‘‡s16V½ç œ/[†‘Ì ç

016

. A -isomorphism is a -homomorphism ^ç such that ^ç is bijective on each

D ! MgNPO 8a

. We write^è if there exists a -isomorphism between and .

2.3 Pre-logical Relations

First, some definitions. A relation between and (written ^{J &} ) is a^{MgNPO „a}- indexed family of sets satisfying ^{EJ # &s(} for all ^{D ! M%NPO „a}. We write

Ò Ò ƒ a!šÜ

if^{Ò !}#gÜ"Ò ƒ !š(VÜ} and for all^{/! i jGk c} , ^{Ò œ/¢ Ò ƒœ/“!Ü €Ý }. The composition of relations ^{J &} and ^{ƒ J &µé} is defined by type-wise composition of

and

ƒ. The exponential relation of

and

is defined by

VPÄ; "!$#% ê&)(* 4+¢-'0/,21 "!~3͆ˆ‡$/,5†‘ÌV1 "!$«7G3

Pre-logical relations were proposed by Honsell and Sannella[8], and are a gener- alised notion of logical relations. In this paper, we adopt the following definition of pre-logical relations.¹

Definition 5 (Pre-logical Relations[8]). A relation ^{J &} is pre-logical if 1. ^{'J ™} , or equivalently for all^„56z!m and ^œ/416ë!m , the

pair^{͆ ‡ /45† Ì 16} is included in , and

2. for all^{^ !~X wGx} , the pair ^{^ ‡ ^ Ì} is included in .

We contrast the above to the definition of logical relations. A logical relation is a type- indexed family of binary relations satisfying ^t and for each

^

!$X

,^{^ ‡ ^ Ì "!$} . Thus when we give a logical relation, we perform the following

1Originally pre-logical relations were defined over lambda applicative structures, which is a general class of set-theoretic models of the simply typed lambda calculus. In the case that the underlying models are combinatory algebras, the definition coincides with definition 5 as observed in [8].

steps: we first give a relation on base types, then extend it to higher-order types using the above scheme and check whether the interpretations in and of each of the constants are related by

. In contrast, the definition of pre-logical relations lacks right- to-left inclusion in the above scheme.² Thus it allows flexibility of choice of relations at higher-order types. We note that logical relations are also pre-logical relations, since the above scheme implies that the relation relates^{C Yy} combinators at all types.

In [8] various characterisation of pre-logical relations are studied. One notable char- acterisation is via the basic lemma.

Theorem 1 (Basic Lemma for Pre-logical Relations[8]). Let

J & . Then

-'

Ò Ò ƒ

ë!µÜ]3–

“ÞÞr ßß

Ò ÞÞr

ßß

Ò ƒ

‰!m

holds for any well-formed term^cÄq$rìQGD if and only if is a pre-logical relation.

Another notable property of pre-logical relations is that the composition of two pre- logical relations is again a pre-logical relation.

Theorem 2 (Composability of Pre-logical Relations[8]). Let ^{J &} and ^{ƒ J}

&Wé

be pre-logical relations. Then^{}í" ƒ J &›é} is a pre-logical relation.

2.4 Partial Equivalence Relations

Recall that a PER (ranged over by ^î ) over is a relation ^{î J &} such that for all^{D ! MgNPO „a},^î is symmetric and transitive. We write the domain of^î by

+î

+GÄ/m!m#

+;0/,/‰!

î 7

. Then^î is just an equivalence relation over ^{+î +}, so we write ^Þ/6ß for the equivalence class of^{/š!Ä+î +} by^î and^{# æ‘î} for the quotient

+î +

æˆî .

When a PER^{î J &} is pre-logical (or logical), we call^î a pre-logical (or logical) PER. The quotient of a combinatory algebra by a pre-logical PER is again a combinatory algebra.

Proposition 2 ([8]). Let^î be a pre-logical PER over .

1. The tuple^{0# æˆî «ï Þ5Š%‡ ߜ} where^{Þ/uߢï Þ1GßP Þ/g† ‡ 1;ß} is a -combinatory algebra.

We call this the quotient of by^î , and write it by^*æˆî .

2. Let ^{cðqÛr QD} be a well-formed term and ^{Ò !ñ# æ‘î Ü} . Then ^{\æ‘î“ÞÞr ßßÒ}

ÞWÞÞr ßßSÓGß

where^ӓ!$#%Ü and^{Ӝ/z! Ò 0/} for all^{/~! i jGk c} . Definition 6 (Projection). We define the projection relation^ò

î J

*æ‘î

& as the following^M%NPO

„a

-indexed family of binary relations:

ò î

5VÄ;

Þ¦ ß8

¦

]!)#

æ‘î

a&$#%a+

¦

!E+

î

u+ó7;3

Lemma 1. The projection^{ò î} is a pre-logical relation.

Proof. Clearly ^{ò î} relates all constants in^{X wGx} . From the definition of pre-logical PERs,^î is closed under the application operator. Therefore^ò

î

is so as well. ^ôõ

2Indeed, the reverse direction is required to hold only for lambda-definable elements because of the presence of the combinators in the set of constants.

3 Behavioural Equivalence and Pre-logical Relations

Behavioural equivalence identifies two models showing the same behaviour in response to all observations. Each observation compares the values of two terms of observable types, whose values are directly accessible to programmers. This definition of obser- vation formalises the use of experiments to detect the difference of behaviour of visi- ble data types between two models. Thus, intuitively speaking, if two models are be- haviourally equivalent, they provide the same programming environment to program- mers, even though they may have different implementations of invisible data types.

We establish a link between behavioural equivalence and pre-logical relations. The result is a natural extension of [8] to allow free variables of observable types, and an extension of [12] to handle higher-order types.

The definition of behavioural equivalence is adapted from [7]. There are other pos- sibilities for the treatment of free variables, but we do not discuss them. For detail, see [7]. We fix a set ^{ö ( C J MgNPO „a} called the observable types. We first introduce an auxiliary notion of^{ö ( C} -surjective environment.

Definition 7. An ^ö

( C -surjective environment between and is a tuple

c ÓÓ

ƒ

where ^c is an ^ö

( C -context and

Ӎ! #%Ü

and

Ó ƒ

!(*Ü

are environments such that

÷k

œÓ [

Õ ˆÖ=ø4ù w #

and^÷k

œÓ

ƒ

]

Õ =Ö=ø,ù w (

.

We say is^{ö ( C} -countable if the set^{Õ =Ö=ø,ù w #} is countable.

We note that if there exists an^{ö ( C} -surjective environment between and , then and are^{ö ( C} -countable. This is due to the cardinality of the set of variables.

Definition 8 (Behavioural Equivalence). We say and are behaviourally equiv- alent w.r.t. ^ö

( C (written ^{Kú ø,ù}

w ) if there exists an ^ö

( C -surjective environ- ment

c ÓÓ

ƒ

between and such that for any^D

! ö ( C and well-formed terms

c{q)r

áûQˆD , we have^{WÞÞr ßßSÓa “ÞÞá ßßSÓFÅa˜ ÞÞr ßßSÓ ƒ ÞÞá ßßSÓ ƒ}.

We also give another formalisation of behavioural equivalence. We first introduce a program equivalence in a model, then we say two models are behaviourally equivalent if the program equivalence in both models coincides.

Definition 9. 1. Let^c be an^ö

( C -context,^D

! ö ( C and ^cÛqür

áýQPD be well-

formed terms. We write

+

cþqFr

è

áÔQ%D if for all ^Ò

!U#%Ü

, we have

“ÞÞr ßßÒ

“ÞÞá ßß

Ò . 2. We write

è

ø4ù

w if^{# è (} for any^{D ! ö ( C} , and for any^{ö ( C} -context^c ,

D ! ö ( C and well-formed terms^{cUqpr áÿQD} , we have ^{+ cÛqpr}

è á Q

D

Åa˜

+

c{q)r

è

áHQˆD .

We introduce observational pre-logical relations to characterise behavioural equiva- lence (c.f. Schoett’s correspondence[12]).

Definition 10 (Observational Pre-logical Relations). An observational pre-logical re- lation ^{J &} w.r.t. ^{ö ( C} is a pre-logical relation such that for all^{D ! ö ( C} ,

\J

#

&$(

is a bijection.

Proposition 3. Let ^{J &} and^{C J &›é} be observational pre-logical relations w.r.t.^{ö ( C} . Then^{Rí C} is an observational pre-logical relation w.r.t.^{ö ( C} .

The following theorem characterises behavioural equivalence in terms of observational pre-logical relations. Simultaneously, it shows that the two formalisations of behavioural equivalence coincide.³

Theorem 3. The following are equivalent:⁴ 1. ^{Ÿú ø,ù w} .

2. and are^{ö ( C} -countable and^#

è

ø,ù

w .

3. and are ^{ö ( C} -countable and there is an observational pre-logical relation

J & w.r.t.^{ö ( C} .

Proof. (Sketch) ( ^˜ ) The assumption implies that there exists an^{ö ( C} -surjective environment ^{c ÓÓ ƒ}. From this, and are ^{ö ( C} -countable. We then define for each^{D ! ö ( C} ,^{ç Q # ™(} by^{ç ¤ ]Ó ƒœ/}

<

, where^/

< ! i j=k

c

is a variable such that^Ó0/

<

z

¤ . We can show^ç is well-defined and gives an isomorphism. Next we show ^{+ hÆqµr}

è

áÇQ6D implies ^{+ hÆqµr}

è

áÇQ6D ; the reverse direction

is by symmetry. Let^{Ò ƒ !~(*ä} . From the definition of^{ö ( C} -surjective environment, for all^{/µ! i j=k h} , there exists¹

Ý ! i j=k

c

such that^{Ò ƒœ/z Ó ƒœ1}

Ý

. Then we define an environment^{Ò !ü#}

ä

by^{Ò 0/UÓ01}

Ý

and a variable renaming by ^0/`1

Ý

. Now we have ^WÞÞr

ßßSÓã

“ÞÞr ßßÒ

“ÞÞá ßßÒ

“ÞÞá

ßßSÓ

. This implies^ÞÞr

ßß

Ò ƒ

ÞÞr

ßߖÓ

ƒ

ÞÞá

ßߖÓ

ƒ

ÞÞá ßßÒ ƒ from^{ú ø,ù}

w .

(^E˜ ) From

è

ø,ù

w , we can choose bijections ^Z for each ^{D ! ö ( C} satisfying ^{“ÞÞr ßß8 ÞÞr ßßm!… Z} for all ^{n qÄr Q"D} . Then it is easy to see that the following relation

J & is an pre-logical relation:

V

“ÞÞr ßßSÓ ÞÞr ßߖÓ

ƒ

]+

c is an^{ö ( C} -context ^{Ð cq›r Q=D нœÓÓ ƒz!)}

ÜZ

where

is clearly a bijection for each^D

! ö ( C .

(^_˜ ) Since and are^{ö ( C} -countable, for each^{D ! ö ( C} and each pair

¦

YP!ã

, it is possible to assign a distinct variable^{/ ž ‹} . Then we define an^{ö ( C} - surjective environment

c ÓÓ

ƒ

by^c

œ/

ž ‹

‰

D ,

Ӝ/

ž ‹

‰

¦ and

Ó ƒ 0/

ž ‹

‰…

. The goal^{ú ø4ù}

w follows from lemma 1. ^ôõ

Example 2. We construct a logical relation ^5ž

> J

5ž

> &

5ž

>

from the following relations at base types:

¨8©2©ªP

i

¨8©Y©5ªU

:=<?>

i

:G<?>

5ž

>

 

b È "!WÀWAm"&ÎA˙( ¨8©2©ª"+¢-/W3/~!

b

Åa˜ È œ/]ľ€¾?7

We can easily show that relates the interpretation of all constants, and by definition, it is bijective on^{T¢¡‘¡‘£ ¤;¥ 7} . Therefore we have ^ž

>

ú

¨8©Y©5ª‹

:G<?>

5ž

>

.

Example 3. In [9], the notion of constructive data refinement is formalised in terms of the existence of a pre-logical relation. They demonstrate that an implementation of

3The proof of theorem 3 does not rely on particular properties of combinatory algebras. Thus we can expect that it holds over lambda applicative structures.

4In fact still holds when dropping the condition that and are -countable.

real number computation in the programming language PCF forms a data refinement in their sense; for any model of PCF, there exists a model of real number computation such that and

+

(the -reduct of ) are closed observationally equivalent w.r.t.

T.¡‘¡‘£

. To show this, they give an actual construction of and ^{J & +} from any PCF model , where is a pre-logical relation but not a logical relation. For details, see [9]. We believe that we can replace closed observational equivalence with behavioural equivalence and we can still construct a model such that^{ú ¨8©2©ª +} .

4 Indistinguishability Relations

We introduce an equivalence of values called indistinguishability based on their be- haviour rather than their denotation. We regard two values in a model as “behaviourally”

indistinguishable if they are interchangeable in any program. This is shown by perform- ing a set of experiments; we fit one value into a program yielding a visible result, and see whether any difference is detected when we exchange the one with the other. If two values pass the above experiment over all possible programs, then we say that they are indistinguishable. This identification of values is more suitable to provide an abstract aspect of specifications.

There are several ways to formalise the above idea. In this paper we adopt the same definition of indistinguishability as [7] for combinatory algebras.

Definition 11 (Reachable). Let^{D ! MgNPO „a}. A value^{! !}#} is ^{ö ( C} -reachable if there exists an^{ö ( C} -context^c , a well-formed term^{cÄq_r QD} and^Ó$!_#%Ü such that

!

WÞÞr ßßSÓ

.

Definition 12 (Indistinguishability Relation). Let^D

!

M%NPO

„a

. We say two values

!

#"v!Î#

are indistinguishable (written^{!%$ ‡}

"

) if they are ^ö

( C -reachable and for any^ö

( C -context^c ,^{D ƒ}

! ö ( C ,

Ó)!m#%Ü

and well-formed term^c

/

QGD$q$rìQGD ƒ, we have^{“ÞÞr ßßSÓÊ/›å ! 7 WÞÞr ß}ßSÓÊ/$å&" 7

.

The indistinguishability relation is defined on each combinatory algebra. Thus^$ gives rise to a family of PERs indexed by^{”*• „a}. The results in this section are proved for only one combinatory algebra, but readers may regard them as statements for the family of indistinguishability PERs.

In ^ž

>

,^{/ $}

ž

>

‡'Á„Â0Ã

1

implies^{/  1} . We note that ^$

5ž

>

‡êÁ„ÂÃ

is a partial equivalence relation but not a total one since infinite sets of natural numbers are not^{ö ( C} -reachable.

Theorem 4. The indistinguishability relation^{$ ‡} is a pre-logical PER such that^{$ ‡}

i('*) for all^{D ! ö ( C} .

Proof. (Sketch) It is easy to see that ^{$ ‡} is a PER which relates all constants and is

i

for all ^{D ! ö ( C} . We show it is closed under application. We assume ^{¦+$ ‡} and^{/ $ ‡ 1} . Let^c be an ^{ö ( C} -context,^{D ƒƒ ! ö ( C} ,^{c 9üQdD ƒ qr QdD ƒƒ} be a well- formed term and^Ó$!_#gÜ . Since^¦ is^{ö ( C} -reachable, we can write^{¦ “ÞÞî ßßÒ} with a well-formed term^î and an environment such that^{i j=k œÓ ,l i j=k Ò ‰Än} . Then from proposition 1 and

/ $ ‡ 1

, we have^“ÞÞr

ßߖÓÊ

9 å ¦

†"/,7

WÞÞr`Þî "

æ‘9 ßSßß«œÓ|

Ò

¢,"å

/7

“ÞÞr ßߖÓu

9 å ¦

†17

. We can similarly swap^¦ and . Thus we obtain^{¦ † / $ ‡ —†1} .

By analogy with the terminology of denotational semantics, a -combinatory algebra is fully abstract when the indistinguishability relation on and the set-theoretic equality coincide (the proof is omitted).

Theorem 5. The quotient model^*æ-$

‡

is^$ -fully abstract, i.e. for all ^D

! M%NPO 8a

and^¤

?Tg!Î#

æ-$

‡

,^¤

T

iff^{¤.$ ‡0/2143}

T

.

5 Factorisability

We have seen two approaches to obtain abstract models of specifications; behavioural equivalence on the one hand and indistinguishability relation on the other hand. Both of them naturally arise from the motivation of reasoning about specifications from a behavioural point of view. Thus we are interested in considering their relationship. The key idea is the notion of factorisability[4].

Definition 13 (Factorisability). Let^î be a^{”*• „a}-indexed family of PERs and^ú be an equivalence relation over^{”*• „a}. Then

– ^ú is left-factorisable by^î if for all ^{! ”V• „a},^{*æ‘î ‡ è ‰æ‘î Ì ˜ …úš} . – ^ú is right-factorisable by^î if for all ^{! ”*• 8a}, ^{âúû ˜ *æ‘î ‡ è}

ëæˆî

Ì

.

We say^ú is factorisable by^î if both of the above hold.

In this section we show that behavioural equivalence is factorisable by the indistin- guishability relation. First we prove left-factorisabilty.

Theorem 6 (Left-Factorisability).^*æ5$

‡ è

‰æ-$

Ì$˜

Ÿú ø4ù

w .

Proof. ^{*æ-$ ‡ è ‰æ-$ Ì} implies ^{*æ-$ ‡ ú ø4ù w ëæ5$ Ì} . From theorem 4, we have

*æ-$

‡ ú

ø4ù

w and^{‰æ-$ Ì ú ø,ù w} . Thus^{ú ø4ù w} by transitivity. ^ôõ In [7], Hofmann and Sannella represented the indistinguishability relation and the “ex- periments” for behavioural equivalence in a higher-order logic, then showed that the satisfiability of the experiments coincide in each model when quotients of two mod- els are isomorphic. However this approach seems not to work in this paper, since their method depends on the finiteness of specifications to represent the indistinguishabil- ity relation, while combinatory algebras have a countably infinite number of types and

C

2y

-combinators.

The proof of right-factorisability is essentially the same as the one in [7].

Theorem 7 (Right-Factorisability).^{Ÿú ø,ù}

w

˜

*æ-$

‡ è

ëæ5$

Ì

.

Proof. (Sketch) From^{Ëú ø,ù w} , there is an observational pre-logical relation ^J

& w.r.t.^{ö ( C} . Now we define a relation^{ç J *æ-$ ‡ & ‰æ-$ Ì} :

çuÄ;

\æ-$

‡ ÞÞr ßßSÓ

‰æ-$

Ì

ÞÞr ßßSÓ

ƒ

4+

c is an^{ö ( C} -context^{Ð c{q)r QˆD Ðz0ÓÊ2Ó ƒz!$}

Ü 7

We can show that

ç

gives a partial injection in both directions. Moreover, all elements in^*æ5$

‡

and^‰æ-$

Ì

are ^ö

( C -reachable. Therefore

ç

is total and surjective, i.e. is bijective for each^D

!

M%NPO 8a

. It is easy to see that

ç

is a -isomorphism. ^ôõ