Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@leopard.cs.byu.edu
Subject: Difficulties with large terms
Date: Thu, 05 Jan 1995 22:10:07 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:198010:950105221016"@cl.cam.ac.uk>


In my recent work on BDDs, I've been playing with some rather large terms,
and I've noticed an unpleasant bottleneck.

Part of the appeal of the LCF/HOL approach (and a good answer to the
assertion that decomposition to primitive inferences is fundamentally
inefficient) is that transformations from |- E[t] to |- E'[t] can be done
by appealing to a pre-proved theorem, rather than repeating a perhaps
difficult proof every time. That is, if we store the theorem:

  |- !x. E[x] ==> E'[x]

it may then be instantiated as required:

  |- E[t] ==> E'[t]

and we may then perform a Modus Ponens step with |- E[t] to get |- E'[t].

All very well, but the Modus Ponens step performs an *alpha-equivalence*
test between E[t] and E[t]. This of course returns "true", but necessitates
a complete traversal of E[t]. If |t| is large, this is very inefficient. If
MP tested for *equality* instead, however, then then test would (in a
decent compiler) short-circuit with a pointer EQ when it reaches |t| in its
traversal. Thus the complexity would be the same as any purely applicative
implementation of such a transformation.

So, I believe that HOL primitives such as MP and TRANS should allow quick
pointer EQ tests, otherwise things like this are going to be difficult.
Some possibilities are:

* Put an EQ test in the "aconv" code (but does ML make such a thing
  available? I don't think so...)

* Change all primitive rules to use "=" rather than "aconv" (arguably a
  retrograde step from the usability point of view; one would want to build
  "aconv" versions on top).

* Change all primitive rules to use "t1 = t2 or aconv t1 t2" instead of
  "aconv t1 t2". A bit ugly but reasonable. The only problem is that
  failures are going to take twice as long. But does one ever expect
  failures? Not so often I think.

Anyway, as an illustration of how the trivial-looking matter of unwinding a
recursion equation is quadratic with the standard TRANS, see the hol90 code
below. Can anyone think of a linear implementation without changing the
underlying primitives? Here are some sample results:

        SIZE    New TRANS       Old TRANS
       -----------------------------------
        1         0.00             0.00
        2         0.00             0.10
        4         0.10             0.00
        8         0.10             0.20
        16        0.30             0.20
        32        0.50             0.50
        64        0.10             0.12
        128       0.20             0.28
        256       0.46             0.67
        512       0.82             1.92
        1024      1.62             6.11
        2048      3.26            20.63
        4096      6.54            75.32
        8192     12.39           288.53
        16384    25.58          1123.35
        32768    52.83          4371.91
       -----------------------------------

John.

*       *       *       *       *       *       *       *       *       *

open System.Timer;

new_theory "BIG";

System.Control.interp := false;

load_library {lib = hol88_lib, theory = "-"};

open Psyntax Compat;

val % = Parse.term_parser;

val list_Axiom = theorem "list" "list_Axiom";

(* ------------------------------------------------------------------------- *)
(* Define an illustrative constant.                                          *)
(* ------------------------------------------------------------------------- *)

val ANDS = new_recursive_definition Prefix list_Axiom "ANDS_DEF"
 (%`(ANDS [] = T) /\
    (!h t. ANDS (CONS h t) = h /\ ANDS t)`);

(* ------------------------------------------------------------------------- *)
(* Our own TRANS, which short-circuits on L = R.                             *)
(* ------------------------------------------------------------------------- *)

exception Toss;

fun TRANS' th1 th2 =
   let val (h1,c1) = dest_thm th1
       and (h2,c2) = dest_thm th2
       val (lhs1,rhs1) = dest_eq c1
       and (lhs2,rhs2) = dest_eq c2
       and hyps = union h1 h2
   in
   if (rhs1 = lhs2 orelse aconv rhs1 lhs2)
   then mk_thm(hyps,mk_eq(lhs1,rhs2))
   else raise Toss
   end
   handle _ => raise Toss;

(* ------------------------------------------------------------------------- *)
(* Make a big list to play with.                                             *)
(* ------------------------------------------------------------------------- *)

local val F = %`F`
      val N = %`[]: bool list`
      fun blist(n,l) =
        if n < 1 then l
        else blist(n - 1,mk_cons(F,l))
in
fun mk_blist n = blist(n,N)
end;

(* ------------------------------------------------------------------------- *)
(* Unwinding with TRANS'.                                                    *)
(* ------------------------------------------------------------------------- *)

local val [ANDS_NULL, ANDS_CONS] = CONJUNCTS ANDS
in
fun EXPAND_1 tm =
  let val (cnst,lst) = dest_comb tm
   in if is_cons lst then
      let val (h,t) = dest_cons lst
          val th1 = EXPAND_1 (mk_comb(cnst,t))
          val t' = rand(lhs(concl(th1)))
          val th2 = SPECL [h, t'] ANDS_CONS
          val cjtm = rator(rand(concl th2))
          val th3 = AP_TERM cjtm th1
       in TRANS' th2 th3
      end
      else ANDS_NULL
  end

end;

(* ------------------------------------------------------------------------- *)
(* Unwinding with TRANS.                                                     *)
(* ------------------------------------------------------------------------- *)

local val [ANDS_NULL, ANDS_CONS] = CONJUNCTS ANDS
in
fun EXPAND_2 tm =
  let val (cnst,lst) = dest_comb tm
   in if is_cons lst then
      let val (h,t) = dest_cons lst
          val th1 = EXPAND_2 (mk_comb(cnst,t))
          val t' = rand(lhs(concl(th1)))
          val th2 = SPECL [h, t'] ANDS_CONS
          val cjtm = rator(rand(concl th2))
          val th3 = AP_TERM cjtm th1
       in TRANS th2 th3
      end
      else ANDS_NULL
  end

end;

(* ------------------------------------------------------------------------- *)
(* Tests.                                                                    *)
(* ------------------------------------------------------------------------- *)

fun time f arg =
  let val TIMER = start_timer()
   in f arg; check_timer TIMER
  end;

fun go tm =
  let val TIME_1 = time EXPAND_1 tm
      val TIME_2 = time EXPAND_2 tm
   in (TIME_1,TIME_2)
  end;

1;      go (mk_comb(%`ANDS`,mk_blist 1));
2;      go (mk_comb(%`ANDS`,mk_blist 2));
4;      go (mk_comb(%`ANDS`,mk_blist 4));
8;      go (mk_comb(%`ANDS`,mk_blist 8));
16;     go (mk_comb(%`ANDS`,mk_blist 16));
32;     go (mk_comb(%`ANDS`,mk_blist 32));
64;     go (mk_comb(%`ANDS`,mk_blist 64));
128;    go (mk_comb(%`ANDS`,mk_blist 128));
256;    go (mk_comb(%`ANDS`,mk_blist 256));
512;    go (mk_comb(%`ANDS`,mk_blist 512));
1024;   go (mk_comb(%`ANDS`,mk_blist 1024));
2048;   go (mk_comb(%`ANDS`,mk_blist 2048));
4096;   go (mk_comb(%`ANDS`,mk_blist 4096));
8192;   go (mk_comb(%`ANDS`,mk_blist 8192));
16384;  go (mk_comb(%`ANDS`,mk_blist 16384));
32768;  go (mk_comb(%`ANDS`,mk_blist 32768));