Making Variables Abstract:
An Equational Theory for Russell
Alan Demers
Computer Science Department
Cornell University
Ithaca, NY 14853
James Donahue
Xerox Corporation
Palo Alto Research Center
3333 Coyote Hill Road
Palo Alto, CA 94304
Introduction
One of the fundamental notions of programming, and thus of programming languages, is the variable.  Recently, the variable has come under attack.  The proponents of "functional programming" have argued that variables are at the root of all our problems in programming.  They claim that we must rid our languages of all manifestations of the "vonNeumann bottleneck" and learn to live in the changeless world of functional combinators.
While we may not believe all the claims of the functional programming advocates, there is evidence that the treatment of variables in most programming languages leaves much to be desired. In this paper we discuss how to make variables "abstract", i.e., how to introduce the notion of variable into a language so that variables have reasonable mathematical properties.
This paper includes:
a discussion of language design principles that allow a more mathematical treatment of variables in programming languages, and
a description of an equational logic for the programming language Russell [Boehm80].  Although this logic follows much of the development of abstract data types (cf. [Guttag78]), it is novel in its treatment of a language in which expressions not only produce values but also can have effects. We discuss the overall structure of the logic and present in detail the rules particularly relevant to the semantics of variables. A complete presentation of the logic appears in [Demers82], and the rule numbers in this paper agree with the numbers used there.
In the next section, we discuss the underlying language principles needed to make an equational specification of variables possible. In the sections that follow, we present a logic that does so for Russell.
Language Principles
In designing Russell, we gave considerable thought to Backus's criticisms of "vonNeumann" languages [Backus78]. We were (and remain) convinced that any general-purpose programming language must incorporate some notion of variable and state. However, we were concerned that
We ought to be able to give proof rules for all of Russell. This concern has led us in two directions. Hans Boehm [Boehm82] has developed a Hoare-style proof system for the language.  In this paper we take a different approach to specifying the language -- an equational or algebraic theory.
The proof system should be small and yet treat the entire language. We did not want to restrict ourselves to "small, weak subsets of full vonNeumann languages that have states that are vastly simpler than real ones." [Backus78, p.618]
We feel that we have achieved both of these goals. Below we present the equational theory of Russell. It is small enough to fit on a few pages of text, yet we feel it provides the essential insights a programmer needs.
The development of an equational logic for Russell was significantly aided by two important design decisions. The first of these was to adopt the principle of type-completeness [Demers80]. Basically, type-completeness means
Every Russell expression has a type;
For any type in Russell there is an expression of that type; and
Any Russell expression can be parameterized with respect to any free identifier occurring in it to yield a function of a more complex type.
Because Russell is type-complete, it has a simple, clearly identifiable language core of combining forms and then a larger set of interchangeable parts. These interchangeable parts include the builtin types and, most importantly for our purposes, the operations on variables. In most programming languages variables can be manipulated by programs (they can be passed as arguments to procedures, for example) but the operations that manipulate them are not all part of the surface syntax of the language. Assignment usually is a named primitive operation, but other operations like variable allocation usually are not, making it impossible to define the semantics of variables using the same logic that defines the non-variable component of the language.
There are compelling reasons for this -- few languages have type structures rich enough to describe such operations as variable allocation. Type-completeness makes it possible for all the operations that manipulate variables in Russell to be named functions in the programming language. Making Russell type-complete allowed us to bring the operations on variables up to the surface, so that the same equational theory that defines the language core can also define the parts of the language that manipulate variables.
The other important design decision was to begin developing an equational proof system for Russell before the language design was frozen. While developing the equational system, we found places where critical properties of the operations on variables could not be expressed as equations among expressions of the language. Our decision to develop an equational specification had an interesting consequence -- instead of enriching an assertion language for describing Russell, we were forced to enrich the programming language itself. It seems to us that this is an important point. A good deal has been written about the need to develop a language and its proof rules simultaneously; the hope is that the language will be molded by the desire to keep its proof rules simple. The use of an equational system puts an interesting twist on this idea: the requirements of the proof rules may point out areas where the programming language should be made more expressive.
In the following section we describe the Russell language subset used in this paper. We then present the overall structure of our equational proof system, and discuss the most important inference rules. The complete set of rules is given in [Demers82]. Next we discuss proof rules for operations on simple variables. We give two sample proofs to convey the flavor of reasoning in the system. Finally, we give rules for composite variables (records) which show how their semantics are straightforward compositions of the semantics of their components.
The Programming Language
The language used below is a minor modification of Russell [Boehm80]. As we have already remarked, Russell is a type-complete language. It includes function- and type-valued expressions and treats them on an equal footing with more conventional expressions.
Russell is statically typed. As described below, the Russell logic includes rules by which we associate with each expression e a syntactic type specifier or signature S. The signature of e tells whether e denotes a value or a variable, and gives an expression for the type of e. Thus, a signature has the form "var exp" or "val exp" where, informally, "exp" must be a type-valued Russell expression. Formally, S is a legal signature iff the formula legal S is provable in the logic.
Expressions have a fairly conventional syntax. In the following description, variables beginning with p,q,...,x,y,z represent identifiers; variables beginning with d,...,h or T represent expressions; and those beginning with S represent signatures. A Russell expression may be any of:
An identifier or constant. Special identifiers such as int, bool and type, which are builtin types, and a number of builtin functions to be introduced below, are treated as constants that may not be redeclared.
A sequential composition, of the form ( e1; ... ; en )
A let-block, of the form let ... ; xi ~ di; ... in e ni
A conditional, of the form if e1 then e2 else e3 fi
A loop, of the form while e1 do e2 od
An application e0[e1, ..., en] of function e0 to arguments e1 through en.  When no confusion should arise we shall frequently write applications in infix rather than prefix notation.
A function type expression, of the form func[ ... ;xi : Si; ... ] S.  Intuitively, such an expression denotes the type of n-parameter functions, where x1 through xn are parameter names, S1 through Sn are the corresponding parameter signatures, and S is the result signature. For example, 
func[x: val int; y: val int] val int
is an expression for the type of the integer addition operation.
A function construction, of the form func t[ ... ;xi : Si ;... ] { e }  Such an expression denotes a function, where x1 through xn are parameter names and S1 through Sn are the corresponding parameter signatures as above; identifier t is a local name for the function, which allows it to call itself recursively;  and expression e is the function body. For example,
func square[x: val int]
{ if x<0 then square[-x] else if x>0 then square[x-1]+x+x-1 else 0 fi fi }
is an expression for an integer squaring function.
The Structure of the Logic
The first task in specifying the semantics of variables is to find a set of operations suitable for characterizing their behavior. What sort of behavior must be captured?
That one can assign to a variable and extract the value possessed by a variable.
That variables can alias -- two syntactically distinct variable-producing expressions in a program can produce semantically indistinguishable results.
That new variables can be allocated. This allocation does not change the value of any existing variable, nor does the new variable alias with any existing variable.
In Russell the operations of assignment and value extraction, the predicates that test for aliasing and the operation of allocating a new variable are all just particular builtin functions. Thus it seemed natural to apply the ideas of abstract data type specification, where semantics is given by a set of equations relating the results of function applications, to defining Russell. In doing so we encountered two problems not common to the usual equational specifications:
Russell expressions can have effects, as well as produce values -- that is the whole point of having variables in the language. Thus, the equations of our system must relate not only the values of expressions but also the effects of evaluating them. In a sense, one of the major problems in the development of an equational theory for Russell is the semantics of the ";" operator.
Equivalences between expressions may hold only in certain contexts. For example, the following equivalence is obviously valid:
(let x ~ 3 in y := 4; x ni ) W (y := 4; 3)
Here we have substituted the right-hand side of the declaration ("4") for the declared identifier ("y") within block body. On the other hand, consider
(let x ~ ValOf[y] in y := 4; x ni) W (y := 4; ValueOf[y])
Again we have just substituted the right-hand side of a declaration for the left-hand identifier.  However, this equivalence is clearly invalid. The equations of our system must include premises that allow the first substitution but disallow the second.
These constraints led us to a Gentzen-style deductive system having much in common with those of [Bates82] and [Martin-Lof79]. In the remainder of this section we present the basic structure of the system. In later sections we give the rules of inference that define our Russell subset.
Formulas
Our logic is basically an equational one -- formulas can have the form e1 W e2, where e1 and e2 are expressions of the programming language. However, to deal with the problems discussed above we need several other kinds of formulas. The formulas of our system include:
Typings. These are formulas of the form e: S, which assert that e is a legal Russell expression whose signature is S.
Legality Assertions. These are formulas of the form legal S, which assert that S is a legal signature -- S has the form var e or val e where e is a type-valued expression whose value is independent of the store.
Purity Assertions. These are formulas of the form pure e, which assert that expression e is independent of the values of any variables -- e neither has an observable effect nor produces a value that depends on the current state. An expression e is said to be pure if pure e holds. The notion of purity is an important one and is discussed at some length below.
Equivalences. These are formulas of the form e1 W e2, which assert that expressions e1 and e2 are completely equivalent -- that they have the same value and produce the same observable effects when evaluated. If exp is a Boolean expression we will sometimes abbreviate "exp W True" by "exp". Note that True is a pure, total expression -- its evaluation always terminates without error or observable effect -- so the equivalent expression exp must likewise be pure and total.
It is worth noting that the truth or falsity of any formula is independent of the store. For example, if e1 W e2 is true the expressions e1 and e2 may reference program variables but the two expressions must be equivalent independent of what values are possessed by those variables.
Environments
An environment G is a set of formulas  G = Q U F where Q is a set of typings in which only simple identifiers (not arbitrary expressions) may appear on the left hand sides, and F is set of equivalence formulas. When Q contains a typing (x: S) we say that Q (and hence G) defines x. G is closed if Q defines every identifier that occurs free in a formula of Q or F. All environments arising in correct proofs are closed.
Given G and a set of program identifiers x1 through xn, we may construct
G - {x1, ..., xn} =def U { G' | (G' I G) & (G' is closed) & (G' defines none of the xi) }.
i.e., the maximal closed subset of G not defining any of x1 through xn.
Less formally, this construction simply deletes from G definitions of x1 through xn and any formulas that depend on them. By construction G - {x1 , ... , xn} is closed, since an arbitrary union of closed environments is easily seen to be closed. Using the above construction, we define
(G, x1: S1, ..., xn: Sn) =def G - {x1 , ... , xn} U { x1: S1, ... , xn: Sn },
which gives the effect of declaring program identifiers on the environment -- first all references to previous instances of the identifiers are deleted from the environment, and then new typings are added. Note that (G, x1: S1, ..., xn: Sn) is closed if all free identifiers of S1 through Sn are among x1 through xn or are defined in G - {x1 , ..., xn}.
Similarly, we define G | {x1 , ..., xn}, the var restriction of G to x1 through xn, by
G|{x1, ..., xn} =def U { G' | (G' I G) & (G' is closed) & ((y: var T) B G' g Ei y = xi) }
This restricts G so that any free identifiers with var signature must be among x1 through xn.
Finally, we define
Gval =def G | {}
i.e., the restriction of G to no var identifiers (leaving only identifiers with val typings). This operation is useful because expressions that can be typed using only the information in Gval are guaranteed to be pure.
Goals
A goal G has the form
G p F
with the meaning that the formula F is a consequence of the typings and equivalences in G.
Inference Rules
An inference rule has the form
G1, ..., Gn
      G
