This book made available by the Internet Archive.

ABSTRACT

We present a simple correspondence between a large subset of ALGOL 60 language and lambda-calculus. With the aid of this correspondence, a program can be translated into a single lambda-expression. In general, the representation of a program is specified by means of a system of simultaneous conversion relations among the representations of the program constituents. High-level programming language features are treated directly, not in terms of the representations of machine-level operations. The model includes input-output in such a way that when the representation of a (convergent) program is applied to the input item representations, the resulting combination reduces to a tuple of the representations of the output items. This model does not introduce any imperative notions into the calculus; the descriptive programming constructs, such as expressions, and the imperative ones, such as assignments and jumps, are translated alike into pure lambda-expressions. The applicability of the model to the problems of proving program equivalence and correctness is illustrated by means of simple examples.

-Ill-

If one wishes to study properties of programs, then one should either develop rules of deduction and inference that apply directly to programming language constructs (e.g., Hoare [1]), or represent programs by the objects of some mathematical system [e.g., 2,3,7-10] and work with these representations. As a step in the second direction, this paper describes a way of representing programs by lambda-expressions [4-6].

Since a number of lambda-calculus (or, related, combinatory logic) models of programming languages have already appeared in the literature [among them, 7-10], the proposal of yet another such model may require justification. So we will first indicate some distinguishing features of our model vis-a-vis others.

1. Our model does not introduce any imperative or otherwise foreign notions to lambda-calculus. This is in contrast to Landin [7], in which imperative features of programming languages are accounted for by ad hoc extensions of the calculus. We find that the calculus, in its purity, suffices as a model of programming languages. By not making any additions to the lambda-calculus, we have the guarantee that all its properties, in particular,the consistency and the Church-Rosser property [6], are valid in our model. For example, even when a program requires a fixed order

of execution, the lambda-expression obtained by evaluating the program representation in any order, whatsoever, represents the program result correctly.

2. Programs are translated into lambda-expressions, not interpreted by a lambda-calculus interpreter (Reynolds [10]). Thus, programming semantics is completely reduced to lambda-calculus semantics, but without commitment to any particular view of the latter. Also, all lambda-expression transformations are applicable to programs.

3. Assignments are modelled by the substitution operation of lambda-calculus. Consequently, the notions of memory, addresses, and fetch and store operations do not enter our model in an explicit manner (Stratchey [8], Reynolds [10]).

-1-

4. High-level programming language constructs are represented by lambda-expressions directly, not in terms of the representations of the machine-level operations (Orgass-Fitch 19]) of the compiled code.

5. This model spans the full ALGOL 60 language. It is also applicable to a number of other advanced programming features, such as collateral (parallel) statements, the use of labels and procedures as assignable values, coroutines, etc.

6. As a matter of opinion, it seems that our representations are much simpler and clearer than the ones given in other models. Also they seem to have obvious intuitive justifications.

The model will be described informally, and only for a representative set of programming language constructs. But enough motivating details and illustrations will be provided to, hopefully, convey the method, and suggest its extension to other programming features. A more complete treatment can be found in [11].

-2-

2.1 Preliminaries

To fix our terminology and notation for lambda-calculus (LC), we include the following definitions.

We assiime given a set of entities, called variables . A lambda-expression (LE) is either a variable, or the application (e-je-) of an LE e, to an LE e^ , or the abstraction (Xx:e) of an LE e with respect to a variable x. In writing LE's, parentheses may be omitted under the convention that applications associate to the left and abstractions to the right, with the former taking precedence over the latter. For instance,

(Ax: (Ay: (Az:(((x z) (y z))u))))

may be abbreviated to

Ax: Ay: Az: xz(yz)u .

As an additional convention, the above may be further abbreviated to

Axyz : xz(yz)u

Identity of LE's is indicated by the symbol '=', which is also used as a definition symbol.

In the LE (Ax:e), the first occurrence of x is a binding occurrence, and e is the range of that occurrence. An occurrence of a variable in an LE is bound if it is either binding or in the range of any binding occurrence of the same variable; otherwise, the occurrence is free . If e,f, ,...,f are LE's and x^,...,x variables, then

sub [ f ^ , x^; . . . ; f^ , Xj^; e ]

denotes the result of simultaneously substituting f. for all free

occurrences of x. (1 _< i £ n) in e.

The basic LC rules of transformation, called contractions , are these:

T

-3-

(a) Xx:e -* Ay: sub[y,x;e],

if y has no free occurrences in e, and no free occurrences of x become bound occurrences of y by the substitution.

(3) (Xx:e)f -^n sublf,x;e],

if no variable with free occurrences in f has bound occurrences in e. , ,

(n) Xx: ex ^ e,

if X has no free occurrences in e.

The converse of 3- (or n-) contraction is called 3- or nexpansion . Contractions and expansions may be applied to the whole or a part (which must itself be an LE) of an LE. Reduction (->) consists of a (possibly empty) sequence of contractions. As an example of reduction, it can be shown that

(Ax, x„ : e) f, f„ -> sub [f, ,x, ; . . . ; f^ ,x ;e] ,

1 n 1 n ii nn

provided that no variable with free occurrences in f's has bound

occurrences in e. Conversion ( = ) consists of a (possibly empty)

sequence of contractions and expansions. If it is the case that

e = f, then there exists an LE g such that e ^- g and f -^ g

(Church-Rosser Theorem [6]). An LE is irreducible if no 3- or

n-contraction is applicable to it, even after any intermediate

a-contractions. A normal form of an LE e is an irreducible LE g,

if one exists, such that e = f. If e possesses a normal form f,

then f is unique up to the applications of a-contractions, and,

moreover, e -> f; f can be obtained from e by using, among other

possibilities, the standard-order reduction algorithm , in which

one always chooses the leftmost 3- or n-contraction at each step

in reduction. '

A natural interpretation of LE's is as functions: the LE (f e)

may be regarded as the functional expression f(e), and (Ax:e) as

the function f defined by f(x) = e in the customary functional

notation. With this interpretation, the LE (e^e-e^-.-e ) may be

-4-

viewed variously as e, (e„ ,. . . ,e ) , or [e, (e„) ] (e-,,. . . ,e ) ,

± z. n i. ^ J n

where e,(e^) is understood to yield a function as its value, etc. The functional interpretation of LE's is the intuitive basis of our model.

Following are some definitions and abbreviations that will be used later:

<a, ,...,a > = Ax: xa,... a , n > 0 In 1 n —

I = Ax:x

Q E (Axy:xx)(Axy:xx)

Y = Ax: (Ay: x(yy)) (Ay: x(yy))

a ,b = Ax: axb

elem. s Ax, ...x : x. , 1 < i < n

1, n 1 n 1 ' — —

replace . = Ayx,... x : <x-,...,x._,,y,x. ,,...,x >, l<i<n.

Detailed information about LC may be found in [4-6].

We use the ALGOL 60 notation [12], whenever possible, to express programming language constructs. By the environment of a point in a program, we mean a list of all the variables whose scopes include that point; in this list, the variables are arranged in their order of declaration within individual blocks, with the blocks taken in the innermost to outermost order. In general, the LC representation of a construct may depend on its own environment (i.e., of the point at which it occurs), as well as the environments of its components. We denote the LC representation of a construct X appearing in the environment E by {x}„ , or simply {x}, when the environment is understood, or is irrelevant to the representation, such as when X is a constant.

-5-

Before we can choose the LC representations of various programming language constructs, we must decide exactly how we are to represent complete programs. We will take the view that it is the external input-output behavior that most appropriately characterizes a program. Consider, for example, the program

begin integer a,b,c;

read a; read c; b := a+c; write b; b := b-2xc; write b end

in which read and write are assumed to be the standard statements for performing input-output operations. As far as only the external input-output is concerned, the above program behaves as a two-argument function which produces as value two quantities, the sum and the difference of the argiiments; in LC notation, this function can be expressed by

Axy: <x+y, x-y> . (1)

(Note that x+y and x-y are not strictly LE's, but they can be easily translated to be such.) Accordingly, we would like to set up the model in such a manner that the representation of the above program may turn out to be the LE (1), or, as seems more likely, an LE which can be reduced to (1). So constructed, the model would enable us, in essence, to abstract out of a program code the function from the input space to the output space that the program computes .

More generally, if P is a program, i ,...,i its inputs, and o,,...,o its outputs, then our representations are intended to satisfy the reduction relation

{P}{i,}... {i„} ^ <{o,},...,{o^}> . (la)

1 p 1 q

While the main goal of the present model is to obtain purely

functional descriptions of programs, it will become evident

later that the representations in this model are also capable

of simulating the execution-time behavior of programs. Specifically,

-6-

when a slightly modified version of the standard-order reduction algorithm is employed to carry out (la), it, in effect, furnishes the step-by-step trace of executing the program P with the input data items i, ,... ,i .

2.3 Variables

Program variables are represented by LC variables, possibly with the same symbolic denotation. However, all program variables with non-disjoint scopes must have mutually distinct representations; thus, if the same identifier is used for two such variables, the corresponding LC representations must be distinguished from each other, say, by superscripting the identifier with the respective block level numbers.

A single LC variable is used to represent an array also; however, the treatment of arrays is deferred to a later section, and until that discussion we assume all variables to be simple.

2.4 Constants, Operations, Relations

We do not concern ourselves here with the purely arithmetical aspects of programming language; so we take for granted the LC representations of numbers, logical values, arithmetic and logical operations, and relations. (The representation method may be found in [4,11].) We assume that these representations satisfy the reduction relations of the form

{*} {a} -^ {* a} ,

{o} {a} {b} ^ {a o b} ,

where * and o are unary and binary operators, respectively, and a and b are the quantities of proper types. (Note: {x} denotes the LC representation of X, ref. end of Sec. 2.1.) The representations of logical values are assumed to satisfy

{true} {a} {b} ^ {a} { false } {a} {b} ^ {b} for all a and b.

-7-

Let us limit ourselves for the present to the expressions that do not contain function designators. (This restriction will be lifted later when we discuss procedures.) In view of the previous section, the representation of such expressions is essentially a matter of rearranging the individual operator and operand representations into a parenthesized prefix form. For example,

a + if b 7^ 0 then c/b else 15 (2)

is represented by

{+}{a}{{7^}{b}{0}({/}{c}{b}){l5}) . (3)

For convenience in reading, we utilize Landin's idea of "syntactic sugaring" [7]: we designate (3) by simply underlining (2)

2.6 Assignments

Before discussing any particular type of statements, we will

first indicate the general idea behind our LC representations.

Consider a given statement S of a program. Let (v,,...,v ) be

'■ In

the environment of S, and denote by F the section of the program following S and extending all the way to the program end. (F will be referred to as the program remainder of S.) The two parts of the program, one consisting of F alone, and the other composed of S and F together, may be interpreted as two functions 4) and 4)', respectively, of the arguments v, ,...,v . With this interpretation in mind, the effect of the statement S is to transform (J) into (j)' . As the representation of S, therefore, we take precisely the function (to be accurate, the fionctional operator) a given by

