Effectful applicative similarity for call-by-name lambda calculi

Abstract

ion result for such a generic, coinductive methodology for program equivalence.

Introduction

Program equivalence is a crucial notion in the theory of programming languages, and its study is at the heart of programming language semantics. When higherorder functions are available, programs have a non-trivial interactive behaviour, and giving a satisfactory and at the same time handy definition of program equivalence becomes complicated. The problem has been approached, in many different ways, e.g. by denotational semantics or by contextual equivalence. These two approaches have their drawbacks, the first one relying on the existence of a denotational model, the latter quantifying over all contexts, thus making the task of proving programs equivalent quite hard. Handier methodologies for proving programs equivalent have been introduced along the years based on logical relations and applicative bisimilarity. Logical relations were originally devised for typed, normalising languages, but later generalised to more expressive formalisms, e.g., through step-indexing [ 2 ] and biorthogonality [ 3 ]. Starting from Abramsky’s pioneering work on applicative bisimilarity [ 1 ], coinduction has also been proved to be a useful methodology for program equivalence, and has been applied to a variety of calculi and language features [ 17 ].

The just described scenario also holds when the underlying calculus is not pure, but effectful. There have been many attempts to study effectful calculi [ 19,16 ] by way of denotational semantics [ 9,8 ], logical relations [ 4 ], and applicative bisimilarity [ 14,7,5 ]. But while the denotational and logical relation semantics of effectful calculi have been studied in the abstract [ 11,13 ], the same cannot be said about applicative bisimilarity and related coinductive techniques. There is a growing body of literature on applicative bisimilarity for calculi with, e.g., nondeterministic [ 14 ], and probabilistic effects [ 7 ], but each notion of an effect has been studied independently, often getting different results. Distinct proofs of congruence for applicative bisimilarity, even if done through a common methodology, namely the so-called Howe’s method [ 12 ], do not at all have the same difficulty in each of the cases cited above.

The observations above naturally lead to some questions. Is there any way to factor out the common part of the congruence proof for applicative bisimilarity in effectful calculi? Where do the limits on the correctness of applicative bisimilarity lie, in presence of effects?

This paper is part of a longstanding research effort directed to giving answers to the questions above. The first two authors, together with Paul Blain Levy, have recently introduced a general notion of applicative bisimilarity for lambdacalculi based on monads and relators [ 6 ]. This provides, under mild conditions, a sound methodology for checking contextual equivalence of programs. The central idea is to take simulations as relations on terms and to use a relator to lift a (candidate) simulation to a relation on the monadic images of values. There is however little hope to prove a generic full-abstraction result in such a setting, although for certain notions of an effect, full abstraction is already known to hold [ 1,5 ].

In this paper, we study a different notion of simulation, which puts in relation not terms but their semantics. This way, interaction between terms and the environment can be modeled by an ordinary, deterministic, transition system and, with minimal side conditions, similarity can be proved to be not only a sound, but also to coincide with the contextual preorder. This, however, only holds when terms are call-by-name evaluated.

We first of all introduce a computational -calculus in which general algebraic effects can be represented, and give a monadic call-by-name operational semantics for it, showing how the latter coincides with the expected one in many distinct concrete examples. We then show how applicative bisimilarity can be defined for any instance of such a monadic -calculus, and that in all cases it is also fully-abstract. Along the lines, we also prove a CIU Theorem. 2

Mathematical Preliminaries

In this section, we recall some basic definitions and results on complete partial orders, categories, and monads. Due to space constraints, there is no hope to be comprehensive. The reader can refer to [ 6 ] for details and further references.

We assume basic familiarity with domain theory. In particular, we do not define the notions of directed complete partial order (dcpo for short), and of pointed dcpo (dcppo for short). Similarly, we do not give the notions of monotone, continuous, and strict functions, which are standard. Following [ 19,20 ], we consider operations producing effects coming from a signature. Semantically, dealing with operation symbols requires the introduction of appropriate algebraic structures interpreting such operation symbols as suitable functions. Combining the algebraic and the order theoretic structures just described, leads to consider algebras carrying a domain structure (dcppo, in this paper), and with all function symbols interpreted as continuous functions. The formal notion capturing all these desiderata is the one of a continuous -algebra [ 10 ]. Recall that a signature = (F ; ) consists of a set F of operation symbols and a map : F ! N, assigning to each operation symbol a (finite) arity.