with the meaning that from G1 through Gn we may conclude G. We call G the conclusion of the rule, and G1 through Gn its hypotheses or subgoals. We shall frequently abbreviate by allowing lists of formulas to appear in hypotheses and conclusions.  For example
G p (  F1, F2 )
G p (  F3, F4 )
is an abbreviation for the two rules
G p F1, G p F2
G p F3
and
G p F1, G p F2
G p F4
We also follow the convention that the variables t, u,..., z represent new identifiers, and that an expression of the form d[ ... ei / xi ... ] which represents the result of simultaneously substituting e1 through en for x1 through xn, is legal only if no capture occurs.
Theorems
The set of theorems is the smallest set of goals closed under deduction using the inference rules. This set is nonempty, since there are inference rules with no hypotheses.
Basic Rules
The system includes some logical rules stating obvious basic facts about equivalences and typings. Among them are assumption and modus ponens rules, rules stating reflexivity, transitivity and symmetry of W, and substitution rules that allow provably equivalent expression to be substituted for one another in equivalence formulas and typings. These rules are straightforward, and can be found in [Demers82].
The Russell subset we are using includes builtin types int and bool with the Boolean, arithmetic and comparison operators +, -, *, /, <, &, V, etc. These operations treat values rather than variables, and in a Hoare-style system there are equivalent, identically-named functions in the assertion language. To enable us to reason about terms that use these operators, we include all rules of the form
L10 (equivalent terms)
Q p (e1: T, e2: T)
G p e1 W e2
where
Q consists of the typings contained in G.
T is either int or bool,
Expressions e1 and e2 are equivalent terms using only the builtin int and bool operators mentioned above. Free identifiers are considered universally quantified.
These rules correspond roughly to the assumption "all true formulas in the assertion language are axioms" frequently made when discussing relative completeness of systems of proof rules -- cf. [deBakker80].
Using the complete set of rules from [Demers82], we can show that if e1 and e2 use only the bool operators listed above, and if
G p  e1 W e2
is provable, then
G p  (e1 , e2 ) W True
is provable, and so is
G p  e3 W True
whenever e3 is a bool term such that e1 , e2 tautologically implies e3.
Purity, Null Effect and Legality
In giving the semantics of a language in which expressions may have effects, it is necessary at times to limit the use of inference rules to only those subexpressions that are provably independent of state. For example, an equivalence such as
f[ e1 , e1, e2 ]  W  g[ e2 , e1 ]
must be provable only if the meanings of e1 and e2 are independent of the number of times they are evaluated and the order in which they are evaluated. We can guarantee this by requiring that e1 and e2 be pure -- intuitively, that evaluation of e1 or e2 neither depend on nor affect the value possessed by any variable. Thus, the logic includes purity assertions and a number of rules that allow us to deduce that expressions are pure. Purity assertions are perhaps the most novel aspect of this work, and they appear as hypotheses in many of the rules below.
Purity is not the same as freedom from side-effects. Consider the expression "ValOf [ x ]", which extracts the value possessed by variable x. This expression has no effect, but its value manifestly depends on the state; thus it is not pure.
Conversely, evaluation of a pure expression can have an effect, since it does not necessarily terminate without error. Thus the plausible null effect rule
(pure null effect (UNSOUND))
G p  ( ( e1; e2 ): S, pure  e1 )
G p  ( e1; e2 ) W e2
is unsound because it fails to account for possible abortion or nontermination in e1.  For example, it could be used to show
(1/0; 17)  W  17
which is clearly untrue because the erroneous division by zero occurs in the left side of the equation but not the right.
Since a pure expression is independent of the state, its effect must be the same -- abortion, nontermination, or no effect -- every time it is evaluated. Similarly, the value of a pure expression, if it has a value, must be the same every time it is evaluated. In short, a pure expression may be evaluated any number of times, provided it is evaluated at least once.  The two rules
P1 (pure idempotence)
G  p  e: S, pure e
G  p  e W ( e; e )
and
P2 (pure reordering)
G p  ( e1: S1, e2: S2, e3: S3)
G p  pure e1 
G p  (e1; e2; e3) W (e2; e1; e3)
capture this behavior. Note that only one of two expressions being reordered needs to be pure.  In the rules below, a hypothesis of the form
G  p pure e
appears whenever the rule's conclusion involves moving or duplicating (but not entirely eliminating) subexpression e.
Purity Rules
Below are the rules by which one deduces purity of expressions. One of the attractive points of Russell is that there is a large class of syntactically identifiable pure expressions. The following two rules illustrate this. Intuitively, they state that any identifier is pure and that any type-correct Russell expression that imports no var identifiers and does not produce a var result is pure.
P3 (identifier purity)
G  p  x: S
G  p  pure x
P4 (value purity)
Gval  p  e: val T
G  p  pure e
Rule P4 is surprisingly powerful. Although it requires a proof of pure e to begin in an environment without var typings, it does not prohibit introduction of var typings in proofs of the subgoals. Thus, the rule can be used to prove that an expression is pure even if the expression allocates variables, provided it does not refer to variables from the surrounding context.
P5 (substitution purity)
G p  (e1 W e2, pure e1)
G p  pure e2
This rule allows us to prove an expression is pure even if it violates the simple syntactic characterization of purity given in the previous two rules, by proving it equivalent to another expression known to be pure.
In addition to the above rules, there are rules that allow us to deduce purity of composite expressions. These rules can be found in [Demers82]. For the most part they are straightforward -- they merely state that composite expressions are pure if their components are, and that function type expressions and function constructions are pure unconditionally. For applications the purity rule is more subtle, however.
P12 (application purity)
G p  ( ..., ei: val Ti, ..., f[ ..., ei, ... ]: val T )
G p  ( pure f, ..., pure ei, ... )
G p  pure f[ ..., ei, ... ]
This rule states that an application is pure if the function and argument expressions are pure and neither the arguments nor the result are variables. Although this rule may seem weak at first glance, it is the strongest rule one could hope for in general. Applications that take var arguments or produce var results may be impure even though all their subexpressions are pure -- value extraction and variable allocation, both of which are obviously impure, are simple examples of this.
Applications of certain builtin functions may be pure even though they violate the rather stringent hypotheses of rule P12 above. For these functions there are special application purity rules. Some of these rules appear below; the remaining ones may be found in [Demers82].
Null Effect Rules
We have argued that our rules cannot allow a pure expression to be discarded even if its value is never used. However, there are a number of Russell constructs whose evaluation is guaranteed to terminate without error or observable effect, and such expressions can safely be discarded when their values are unused. For each such expression e there is a special null effect rule of the form
(null effect rule scheme)
G p  (e1; e2 ): S
G p  (e1; e2 ) W e2 
The most general of these rules is
P13 (identifier null effect)
G  p (x; e): S
G  p (x; e)  W  e
which allows us to discard evaluation of an identifier if the value is not subsequently used.
There are also null effect rules for function types and function constructions:
P14 (func type null effect)
G  p (func[ ... ; xi: Si; ... ] S ; e): S'
G  p (func[ ... ; xi: Si; ... ] S ; e) W e
P15 (func construction null effect)
G  p (func f[ ... ; xi: Si; ... ] {e}; e'): S'
G  p (func f[ ... ; xi: Si; ... ] {e}; e') W e'
These rules state that building a function type or a function value in Russell has no effect.  Of course, they say nothing about the effect of subsequently applying the function -- there can be no general null effect rule for applications, since this depends on the details of the function body. A number of the builtin functions are guaranteed to terminate without error or effect if their arguments do. There is a separate null effect rule for each such function.
There are no specific rules for proving that a composite expression has no effect if its components have none; however, such facts are provable in the system.
Signature Legality Rules
Earlier we remarked informally that a signature var e or val e is legal only if e is a type expression whose value is independent of the store.  We now have the mechanism to make this remark formal:
S1 (signature legality)
G p (T: val type, pure T)
G p (legal var T, legal val T)
Recall that evaluation of a pure expression does not necessarily terminate without error.  Thus, for example, the above rule allows  a legal signature to contain a nonterminating type expression.  This is generally acceptable.  We could easily eliminate it by adding to the rule  the additional hypothesis
G p (T; True) W True
which precludes nontermination or abortion of T.  This approach is taken in the discussion of records below, as it simplifies the presentation of the rules.
Composite Expressions
Earlier we described the rules by which we may deduce that a composite expression is pure. We shall also require signature rules for composite expressions, which allow us to deduce that expression e is type-correct by proving a formula of the form e: S. Finally, we shall require rules allowing us to deduce equivalences between composite expressions. The most important of the composite expression rules are discussed below; the remaining ones can be found in [Demers82].
The simplest signature rule is the one for sequential composition:
S2 (; signature)
G p (e1: S1, ..., en: Sn )
G p ( e1 ; ... ; en ): Sn
Basically, this rule states that a composite expression is type-correct if all its subexpressions are. Most of the other signature rules are similar, and may be found in [Demers82]. The signature rules for applications and let-blocks are more interesting, however, as they embody the "signature calculus" rules of [Boehm80].
The signature rule for function applications is as follows:
S3 (application signature)
G p f: val func[ ...; xi: Si; ... ] S
G p ( ... , ei: Si[ ... ej / xj ... ], ... )
G p legal S[ ... ej / xj ... ]
G p f[ ... , ei , ... ]: S[ ... ej / xj ... ]
The subgoals and conclusion of this rule involve simultaneous substitution of the argument expressions ei for the corresponding parameter names xi. These substitutions enable the rule to deal with type-valued parameters. For example, let p be the polymorphic identity function
func p[ t: val type; x: val t] { x }
so that
p: val func[ t: val type; x: val t ] val t
For the (type-correct) application
p[int, 17]
The second and third subgoals of the function signature rule are instantiated as
G p int: val type[ int, 17/t, x ]
G p 17: val t[ int,17/t, x ]
G p legal val t[ int, 17/t, x ]
or, equivalently,
G p int: val type
G p 17: val int
G p legal val int
These allow the conclusion
G p p[ int, 17 ]: val int
as desired.
The signature rule for let-blocks can be developed from the application signature rule. Following Landin's "principle of correspondence" [Landin66], we expect the expression
let ... ; xi: Si ~ ei; ... in d ni
to be type-correct iff the application
f [ ..., ei, ... ]
is type-correct, where f has signature
func [ ...; xi: Si; ... ] S
and S is the signature of the block body d. The rule
S4 (let signature)
(G, ..., xi: Si, ...) p d: S
G p ( ..., ei: Si[... ej / xj ...], ... )
G p legal S[... ej / xj ...]
G p let ...; xi: Si ~ ei; ... in d ni: S[ ... ej / xj ... ]
follows quite directly.
The remaining composite expression rules are those that allow us to deduce equivalences. A few of these rules are described below; a complete list appears in the [Demers82]. The most interesting and, for our purposes, the most important of the rules are the ones dealing with let-blocks, function applications and conditionals.
Most of the let rules are used to rename bound identifiers, to rearrange the components of a let-block, or to combine a block with an adjacent expression. For example, the rule
C6 (let absorption (right))
G p let ... ; xi ~ di; ... in e1 ni: S1 
(G - {... xi ...} ) p  e2: S2
G p let ... ; xi ~ di ; ... in e1 ni; e2  W let ... ; xi ~ di; ... in e1; e2 ni
allows an expression e2 to be "absorbed" into a let-block from the right. The requirement that e2 can be typed with an environment from which the new identifiers xi have been eliminated ensures that capture cannot occur.
The following two rules allow let-blocks to be introduced and eliminated.
C8 (let elimination (a))
G p let x ~ d in e ni: S
G/{x} p e: S
G p let x ~ d in e ni W (d; e)
This rule states that a binding that is never referred to may be eliminated.
C9 (let elimination (b))
G p e: S
G p let x ~ e in x ni W e
In neither of these rules is there any requirement that the subexpressions be pure.
The most complex of the let rules is the following substitution rule:
C10 (let substitution)
G p  let ... ; xi : Si ~ di ; ... in e ni: S
... 
(G, ... , xi: Si ... ) p let ... ; xi : Si ~ di ; ... in gj ni W let ... ; xi : Si ~ di; ... in hj ni
(G, ... , xi: Si ... ) p pure gj, pure hj
...
(G, ... , xi: Si ... ) U { ... , gj W hj, ... } p e W e'
G p let ... ; xi: Si ~ di ; ... in e ni W let ... ; xi: Si ~ di; ... in e' ni
When the number of gi-hi pairs is zero, this rule specializes to the obviously sound rule:
C10.1 (let equivalence)
G p let ... ; xi: Si ~ di; ... in e ni: S
(G, ... , xi: Si ... ) p e W e'
G p let ... ; xi: Si ~ di ; ... in e ni W let ...; xi: Si ~ di; ... in e' ni
Informally, gi W hi can be used as a predicate describing the bound values; so the general form of the rule allows us to use knowledge of the bound values in proving the equivalence of e and e'. For example, letting g1 be x1 and h1 be d1, we can derive the following extremely useful rule:
C10.2 (pure b-conversion)
G p  (let x1: S1 ~ d1; ... in e ni: S, pure d1 )
G p  let x1: S1 ~ d1; ... in e ni W let x1: S1 ~ d1; ... in e[d1 / x1] ni
provided no capture occurs. This derived rule is related to the b-conversion rule of the lambda calculus.
Two important rules give the meaning of function application:
C18 (application argument evaluation)
G p d[ ..., ei, ... ]: S
G p d [ ..., ei, ... ] W let x ~ d; ... ; yi ~ ei ; ... in x[ ..., yi, ... ] ni
This rule states that argument evaluation may be done by let-binding; thus, the rule implies that parameters are passed by value, and that argument evaluation proceeds from left to right.
C19 (application meaning)
G p  (func p[ ...; xi: Si ; ... ]{ e })[ ..., ei, ... ]: S
G p (func p[ ... ; xi : Si ; ... ]{ e })[ ..., ei, ... ]
W let p ~ (func p[ ...; xi: Si; ... ]{ e });... ; xi ~ ei; ... in e ni ni
The binding for p in the right hand side of the conclusion is necessary in case e calls p recursively. If there are no recursive calls, this binding can be eliminated using the let-elimination rule (C8) and the func construction null effect rule (P15). 
Another important class of rules define conditional expressions. These include a signature rule, absorption rules analogous to the let absorption rules above, and a condition evaluation rule similar to application argument evalutation.
There are also three if elimination rules:
C13 (if elimination (true))
G p if True then e2 else e3 fi: S
G p if True then e2 else e3 fi W e2 
C14 (if elimination (false))
G p if False then e2 else e3 fi: S
G p if False then e2 else e3 fi W e3 
C15 (if elimination (parallel))
G p if e1 then e2 else e2 fi: S
G p if e1 then e2 else e2 fi W ( e1 ; e2 )
The most complex of the if rules is:
C16 (if substitution)
G p if e1 then e2 else e3 fi: S
G p pure e1
G U {e1 W True} p e2 W d2
G U {e1 W False} p e3 W d3
G p if e1 then e2 else e3 fi W if e1 then d2 else d3 fi
Like let substitution (C10), this rule introduces new equivalences into the environments of its subgoals, making it possible to use knowledge of the truth or falsity of the condition in proving properties of subexpressions e1 and e2. As we illustrate below, the if substitution and parallel if elimination rules can be used together to perform case analysis in the system.
The Semantics of Variables
In Russell, the operations that manipulate variables are generally components of data types. Each builtin type T includes the components:
:= : func[var T ; val T] val T
ValOf : func[var T] val T
New : func[ ] var T
These operations perform assignment, value extraction and allocation for variables of type T. The rules below specify precisely how they behave. We give the rules for the builtin type int, but essentially the same rules hold for all builtin types, including composite types such as arrays and records. Similar rules are expected to hold for user-defined types as well. However, one must be somewhat careful here. The fact that a user-defined type happens to have a New operation with the right signature does not mean that it will necessarily obey these rules -- there is nothing in the name of an operation that prescribes its semantics.
Assignment and Value Extraction
The first step in specifying the semantics of variables is to give rules relating the effects and values produced by assignment and value extraction. These include
V1 (:= value (left))
G p ( e1 := e2 ): val int
G p pure e1
G p ( e1 := e2 ) W ( e1 := e2 ; ValOf[ e1 ] )
V2 (:= value (right))
G p ( e1 := e2 ): val int
G p pure e2
G p ( e1 := e2 ) W ( e1 := e2 ; e2 )
These two rules give the value of assignment expressions: the value produced is the value of the right hand side and the value of the right hand side becomes the value produced by ValOf after the assignment.
P16 (ValOf null effect)
G p e1: var int
G p e2: S
G p ( ValOf [ e1 ] ; e2 ) W (e1; e2)
This rule gives the effect of ValOf -- it has none.
V3 (:= annihilation)
G p ( e := e1 ): val int
G p ( e := e2 ): val int
G p ( pure e , pure e2 )
G p (e := e1; e := e2) W (e1; e := e2)
V4 (self :=)
G p ( e := ValOf[ e ] ): val int
G p pure e
G p e := ValOf[e] W ValOf[e]
These two rules give the effect of assignment. Rule V3 states that if two successive assignments are made to the same variable, only the second one can be noticed. The "pure e2" premise to the rule guarantees that the value of e2 does not depend on the prior value of the variable. Rule V4 states that assigning the value of a variable to itself has no effect.
Aliasing
The next step in developing a specification of variables is to give rules that describe when variables share storage. To do so in an equational system we must add several new builtin functions to the programming language:
alias, contains, disjoint:
val func [T1, T2: val type] val func[x:var T1, y: val T2] val bool
Informally, alias[T1,T2][e1 ,e2 ] is true if the expressions e1 and e2 evaluate to the same variable; contains[T1,T2][e1 ,e2 ] is true if the expression e1 evaluates to a variable that contains e2 as a component, so that changing the contents of variable e1 will change the contents of e2, while changing the contents of e2 will change a component of the contents of e1. Finally, disjoint[T1,T2][e1 ,e2 ] is true if no changes to the contents of e1 will affect the contents of e2 and vice versa. Formally, these functions are related by inference rules given below.
As mentioned earlier, we feel it is important that our attempt to develop an equational specification of Russell pointed out areas in which the language needed to be made more expressive. The alias, contains and disjoint predicates were introduced to make an equational description of the language possible; but after some consideration they began to seem natural and potentially quite useful in ordinary programming. For example, a program that manipulates large arrays can use them to test whether an efficient in-place algorithm can be used or copying is required.
The following inference rules define alias, contains and disjoint:
V5 (alias definition)
G p  ( e1: var T1, e2: var T2)
G p  ( pure e1 , pure e2 )
G p alias[T1,T2][ e1 , e2 ] W (contains[T1, T2][ e1 , e2 ] & contains[T2, T1][ e2 , e1 ])
V6 (disjoint definition)
G p ( e1: var T1, e2: var T2)
G p ( pure e1 , pure e2 )
G p disjoint[T1,T2][ e1 , e2 ] W (contains[T1, T2][ e1 , e2 ] & contains[T2, T1][ e2 , e1 ])
These two rules define alias and disjoint in terms of contains: two variables alias if each contains the other, and two variables are disjoint if neither contains the other.
P17 (contains purity)
G p contains[T1, T2][ e1 , e2 ]: val bool
G p ( pure e1 , pure e2 )
G p pure contains[T1, T2][ e1 , e2 ]
P18 (contains null effect)
G p (contains[ T1, T2][x1 , x2 ] ; e): S
G p (contains[ T1, T2][x1 , x2 ] ; e) W (T1; T2; e)
V7 (contains transitivity)
G p ( x1: var T1, x2: var T2, x3: var T3)
G p (contains[T1, T2][ x1 , x2 ] & contains[T2, T3][ x2 , x3 ]) g
contains[T1, T3][ x1 , x3 ] W (T1; T2; T3; True)
V8 (contains reflexivity)
G p x: var T
G , F p contains[T,T][x,x] W (T;True)
V9 (nonoverlap)
G p ( ... , xi: var Ti, ... )
G p ((contains[T1, T0][x1 , x0 ] & contains[T2 , T0][x2 , x0 ]) g
contains[T1, T2][x1 , x2 ] V contains[T2, T1][x2 , x1 ])) W (T0; T1; T2; True)
V10 (acyclic)
G p ( x1: var T, x2: var T)
G p contains[T1, T2][x1 , x2 ] W contains[T2, T1][x2 , x1 ]
These rules give the essential properties of contains. Rule P17 states that an application of contains is independent of the store if its arguments are; similarly, by rule P18 an application of contains has no observable effect if the argument evaluations have none. Rules V7 and V8 state the obvious facts that containment is transitive and reflexive. Rule V9 states that variables do not overlap -- if two variables contain anything in common, then one of the two variables must contain the other. Finally, rule V10 is a well-foundedness requirement, stating that a variable cannot be properly contained in another variable of the same type.
The following three rules give the semantic import of the alias, contains and disjoint tests in the programming language.
V11 (alias equivalence)
G p ( e1: var T, e2: var T)
G p  ( pure e1 , pure e2 )
G p alias[T, T][ e1 , e2 ] W True
G p e1 W e2
This rule states that two variables that alias are completely indistinguishable. Note the hypotheses "pure e1" and "pure e2" are essential and are not implied by purity of "alias[T, T][ e1, e2 ]" -- e1 and e2 might be impure but have effects that exactly cancel one another. For example, one can prove that 
alias[ int,int ] [(x := ValOf[x]+1 ; y),(x := ValOf[x]-1; y)]
is pure and equivalent to True even though the subexpressions
x := ValOf[x] - 1
are obviously impure.
V3a (:= annihilation (generalized))
G p ( x := e1 ): val T1
G p ( e := e2 ): val T2
G p contains[T2,T1][e,x] W True
G p ( pure e , pure e2 )
G p( x := e1 ; e := e2 ) W ( e1; e := e2 )
This rule states that an assignment to variable e hides the effect of a previous assignment to x if e contains x. As in the annihilation rule given earlier, the purity hypotheses are necessary to ensure that neither e nor e2 depends on the previous value of x.
V12 (reordering)
G p ( ... , xi: var Ti, ... )
G p ( ... , yj: var Yj , ... )
G p ( ... , disjoint[Ti, Yj ][xi , yj ], ... )
(G | ...xi ...) p e1: S1
(G | ... yj ...) p e2: S2
G p e3: S3
G p  (e1; e2; e3 ) W ( e2 ; e1; e3 )
This rule allows us to conclude that the effects of two expressions do not interfere with one another, so that the expressions may be evaluated in either order. The hypotheses require that the free var identifiers of e1 are among x1 through xn, the free var identifiers of e2 are among y1 through yn, and all x's are disjoint from all y's. There is no requirement that the x's or y's themselves be pairwise disjoint, as this is not necessary to show that e1 and e2 do not interfere.
Variable Allocation
We can now give the rules that define the allocation function for variables of type int:
V13 (New disjoint)
G p e: var T
G p disjoint[int,T][New[ ], e] W ( T; e; True)
P19 (New null effect)
G p e: S
G p ( New[ ]; e ) W e
V14 (New inaccessible)
G p e: S
G p New[ ] := e W   e
These three rules give the important properties of the value and effect of New -- a new variable is disjoint from any other variable, and allocating or even assigning to a new variable has no observable effect. There is no rule stating that New is pure -- it is not pure, since it produces a new variable each time it is invoked. However, as noted above, it may be possible in the system to prove that an expression is pure even if it creates new variables, provided it does not use any variables from the surrounding context. For example, one can use the value purity rule (P4) to show that the expression
let x: var int ~ New[ ] in x:=17 ni
is pure; and, with some manipulation, one can use the New inaccessible rule (V14) to show that it is equivalent to the constant 17.
Note that the above rules leave many things unsaid about variables in Russell. They do not specify an implementation, but only the observable characteristics of variables in programs. Variable allocation may be done using a stack or a heap; the definition of New is insensitive to such implementation decisions. The operations of assignment or value extraction could have "benevolent side-effects" [Hoare72] like garbage collection; the only obligation is that after an assignment the only variable to yield a new value is the one to which the assignment was made.
Two Examples
To demonstrate the use of our equational system, we give two substantial examples.
A Derived Rule
Our first example illustrates how case analysis can be performed within the system. We shall prove the following derived inference rule:
G p (x1 := e1: val T, x2 := e2: val T)
G p (pure e1 , pure e2 )
G p (T; True) W True
G p (x1 := e1; x2 := e2; ValOf[x1]) W
(x1 := e1; x2 := e2; if disjoint[T,T][x1 , x2] then e1 else e2 fi)
Intuitively this rule is true because two variables of the same type are either disjoint or alias -- they cannot overlap, nor can one of them properly contain the other.
The proof of this derived rule proceeds as follows. Using disjoint definition (V6), contains null effect (P18), and if elimination (C15), we show
x1 := e1; x2 := e2; ValOf[x1] W 
disjoint[T,T][x1; x2]; x1 := e1; x2 := e2; ValOf[x1] W
if disjoint[T,T][x1 , x2] then (x1 := e1; x2 := e2; ValOf[x1])
else (x1 := e1; x2 := e2; ValOf[x1]) fi
Next, using if substitution (C16) with subgoals
G U {disjoint[T,T][x1 , x2]} p (x1 := e1; x2 := e2; ValOf[x1]) W (x1 := e1; x2 := e2; e1)
G U {ndisjoint[T,T][x1 , x2]} p (x1 := e1; x2 := e2; ValOf[x1]) W (x1 := e1; x2 := e2; e2)
(which are discussed below) we obtain
W if disjoint[T,T][x1; x2] then (x1 := e1; x2 := e2; e1) else (x1 := e1; x2 := e2; e2) fi
from which we can obtain the desired result using if absorption rules.
The first of the two subgoals is straightforward, since the assumption that x1 and x2 are disjoint allows the assignment expressions to be reordered. The second subgoal is a bit more complicated. Using disjoint definition (V6) and the hypothesis that
disjoint[T,T][x1 , x2] W False
we obtain, after some manipulation,
contains[T,T][x1 , x2] V contains[T,T][x2 , x1] W True
Using contains acyclic (V10) we can show the two disjuncts on the left hand side are equivalent. After more manipulation this leads to
(contains[T,T][x1 , x2] & contains[T,T][x2 , x1]) W alias[T,T][x1 , x2] W True
Now that x1 and x2 have been shown to alias, the desired result follows directly.
A Simple Procedure
As a second example of the use of our system, we consider a theorem presented in [Cartwright78]. Let SWAP represent the Russell expression
func swap[y1 , y2: var int] val int
{ let t ~ New[] in t := ValOf[y2]; y2 := ValOf[y1]; y1 := ValOf[t] ni }
which is a standard function for swapping the values of two variables. We would like to show that swap works correctly whether or not x1 and x2 are disjoint -- roughly speaking, we would like to prove something analogous to the Hoare-style correctness formula
{ x1 = a1 & x2 = a2 } swap[x1 , x2] { x2 = a1 & x1 = a2 }
Since the formulas of our system are equivalences between programming language expressions, we cannot even state precisely this formula. What we can show is that for any G from which there are deductions
G p (x1: var int, x2: var int)
G p (e1: val int, e2: val int)
G p (pure e1 , pure e2 )
G p swap W SWAP
there is also a deduction
G p (x1 := e1; x2 := e2; swap[x1 , x2]) W (x2 := e1; x1 := e2 )
This equivalence formula appears similar to the Hoare formula, and a proof of it should convince the reader that calling swap actually does exchange the values of the arguments. However, the two formulas really are technically quite different. For example, if x1 and x2 are aliased, the Hoare formula
{ x1 = 11 & x2 = 17 } swap[x1 , x2] { x2 = 11 & x1 = 17 }
holds because the precondition cannot possibly be satisfied; the equivalence
(x1 := 11; x2 := 17; swap[x1 , x2]) W (x2 := 11; x1 := 17 )
holds because 17 is stored over 11 on both sides. The similar equivalence
(x1 := 11; x2 := 17; swap[x1 , x2]) W (x1 := 17; x2 := 11 )
does not hold when x1 and x2 are aliased.
The proof (of the true equivalence) proceeds as follows. Using substitution we can show the left hand side of the desired result is equivalent to
(x1 := e1; x2 := e2; SWAP[x1 , x2])
By application meaning (C19) this is equivalent to
(x1 := e1; let y1 ~ x1; y2 ~ x2 in ... (body of SWAP) ... ni)
Using the derived b-conversion rule (C10.2), let elimination (C8) and identifier null effect (P13) y1 and y2 can be eliminated to yield
(x1 := e1; x2 := e2; let t ~ New[] in t := ValOf[x2]; x2 := ValOf[x1]; x2 := ValOf[t] ni)
Now let motion can be used to convert this to
(let t ~ New[] in x1 := e1; x2 := e2; t := ValOf[x2]; x2 := ValOf[x1]; x1 := ValOf[t] ni)
(A use of let renaming may be required here to avoid capture of free variables of e.)
At this point we invoke the let substitution rule in its full generality. We first prove the subgoal
let t ~ New[] in disjoint[int,int][t, xi] ni W let t ~ New[] in True ni
which is straightforward; we then prove
(G, t: var int) U { disjoint[int,int][t, xi] } p  
(x1 := e1; x2 := e2; t := ValOf[x2]; x2 := ValOf[x1]; x1 := ValOf[t]) W
(t := e2; x2 := e1; x1 := e2 )
This subgoal is more substantial than the first. It is fairly straightforward to transform the left side to
(t := e2; x1 := e1; x2 := e2; x2 := ValOf[x1]; x1 := e2 )
At this point we perform a case analysis. Just as in the previous example, we obtain one case in which
disjoint[T,T][x1 , x2] W True
and another case in which
alias[T,T][x1 , x2] W True
The first case can be dealt with easily by reordering the assignments to x1 and x2. The second case can be handled just as easily by using := annihilation (V3) to eliminate the unwanted assignments.
From the two major subgoals above, let substitution (C10) allows us to conclude that the original expression is equivalent to
let t  ~ New[] in t := e2; x2 := e1; x1 := e2 ni
This is easily transformed to
let t ~ New[] in t := e2 ni; x2 := e1; x1 := e2
from which the let block can be eliminated using argument evaluation (C18) and New inaccessible (V14). This gives us the desired equivalence.
Structured Variables
The set of operations used above for simple variables forms the basis of the characterization of composite variables like records or arrays. Below we present the definition of records in Russell; arrays can be treated by a similar approach.
A Russell expression for a record type has the form
record ( f1 : T1; ...; fn : Tn )
This is a slight simplification of the actual Russell syntax -- in particular, recursively defined types are not allowed -- but it will suffice for our purposes. Such an expression denotes a record type with fields f1 through fn of types T1 through Tn respectively. We shall use the signature rule
S9 (record type signature)
G p ( ..., legal val Ti, (Ti; True) W True, ... )
G p record ( ...; fi : Ti; ... ): val type
The hypotheses of this rule demand that the expressions for the types of the fields (T1 through Tn) be pure and free of side effects. While not strictly necessary, this restriction considerably simplifies the rules below; without it the conclusions of the rules would have to contain additional occurrences of the Ti with no purpose other than to ensure soundness of the rules in the face of erroneous or nonterminating type expressions.
P20 (record type purity)
G p record ( ...; fi : Ti; ... ): val type
G p pure record ( ...; fi : Ti; ... )
P21 (record type null effect)
G p record ( ...; fi : Ti; ... ): val type
G p (record ( ...; fi : Ti; ... ); e) W e
These are standard purity and null effect rules, reflecting the fact that constructing a record type value is independent of the store and terminates without error.
For this section, we let
RR =def record ( ...; fi : Ti; ... )
be a fixed record type expression. Associated with RR are the usual operations of assignment, value extraction and variable allocation:
:= :  func[var RR; val RR] val RR
ValOf :  func[var RR] val RR
New :  func[] var RR
In addition, there are constructor and field selector functions:
Mk :  func[val T1; ...; val Tn] val RR
f1l :  func[val RR] val T1
f1r :  func[var RR] var T1
...
fnl :  func[val RR] val Tn
fnr :  func[var RR] var Tn
In Russell, function names can be overloaded -- two or more functions can have the same name -- as long as they have different types so they can be disambiguated. Thus, the identifying subscripts "l" and "r" on the field names are technically unnecessary. We retain them below for clarity.
To specify the meaning of the record type constructor, we must give meanings for each of the above operations. These meanings are defined in terms of the operations for the types Ti. In the rules that follow, we use the notation Ti$:=, Ti$ValOf and Ti$New for the assignment, value extraction and allocation functions for variables of type Ti.
Construction and field selection for record values are described by two simple rules: 
V15 (record val selection)
G p ( ..., xi: val Ti, ... )
G p fil [ Mk[..., xj, ...] ] W xi
V16 (record val construction)
G p (e: val RR, pure e)
G p Mk[..., fil[e], ...] W e
These are the simple McCarthy rules for the LISP constructors [McCarthy60] restated in Russell terms. The additional rule
V17 (record var selection)
G p (e: val RR, pure e)
G p ValOf[e] W Mk[..., Ti$ValOf[fir[e]], ...]
shows how the var and val field selection functions relate to one another. Note that the identity
fil[ ValOf[e] ] W Ti$ValOf[ fir[e] ]
follows immediately from rules V14 and V17.
The next few rules describe the aliasing behavior of the fields of record variables.
V18 (field new)
                    
G p fir[New[]] W Ti$New[]
This rule states that a field selected from a new record variable is indistinguishable from a new variable of the field type. Thus, by new disjoint (V13), the fields of new records are disjoint from all existing variables.
V19 (field disjoint)
G p (e: val RR, pure e)   
G p disjoint[Ti, Tj][fir[e], fjr[e]] W True
for all i = j. This rule states that the fields of a record variable are disjoint from one another. Note this fact is not a consequence of the preceding rule.
V20 (field containment (a))
G p ( e1: var U, e2: var RR )
G p ( pure  e1 , pure e2 )
G p contains[U,RR][e1, e2] W ... & contains[U, Ti][e1, fir[e2]] & ...
This rule states that a record variable contains all of its fields, and that it contains nothing else -- any variable that contains all the fields contains the record.
V21 (field containment (b))
G p ( e1: var RR, e2: var U )
G p ( pure  e1 , pure e2 )
G p contains[RR,U][e1, e2] W alias[RR,U][e1, e2] V ... contains[Ti, U][fir[e1], e2] ...
This rule states that there is nothing between a record and its fields -- a variable that is contained in a record either aliases with the entire record or is contained in one of the fields.
Finally, there are purity and null effect rules for the val and var field selector functions. The var rules
P22 (field purity (var))
G p (fir[e]: var Ti, pure e)
G p pure fir[e]
P23 (field null effect (var))
G p (fir[e]; g): S
G p (fir[e]; g) W (e; g)
may appear strange at first glance, but they are both sound and reasonable -- even though a var field selector function is passed a variable as an argument, it neither examines nor modifies the value possessed by that variable.
As an extended example, we illustrate that the obviously sound rule
G p (x := e: val RR, pure e)
G p x := e W Mk[..., fir[x] := fil[e], ...]
can be derived from the above rules. Beginning from x := e, we first use  field containment (V20) and := annihilation (V3) to show
x := e W (...; fir[x] := fil[e]; ...); x := e
we then use record val construction (V16) to obtain
W (...; fir [x] := fil [e]; ... ); x := Mk[... , fil [e] , ...]
By argument evaluation (C18) this becomes
W (...; fir [x] := fil [e]; ... ); let ...; ti ~ fil[e]; ... in Mk[..., ti, ...] ni
Using let motion rules -- note that e is pure and thus commutes with any expression -- we obtain
W let t1 ~ f1l[e]; ...; tn-1 ~ fn-1l[e]; tn ~ ( ...; fir[x] := fil[e]; ...; fnl[e] ) in Mk[..., ti, ...] ni
It is easily shown that
(fnr[x] := fnl[e]; fnl[e] ) W (fnr[x] := fnl[e] )
Using this fact and let motion n times we can reduce the above expression to
W let ...; ti ~ (fir[x] := fil[e] ); ... in Mk[..., ti, ...] ni
which by argument evaluation (C18) finally reduces to
Mk[...; (fir[x] := fil[e] ); ...]
as desired.
Conclusions
In this paper we have presented an equational theory for Russell and argued that
It presents a useful mathematical specification of variables in Russell, and
This sort of equational theory can be construed to cover all of even a very rich language like Russell.
The equational logic presented here is certainly not a complete replacement for a conventional Hoare-style system. Most importantly, there are no induction principles to allow proofs of general properties of program correctness. Theorems in this system can give the final results of program execution for particular inputs; but statements such as "for any integer n, this program computeds n!" are outside its scope. On the other hand, the fact that it is always possible to deduce the result of a terminating computation in the system argues that it gives a complete specification of variables; and this form of specification is a particularly pithy way to get across important properties of the programming language to potential users. In particular, there are components of the Russell equational theory that present the language better than any of our attempts at informal description. When writing the informal description of Russell and explaining the language to others, we often found that describing New as  "allocating a new variable" was inadequate; moreover, the "operational" description of New conflicted with our desire to present a "mathematical" characterization of the language. It is far more edifying to give inference rules such as
G p e: var T
G p disjoint[int , T][int$New[] , e] W (T; e; True)
and
G p e: S
G p ( New[]; e ) W e
which say very clearly that New produces a result that is disjoint from any other variable, and that applying New has no other effect.
In addition, as we noted above, the process of producing the equational theory led us to make some important changes in the language. It was only when we began to work on the theory that we found the need to introduce alias, contains and disjoint into the programming language. We now consider these operations to be perfectly natural and potentially quite useful.
References
[Backus78]
Backus, J. Can programming be liberated from the vonNeumann style? A functional style and its algebra of programs. CACM 21 (1978), pp. 612-641.
[Bates82]
Bates, J. and R. Constable. The definition of mprl. TR-82-492, Department of Computer Science, Cornell University, 1982.
[Boehm80]
Boehm, H., A. Demers and J. Donahue. An informal description of Russell. TR-80-430, Department of Computer Science, Cornell University, 1980.
[Boehm82]
Boehm, H. A logic for expressions with side-effects. Proceedings Ninth Symposium on Principles of Programming Languages (1982), pp. 268-280.
[Cartwright78]
Cartwright, R. and D. Oppen. Unrestricted procedure calls in Hoare's logic. Proceedings Fifth Symposium on Principles of Programming Languages (1978), pp. 131-140.
[deBakker80]
J. deBakker. Mathematical Theory of Program Correctness. Prentice-Hall, 1980.
[Demers80]
Demers, A. and J. Donahue. Type completeness as a language principle. Proceedings Seventh Symposium on Principles of Programming Languages (1980), pp. 234-244.
[Demers82]
Demers, A. and J. Donahue. An equational theory for Russell. TR-82-534, Department of Computer Science, Cornell University, 1982.
[Dijkstra72]
Dijkstra, E. Notes on structured programming. In Dahl, O-J., E.W. Dijkstra and C.A.R. Hoare, Structured Programming, Academic Press, 1972.
[Guttag78]
Guttag, J. and J. Horning. The algebraic specification of data types. Acta Informatica 10 (1978), pp. 27-52.
[Hoare72]
Hoare, C.A.R. Proofs of correctness of data representations. Acta Informatica 1 (1972), pp. 271-281.
[Landin66]
Landin, P.J. The next 700 programming languages. CACM 9 (1966).
[Martin-Lof79]
Constructive mathematics and computer programming. Sixth International Congress for Logic, Methodology and Philosophy of Science, Hanover, Germany (1979).
[McCarthy60]
McCarthy, J. Recursive functions of symbolic expressions and their computation by machine, part I. CACM 3 (1960), pp. 184-195.
Appendix
L1 (assumption)
          
G p F
for any formula F B G.
L2 (modus ponens (typing))
G p x: S
G U {x: S} p F
G p F
L3 (modus ponens (equivalence))
G p e1 W e2
G U {e1 W e2} p F
G p F
These rules allow any provable typing or equivalence to be added to G for making further deductions.
L4 (reflexivity)
G p e: S
G p e W e
L5 (symmetry)
G p e1 W e2
G p e2 W e1
L6 (transitivity)
G p e1 W e2
G p e2 W e3
G p e1 W e3
These three rules state that W is an equivalence relation.
L7 (typing substitution (left))
G p e1: S
G p e1 W e2 
G p e2: S
L8 (typing substitution (right))
G p e1 W e2 
G p d: S[ e1 / t ]
G p d: S [ e2 / t ]
L9 (equivalence substitution)
(G, x: S) p e: S'
G/x p legal S'
G p e1: S
G p e1 W e2
G p e [ e1 / x ] W e [ e2 / x ]
The second hypothesis of rule L9 guarantees that the identifier x being substituted for does not occur free in the signature of e.
L10 (equivalent terms)
Q p (e1: T, e2: T)
G p e1 W e2
where
Q consists of the typings contained in G.
T is either int or bool,
Expressions e1 and e2 are equivalent terms using only the builtin int and bool operators mentioned above. Free identifiers are considered universally quantified.
P1 (pure idempotence)
G  p  e: S, pure e
G  p  e W ( e ; e )
P2 (pure reordering)
G p  ( e1: S1, e2: S2, e3: S3)
G p  pure e1 
G p  (e1; e2; e3) W (e2; e1; e3)
P3 (identifier purity)
G  p  x: S
G  p  pure x
P4 (value purity)
Gval  p  e: val T
G  p  pure e
P5 (substitution purity)
G p  (e1 W e2, pure e1)
G p  pure e2
P6 (; purity)
G p ( ... , pure ei , ... )
G p pure ( ... , ei ; ... )
P7 (let purity)
G p let ... ; xi ~ di ; ... in e ni: S
G p ( ... , pure di , ... )
(G, ... xi: Si , ... ) p pure e
G p pure let ... ; xi ~ di ; ... in e ni
P8 (if purity)
G p if e1 then e2 else e3 fi: S
G p (pure e1, pure e2, pure e3 )
G p pure if e1 then e2 else e3 fi
P9 (while purity)
G p while e1 do e2 od: S
G p (pure e1 , pure e2 )
G p pure while e1 do e2 od
P10 (func type purity)
G p func[ ... ; xi : Si ; ... ] S: val type
G p pure func[ ... ; xi : Si ; ... ] S
P11 (func construction purity)
G p func f[ ... ; xi : Si ; ... ] { e }: S
G p pure func f[ ... ; xi : Si ; ... ] { e }
P12 (application purity)
G p  ( ..., ei: val Ti, ..., f[ ..., ei, ... ]: val T )
G p  ( pure f, ..., pure ei, ... )
G p  pure f[ ..., ei, ... ]
P13 (identifier null effect)
G  p (x; e): S
G  p (x; e)  W  e
P14 (func type null effect)
G  p (func[ ... ; xi: Si; ... ] S ; e): S'
G  p (func[ ... ; xi: Si; ... ] S ; e) W e
P15 (func construction null effect)
G  p (func f[ ... ; xi: Si; ... ] {e}; e'): S'
G  p (func f[ ... ; xi: Si; ... ] {e}; e') W e'
P16 (ValOf null effect)
G p e1: var int
G p e2: S
G p ( ValOf [ e1 ]; e2 ) W (e1; e2)
P17 (contains purity)
G p contains[T1, T2][ e1 , e2 ]: val bool
G p ( pure e1 , pure e2 )
G p pure contains[T1, T2][ e1 , e2 ]
P18 (contains null effect)
G p (contains[ T1, T2][x1 , x2 ] ; e): S
G p (contains[ T1, T2][x1 , x2 ] ; e) W (T1; T2; e)
P19 (New null effect)
G p e: S
G p ( New[ ]; e ) W e
P20 (record type purity)
G p record ( ...; fi : Ti; ... ): val type
G p pure record ( ...; fi : Ti; ... )
P21 (record type null effect)
G p record ( ...; fi : Ti; ... ): val type
G p (record ( ...; fi : Ti; ... ); e) W e
P22 (field purity (val))
G p fil [e]: val Ti
G p pure e
G p pure fil[e]
P23 (field null effect (val))
G p (fil[e]; g): S
G p (fil [e]; g) W (e; g)
C1 (let renaming)
G p let ... ; xi ~ di ; ... in e ni: S
G p let ... ; xi ~ di ; ... in e ni W let ... ; ti ~ di[... tj / xj ...]; ...  in e[... tj / xj ...] ni
C2 (let reordering)
G p let t1 ~ d1; t2 ~ d2; in e ni: S
G p let t1 ~ d1; t2 ~ d2; in t1 ni W let t2 ~ d2; t1 ~ d1; in t1 ni
G p let t1 ~ d1; t2 ~ d2; in t2 ni W let t2 ~ d2; t1 ~ d1; in t2 ni
G p let t1 ~ d1; t2 ~ d2; in e ni W let t2 ~ d2; t1 ~ d1; in e ni
C3 (let absorption (left))
G p  e: S
G p  let x1 ~ d1; ... in e' ni: S'
G p  (e; let x1 ~ d1; ... in e' ni) W let x1 ~ (e; d1); ... in e' ni
C4 (let motion)
G p  (e; d1) W let t ~ d1 in e; t ni
G p  let x1 ~ d1; x2 ~ (e; d2);   in e' ni: S'
G p  let x1 ~ d1; x2 ~ (e; d2); in e' ni W let x1 ~ (e; d1); x2 ~ d2; in e' ni
C5 (let absorption (center))
(G/... xi ... ) p e: S
G p  let ...; xi ~ di; ... ; xn ~ (e; dn) in e' ni: S'
G p  let ...; xi ~ di; ... ; xn ~ (e; dn) in e' ni W let ...; xi ~ di; ...; xn ~ dn in d; e' ni)
C6 (let absorption (right))
G p let ... ; xi ~ di ; ... in e1 ni: S1 
(G - {... xi ...} ) p  e2: S2
G,F p let ... ; xi ~ di ; ... in e1 ni; e2  W let ... ; xi ~ di; ... in e1; e2 ni
C7 (let nesting)
G p let ... ; xi ~ di; ...; yj ~ ej; ... in e ni: S
(G/... xi ...) p ( ... , ei: Si, ... )
G p let ...; xi~di; ... yj~ej; ... in e ni W let ...; xi~di; ... in let ... yj~ej; ... in e ni ni
C8 (let elimination (a))
G p let x ~ d in e ni: S
G/{x} p e: S
G p let x ~ d in e ni W (d; e)
C9 (let elimination (b))
G p e: S
G p let x ~ e in x ni W e
C10 (let substitution)
G p  let ... ; xi : Si ~ di ; ... in e ni: S
... 
(G, ... , xi: Si ... ) p let ... ; xi : Si ~ di; ... in gj ni W let ... ; xi : Si ~ di; ... in hj ni
(G, ... , xi: Si ... ) p  pure gj , pure hj
...
(G, ... , xi: Si ... ) U { ... , gj W hj, ... } p e W e'
G p  let ... ; xi: Si ~ di ; ... in e ni W let ... ; xi: Si ~ di; ... in e' ni
C10.1 (let equivalence)
G p  let ... ; xi: Si ~ di; ... in e ni: S
(G, ... , xi: Si ... ) p e W e'
G p  let ... ; xi: Si ~ di ; ... in e ni W let ...; xi: Si ~ di; ... in e' ni
C10.2 (pure b-conversion)
G p  let x1: S1 ~ d1; ... in e ni: S
G p pure d1
G p  let x1: S1 ~ d1; ... in e ni W let x1: S1 ~ d1; ... in e[ d1 / x1 ] ni
C11 (if absorption)
G p  if e1 then e2  else e3 fi ; e4: S
G p  (if e1 then e2  else e3 fi ; e4 ) W if e1 then (e2 ; e4)  else (e3 ; e4) fi
C12 (if condition evaluation)
(G/x) p  if e1 then e2  else e3 fi: S
(G/x) p  if e1 then e2  else e3 fi W let x ~ e1 in if x then e2 else e3 fi ni
C13 (if elimination (true))
G p if True then e2 else e3 fi: S
G p if True then e2 else e3 fi W e2 
C14 (if elimination (false))
G p if False then e2 else e3 fi: S
G p if False then e2 else e3 fi W e3 
C15 (if elimination (parallel))
G p if e1 then e2 else e2 fi: S
G p if e1 then e2 else e2 fi W ( e1 ; e2 )
C16 (if substitution)
G p if e1 then e2 else e3 fi: S
G p pure e1
G U {e1 W True} p e2 W d2
G U {e1 W False} p e3 W d3
G p if e1 then e2 else e3 fi W if e1 then d2 else d3 fi
C17 (while meaning)
G p  while e1 do e2 od: val bool
G p  while e1 do e2 od W if e1 then e2; while e1 do e2 od else False fi
C18 (application argument evalutation)
G p d[ ..., ei, ... ]: S
G p d [ ..., ei, ... ] W let x ~ d; ... ; yi ~ ei ; ... in x[..., yi, ...] ni
C19 (application meaning)
G p  (func p[ ...; xi: Si ; ... ]{ e })[ ..., ei, ... ]: S
G p (func p[ ... ; xi : Si ; ... ]{ e })[ ..., ei, ... ] 
	W let p ~ (func p[ ...; xi: Si; ... ]{ e });... ; xi ~ ei; ... in e ni ni
S1 (signature legality)
G p (T: val type, pure T)
G p (legal var T, legal val T)
S2 (; signature)
G p (e1: S1, ..., en: Sn )
G p ( e1 ; ... ; en ): Sn
S3 (application signature)
G p f: val func[ ...; xi: Si; ... ] S
G p ( ... , ei: Si[ ... ej / xj ... ], ... )
G p legal S[ ... ej / xj ... ]
G p f[ ... , ei , ... ]: S[ ... ej / xj ... ]
S4 (let signature)
(G, ..., xi: Si, ...) p d: S
G p ( ..., ei: Si [ ... ej / xj ... ], ... )
G p legal S [ ... ej / xj ... ]
G p let ...; xi: Si ~ ei; ... in d ni: S[ ... ej / xj ... ]
S5 (if signature)
G p  e1: val bool
G p  e2: S , e3: S
G p  if e1 then e2  else e3 fi: S
S6 (while signature)
G p  e1: val bool
G p  e2: S
G p  while e1 do e2 od: val bool
S7 (func type signature)
(G, ... xi: Si , ... ) p ( ... , legal Si , ... , legal S )
G p  func[ ... ; xi : Si ; ... ] S: val type
S8 (func construction signature)
G p  legal val func[ ... ; xi: Si; ...] S
(Gval, f: val func[ ... ; xi: Si; ...] S, ... , xi: Si , ...) p e: S
G p func f[ ... ; xi: Si ; ...] { e }: val func[ ... ; xi: Si; ...] S
S9 (record type signature)
G p ( ..., legal val Ti, (Ti; True) W True, ... )
G p record ( ...; fi : Ti; ... ): val type
V1 (:= value (left))
G p ( e1 := e2 ): val int
G p pure e1
G p ( e1 := e2 ) W ( e1 := e2 ; ValOf[ e1 ] )
V2 (:= value (right))
G p ( e1 := e2 ): val int
G p pure e2
G p ( e1 := e2 ) W ( e1 := e2 ; e2 )
V3 (:= annihilation)
G p ( e := e1 ): val int
G p ( e := e2 ): val int
G p ( pure e , pure e2 )
G p ( e := e1 ; e := e2 ) W ( e1 ; e := e2 )
V3a (:= annihilation (generalized))
G p ( x := e1 ): val T1
G p ( e := e2 ): val T2
G p contains[T2,T1][e,x] W True
G p ( pure e , pure e2 )
G p( x := e1 ; e := e2 ) W ( e1; e := e2 )
V4 (self :=)
G p ( e := ValOf[ e ] ): val int
G p pure e
G p e := ValOf[e] W ValOf[e]
V5 (alias definition)
G p  ( e1: var T1, e2: var T2)
G p  ( pure e1 , pure e2 )
G p alias[T1,T2][ e1 , e2 ] W (contains[T1, T2][ e1 , e2 ] & contains[T2, T1][ e2 , e1 ])
V6 (disjoint definition)
G p ( e1: var T1, e2: var T2)
G p ( pure e1 , pure e2 )
G p disjoint[T1,T2][ e1 , e2 ] W (contains[T1, T2][ e1 , e2 ] & contains[T2, T1][ e2, e1 ])
V7 (contains transitivity)
G p ( x1: var T1, x2: var T2, x3: var T3)
G p (contains[T1, T2][ x1 , x2 ] & contains[T2, T3][ x2 , x3 ]) g
contains[T1, T3][ x1 , x3 ] W (T1; T2; T3; True)
V8 (contains reflexivity)
G p x: var T
G p contains[T,T][x,x] W (T;True)
V9 (nonoverlap)
G p ( ... , xi: var Ti, ... )
G p ((contains[T1, T0][x1 , x0 ] & contains[T2 , T0][x2 , x0 ]) g
contains[T1, T2][x1 , x2 ] V contains[T2, T1][x2 , x1 ])) W (T0; T1; T2; True)
V10 (acyclic)
G p ( x1: var T, x2: var T)
G p contains[T1, T2][x1 , x2 ] W contains[T2, T1][x2 , x1 ]
V11 (alias equivalence)
G p ( e1: var T, e2: var T)
G p  ( pure e1 , pure e2 )
G p alias[T, T][ e1 , e2 ] W True
G p e1 W e2
V12 (reordering)
G p ( ... , xi: var Ti, ... )
G p ( ... , yj: var Yj , ... )
G p ( ... , disjoint[Ti, Yj ][xi , yj ], ... )
(G | {... xi ...}) p e1: S1
(G | {... yj ...}) p e2: S2
G p e3: S3
G p  (e1; e2; e3 ) W ( e2 ; e1; e3 )
V13 (New disjoint)
G p e: var T
G p disjoint[int,T][New[ ], e] W ( T; e; True)
V14 (New inaccessible)
G p e: S
G p New[ ] := e W e
V15 (record val selection)
G p ( ..., xi:  val  Ti, ... )
G p fil [ Mk [..., xj, ...] ] W xi
V16 (record val construction)
G p (e: val RR, pure e)
G p Mk [... , fil[e], ...] W e
V17 (record var selection)
G p (e: val RR, pure e)
G p ValOf[e] W Mk[..., Ti$ValOf[fir[e]], ...]
V18 (field new)
                    
G p fir[New[]] W Ti$New[]
V19 (field disjoint)
G p (e: val RR, pure e)   
G p disjoint[Ti, Tj][fir[e], fjr[e]] W True
V20 (field containment (a))
G p ( e1: var U, e2: var RR )
G p ( pure  e1 , pure e2 )
G p contains[U,RR][e1 , e2] W ... & contains[U, Ti][e1, fir[e2]] & ...
V21 (field containment (b))
G p ( e1: var RR, e2: var U )
G p ( pure  e1 , pure e2 )
G p contains[RR,U][e1, e2] W alias[RR,U][e1, e2] V ... contains[Ti, U][fir[e1], e2] ...
�ÊL«–
"blueandwhite" style˜Ititleš
œ;˜;Iauthor˜KL˜c
headš
œ˜Ibodyš
œ±˜±Nš
œï˜ïNš
œ˜Iitemš
œ~˜~Oš
œª˜ªNš
œÎ
˜Î
—š
œ˜Nš
œ�˜�Oš
œ£˜£Oš
ϐ
˜ê
Nš
œÚ
˜Ú
NšœŸ
Ïeœ/˜ß
Oš
œ$˜$Oš
œ@˜@Oš
œ‹
˜‹
Nš
œñ˜ñNš
œ…˜…Nšœ°�œ6�œ¸˜ÄNš
œ¦˜¦—š
œ˜Nš
œ�˜�Nš	œ�
�	œ‘
Ïbœ
žœzžœ˜âNš
œœ˜œOšœ�
œ�œžœžœžœ‰
˜Ò
Ošœ�œÏd
œ	Ÿ
œ˜6Ošœ�	œžœŸ
œŸ
œžœž˜7Ošœ�œžœŸ
œ
žœŸ
œ
žœŸ
œ
ž˜3Ošœ�œžœŸ
œ
žœŸ
œ
ž˜%Ošœ�œŸ
œŸ
œŸ
œŸ
œŸ
œ
Ÿ
œn˜¶
šœ�
œžœŸ
œŸ
œ^Ÿ
œ
Ÿ
œŸ
œ
Ÿ
œY˜ Iexamplešžœžœžœž˜$Icontinuationš
œ@˜@—šœ�œžœ
Ÿ
œŸ
œ=Ÿ
œ
Ÿ
œŸ
œ
Ÿ
ρ
˜íPšžœ
žœžœ
žœžœžœžœ
žœžœžœžœ
žœ˜bQš
œ2˜2——š
œ˜Nš
ϻ
˜ª
Ošœ
�œ�œ˜POšœ�œ~˜–
Ošœ�	œ�
˜¤
Nš
œÚ˜ÚNš
œü˜üNš
œ~˜~Pš	œ
žœžœžœÏm
œ˜*Qš
œ–
˜–
Pš	œ
žœžœžœ 
œ˜9Qš
œý
˜ý
Nš
œž˜žš
ž˜NšœHŸ
œ
 
œŸ
œ	Ÿ
œŸ
œ­
˜ŒOš�œn˜uOš�œ!žœ?žœžœO˜Ó
Oš�œ!žœÕ
žœY˜èOš�œ"Ÿ
œ
 
œŸ
œ!Ÿ
œŸ
ϵ
 
ς
˜ÚNšœjŸ
œ
 
œŸ
œŸ
œŸ
œˆ
˜š—š
ž˜Nš"œ�œ
Ïg
œ¡œ¡
œ
 
¡œ¡
œy¡
œ&¡
œ&¡
œ¡
œ�œ¡
œ�œ¡
œ;¡
œ¡
œ8˜£Nšœ¡
œ#Ÿ
œ
Ÿ
œ˜HPš¡
œ
Ïl
œŸ
œŸ
œŸœ
 
œ¡
œ¡
œ 
œ
¡
œ 
œ¡
œ
 
œ¡
œŸ
œ˜ZQšœ#¡
œŸ
œ
Ÿ
œ
˜GNšœ5¡
œŸ
œ
Ÿ
œ7¡
œ
¢
œŸ
œ
Ÿ
œ�
˜�Pšœ
¡
œŸ
œŸ
œŸ
œŸ
œŸœ
¡
œ
¢
œŸ
œ
Ÿ
œ 
œŸ
œŸ
œ	Ÿ
œŸ
œ˜MQšœÙ
¡
œŸ
œŸ
œŸ
œŸ
œ(Ÿ
œ
Ÿ
œŸ
œ
Ÿ
œ¡
œ
¢
œŸ
œ	Ÿ
œ˜áNšœ¡
œŸ
œ	Ÿ
œžœ
�œ¡
œŸ
œ
Ÿ
œ˜VPš#¡
œŸ
œŸ
œŸœ
 
œ¡
œ¡
œ 
œ
¡
œ 
œ¡
œ
 
œžœ 
¡œ 
œ
 
œŸ
œ˜YQš	œ¡
œ#žœŸ
œ
Ÿ
œ
˜]Nš
œ˜Pš¡
ŸœŸœ
¡
œ˜Qš
œ¡
œžœ,žœh¡
Ÿœ˜Ú
—š
ž˜Nš
œ˜Pš¡
œ
 
œ˜QšœX¡
œ
˜Z—š
ž˜Nš
œ˜PšÏz
Ðdz
£¤
˜Pš
œ˜QšœŸ
œ
Ÿ
œ"�
œŸ
œ
Ÿ
œ�
œ�œt˜‚PšÐgz
£
Ðmz
£¤
£¤
£˜Pš¡
œ
 
œŸ
œŸ
œ˜Qš
œ$˜$Pš¥
£
¦
£¤
£¥
£
¦
£¤
˜Pš¡
œ
 
œŸ
˜Qš
œ˜Pš¥
£
¦
£¤
£¥
£
¦
£¤
˜Pš¡
œ
 
œŸ
˜Nš
œƒ
Ÿ
œŸ
œCŸ
œ
Ÿ
œŸ
œ
Ÿ
œ%˜�—š
ž˜Nšœ�œ™
˜¬
——š
ž˜Nšœr�
œ�œ�œ�œ�œ 
œ�œ¸
˜˜Nšœ7žœžœC 
œ 
œ 
œ‚˜�š
œ˜Pš¥
£
¦
£¤
£¤
£˜Pš	¡
œ
 
œŸ
œ
 
œŸ
˜—Qš
œ˜Oš¡
œ&¡
œ
˜)Ošœžœžœ
˜Oš	œ
Ÿ
œŸ
œ-žœžœS˜¡
Qš
œÎ
˜Î
NšœFŸ
œŸ
œžœ˜Pš	¡
œ
 
œŸ
œ
 
œŸ
˜Qš
œ˜Pš¡
œ
 
œŸ
œ
Ïq
œŸ
œ 
œ˜Qš
œ˜Pš¡
œ
 
œŸ
œ
 
œ˜Qš
œ
Ÿ
œžœŸ
œ
§
œŸ
œŸ
œ
˜G—š
ž ˜ Nš
Ϙ
˜ò
Pš
œÐdg
Ϭ
œŸ
œ 
œŸ
Ϭ
œ˜!Qšœ*¨
œŸ
œ�
¨
œŸ
œ�œ%¨
œŸ
œ²˜¯Nš
œð
˜ð
NšœŠ
�œ˜š
š
œ˜Pš¥
£
¦
£¤
£¤
£Ðbz£¤
£˜ Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
˜—QšœSŸ
œ(˜|Pšœ 
œ˜Qš
œy˜yNšœÇ�&œ˜ýš
œ˜Pš¥
£¦
£©£˜Pš¡
œ 
œ 
œ	˜—Qš
œ˜š
œ˜Pš¡
œ
 
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ
˜Pš¥
£
¦
£©£¤
œ
˜
Pš¡
œ
 
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ
˜ —Qš
œŒ
˜Œ
Pš¡
œ 
œ
žœ˜Qš
œu˜uš
ž˜NšœÑžœ$žœ˜‹š
œ˜Pš¥
£¦
£˜
Pš¡
œ 
œžœ˜—š
œ˜Pš¥
¤£¦
£©£˜Pš¡
œ 
œžœ˜—Qšœlžœ/žœÔ
˜õš
œ˜Pš¥
£
¦
£¤
£
¦
£¤
£©£Ñdgz
¥
˜Pš¡
œ
 
œžœŸ
˜—Qš
ϯ
˜Ø
Nš
œŸ˜Ÿš
œ˜Pš¡
œ
 
œ
Ÿ
œžœŸ
œŸ
œ	žœ˜7Pš
¥
£
¦
£©£	©£¤
£˜"Pš¡
œ
 
œžœ
Ÿ
œ˜—Nšœc�2œƒ
žœžœ²
˜æNš
œ’˜’—š
ž˜Nšœ�œá
�œa�œ˜…š
œ˜Pš¥
£
¦
£¤
£¤
£˜Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
œ
˜—Nš
œ"˜"š
œ˜Pš¥
£¦
£
˜Pš¡
œ 
œ	 
œ˜—Qš
œ]˜]Nš
œO˜Ošœžœ˜Pš
¥
£¦
£©£	¤
£¤
£˜*Pš¡
œ 
œžœ	Ÿ
œŸ
œ 
œ˜*—šœžœ˜#Pš
¥
£¦
£©£¤
£¤
£˜.Pš¡
œ 
œžœŸ
œŸ
œ 
œ˜/—Qš
œÑ˜ÑNš
œž
˜ž
—š
ž˜Nšœ0žœžœŠ
˜Æ
˜Pš¥
£
¦
£©£©£˜Pš¡
œ
 
