Re: Formal semantics of language semantics

"Mark" <whopkins@alpha2.csd.uwm.edu> writes:
|> "Nick Maclaren" <nmm1@cus.cam.ac.uk> writes:
|> >Now, in the case where this is provably safe, it is quite possible
|> >that the proof involves some quite high-level mathematics. E.g.
|> >the path switches might involve two properties that are related
|> >only through the Extended Riemann Hypothesis.
|> >
|> >Can you handle that semantic constraint?
|>
|> Merely asking this question, itself, provides a perfect illustration
|> of the problem I was referring to. What you're asking for to be done,
|> which is exactly what a semantics traditionally tries to do, is indeed
|> the very mistake I'm referring to -- (re)quoted for emphasis below:
|>
|> Mark <whopkins@alpha2.csd.uwm.edu> wrote:
|> >[...] a somewhat illucid attempt to try and cram things that don't
|> >belong together into a single monolithic formalism, without further
|> >factoring out
|> ^^^^^^^^^^^^^
|>
|> The question of the semantic constraint you brought up and the question of
|> control flow semantics don't belong together. The latter is factored out
|> at the syntatic level -- as shown in both that article and illustrated
|> in the case of several semantic formalisms.


What you seem to be saying is that certain semantic constraints should
not be expressible in a language specification, which is a statement
about language design and not about the formal semantics of a
particular language. The simple fact is that, in almost all
programming languages, the control flow can vary arbitrarily (in a
halting problem sense) according to the data.


I have actually seen programs where the constraint I referred to was
inherent in the problem. They are fairly rare, but not as rare as all
that. The situation was that some of the apparently possible control
flow was illegal, but it was possible to prove that it could not occur
using higher mathematics than that used in the program!


So, do tackle a more restrictive problem if you like, but please don't
say that the more general one isn't important. It is.




Regards,
Nick Maclaren,
University of Cambridge Computing Service,
New Museums Site, Pembroke Street, Cambridge CB2 3QH, England.
Email: nmm1@cam.ac.uk
Tel.: +44 1223 334761 Fax: +44 1223 334679

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