<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
<font face="Arial">One can certainly use an operational semantics such
as bisimulation, but you don't have to abandon denotational semantics.
The trick is to make output part of the "final answer". For a
conventional imperative language one could define, for example, a
(lifted, recursive) domain:<br>
<br>
Answer = Terminate + (String x Answer)<br>
<br>
and then define a semantic function "meaning", say, such that:<br>
<br>
meaning loop = _|_<br>
meaning loop' = <"x", <"x", ... >><br>
<br>
In other words, loop denotes bottom, whereas loop' denotes the infinite
sequence of "x"s. There would typically also be a symbol to denote
proper termination, perhaps <>.<br>
<br>
A good read on this stuff is Reynolds book "Theories of Programming
Languages", where domain constructions such as the above are called
"resumptions", and can be made to include input as well.<br>
<br>
In the case of Clean, programs take as input a "World" and generate a
"World" as output. One of the components of that World would
presumably be "standard output", and that component's value would be
_|_ in the case of loop, and </font><font face="Arial"><"x",
<"x", ... >> in the case of loop'. Another part of the World
might be a file system, a printer, a missile firing, and so on.
Presumably loop and loop' would not affect those parts of the World.</font><br>
<font face="Arial"><br>
If returning one World is semantically problematical, one might also
devise a semantics where the result is a sequence of Worlds.<br>
<br>
-Paul<br>
<br>
</font><br>
Arnar Birgisson wrote:
<blockquote
cite="mid:28012bc60711010759v1b0bb734hb77fae9b9a43cc7a@mail.gmail.com"
type="cite">
<pre wrap="">Hi there,
I'm new here, so sorry if I'm stating the obvious.
On Nov 1, 2007 2:46 PM, apfelmus <a class="moz-txt-link-rfc2396E" href="mailto:apfelmus@quantentunnel.de"><apfelmus@quantentunnel.de></a> wrote:
</pre>
<blockquote type="cite">
<pre wrap="">Stefan Holdermans wrote:
</pre>
<blockquote type="cite">
<pre wrap="">Exposing uniqueness types is, in that sense, just an alternative
to monadic encapsulation of side effects.
</pre>
</blockquote>
<pre wrap="">While *World -> (a, *World) seems to work in practice, I wonder what
its (denotational) semantics are. I mean, the two programs
loop, loop' :: *World -> ((),*World)
loop w = loop w
loop' w = let (_,w') = print "x" w in loop' w'
both have denotation _|_ but are clearly different in terms of side
effects. (The example is from SPJs awkward-squad tutorial.) Any pointers?
</pre>
</blockquote>
<pre wrap=""><!---->
For side-effecting program one has to consider bisimilarity. It's
common that semantically equivalent (under operational or denotational
semantics) behave differently with regard to side-effects (i/o) - i.e.
they are not bisimilar.
<a class="moz-txt-link-freetext" href="http://en.wikipedia.org/wiki/Bisimulation">http://en.wikipedia.org/wiki/Bisimulation</a>
Arnar</pre>
</blockquote>
<br>
</body>
</html>