œž	œž	œ˜—N˜±Pš¡
œ
 
œ 
œ˜Q˜œ
——š
ž˜Nšœq�œØ˜ØN˜B˜Pš¥
£
¦
£¤
£¤
£¤
£¤
£˜Pš	¡
œ
 
œŸ
œ
Ÿ
œŸ
˜—Qšœß
žœb˜ÄN˜;˜Pš
¡
œ
 
œžœŸ
œŸ
œ	˜%Pš¡
œ
 
œ
Ÿ
œŸ
œŸ
œŸ
œ
˜,Pš
¥
£
¦
£
©£	¤
£¤
£˜Pš
¡
œ
 
œŸ
œŸ
œŸ
œ˜-—NšœhŸ
œ(Ÿ
œ‚
˜”Pšžœž	œžœ	˜$Q˜Pš	œžœž	œžœžœ˜*Q˜"Pšœžœ˜
Q˜PPš
¡
œ
 
œ
žœžœžœ˜!Pš¡
œ
 
œžœžœ
˜Pš
¡
œ
 
œ
žœ
žœžœ˜Q˜Pš¡
œ
 
œ
žœž˜Pš¡
œ
 
œžœ
ž˜Pš	¡
œ
 
œ
žœ
žœ
ž˜Q˜Pš	¡
œ
 
œžœžœ
ž˜Q˜Nšœžœ“
˜­
PšžœŸ
œŸ
œŸ
œžœž˜"Q˜&Pšœ
Ÿ
œ˜Q˜&Pšžœ	Ÿ
œŸ
œ	˜Q˜4šœžœ˜Pš	œ
¡
œŸ
œŸ
œ 
œ˜Pš¡
œ
 
œ	Ÿ
œŸ
œŸ
œŸ
œ˜)Pš
¥
£
¦
£
©£¤
£¤
£˜Pš¡
œ
 