[CF (cf)) ] (v^, . . . ,v^) = (})' (v^,. . . ,v^) ,

which accomplishes the above transformation.

A key step in representing a programming operations is to find a suitable (f)' for it, based on the intuitive understanding of the effect of the operation. Purely for the sake of motivation, we will include details of this step in describing the first few of our representations.

-8-

environment (v, ,...,v ). The (j)' in this case differs from cj)

in having the argument v. set to e. Thus, in effect, the above statement behaves as the function 0 such that

[0(4)) ] (v-j^,. . . ,v^) = (J)' (v^,. . . ,v^) = 4) (Vj^,. . . ,v^_^,e,v^_^^ ,. .. ,v^)

Accordingly, we adopt the following LC representation of assignment statements.

{v. := e}, > = A(j>v- ...v : (^v^ ...v. nlelv.,, ... v . (4)

1 (v, ,...,v ) ^1 n ^ 1 1-1 1+1 n 1 n

(An assumption londerlying (4) is that any needed type-conversion

has been incorporated within e itself.)

If the expression e contains only the variables v, ,...,v

for some m < n, then the variables v ,,,...,v can be dropped

m+i n

from the above LE (by n-contraction), reducing it to

A(t)v, ...V : (j)V, . . . V. ,{e}v.,,... v^ . ^1 m ^ 1 1-1 1+1 m

Note that the multiple assignment of ALGOL 60 and the collateral (parallel) assignment of ALGOL 68 pose no special problem. As an illustration of the latter, the statement (x := y, z:=x) occurring in the environment (x,y,z) has the LC translation A(J)xyz : (f)yyx.

From (4) it is clearly seen that the LE representing an assignment statement does not contain any free variables, as V,,...,v are the only variables that can legitimately occur in e. This property of containing no free variables will be seen to be enjoyed by the LC representation of all types of statements, and will be used to simplify the representations.

-9-

Consider the compound statement S = begin S,;S„ end appearing in the environment (v,,...,v ). Let F be the segment of the program that follows S. The execution of S;F has precisely the same effect as that of S,;S„;F. We can imagine the program sections F, (S-^'F), and (S, ;S ;F) to be some functions (t>, <p" , and (})' , respectively, of the arguments v, ,...,v , and S, S, , S- to be the functional operators a, a,, a- such that

l02i<t> ) ] (Vj^, . . . ,v^) = (})" (v^,. . . ,v^) ,

[a^ (())")] (Vj^,. .. ,v^) = (|)' (Vj^,. . . ,v^) ,

[a (4) ) ] (v^,. . . ,v^) = (j)' (v^,. . . ,v^) .

In LC notation,

(j)" = Av, ...v : a-tf) V, . . . V -* 02<t> I

as the statement representations O2 and (|) do not contain free variables; hence,

a = Actv, . . . V : (i)'v, ... V = Ad)V, . . . v : a, d)"v, . . . v ^1 n^l n ^1 nl^l n

-> A(j)V, . . . V : a, (a_(j))v, ...v -> \^: o ^ {a 2<^) .

The generalization to an n-component compound is obvious. So we are led to the following LC representation of compound statements.

( begin S^;S2;•••;S^ end} e \^: [S^] {{S^] {... {{S^]^) ...))

Notice the convenient fact that the individual statement representations in (5) appear from left to right in the same order in which the statements occur in the compound (Cf. Stratchey [8]).

(5)

-10-

Example : Rules (4) and (5) are illustrated by the following statements and their LC representations. The environment is assumed to be (x,y).

(a)

(b)

Statements

begin

X := 2;

y : = x+ 3 ;

X := y+x end

begin

y := 5:

X := y+2 end

LC Representations

A(})xy: (p2_ Y ^ A, say Acj)xy: (^x x+3 = B A4)xy: 4) x+y y = C X(^: A(B(C <j)) ) = D

X(})xy: (t)X 5^ = E Acf)xy: (}> y+2 y = F Acj): E(F 4)) E G

It can be verified that the LC representations of the equivalent program segments (a) and (b), namely, D and G, are indeed mutually convertible LE' s; specifically, D ->■ A(|)xy: 4) ]_ 5 -^ G. The normal form A(J)xy: (}) 2 ^^ of these representations corresponds to the collateral assignment statement (x := 7, y := 5), which may be thought of as the simplest version of the above code.

2.8. Blocks .

Next, let us consider a block S whose head declares the variables u, ,...,u , and initializes these to the values c, ,...,c

m'

and whose body consists of the statements S, ,...,S , in that

1 p

order. The execution of S can be broken down into three operations performed in succession.

1)

2)

Extension of the existing environment by the variables

u

1'

,u (initialized at c,,.

m

Execution of the compound begin S^ ;... ;S end

3) Deletion of the variables u,,...,u from the environment.

1 m

-11-

Let these three operations be denoted by the functions a, 3, and Y« Let (v, ,...,v ) be the environment of S. Then with the obvious significance of other symbols, we have

[a (4)) ] (v^ ,. . . ,v^) = 4) (c^ ,. . . ,c^f v^,...,v^)

[B ((}))] (Uj^,... ,Uj^,v^ ,... ,v^)

[a, (a„ (... (a ((})))...))] (u, ,... ,u^,v^ ,... ,v ) i ^ 9 1 m i n

[Y (*) ] (Uj^, . . . ,Uj^,Vj^, . . . ,V^) = (}) (v^,. . . ,v^)

[a((^)] (Vj_,... ,v^) = [a(6(Y('l')))] (Vj_,... ,v^) .

By expressing the above in LC notation, and making use of proper substitutions and simplifications, we obtain -1"

a = Ad)v,...v : a,(a^{...(a (Au, . . . \r : *))...)) c, .. . c v^ . . . v ^1 n 12 pi in ^'' 1 ml n

Consequently, we choose the following representation of blocks:

{begin <type>u- :=c, ;...;<type>u :=c ;S,;S_;... ;S end}, ^

— ^ — ^^ 1 1 '-uf jn ml2 p (v, ,. . . ,v )

in

= A())V^...v^: {Sj^}p({S2}p(. .. ({S }p(AUj^. . .Uj^rcf))) . ..))

^^l^E ---^^m^E ^1 ••• ^n '

where E = (v, ,...,v ) and F = (u, ,...,u ,v,,...,v ). In 1 m 1 n

(6)

In (6), we assume that the expressions c. include any

required type-conversion operations. In the case that the

variables are left uninitialized in the block-head, any arbitrary

LE can be used in place of c.. One might wish to use for this

purpose an LE which would play the role of the everywhere undefined

function. This function is modelled, for example, by the LE

-12-

Q. = (Axy:xx) (Axy:xx) , which has the property fix ->■ fi for all x. It should be noted, however, that Q. does not possess a normal form (as can be easily verified). As a result, if fi is used in place of the missing c.'s in (6), then the presence of any variables that remain undefined throughout the program execution would cause the program representation to behave as if the program contained an infinite loop.

If the variables declared in a block-head are not initialized, then V. (1 _< i _< n) have no free occurrences in the expression at the right-hand of (6), and we have the simpler representation

{ begin <type>u,;...;<type>u ;S ;S^ ; . . . ;S end } , >

In

5 Xcf): {S, }„({S„}„(. . . ({S^}„(AUt . . u^:4)))... )) fi fi ...Q,

Xr^r pro. m 1^ j

m times where F = (u^^,. . . ,u^,v^ ,. . . ,v^) . (7)

2.9 Input-Output

We shall assume for simplicity that the program input and output operations are each restricted to a single file. A file of items a,,...,a will be represented by the tuple

<{a,},...,{a }>, i.e., Xx: x{a, } ... {a } .

(The empty file is represented by the null tuple < > e Ax: x = I.)

For given LE's u, v, and w, we will abbreviate the LE

Ax: uxv by u,v and the LE u,v ,w by u,v,w . It can be easily verified that

<x,,...,x >,y ^ <x,,...,x ,y> 1 n -^ 1 n -^

