commit 8244d2b45c2b5cc45e1efb7a2a59bc0451be9ff7
parent 2f1568ca38beb41f0eae3ae285e5f7db65a666a2
Author: Wolfgang Corcoran-Mathe <wcm@sigwinch.xyz>
Date: Tue, 6 Feb 2024 14:53:26 -0500
Formal semantics: Replace chapter with a note and a PDF URL.
Diffstat:
1 file changed, 4 insertions(+), 65 deletions(-)
diff --git a/doc/r7rs-small/formal-semantics.texinfo b/doc/r7rs-small/formal-semantics.texinfo
@@ -1,68 +1,7 @@
@node Formal semantics
@section 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 [36]; the definition of dynamic-wind is taken from [39]. The notation is
-summarized below:
-
-[r7rs-Z-G-1.png]
-
-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 permute and 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 new is implementation-dependent, but it must obey the following
-axiom: if new σ ∈ L, then σ (new σ ∣ L)↓2 = false.
-
-The definition of calK is omitted because an accurate definition of calK would complicate
-the semantics without being very interesting.
-
-If P is a program in which all variables are defined before being referenced or assigned,
-then the meaning of P is
-
- calE [ [ ((lambda (I*) ] ]
- P')
- @svar{undefined}
- @dots{})
-
-where I* is the sequence of variables defined in P, P′ is the sequence of expressions
-obtained by replacing every definition in P by an assignment, @svar{undefined} is an
-expression that evaluates to undefined, and calE is the semantic function that assigns
-meaning to expressions.
-
-@menu
-* Abstract syntax::
-* Domain equations::
-* Semantic functions::
-* Auxiliary functions::
-@end menu
-
-@node Abstract syntax
-@subsection Abstract syntax
-
-XXX: TeX!
-
-@node Domain equations
-@subsection Domain equations
-
-XXX: TeX!
-
-@node Semantic functions
-@subsection Semantic functions
-
-XXX: TeX!
-
-@node Auxiliary functions
-@subsection Auxiliary functions
-
-XXX: TeX!
+[The formal semantics chapter uses complex LaTeX that is very
+difficult to translate to Texinfo. At some point, an attempt may
+be made to do this. Meanwhile, see
+@url{https://small.r7rs.org/attachment/r7rs.pdf, the PDF}.]
