Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Message-Id: <199510101957.VAA19923@tanichka.abo.fi>
To: info-hol@cs.uidaho.edu, John Harrison <jharriso@ra.abo.fi>
Subject: Re: ACCEPT_TAC nit pick...
In-Reply-To: Your message of "Tue, 10 Oct 1995 18:53:32 EET."
             <199510101802.LAA14518@dworshak.cs.uidaho.edu>
Date: Tue, 10 Oct 1995 21:56:58 +0200
From: John Harrison <jharriso@ra.abo.fi>
Mime-Version: 1.0
Content-Transfer-Encoding: quoted-printable

Rob writes:

| Hi, why does HOL90 behave in the following way? (not giving you your actual
| goal term as the resulting theorem, but rather the thm you gave to
| ACCEPT_TAC)

There are a several similar problems with "terminal" tactics. ACCEPT_TAC
may also give you fewer assumptions than you started with, i.e. solving the
goal

        A ?- t

with a theorem |- t gives you |- t and not A |- t. One doesn't often notice
this effect because the assumptions mostly arise from DISCH_TAC or
DISCH_THEN, whose inverted form DISCH still trivially discharges a
nonexistent assumption. Conversely, B |- t will give more assumptions, and
here the validity check fails (but switch it off and you get B |- t).

I favour keeping the eventual forward proof as simple as possible, which
argues for putting in separate equality and aconv tests in ACCEPT_TAC, but
continuing to allow wrong assumption lists. Extra assumptions can always be
filtered out at the top level (e.g. TAC_PROOF could include a test, and
even a coercion function).

On adding an equality test first, Tom says:

| I assume Konrad means the added execution time, and not the
| complexity of the code for ACCEPT_TAC.  The point is a very
| valid one in general. In this case, however, I think that
| it would be okay to execute the "two tests" -- mu guess is
| that most of the times ACCEPT_TAC is actually executed is on
| fairly small terms.

In fact, on big terms it would probably be *better*. Equality tests which
return "true" often do so very quickly, because after only a little
traversal, terms with a common "ancestry" are found; these instantly
compare equal as pointers. So in many situations, certainly those where
"aconv x y" is statistically likely to return "true", replacing it by "x =
y or aconv x y" would actually be an optimization. (Even without shortcuts,
equality was faster than aconv last time I tried.) In fact, without this
optimization, some HOL derived rules are likely to fail horribly on large
terms. I'll be lobbying for some such optimizations in the next release of
hol90.

Of course one of the potential advantages of de Bruijn terms is that such
short-circuiting could easily be inserted explicitly into "aconv". However,
this would demand a pointer equality test like LISP's EQ or CAML's "==",
which doesn't exist in Standard ML. (Though it can be hacked using type
casts from "System.Unsafe" in SML/NJ.)

John.

=========================================================================
John Harrison                   | email: jharriso@ra.abo.fi
Åbo Akademi University          | web:   http://www.abo.fi/~jharriso/
Department of Computer Science  | phone: +358 (9)21 265-4049
Lemminkäisenkatu 14a            | fax:   +358 (9)21 265-4732
20520 Turku                     | home:  +358 (9)21 2316132
FINLAND                         | time:  UTC+2:00
=========================================================================