1 n 1 n

so that "," may be regarded as the operation of writing on a file, and the file resulting from writing an item a on a given file b may be represented by {b},{a} .

-13-

Now let S be a statement appearing in the environment V,,...,v of a program, and let a be the LC representation of S. In' our disucssion so far, a has been an LE of the form

X(bv, ... V : ... , (*)

^ 1 n ' * '

with the argiament 4) standing for the program remainder of S. Accordingly, the execution of S has been modelled by the reduction of the LE

o (b V, ... V , — -1 -n

in which the underlined symbols denote the values of the corresponding arguments immediately prior to the execution of S. In order to take input-output into account, we will generalize the representations so as to model the above execution by the reduction of the LE

a (j) V, ... V {w}{u, }{u~} . . . {u } , (8)

_ _i. _2. 1 ^ m

with w denoting the output file and u. the i-th of the m items remaining on the input file at the moment of execution. (As soon as an item is read, it is supposed to disappear from the input file.) This arrangement requires that the representations of statements be generally of the form

AAv, . . .V o i, . . .i : . . . ,

^ 1 n 1 m

where o, i,,...,i are the extra variables denoting the output 1 m

file and input items. It must be evident, however, that the representations of those statements which do not involve input-output can be simplified back to the form (*) by the use of n-contractions. Furthermore, in the case of input-output statements, the following choice of LC representations is obvious.

{read v.}(^_^^_^^^^) = A(},v^ . . . v^oi :*v^. . . v ._^i v.^3^...v^o (9)

{write e}, i = A({)V,...v o: (()V,...v o,{e} , (10) (V, ,...,V ) J. n X n

where e is some expression to be output.

-14-

2.10 Programs

Let the input file initially presented to a given program

consist of items i,,..•,i , and let o,,...,o constitute

1 p 1 q

the items of the final output file produced by the program. As remarked in Sec. 2.2, we wish to choose a program representation so as to obtain the relation

{program}{i,}...{i } ^ <{o,},...,{o }> . (11)

1 p i q

Now the execution of a particular statement of the program is simulated by an LE given by (8) in the previous section. Suppose that as an instance of such a statement we take the entire outermost block of the program. Recalling the significance of symbols used in connection with (8), we obtain the following conditions:

a = {program block},

n = 0 as the environment is null,

{w} =1, as the output file may be considered empty at the start of the program,

m = p, and u.=i. , l<j<p.

Furthermore, in place of ^ , the "null" program remainder, we may arbitrarily choose to employ the LE 1 = X(^: ^ . On substituting these values, the execution of the program is seen to amount to the reduction of the LE

{program block} I I {i,} ... {i } . (12)

^ ^ i p

Next, consider (8) again — but this time for the case when the entire program has been executed. Now we have:

0=1, the null program segment,

n = 0, as the environment is null,

{w} = <{o-| },..., {o }> , representing the final output file,

m = 0, assuming the program exhausts the input file,

()) = I .

-15-

Thus, (8) in this case becomes the LE

which reduces to

I I <{o, } ,...,{o }>

<{o,},...,{o }> . (13)

If our representations work properly, then the LE (12) should reduce to the LE (13). Comparing this reduction relation with (11), we obtain

{program} = {program block} I I . (14)

Example . To illustrate the parts of the model introduced so far, we will describe in some detail the representation of the simple program mentioned at the beginning of Section 2.2. The components of the program and their representations are shown side by side below.

Statements Representations

begin integer a,b,c;

read a; A(J)abcoi: (})ibco = A , say

read c ; Xcjjabcoi :(j)abio ^ B,

b := a+c; A())abc:(t)a a+c c = C ,

write b; A(t)abco: (Jjabc o,b = D ,

b := b-2xc; A4)abc:())a b-2xc c = E ,

write b X^ahco:(\)ahc o,b = F ,

end X<i): A(B (C (D (E (F (Aabc :<{))))))) S^i^f2 e g .

Since G represents the program block, the representation of the whole program is Gil. It can be easily verified that

G I I ->■ Axy ;< x+y , x-y > .

Thus Gil indeed abstracts out the input-output behavior of the program. (Cf. the discussion in Sec. 2.2.) The execution trace of the above program, when run with the data items 5 and 3, is reflected in the following LC reduction sequence.

-16-

Gil 5 3^ A(B(C(D(E (F(Aabc: I))))))n$^ni 5 3 -> B(C(D(E(F(Aabc: I))))) 5 fi f^ I 3 ^ C(D(E(F(Aabc: I)))) 5 f2 3 I

^ D(E(F(Aabc: I))) 5 5+3 3 1-^ D (E (F ( Xabc : I) ) ) 5 8 3 1 ^ E(F(Aabc:I)) 5 8 3 lj_8 -> E(F(Aabc:I)) 5 8 3 <8> ^ F(Aabc:I) 5 8-2x3 3 <8> ^ F(Aabc:I) 5 2 3 <8> ^ (Aabc:I) 5 2 3 <8> ,2 -^ (Aabc:I) 5 2 3 <8,2> ^ I<8,2> ->■ <8,2> ~

2.11 Conditional Statements

Recall that the LC representation of a boolean expression b has the property that for all LE's p and q, we have

{b} p q ->■ p , if b has the value true , -^ q , if b has the value false .

In view of the above property, we choose the representation of a two-branch conditional statement as follows:

{if b then S, else S^}, v

— 1 2 (v^,...,v^)

= A

c})v,...v : {b} ({S, }(J)Vt . . .V ) ( {S„ }4)V, . . . v ) (15)

1 n 11 n 21 n

For the purpose of representation, a one-branch conditional statment (an if-statement, in ALGOL 60 terminology) may be viewed as a two-branch conditional with a dummy or "do-nothing" statement for the second branch. When appearing in the environment (Vi,...,v ), the "do-nothing" statement can obviously be represented by the LE

Acbv, ... V : (bv-, . . . v , ^1 n ^ 1 n

which reduces to I. On substituting this LE for (S^) in (5),

we obtain

{if b then S,} , >

— 1 {v^,. . . ,v^)

= A(t)V, ...v„: {b} ({S, }ct)V, . . .v^) ((j)V, . . . v„) . (16)

1 n 11 ni n

-17-

It must be evident that if b is a boolean expression , then for for all LE's p, q, and r, the following conversion relation holds:

{b}(pr) (qr) = {b} p q r .

The repeated application of this relation allows us to rewrite (15) in the alternative form

{if b then S^ else S2} (^ ,. . . ,v ) ^ ^"^^1 " * ^n' ^^^S^} {S2 }(t)V^. . . v^

(17)

(Notice that although the LE's {S,} and {S-l do not contain

free occurrences of v,,...,v , the LE {b} may very well contain

these; therefore, these variables cannot be dropped from (17).)

On taking S^ to be the dummy statement in (17), hence i^2^ ^° ^®

I, we get the following alternative to (16):

{if b then S, } ,„ „x =X(})V .--v: {b} {S^ }!(}) v . . . v (18)

Example . Suppose that the statement ^

if a < b then a := a+1 else b := a+b

appears in the context (a,b,c) in a program. The formulas (15) and (17) respectively yield the LE's (A) and (B) as the representations of the above statement.

(A) X(f)abc: a<b ((Acjiabc: ({) a+1 be) (})abc) ((X(j)abc: ipa a+b c) (jiabc) -»■ A())abc: a<b ((}) a+1 be) i<i> a a+b c)

= A(J)abc: a<b ((}) a+1 b) {<t>a a+b) c -^ A(tiab: a<b (cj) a+1 b) {^a a+b)

