Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu
In-Reply-To: <94Feb23.201539met.326474@tuminfo2.informatik.tu-muenchen.de> (windley@leopard.cs.byu.edu)
Subject: Re: Partial evaluation in ML?
Message-Id: <94Feb23.205518met.8124@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 23 Feb 1994 20:55:04 +0100


> This implies that HOL is doing partial evaluation on curried
> arguments, doesn't it?  Is it really, or is it doing something simpler
> which I'm missing?

The "partial evaluation" has been carefully put in by hand (originally
by Larry Paulson for Cambridge LCF): if you write an ML function in the
manner

    fun f arg1 = 
       let x = < code 1 >
       in fn arg2 => < rest of code >
       end

then "f M" will evaluate "code 1" on M, leaving the rest of the code
unevaluated in a closure abstracted by "arg2". This sort of thing is
what is happening in the rewriting code. The theorem proving you see is
preliminary to the incorporation of theorems into the rewrite-rule
"term-net" (a hash-table-like data structure indexed by terms, in this
case the left-hand sides of rewrite rules). The following
transformations are recursively applied

(* Split a theorem into a list of theorems suitable for rewriting:
 *
 *   1. Specialize all variables (SPEC_ALL).
 *
 *   2. Then do the following:
 *
 *        |- t1 /\ t2     -->    [|- t1 ; |- t2]
 *
 *   3. Then |- t --> |- t = T and |- ~t --> |- t = F
 *
 ***)

Konrad.