7.2 Formal semantics ¶

This section provides a formal denotational semantics for the primitive expressions of Scheme and selected built-in procedures. The concepts and notation used here are described in Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory³⁹; the definition of dynamic-wind is taken from How to Add Threads to a Sequential Language Without Getting Tangled Up⁴⁰. The notation is summarized below:

$\begin{array}{ll}\hfill ⟨\mathrm{\dots }⟩\hfill & \text{sequence formation}\\ \hfill s\downarrow k\hfill & k\text{th member of the sequence}s\text{(1-based)}\\ \hfill \#s\hfill & \text{length of the sequence}s\\ \hfill s\S t\hfill & \text{concatenation of the sequences}s\text{and}t\\ \hfill s†t\hfill & \text{drop the first}k\text{members of sequence}s\\ \hfill t\to a,b\hfill & \text{McCarthy conditional}“\text{if}t\text{then}a\text{else}b”\\ \hfill \rho [x/i]\hfill & \text{substitution}“\rho \text{with}x\text{for}i”\\ \hfill x\mathrm{in}\mathrm{D}\hfill & \text{injection of}x\text{into domain}\mathrm{D}\\ \hfill x|\mathrm{D}\hfill & \text{projection of}x\text{into domain}\mathrm{D}\end{array}$

The reason that expression continuations take sequences of values instead of single values is to simplify the formal treatment of procedure calls and multiple return values.

The boolean flag associated with pairs, vectors, and strings will be true for mutable objects and false for immutable objects.

The order of evaluation within a call is unspecified. We mimic that here by applying arbitrary permutations $\mathrm{permute}$ and $\mathrm{unpermute}$, which must be inverses, to the arguments in a call before and after they are evaluated. This is not quite right since it suggests, incorrectly, that the order of evaluation is constant throughout a program (for any given number of arguments), but it is a closer approximation to the intended semantics than a left-to-right evaluation would be.

The storage allocator $\mathrm{new}$ is implementation-dependent, but it must obey the following axiom:

The definition of $𝒦$ is omitted because an accurate definition of $𝒦$ would complicate the semantics without being very interesting.

If $\mathrm{P}$ is a program in which all variables are defined before being referenced or assigned, then the meaning of $\mathrm{P}$ is

where ${\mathrm{I}}^{\ast }$ is the sequence of variables defined in $\mathrm{P}$, ${\mathrm{P}}^{\prime }$ is the sequence of expressions obtained by replacing every definition in $\mathrm{P}$ by an assignment, $⟨\mathrm{undefined}⟩$ is an expression that evaluates to $\mathrm{undefined}$, and $ℰ$ is the semantic function that assigns meaning to expressions.

• Abstract syntax
• Domain equations
• Semantic functions
• Auxiliary functions