(B) Acfiabc: a<b (A(|)abc: <t> a+1 be) (A(|)abc: <^a a+b c) ^lahc -> A(t)ab : a<b (A(J)ab: <t> a+1 b) (A({)ab: ({)a a+b ) 4)ab

-18-

2.12 Arrays

Arrays can be interpreted as tuples and hierarchies of tuples, as follows: An array of a single dimension is represented by a tuple of the representations of the individual array elements, taken in the order of the lowest to the highest subscript. An array of dimension n+1 is represented by a tuple whose elements are the representations of the n-dimensional subarrays (or slices , in the ALGOL 68 terminology [13]) obtained by fixing the first subscript in turn from the lowest to the highest possible value. For example, the array A[l:2, 1:3] is represented by

<*^^j^l'^12'^13^ ' <^21'-22'-23^^

where A.. is the representation of the array element A[i,j].

As in the case of simple variables, an array identifier can itself be used as the LC variable to denote the array.

With the above interpretation of arrays, we next describe the

representation of subscripted variables in expressions, assignments to subscripted variables, and array declarations. In this

description, we assume, for simplicity, that all arrays have the lowest subscript bound of 1.

Subscripted variable as an operand in an expression . The representation in this case is just the corresponding element of the tuple representing the array. Thus, we need some operator to extract an element of a tuple, given the element position. For given integers i and m such that 1 < i < m, define the LE

and note that

elem. = Ax, ... x : x. ,

1, m 1 m 1 '

<a, , . . . ,a > elem. -> a. 1 m 1, m 1

Thus, given the declaration array v[l:m], we have

{v[i] } = V elem.

1 ,m

-19-

This representation is inadequate, since, in general, i and m

are given as expressions rather than constants, and their values

may not be known at the time of LC translation of the program.

However, it can be shown [11] that there is an LE elem such that

for all LE's a and b, if a -> i and b ->■ m for integers 1 <_ i £ m,

then

elem a b -»■ elem. 1 ,m

Hence, given the array declaration v[l:e], we define

{v[f] } = v(elem {f}{e}) . .,

More generally, for array v [1 :e, ,...,1:e ] ,

{v[f^,...,f^]} = v(elem {f^}{e^}) ... ( elem ^f^^^^n^^ *

Assignments to subscripted variables . The representation consists in replacing the designated element of the tuple representing the array with the representation of the new value, and requires changing all the slices that contain the element. As an example of a replacement operator, define, for given integers i and m such that 1 _< i £ m,

replace j^^^^ = Ayx^^. . .Xj^:<x^ ,. . . ,x^_^,y ,x^^^ ,. . . ,x^> .

Then, it is easy to see that for all LE's a,,...,a ,b,

<a^,... ,a^> ( replace j^^^ b) ^ <aj^,. . . ,a^_^ ,b , a^^^ ,a^> .

Again, one can define [11] an LE replace with the property that for all LE's a and , b, if a ^^ _i and b ^ m, where i and m are integers, 1 £ i £m, then

replace a b -^ replace ■

,m

Hence, given the declaration array v.[l:e], we have

{v.[f]:=g}, „ . s A(()v, . . . v :(})v, . . .V . ., (v. ( replace { f} {e} (g)) ) ] \V-| , . • . '"„' ■'■ " -'- j"-'- J

V . , , . . . V .

3 + 1 n

-20-

The above representation can be generalized to the case of arrays of dimension higher than one [11], but we omit these details.

Array declaration . Recall that a variable declaration affects the representation of the block in whose head it occurs; specifically, the block representation has as a component the initial value of the variable. Array declarations are handled precisely in the same fashion as the simple variables, with the following exception: if an array is not initialized at the time of declaration, the block representation is obtained by assuming all the array elements to be fl. Thus, for an array with the bound pairs 11:2, 1:3J, the initial value is represented by <<f^ ,fl ,f^> ,<f2 ,Q ,fl>> . Since, in general, array bounds may be specified by expressions, we need to create tuples of arbitrary dimensions and sizes in which all elements are 9,. This is possible by means of an LE tupinit with the property

tupinit 1 m ->- <S ,n,f^. . . ,n> L , J

m elements

tupinit n+1 m, . . . m , , -> <A,A,...,A> , where

— "^ —1 —n+1 I ]

^ Y ^

m, elements

A = tupinit n m^ ... HI .-i •

The definition of tupinit may be found in [11].

Example . The representations discussed above are illustrated on the following block, assumed to occur in the environment (n).

begin array p[l:n], q[l:2, 1:2]; integer r;

r := q[e,f]; A = A(})pqrn : 4)pq (q (elem{e}2) (elem{ f }2 ) ) n p[r] := g B = A({)pqrn: (j) (p ( replace r n {g})) qrn

end C = A(|)n:A(B(Apqr:({))) ( tupinit 1 n) <<fl ,n> , <Q ,fl>>l^n

n;

-21-

3. ITERATION AND JUMPS

3.1 Recursive Definition of Lambda-Expressions

In dealing with program loops, we will be in need of the recursive definitions of the form

in which an LE is defined in terms of itself, by using its own name for one or more of its components. Much towards the precise understanding of such definitions has been contributed, among others, by Morris [14], Manna [3,15,16], de Bakker [17], and Rosen [18] , who have built upon the pioneering work of Kleene [19] and Scott [20,21], Referring the reader to the cited work for a rigorous analysis of recursive definitions, we shall be content here with informal, intuitive comments.

A possible explanation of (19) is the following purely mechanical one. As would be possible in the case of a non-recursive definition, we allow the replacement of an appearance of A in any LE by the right-hand side of (19). In other words, we interpret (19) as a reduction rule

A^ A A . (19a)

By a sequence of such reductions of A and the other LC contractions, it may be possible to reduce an LE containing A to a normal form. It has been shown (e.g., Rosen [18]) tha^ the Church-Rosser property holds with this broader sense of reduction also; consequently, most other important properties of reduction, such as the uniqueness of normal forms and the correctness of the standard-order reduction algorithm, are valid when the reduction rules of form (19a) (with distinct left-hand sides) are admitted. The interpretation of a recursive definition as a replacement or reduction rule certainly enables us to use the definition; but what, actually, is the object that is so defined? It is obvious that applying the reduction rule (19a) to A itself cannot lead to an "ordinary" definition — a non-self-referencing — description of A. However, such a definition may be possible

-22-

if we interpret A as a solution of the reduction relation (not rule )

A-^...A...A... , (20)

or the conversion relation /

/\ — • • • 1\ • • • I\ •••• V^JL/

These relations have, in general, infinitely many solutions. To see this in the case of (21), rewrite it in the form

or

A = FA , (22)

where F = Xx: ...x...x... does not involve A. It is now

oo

immediate that for all LE's p, the LE F p (where

a^b = ^(a(. . . (a^ b) . . .) ) and a b = lim a b) satisfies (22).

FT^ times n^°°

Also, note that because the LE

Y = Ax: (Ay: x(yy))(Ax: x(yy))

has the property

Ya ^ a(Ya) (23)

for all a, the LE YF is another solution of (22),

To reduce an LE containing A, we may, under this latter interpretation of the definition (19), replace A by a solution of (21), and then apply a sequence of contractions. The results of reduction under this interpretation and the ones under the previous interpretation (of using (19) as a reduction rule) may, in general, be expected to be different.

Now let us define a partial order on LE's as follows: a £ b (a is extended by b), if for all c it is the case that whenever ca has a normal form, then ca = cb. For example, we have Q < h for all LE' s b, where Q. is as introduced in

00

Sect. 2.8. One can show [14] that F fJ, as well as YF, are minimal solutions of (22), that is, they are extended by all LE's satisfying that relation. It turns out that, for all LE's containing A, the normal form reductions resulting from the

-23-

replacement of A by a minimal solution of (21) in thi second interpretation are precisely the same as those resulting under the first interpretation of using (19a; as a reduction rule. It is natural, therefore, to identify the LE A defined by (19) with a minimal solution of (21). Although, in general, (21) has infinitely many, mutually non-conver'cible, minimal solutions, these solutions are equivalent in the sense that they are all extended by each other, and have the same intuitive interpretation as functions. Hence, we arbitrarily adopt one of these, YF, with F as defined earlier, as the minimal solution.

Sometimes, minimal solutions are expressed in the "y-notation" [17J: we write the minimal solution of (21) as the y-expression

yx;

The y-expressions resemble A-expressions in variable binding properties; and they have the associated rules

yx: e -^ yy: (Ax:e)y (24)

yx: e ■> (Ax:e) (yx:e) (25)

The first rule simply renames the "y-bound" variable, while the second becomes obvious in view of the fact that being a solution of X = e = (\x:e)x, the LE yx:e must itself satisfy this conversion relation for x.

The above interpretations can also be generalized to include the simultaneous recursive definition of several LE's in the form

^1 = FA ••• \ '

A = F A- . . . A^ n n 1 r

(26)

where, it is understood, the LE's F's do not involve A's. The generalized interpretations are, briefly:

(a) The definitions (26) may be regarded as a set of reduction rules (replacing = by -> ) without concern as to the values of A's.

(b) The A's defined by (26) may be regarded to be the

-24-

minimal solutions of the system of conversion relations

A^ = F.Aj^...A^, lj<i<n. (27)

An explicit soluion of (27) is given by

A. = Y. F,...F , 1 1 ,n 1 n

where

Y. = AZt...z : Y(Ax: <xZt,...,xz >)(Ax,...x :x.) . i,n 1 n I'n 1 ni

Alternatively:

(~) A. = A.

I

where

(0) (J+1) (J) (J)

A. ' S Q , and A. EF-A^.-.A . 1 1 1 1 n

The interpretations (a) and (b) result in identical normal form reductions of the LE's containing A's.

3.2. Iteration Statements

The representation of the for statement of ALGOL 60 is obtained by expressing this statement in terms of the simple (non-ALGOL 60) while loop of the form while ... do ... . To represent the latter, consider the statement while b do S appearing in the environment (v,,...,v ). Calling this statement by the name T, we may (recursively!) describe it, for the purpose of LC representation, as

if b then begin S;T end

Now the formulas for the representation of compound and conditional statements, (5) and (16), respectively, are applicable to the above statement, so that its representation {t} is, recursively, the LE

A4)V,...v : {b}((A4): {S } ( {t}(J)) ) ())V, . . . v )(4)V,...v )

= A(t)Vj_. . .v^: {b} ({S} ({T}(i)) )(J)V^. . .v^ .

-25-

Thus, we adopt the representation

{ while b do S}, „ \ = V^^- A4)V^...v : {b} {{S} (x({)) ) ((>v^ . . . v ,

1 n

(28)

Alternative definitions of the same LE, call it A, are

A = A(})V, V : {b} ({S} (A(})) ) (])V^. . .v^ ,

A = Y{Xx^v^. . .v^: {b} ({S} (xcj)) ) (})Vj^. . .v^) .

Example . At this point, we illustrate the LC representations introduced so far by means of a complete program. Also, as an application of the model, we derive the correctness of the program in terms of its representation. Given below are the individual statement representations, shown on the same line as the statements (or on the last line for multiple line statements), and have been designated names for reference purposes.

A = A<j)xyoi :(t)iyo B = A())xy: 4)xO^

C = A(|)zxy : 4)0^xy

D = X(})zxy :(t)zx l+y+2x z

E = X4)zxy:()) z+1 xy

F = \<t>: D(E(}))

