Re: specifying semantics, was Formatting of Language LRMs

On Tue, 24 Jun 2014 02:19:05 -0700 (PDT), seimarao@gmail.com wrote:


>Is there something for semantics as BNF is for grammars ?


First, there is no canon BNF. What we refer to as "Backus-Naur Form"
today is not the original used for Algol-58, but is BNF plus a handful
of widely accepted practical extensions - alternation set notation,
closure notation, etc. - which together is known as EBNF ('E' for
"extended") or sometimes "core" EBNF.


Core EBNF is easily (but not trivially) portable: every popular
grammar tool understands it in concept, but not every tool uses
exactly the same rule syntax.


In addition, nearly every tool extends core EBNF to enable its own
unique features. Grammars taking advantage of any feature not in core
EBNF generally will not be portable (not trivially and possibly not
even easily) to a different tool.




To answer your question: No ... there really is nothing for semantics
that approaches the ubiquity of EBNF for grammars. The closest thing
in practice is the lambda calculus, but there are multiple forms of
the calculus and you'll find that every author extends their chosen
form in some slightly different way.




Moreover, there are 3 broad categories of semantic description:
operational, denotational and axiomatic. Lambda calculus really is
suitable only for expressing operational and/or denotational forms.
Axiomatic descriptions generally take the form of a propositional
algebra.


Historically, *most* languages have been described by operational
semantics alone, and the majority did not use any formal calculus to
do so. The most common form of description is, in fact, text - in
conjunction with a "reference" implementation: a compiler or
interpreter against which new implementations can be compared.


Scheme, ML and Haskell are described by denotational semantics. There
undoubtedly have been others but these are the ones I know offhand.


I'm not aware any languages that are described solely by axiomatic
semantics [possibly some of the declarative logic or theorem prover
languages, but I'm not very familiar with any of these]. AFAIHS,
axiomatic descriptions tend to be more for the developer of a compiler
than for the user of it. When the language gets documented, it tends
to be using an operational or denotational description.




>What do the books on type systems, lambda calculus, etc, teach and
>where are their topics applied ?


Read some and find out.


George

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