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 ; 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 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].