Note on Algol and Conservatively Extending Functional Programming

Syracuse University
SURFACE

College of Engineering and Computer Science Former Departments, Centers, Institutes and Projects

College of Engineering and Computer Science

1995

Note on Algol and Conservatively Extending Functional Programming

Peter W. O'Hearn Syracuse University

Follow this and additional works at: https://surface.syr.edu/lcsmith_other Part of the Programming Languages and Compilers Commons
Recommended Citation O'Hearn, Peter W., "Note on Algol and Conservatively Extending Functional Programming" (1995). College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects. 32. https://surface.syr.edu/lcsmith_other/32
This Article is brought to you for free and open access by the College of Engineering and Computer Science at SURFACE. It has been accepted for inclusion in College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects by an authorized administrator of SURFACE. For more information, please contact [email protected]

J. Functional Programming 1 (1): ??{???, ?? 1995 c 1995 Cambridge University Press 1
Note on Algol and Conservatively Extending Functional Programming
Peter W. O'Hearny
Syracuse University
Abstract
A simple Idealized Algol is considered, based on Reynolds's \essence of Algol." It is shown that observational equivalence in this language conservatively extends observational equivalence in its assignment-free functional sublanguage.
1 Introduction
In \The essence of Algol," Reynolds (1981) presents a view of Algol as a call-byname language based on the typed -calculus, with \imperative" primitive types. A central feature of the design is the interaction between assignment and procedures.
Side e ects are wholly isolated in a primitive type comm of commands, and do
not occur when computing a value of functional type. That is to say, side e ects in procedures are latent, in the sense that an e ect occurs only by evaluating a
procedure call as a term of type comm. As a result, function types retain a genuine
\functional character." For instance, the full and laws are valid equivalences in Algol-like languages. This functional aspect of Algol has been emphasized strongly by Reynolds (1981; 1988; 1992), and echoed in the works of Tennent (1989; 1991) and Felleisen and Weeks (1993).
The purpose of this short note is to give a technical result further exemplifying this functional character. Speci cally, observational (or contextual) equivalence in a simple Idealized Algol conservatively extends equivalence in a simply-typed assignment-free functional sublanguage. This means that two program fragments that can be interchanged in all assignment-free programs without a ecting observable behaviour can also be safely interchanged in any context in the full imperative language. Thus, not only are , , and so on preserved, but so are all equivalences from the assignment-free fragment of the language.
The proof of conservativity utilizes denotational models. The interesting twist in the proof is the use of a non-standard model for the Algol-like language. We want to work with a model of the full imperative language in which semantic equality conservatively extends equality in a standard domain-theoretic model of functional
y Research supported by NSF grant CCR-92110829.

2

Peter W. O'Hearn

languages. It turns out that standard models of Algol-like languages are not suitable because they contain what Reynolds calls \snapback" operations, which cause backtracking of state changes that require copying of the entire state (cf. (O'Hearn and Tennent, 1995; O'Hearn and Reddy, 1995) for discussion). These operations violate the intuitive property of irreversibility of state changes, and Section 3 shows an example of where snapback invalidates an equivalence true in the assignmentfree sublanguage. Thus, conservativity fails for the standard models. The main step in the proof is the formulation of a non-standard model for which a semantic conservativity result does hold.
The result we seek concerns not only semantic equality, but observational equivalence; that is, equivalence in all program contexts. It can be (and is often) the case that semantic equality and observational equivalence for a model and language do not match. In order to extend our result to observational equivalence we need to work with a fully abstract model of the assignment-free sublanguage, a model in which semantic and observational equivalence do coincide. For this we use Plotkin's (1977) fully abstract model of PPCF, a language with recursion and basic arithmetic constructs, and extended with a (determinate) parallel conditional. The proof does adapt easily to other functional sublanguages, including sequential PCF, simply by working with term models. But since this adaptation should be clear from the form of the proof it seems reasonable, for the sake of simplicity, to show the result utilizing the standard continuous-function model of parallel PCF. A fully abstract model is not required for the full Algol-like language.
I consider the result given here to be part of folklore. Amongst those with a detailed knowledge of \The essence of Algol," the result is I suspect either already known, or would become known soon after the question was considered. But it is a piece of folklore that deserves to be explicitly noted, especially in light of the growing interest in integrating functional and imperative programming, e.g., (Swarup et al. , 1991; Wadler, 1990b; Wadler, 1990a; Peyton-Jones and Wadler, 1993; Guzman and Hudak, 1990; Launchbury and Peyton Jones, 1995). Conservative extension results of the kind considered here have been a speci c concern in (Odersky et al. , 1993; Odersky, 1994; Riecke, 1993; Riecke and Viswanathan, 1995).

2 Idealized Algol
Idealized Algol extends simply-typed functional programming with primitive types for imperative features. We take the language PCF, a typed -calculus with recursion and basic arithmetic constructs, as our representative pure functional language. The language IA (for Idealized Algol) extends PCF with two additional primitive
types, the type comm of commands and the type var of storage variables. Alto-
gether, the types of IA are
t ::= nat j bool j var j comm j t ! t :
For simplicity, we only consider storage variables that hold natural-number values; variables for the booleans could easily be added. Though we will not do so here,
in the presence of product types we could take comm as the only additional type,

Algol and Functional Programming

3

beyond those of PCF, by de ning var as syntactic sugar for (nat ! comm) nat
(Reynolds, 1981). Many of the essential properties of IA can be immediately brought to light by
considering a semantics for the types. In the following, each type t determines an !-complete partial order S t] with a least element.
S comm] = S ) S? S nat] = S ) N? S bool] = S ) T? S S tv0a! r] t] == SS ) t0] L)? S t]

