[Prev][Next][Index][Thread]

[main@boulder.Colorado.EDU: Re: beyond omega]



Date: Mon, 28 Mar 88 16:13:08 EST
From: meyer
To: main@boulder.Colorado.EDU
In-reply-to: Michael Main's message of Tue, 22 Mar 88 20:24:06 MST <8803230324.AA24853@boulder>
Subject:  lists

You haven't asked, but here's a working title for my talk at the May
workshop:
``Remarks on Continuous vs. Monotone, Typed vs. Untyped, Direct vs.
Continuations, Higher-Order Computability vs. Symbol-Pushing, and Related
Controversies,''

As you will realize from the paper below, this will be a early version of the
talk I will give at LICS 88.  I've sent hard copy, but the promised
LaTeX file follows in two messages.

Regards, A. 
----------------------------
Return-Path: <main@boulder.Colorado.EDU>
Date: Tue, 29 Mar 88 09:50:05 MST
From: Michael Main <main@boulder.Colorado.EDU>
To: meyer@THEORY.LCS.MIT.EDU
Subject: Re:  lists

Thanks for the information on your talk.  Sounds like a great title.
I vote for monotone, typed, direct, higher-order.  But perhaps you
will change my mind.

Anyway, you're set up for the 50-minute before lunch talk on
Friday May 20.  Let me know if you need any further arrangements made.

By the way: a number of the talks (particularly in the mornings) will
be of a tutorial nature.  I am considering giving a talk called
"Beyond Omega" to explain why countable limits are not enough when
giving the semantics of programs with countable nondeterminism.
This would give an intuitive explanation of the results of Plotkin
and Apt, stated in terms of relational semantics.  Can you give me a
guess as to how much interest there may be in this topic.  Thanks.

Michael
------------------------------------
Date: Tue, 29 Mar 88 13:42:30 EST
From: meyer
To: main@boulder.Colorado.EDU
CC: allen%cvaxa.sussex.ac.uk @@nss.cs.ucl.ac.uk
In-reply-to: Michael Main's message of Tue, 29 Mar 88 09:50:05 MST <8803291650.AA13123@boulder>
Subject:  beyond omega

`Beyond Omega' sounds interesting to me, and people SHOULD be interested in
the Apt-Plotkin paper even if they don't realize that, so the tutorial sounds
well-chosen.  A way to test the waters would be to forward your query to my
TYPES and LOGIC lists.  Shall I?

One remark connecting that stuff with my concerns: as Stoughton tells me he
points out in his thesis, the Apt-Plotkin semantics is NOT fully abstract in
what I believe is the USUAL, more appropriate sense of that phrase.  Namely,
two OPEN programs, i.e., phrases of program type with variables of program
type ranging over all program meanings, may not be equal under all
interpretations of the variables, even though all their closed instances are
equal.  (The problem springs from the fact that the space of program meanings
contains various nondeterministic state transforms which are not definable by
any program term.)  Stoughton calls this a failure of ``contextual full
abstraction'', contexts---terms with ``holes''---being an obscure way of
talking about open terms.

What Apt-Plotkin show is that two CLOSED programs are semantically equal iff
they yield the same state-transformation/termination-property in all
contexts.  I would refer to this as an `adequacy' property, though they call
it full abstraction.  I never checked to see what results Stoughton has about
the existence of contextually fully abstract semantics.  I'm cc'ing him in
hopes of a comment.

Regards, A. 
-----------------------------
Return-Path: <main@boulder.Colorado.EDU>
Date: Tue, 29 Mar 88 13:07:55 MST
From: Michael Main <main@boulder.Colorado.EDU>
To: meyer@THEORY.LCS.MIT.EDU
Subject: Re:  beyond omega

Thanks for the feedback on my tentative talk.  I 
would appreciate further feedback from the TYPES and
logic mailing lists.  Could you pass this on to them
and request responses to be sent to
			 main@boulder.colorado.edu.  
Also, let me know if you think there may be any advantage for my talk to be
either before or after yours (with respect to the issue of monontonicity
versus continuity).

Best wishes,

Michael

END