G = X(j)zxy: z<x (F (G<|)) ) (})Zxy

H = X(i): C(G(Az:(()) ) f2

J = A({)xyo:(j)xy o,y

K = A((): A(B (H(J(Axy :<})))) )Qi^

{program} s P = KII

-26-

We wish to prove that on reading a nonnegative integer n,

2 this program will print out the integer n . According to our

input-output conventions, we need to show that

2

P n ->■ <n_> , for all integers n >^ 0 . (i)

This is done in four steps, as follows.

(a) We show that for all LE <j) and all integers n and i,

2 2

G (J) i^ n j^ ^ 4* i. D. i_ / if i >^ n , (ii)

2 2

G (J) i n i^ ^- G4) i+1 n (i+1) , if i < n . (iii)

By using the definition of G, we obtain

2 2

G <i> i n i^ ^ i < n (F(G(J))) (j) i n i

If i >^ n, then i < n ->- false , so that (ii) is immediate. Otherwise, i < n ^ true, and the above LE

^ F(G<f))i n i^ -V D(E(G(})))i n i^

^ E(G(}))in 1+i +2x1 -v E(G(})) i n (i+1)

-> G(J) i+1 n (i+1) .

(b) Next, for all integers n and i such that 0 < i _< n, we have

2

G(t)OnO^G(t>ini_ . (iv)

This is proved by induction on i. From (iii) one easily verifies (iv) both for i = 1, and for i = j + 1 _< n when the case for i = j < n is assumed.

(c) Next, we claim that for all integers n >^ 0, it is the case that

H(j)np->4)nnr. (v)

For, we have

-27-

H(t)nq E (A(J): C {G{Xz :<^) ) Q) <i> n 0 -V C(G(Az:(})) )^ n 0 H- G(Az:()))0 n 0

Now if n = 0, then from (ii) it follows that

2 2 G(Az:(J))0 n 0 ^ (Az:(l))n n n_ ^ (}) n n_ .

On the other hand, if n > 0, then for the case i = n, (iv) yields

G(Xz:(t))0 n 0 ^ G(Az:(())n n n_

2

->■ (Az:({))n n n_ , by (ii)

2

->- 4) n n_ .

(d) Finally, to prove (i) we simply use the definitions of the LE' s A through P, obtaining, for all integers n >^ 0,

PnEKIIn-^ A(B(H(J(Axy:I) ) ) )nS^In -> B(H(J(Axy:I) ) )n fi I

-^ H(J(Axy:I) )n 0 I

2 -^ J(Axy:I)n n_ I , by (v)

2 2

■> (A xy : I) n n_ I ,n

->■ I ,n

2 ->■ <n > .

-28-

Returning to the discussion of iteration statements, we can express the general for statement of ALGOL 60 in terms of the simple while loop treated above. For example, we can reformulate the statement

fo

r V. := e, step q^ until eo do S

as

begin v. :=e, ; while (v.-e.,) xsign(e„) < 0 do

begin S; v. := v.+e2 end end . .:■:•:'

The latter form can then be represented as an LE by employing the representations of compound and while statements. Omitting the detail"^ of derivation, we list below the LC representations for the three cases of for list elements, namely, arithmetic expression, while element, and step-until element:

{for V. = e do S}, .

1 — (v^ ,. . . ,v„)

1 n '

s A(})V,...v : {S }(J)V, . . . V. _, {e}v. , . . . V . (29)

{for V. := e while b do S} , > 1 — (Vj^,...,V^)

= yx: A(})V, . . .V : (Xv. : {b }) {e} ( {S } (xcj)) ) ())V, . . . v. _^{e}v^_i_^ . . . v^ (30)

= Y(Ax(t)V, . . .V : (Av. : {b}) {e} ({S} (x(})) ) <})V, . . .v._j^{e}v^_i_, . . .v^)

{for V. = e, step e- until e, do S}, >

= A(t)V,...v : (Y ( Axcbv, . . .V : { (v.-e,)x sign (e„) < 0} ^1 n 1 n ij 2. —

({S}(Av,...v :x(()V,...v. , {v.+e-Iv. , , . . .v^) ) 1 n 1 i-i 1 2. 1+1 n

(j)V, . . .v^) ) (f)VT . . .V. 1 {e, }v. , T . . .V . (31) 1 n 1 1-1 1 1+1 n

-29-

To execute the statement S s goto L, we may, in effect, siobsti-tute the part of the program following L for the one following S. This observation is the basis of our representation of both labels and jump statements.

A label is identified with the part of the program following

it. To be accurate, the representation of a label L occurring

in a program P is taken to be the representation of the program

P' obtained from P by deleting all the statements, but retaining

the declarations, that appear above L. This representation can

be obtained in a simpler manner by using the following inductive

scheme: Let the label L occur in a block b whose declared

variables are v, , . . . ,v .

1 n

1) If L is followed by statements S, ,... ,S , and a label M,

^ 1 m

in that order, all within b, then

{L} s {S,}({S„}(...({S^}{M})...)) 12 m

2) If S, ,S„,...,S are the statements following L to the

12m ^

end of b, then

{l} S {S^}({S2} (. .. ({Sj^}(AVj_. . .v^:N) ) . . .)) ,

where N e l, if b is the outermost block, else N is the representation of the program part following b, that is, of the (possibly imaginary) label immediately after the end of b. According to the rules of ALGOL, the label to which a jump can be made must be in a block which is the same as, or outer to, the block containing the jump statement. It follows that (the list of variables constituting) the environment of a jump statement must contain the environment of the referred label as a final segment. Suppose (v,,...,v ) is the environment of the statement S s goto L, and (v ,...,v ), where 1 £ m £ n, is the environment of L, and let (j) represent as usual the program

-30-

remainder of S. The execution of S causes the program to compute the function {l} (v ,...,v ) instead of (})(v. ,...,v ) Hence, the representation of S can be taken to be the LE

which reduces to

AAv, ... V : {L}v ... V , ^1 n m n

X<i)V^ . . . V , : {l} 1 m-i

Thus, we define

{ goto L, environment (L)= (v,...,v),l£m_<n}, ,

1 n

= A(f): (Av^. . .v^_^: {L}) . (32)

It is sometimes convenient, specially in connection with conditional statements, to write the right-hand side LE in the convertible forms

Xi)V, . . .V : {l}v ...V or A4'V,...v : (Av,...v ,:{l})v,...v . ^In mn ^Inl m-1 1 n

Example . The representation of goto statements and labels is illustrated by means of a complete program. The program below has been derived from the program given in the previous example simply by expressing the while loop in terms of goto 's. As another application of the model, we prove the (input-output) equivalence of the two programs.

As before, the representations of individual statements are shown on the same line as the statement, or on the last line for a multiple-line statement, and are designated identifying names. The LE's common to the representation of both programs have the same names. Label representations are given at the end. (The superfluous label M serves simply to illustrate the case (1) of label representations discussed above.)

-31-

begin integer x,y;

read x; A = A(})xyoi :(j)iyo

y := 0; B = X(J)xy :<J)xO^ begin integer z;

z := 0; C = A(f)zxy :(t)0^xy ->■ A(j)z: (pO_ L: i_f z=y then goto N

else goto M; D'e A(()Zxy: z=y (Az:N)Mzxy

M: y := y+2x z+1; E'= X(t)Zxy :(})zx y+2x z+1

z := z+1; . F'= A(j)Zxy:(}) z+1 xy

goto L G' = A({): L

end; E'= A(t): C (D' (E ' (F ' (G" ( Az :(()))))) fi

N: write y; J = A(f)xyo:4)xy o,y

end K'= Ac}): A (B (H ' (J ( Axy :(}))))) f2J^

{Program} E P' e K'll

L = D'M , M E E' (F* (G' (Az:N) )) , N E J(Axy:I)

We wish to prove that the above program and the program of the previous example produce the same output when executed with the same non-negative integer as the input datum. That is, in terms of their representations, we wish to show that for all integers n >_ 0,

P n = P'n . (i)

Of course, this can be shown by using the previously obtained result

2

Pn -^ <n > m conjunction with a direct proof of the fact that

2

P'n ^ <n >. But we will prove the equivalence of the programs by

verifying, in effect, thattheir differing parts do the same work when the programs are executed. These differing parts are represented by the LE's H and H'. If we can show that for all integers n >^ 0,

H N n 0 = H'N n 0 (ii)

(where N e j(Axy:I), defined in the present example), then (i) is demonstrated as follows. From the previous example, part (d), we know that for all n > 0,

-32-

P n -> H(J(Axy :I) )n 0 I ,

= H N n 0 I .

Since P and P' differ only with respect to their components H and H", respectively, we must also have for all n >^ 0, ,

P'n -> H'N n 0 I .

Hence, P n = P'n by (ii).

It remains to verify (ii). From (v) in the previous example, we have for all integers n >_ 0,

2

HNnO^Nnn .

So (ii) would follow if we can also prove

2

H'NnO->Nnn_. (iii)

To outline the proof of (iii), we simply state the sequence of reduction relations leading to it.

(1) L i n i^ -^

N n n_ , if 1 = n ,

2

L i+1 n (i+1) , if i 7^ n .

(2) LOnO->Lini3., for 0 < i <_ n

2

(3) LOnO->Nnn_ , for n >_ 0

2

(4) H'4) n 0 •> N n n_ , for n >_ 0 .

The treatment of designational expressions and switches is omitted, except for an example which should suffice to indicate how these can be represented as LE's. In the schematic program below, b and c denote Boolean, and e and f, arithmetic expressions,

-33-

begin integer x; M: ... begin integer y;

begin integer z;

switch S := K, if b then Sle] else L, M;

• • •

K: ...

begin integer w; , ■

* * *

goto if c then M else SIf]; end w; — ' ..