Definition 1. Given a signature , a continuous -algebra is a dcppo (D; v; ?)

such that for any function symbol in there is an associated continuous function D : D ( ) ! D.

Example 1. Let X be a set: the following are examples of dcppo (see [ 6 ] for further examples). 1. The flat lifting Xundef of X, defined as X + fundefg, ordered as follows: x v y iff x = undef or x = y. 2. The set (X +E)undef (think to E as a set of exceptions), ordered as in previous example. We can consider the signature = fraise(e) j e 2 Eg, where each operation symbol raise(e) is interpreted as the constant inl(inr(e)). 3. The powerset PX, ordered by inclusion. The least upper bound of a chain of sets is their union, whereas the bottom is the empty set. We can consider the signature = f g containing a binary operation symbol for nondeterministic choice. The latter can be interpreted as (binary) union, which is indeed continuous. 4. The set of discrete subdistributions DX = f : X ! [0; 1] j Px2X (x) 1g over X, ordered pointwise: v iff 8x 2 X: (x) (x). The dcppo structure is pointwise induced by the one of [0; 1] with the natural ordering. The least element is the always zero distribution x 7! 0 (note that the latter is a subdistribution, and not a distribution). We can consider the signature = f p j p 2 [0; 1]g with a family of probabilistic choice operations indexed by real numbers in [0; 1]. We can interpret p as the binary operation (x; y) 7! p x + (1 p) y, which is indeed continuous.

Since we are interested in effectul calculi, we rely on monads hT; ; i [ 15 ] (on the category of sets and functions) to model the kind of effects we are interested in. For a function f : X ! T Y we denote by f y its Kleisli lifting

Y T f : T X ! T Y . We are interested in monads carrying a continuous algebra structure. That is, for a fixed signature , we require a monad T to come with a map associating to any set X an order vX on T X and an element ?X 2 T X such that (T X; vX ; ?X ) is a continuous -algebra wrt the order vX . We also require Kleisli lifting to satisfy specific continuity conditions4. The reader can consult [ 6 ] for details.

Example 2. It is easy to see that all the constructions in Example 1 carry a monad structure. 4 For all sets X; Y we require (notice that T Y being a dcppo, so is X ! T Y ) both sup F y = supf2F f y and f y(sup T ) = supt2T f y(t) to hold, where F X ! T Y and T T X are directed.

Finally, following [ 19 ] we require monads to properly interact with algebraic operations.

Definition 2. Let T be a monad carrying a continuous -algebra structure.

We say that T is algebraic if for any function f : X ! T Y , f y is -algebra

homomorphism. That is, f y( X (t1; : : : ; tn)) =

Y (f y(t1); : : : ; f y(tn)): We treat ?X as an algebraic constant, so that the above definition implies f y(?X ) = ?Y , for any f : X ! T Y . 3

Syntax and Operational Semantics

In this section we introduce a computational -calculus and give it call-by-name monadic operational semantics following [ 19 ]. We fix a signature and a monad hT; ; i satisfying the conditions of previous section.

Definition 3. For a fixed signature

are defined as follows: the sets and V of terms and values M; N ::= V j M N j (M; : : : ; M ) V ::= x j x:M:

We let letters M; N : : : and V; W; : : : to range over terms and values, respectively.

We denote by (x) the set of terms with free variables from x and write for

the set (;). Similar conventions apply to the set of values.

We give operational semantics to our calculus as in [ 19 ] (which we refer to for details). An indexed function symbol i consists of a function symbol 2 together with an index i 2 f0; : : : ; ( ) 1g. Evaluation contexts are defined by the simple grammar: E ::= [ ] j EM . Small-step semantics is defined by means of a binary relation ! on closed terms and of a ternary relation ! on closed terms and indexed function symbols, according to the rules in Figure 1.

