|
To provide an operational semantics of the Scheme language means to formally describe the process of evaluation for its expressions.
The most formal and precise way to do that is by means of a formal system,
as done in the paper "Structured Operational Semantics of a fragment of the language Scheme" (part of the reading material of the course.)
A frame is a finite set of associations between variable names and values.
When a Scheme session is opened, the environment consists only in the top level frame,
containing the default associations for the predefined symbols.
This environment will be possibly modified by the evaluation of the Scheme expressions during our session.
When the interpreter evaluates a define expression, the evaluation is performed in the current frame (the top level one in case we have just opened the Scheme session). The evaluation of a define expression modifies the current frame.
Example: (define c (+ 5 3)) (define b (= c 8)) (define c 2) (= c 8) > #f
The evaluation of the expression (+ 5 3) produces the value 8, which is associated
to the variable c.
F2-------- | c -> 8 | ---------- The expression (= c 8) is evaluated, giving true as value (we need to distinguish between the expression #t and its value), and the frame is modified by adding b -> true:
F2------------ | c -> 8 | | b -> true | -------------- (define c 2) is evaluated and since c is a variable already present in this frame, it is overwritten (we need always to be aware that "overwriting" can have unpredictable side-effects).
F2------------ | c -> 2 | | b -> true | -------------- If we now evaluate again (= c 8) its value is obviously "false". So, the value of this expression depends on when it is evaluated, not a very nice thing indeed!
Notice that, if we write b on the prompt, we obtain "true" as value.
In fact the evaluation of the value to associate to b is done only once,
when the interpreter evaluate the expression (define b (= c 8));
from that moment on the value of b will be true (unless we "overwrite" the variable b).
The value of functions, implementation of beta-reduction, scoping problem, closures and evaluation of applications
We said that, in an environment, values are associated to identifiers.
We know that for Scheme an abstraction is a value;
So the value of a lambda-expression is the lambda-expression itself. (define (f x) (+ 3 x))(recall that this definition is equivalent to (define f (lambda (x) (+ 3 x))) ) ) the following association is inserted in the current frame F: f --> value-of-(lambda (x) (+ 3 x)). So, according to the fact that a lambda expression is a value (and hence cannot be further evaluated) such association is f --> (lambda (x) (+ 3 x)) If we now evaluate (f 5)the interpreter looks in the environment for an association for the symbol f and finds the lambda-expression (lambda (x) (+ 3 x)). Now, since we get immediately the value of the argument of f, 5, we expect the interpreter to perform the beta reduction of the redex ((lambda (x) (+ 3 x)) 5) and, afterwards, the evaluation of (+ 3 5) ( + is a predefined function and the interpreter will call an inner procedure in order to compute 3 + 5).
Since substitution is an heavy operation to implement, here is what Scheme does instead of actually performing a beta-reduction:
| |
F-------------------------|
^
|
F1------------
| x --> 5 |
-------------
You see, in this way we sort of perform the beta-reduction avoiding to actually perform the substitution. Let us go back now to the value of lambda expressions. As a matter of fact the value of a lambda expression is something a bit more complex than simply the lambda expression itself. To explain why, let us consider the following example.
(define a 3)
(define (f x) (+ a x))
(define (g y)
(let ((a 2))
(f y)))
(g 5)
According to what we said up to now, f should now be associated to the "value " (lambda (x) (+ a x)).
Making the first choice means that we wish our language to have static scoping.
A language with static scoping implies however some machinery for its realization.
The implementation of static scoping by means of closures works, roughly, as follows:
in order to evaluate an application (e0 e1...em)
where the value of e0 is a closure, the interpreter evaluates
the body of the function using the pointer in the closure, and taking into account
the associations formal parameters -> actual parameters. The value of lambda expressions:
Let us see, step by step, what really happens during the evaluation of the previous example.
(define a 3) is evaluated we get
| a --> 3 |<---p1 F------------- Then when we evaluate
(define (f x) (+ a x)) the frame F is modified as follows
| a --> 3 | | f --> <(lambda (x) (+ a x)), p1> |<--- p1 F---------------------------------------
where the current frame pointer is still p1.
(define (g y)
(let ((a 2))
(f y)))
modifies F as follows
| a --> 3 | | f --> <(lambda (x) (+ a x)), p1> | | g --> <(lambda (y) (let ((a 2)) (f y))), p1> | <--- F------------------------------------------------ p1 Now, if we evaluate
(g 5)
in F (that is using p1 as current frame pointer), the interpreter first evaluates the identifier "g". Its value is found in F: the closure <(lambda (y) (let ((a 2)) (f y))), p1>.
| a -- 3 |
| f --> <(lambda (x) (+ a x)), p1> |
| g --> <(lambda (y) (let ((a 2)) (f y))), p1> | <--- p1
F-------------------------------------------------
^
| p1
--------------
| y --> 5 | <---- p2
F1------------
Now, using p2 as current frame pointer, the interpreter evaluates the body of g, that is it evaluates
(let ((a 2)) (f y)) We know (rsSee Notes on let) that evaluating this expression is like evaluating
((lambda (a) (f y)) 2) So, since the evaluation of (lambda (a) (f y)) in p2 is the closure <(lambda (a) (f y)), p2>, we get
| a --> 3 |
| f --> <(lambda (x) (+ a x)), p1> |
| g --> <(lambda (y) (let ((a 2)) (f y))), p1> | <--- p1
F------------------------------------------------
^
| p1
--------------
| y --> 5 | <--- p2
F1------------
^
|p2
--------------
| a --> 2 | <--- p3
F2------------
We have now to evaluate (f y) using now p3 as current frame pointer.
| a --> 3 |
| f --> <(lambda (x) (+ a x)), p1> |
| g --> <(lambda (y) (let ((a 2)) (f y))), p1> | <--- p1
F------------------------------------------------
^ ^
| p1 | p1
-------------- --------------
| y --> 5 | <--- p2 | x --> 5 | <--- p4
F1------------ F3------------
^
|p2
--------------
| a --> 2 | <--- p3
F2------------
In F3 (that is using p4 as current frame pointer) the interpreter now evaluates the body
(+ a x)
+ is a predefined operator, so the interpreters starts evaluating its arguments.
It looks for an association for "a" in F3.
Not finding any, it goes up and finds an association for "a" in F.
So the evaluation of "a" in F3 returns the value 3.
You see how, by means of pointers in closures, we managed to evaluate the body of f
considering as value of "a" the one associated to it when f has been defined (even if, at the moment of the evaluation of (f y) in F2, "a" is associated to the value 2.) At the end of the evaluation of (g 5) the temporary frames used during the evaluation of (g 5) are logically "destroyed". More simply, any reference to the temporary frames is lost (the pointers p2, p3 and p4 are not usable anymore). The Garbage Collection process will realize later on that some frames are not accessible anymore (i.e. no usable pointer points at them) and hence it will "discard" them (in implementation terms it will deallocate the memory they occupy). NOTE: During the evaluation of an expression it is often the case that a current frame pointer p changes, in order to complete the evaluation of some subexpressions, and then turns back to be p again. It is clear that, in order to keep track of what is the current frame pointer and which pointer will turn back to be the current one after an evaluation, a data structure is needed: a "Stack of pointers". The upper one being the current frame pointer, while those below it being the ones that will turn back to be the current one after the various evaluations. Conditionals Let us see how conditional expressions are evaluated in Scheme.
(if exp exp1 exp2)
The interpreter evaluates exp; if its value is different from false it evaluates exp1 and returns its value as the value of the whole conditional expression. Otherwise it evaluates exp2 and returns its value.
(cond (test1 exp1)...(testn expn) (else exp)) A cond expression can be looked at as a series of nested if. Hence its operational semantics can be given in terms of if. Let and Letrec For what concerns the let expression
(let ((var1 exp1)
...
(varn expn))
exp)
As it is explained in the Notes on let, the operational semantics of let expressions can be given in terms of application and lambda abstraction. So, there is no need to describe explicitely how a let expression is evaluated.
There is a version of lec, however, that cannot be described in terms of other expressions, it is the letrec.
(let ((f (lambda (x) (f x)))
(f 3))
So, everything looks ok, since f is a function that keeps calling itself recursively forever.
At least so it seems to us.
(let ((f (lambda (x) (f x)))
(f 3))
corresponds to the evaluation of
( (lambda (f) (f 3)) (lambda (x) (f x)) )
Let us assume that p is the current frame pointer.
What happens when this expression is evaluated?
We first evaluate (lambda (f) (f 3))
Its value is the closure <(lambda (f) (f 3)), p>.
| | <--- p
F----------------------
^
|
|
---------------------------------
| f --> <(lambda (x) (f x)), p> | <--- p1
F1-------------------------------
The new temporary frame, which is now the current frame,
contains the association between the formal and the actual argument of the function.
In our case such association is between the local variable f of the let expression and its value. What it is relevant to notice is that the value associated to f has been evaluated using p as current frame pointer, that is the current frame pointer used for the evaluation of the let expression itself.
| |<--- p
F----------------------
^ ^ ------------
| |__________________________| x --> 3 |<--- p2
| F2----------
---------------------------------
| f --> <(lambda (x) (f x)), p> | <--- p1
F1-------------------------------
The computation goes on with the evaluation of (f x) with p2 as current frame pointer.
It is easy to check now that when we evaluate (f x) in F2 we get an error, since there is no value associated to f in F2 and no value in F either!
| |<--- p
F----------------------
^
|
|
---------------------------------
| f --> <(lambda (x) (f x)), p1>| <--- p1
F1-------------------------------
and then
| |<--- p
F----------------------
^
|
|
---------------------------------
| f --> <(lambda (x) (f x)), p1>| <--- p1
F1-------------------------------
^
|
-----------
| x --> 3 |<-- p2
F2----------
Notice how now, the evaluation of (f x) in F2 would really lead to an infinite computation.
How can we achieve such an effect?
(letrec ((f (lambda (x) (f x)))
(f 3))
In the evaluation of a letrec expression, the expressions whose values will be associated to the local variables are evaluated in the very same frame that will contain the new local associations. That is why, by using letrec instead of let, we get p1 instead of p in the closure associated to f. Notice that, unlike the let, the behaviour of a letrec expression cannot be described in terms of other expressions. Hence its semantics has to be given explicitely. In order to fix better what we have learned, let us have a look at another example. It is an example showing that, when a pointer p is in the closure associated to an identifier in a frame F, it is not always the case that p points to F itself. Let us consider the following Scheme session.
(define f (lambda (y) y))
(define (g x)
(define h f)
(h x))
(g 1)
We assume that, before beginning the session, p1 is the current frame pointer, pointing to the frame F1.
p1--> | f -> <(lambda (y) y), p1> |
F1---------------------------
The evaluation of the second define modifies F1 as follows.
| |
p1--> | f -> <(lambda (y) y), p1> |
| g -> <(lambda (x) (define h f) (h x)), p1>|
F1-------------------------------------------
At this point we evaluate the application (g 1). Remark: Recall that when the interpreter evaluates an application (exp1 exp2), it does not expect exp1 to actually be a lambda abstraction or a predefined function, but rather its value to be one of the two. The value of g is a closure, the value of 1 is 1. The semantics of the application tells us that if the value of the first expression is a closure, the frame pointed by the pointer in the closure has to be extended with a new frame containing the associations "formal parameters -> actual parameters". Such a new frame becomes the current frame.
| |
p1--> | f -> <(lambda (y) y), p1> |
| g -> <(lambda (x) (define h f) (h x)), p1>|
F1-------------------------------------------
^
|
F2 --------
p2 --> | x -> 1 |
----------
Now we evaluate g's body, that is (define h f) (h x)using p2 as current frame pointer. The evaluation of the local define modifies the current frame F2 inserting the association "h -> f's value". Since f is a variable, the interpreter looks for an association for f in F2. Not finding any, it looks for it in F2. So, the value of f is >(lambda (y) y), p1> the evaluation of the local define modifies the environment as follows.
| |
p1--> | f -> <(lambda (y) y), p1> |
| g -> <(lambda (x) (define h f) (h x)), p1>|
F1-------------------------------------------
^
|
F2 ---------------------------
p2 --> | x -> 1 |
| h -> <(lambda (y) y), p1> |
-----------------------------
You see, now we have F2 as current frame, containing an association var -> closure, and the pointer in the closure does not point to F2 but to another frame, F1.
| |
p1--> | f -> <(lambda (y) y), p1> |
| g -> <(lambda (x) (define h f) (h x)), p1>|
F1-------------------------------------------
^ ^
| |
F2--------------------------- F3-----------
p2--> | x -> 1 | | y --> 1 |<-- p3
| h -> <(lambda (y) y), p1> | -------------
-----------------------------
Now, with p3 as current frame pointer, we evaluate h's body, that is y. In the previous example, in order to introduce the local variable h, a let expression could be used instead of the inner define (let expressions introduce local variables).
(define (g x)
(let ((h f))
(h x)))
We notice however that between the two constructions there is a difference:
an internal define modifies a frame, while the let expression adds a new frame.
Let us see what would have happened in case we had used let.
...
^
|
F2--------
p2--> | x -> 1 |
----------
^
|
F4---------------------------
p4--> | h -> <(lambda (y) y), p1> |
----------------------------
In our example above the final result is identical if we use let or the inner define. There can be cases, however, in which modifying a frame and "attaching a new frame to it" can produce different results.
Exercise:
Describe what happens in the evaluation of the following SCHEME session
(i.e. describing the various frames, their modifications etc. along the lines of the examples
above)
(define (K x)
(lambda (x)
(+ (let ((x 1)
(fun (lambda (y) (+ x 1))))
(fun x))
(+ x x))))
(define t 44)
(define x 8)
(let ((x (+ x 2))
(gg (lambda (y) t))
(t 66)
(fun 21))
((lambda (x) (+ (gg 1) fun)) ((K fun) x) ))
Temporary memorization of values (A thank to P. Giarrusso)
(define a ((lambda (x) (+ 1 x)) (- 3 2)))
the value of the expression ((lambda (x) (+ 1 x)) (- 3 2)), i.e. 2,
will be associated in the environment to the identifier a.
A formal system for the description of the operational semantics of Scheme
Giving an operational semantics for a language corresponds, roughly, to explaining how the interpreter of the language works.
Up to now, for Scheme, we have done it in a rather informal way.
A formal description of Scheme operational semantics is useful in order to make the semantics itself non ambiguous, and in order to ease the implementation of the interpreter. Our operational semantics of Scheme is, instead, a Big Step semantics, that is a formal system whose judgments can be roughly interpreted as
Let us first precisely describe the form of the judgments of our formal system.
Then for the define expressions the judgments are of the form:
whose informal meaning is: the evaluation of the define expression "d" modifies the environment from zeta to zeta' For the other expressions the judgments are of the form:
whose informal meaning is the evaluation of the expression "e" returns the value v and modifies the environment from zeta to zeta' You see, we are giving a Big Step semantics: the judgment does not say that the expression "e" reduces with one computational step to the expression "e' ", but, rather, it says what is the value that is obtained by the complete evaluation of "e", if it converges.
Remark:
We have only studied a small subset of Scheme, avoiding the use of any imperative operator (useful sometimes, but to be used with great care);
In the purely functional fragment of Scheme, the only modifications we can produce on the environment are those obtained by the evaluation of define expressions.
To go on now with our formalization, we need to formalize precisely the Scheme syntax.
To formalize, instead, what we intend for a value, we define the set of values V. To define V we introduce a few semantic categories:
In the pages 4-6 of the paper, you can find the description of the other syntactic and semantic categories.
We formalize now the concept of frame. Example: Let us consider the frame
------------------ | a -> 2 | | b -> #t | | f -> <..., p> | ------------------
This is the graphical representation of a partial function: the function associating
the value 2 to the variable a, the value #t to the variable b, and the closure <..., p> to the variable f (recall that closures belong to the set V of values).
During the evaluation of an expression, a frame can be modified (by evaluating define expression, for instance).
We denote by
The empty frame is denoted by the emptyset symbol (for typographic reasons we shall write "ef").
We formalize now the concept of environment.
Env is the set of partial functions from pointers to pairs of the form (pointer, frame). Recall that in an environment there always exists the top level frame (the fatherless one). That is why we have added the symbol "top" in the definition.
Let us consider the environment zeta containing the frame rho of the example above.
Let n be pointer to the frame rho end let us assume the rho's father to be pointed at by n' (n'=top in case rho be the top level frame). This notation tells us that this environment is identical to zeta, but for the fact that now the pointer n points to the modified frame rho (containing the new association x -> 1). Now we can finally present the Formal System of Scheme Structured Operational Semantics . At the base of the system for expressions we have axioms of the following shape: These axioms state that the value of the constant 3 is the number 3 in any possible environment and in any possible current frame.
Axioms like the above one shows how predefined functions behave. There will naturally be judgments of this sort for every constant and for every predefined function. Look in the paper (at page 7) for the general form for this type of judgments.
Now, let us have a look at rules (var 1) and (var 2).
As a matter of fact (var 1) not a rule, it is an axiom.
We could read the same axiom bottom up. In this way it represent what the interpreter does when evaluating a variable x:
The rule (var 2) describes how the interpreter evaluates a variable x in case it is not in the pointed frame. It looks for it in the father frame.
(var 2) is a real inference rule and in this case the premise judgment is
"zeta, n' |-- x -> v, zeta ".
The notion of error in our system is formalized by assuming that an error is produced by the
interpreter whenever no rule is applicable, i.e. the expression we need to evaluate is
in no consequence judgment of any rule (and therefore we cannot succeed in deriving any judgment for our expression).
Now we analyse the rule that formalizes the evaluation of applications.
An application in Scheme is an expression of the form (e0 e1... em),
where e0 has to be an expression whose value is a closure or a predefined function.
For example e0 could be +, or (lambda (x) (- x 3)) or (lambda (x) x) +), etc, etc.
Let us consider (appl 1). Remark. At the end of the evaluation there is no reference left to the frame Next(zetam+1). When the garbage collector will realize that the part of memory that implements this frame is not referenced by any pointer anymore, it will add it in the heap so it can be used again.
We now discuss the Hypothesis 3.
(define H
(lambda (arg)
(define S (+ c 1))
(define c 3)
(+ (+ S c) arg)))
According to the semantics just defined, when we evaluate an application of H to an argument, say (H 5)on H, the interepreter extends the frame in which H has been defined and inserts in it the following associations: Read by yourself the other rules of the semantics in the paper (not the ones for "begin" and "set")
NOTE:
Many exercises on operational semantics ask to take a rule and to modify it in a certain way. By means of these exercises you can check whether you have undertood how to "read" the rules.
Of course, by modifying one of these rules one completely changes the way the interpreter evaluates expressions.
|