[Prev][Next][Index][Thread]

[sieber: denotational versus operational semantics]

Date: Wed, 25 May 88 14:31:05 +0200 (MET dst)


Date: Tue, 24 May 88 17:28:43 EST
From: sieber
To: meyer%THEORY.LCS.MIT.EDU@unido.uucp, matthias@rice.edu@unido.uucp
Subject: denotational versus operational semantics


In my eyes your (and I mean both of you) emphasis on operational
semantics is too strong.  How about this view:
  
A programming language is not defined by rewrite rules but by CONCEPTS
like 'values', 'states', 'state transformations', which exist (at
least in the intuition of its designers) BEFORE anyone invents rewrite
rules.  Denotational semantics is a tool for expressing such concepts
mathematically.  (Hence a very important aspect of a denotational
semantics should be, that it really meets our intuition about the
programming language; possibly we haven't paid enough attention to
this issue, because we concentrated too much on other aspects like
full abstraction.)  Operational semantics comes AFTERWARDS.  It is
only necessary for making our programs executable on a computer, not
for understanding them.  IT must be adequate, if we compare it with
the original intuition (formalized by denotational semantics).  Of
course there must be compromises: If the implementation of our
original programming language---defined by concepts---turns out to be
too inefficient (or even impossible), then we have to change it.  But
that still doesn't mean that "operational semantics comes first", 

The simplest example for this view are typed lambda-terms.  Aren't
they a formalization of the (mathematical) concept 'function'?  Aren't
the rewrite rules precisely defined in a way that allows us to think
about lambda-terms as functions?

What is wrong with that view?  Or do you agree with it and I only
misunderstand you? 

Kurt.

--------------------

Date: Tue, 24 May 88 17:47:27 edt
From: "Albert R. Meyer" <meyer%THEORY.LCS.MIT.EDU@unido.uucp>
To: sieber%fb10vax.sbsvax@sbsvax.uucp
Cc: matthias@rice.edu
In-Reply-To: "Kurt Sieber"'s message of Tue, 24 May 88 17:28:46 +0200 (MET dst) <8805241528.AA25293@fb10vax.sbsvax.uucp>
Subject: denotational versus operational semantics
Return-Path: <unido!uunet!THEORY.LCS.MIT.EDU!meyer> (from sbsvax.uucp)

Personally, I mostly agree with your view that semantics has priority, but I
regard the view as somewhat controversial.

For example, an opposing view is that, while there obviously must be an
intuitive idea of recursively declared function in the mind of the
programming language designers preceding its appearance in the syntax of a
programming language, many folks would argue that the intuitive
idea of recursive function was a ``constructive'' idea based a copy-rule-like
understanding.  In other words, the intuitive ideas of ``functions'' and
``values'' are operational notions from the start---just vaguer than the
precise rewrite rules which come later.

This view gets some support from the history of McCarthy's ideas while he was
developing LISP and also I think from the ALGOL designers' writings.

I suspect that prior to both operational and semantical views are logical
views.  Designers start off with an idea of the THEORY of how their language
will behave, including presumptions, eg, that equational reasoning will be
applicable to some degree in reasoning about recursive declarations (whence
the copy-rule), that ``functions'' in the language will satisfy an
extensionality axiom, etc.

This is why I am content to work with a model which is NOT fully abstract, so
long as it can be used in conjunction with logical means for proving
observational congruences.

Regards, A.

P.S. Would you forward your comment and this reply to TYPES?