end z; L: ... end y; end

The representations of the switch and goto statements in the above program are, respectively,

S = <K, b(Xzyx: S [e] ^zyx) (Az :L) , Azy:M> ,

A(})wzyx: c (Xwzy :M) (Aw: S[f]-,) ,

where, for brevity, underlined letters are used to designate

corresponding representations, and the LE ( elem i n)

(Cf. Sec. 2.12) is written [ij .

— n

-34-

.4. PROCEDURES

r "■■ ■

4.1 Functions

We use the term function to denote a type procedure without any side effects. In particular, a function is a procedure in which

(1) a value is associated with the procedure name,

(2) all parameters are called by value,

(3) no global variables are modified,

(4) no jumps are made outside the function body, and no procedures are used other than functions.

Because of the above restrictions, the representation of functions is much simpler than that of general procedures. Since many procedures encountered in programs are truly functions, it seems useful to deal with them as a special case.

For the moment, let us consider only the functions which do not involve global variables at all. For these, the environment of the function declaration is immaterial. Let f(p,,...,p ) be such a function with parameters p.. We wish to represent f in such a manner that for all expressions e,,...,e

{f }{ej^}. . . {e^} ^ f (e^^,. . . ,e^) (i)

Such a representation is accomplished as follows: We use a variable it to denote the function value; that is, all assignments to f are represented as if made to it. Further, we represent the statement S constituting the body of f by taking its environment to be (■'T,Pi ,' • ' ,p )• Now, starting with an arbitrary value of tt, and the values e. of p. , the execution of S has the effect of assigning the value f(e,,...,en) to tt , and certain values to p. which are irrelevant to the result; say, we have

{s}(j)TT{ej^}. . . {e^} -^ (}) f (e^^,. . . ,e^) P3_---Pn • (^i)

-35-

Comparing (i) and (ii) , we can choose the LE Airp . . .p :it for (J) , Q. for IT, and {S}(})7t for {f}, so as to satisfy (i) . Thus, we adopt

{ function f (p, ,. . .p ) with body S}e{S}, . (Airp, . . .p :it) J

j_ n V'i^,p^,..»pj X n

, ,u:i. ■ -zAr: ■ : . :j I... (33)

It should be pointed out thvt a label appearing in the body of a function is to be represented as the part of the function (not the program) that follows the label.

Example . The following procedure is a function; hence (33) is applicable.

integer procedure mod(x,y); value x,y; integer x,y; begin integer q;

q := x-Jy; < A = A())qTrxy :(j) x^y TTxy

mod := x-yxq B = A(|)qiTxy: (l)q x-yxg xy

end q C = A(j): A (B (Aq:()))) Q .. _

end mod; mod = C(ATTxy:TT)fi

Example . Simplification of a function representation.

integer procedure fact(n); value n; integer n; fact := i_f n £ 0 then 1 else n x fact(n-l) ;

In this case, we have

{body} = A(t)7rn: (\) ( n=0 1 (n x (fact (n-1) ) ) n fact E {body } (Aftn :it) f2

■^ An: n=0 1 (nx (fact (n-1) )) ,

so that, alternatively,

fact E Y(Azn: n=0 1 (nx(z(n-l))) ) .

-36-

Finally, it is easy to lift the restriction about global variables imposed earlier on functions: All one needs is to treat each variable in the environment of a function declaration as a parameter, in addition to the explicitly declared parameters of the function. This is illustrated below.

Example .

begin integer x,y;

integer procedure f(n); value n; integer n;

f := n+x; A = AcJjTrnxy: (J) n+x nxy

... f = A( Airnxy : tt) fi

begin integer z;

X := f(y)+z A(()zxy : ({)Z (fyxy)+z y

4.2 Call-by-name, Side-effects

In the previous section, we have described the LC representation of procediores subject to rather stringent conditions. We will now show how the representations can be extended to more general procedures, allowing call-by-name, the use of global variables, and side effects. However, we limit ourselves here to considering the formal paramters of the type integer and label only. But the extension of the model to include real and boolean parameters is trivial.

In ALGOL 60, a procedure call is intended to have the effect of an appropriately modified copy of the procedure body [12]. The modification in the case of call-by-name consists in replacing each instance of a called-by-name formal parameter by the corresponding actual parameter. (It is understood that any name conflicts between the variables appearing in the actual parameter expressions and the local variables of the procedure are to be first removed by renaming the latter variables.) Instead of performing such symbolic substitution, however, which would require

-37-

keeping procedures in text form at the execution time, ALGOL compilers accomplish the same effect by treating formal parameter references in procedure as calls on special "parameter procedures" generated from actual parameters [22]. As a result, if an operation refers to a formal parameter during the execution of a procedure, then the procedure execution is suspended to evaluate the corresponding actual parameter in the environment of the procedure calling statement , and then the procedure execution is resumed using the so-acquired value in the operation. Of course, depending upon the type and use of a parameter, the actual parameter evaluation may yield a value (e.g., an arithmetic or Boolean quantity when the formal parameter is an operand in an expression) or a name (e.g., the address of a variable when the formal parameter appears to the left of an assignment statement.) Our LC interpretation is based on a similar idea. But we make use of different "parameter procedures" for different operations performed with the same parameter; namely, the evaluation of actual parameter expressions, making assignments to the variables provided as actual parameters, and jump to an actual label.

4.3. Integer Parameters '

In the absence of procedures we were able to express each statement in a program as a function which had for its arguments the variable tj), denoting the program remainder (that is, the part of the program following the statement), and the variables constituting the environment of the statement. Clearly the representation of a statement S in a procedure body would involve two sets of program remainders and environments — namely, one set for S itself and one for the statement, say T, that calls the procedure. The program remainder of T corresponds to the familiar "return" address or label for the procedure call. Now, any formal parameter instances in S give rise to actual parameter evaluations in the environment of T, but after the evaluation the control must eventually transfer back to S.

-38-

Hence the representation of parameter evaluation also involves the two sets of environments and proc/ram remainders; but this time the program remainder of S serves as the return address. We will use the variable p to indicate the program remainder at the return point and t}), as usual, for the program remainder at the current point.

We have so far represented, and will continue to represent, each program variable by a single LC variable. The representation of an assignment statement may be conceived as "binding" the LC variable representing the variable appearing at the left-hand side to the representation of the right-hand expression. In general, the LC variables representing program variables are "bound" at any time to the current values of the corresponding program variables. With each called-by-value formal parameter we similarly need to associate a single LC variable, bound to the current "value" of the parameter at any time. However, we need to carry more information with a called-by-name formal parameter; depending on the type and use of a parameter we shall associate a number of LC variables with it. For each called-by-name formal parameter of type integer, we require three variables best thought of as being bound, respectively, to the "value" associated with it and to the "parameter procedures" for evaluating it and making assignments to it. If p is an integer parameter, then these three variables will be usually denoted by P/ Pp ' ^^"^ P • (The parameter of type label will be discussed later.) The environment of a statement in a procedure body will consist of the following, in the given order:

a) variables local to the procedure,

b) p , the return variable,

c) variables representing the formal parameters,

d) variables global to the procedure.

The present descriptive use of "binding" and "bound" has no connection with the terms defined at the beginning of Sec. 2.1,

-39-

Next, associated with each called-by-name actual parameter p of type integer, and individual to each procedure call , is an LE that represents the parameter procedure for its evaluation; in case p is a program variable (rather than an expression), there is also another LE which represents the "parameter procedure" to effect assignments to p called for in the procedure. These "actual evaluation" and "actual assignment" operators are usually denoted e and a , respectively, with further distinguishing marks added when more than one procedure call is involved.

Lastly, associated with each called-by-name formal parameter of

type integer, and unique to each environment within the procedure

body , are two LE's which represent the calls on the "actual

evaluation" and "actual assignment" parameter procedures mentioned

above. For convenience, these LE's are referred to as "formal

evaluation" and "formal assignment" operators, and are usually

denoted e and a where p is the formal parameter, with

P P further distinguishing marks added if more than one environment is

involved. If, in a statement in a procedure body, a formal

parameter appears as an operand of an expression, the statement

will be represented as if preceded by a formal evaluation;

likewise, if a formal parameter occurs at the left-hand side

of an assignment statement, that statement will be represented

as if immediately followed by a formal assignment.

The above ideas will now be illustrated by means of a very

simple example:

begin integer a;

procedure P(x); integer x; x:=x+2;

P (a) ;

end .

The body of the above procedure consists of a single statement, and that statement needs to be both preceded by a formal evaluation and followed by a formal assignment. Thus, it is represented by the compound

-40-

X(j): e^(A(a^4)) ) = B ,

say, where A is the representation of x:= x+2 as an ordinary assignment statement. Since there are no local variables in the procedure, the environment of this latter statement consists of the following:

p the "return" variable,

X the "parameter evaluation" variable,

X the "parameter assignment" variable,

X the "parameter" variable, and

a the global variable.

Thus we can write