( x:M )N ! M [N=x] (M0; : : : ; Mn 1) !i Mi

M ! N E[M ] ! E[N ]

M !i N

E[M ] !i E[N ]

We now give a monadic multi-step operational semantics to the above calculus. Multi-step operational semantics relates a closed term M to a set of elements in T V, representing finite approximations of its evaluation. We refer to elements in T V as monadic values.

Definition 4. Define the relation ) between closed terms and monadic values by the rules in Figure 2, where ? is the bottom element of T V and V is the interpretation of in T V.

V )

M ) ? (V )

M ! N

N ) t M ) t

M !i Ni M )

Ni ) ti

V (t1; : : : ; tn) supM)t t.

It is easy to prove that the set ft 2 T V j M ) tg of finite approximations of (the execution of) M is directed, meaning that it has a least upper bound. Definition 5. Define the evaluation function J K : 0 !

T (V) by JM K = 4

Observational Equivalence

In this section we give a general notion of observation on top of which we define several behavioural preorders. We rely on the basic assumption that we can only observe side effects.

Intuitively, an observation is a function that takes an element in T V representing the computation of a term and returns what we can observe about it. Since we assume that the observable part of a computation consists only of the side effects that could occur during such computation, such observable part is uniquely determined by the semantics of the operations considered.

Since we are working with an untyped calculus, it is customary not to observe values5.

Definition 6. Let 1 = f g be the one element set and !X : X ! 1 be the unique function mapping each element in X to . Define the observation function

Obs : T V ! T 1 as T (!V ). Observations trivially extends to terms by defining

Obs(M ) as Obs(JM K).

Note that by very definition of monad we have T (!V ) = ( 1 !)y. As a consequence, since T is algebraic an easy calculation shows that we have the following equalities:

Obs(?) = ?T (1);