Here, ) is is the continuous function space, T = ftt; g is a two-point set (of truth values), L is a countably in nite set (of locations), N is the set of natural numbers, and S is a suitable set of states.
The striking point to notice is that the interpretation of the function type is exactly as in a domain-theoretic semantics of a purely-functional language. In comparison, in most imperative languages such as Pascal, ML, or Scheme, the collection of states would be used to interpred functions themselves. Furthermore { and this is related to the interpretation of the function type { side-e ects are wholly con-
centrated in the type comm, since no other primitive types have the state in an output position. The nat and bool types are state-dependent, but in a read-only
way. These aspects of the language are an example of what Strachey (1972) termed structural properties, on display from the semantics of types alone, prior to considering primitive operations or terms at all, let alone operational semantics.
IA is an applied -calculus with certain constants. An in nite set of variables xt : t, for each type t, is assumed, together with formation rules for -abstraction and application:

M :s!t N :s MN :t

M :s xt:M : t ! s

The constants come in two groups. One group consists essentially of the operations of PPCF, i.e., PCF together with a parallel conditional.

succ; pred : nat ! nat ifb : bool ! b ! b ! b pif : bool ! ! ! 0 : nat 0? : nat ! bool
tt; : bool Yt : (t ! t) ! t

In the rule for ifb, the sequential conditional, b ranges over all primitive types including var and comm. In the rule for pif , the parallel conditional, ranges over only nat and bool. In the rule for Yt, the recursion combinator, t ranges over
all types of IA.

4

Peter W. O'Hearn

The constants for the imperative fragment of IA are as follows.

:= : var ! nat ! comm deref : var ! nat skip : comm
; : comm ! comm ! comm new : nat ! (var ! comm) ! comm

new v P creates a local storage variable `, initializes its contents to v, executes
P (`), and de-allocates ` on completion. With this explanation the binding of an
identi er denoting a local variable is accomplished using , as in new v ( x:C).
PPCF is a sublanguage of IA. The PPCF types are

::= nat j bool j ! :

PPCF terms are build from variables x , abstraction, application, and the constants
just given (with the restriction that in ifb b is nat or bool). We will denote the
standard continuous-function model of PPCF by P ]. The interpretation of types is as usual:
P nat] = N? P P b0o! ol] ] == TP? 0] ) P ]

A P ]-environment u is a type-respecting map that assigns a value u(x ) 2 P ] to each variable x , and the meaning of a PPCF term is a (continuous) map from environments into values so that P M]u 2 P ] when M : . All of the constants
have their usual interpretations, with pif being the parallel conditional. We often suppress mention of environments when speaking of P c], for c one of the given
constants. We refer to (Plotkin, 1977; Gunter, 1992) for detailed de nitions. Returning to IA, to complete the semantics of types we have to de ne the set S
of states. There are a number of ways to do this, one of the simplest of which is to set
S = L ) (N + funusedg)
The unused portion is used to de ne the local variable declarator new. For this to
work, we must assume that there is a partial function new : S * L that selects a new unused location if there is one, and is unde ned if all locations are in use; see the textbook (Tennent, 1991) for a more detailed discussion.
An S ]-environment u is a function associating an element u(xt) 2 S t] to each variable xt. The following semantic equations de ne a continuous function S M] : E ) S t] for M : t, where E is the (componentwise ordered) domain of

Algol and Functional Programming

5

environments. xt] u = u(xt)

Y ]f = F 2 fi( )

S
S M (N )] u = S M ] u(S N ] u)

0] S t
Ss

=

0i N

?

S xt:M ] u a = S M ] (u j xt 7! a)

S 0?]a s = P 0?](a(s))

S pred] a s = P pred] (a(s))

S tt] s = tt

S succ] a s = P succ] (a(s))

S ]s =

S skip]s = s b(s0) if a(s) = s0 =

S ;] a b s =

?

6?
if a(s) = ?

S deref]a s =

s(`) if a(s) = ` 6= ? ? if a(s) = ?

S :=] a b s

=

s(` 7! v) 8?

