Does anyone know of a precise specification for CL grammar?
Most English prose specifications such as those in Steele's CLtL2
seem to be lacking in precision.
For example, how should the following be read:
(#xa#(1))
(#xa(1))
(#1=1#1#(1))
(#1=1#(1))
etc.
In article <················@martigny.ai.mit.edu> ···@zurich.ai.mit.edu (William G. Dubuque) writes:
>Does anyone know of a precise specification for CL grammar?
>Most English prose specifications such as those in Steele's CLtL2
>seem to be lacking in precision.
The reader specification in section 22.1.1 is about as precise as you can
get, considering that CL allows reprogramming the lexer using read macros.
It's certainly good enough to answer all your questions.
>For example, how should the following be read:
>
>(#xa#(1))
Unspecified. #x is required to be followed by a rational, and "a#" isn't
valid syntax for a rational (see the grammar in table 22-2).
>(#xa(1))
That should be equivalent to (10 (1)).
>(#1=1#1#(1))
Equivalent to (|1#1#| (1)).
>(#1=1#(1))
Equivalent to (|1#| (1))
A common thread in your examples is confusion between terminating and
non-terminating macro characters. Sharpsign is a non-terminating macro
character, so it's treated as a constituent when it's embedded in a token.
See step 8 of the algorithm in 22.1.1.
--
Barry Margolin
BBN Internet Services Corp.
······@near.net
From: ······@nic.near.net (Barry Margolin)
Date: 10 Feb 1995 05:20:11 -0500
In article <················@martigny.ai.mit.edu> ···@zurich.ai.mit.edu (William G. Dubuque) writes:
>Does anyone know of a precise specification for CL grammar?
>Most English prose specifications such as those in Steele's CLtL2
>seem to be lacking in precision.
The reader specification in section 22.1.1 is about as precise as you can
get, considering that CL allows reprogramming the lexer using read macros.
It's certainly good enough to answer all your questions.
Thanks for your reply. I do not agree that Steele's description
of the reader in anywhere near precise. Granted, someone like you
or I who has been using CL for over a decade can infer what is
meant, but if someone was reading CLtL2 as a spec for
implementation the rigor is lacking. (fyi: I'm implementing a CL
reader for GNU Emacs elisp, and I decided to read CLtL2 to
clarify the fine points).
The primary problem I wanted to illustrate is that Steele states
nowhere how the standard # dispatching macro operates when it
reads the arguments of the macro. For example, what kind of read
or tokenization is performed when reading the 'char object' x in
#\x or what kind of read is performed when reading the feature in
#+feature ? Different implementations may interpret such
differently, e.g:
CLoe ACL/Win
---------- --------
#\x#\y #\x #\y error
(#xa#(1)) (|A#| (1)) error
#+#+ 1 2 3 4 5 5 5
#+ 1 #< 2 2 error
I bet you'll find differing results in other implemetations also.
Granted these are unusual cases, but one cannot have a standard
without absolute precision, especially when it comes to matters
of grammar and syntax.
I would not be surprised if the lack of rigor here stems from the
fact that most CL implementors never used a parser or lexer
generator to generate a reader or lexer but instead compose these
algorithms by hand. Use of a parser or lexer generate would help
to uncover such ambiguities and imprecision.
-Bill
···@zurich.ai.mit.edu (William G. Dubuque) writes:
[ discussion of ambiguous reader syntax deleted ]
> I would not be surprised if the lack of rigor here stems from the
> fact that most CL implementors never used a parser or lexer
> generator to generate a reader or lexer but instead compose these
> algorithms by hand. Use of a parser or lexer generate would help
> to uncover such ambiguities and imprecision.
>
> -Bill
Howdy,
Good point. Are there any 100% portable CL sources
available that implement a Lisp reader and that are PD. Such
a beast could be very valuable to both the Lisp implementor
and user communities. Also a test file that would really
wring out a reader implementation.
Ideally, such a beast would be : (1) very well
commented (2) no implementation dependencies (3) somewhat
"dumbed down" to support various popular but "inferior
Lisp dialects (xlisp? elisp?...) (4) some comments on
how to speed up the implementation and where it matters
(5) pointers to relevant parts of CLtL2 and the ANS
spec and where they differ (if they differ).
=============================================
Scott McLoughlin
Conscious Computing
=============================================
In article <············@sytex.com> ····@sytex.com (Scott McLoughlin) writes:
> Good point. Are there any 100% portable CL sources
>available that implement a Lisp reader and that are PD.
The most likely candidate is probably the reader in CMU CL.
--
Barry Margolin
BBN Internet Services Corp.
······@near.net
[Jeff Dalton]
| Of course one can have a standard without absolute precision!
| Whatever gave you the idea that one couldn't?
wearing my standards-committee member and standards writer hat for a second
or two (it hurts to wear it), a standard with absolute precision must be
about things for which absolute precision makes sense, such as dimensions
of physical objects such as those for mechanical and electrical
engineering. however, even they will not enumerate everything that will go
wrong if you do something that is outside of the scope of the standard.
defining the scope of a standard is the hardest part of the process,
because it defines what you will and will not talk about.
the Lisp reader as defined does not detail what will happen to any random
character sequences when presented to it as input, but rather what should
be presented as input to that reader when a particular set of results is
expected and desired. I think this is no different from any other syntax
description, formal or informal.
| Indeed, can anyone think of a programming language standard that does
| have absolute precision?
modula-2 comes close. its formal semantics is defined using VDM. I also
think Scheme comes close for its semantics. this hinges on an operational
definition of "absolute precision" that makes it possible for the this term
to make sense, and I don't think we have an absolutely precise definition
of "absolute precision" against which anything could be measured.
#<Erik>
--
miracle of miracles. look what the Net dragged in.
In article <·····················@naggum.no> Erik Naggum <····@naggum.no> writes:
>[Jeff Dalton]
>| Indeed, can anyone think of a programming language standard that does
>| have absolute precision?
>
>modula-2 comes close. its formal semantics is defined using VDM. I also
>think Scheme comes close for its semantics.
Of course, the precision of these formal semantics hinges on the precision
of VDM and Denotational Semantics. Are these defined with absolute
precision? And if so, how about the formalism upon which they're defined?
According to Godel's Theorem, no sufficiently powerful formal system can be
defined with absolute precision.
--
Barry Margolin
BBN Internet Services Corp.
······@near.net
On 18 Feb 1995, Barry Margolin wrote:
> According to Godel's Theorem, no sufficiently powerful formal system can be
> defined with absolute precision.
That's interesting, Barmar. This is a bit of a tangent, but I never
thought of Godel's theorem as having much to do with precision. But
probably I don't understand it all that well. I thought it was essen-
tially that in any sufficiently powerful formal system, there are true
statements which can't be proven.
In article <··········@tools.near.net>,
Barry Margolin <······@nic.near.net> wrote:
> Of course, the precision of these formal semantics hinges on the precision
> of VDM and Denotational Semantics. Are these defined with absolute
> precision? And if so, how about the formalism upon which they're defined?
>
> According to Godel's Theorem, no sufficiently powerful formal system can be
> defined with absolute precision.
Errrrm. The sort of systems we're talking about here are nowhere near
to being "sufficiently powerful", surely.
--
Gareth McCaughan Dept. of Pure Mathematics & Mathematical Statistics,
·····@cus.cam.ac.uk Cambridge University, England. [Research student]
In article <··········@lyra.csx.cam.ac.uk> ·····@can.pmms.cam.ac.uk (Gareth McCaughan) writes:
>In article <··········@tools.near.net>,
>Barry Margolin <······@nic.near.net> wrote:
>
>> Of course, the precision of these formal semantics hinges on the precision
>> of VDM and Denotational Semantics. Are these defined with absolute
>> precision? And if so, how about the formalism upon which they're defined?
>>
>> According to Godel's Theorem, no sufficiently powerful formal system can be
>> defined with absolute precision.
>
>Errrrm. The sort of systems we're talking about here are nowhere near
>to being "sufficiently powerful", surely.
Actually, I'm pretty sure they are. A denotational semantics is
rather like an interpreter in lambda-calculus.
-- jeff
In article <··········@cogsci.ed.ac.uk>,
Jeff Dalton <····@aiai.ed.ac.uk> wrote:
>In article <··········@lyra.csx.cam.ac.uk> ·····@can.pmms.cam.ac.uk (Gareth McCaughan) writes:
>>> According to Godel's Theorem, no sufficiently powerful formal system can be
>>> defined with absolute precision.
>>
>>Errrrm. The sort of systems we're talking about here are nowhere near
>>to being "sufficiently powerful", surely.
>
>Actually, I'm pretty sure they are. A denotational semantics is
>rather like an interpreter in lambda-calculus.
I think we may be slightly at cross-purposes here.
The trouble is that the remark I quoted and commented on (>>> above) is
ambiguous; it might be about
1/ what is valid syntax in the system,
or about
2/ what the system "does" with a given piece of valid syntax.
This is made worse because in certain ways 2/ can be treated as a special
case of 1/, with a different system. (Consider the axioms and rules of
derivation as being definitions of valid grammar.)
And there's another ambiguity: suppose we take meaning 2/; what does
defining a system actually mean? It might be
1/ describing the process by which input is processed,
or
2/ giving a simple (meaning primitive recursive, or something)
description of what output results from given input.
With meaning 1/, obviously any computer language can be defined with
complete precision (provide an implementation of the language, and
define the language in terms of the implementation); with meaning 2/,
things are rather different. Godel-type problems only arise with
(2/, case 2/), or with languages whose *syntax* is Turing-powerful,
so to speak.
Now, I thought the sort of thing we were discussing was [originally]
the way the CL reader deals with its inputs, and [later] specifications
of computer languages in standards.
In either case, it is possible to specify the behaviour completely
and precisely, by (for instance) providing an actual implementation
and decreeing that correct behaviour is behaviour identical to that
which the specified implementation exhibits.
So what I should really have said was that Godel's theorem isn't
really relevant. The statements Godel's theorem *does* refute are
statements like
It is possible to determine, for any program in language X, whether
it will run forever, and what output it will produce.
But I don't think anyone was suggesting anything of that sort.
Of course I could produce a programming language whose valid programs
weren't definable in a useful way: for instance, by decreeing that only
programs which always terminate are legal syntax. But most languages
do *not* have that sort of problem with their syntax, and most languages
can be defined (in the only sense that matters) perfectly precisely,
despite Godel's theorem.
Perhaps I've misunderstood the remark about Godel's theorem; if so,
some clarification as to what *was* meant would be welcome.
--
Gareth McCaughan Dept. of Pure Mathematics & Mathematical Statistics,
·····@cus.cam.ac.uk Cambridge University, England. [Research student]
In article <··········@lyra.csx.cam.ac.uk> ·····@owl.pmms.cam.ac.uk (Gareth McCaughan) writes:
>In article <··········@cogsci.ed.ac.uk>,
>Jeff Dalton <····@aiai.ed.ac.uk> wrote:
>>In article <··········@lyra.csx.cam.ac.uk> ·····@can.pmms.cam.ac.uk (Gareth McCaughan) writes:
>
>>>> According to Godel's Theorem, no sufficiently powerful formal system can be
>>>> defined with absolute precision.
>>>
>>>Errrrm. The sort of systems we're talking about here are nowhere near
>>>to being "sufficiently powerful", surely.
>>
>>Actually, I'm pretty sure they are. A denotational semantics is
>>rather like an interpreter in lambda-calculus.
>
>I think we may be slightly at cross-purposes here.
Well, I didn't bring in the Godel stuff (it was Barmar).
>The trouble is that the remark I quoted and commented on (>>> above) is
>ambiguous; it might be about
> 1/ what is valid syntax in the system,
>or about
> 2/ what the system "does" with a given piece of valid syntax.
>
>[...]
>
>And there's another ambiguity: suppose we take meaning 2/; what does
>defining a system actually mean? It might be
> 1/ describing the process by which input is processed,
>or
> 2/ giving a simple (meaning primitive recursive, or something)
> description of what output results from given input.
>
>With meaning 1/, obviously any computer language can be defined with
>complete precision (provide an implementation of the language, and
>define the language in terms of the implementation);
You might define language A by an implementation in A.
This used to be done (e.g. so-called "definitional interpreters")
and has some problems (such as multiple fixed points). And if
you define language A by an implementation in language B, which
is more or less what a formal definition does, you need a
precise definition of B.
(Actually, I like definitional interpreters and I know about
Henry Baker's paper on defining CL macros and forms in terms
of other ones -- I say this only to head off some postings
that would otherwise be called for.)
> with meaning 2/,
>things are rather different. Godel-type problems only arise with
>(2/, case 2/), or with languages whose *syntax* is Turing-powerful,
>so to speak.
Like Algol 68. ^_^
>Now, I thought the sort of thing we were discussing was [originally]
>the way the CL reader deals with its inputs, and [later] specifications
>of computer languages in standards.
Right. And when specs in standards try to be absolutely precise,
they resport to formal definitions of the syntax and a semantics.
But actual standards tend to leave some things undefined even then
(e.g. the order of arg evaluation in Scheme).
>In either case, it is possible to specify the behaviour completely
>and precisely, by (for instance) providing an actual implementation
>and decreeing that correct behaviour is behaviour identical to that
>which the specified implementation exhibits.
I don't know of any standard that works that way unless the
"actual implementation" is in some formal system such as VDM
or denotational semantics.
But let's consider a different example. An actual implementation in,
say, C isn't enough because the C standard isn't absolutely precise
and the implementation may be use implemention-defined parts of
the language. So how about an implementation in C, but compiled
and run on specified hardware? You'll have to go at least that
far.
>So what I should really have said was that Godel's theorem isn't
>really relevant. The statements Godel's theorem *does* refute are
>statements like
> It is possible to determine, for any program in language X, whether
> it will run forever, and what output it will produce.
>
>But I don't think anyone was suggesting anything of that sort.
I'm not sure exactly what Barmar had in mind by bringing in Godel.
--jeff
In article <··········@gap.cco.caltech.edu>, Seth LaForge
<······@off.ugcs.caltech.edu> wrote about Godel's Theorem, and about
Barry Margolin's <······@nic.near.net> guess that it was applicable to
the notations used to describe the formal semantics of programming
languages <··········@tools.near.net>. Seth went on to say:
>For a very good, easy to follow (or as easy as is possible) discussion
>of Godel's theorem, as well as quite a few other
>philosophical/mathematical/computer scientific things, see Douglas
>Hofstadter's excellent book _Godel, Escher, Bach: an Eternal Golden
>Braid_.
Hofstadter's book is of course a tour de force, and a brilliant
attempt to make difficult ideas accessible to a more or less
non-technical audience. Individual chunks of it are very easy to
follow, and it gives you a good top-level view of the argument.
However, it's a very long complicated book. Hofstadter is consciously
attempting to make the structure of his text reflect the matter of his
argument, and I find this makes it difficult to follow.
Technical people are likely to find Boolos, G.S. & Jeffrey, R.C:
_Computability and Logic_: Cambridge University Press, 2nd Edition
1980: ISBN 0 521 23479 4 easier to work with, as it's much shorter
and isn't coy about using formal notation and a clear technical
exposition (but it's also much less fun).
--
------- ·····@rheged.dircon.co.uk (Simon Brooke)
;; I'd rather live in sybar-space
In article <··········@rheged.dircon.co.uk>, ·····@rheged.dircon.co.uk
(Simon Brooke) wrote:
> In article <··········@gap.cco.caltech.edu>, Seth LaForge
> <······@off.ugcs.caltech.edu> wrote about Godel's Theorem, and about
> Barry Margolin's <······@nic.near.net> guess that it was applicable to
> the notations used to describe the formal semantics of programming
> languages <··········@tools.near.net>. Seth went on to say:
Why don't you read the master himself? For $4.95 at your local bookstore,
no less!
Godel, Kurt. On Formally Undecidable Propositions of Principia Mathematica
and Related Systems. Transl. B. Meltzer. Dover Publs., NY 1992.
ISBN 0-486-66980-7.
I have found that in many cases, the guy who originates the idea usually
provides the best motivation for what he is doing. Too many of the
'reformatters' kill the motivation, and without it, too many rabbits
get pulled out of the hat. (Perhaps this is in that fine tradition of
mathematics -- to cover all tracks of how a proof was discovered.)
--
www/ftp directory:
ftp://ftp.netcom.com/pub/hb/hbaker/home.html
In article <················@martigny.ai.mit.edu> ···@zurich.ai.mit.edu (William G. Dubuque) writes:
>Does anyone know of a precise specification for CL grammar?
>
>Most English prose specifications such as those in Steele's CLtL2
>seem to be lacking in precision.
>
>For example, how should the following be read:
>
>(#xa#(1))
Error, because # is a non-terminating macro char and hence part of
what #x will read. Then, a# is not a hex number.
>(#xa(1))
(10 (1))
>(#1=1#1#(1))
(1#1# (1)), where 1#1# is a symbol. You made #1 = to that symbol.
>(#1=1#(1))
(1# (1)), where 1# is a symbol. You made #1 = to that symbol.
>etc.
The key is that # is not a terminating macro and that it's an
alphabetic "costituent" when not treated as a macro.
-- jeff