œ
žœŸ
œŸ
œŸ
œžœžœ
Ÿ
œŸ
œ˜;—Q˜Nšœ”žœ0˜ÇNšœžœNžœP˜°
šœžœ˜Pš¡
œ
 
œ
žœŸ
œŸ
œžœŸ
œ
žœŸ
œ
˜(Pš£
¥
£
Ðlz
£¤
£¦
£¤
£¤
˜Pš!¡
œ
 
œ
žœŸ
œŸ
œžœŸ
œ
žœŸ
œ 
œ
žœŸ
œŸ
œžœŸ
œŸ
œ
ž˜O—Qš	œŸ
œžœ-Ÿ
œBŸ
œ8˜Ü
Nšœžœ(˜Išœžœ˜Pš
¡
œ
 
œ
žœžœžœ˜Pš¥
£¦
£˜Pš¡
œ
 
œ
žœžœžœ
 
œ˜—Q˜Lšœžœ˜Pš¥
£
¦
£˜Pš¡
œ
 
œ
žœžœžœ
 
œ˜—Q˜SNšœžœ�œ˜Ešœžœ˜š¡
œ
 
œžœŸ
œŸ
œŸ
œžœžœ˜,P˜—Pš&œ
¡
œ	Ÿ
œŸ
œ 
œ
žœŸ
œŸ
œŸ
œžœŸ
œ
žœ
 
œ
žœŸ
œŸ
œŸ
œžœŸ
œ
ž˜ešœ
¡
œ	Ÿ
œŸ
œ 
œ
žœŸ
œžœŸ
˜)P˜—Pš£
¥
£	¤
£¤
£¦
£
¤
£
¦
£¤
£¦
£¦
£˜8Pš¡
œ
 
œ
žœŸ
œŸ
œŸ
œžœž 
œ
žœŸ
œŸ
œŸ
œžœž˜M—QšœŸ
œŸ
œB˜Zšœžœ
˜Pš¡
œ
 
œ
žœŸ
œŸ
œŸ
œžœžœ˜)Pš£
¥
£	¤
£¤
£¦
£¦
£˜Pš¡
œ
 
