Re: Formal semantics of language semantics

<i.dittmer@fh-osnabrueck.de> wrote:
>> Are there any notations commonly used to define the semantics of a
>> programming language? (Similar to how BNF defines the syntax).
>
>Many. All two-level-grammars (van-Wijngarden, affix, extended affix
>(also used to describe whole compilers formally), attribute (also for
>compilers),...), denotational semantics, fixpoint semantics, predicate
>semantics, Wiener definition method (used for PL/I), and so on and so
>on...


This reminds me that I have a book:
    David A. Schmidt, "Denotational Semantics".


I find this book useful to look into from time to time to figure out some
common computer language definitions.


Essentially, if one wants to define the semantics expressed by computer
language, then on ends up at classifying the semantic components that is
used by the computer languages. Such classification is a common approach
in (pure) mathematics, as well.


Then, in a computer, one ends up on the problem that the components may
not have efficient implementation, which I think is why many computer
language definitions avoid a formal approach of defining the semantics: It
does not really help the practical nature of language implementation.


As an alternative to that, formally defining the semantics of the whole
language, one may take the approach of only classifying a certain subset
of the runtime semantics, accepting that these are to be used for high
level communications, says between different computer languages or even
computers. One then ends up on approaches like CORBA, I think: If
different computers should be able to work together, somehow a common
binary model must be defined for the objects one use in communication.


I developed such a communication or runtime model, with the point that
lambda calculus can be expressed via it:


Each runtime object f has an evaluation mechanism by which it can take a
reference of an object x, and after evaluation return a reference to
another object y. One might write this process as y = f(x), or even better
something like
        f(x) ~> y
expressing the causality taking place in computer (unlike mathematical logic).


Now, when I implemented the lambda calculus like that, I arrived at a
variation of a series of runtime objects for free and bound variables,
lambda expressions etc, plus that the runtime object must understand the
substitution process, that are in effect the components of runtime
"closures". If I would take this process further to define an underlying
common binary model for these objects, then I would arrive at a variation
of lambda calculus implementation that is independent of the languages and
evaluates by communication alone.


But the reason that computer folks is not using such an approach is that
it would not be efficient. On the other hand, by not using such general
methods, one is loosing generality in the sense that sufficiently general
objects (in the structural sense) cannot be manipulated: For example, it
is uncommon in functional languages that they admit treating the lambda
binder as an object for manipulation (in the runtime model above it shows
up as a runtime constructor for bound lambda expressions), or good
intercommunication with other functional languages or even only in a
distributed sense.


So I think one will have a series of tradeoffs here, more general but less
implementation efficient approaches against the more special more
efficient implementation approaches.


    Hans Aberg * Anti-spam: remove "remove." from email address.
                                    * Email: Hans Aberg <remove.haberg@member.ams.org>
                                    * Home Page: <http://www.matematik.su.se/~haberg/>
                                    * AMS member listing: <http://www.ams.org/cml/>

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