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
In-reply-to: <9505221831.AA04663@thunder.cli.com> (kaufmann@CLI.COM)
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.142Received: (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 In-reply-to: <9505222043.AA04830@thunder.cli.com> (kaufmann@cli.com) 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 In-reply-to: Your message of "Mon, 22 May 1995 16:32:16 CDT." <199505222132.QAA14234@pythagoras.ma.utexas.edu> 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.
1. What are advantages/disadvantages of using types in known proof-checking 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 | In-Reply-To: <9505210127.AA07165@everest> (pal@everest.cs.uq.oz.au) | Subject: Re: [John.Harrison@cl.cam.ac.uk: Re: Undefined terms]
Sear John Harrison,
Peter Lindsay forwarded your message to QED (I don't receive it).
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