œ
žœŸ
œŸ
œŸ
œžœž 
œ
žœŸ
œŸ
œŸ
œžœž˜L—Nšœ
Ÿ
œ
 
œŸ
Ϯ
Ÿ
œŸ
œŸ
œŸ
œ4˜¡šœ¡
œ˜Pš¥
£
¦
£©£¤
£¤
£¤
£©£©£©£¤£
˜0Pš ¡
œ
 
œžœŸ
œŸ
œŸ
œžœž 
œ
žœŸ
œŸ
œŸ
œžœŸ
œŸ
œž˜I—Qšœ@¡
œ(˜iN˜=˜%Pš¥
£
¦
£
¤
£
˜Pš¡
œ
 
œŸ
œ 
œ
žœŸ
œŸ
œžœ
Ÿ
œž˜O—Qšœ9žœ˜»
˜Pš¥
£
¦
£©£
¤
£¤
£¤
£
˜:Pš¡
œ
 
œžœŸ
œŸ
œŸ
œ 
œ
žœžœ
Ÿ
œŸ
œŸ
œŸ
œžœž˜‚
—Qšœ±
žœžœ&˜ý
Nšœƒ
žœe˜ë
Nšœžœ˜*šœžœ˜Pš¥
£
¦
£
©£©£¤
£
©£¤
£
©£˜!Pš¡
œ
 
œ
žœžœŸ
œ
žœŸ
œ
žœ
 
œŸ
œ
˜$—šœžœ˜Pš¥
£
¦
£
©£©£¤
£
©£¤
£
©£˜"Pš¡
œ
 
œ
žœžœŸ
œ
žœŸ
œ
žœ
 
œŸ
œ
˜%—šœžœ˜Pš¥
£
¦
£
©£¤
£
©£¤
£
©£¤
£
©£˜Pš¡
œ
 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
žœ
 
œŸ
œŸ
œ˜*—Nšœžœ
˜$šœžœ˜Pš¡
œ
 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
žœ˜Pš¡
œ
 
œ
žœŸ
˜Pš¡
œ
 
œŸ
œ
 
œ 
œŸ
œ
 
œŸ
˜Pš¥
£
¦
£¤
£
¦
£¦
£¤
£
¦
£¤
˜Pš ¡
œ
 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
ž 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
ž˜7—QšœžœØ
Ÿ
œŸ
œžœžœO˜ô—š
ž˜N˜‰
Oš	œžœ
žœžœžœ˜Ošœžœ
žœžœ˜Ošœžœžœ˜Qšœ¸
žœÃ˜þš
ž˜N˜£
˜Pš¡
œ
 
œŸ
œŸ
œžœ
ž˜Pš¥
£
¦
£
©£¤
˜Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ˜-—˜Pš¡
œ
 
œŸ
œŸ
œžœ
ž˜Pš¥
£
¦
£
©£¤
˜Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ˜$—N˜Ï
˜Pš	¡
œ
 
œŸ
œžœ
ž˜Pš¥
£
¦
£¤
£˜	Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
œŸ
œ
˜$—N˜3˜Pš	¡
œ
 
œ	Ÿ
œžœ
ž˜Pš	¡
œ
 
œ	Ÿ
œžœ
ž˜Pš
¥
£
¦
£©£©£¤
£˜Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
œŸ
œ
˜&—˜Pš¡
œ
 
œžœ
ž˜ Pš¥
£
¦
£
©£˜
Pš¡
œ
 
œ 
œ	˜—Nšœä
Ÿ
œƒ
˜è—š
ž˜N˜Ý
˜PšžœŸ
œŸ
œžœ
žœžœžœŸ
œžœŸ
œ
ž	˜B—Qš/œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ*Ÿ
œŸ
œŸ
œŸ
œŸ
œ(Ÿ
œ<Ÿ
œŸ
œ"Ÿ
œ-Ÿ
œŸ
œŸ
œŸ
œŸ
œ-ŸœŸ
œ�
œG˜µN˜·N˜B˜Pš¡
œ
 
œŸ
œžœŸ
œŸ
œžœŸ
œ
˜Pš¥
£
¦
£©£¤
£©£¤
£˜Pš ¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ˜Y—˜Pš¡
œ
 
œŸ
œžœŸ
œŸ
œžœŸ
œ
˜Pš¥
£
¦
£©£¤
£©£¤
£˜Pš ¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ˜\—N˜­
˜Pš
¡
œ
 
œŸ
œŸ
œŸ
œŸ
œž˜)Pš
¥
£
¦
£©£¤
£	¤
£˜Pš¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ˜$—˜Pš¥
£
¦
£
¤
£¤
£¤
£¤
£
˜(Pš¡
œ
 
œ
Ÿ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œ˜3—˜Pš¥
£
¦
£¤
£¤
£¤
£¤
£¤
£
˜)Pš(¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ˜r—˜Pš¥
£
¦
£	˜Pš¡
œ¡
œ
 
œ 
œ	˜%—˜Pš¥
£
¦
£
©£¤
£˜š¡
œ
 
œ
Ÿ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
˜APšœ
Ÿ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ˜N——˜
Pš
¥
£
¦
£¤
£©£©£˜Pš¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ˜;—N˜ƒN˜y˜Pš¡
œ
 
œŸ
œžœŸ
œžœ˜Pš¡
œ
 
œžœŸ
œžœŸ
œ˜Pš
¥
£
¦
£¤
£¤
£¦
£˜!Pš	¡
œ
 
œŸ
œ
 
œŸ
˜—NšœlŸ
œ
Ÿ
œ�œ%Ÿ
œŸ
œŸ
œŸ
œc˜³Pšœžœ
žœ/˜=Q˜=Pšœ 
œ˜Q˜˜#Pš	¡
œ
 
œ	Ÿ
œžœŸ
˜Pš	¡
œ
 
œ	Ÿ
œžœŸ
˜Pš
¡
œ
 
œŸ
œŸ
œ 
œ˜Pš
¥
£
¦
£©£©£¤
£˜Pš¡
œ
 
œŸ
œ	Ÿ
œ 
œŸ
œŸ
œ˜*—Nšœß
Ÿ
œ$˜„˜Pš
¡
œ
 
œ
Ÿ
œžœŸ
œ˜Pš¡
œ
 
œ
Ÿ
œžœ˜Pš
¡
œ
 
œŸ
œŸ
œŸ
œ˜.Pš
œ
¡
œŸ
œ 
œŸ
œŸ
˜Pš
œ
¡
œŸ
œ 
œŸ
œŸ
˜Pš¥
£
¦
£¤
£¤
˜
Pš¡
œ
 
œŸ
œŸ
œŸ
ž
œ 
œŸ
œŸ
œŸœ
˜$—NšœÆ
žœŸ
œŸ
œ
Ÿ
œžœŸ
œŸ
œ
Ÿ
œ�
Ÿ
œŸ
œ˜â—š
ž˜NšœTžœ
˜X˜Pš¥
£
¦
£©£˜Pš¡
œ
 
œ
žœ 
œ˜.—˜Pš¥
£
¦
£˜Pš¡
œ
 
œ 
œ˜—˜Pš¥
£
¦
£˜Pš¡
œ
 
œ
 
œ˜—Nšœ†�œÕ˜ÞPšžœžœ
žœž˜#Q˜ƒ
—Nš
œ´˜´—š
ž˜N˜Rš
ž˜N˜ˆ
Pš¡ 
œŸ
œŸ
œžœŸ
œŸ
œžœ˜&Pš¡ 
œžœŸ
œžœŸ
œ˜Pš¥¦
£¦
£˜Pš'¡ 
œŸ
œŸ
œŸ
œŸ
œ	Ÿ
œ 
œŸ
œŸ
œŸ
œŸ
œ
žœŸ
œŸ
œžœŸ
œ
žœŸ
œ
žœ
˜hQ˜©
Nšœtžœ˜‘
Pš
œ
Ÿ
œŸ
œŸ
œŸ
œ	Ÿ
œ 
œ
˜ PšœŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ	Ÿ
œ 
˜6PšžœŸ
œŸ
œžœŸ
œŸ
œŸ
œŸ
œ	Ÿ
œžœŸ
œŸ
œŸ
œŸ
œ	Ÿ
œž˜fQšœžœ!˜/Pš¡ 
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ	Ÿ
œ 
œŸ
œŸ
œŸ
œŸ
œŸ
œ
˜YPš!¡ 
œ 
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ	Ÿ
œ 
œŸ
œŸ
œŸ
œŸ
œŸ
œ
˜Z	˜%Pš! 
œ
žœŸ
œŸ
œžœŸ
œŸ
œŸ
œŸ
œŸ
œžœŸ
œŸ
œŸ
œŸ
œŸ
œž˜Y—Qšœ2žœ˜FNšœMŸ
œŸ
ϴ
˜ú
PšœŸ
œŸ
œ 
œ˜Q˜#Pš
œŸ
œŸ
œ 
œŸ
œŸ
œ 
œ˜6Q˜†
PšœŸ
œŸ
œ 
œŸ
œŸ
œ 
œ
Ÿ
œŸ
œ 
œ˜NQšœ
Ÿ
œŸ
œ?˜Q—š
ž˜N˜Š
š	žœŸ
œŸœ
žœž˜#Pšœžœžœ
Ÿ
œŸ
œŸ
œŸ
œ
žœ˜G—Qšœ‡
Ÿ
œŸ
œt˜ƒPšœŸ
œŸ
œ
 
œŸ
œŸ
œ	Ÿ
œŸ
œŸ
œŸ
œ
 
œŸ
œŸ
œ˜9Qšœ‘
�œ¡
œ ˜Ë
Pš¡ 
œŸ
œžœŸ
œžœ
˜Pš¡ 
œŸ
œžœŸ
œžœ
˜Pš¡ 
œžœŸ
œžœŸ
œ˜Pš¡ 
œ 
œ˜Q˜Pš¡ 
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ˜?Nšœ…Ÿ
œŸ
œ˜¬PšœŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œ˜9Q˜LPšœŸ
œ	Ÿ
œŸ
œŸ
œ 
œŸ
œ	Ÿ
œ˜;Q˜IPšœŸ
œ	Ÿ
œŸ
œŸ
œ 
œŸ
œ	Ÿ
œ˜;Qšœ�œŸ
œŸ
œ
˜)Nšœ�œ{˜‘
Pš
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ˜#Q˜2PšœŸ
œŸ
œžœŸ
œŸ
œŸ
œŸ
œ
žœžœ
˜=Qš	œ¡
œžœ4Ÿ
œŸ
œ˜‡
PšœŸ
œŸ
œŸ
œŸ
œžœžœ
Ÿ
œŸ
œŸ
œŸ
œ
žœ
˜YQšœžœ&˜-Pšœ
žœžœŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ
žœ
˜YQšœ
žœH˜UNšœžœE˜dPšžœžœ
žœ
žœŸ
œžœ
 
œ
žœžœž˜GQ˜'Pšœ
¡
œžœ 
œžœ
žœŸ
œ 
œ˜2PšœŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œŸ
œ˜fQ˜kPšœŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ˜9Q˜fPšœŸ
œŸ
œ 
œ˜Q˜PšœŸ
œŸ
œ 
œ˜QšœJŸ
œŸ
œt˜Æ
Nšœ"žœW˜}PšžœžœŸ
œŸ
œŸ
œŸ
œŸ
œ
ž˜0Q˜PšžœžœŸ
œ
žœŸ
œŸ
œŸ
œŸ
˜/Qšœžœ{˜�
——š
ž˜N˜ð
N˜3Pš
žœŸ
œŸ
œŸ
œŸ
œ˜ Qš	œØ
Ÿ
œ
Ÿ
œŸ
œ
Ÿ
œ.˜©šœžœ˜Pš¥¦
£©	£¤
£¤
£¦
£˜1Pš
¡ 
œ
žœ	Ÿ
œŸ
œ	ž˜*—QšœVŸ
œ
Ÿ
œÙ
Ÿ
œy˜µšœžœ
˜Pš
¥¦
£
©£	¤
£¤
£	©˜*Pš	¡ 
œ
žœ	Ÿ
œŸ
œ˜%—šœžœ˜Pš
¥¦
£
©£	¤
£¤
£	©˜*Pš¡ 
œžœ	Ÿ
œŸ
œ 
œ˜)—Q˜¤
N˜Pš
�œŸœ
žœ	Ÿ
œŸ
œ˜$Qšœ3�œR˜‡
Pšœžœ
žœ
�œžœ
�œžœ
�˜!Pš
œ	žœ
žœ
�œžœ
�˜Pšœžœžœ
�˜Q˜@Pšœžœ
žœŸ
œžœŸ
œžœ
�˜&Pšœ
Ÿœžœ
žœ
�œžœŸ
˜šœ
Ÿœžœ
žœ
�œžœŸ
˜P˜—Pšœ
Ÿœžœ
žœ
�œžœŸ
˜Pšœ
Ÿœžœ
žœ
�œžœŸ
˜Qšœ"�
ϛ
˜¡Nšœ´
Ÿ
œ1Ÿ
œŸ
œŸ
œZŸ
œ
˜×N˜Všœž
œ˜Pš	¥¦
£	¤
£
©£¤
£˜Pš
¡ 
œŸœŸ
œ	 
œŸ
˜!—šœž
œ˜Pš	¥¦
£©£
Ðez£©£˜Pš¡ 
œ
Ÿœ
 
œ˜—Q˜yšœž
œ˜Pš	¥¦
£©£
¬£©£˜Pš	¡ 
œ
 
œ
Ÿ
œŸœ
˜-—QšœžœžœH˜aPš	œ
Ÿœ
 
œŸ
œ	Ÿœ˜$Q˜+N˜T˜Pš
£˜Pš	¡ 
œŸœ 
œŸ
œ˜—Q˜Þ
˜Pš
¥¦
£©£
¬£©£œ˜Pš
¡ 
œŸ
œŸ
œŸœŸœ 
œ˜+—Qšœ
 
œk�œ%˜ž
˜Pš
¡ 
œŸ
œžœŸ
œžœ
�œ˜Pš¥¦
£©£¤
£©£¤
£˜Pš¡ 
œ�œŸ
œŸ
œ 
œ 
œŸ
œŸ
œŸœŸ
œ 
œ˜E—Q˜§
˜Pš
¡ 
œŸ
œžœ
�œŸ
œžœ˜Pš¥¦
£©£¤
£©£¤
£˜Pš¡ 
œ
�œŸ
œŸ
œ 
œ�œŸ
œŸ
œ 
œŸ
œŸœŸ
œŸ
œ˜W—Q˜¾
Nšœ8žœžœžœ˜kšœžœ˜Pš¥¦
£¤£©£¤
£©£˜Pš¡ 
œ
žœŸœ˜—šœžœ˜Pš¥¦
£¤£
˜Pš¡ 
œŸœ 
œ˜—Qšœ\žœ„
˜ã
N˜CPš	¥¦
£
©£
¬£©£˜Pš	¡ 
œ 
œ
ŸœŸœ	˜+Q˜‚
Pšœ 
œŸœŸœ˜-Qšœž
œ˜3Pš 
œŸœ	ŸœŸœ˜?Q˜)Pš 
œŸœ	Ÿœ
žœŸ
œŸœ	žœ
Ÿ
œž˜SQšœžœW˜`Pš 
œ
žœŸ
œŸœŸœŸœŸ
œŸœŸœŸœžœ
Ÿ
œž˜kQš
œ˜Pš
œŸœŸœŸœ 
œŸœŸœ˜1Qšœžœ5˜LPš 
œ
žœŸ
œŸœŸœžœ
Ÿ
œž˜?Q˜5Pšœ
ŸœŸœ˜!Q˜—š
ž˜N˜POšœ�œ+˜LO˜gNšœÈ�œ–˜ä	Pš¥¦
£©£˜Pš	¡ 
œ
žœžœ 
œ
˜3Q˜Pš¥¦
£˜Pš¡ 
œ 
œ˜Q˜†
N˜ì—š
ž
˜
š
œ
˜
Nšœs�œ˜�
—˜	Nšœ.¡
œI˜x—˜	N˜�
—˜	Nšœ4�Cœ˜Œ
—š
œ˜NšœK�Cœ˜£
—š
œ˜Nšœ�+œ˜M—š
œ
˜
NšœE�Eœ˜Ÿ
—˜
N˜�
—š
œ˜Nšœ\�œ˜Š
—š
œ
˜
NšœE�œ˜l—š
œ	˜	Nšœ<�œ˜d—˜
Nšœ0�œ
˜?—š
œ˜Nšœ3�Mœ˜š
—š
œ˜Nšœb�œ˜~——˜P˜Pš
£
˜
š¡
œ
 
œ˜Qšœ 
œ
¡
œ
˜—šœ�œ
˜Pš¡
œ
 
œ˜Pš¥
£
¦
£¦
£˜Pš¡
œ
 
œ˜—šœ�œ˜Pš	¡
œ
 
œŸ
œ
 
œŸ
˜Pš¥
£
¦
£¤
£
¦
£¤
£¦
£˜Pš¡
œ
 
œ˜QšœD¡
œ˜d—˜Pš¥
£
¦
£˜Pš¡
œ
 
œ 
œ˜	—˜
Pš	¥
£
¦
£¤
£
¦
£¤
˜Pš	¡
œ
 
œŸ
œ
 
œŸ
˜—˜Pš	¡
œ
 
œŸ
œ
 
œŸ
˜Pš	¥
£
¦
£¤
£
¦
£¤
˜Pš	¡
œ
 
œŸ
œ
 
œŸ
˜Qšœ 
œ˜:—˜Pš¡
œ
 
œŸ˜	Pš
¥
£
¦
£¤
£
¦
£¤
œ
˜Pš¡
œ
 
œŸ˜	—˜ Pš
¡
œ
 
œŸ
œ
 
œŸ
œ
˜Pš¥
£
¦
£¤
£˜Pš¡
œ
 
œ	Ÿ
œ˜—˜Pšœ
¡
œ 
œ˜Pš¡
œ 
œ
žœ˜Pš¡
œ
 
œŸ
œ˜	Pš	¥
£
¦
£¤
£
¦
£¤
˜Pš
¡
œ
 
œŸ
œ 
œŸ
œ˜Q˜‚
—š
œ˜Pš¥
£
¦
£¤
£¤
£˜Pš	¡
œ
 
œŸ
œ
 
œŸ
˜Qš
œ˜Oš¡
œ&¡
œ
˜)Ošœžœžœ
˜Oš	œ
Ÿ
œŸ
œ-žœžœS˜¡
—š
œ˜Pš¥
£¦
£©£˜Pš¡
œ 
œ 
œ
˜—š
œ˜Pš¡
œ
 
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ
˜Pš¥
£
¦
£©£¤
œ
˜
Pš¡
œ
 
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ
˜ —š
œ˜Pš¥
£¦
£˜
Pš¡
œ 
œžœ˜—š
œ˜Pš¥
¤£¦
£©£˜Pš¡
œ 
œžœ˜—š
œ˜Pš¥
£
¦
£¤
£
¦
£¤
£©£ª
¥
˜Pš¡
œ
 
œžœŸ
˜—˜
Pš¥
£
¦
£	©£¤
£˜Pš¡
œ
 
œ
žœ
Ÿ
œ˜—šœžœ˜Pš¡
œ
 
œ
žœŸ
œŸ
œžœžœ˜&Pš¡
œ
 
œ	žœŸ
œ˜Pš£
¥
£¤
£¤
£	¦
£
©£˜Pš¡
œ
 
œ
žœ
žœŸ
œŸ
œžœž˜(—šœžœ˜Pš¡
œ
 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
žœ˜Pš¥
£
¦
£©£¤
£©£¤
£©£¤
£˜ Pš¡
œ
 
œ
žœ
žœŸ
œ
žœŸ
œ
žœŸ
œ
ž˜!—šœžœ˜Pš¡
œ
 
œ
žœŸ
œ
žœŸ
œ
žœ˜Pš¥
£
¦
£©£¤
£©£¤
£˜Pš¡
œ
 
œ
žœ
žœŸ
œ
žœŸ
œ
ž˜—šœžœ
˜Pš¥
£
¦
£
©£	¤
£¤
£©˜+Pš¡
œ
 
œ
žœ
žœ	Ÿ
œŸ
œ
˜&—šœžœ˜Pš
¥
£
¦
£
©£¤
£¤
£˜*Pš¡
œ
 
œ
žœ
žœŸ
œŸ
œ˜,—š
œ˜Pš¡
œ
 
œ
Ÿ
œžœŸ
œŸ
œ	žœ˜7Pš
¥
£
¦
£©£	©£¤
£˜"Pš¡
œ
 
œžœ
Ÿ
œ˜—š
œ˜Pš¥
£¦
£
˜Pš¡
œ 
œ	 
œ˜—šœžœ˜Pš
¥
£¦
£©£	¤
£¤
£˜*Pš¡
œ 
œžœ	Ÿ
œŸ
œ 
œ˜*—šœžœ˜#Pš
¥
£¦
£©£¤
£¤
£˜.Pš¡
œ 
œžœŸ
œŸ
œ 
œ˜/—˜Pš	¡
œ
 
œŸ
œžœ
ž˜Pš¥
£
¦
£¤
£˜	Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
œŸ
œ
˜#—˜Pš
¡
œ
 
œŸ
œŸ
œŸ
œŸ
œž˜)Pš
¥
£
¦
£©£¤
£	¤
£˜Pš¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ˜$—˜Pš¥
£
¦
£
¤
£¤
£¤
£¤
£
˜(Pš¡
œ
 
œ
Ÿ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œ˜3—˜Pš¥
£
¦
£˜Pš¡
œ
 
œ 
œ˜—šœžœ
˜Pš
¥¦
£
©£	¤
£¤
£	©˜*Pš	¡ 
œ
žœ	Ÿ
œŸ
œ˜%—šœžœ˜Pš
¥¦
£
©£	¤
£¤
£	©˜*Pš¡ 
œžœ	Ÿ
œŸ
œ 
œ˜)—šœžœ˜Pš¡ 
œŸœžœŸ
˜Pš¥¦
£
©£˜
Pš¡ 
œ
žœŸœ˜—šœžœ˜Pš¥¦
£¤£
˜Pš¡ 
œŸœ	 
œ˜—šœžœ
˜Pš¥
£
¦
£
©£¤
£¤
£©£©£˜&Pš!¡
œ
 
œ
žœŸ
œŸ
œžœžœ
 
œ
žœŸ
œŸ
œŸ
œŸ
œžœŸ
œŸ
œž˜g—šœžœ˜Pš¡
œ
 
œ
žœŸ
œŸ
œŸ
œŸ
œžœžœ˜$Pš%¡
œ
 
œ
žœŸ
œŸ
œŸ
œŸ
œžœŸ
œ
žœ
 
œ
žœŸ
œŸ
œŸ
œŸ
œžœŸ
œ
ž˜CPš$¥
£
¦
£
©£¤
£¤
£¤
£¤
£©£¤
£
©¦
£
©£¤
£¤
£¤
£¤
£©£¤
£
©˜CPš ¡
œ
 
œ
žœŸ
œŸ
œŸ
œŸ
œžœž 
œ
žœŸ
œŸ
œŸ
œŸ
œžœž˜A—šœžœ˜Pš¡
œ
 
œ˜	Pš¥
£
¦
£©£¤
£¤
£©£©£˜"Pš¡
œ
 
œžœŸ
œŸ
œžœžœ 
œ
žœŸ
œŸ
œžœž˜D—šœžœ˜Pš¡
œ
 
œŸ
œ 
œ
žœŸ
œ
žœž˜$Pš¥
£
¦
£©£¤
£¤
£¤
£¤
£©£©£˜.Pš ¡
œ
 
œžœŸ
œŸ
œŸ
œŸ
œžœžœ
 
žœŸ
œŸ
œŸ
œŸ
œžœž˜N—šœžœ˜Pšœ
¡
œŸ
œ 
œ˜Pš¥
£
¦
£©£¤
£¤
£	¤
£¤
£©£©£˜6Pš!¡
œ
 
œžœŸ
œŸ
œ	Ÿ
œŸ
œžœžœ
 
žœŸ
œŸ
œŸ
œŸ
œ
žœžœ
˜`—šœžœ˜Pš¡
œ
 
œŸ
œŸ
œžœŸ
œ
žœŸ
œ
˜)Pš£
¥
£
«
£¤
£¦
£¤
£¤
˜Pš#¡
œ
¡
œ
 