Obs( V (V )) = 1( ); Obs( V (t1; : : : ; tn) =

1(Obs(t1); : : : ; Obs(tn)): 5 One is usually more concerned with different notions of convergence, such as may convergence or the probability of convergence.

Remark 1. Notice that the function Obs is uniquely determined by the effect signature. That is because of our choice of not distinguishing between values. Nevertheless, it is easy to see that our definition of Obs can be extended to any function f : V ! X, where the set X represents a set of observables and f encodes a ground observation on values. In fact, we would have Obs(V ) = ( f )(V ).

We can now give a general notion of contextual preorder.

Definition 7. Define contexts by the following two grammars

In this section we define the notion of applicative simulation and prove full abstraction of applicative similarity wrt the CIU preorder. First of all, we lift the notion of application from terms to monadic values. define the application t

M 2 T V of M Definition 8. For t 2 T V and M 2 to t as6: (( x:L) 7! JL[M=x]K)y(t):

It is easy to see that we have:

? ( x:N ) V (t1; : : : ; tn)

M = ?; M = JN [M=x]K; M = V (t1 M; : : : ; tn

M ); and that for terms M; N we have JM N K = JM K N: 6 Note that with a similar strategy it is possible to extend application to T V .

Definition 9. A relation R T V T V is an applicative simulation if whenever (t; u) 2 R we have

1. Obs(t) v Obs(u); 2. For any term M , (t M; u M ) 2 R.

Applicative similarity . is defined as the largest applicative simulation. We ex

tend applicative similarity to terms as follows (we overload the notation): M . N iff JM K . JN K.

Our main result is a full abstraction theorem stating that applicative similarity and the contextual preorder coincide. The proof of such result relies on a CIU Theorem [ 18 ].

Definition 10. The CIU preorder

ciu is defined by

M ciu N () 8E: Obs(JE[M ]K) v Obs(JE[N ]K) where E ranges over the set of evaluation contexts.

Theorem 1 (CIU Equivalence). The following holds: ciu = ctx :

We postpone the proof of Theorem 1 to the next section. We spend the rest of this section showing that applicative similarity is fully abstract with respect to the CIU preorder.

Proposition 1 (Soundness). The following holds: . ciu : Proof. Clearly M . N implies M L . N L, for any term L. It is then straightforward to prove that for any evaluation context E, M . N implies E[M ] . E[N ], meaning, in particular, Obs(E[M ]) v Obs(E[N ]). tu

To prove that . is fully abstract wrt ciu we have to prove so we define a grammar for monadic values as follows: ciu

.. To do T ::= t j T

M: We refer to terms generated by the above grammar as monadic terms. We can give semantics to monadic terms as monadic values via the mapping: t = t;

H I

HT M I = HT I M: Monadic term contexts (mt-contexts, for shorts) are defined by: Therefore a mt-context is an expression of the form M1 Mn (where we assume to be left associative). The lifting 4ciu of the CIU preorder to monadic terms is then defined by

T 4ciu U () 8C: Obs(HC[T ]I) v Obs(HC[U ]I):

It is easy to see that there is a bijective correspondence between evaluation contexts and mt-contexts from which it follows the equation ciu = 4ciu.

Proposition 2. The following holds: 4ciu

. : Proof. We prove that 4ciu is an applicative simulation. Suppose t 4ciu u. Obviously Obs(t) v Obs(u) since t = t (and similarly for u). Let now M be a term. We have to prove that t MH4Iciu u M holds. Let C = M1 Mn be a mt-context. Then we have to prove: Obs(HC[t M ]I) = Obs(HC[u M ]I): That immediatly follows from t 4ciu u once one observes that H( M1 Mn)[t M ]I = H( M M1 Mn)[t]I holds. tu

Corollary 1. The following holds: ciu . :

Together with Proposition 1, the above corollary gives a proof of the following:

Proposition 3. Applicative similarity is fully abstract wrt the CIU preorder.

That is: . = ciu :

What remains to be done in order to prove that applicative similarity is fully abstract wrt to the contextual preorder is to prove Theorem 1. 6

A CIU Theorem

In this section we prove Theorem 1. The proof closely follows [ 18 ], and the reader can consult the latter for further details.

We use the notion of frame stack.

Definition 11. The set of frame stacks is defined by the following grammar:

s ::= nil j [ ]M :: s:

A configuration is a pair of the form (s; M ), where s is a stack and M a term. To a stack s = [ ]N1 :: :: [ ]Nn, we can associate the evaluation context Es = N1 Nn (where to nil we associate the empty context). Vice versa, we can associate to any evaluation context E a stack sE such that E = EsE .

We now give operational semantics to configurations. Small step semantics is defined via a relation 7! between configurations, whereas multi-step semantics is defined via a relation Z) between configurations and monadic values. Both these relations are described in Figure 3.

Notice that the set ft 2 T V j (s; M ) Z) tg is directed. As a consequence, we can define the (operational) semantics L(s; M )M of a configuration (s; M ) as

Proposition 4. For any term M , evaluation context E and stack s, we have:

L(s; M )M =

sup t: (s;M)Z)t JE[M ]K = L(sE ; M )M;

L(s; M )M = JEs(M )K: In particular, we have L(nil; M )M = JM K.

(s; M N ) 7! ([ ]N :: s; M ) ([ ]N :: s; x:M ) 7! (s; M [N=x]) (s; (M1; : : : ; Mn)) 7!i (s; Mi) (s; M ) Z) ? (nil; V ) Z) V

(s; M ) Z) t (s; M ) 7! (r; N )

(r; N ) Z) t (s; M ) 7!i (si; Mi)

(si; Mi) Z) ti (s; M ) Z) V (t1; : : : ; tn)

We can now build up a proof of Theorem 1. The proof is based on an adaptation oh Howe’s technique for pure -calculus and thus we only sketch its main part. The reader can consult [ 18 ] for details. First of all, in light of previous proposition let us characterise the CIU preorder in terms of stacks and configurations.

