Article View: comp.specification
Article #394Re: Semantic definition style
From: Peter D. Mosses
Date: Mon, 16 Nov 1992 10:42
Date: Mon, 16 Nov 1992 10:42
65 lines
4016 bytes
4016 bytes
In article <2930740056.0.p00117@psilink.com>, "Ian Sutherland" <p00117@psilink writes:
>Peter Mosses writes:
>>In article <1992Nov11.195443.23006@cis.ohio-state.edu>, ogden@seal (William F Ogden) writes:
>>>operational semantics produce a
>>>welter of irrelevant information (computational histories), from which the
>>>essential information (the input/output pairs, in the case of sequential
>>>programs) must be extracted.
>>
>>But the denotations of statements, declarations, etc., are not I/O
>>relations! They necessarily deal with *auxiliary* entities, such as
>>environments and stores, whose relevance to particular implementations
>>is not nearly so direct as that of the I/O relation.
>
>I don't think the original poster meant "input/output" to refer simply
>to what, say, an OS designer would call "input/output". Certainly those
>who design denotational definitions do not so limit themselves. Both
>"input" and "output" usually include the memory and the environment.
Regarding a semantic description as a requirements specification for
implementations, it seems to me that the denotational semantics of an
entire program should indeed be a function from OS inputs to OS
outputs (at least when assuming batch I/O and determinism).
>>>Now algebraic semantics would seem to be predicated on the dubious
>>>proposition that computation is entirely describable within a limited
>>>first-order subarea of mathematics -- namely algebra.
>>
>>- which can specify Turing machine computations, and hence is
>>universal.
>
>But Turing machines are only "universal" in exactly the sense you took
>issue with above, namely, they are universal in the sense that they can
>produce any recursive input/output function. I don't think Turing
>machine COMPUTATION (reading/writing head moving back and forth, reading
>and writing symbols on individual squares and changing internal state)
>is in some sense a universal model of computational PROCESSING. Does
>anyone know otherwise?
I wasn't advocating the use of Turing machines in semantics! I was
reacting against the suggestion that there is something essentially
*higher-order* about computation and the semantics of programming
languages. In my view, first-order approaches are quite adequate.
(Action semantics is, as you might have guessed by now, first-order.
However, it provides notation for going back and forth between actions
and corresponding data items; this is analogous to an isomorphism
between [D->D] and D in domain theory.)
Perhaps the notion of *action* used in action semantics comes close to
what you'd call a `universal model' of processing? It encompasses the
conventional functional, imperative, and concurrent paradigms of
computation. However, there are certainly some forms of computation
(e.g., interrupts, general continuation-handling) that it doesn't
support directly. And even if one incorporated those, programming
language designers could presumably come up with new ones...
>---
>Ian Sutherland
>ian@eecs.nwu.edu
>
>Sans Peur
--
Peter D. Mosses | Computer Science Department | <pdmosses@daimi.aau.dk>
~~~~~~~~~~~~~~~ | Aarhus University | Phone: +45 86 12 71 88
| Ny Munkegade, Building 540 | Fax: +45 86 13 57 25
| DK-8000 Aarhus C, Denmark | Telex: 64767 aausci dk
Technical Details
Message-ID:
<1992Nov16.104205.3842@daimi.aau.dk>Path:
arc1-ca.pugleaf.net!sparky!uunet!mcsun!sunic!dkuug!daimi!pdmReferences:
<2930740056.0.p00117@psilink.com>Show Full Headers
Complete Article Headers
Newsgroups: comp.specification Path: arc1-ca.pugleaf.net!sparky!uunet!mcsun!sunic!dkuug!daimi!pdm From: pdm@daimi.aau.dk (Peter D. Mosses) Subject: Re: Semantic definition style In-Reply-To: "Ian Sutherland" <p00117@psilink.com> Message-ID: <1992Nov16.104205.3842@daimi.aau.dk> Summary: semantics can be first-order Keywords: semantics, first-order, higher-order, actions Sender: pdm@daimi.aau.dk (Peter D. Mosses) Reply-To: pdm@daimi.aau.dk (Peter D. Mosses) Organization: DAIMI: Computer Science Department, Aarhus University, Denmark References: <2930740056.0.p00117@psilink.com> Date: Mon, 16 Nov 92 10:42:05 GMT Lines: 65