œ
žœŸ
œŸ
œžœŸ
œ
žœŸ
œ 
œ
žœŸ
œŸ
œžœŸ
œŸ
œ
ž˜Q—šœžœ	˜Pš¡
œ
 
œ
žœŸ
œŸ
œŸ
œŸ
œžœž£
œ˜3Pš£
¥
£¤
£¦
£
¤
£¤
£˜&Pš#¡
œ
 
œ
žœŸ
œŸ
œŸ
œŸ
œžœžœ
 
œ
žœŸ
œŸ
œžœŸ
œŸ
œžœž˜a—šœžœ˜Pš
¡
œ
 
œ
žœžœžœ˜Pš¥
£¦
£˜Pš¡
œ
 
œ
žœžœžœ
 
œ˜—šœžœ˜Pš¥
£
¦
£˜Pš¡
œ
 
œ
žœžœžœ
 
œ˜—šœžœ˜š¡
œ
 
œžœŸ
œŸ
œŸ
œžœžœ˜,P˜—Pš&œ
¡
œ	Ÿ
œŸ
œ 
œ
žœŸ
œŸ
œŸ
œžœŸ
œ
žœ
 
œ
žœŸ
œŸ
œŸ
œžœŸ
œ
ž˜dšœ
¡
œ	Ÿ
œŸ
œ 
œžœŸ
œžœŸ
˜+P˜—Pš£
¥
£	¤
£¤
£¦
£
¤
£
¦
£¤
£¦
£¦
£˜8Pš¡
œ
 