Definition 12. Define the CIU order

ciu on terms: M ciu N

Proposition 5. The following hold:

() 8s: Obs(L(s; M )M) v Obs(L(s; N )M):

ciu = ciu :

Dealing with Howe’s technique, it is convenient to work with generalisations of relations on closed terms called -term relations.

Definition 13. An open relation over terms is a set R of triples (x; M; N ) where M; N 2 (x). A closed -term relation is closed if R .

We will use infix notation and write x ` M R N to indicate that (x; M; N ) 2 R. Finally, we will use the notations ; ` M R N and M R N interchangeably. There is a canonical way to extend a closed relation to an open one.

Definition 14. Define the open extension operator mapping a closed relation

over terms R to the open relation R over terms as follows: (x; M; N ) 2 R iff M; N 2 (x), and for all L, M [L=x] R N [L=x] holds.

The notions of reflexivity, symmetry and transitivity straightforwardly extend to open -term relation (see e.g. [ 18 ]).

We say that a relation is compatible if it is closed under the term constructors of the language. The idea of Howe’s technique is to extend a relation R to a relation RH that is compatible by construction. As a consequence, if M RH N holds, then C[M ]RH C[N ] holds as well. That means that in order to prove that a relation R is compatible it is sufficient to prove that R = RH holds. Proving the inclusion R RH is often immediate (provided that R satisfies minimal properties, e.g. reflexivity and transitivity in our case), whereas the other inclusion requires more effort.

Definition 15. Given a -term relation R the Howe’s lifting RH of R is inductively defined by the rules in Figure 4.

x ` xRM x ` xRH M

How1 x ` M RH P x ` MiRH Ni x [ fxg ` M RH L

x ` LRH x ` M LRH N

x ` x:LRN x ` x:M RH N

x ` P RN x ` (N1; : : : ; Nn)RL

How3

How4 x ` (M1; : : : ; Mn)RH L

Lemma 2 (Key Lemma). For all closed stacks s; r and closed terms M; N , if

s( ciu)H r, M ( ciu)H N , then Obs(L(s; M )M) v Obs(L(r; N )M).

Proof (Sketch.). Since Obs is continuous and L(s; M )M) = sup(s;M)Z)t t it is sufficient to prove that for every monadic value t, if (s; M ) Z) t the Obs(t) v L(r; N )M. The latter statement can be proved by induction on the derivation of (s; M ) Z) t as in [ 18 ]. tu 7 We are actually working with ( ciu) .

Corollary 2. The following holds: ( ciu)H = ciu : Proof. We already know that ciu ( ciu)H holds. To prove the other inclusion we have to prove M ( ciu)H N =) M ciu N , for all terms M; N . Suppose M ( ciu)H N . Then, for any stack s, we have s( ciu)H s. By previous lemma we have Obs(L(s; M )M) v Obs(L(s; N )M), meaning that M ciu N . tu We can finally prove Theorem 1.

Theorem 1 (CIU Equivalence). The following holds: ctx = ciu : Proof. It is immediate to see that ctx ciu. For the other inclusion, suppose M ciu N and let C be a context. We prove that C[M ] ciu C[N ] (this will give the thesis simply aplying the definition of ciu with the empty context). Since ciu = ciu = ( ciu)H , we have M ciu N and thus C[M ] ciu C[N ]. It follows C[M ] ciu C[N ]. tu 7

Conclusions

We have shown how a notion of applicative similarity on call-by-name effectful lambda-calculi can be defined and proved fully-abstract. This is very much in line with logical relations as introduced in [ 13 ], but simpler and applicable to untyped -calculi. The underlying transition system has monadic values as states, and is essentially deterministic. This is indeed the reason the framework is only applicable to call-by-name (and not to call-by-value) calculi, in contrast with [ 6 ]. In fact, in the probabilistic call-by-value case our notion of applicative similarity on monadic values is unsound for the contextual preorder, as witnessed by the terms x:(x p ), ( x:x) p ( x: ), and the context ( x:x(x( y:y)))[ ].