A = AApx X X a: (bpx x x+2 a .

Now, as the variable x is bound to the "actual evaluation"

e

operator, and the "formal evaluation" consists of just an application of this LE, we define e to be

or more simply.

XApx X xa: X pcbx x xa ,

XApx X X : X pAx x x

Note the interchange of <p and p above; this signifies that the program remainder at the return point of procedure call becomes the current program remainder during parameter evaluation, and vice versa. In a similar manner, we define

a = Acbpx X X : X pAx x x

(In general, the global variables of the procedure need not appear in the formal evaluation and assignment operators.) The whole procedure may be represented by

P E B(Apx X x:p) ,

which displays the effect that once the procedure execution

is over, (after the application of B), only the return variable

-41-

is retained, and the other variables, namely, the ones connected with parameters, are deleted from the environment.

Next, let us look at the procedure call. There is only one called-by-name actual parameter of type integer in this case. So we need to define two LE's e and a , the actual evaluation

X X

and assignment operators. These serve essentially as the fictitious assignment operators x:=a and a:=x, repsectively, and thus can be defined by

e = Acbpx X xa: pd)x x aa , X ^ e a e a

a = Actpx X xa: pAx x xx . X ^ e a e a

Again the interchange of <j) and p is needed to represent the fact that after evaluating the actual parameter in the environment of the procedure calling statement, the control passes back to the procedure body.

The purpose of the procedure calling statement itself is threefold:

a) to extend the environment from (a) to (x ,x ,x,a)

b) to initialize the added variables; that is, substitute

e for x , a for x , and, by convention, Q for x. X ex a -^

c) to apply P before the rest of the program; that is, substitute P(J) for (J).

Consequently, the statementP (a) above may be represented by the LE

(Ax X x: (Ad)a: Pcbx x xa) ) e a il ,

which simplifies to

Acba: PAe a Qa ^ X X

It should not be difficult to see that coroutines can be represented by using the same idea, as follows: The "remainder" of each coroutine may be represented by a different variable. The coroutine calls are then representable by LE's which simply permute these variables to bring the remainder of the called coroutine in front. We will soon see how we can also account for the private variables of a coroutine by "covering" them when the control passes out of it and "uncovering" them on return.

-42-

We now list the representations discussed piecemeal above along with the original program.

Example .

begin integer a;

procedure P(x); integer x;

f e = Actpx X x: x pAx x x

a = XApx X x: X pcbx x x X ^"^ e a a e a

X := x+2 A = A(t)px x xa: (Jjpx x x+2 a

B E Xcf): el{A{al<^))

; PEB(Xpxxx:p)

' ^ e a

P (a) ; C = A(j)a: P(})£ a f2a

... e^ E AApx X xa: p^x x aa

X ^^ e a e a

a = Acbpx X xa: pAx x xx

X ^ea ea

end

Next, let us consider the LC representation of type procedures in which a value is associated with the procedure identifier. In this case we will use an additional variable tt to denote the procedure value in representing the statements of the procedure body. The representations are otherwise similar to that for routine type procedures discussed above. A procedure call which uses the function designator of a procedure within an expression will be represented as if it were compounded of two statements — the first a procedure call to obtain the value of the procedure, and the second using that value in the expression.

The representation of a type procedure is shown in the following example, which also illustrates the treatment of call-by-value in our present scheme of procedure representation. (Some explanations follow the program.)

-43-

Example

begin integer u,v;

integer procedure P(x,y); integer x,y; value y;

f

begin

P := x-y;

X := y

end compound end P;

e = AApTTx X xy: x pcbirx x xy a = Ad)pTTX X xy: x pctirx x xy

A = X(^p-nx X xyuv: (J)p x-y x x xyuv

B = X(^: e^(A(())

C = AcjjpiTX X xyuv: (j)p7Tx x yyuv

D = X<t>: C(a (f))

E = X(f>: B(D(J))

P = E(ApTTX X xy: pu)

u := P(v,u+l) + u;

end

A<})uv: P(^Qe a Q u+1 uv

X

a

A(J)pTTX X xyuv: pcfjirx x vyuv

a = A4)pTTX X xyuv: p(()7rx x xyux

G = A(})iTuv: ({) TT+u v H 5 A(}): F{G(})) .

The environment of the statements in the procedure above consists of eight variables: namely, the return variable p, the procedure

value variable tt , the three variables

, and X for the

e a

called-by-name parameter x, the single called-by-value parameter

variable y, and finally the two global variables u and v. Of these

the four parameter variables are effectively discarded at the end

of the procedure body execution by the representation P of the

procedure. The procedure call is represented as the compound of

two statements F and G: F computes it, the procedure value, and

G makes use of this in the assignment statement.

■44-

In bot±i previous examples, the environment of the procedure declaration and the procedure call are the same. In the general case, these environments may be different; this is so, for example, when a procedure call takes place in a block inner to the procedure declaration. When this happens, there arises the problem of "covering" the local variables of the calling point that do not have valid declarations in the procedure body. Of course, the covering should be such that the variables may be "uncovered" on return to the calling point. Notice the contrast with jumps in which the variables that do not have valid declarations at the jump label are simply discarded permanently. Covering is also needed in specifying the formal evaluation and assignment operators for use with statements inside a block in a procedure body, since in this case, again, the variables local to the procedure body are invisible at the calling point.

The following example shows a way of covering the non-overlapping parts of the environment, in order to overcome the environment conflict problem. (See explanations below.)

Example

begin integer x;

procedure P (y); integer y; begin integer z;

z : = y+ 3;

e^ = X(t>zpY^Y^y: py^ (Xi|j r^^cjiz) y^y^y

A E A())zpy^y^yx: cf) Y±l PY^Yq^Y^ B = X<i>: e^(A()))

end block

end P ;

C, say

P = C(Xpy^y^y:pI)

begin integer u; P(u+x);

end

end

D =A(j)Ux: P (X<J;:i{;(})u) e Q^x

e^ = A({)Upy^y^yx: pl (Ai|i :ij;(})u) y^y^ u+x x

-45-

In representing the procedure call in the above example, (Ai^:4;(J>u) is passed as the return point argument instead of (|), thus covering u. The application of the former to any LE uncovers u and restores the environment; e.g., in e , the application is made to y , and in P, to I. Note that in the representation of the procedure call, namely, D, we have used Q for what would otherwise have been a ; this is so, because no assignment can be made to the particular actual parameter in this case.

The evaluation and assignment operators, both formal and actual, have been defined above slightly differently than in the two previous examples in which covering was not required. These two examples are worked out once again so as to make the treatment uniform whether or not covering is needed in a particular case.

Example

begin integer a;

procedure P(x); integer x;

e = Ad)px X x: px ( AiIj : liid)) x x x

a = A(i)px X x: px (Ail; ripd)) x x x

x:= x+2 A = Actpx x xa: (bpx x x+2 a

; P=B(Apxxx:pI)

P (a) ; C = A(t)a: P (Aijj :ijj(l)) £ a Q,a

... e = A(i)px x xa: pi (Aip iij^cf)) x x aa

x ^'^£a '^'^'^'^ea

tj = Act)px^x^xa: pi { AiJj rijjc))) x^x^:

end

-46-

Example

begin integer u,v;

integer procedure P(x,y); integer x,y; value y;

e = X(()p7rx X xy: px (At|j: i|;(})) irx x xy a = A(()pTTX x xy: px (AiJ; itjjt})) ttx x xy

begin

P := x-y; A = A({)pTTx x xyuv: <t>p x-y x x x y u v

B E Act): e^(A(}))

x := y C = A(()p7rx x xyuv: (()pTTx x yyuv

D = Acf): C(a^(}))

end compound E e \^: B(D4))

end P; P e E(Apttx x xy: plir)

• • •

u := P(v,u+l)+u; F = A(t)uv: P (Ai|j: ijj())) f2e a Q u+1 uv

e EAcJjpiTX x xyuv:pl (Ai|j :4j(f)) TTx x vyuv a =A(|)pTTx X xyuv: pi (Aijj :4;(J)) TTx x xyux

^ £ Ot t, uc

G = A(t)TTUV: 4) TT+U V

H E Acf): F(G()))

For subscripted variables occurring as actual parameters, the actual evaluation and assignment operators are again chosen so as to represent the fictitious assignments between the formal and actual parameter variables. But now this involves the LE's elem and replace introduced in the discussion of arrays (Sec. 2.12). We will simply illustrate the representation by means of an example.

-47-

Example

begin integer n;

begin integer array x[1:n];

procedure P(u,v); integer u,v; begin

end P ; begin integer y;

P(y,x[y]) end end end

For the above program, the representation of the procedure calling statement P(y/X[y]) is the LE

A(j)yxn: F {X\l) -.^(py) e a Q e a i^ x n , where,

e = Aiypu u uv v vxn: pi (A^': iptty) u u y v v v x n ,

a^ - ^<)>ypu^u^u v^v^v X n: pi (Xi/j: ijj(l)u) u^u^u v^v^v x n

ej = ^^yP^e^a^^e'^a^ ^ "' P^ ^^^^'^'^Y^ ^e^a^ v^v^(x(elem y n) ) x n , a = Ai^ypu u uv V V X n: pi (Ai|j: ijj4)y) u u u v v v (x ( replace y n v))n .

A procedure body may contain a procedure call, possibly a recursive one, in which the formal parameters are used in actual parameter expressions. And the parameters of the nested call may themselves be called by name. The representation in such a case requires covering of all the variables associated with the procedure body, including the local variables, the return variable, and the parameter variables. This is illustrated below.

-48-

Example

begin integer x;

procedure P (y ,n) ; integer y,n; value n; begin

end P; procedure Q(z); integer z; begin integer w; P(z,x) ;

• • •

end Q;

end

If the representation of the body of the procedure P is A, then the representation of P itself is