if a(s) = ` 6= ?, b(s) = v 6= ? if a(s) = ? or b(s) = ?

< b(s) if a(s) = tt

S ifb] a b c s

=

: c(s)

if a(s) = if a(s) =

8<

?
b(s)

?
if a(s) = tt

S pif ]a b c s

=

: c(s)

if a(s) = or c(s) = b(s) if a(s) =

8<

(?s0

j

`

7!

?
unused)

if new(s) = `; e(s) = v 6= ?;

S new ] e p s = :

p( s:`)(s j ` 7! v) = s0

?

otherwise

With the various constants, we have suppressed mention of environments.

3 Conservativity 3.1 Semantic Conservativity
! The model of IA given in the previous section is standard and, even if it is imperfect,
it is certainly computationally adequate wrt a suitable operational semantics (Meyer and Sieber, 1988). Thus, we may consider the semantics as a reference point, for de ning the language. However, the model S ] is not conservative over P ], as the following example shows.
Consider the type bool bool. S bool ! bool] = (S ) T?) ) (S ) T?)
The two occurrences of the set S of states allow us to (semantically) evaluate di erent parts of an expression at di erent states. An example is the function
g 2 S bool ! bool] de ned by:
g(e)s = e(s j ` 7! 0)
where ` 2 L is a xed location. Intuitively, g executes e after changing the state, by assigning 0 to `, and so there are two states, s and (s j ` 7! 0), that play a role in the evaluation of the semantic expression g(e)s. To see this issue on the level of

6

Peter W. O'Hearn

equivalences, consider the terms

M = if x (f(x))

N = ifx (f(tt))

where f : bool ! bool and x : bool are identi ers, and = Ybool( x : x) is the
divergent boolean. This is a valid equivalence in PPCF, P M] = P N], because in the model f is applied directly to the value of x, which is a truth value. However,
in the S ] model f is applied to an argument of semantic type S ) T?, and so
there is an opportunity to apply f in states where x is false. Speci cally, de ne
e 2 S bool] by

e(s) =

tt

if s(`) = 0, otherwise

Now, let s be a state where s(`) 6= 0. Then g(e)s = while g( s0:tt)s = tt.
Therefore, if we consider an environment u where u(f) = g and u(x) = e, we get S M]us = while S N]us = tt. So M and N are not equal in the model S ], and semantic equality in the standard model S ] of IA is not conservative over equality in the model P ] of PPCF.

The function g is an example of the \snapback" e ect, so named because the state change is not recorded globally in the semantics. For instance, in an environment where f denotes function g, an assignment statement x := f(1) will leave location ` unchanged (unless x denotes `) because the change to ` during evaluation of f(1) is temporary.

We now present a semantic model that overcomes this speci c di culty pertaining to conservativity. The model does not address the general problem of irreversibility of state change; see (O'Hearn and Tennent, 1995; Reddy, 1995; O'Hearn and Reddy, 1995) for discussion of this. The aim is to provide a simple (though ad hoc) work-around, that is just enough to achieve conservativity.

The main idea of the new semantics C ] is to push the state as far outward as possible, by interpreting the PPCF fragment in a way that, given any state s, \compiles" to a meaning in the PPCF model P ] by reading values of variables. In intuitive terms, we will maintain the following property for the PPCF fragment:

C M]us = P M]u0 where u0(x) is obtained by \looking up" u(x) in state s