References

1. Samson Abramsky . The lazy lambda calculus . In D. Turner, editor, Research Topics in Functional Programming , pages 65 - 117 . Addison Wesley, 1990 .

2. Andrew W. Appel and David A. McAllester . An indexed model of recursive types for foundational proof-carrying code . ACM Trans. Program. Lang. Syst. , 23 ( 5 ): 657 - 683 , 2001 .

3. Nick Benton , Andrew Kennedy, Lennart Beringer, and Martin Hofmann . Relational semantics for effect-based program transformations: higher-order store . In Proc. of PPDP 2009 , pages 301 - 312 , 2009 .

4. Ales Bizjak and Lars Birkedal . Step-indexed logical relations for probability . In Proc. of FOSSACS 2015 , pages 279 - 294 , 2015 .

5. Raphaëlle Crubillé and Ugo Dal Lago. On probabilistic applicative bisimulation and call-by-value -calculi . In Proc. of ESOP 2014 , volume 8410 of LNCS , pages 209 - 228 . Springer, 2014 .

6. Ugo Dal Lago , Francesco Gavazzo, and Paul Levy. Effectful applicative bisimilarity: Monads, relators, and Howe's method (long version) . Available at https://arxiv. org/abs/1704.04647, 2017 .

7. Ugo Dal Lago , Davide Sangiorgi, and Michele Alberti . On coinductive equivalences for higher-order probabilistic functional programs . In Proc. of POPL 2014 , pages 297 - 308 , 2014 .

8. Vincent Danos and Russell Harmer . Probabilistic game semantics . ACM Transactions on Computational Logic , 3 ( 3 ): 359 - 382 , 2002 .

9. Ugo de'Liguoro and Adolfo Piperno . Non deterministic extensions of untyped lambda-calculus . Inf. Comput. , 122 ( 2 ): 149 - 177 , 1995 .

10. Joseph A. Goguen , James W. Thatcher, Eric G. Wagner, and Jesse B. Wright . Initial algebra semantics and continuous algebras . J. ACM , 24 ( 1 ): 68 - 95 , 1977 .

11. Jean Goubault-Larrecq, Slawomir Lasota , and David Nowak. Logical relations for monadic types . Mathematical Structures in Computer Science , 18 ( 6 ): 1169 - 1217 , 2008 .

12. Douglas J. Howe . Proving congruence of bisimulation in functional programming languages . Inf. Comput. , 124 ( 2 ): 103 - 112 , 1996 .

13. Patricia Johann , Alex Simpson, and Janis Voigtländer . A generic operational metatheory for algebraic effects . In Proc. of LICS 2010 , pages 209 - 218 . IEEE Computer Society, 2010 .

14. Søren B. Lassen . Relational Reasoning about Functions and Nondeterminism . PhD thesis , Dept. of Computer Science, University of Aarhus, May 1998 .

15. Saunders MacLane. Categories for the Working Mathematician . Springer-Verlag, 1971 .

16. Eugenio Moggi . Computational lambda-calculus and monads . In Proc. of (LICS 1989 , pages 14 - 23 . IEEE Computer Society, 1989 .

17. A. M. Pitts . Operationally-based theories of program equivalence . In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation, Publications of the Newton Institute , pages 241 - 298 . Cambridge University Press, 1997 .

18. Andrew M. Pitts . Howe's method for higher-order languages . In D. Sangiorgi and J. Rutten, editors, Advanced Topics in Bisimulation and Coinduction , volume 52 of Cambridge Tracts in Theoretical Computer Science, chapter 5 , pages 197 - 232 . Cambridge University Press, November 2011 .

19. Gordon D. Plotkin and John Power. Adequacy for algebraic effects . In Proc. of FOSSACS 2001 , pages 1 - 24 , 2001 .

20. Gordon D. Plotkin and John Power. Algebraic operations and generic effects . Applied Categorical Structures , 11 ( 1 ): 69 - 94 , 2003 .