œžœŸ
œŸ
œŸ
œžœž 
œ
žœŸ
œŸ
œŸ
œžœž˜N—šœžœ
˜Pš¡
œ
 
œžœŸ
œŸ
œŸ
œžœžœ˜*Pš£
¥
£	¤
£¤
£¦
£¦
£˜Pš¡
œ
 
œžœŸ
œŸ
œŸ
œžœž 
œ
žœŸ
œŸ
œŸ
œžœž˜M—šœ¡
œ˜Pš¡
œ
 
œžœŸ
œŸ
œŸ
œžœžœ˜$Pš¥
£
¦
£
©£¤
˜Pš ¡
œ
 
œžœŸ
œŸ
œŸ
œžœž 
œ
žœŸ
œŸ
œŸ
œžœŸ
œŸ
œž˜K—šœžœ˜Pš¥
£
¦
£©£¤
£
©£¤
£©£¤
£
©£¤
£˜&Pš'¡
œ
 
œžœŸ
œ
žœŸ
œžœŸ
œ
žœŸ
œ 
œ
žœŸ
œ
žœŸ
œŸ
œžœŸ
œŸ
œž˜P—šœžœ˜Pš£
¥
£¦
£©£¤
£
©£¤
£©£¤
£
©£˜%Pš#œ
¡
œ 
œžœŸ
œ
žœŸ
œžœŸ
œ
ž 
œ
žœŸ
œ
žœžœŸ
œ
žœŸ
œ
ž˜M—šœžœ˜Pš¥
£
¦
£
©£©£¤
£
©£¤
£
©£˜!Pš¡
œ
 
