Re: Denotational semantics for lazy / strict functional programming languages

Dirk, thank you for your excellent reply.

Firstly, your comments on notation are gratefully received.
To simplify the discussion I won't address them here.

I think of the language (say, a variant of the lambda
calculus) and the possible semantics of the language
seperately.

Interesting. I think of the semantics as part of the
language. But such a philosophical point is better discussed
in a different thread (if at all ;).

one usually defines the interpretation with respect to the
\rho, and extends it as when interpreting function
abstraction [...]

The way you do it is more "by example", but doesn't cover
the general case (you would notice when you tried to do a
proof with it).

Everything you say here is correct. I was being lazy.

I don't understand why you use a single bracket notation
for the strict semantics. The usual way is to assume given
CPOs for the base types, and just interpret function types
as also *strict* mappings. So there's no need to juggle
with both [T] and [[T]].

The interpretation of application in strict semantics
looks unnecessarily complicated. If you know you have only
strict functions, normal function application will do.

[...] It's also not clear why you don't need the type
restrictions in the lazy case, why you need them in the
strict case, and why you don't assume T->T instead T->U in
the lazy case.

I'll address all these issues together, as it's key to why I
sent the question to the newsgroup in the first place.

In the lazy case, there is no problem. As far as I can
tell, the least fixpoint of the denotation [[F]] of a
function F:T->T is just the one you want for the
denotation of [[mu F]]. (An example *I think* would be the
least fixpoint of the function "\ones -> 1:ones" which is
the infinite list of ones. Note that I'm using Haskell
notation there. This is only possible in a lazy language.)

Consider the same construction in the strict case (using
strict function spaces as you suggest). The least fixpoint
of any [[F]]:[[T]]->[[T]] is always _|_. This is clearly not
a suitable value for [[mu F]], so we have to find an
alternative definition for [[mu F]]. My solution to this
explains the complexity of the semantics I've given. But how
is it usually done?

2. (Assuming Q1) Can I rely on results that relate the
semantics I give with suitable operational semantics?

[...] If you use the usual ones, well, the theorem that
they match is common knowledge, so you can rely on it.

Good. Hopefully I be able to get a definition close enough
to usual ones so that I can rely on the theorem(s).

3. What would be the significance of using monotonic function
spaces rather than continuous function spaces?

A monotonic function space doesn't have unique fixpoints, IIRC.
It's not a CPO resp. DCPO.

Actually, it is a CPO (you define directed joins pointwise;
see, for example, Lemma 8.5 of Davey & Priestley's
"Introduction to Lattices and Order"). So fixed points
should still exist. Nevertheless, I'm still interested in
what the ramifications of using monotonic function spaces
might be.

Again, thanks for your comments. They were very much
appreciated.

Malcolm.

.

Relevant Pages