[SCL] Proposed additions to the SCL draft standard

[John F. Sowa]

Chris,

The point of Tanel's note was that there are "structured annotations",
which have a very direct connection with certain formal constituents.

A theorem prover, for example, may start with a bunch of axioms and
a theorem to be proved.  During the course of the proof, it can
trace how each axiom may be combined, taken apart, and recombined
with parts of other axioms to form the parts of the final result.

For many purposes (both for human understanding and for metareasoning
inside the theorem prover itself) it is important to preserve the
trace of those connections.  Semantically, that trace is a kind of
comment, which has no effect on the truth value of the formula,
but it is directly connected to the constituents that do have
a semantic value.

CM> I have no serious problem with this; though I really do wonder
 > if it's a part of our ABSTRACT syntax to legislate where people
 > put their comments.  The current syntax seems to me to accommodate
 > them just fine simply by not preventing anyone from putting them
 > pretty much wherever they want.

That option does not preserve the connection between the comment and
the semantic constituent when you translate from one language to
another.  As Tanel pointed out, the comments (or structured annotations)
must be tied to constituents of the abstract syntax in order to
preserve the connections during translation.

And by the way, every theorem prover uses at least two languages:
the concrete syntax of the input and output statements and the internal
representation used by the theorem prover itself.  So the option of
tying comments (or structured annotations) to the abstract syntax is
essential for a theorem prover, even if it only uses one concrete
notation.

And even for people who want to put comments wherever they please,
they usually have some reason for putting them at one place rather
than another.  Whatever their reason, it would be nice to keep
the bookmark on the correct page when the text is translated to
another language.

John