Here is the semantics of types.

C]

= S)P ]

C comm] = S comm]

CC vt0a! r] t] == S C tv0a] r) ] C t]

for PPCF types
provided one of t0; t not a PPCF type.

For PPCF types there is now only one occurrence of S, at the outermost level. For
example, C bool ! bool] = S ) (T? ) T?).

Algol and Functional Programming

7

The semantic equations for the PPCF constants must be altered in certain cases.

C M (N )] us = C M ] us(C N ] us) C xt:M ] u s a = C M ] (u j xt 7! ( s 2 S : a))
C succ] s = P succ] C pred] s = P pred]
C if ]s = P if ] C pif] s = P pif] C Y ]s = P Y ]

M; N of PPCF type x:M of PPCF type

For the remaining constants and cases the equations are exactly as for S ]. The non-standard semantics of the PPCF fragment of IA can be easily seen to
satisfy the laws of the typed -calculus. In fact, it is just an interpretation of the typed -calculus in the Kleisli category of a monad on the category of !-complete posets and continuous functions. The functor part of this monad is S ) ({), and the resultant Kleisli category is cartesian closed.

Lemma 1 (Semantic Conservativity)

For all PPCF terms M; N, P M] = P N] i C M] = C N].

Proof
CFoMr a]nuys P=PCPFMte]rum0, Mwhearnedu0Cis]a-ePnvi]r-oennmviernotnmu,enatrsouucthintehaitnduu0(cxt)io=n ush(xow)ss. Athsaat
consequence, for any closed PPCF term M, we clearly have C M] = s 2 S:P M], and so the result holds for closed terms. For open terms M and N the result follows by considering closures ~x:M and ~x:N, which are equal i M and N are (by virtue of -calculus laws).

The reader may enjoy verifying that the terms M and N from the example at the beginning of this section are indeed equivalent in C ].

3.2 Observational Conservativity
Observational equivalence will be generated by observing convergence at ground
type. In the case of IA, this means a closed term of type comm or var, as well as terms of type nat or bool. De nition 2 (Observational Equivalence)
1. For PPCF terms M; N, M PPCF N i for all ground PPCF contexts C ], P C M ]] = ? () P C N ]] = ?
2. For IA terms M; N, M IA N i for all ground IA contexts C ], S C M ]] = ? () S C N ]] = ?
There are typical implicit provisos in this de nition, such as that M and N be of the same type and that C ] be a context that captures all their free identi ers.
As we indicated before, we take the standard model S ] as de ning IA. The model C ], though non-standard, is adequate wrt this model.

8

Peter W. O'Hearn

Lemma 3 (Adequacy)

For all closed IA terms M of ground type, S M] = ? i C M] = ?.

Proof The proof uses a standard \logical-relation argument" (Tennent, 1991; Gunter, 1992) to connect the meanings in the two models. Given (complete and pointed) relations Rb C b] S b] on IA primitive types, we lift to higher types by the clauses:
(p; p0) 2 R ! 0 () 8(a; a0) 2 R :(( s : (ps)(as)); p0(a0)) 2 R 0 (p; p0) 2 ! Rt t0 () 8(a; a0) 2 Rt :(p(a); p0(a0)) 2 Rt0 where one of t; t0 is not a PPCF type. Then taking Rb as the equality relation, this
generates a family of relations. One checks that each constant of IA is invariant under the resulting relation, using the fact that each Rt is pointed and closed under lubs of !-chains in the case of xed-point. One then shows that the meanings of all terms map related environments to related meanings in the usual way, and adequacy follows.

This, together with lemma 1, yields the result.

