Re: Formal semantics of language semantics

Nick Maclaren <nmm1@cus.cam.ac.uk> wrote:
>> It is true that the van Wijngaarden grammar used to define
>>Algol 68 in the RR did not attempt the semantics; but it is *also*
>>true that vW grammars *can* be used to define semantics%, [...]
>Um. I am not sure. I agree that it can be used to define SOME OF
>the semantics, yes. The question is whether it can be extended to
>the nastier, more context-dependent and less structured aspects.
>I was answering the question "Can they be used to define ALL of
>the semantics?" [...]


The answer is still "yes". It is "easy" to write a vW grammar
to emulate a universal Turing machine, and "hence" to write a vW
grammar that does anything whatsoever that is "interesting", In
particular, for example, you could write a "reference" C compiler in a
vW grammar that imported the C code for a program, put it through all
the phases of macro- expansion, etc., and "compiled" it into byte code
for some standard machine [virtual or real], then "ran" the byte code
with as much or as little ambiguity as the standard required. I don't
know how much closer you could ever expect to come to defining all, or
even ALL, the semantics.


>The aspects that I was trying to define formally were things like
>aliasing rules in an Algol/Fortran/C-like language, [...]


Yes. If you can build such things into a compiler, for either
static or dynamic checking, you can build them into a vW grammar.


> I have never seen a language
>that defined such things formally, for a sufficiently general and
>practical model, nor even a book that addressed them seriously :-(


There are rather few books that address vW grammars seriously
at all. You already *know* how difficult many people find the vW
grammar that defines just the grammar of Algol 68; no practical
language is going to be significantly simpler, and many [most?
certainly C and C++] are going to be much worse. Add in the semantics
as well, and you're going to have a book two or three times the length
of the Algol RR, just to give a formal definition of C. [Mind you,
that might well be better than the present situation, where the
standard definition of C is already longer than that of Algol 68 and
yet people still argue about whether some given code is correct C.]


>The issue with all of those is that they are inherently dynamic
>and involve the interactions between a potentially unbounded and
>not statically specified collection of objects.


This is not a problem for a 2-level grammar; as with the RR
definition of Algol, you use one level to define an unbounded
collection of grammar rules for the other.


>Languages like ML attempt to avoid hand-waving, but they deal with
>a lot of such problems by denying their existence. This is very
>obvious in the second example I gave, where the effective language
>definition starts "Assuming a perfect garbage collector, ..."


So the vW grammar could include a construct to free all
inaccessible storage after each and every pointer assignment or stack
reduction. Virtually free in the grammar [exc that someone has to
write the GC algorithm], however impractical in real life.


> The
>same is true of aliasing, where they make the Algol/Fortran/C issues
>'impossible', but without resolving the underlying problem.


"Similarly ...." Keep in the grammar a model of the storage
[cf the RR "NEST", but now it's maintained at "run time" as well as
during compilation], add an aliasing predicate to the grammar, and
check as necessary.


> And
>similarly with exception handling, where practical programmers are
>dealing with necessarily unclean exceptions.


Build it into your byte code .... Whatever your hardware
can do, a vW-grammar emulation of it can do the same.


I repeat -- the only *real* problem is that doing it generates
*huge* grammars that have *ginormous* productions. We're talking
large books to include the grammar, and large universes to include the
productions.


--
Andy Walker, School of MathSci., Univ. of Nott'm, UK.
anw@maths.nott.ac.uk

Return to the comp.compilers page.
Search the comp.compilers archives again.