Re: Denotational semantics for lazy / strict functional programming languages

MalcolmTyrrell <malcoh0l@xxxxxxxx> wrote:
I'm trying to find a standard and fixed presentation of the
denotational semantics of functional programming languages. In
particular, I'd like one which includes the semantics of both lazy and
strict languages.

I am not sure what you mean by that -- usually, I think of the language
(say, a variant of the lambda calculus) and the possible semantics of
the language seperately. So one would have a single language with
strict semantics on the one hand and lazy semantics on the other hand,
but not a "strict language" and a "lazy language".

I've put the note here:
http://webpages.dcu.ie/~tyrrelma/DenotationalSemantics.pdf

Ok, I had a quick look. I hope I didn't miss anything major.

The questions I'm interested in are:

1. Have I done it the / a standard way?

Most of it looks standard. Continuous functions are normally just
written as an arrow between domains (without the 'c'). One possible
notation to emphasize strictness in function is adding a '!'.

I haven't seen the notation with sub- and superscript for a
particular environment \rho that maps x to y. Also, one usually
defines the interpretation with respect to the \rho, and extends it as
when interpreting function abstraction (There are several notations
for extending \rho, pick the one you like best :-).

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).

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]].

Your interpretation of function abstraction is a bit awkward because
you use \lambda both on the formal side and to define an actual
denotational function. Maybe it would be clearer to use the usual
mathematical way of defining functions, with a definition by cases
(bottom is always mapped to bottom) for the strict semantics.

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

I don't understand your treatment of the fixpoint operator (both
for lazy and strict semantics). If you already use type annotations
inside lambdas, then maybe a typed version like \mu x:T.t would
be better (that would correspond to \mu (\lambda x:T.t) in your notation).
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.

Oh, and the dot after the lambda is usually just the "full stop",
not \cdot.

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

I don't understand the question. If you give operational semantics and
denotational semantics, you have to show that they match. If you use
the usual ones, well, the theorem that they match is common knowledge,
so you can rely on it.

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.

Fixpoints should still exist, but would it effect the answer to
question 2?

Well, you cannot interpret fixpoint constructions in the first place,
because there's no unique fixpoint. If you pick just any fixpoint,
you'd have to show that the operational semantics match the
denotational semantics. The means you would have to show that all your
functions in the denotation are continous, anyway, otherwise you
wouldn't get the smallest fixpoint as you do in the operational semantics.
But then you could restrict yourself to continous functions right from the
beginning.

4. In your opinion, the notation I'm using is:
[ ] canonical
[ ] standard
[ ] acceptable
[ ] non-standard
[ ] cranky

Many standard things, most acceptable, some unusual.

Any other comments or observations are welcome.

See above.

Thanks for any help,

HTH,

- Dirk

.

Relevant Pages

  • Re: Query regarding Semantic Analyzer
    ... notations commonly used to define the semantics of a programming ... Attribute grammars, Two level Grammar, Denotational Semantics, ... Operational semantics, Axiomatic semantics etc. ... more natural for language designers, ...
    (comp.lang.fortran)
  • Re: Denotaional Semantics
    ... The first denotational semantics for Scheme was developed ... semantics for a language is that it formally encompases *ALL* meaning ...
    (comp.lang.scheme)
  • Re: Denotational semantics for lazy / strict functional programming languages
    ... I think of the semantics as part of the ... I was being lazy. ... as also *strict* mappings. ... strict function spaces as you suggest). ...
    (comp.lang.functional)
  • Re: future of lazy programming
    ... discussion up to this point has implied that choosing strict versus lazy ... evaluation semantics will loop with strict evaluation. ... one really wants lazy evaluation ...
    (comp.lang.functional)
  • Re: [PATCH 1/3 v3] dma: document dma_{un}map_{single|sg}_attrs() interface
    ... ordering semantics. ... and this is a NUMA interconnect thing. ... of the attribute needs to reflect the semantics of what the driver ... strict ordering, all accesses to this mapping are ordered. ...
    (Linux-Kernel)