Proposition 4 (Observational Conservativity)

For all PPCF terms M; N,

M PPCF N () M IA N

Proof If a PPCF context C ] distinguishes M and N in P ], say P C M]] 6= ? and P C N]] = ?, then by the semantic conservativity lemma we have C C M]] 6= ? and C C N]] = ?. The ( direction then follows from the adequacy lemma.
Conversely, if M PPCF N then P M] = P N] by the full abstraction theorem for P ]. By the semantic conservativity lemma we get C M] = C N], and then M IA N follows from the adequacy lemma and the compositionality of C ].

The interesting part of this argument is the use of the non-standard model of IA. It shows that the presence of snapback operations is the only reason for the failure of conservativity in standard models of Algol. The result also illustrates, by way of equivalences, some of the undesirable properties of snapback operations, and thus weaknesses in the models of, e.g., (Oles, 1982; O'Hearn and Tennent, 1995; Sieber, 1994). Among the more advanced models of Algol-like languages, Tennent's (1990) model of speci cation logic is the only one in which a semantic conservativity result holds.

4 Conclusion
Reynolds's Algol, unlike Algol 60, disallows side e ects in integer and boolean expressions. This leads to a clear distinction between the types of phrases (integers, booleans) that are evaluated for the value they produce, and commands, which are evaluated soley for their side e ects. Analogous conservation results typically fail for languages where there is a less strict separation. For instance, in ML or Scheme

Algol and Functional Programming

9

! procedure invocation is inextricably bound up with state change, and equivalences
such as f(1)+f(2) f(2)+f(1) that (viewed at an appropriate level of abstraction) hold in the e ect-free subset { what is often referred to as the \pure" subset { do not hold in contexts where f can have a side e ect. In versions of Algol that allow side e ects in expressions, such as (Weeks and Felleissen, 1993), conservativity is also lost, though the laws of the typed -calculus remain valid.
Some recent proposals for integrating imperative and functional programming also use types to isolate e ects from the procedure mechanism (Peyton-Jones and Wadler, 1993; Launchbury and Peyton Jones, 1995). A type T (a) is used for state
transformers that change the state and also return a value of type a: the type comm
in IA resembles T (unit) for a type unit with a trivial value. In these languages integer and boolean expressions are completely state-independent, whereas in IA expressions are read-only or passive, in that they are state-dependent but sidee ect free. The imperative -calculus (Swarup et al. , 1991) is even closer to IA, but also uses state-independent expressions. In order to maintain equational laws in a setting that does not allow for passive or read-only types excessive sequencing of dereferencing operations is required. This is one of the motivations for considering general notions of passivity (Reynolds, 1978; Wadler, 1990b; Reddy, 1994; O'Hearn et al. , 1995).
Although every speci c equation true in the functional sublanguage remains true in IA, it is important to note that not all \global properties" of equivalence are preserved. One example is the context lemma (Milner, 1977): two closed terms M; N of functional type in PPCF are equivalent i MV~ NV~ for all closed vectors V~
of arguments. This property fails in IA already at the type comm comm. For
instance, the procedures c : c and c : c; c are not observationally equivalent, but closed applicative contexts are not su cient to distinguish them: up to equivalence,
skip and are the only closed terms of type comm in IA. To create a distinguishing context we must use new, as in
new 0 ( x : ( ](x := x + 1)); if x = 1 then skip else )
This failure of the context lemma can perhaps be attributed to the presence of impure features in IA, though it is di cult to make this attribution precise since \impure" is ill-de ned.

References
Gunter, C. A. 1992. Semantics of Programming Languages: Structures and Techniques. MIT Press.
Guzman, J., and Hudak, P. 1990. Single-threaded polymorphic lambda calculus. Pages 333{345 of: Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science. Philadelphia, PA: IEEE Computer Society Press, Los Alamitos, California.
Launchbury, J., and Peyton Jones, S. 1995. State in Haskell. Lisp and Symbolic Computation. Special issue on State in Programming Languages. To appear.
Meyer, A. R., and Sieber, K. 1988. Towards fully abstract semantics for local variables: preliminary report. Pages 191{203 of: Conf. Record 15th ACM Symp. on Principles of Programming Languages. ACM, New York.