œ
žœžœŸ
œ
žœŸ
œ
žœ
 
œŸ
œ
˜$—šœžœ˜Pš¥
£
¦
£
©£©£¤
£
©£¤
£
©£˜"Pš¡
œ
 
œ
žœžœŸ
œ
žœŸ
œ
žœ
 
œŸ
œ
˜%—šœžœ˜Pš¥
£
¦
£
©£¤
£
©£¤
£
©£¤
£
©£˜Pš¡
œ
 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
žœ
 
œŸ
œŸ
œ˜*—šœžœ˜Pš¡
œ
 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
žœ˜Pš¡
œ
 
œ
žœŸ
˜Pš¡
œ
 
œŸ
œ
 
œ 
œŸ
œ
 
œŸ
˜Pš¥
£
¦
£¤
£
¦
£¦
£¤
£
¦
£¤
˜Pš ¡
œ
 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
ž 
œ
žœŸ
œ
žœŸ
œ
žœŸ
œ
ž˜7—šœžœ	˜Pš¥
£
¦
£©£¤
£
©£¤
£
©£©˜ Pš"¡
œ
 
œžœŸ
œ
žœŸ
œ
ž 
œ
žœŸ
œ
žœŸ
œžœŸ
œ
žœŸ
œ
žœž˜G—˜&Pš¥
£
¦
£
¤
£
˜Pš¡
œ
 
œŸ
œ 
œ
žœŸ
œŸ
œžœ	Ÿ
œž˜M—˜Pš¥
£
¦
£©£
¤
£¤
£¤
£
˜:Pš¡
œ
 
œžœŸ
œŸ
œŸ
œ
 
œ
žœžœ
Ÿ
œŸ
œŸ
œŸ
œžœž˜„
—˜Pš¥
£
¦
£©£©£˜Pš¡
œ
 
œž	œž	œ˜—˜Pš¥
£
¦
£¤
£¤
£¤
£¤
£˜Pš	¡
œ
 
œŸ
œ
Ÿ
œŸ
˜—˜Pš
¡
œ
 
œžœŸ
œŸ
œ	˜%Pš¡
œ
 
œ
Ÿ
œŸ
œŸ
œŸ
œ
˜,Pš
¥
£
¦
£
©£	¤
£¤
£˜Pš
¡
œ
 
œŸ
œŸ
œŸ
œ˜-—šœžœ˜Pš	œ
¡
œŸ
œŸ
œ 
œ˜Pš¡
œ
 
œ	Ÿ
œŸ
œŸ
œŸ
œ
˜,Pš
¥
£
¦
£
©£
¤
£¤
£˜Pš¡
œ
 
œ
žœŸ
œŸ
œŸ
œžœžœ
Ÿ
œŸ
œ˜;—šœžœ˜Pš¡
œ
 
œŸ
œž˜Pš¥
£
¦
£¤
£¤
£˜Pš¡
œ
 
œžœŸ
œ
žœŸ
œžœŸ
œ
žœ˜!—šœžœ˜Pš¡
œ
 
œŸ
œž˜Pš¥
£
¦
£¤
£˜
Pš¡
œ
 
œžœŸ
œ
žœŸ
œ
žœž˜ —˜Pš£
¥
£¤
£¤
£	¦
£	©£¤
£	©£˜;Pš¡
œ
 
œžœ	Ÿ
œŸ
œž˜,—˜ Pš¡
œ
 
œžœ
žœ	Ÿ
œŸ
œ˜)Pš£
¥
¤£©£	¤
£¤
£¤
£¤
£¦
£˜DPš¡
œ
 
œ
žœŸ
œŸ
œžœ
žœŸ
œŸ
œ˜E—šœžœ˜Pš¥¦
£©	£¤
£¤
£¦
£˜1Pš
¡ 
œ
žœ	Ÿ
œŸ
œ	ž˜*—˜Pš¡
œ
 
œŸ
œŸ
œžœ
ž˜Pš¥
£
¦
£
©£¤
˜Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ˜-—˜Pš¡
œ
 
œŸ
œŸ
œžœ
ž˜Pš¥
£
¦
£
©£¤
˜Pš¡
œ
 
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ˜$—˜Pš	¡
œ
 
œ	Ÿ
œžœ
ž˜Pš	¡
œ
 
œ	Ÿ
œžœ
ž˜Pš
¥
£
¦
£©£©£¤
£˜Pš¡
œ
 
œ	Ÿ
œ	Ÿ
œ 
œŸ
œ	Ÿ
œ˜,—˜#Pš	¡
œ
 
œ	Ÿ
œžœŸ
˜Pš	¡
œ
 
œ	Ÿ
œžœŸ
˜Pš
¡
œ
 
œŸ
œŸ
œ 
œ˜Pš
¥
£
¦
£©£©£¤
£˜Pš¡
œ
 
œŸ
œ	Ÿ
œ 
œŸ
œŸ
œ˜*—˜Pš¡
œ
 
œžœ
ž˜ Pš¥
£
¦
£
©£˜
Pš¡
œ
 
œ 
œ	˜—˜Pš¡
œ
 
œŸ
œžœŸ
œŸ
œžœŸ
œ
˜Pš¥
£
¦
£©£¤
£©£¤
£˜Pš ¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ˜Y—˜Pš¡
œ
 
œŸ
œžœŸ
œŸ
œžœŸ
œ
˜Pš¥
£
¦
£©£¤
£©£¤
£˜Pš ¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ˜[—˜Pš¥
£
¦
£¤
£¤
£¤
£¤
£¤
£
˜)Pš(¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ˜r—˜Pš¥
£
¦
£©£˜Pš¡
œ
 
œ 
œ	˜!—˜Pš¥
£
¦
£
©£¤
£˜š¡
œ
 
œ
Ÿ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
˜APšœ
Ÿ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œ˜N——˜
Pš
¥
£
¦
£¤
£©£©£˜Pš¡
œ
 
œŸ
œŸ
œŸ
œŸ
œ 
œŸ
œŸ
œŸ
œŸ
œ˜;—˜Pš¡
œ
 
œŸ
œžœŸ
œžœ˜Pš¡
œ
 
œžœŸ
œžœŸ
œ˜Pš
¥
£
¦
£¤
£¤
£¦
£˜!Pš	¡
œ
 
œŸ
œ
 
œŸ
˜—˜Pš
¡
œ
 
œ
Ÿ
œžœŸ
œ˜Pš¡
œ
 
œ
Ÿ
œžœ˜Pš
¡
œ
 
œŸ
œŸ
œŸ
œ˜.Pš
œ
¡
œ	Ÿ
œ 
œŸ
œŸ
˜Pš
œ
¡
œ	Ÿ
œ 
œŸ
œŸ
˜Pš¥
£
¦
£¤
£¤
˜
Pš¡
œ
 
œŸ
œŸ
œŸ
ž
œ 
œŸ
œŸ
œŸœ
˜$—˜Pš¥
£
¦
£©£˜Pš¡
œ
 
œ
žœ 
œ˜.—˜Pš¥
£
¦
£˜Pš¡
œ
 
œ
 
œ˜—šœž
œ˜Pš	¥¦
£	¤
£©£¤
£˜Pš
¡ 
œŸœ
Ÿ
œ	 
œŸ
˜"—šœž
œ˜Pš	¥¦
£©£
¬£©£˜Pš¡ 
œŸœ
 
œ˜—šœž
œ˜Pš	¥¦
£©£
¬£©£˜Pš	¡ 
œ
 
œ
Ÿ
œŸœ
˜-—˜Pš
£˜Pš	¡ 
œŸœ 
œŸ
œ˜—˜Pš
¥¦
£©£
¬£©£œ˜Pš
¡ 
œŸ
œŸ
œŸœŸœ 
œ˜+—˜Pš
¡ 
œŸ
œžœŸ
œžœ
�œ˜Pš¥¦
£©£¤
£©£¤
£˜Pš¡ 
œ�œŸ
œŸ
œ 
œ 
œŸ
œŸ
œŸœŸ
œ 
œ˜F—˜Pš
¡ 
œŸ
œžœ
�œŸ
œžœ˜Pš¥¦
£©£¤
£©£¤
£˜Pš¡ 
œ
�œŸ
œŸ
œ 
œ�œŸ
œŸ
œ 
œŸ
œŸœŸ
œŸ
œ˜W———…—Þ
U