P = A(Xpy^y^yn: pi) .

The representation of the statement P(z,x) is

X(t>: e^(B(l)) ,

where e is the formal evaluation operator for z in Q, and z

B represents the call on P, as follows:

B = A())wpz z z x; P (Aij; :i[i(})wpz z z)e a fix x , Gy = A(})wpz^z^z p-^y^y^y x: p^I (Atjj :ijj({)wpz^z^z)y^y^z x , a E Ad)wpz z z p^y y y x: p, I (X(l; riiiAwpz z y)y y y x .

-49-

The next example illustrates the representation of a procedure calling statement in which an actual parameter itself consists of a call on a procedure.

Example

begin integer x;

procedure P(r,s); integer r,s; begin ... end P;

procedure Q(t); integer t; begin ... end Q;

begin integer y; , :.

P(x, Q(y)) ; end end

Because the second actual parameter, Q(y), in the above procedure calling statement P(x, Q(y)) does not require an assignment operator, the latter statement is represented by the LE

A())yx: P(A()):ij;<j)y)e a f^ e fl fix. ■ -

The first actual parameter, x, poses no problem, other than the covering of the variable y not visible to the procedure declaration of P; hence, we define

e = AAypr r r s s s x: pi (Aii» iilKfcy) r r x s s s x ,

a = AAypr r r s s s x: pi (Ail) :iiid)y) r r r s s s r .

For the second actual parameter, Q(y), things are slightly more complex. (Note, however, that only an evaluation operator is needed in this case; the assignment operator is undefined.) First, we have to provide for a call on Q — which requires covering all the variables associated with the call of P -- with the following actual evaluation and assignment operators:

-50-

aj = A(i)ypr^r^r s^s^s p^ tt t^t^t x: p^I ( A^j : 4j(})tpr^r^r s^s^s)ut^t^t x

Now, e^ is defined in terms of a call on Q, followed by an assignment of the resulting value to s, as follows:

a a^

A = A(})ypr^r^r s^s^s x: Q (Aij; :4;(f)ypr^r^r s^s^s)Q e^a^Q x ,

B s A(t)ypr^r^r s^s^sttx: pi (Aijj: ij;(|)y) r^r^r s^s^tt x ,

e^ E A(|): A(B(j)) . s

4.4 Label parameters

The representation of label parameters is actually much simpler than of the integer variety. The reason is that two different operations, evaluation and assignments, are possible with the latter type; in addition, the value of the parameter at any time has to also be carried along within the representation. In the case of a label parameter, the only possible actual operation is a jump to it. Thus, with each formal label parameter, p, we need to associate only one variable, usually denoted by p , which is to be bound to the operator for effecting the actual goto operation. (The variable p is an element of the environment of the procedure in which p is declared.) Next, associated with each actual label parameter, and individual to each procedure call, is an LE that represents the parameter procedure to effect the jump to the actual label. For a parameter p, this "actual goto " operator is usually denoted by y / with further distinguishing marks added when more than one procedure call is involved. Lastly, associated with each formal label parameter, and unique to each environment within the procedure body, is an LE, the "formal goto " operator, that represents a call on the actual parameter procedure, that is, an application of the actual goto operator; the formal

-51-

goto operator for the parameter p is denoted y / again with further distinguishing marks added if more than one environment is involved.

For anyone who has followed the previous treatment of jumps (Sec. 3.3) and procedures with integer parameters (Sec. 4.3), the example below should suffice to explain how to represent label parameters.

Example

begin integer a;

procedure R(v); label v;

goto v; A S Y^ E X(})pv : p v^ (Aijj ril^cf)) v

R = A(Xpv :pl) ^^

begin integer b;

procedure P(x,z); integer x; label z;

e E Acbpx X X z : px {\\b zixb) x x x z X ea Y£ e ci y

a E Ad)px X X z : px (Ail;: iLid)) x x x z X ^ea ya^ ^^ e a y

y = AApx X x z : pz (Ail; til;*) x x x z 'z ^*^ e a Y y e a y

R(z); B E Acbpx x xz ba: R(Aiii rilxbpx x xz b)y a

' ^ e a y ^ e a y 'v

a_ f

y = Acbpx X xz bpiV a: y cbpx x xz b a 'v ^ e a y 1 y 'z^^ e a y

begin integer c,d;

P(d,L) C = Ac})cdba: P (Ai|; :4^(t)cd) e^a^f^y^ba

pi

e = Acbcdpx x xz ba: X ^ e a y

pi (Alii :4;(bcd) x X dz ba

a E Acbcd p X X xz ba: X ^ ^ e a y

pi (Alii: liicbcx) X X xz ba

y = Acbcdpx x x z ba: Lba ' z ^ e a y

end; Xj : ...

end end

-52-

By interpreting programming constructs intuitively as functions rather than machine commands, we have succeeded in modelling programming languages in pure lambda-calculus. We have been able to provide a nonimperative, completely descriptive representation of most of the important features of programming languages, including assignments, jumps, and procedures involving call-byname and side-effects.

An immediate application of the model is in a simple semantic specification of programming languages in terms of lambda-calculus, achieving a standard of rigor that matches their syntactic specification. Of more interest, however, is the potential of this model in the study of properties of programs, in proving program equivalence and correctness, and in program simplification (source code level) and optimization (compiled machine code level). Since we describe a program as a lambda-expression, the above mentioned applications essentially reduce to transformations within lambda-calculus. The possibilities of some of these applications have been indicated in the body of the paper by means of examples.

-53-

1. Hoare, C. A. R., "An Axiomatic Basis for Computer Programming," Comm. ACM 12, 10 (Oct. 1969), 576-580, 583.

2. Burstall, R. M., "Formal Description of Program Structure and Semantics in First-Order Logic," Machine Intelligence _5

(ed. Meltzer, B., Michie, D.) Edinburgh Univ. Press (1970), 79-98.

3. Manna, Z,, Vuillemin, J., "Fixpoint Approach to the Theory of Computation," Comm. ACM 15 , 7 (July 1972), 528-536.

4. Church, A., The Calculi of Lambda-Conversion , Princeton,1941.

5. Curry, H. B., Feys, R., Combinatory Logic , Vol. I, North-Holland, Amsterdam (1968).

6. Hindley, J. R., Lercher, B., Seldin, J. P., Introduction to Combinatory Logic , Cambridge Univ. Press, London (1972).

7. Landin, P. J., "A Correspondence between ALGOL 60 and Church's Lambda-Notation," Comm. ACM 8, 2-3 (Feb., March 1965), 89-101, 158-165.

8. Stratchey, C, "Towards a Formal Semantics," in Formal Language Description Languages (ed. Steel, T. B.), North-Holland, (1966) , 198-220.

9. Orgass, R. J., Fitch, F. B., "A Theory of Programming Languages," Studium Generale 22 (1969), 113-136.

10. Reynolds, J. C., "Definitional Interpreters for Higher-Order Programming Languages," Proc. ACM Conf . (Aug. 1972), 717-740.

11. Abdali, S. K., "A Combinatory Logic Model of Programming Languages," in preparation.

12. Naur, P., et al., "Revised Report on the Algorithmic Language ALGOL 60," Comm. ACM 6 , 1 (Jan. 1963), 1-17.

13. van Wijngaarden, A., et al., "Report on the Algorithmic Language ALGOL 68," Numerische Math . 14 (1969), 79-218.

14. Morris, J. H., "Lambda-Calculus Models of Programming Languages," Project MAC Report MAC-TR-57, MIT, Cambridge, Mass. (Dec. 1968).

-54-

15. Manna, Z., Ness, S., Vuillemin, J., "Inductive Methods for Proving Properties of Programs," SIGPLAN Notices 7 , 1 (Jan. 1972) 27-50.

16. Cadiou, J. M., Manna, Z., "Recursive Definitions of Partial Functions and their Computations," SIGPLAN Notices 1_, 1 (Jan. 1972), 58-65.

17. de Bakker, J. W., Recursive Procedures , Mathematical Centre, Amsterdam (1972).

18. Rosen, B. K., "Tree-Manipulating Systems and Church-Rosser Theorems," JACM 20 , 1 (Jan. 1973), 160-187.

19. Kleene, S. C. , Introduction to Metamathematics , van Nostrand, Princeton, New Jersey (1950).

20. Scott, D., "Outline of a Mathematical Theory of Computation," Proc. 4th Ann. Princeton Conf. on Info. Sci. and Sys . (1970), 169-176.

21. Scott, D., "Lattice Theory, Data Types, and Semantics," in Formal Semantics of Programming Languages , (ed. R. Rustin), Prentice-Hall, New Jersey (197 2) , 65-106.

22. Randell, B., Russell, L. J., ALGOL 60 Implementation , Academic Press, New York (1964).

-55-

This report was prepared as an account of Government sponsored work. Neither the United States, nor the Commission, nor any person acting on behalf of the Commission:

A. Makes any warranty or representation, express or Implied, with respect to the accuracy, completeness, or usefulness of the Information contained In this report, or that the use of any Information, apparatus, method, or process disclosed In this report may not Infringe privately owned rights; or

B. Assumes any liabilities with respect to the use of, or for damages resulting from the use of any information, apparatus, method, or process disclosed in this report.

As used in the above, "person acting on behalf of the Commission" Includes any employee or contractor of the Commission, or employee of such contractor, to the extent that such employee or contractor of the Commission, or employee of such contractor prepares, disseminates, or provides access to, any information pursuant to his employment or contract with the Commission, or his employment with such contractor.

-56-