Boute reference

yodaiken@sphinx.nmt.edu
Thu, 12 May 1994 11:41:54 -0600

@inproceedings{ BouteEssay ,
author="Boute, R. T." ,
title="On the shortcomings of the axiomatic approach
as presently used in Computer Science. ",
booktitle="Compeuro 88 Systems Design: Concepts Methods, and Tools",
year=1988,
}

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id PAA12103 for qed-out; Mon, 22 May 1995 15:35:35 -0500
Received: from pythagoras.ma.utexas.edu (pythagoras.ma.utexas.edu [128.83.133.41]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id PAA12098 for <qed@mcs.anl.gov>; Mon, 22 May 1995 15:35:29 -0500
Received: (from bshults@localhost) by pythagoras.ma.utexas.edu (8.6.10/8.6.10) id PAA14060; Mon, 22 May 1995 15:32:07 -0500
Date: Mon, 22 May 1995 15:32:07 -0500
From: Benjamin Price Shults <bshults@fireant.ma.utexas.edu>
Message-Id: <199505222032.PAA14060@pythagoras.ma.utexas.edu>
To: John.Harrison@cl.cam.ac.uk
CC: qed@mcs.anl.gov
In-reply-to: <"swan.cl.cam.:266770:950519095422"@cl.cam.ac.uk> (message from John Harrison on Fri, 19 May 1995 10:54:02 +0100)
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.062

I see now that Harrison's [2] means the same thing that I intended my
[5] to mean. I'm sorry I complicated things unnecessarily.

Bernays called Harrison's "something": "the empty set" and
Morse-Kelley called it: "the universe".

Benji

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id PAA11772 for qed-out; Mon, 22 May 1995 15:24:57 -0500
Received: from pythagoras.ma.utexas.edu (pythagoras.ma.utexas.edu [128.83.133.41]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id PAA11766 for <qed@mcs.anl.gov>; Mon, 22 May 1995 15:24:49 -0500
Received: (from bshults@localhost) by pythagoras.ma.utexas.edu (8.6.10/8.6.10) id PAA14051; Mon, 22 May 1995 15:23:53 -0500
Date: Mon, 22 May 1995 15:23:53 -0500
From: Benjamin Price Shults <bshults@fireant.ma.utexas.edu>
Message-Id: <199505222023.PAA14051@pythagoras.ma.utexas.edu>
To: kaufmann@CLI.COM
CC: holmes@catseye.idbsu.edu, moore@CLI.COM, qed@mcs.anl.gov
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.064

I think this problem is addressed in a slightly different way (from
the four suggestions given by Harrison) in the popular classical
axiomatizations of set theory (Goedel-Bernays, Morse-Kelley). Of
course, this is in the context of a first-order theory with some
additional axiom schemata, which may be far from what most of you are
thinking of. But perhaps it's worthy of inclusion in the discussion.

5. Resolutely give all partial functions the same value on points
outside of their domain. (This comes as a consequence of the basic
underlying language and definitions.)

Bernays uses the definite descriptor term $\iota_x (A)$ to represent
the object which is the unique $x$ such that $A$. In order that this
term be well-defined when there is no unique such object, Bernays says
that when there is no such object then $\iota_x (A)$ always represents
the empty set. He uses two axiom schemata to accomplish this.

So in Bernays' language we might say

1/x=\iota_y(x is real and x<>0 and x*y=1).

So we do get that 1/0={} (and 1/a-foo = {}) but we don't really care.

In Morse-Kelley's set theory they get around the use of the definite
descriptor by defining {x}={z: if x\in V, then z=x} where V is the
universe class.

In this system we might say (I'm skipping a lot of intermediate but
fairly standard definitions):

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

Thus, the-reciprocal-function(0) = V, the universe class. But then
again, we don't care.

This turns out to be very convenient for these authors in many ways.

My Ipr system implements an axiom schema for dealing with the definite
descriptor but also allows the user to construct his set theory so
that there is no need for it (as in MK's set theory). Thus the user
may select his favorite way of dealing with undefined terms, or not
worry about it (which is hopefully what most USERS of qed will do).
However, I would not expect that QED will be flexible enough to allow
the user to make such choices at so basic a level.

Benji

--
Benjamin Shults                 Email:  bshults@math.utexas.edu
Department of Mathematics       Phone:  (512) 471-7711 ext. 208
University of Texas at Austin   WWW:    http://www.ma.utexas.edu/users/bshults
Austin, TX  78712   USA         Office: RLM 10.142

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id PAA12227 for qed-out; Mon, 22 May 1995 15:44:31 -0500
Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with SMTP
id PAA12218 for <qed@mcs.anl.gov>; Mon, 22 May 1995 15:44:22 -0500
Received: from thunder.cli.com by cli.com (4.1/SMI-4.1)
id AA17163; Mon, 22 May 95 15:43:05 CDT
From: kaufmann@CLI.COM (Matt Kaufmann)
Received: by thunder.cli.com (4.1) id AA04830; Mon, 22 May 95 15:43:05 CDT
Date: Mon, 22 May 95 15:43:05 CDT
Message-Id: <9505222043.AA04830@thunder.cli.com>
To: bshults@fireant.ma.utexas.edu
Cc: John.Harrison@cl.cam.ac.uk, qed@mcs.anl.gov
In-Reply-To: <199505222032.PAA14060@pythagoras.ma.utexas.edu> (message from Benjamin Price Shults on Mon, 22 May 1995 15:32:07 -0500)
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.065

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.

Stop me before I write again!

-- Matt

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id QAA13028 for qed-out; Mon, 22 May 1995 16:33:16 -0500
Received: from pythagoras.ma.utexas.edu (pythagoras.ma.utexas.edu [128.83.133.41]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
id QAA13023 for <qed@mcs.anl.gov>; Mon, 22 May 1995 16:33:10 -0500
Received: (from bshults@localhost) by pythagoras.ma.utexas.edu (8.6.10/8.6.10) id QAA14234; Mon, 22 May 1995 16:32:16 -0500
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
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.066

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

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id QAA13383 for qed-out; Mon, 22 May 1995 16:50:17 -0500
Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with SMTP
id QAA13374 for <qed@mcs.anl.gov>; Mon, 22 May 1995 16:50:03 -0500
Received: from thunder.cli.com by cli.com (4.1/SMI-4.1)
id AA17203; Mon, 22 May 95 15:49:10 CDT
From: kaufmann@CLI.COM (Matt Kaufmann)
Received: by thunder.cli.com (4.1) id AA04847; Mon, 22 May 95 15:49:09 CDT
Date: Mon, 22 May 95 15:49:09 CDT
Message-Id: <9505222049.AA04847@thunder.cli.com>
To: bshults@fireant.ma.utexas.edu
Cc: holmes@catseye.idbsu.edu, moore@CLI.COM, qed@mcs.anl.gov
In-Reply-To: <199505222023.PAA14051@pythagoras.ma.utexas.edu> (message from Benjamin Price Shults on Mon, 22 May 1995 15:23:53 -0500)
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.068

Warning to QED -- some of the recent discussion could be a bit out of sync,
because of tiny delays in the distribution of mail to qed@mcs.anl.gov.

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id GAA18941 for qed-out; Tue, 23 May 1995 06:25:53 -0500
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
id GAA18936 for <qed@mcs.anl.gov>; Tue, 23 May 1995 06:25:27 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP-6.5) to cl; Tue, 23 May 1995 12:24:29 +0100
To: qed@mcs.anl.gov
Subject: Re: Undefined terms
Date: Tue, 23 May 1995 12:24:16 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:158810:950523112446"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.077

You are right: in [2] I meant to allow various arbitrary values in different
situations. This makes the proposal [5] genuinely different. In HOL these
"arbitrary values" arise in two ways:

(1) Explicitly via the choice operator @ (an indefinite descriptor, so "@x.
P[x]" means "some x such that P[x]"). For example, one could define

inv = \x. @y. x * y = 1

(2) Via the principle of constant specification, which allows the
introduction of constants when a witness can be shown to exist.
For example:

|- !x. ~(x = 0) ==> ?y. x * y = 1

so

|- !x. ?y. ~(x = 0) ==> (x * y = 1)

Skolemizing

|- ?f. !x. ~(x = 0) ==> (x * f(x) = 1)

and introducing a constant "inv":

|- !x. ~(x = 0) ==> (x * inv(x) = 1)

Sometimes (1) results in more accidental theorems. We can't say much about
inv(0), but we do at least know that it's "@y. F" (F = falsum). This means that
any other constant of the same type defined in a similar way will also be equal
to "@y. F" when the body is false. Method (2) does not have this weakness. In
fact one could define two constants "inv" and "inv'" based on the same theorem,
without any relationship between inv(0) and inv'(0) being deducible. Some
HOL users considered this sufficiently important to justify the principle of
constant specification (in the old days, HOL only allowed definitions of the
direct form "c = <closed term>", or so I'm told). On the other hand, we are not
explicit about the value of "@y. F" in a model. In the standard HOL semantics,
we just assume a single choice function from the start. You can read this
semantics (due to Andy Pitts) in the HOL book from CUP, or in machine-readable
form in the standard HOL distribution.

John.

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id HAA19313 for qed-out; Tue, 23 May 1995 07:46:31 -0500
Received: from vega.anu.edu.au (root@vega.anu.edu.au [150.203.160.27]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
id HAA19308 for <qed@mcs.anl.gov>; Tue, 23 May 1995 07:46:24 -0500
Received: (from mcn@localhost) by vega.anu.edu.au (8.6.12/8.6.9) id VAA15893 for qed@mcs.anl.gov; Tue, 23 May 1995 21:59:00 +1000
Date: Tue, 23 May 1995 21:59:00 +1000
From: Malcolm Newey <Malcolm.Newey@cs.anu.edu.au>
Message-Id: <199505231159.VAA15893@vega.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Re: Undefined terms
X-Sun-Charset: US-ASCII
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.080

In John Harrison's recent posting he discussed limits in analysis and his
preferred use of a relation ( --> meaning tends to), instead of the use
of the limit function ( lim: ((real->real)->real) ).  This should have been
labelled as a separate technique for coping with undefined terms:

[6]	Simply resist the temptation to write a partial function
using functional notation and, instead, capture the notion
by means of a relation.  If  F  is a partial function we
find difficult to deal with in our logic, then we can
introduce a constant for a corresponding relation F':
F'(x,y)  iff  F(x) is defined and F(x)=y

This is a technique widely used in the HOL community; in fact, it is common
practice when defining a function to first introduce a relation F' that
expresses the partial function exactly.  Having so done, we can prove that
F' can be extended to a total function.  Depending on how we do it, a
function can then be defined according to technique [1] or [2].

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id FAA16715 for qed-out; Mon, 29 May 1995 05:53:13 -0500
Received: from compu735.mathematik.hu-berlin.de (compu.mathematik.hu-berlin.de [141.20.18.102]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with SMTP
id FAA16710 for <qed@mcs.anl.gov>; Mon, 29 May 1995 05:52:59 -0500
Received: from kummer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
(1.37.109.8/16.2/4.93/main) id AA03748; Mon, 29 May 1995 12:52:46 +0200
Received: from wega.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
id AA12849; Mon, 29 May 95 12:52:25 +0200
Date: Mon, 29 May 95 12:52:25 +0200
From: dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)
Message-Id: <9505291052.AA12849@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Natural Language Output for Your Theorem Prover?
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801761532.002

To whom it may concern

The mail server of the ILF system is now online for the public. It takes
model elimination proofs and returns natural language proof presentations
as LaTeX source. Proofs from other calculi can be presented if they have
been equipped with a block structure.

Moreover, a visualisation of the logical dependencies between the formulas
in the proof can be delivered.

You can receive more detailed information by sending a message with text

help

to the ILF Server

ilf-serv@mathematik.hu-berlin.de

Then, the ILF Server will also tell you, how to obtain a version of the
Server documentation which is appropriate to your purposes.

Please, recall that the ILF Server is an experimental system and report
errors, problems, questions and suggestions for further improvements to

ilf-serv-request@mathematik.hu-berlin.de

I should be grateful, if you forward this message to anybody possibly
interested in the subject.

With best regards

Bernd, Ingo Dahn

***************************************
* Bernd, Ingo Dahn		      *
*				      *
* Humboldt-University		      *
* Institute of Pure Mathematics       *
* Ziegelstr. 13a		      *
* D-10099 Berlin		      *
*				      *
* Phone: (+49)30-2843-1829	      *
* Fax  : (+49)30-2843-1846            *
* Mail : dahn@mathematik.hu-berlin.de *
*				      *
***************************************

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id NAA29638 for qed-out; Mon, 5 Jun 1995 13:19:14 -0500
Received: from scapa.cs.ualberta.ca (root@scapa.cs.ualberta.ca [129.128.4.44]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
id NAA29629 for <qed@mcs.anl.gov>; Mon, 5 Jun 1995 13:19:04 -0500
Received: from sedalia.cs.ualberta.ca by scapa.cs.ualberta.ca id <13059-3>; Mon, 5 Jun 1995 12:18:45 -0600
Subject: To type or not to type
From: Piotr Rudnicki <piotr@cs.ualberta.ca>
To: qed@mcs.anl.gov
Date: 	Mon, 5 Jun 1995 12:18:37 -0600 (MDT)
X-Mailer: ELM [version 2.4 PL24]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 648
Message-Id: <95Jun5.121845-0600_mdt.13059-3+78@scapa.cs.ualberta.ca>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 802439556.008

Hi:

I would like to propose the subject of typing as a topic for discussion during
the QED workshop in Warsaw.  In August, last year there was some discussion
on this forum that started with L. Lamport's note "Types considered
harmful".  I am interested in discussing the following:

0. What do we mean by "type"?

1. How types are handled in various QED-like systems?
Here I would like to hear from other people.

or theorem proving systems?  Users' view vs implementers' view.

2. Why is type theory neglected in mathematical pratice?

Piotr (Peter) Rudnicki

Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id GAA27097 for qed-out; Tue, 13 Jun 1995 06:14:40 -0500
Received: from swan.cl.cam.ac.uk (swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
id GAA27091 for <qed@mcs.anl.gov>; Tue, 13 Jun 1995 06:14:17 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP-6.5) to cl; Tue, 13 Jun 1995 12:08:29 +0100
X-Uri: <URL:http://www.cl.cam.ac.uk/users/jrh>
To: qed@mcs.anl.gov
Subject: Re: Undefined terms
Date: Tue, 13 Jun 1995 12:08:24 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:286540:950613110840"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

On the subject of ways of dealing with partial functions, I also got the
following message which I've been asked to forward to QED.

John.

| Date: Sun, 4 Jun 95 15:08:16 BST
| From: Cliff B Jones <cliff@cs.man.ac.uk>
| To: John.Harrison@cl.cam.ac.uk
| Cc: pal@everest.cs.uq.oz.au
| Subject: Re: [John.Harrison@cl.cam.ac.uk: Re: Undefined terms]

Sear John Harrison,

There is another approach which re-defines the logical operators to
cope with "gaps" (Blamey's phrase). The following paper relate to such
a LPF:

@article{BCJ84,
author =        "H. Barringer and J.H. Cheng and C. B. Jones",
title =         "A Logic Covering Undefinedness in Program Proofs",
journal =       acta,
volume =        "21",
pages =         "251--269",
year =          "1984"
}

@phdthesis{Cheng86,
title =         "A Logic for Partial Functions",
author =        "J.H. Cheng",
school =        "University of Manchester",
year =          "1986"
}

@article{JonesMiddelburg94,
author   = "C.B. Jones and C.A. Middelburg",
title    = "A Typed Logic of Partial Functions Reconstructed
Classically",
journal  = "Acta Informatica",
volume   = 31,
number   = 5,
pages    = "399--430",
year     = 1994
}

cliff jones