Date: Mon, 22 May 1995 16:32:16 -0500
From: Benjamin Price Shults <bshults@fireant.ma.utexas.edu>
Message-Id: <199505222132.QAA14234@pythagoras.ma.utexas.edu>
To: kaufmann@CLI.COM
CC: John.Harrison@cl.cam.ac.uk, qed@mcs.anl.gov
In-reply-to: <9505222043.AA04830@thunder.cli.com> (kaufmann@cli.com)
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Matt Kaufmann said:
   Actually, I think there may still be a difference between your [5] and
   Harrison's [2].  I interpreted [2] to allow different "default" values for
   different function applications, but I interpreted your [5] as a proposal to
   use one error value for all occasions, kind of a "bottom" (in the Scott sense).
   In that sense, your [5] is a sort of strengthening of [1], in that you are
   fixing one value for all "erroneous" applications.  I suppose that one could
   also view your [5] as a sort of [4], i.e., "bottom" is a way to make sense out
   partiality.  Now to confuse the matter, I can't help but mention that this ties
   into [3], in the sense that one could conceive of a "bottom" of each type.


Perhaps Harrison will clarify what he intended by [2].

Bernays' approach, then is [5] (or maybe [2]) whereas Morse-Kelley
really does allow different default values as my example accidentally
showed.  To make the point I wanted to make, and to be more consistent
with Kelley, I should have defined

the-reciprocal = {<x,y>:if x is real and x <> 0 then x*y=1}

Then, the-reciprocal(0) = V.

The point is that in Bernays, there is one default value for all
undefined terms but in Kelley it is flexible (although he seems to
prefer V as teh default).

Matt Kaufmann said:
   Stop me before I write again!

We should probably both stop.

Benji