[Prev][Next][Index][Thread]
Re: semantics for F_{sub,rec} ??
> "if it turns out as built on sand (in the sense that it lacks a good
> semantics for the target language used in these translational
> interpretations)."
>
> Would you mind illustrating this "building on sand" portion of your
> letter with, oh say, one or two practical examples?
> - How would programmers suffer from a lack of a classical semantics?
> - How would programming language researchers suffer?
> - What can go wrong?
what I meant was that it POTENTIALLY builds on sand as the target language
of the translation hasn't a much clearer semantics then the source language;
in particular, the FOOL book uses as target language a higher order
polymorphic lambda calculus with subtyping, recursion and STATE; this latter
aspect hasn't been investigated at all; what comes to my mind is the vague
possibility of using computational monads (in this case the state monad) but
it isn't evident that one can build models of this calulus using the Kleisli
category on PERs for the state monad
another problem I have with the target language is that the recursive types
are not initial/terminal algebras for some functor; such a desire is not
pure categorical fetishism because being an initial/terminal solution gives
rise to reasoning principles as in Paulson's book, namely that the least
endomorphism of the solution is identity; this gives rise to Pitts' Theorem
from 1996 which Bernhard Reus and I have used for proving unique existence of
Object Specifications `a la Abadi and Leino
(http://www.cogs.susx.ac.uk/users/bernhard/lics02.ps).
I mean in a sense that situation w.r.t. this translational semantics is a bit
like denotational semantics of Strachey before Scott interfered and provided
a precise semantics for the target language; I can well imagine that target
language not having a well established model is not that important for
practical purposes; but, maybe, you will understand that from the semanticist's
point of view the situation is somewhat unsatisfactory
the intention of my mail was to find out waht was the state of the art in the
field and I received fairly honest and clarifying answers, anmely that for
higher order polymorphism the situation is non-well setted at all
my personal view of the situation is as follows: work with untyped models
and then consider specifications as predicates or pers on this untyped
universe; these polymorphic calculi as used in the FOOL book are a certain
macro languages for particular relatively simple, but practically most relevant
such specifications; I never denied that most types have a clear meaning as
a per on the universe BUT some don't (at least not in an evident way)
anyway, one could enter an endless discussion of what comes first: syntax or
semantics; I, personally, am in favour of semantics but bI am aware of that
one needs both sides of the coin; therefore, I remain sceptical w.r.t. coins
having just one side...
I apologize again for the slightly exaggerated formulation "built on sand"
(I should have added "potentially"); but I was slightly provoked by the
impression conveyed in various papers and books that there were no problem
with the semantics of the target language; I have now learnt from the experts
that this not so at all and that my doubts are justified to some extent; I am
grateful for this honesty! also, I must say, I found it profitable to read
some of the above mentioned papers in the sense that it clarified a lot of
things usually hidden by OOP speak
hope this clarifies my view
Thomas
Follow-Ups: