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