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

Correspondence on continuity and monotonicity

	From: Albert R. Meyer <sun!THEORY.LCS.MIT.EDU!meyer>
	How about forwarding our correspondence to my TYPES and LOGIC email
	lists?

Here goes.
-v

Date: Tue, 5 Apr 88 09:36:40 PDT
From: pratt (Vaughan Pratt)
To: meyer@theory.lcs.mit.edu
Subject: continuity vs. monotonicity
Cc: jcm@navajo.stanford.edu, pratt

John Mitchell passed on to me your "Semantical Paradigms" paper, which
I read with much interest on account of work of my own on monotonicity
and continuity.  In my universal algebra and lattice theory course I
emphasize monotonicity over finite additivity over continuity, making
the point that some quite basic interesting facts we are taught in
mathematics under assumptions of finite additivity (as in point set
topology) and continuity (as in analysis) hold under the weaker
assumption of monotonicity.

In case you're collecting bibliographic references to articles on
continuity vs. monotonicity you might look at the subsection headed
"Induction" on page 23 of STOC-80 (my second article on properties of
dynamic algebras, the first is in FOCS-79).  There I make the point
that we tend to assume continuity only because we believe intuitively
that somehow what we're doing depends on it.  (My paper assumes finite
additivity, but I believe everything except the <- direction of Lemma
1, on which nothing else depends, holds under the weaker assumption of
monotonicity.)

The reason we are so easily confused about this point is that we so
often build irrelevant details into what we think of as our
"fundamental concepts."   These irrelevant details are usually
recognizable by their second-order expression, for example the
definition of succ(X) = {i+1|i in X}, or the definition of reflexive
transitive closure as an infinite union.  Both these examples appear in
the above-cited subsection.

The closing paragraphs of the paper return to this point, giving an
additional detailed example illustrating the point that our intuition
unquestioningly builds in assumptions of continuity.  (Actually I'd be
inclined to say today that what the example really illustrates is the
overuse of second-order logic that I objected to just now in the
preceding paragraph.)

This paper by the way is (he says modestly) a nice source of insights
into the fundamentals of induction, monotonicity, and continuity.  To
quote from page 22, "The class [of models of the Segerberg axioms] can
be considered the algebraic home of induction, in the same sense that
the class of groups can be considered the algebraic home of invertible
operations."  (Today I would make this statement of the fragment of PDL
obtained by omitting union and composition, which play no essential
role in these ideas.  I would also weaken the Boolean component to a
Heyting one, since Booleanness plays no role either.)

I do not believe there is another theory of induction that can
justifiably make the same claim.  Induction naturally takes the form of
a proposition, and the problem with other theories of induction is that
unlike PDL they do not make propositions objects of the theory.

This doesn't address your concerns of adequacy etc. but it does provide
a very abstract setting in which one can stare at the interaction of
induction and monotonicity.
-v

Date: Tue, 5 Apr 88 16:19:47 est
From: Albert R. Meyer <sun!THEORY.LCS.MIT.EDU!meyer>
To: sun!coraki!pratt
In-Reply-To: Vaughan Pratt's message of Tue, 5 Apr 88 09:36:40 PDT <8804051636.AA07744@>
Subject: continuity vs. monotonicity
Cc: jcm@navajo.stanford.edu

Thanks for your comments.  We agree that monotonicity has been inadequately
highlighted in semantics.  I've found it pedagogically very valuable to parse
out the many basic facts which follow purely from monotonicity.  But in the
end I identify some crucial properties which depend on continuity, e.g., full
abstraction of cpo's with continuous functions as a model of simply typed
lambda calculus, and the solution of domain equations.  So I'm not entirely
comfortable with your general assessment that monotone models ``be considered
the algebraic home of induction''.

But anyway, I'll plan to look at your paper and make appropriate reference to
it in the revised Technical Memo version of my LICS paper.

How about forwarding our correspondence to my TYPES and LOGIC email lists?

Regards, A.