Kelsey, R., Clinger, W., and Rees, J., Editors (1998). Revised5
Report on the Algorithmic Language Scheme. Section 7: Formal Syntax
and Semantics.
Questions from:
Barnes,
Brantley,
Edwards,
Erickson,
Fletcher,
French,
Guha,
Kasidhi,
Kuo,
Nyombayire,
Ramdial,
Schmitz,
Shireman,
Smith,
Yilma
Questions missing from:
Petersen,
Rosenbluh,
Contents
Do mathematical specifications like the one we're reading for Scheme exist for languages like C and Java?
Yes, I believe so.
What does the mathematical specification in section 7.2 give us that the less mathematical specification in the rest of the report doesn't give us?
A more careful specification that we can use to resolve any questions. In particular, we can apply the rules by hand
to see what the result should be.
I can see how knowing the first six chapters of the spec would help normal programmers. Would the stuff in 7.2 help out at all (if a normal programmer could even understand it, that is)?
The report can help a programmer understand some things in more depth. For example, the use of permute and unpermute in the definition of function application helps us understand that Scheme's order-of-evaluation is potentially implementation-specific.
Maybe I missed something from previous readings. What does "truish" mean?
The definition of truish is in 7.2.4, I believe. It means not false
.
Why does the section on Formal Semantics begin with 7.2.3 rather than 7.2.4. I struggled through the first section without being sure of what anything was doing until I got to the next section and realized all the functions that had been used weren't defined yet. It seems quite counter intuitive to start with the higher level functions first.
You gotta start somewhere. Some people work top-down (e.g., the authors of the Scheme report). Others work bottom-up. Like all great works of Philosophy, the Scheme report requires you to master the whole to understand the whole.
Sometimes things are described with an equality as in
phi:F = D => E
but other's are described with right arrows.
script C: Cmd => S => S
What's the difference between equality and the right arrow in this
context?
In the first case, we're defining the set F as
functions from the set D to the set E
. We're also saying that
when we use phi as a variable, we mean an element of F. In the
second case, we're saying that script C is a particular function
from Cmds to functions from S to S (or, alternately, from Cmds and
S's to S's).
Starting with the auxillary function lookup. It is defined as follows (p 42):
(1) lookup : U --> Ide --> L
and
(2) lookup = (lambda)(rho) I . (rho) I
In (1), I am confused because I look up in the abstract syntax and the domain equations, and I see this (p.41):
I is an element of Ide // Identifiers
(rho) is an element of U = Ide --> L // Environments
I am assuming that the --> in this case does not mean "if ... then ... else" even though that is the only way it is defined in this section. I am not sure what it means other than "Identifiers map to Locations" and it seems strange that (rho) (epsilon) U is defined as Ide --> L then defining lookup as U --> Ide --> L. I might just be thinking about this wrong, but I think the report is vague enough that I don't understand what is going on completely.
The right-arrows mean function from
. So, Ide --> L
is function from Ide to L
. The first line of lookup gives its type, the second gives its definition.
I took --> to mean "can be defined as". What is the meaning of C: Com* -> U -> C-> C (note the two C's)?
See the previous answer.
I could use clarification on the lambda notation.
What does the lambda symbol stand for? I've checked about ten times just to make sure I wasn't missing where it was defined, but I see nothing.
The expression \ x . body is a function of one parameter,
x, with result of body. In Scheme, we'd write it as (lambda (x) body). In both cases, when we apply a function, we replace every
instance of the formal parameter in the body with the actual parameter.
We then evaluate the modified body.
I am finding the notation confusing. What does the lambda_{rho kappa}
represent?
In section 7.2.3 the expression 'lambda'pk, or 'lambda' followed by another set of symbols is used frequently. I am unclear as to what this is supposed to represent.
Traditionally, a function of two parameters, rho and kappa.
Likewise in the definitions of auxiliary functions on page 42, what
does the A -> B -> C notation stand for? Right now my current guess
is the function takes in A, which evaluates to B, which evaluates
to C or causes C to be returne
On page 40 it is stated that the reason why expression continuations take sequences of values instead of single values is to simplify the formal treatment of procedure calls. How exactly is this achieved?
On page 41 and in the right column, there are three lambda expressions. In the
third lambda expression, how are the two statements equal?
I am confused by the equation describing set!. In particular, what do send and single represent?
I was trying to calculate E[(+ 2 3)] and ran into some difficulty with E[+], in the definition of E*[+ 2 3].
So far, I have
E*[+ 2 3] = \ p k . E[+] p (\ psi e* . psi (e*_1))
(\ e0 . k (<e0> ++ <2 3>))
but I don't know how to reduce this further. ++ stands for sequence concatenation on my limited keyboard. How do I reduce this, or what is E[+]?
The description of set! seems very closely tied to an implementation in terms of how the system is expected to manipulate a storage location when set! is invoked. I know, however, that Scheme is intended to be hardware independent. This suggests that the implementation relies on a more abstract representation of storage. To what extent does this abstraction make assumptions about how it will be handled at the hardware level? Does this make Scheme more or less efficient on systems that implement hardware storage in different ways?
What does Here and elsewhere, any expressed value other than undefined may be used in place of unspecified?
mean?
Um ... it means that when it says unspecified
, the implementation can return whatever value it wants (except, of course, for a special value known as undefined
).
In Sec. 7.2, it says 'x in D' is an injection of x into domain D and
'x | D' is a projection of x into domain D. What is the difference
between an injection and a projection?
Injection typically maps elements from a small set into a larger set.
(That is the cardinality of the mapped set is smaller than or equal
to the cadinality of the set it is mapped into.) Projection typically
maps from a large set to a smaller set. You can think of injection as
casting from a subclass to a superclass and projection as casting from
a superclass to subclass.
I'm confused by the fixed-point property for recursively defined functions.
Yeah, it's confusing. We'll get to it much later.
In the function lambda (I*) gamma>* Eo, is Eo returned as a value...
on line 11 as a continuation it was bound to on line 6, or
on line 8 as the return of function send() - and in this case how do we know of all values passed as parameters to the outer function, that Eo and only Eo remains to be returned.
I assume that you're referring to the "meaning of" that expression.
Since the meaning is a continuation, E is never really returned. Instead,
E0 is evaluated in a context in which the statements have been eavluated
first (and returned as a continuation).
;
Check with Bobby