Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9407111831.AA20162@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Re: "Meta" rewriting
Date: Mon, 11 Jul 94 11:30:57 PDT
From: chou@cs.ucla.edu


My thanks to those who pointed out that what I wrote is a special
case of second-order or higher-order unification.  Could someone
knowledgeable give us a "crash course" on general second-order or
higher-order unification?  I for one shall be much obliged.

Since I wrote my last message at 3:00AM, I forgot to mention the
restrictions of my code.  Some of them are:

(1) The first argument of meta_REWR_CONV should be an equality eq,
    possibly universally quantified.

(2) All "meta-variables" (ie, P_, Q_, etc) in eq should be free
    and have either no argument or a single argument which is
    either a bound variable or a tuple of bound variables which
    are NOT meta-variables.

(3) The constants meta_OBJ, meta_APP0, and meta_APP1 are used by
    meta_REWR_CONV as markers and should not be used by the user.

(4) meta_REWR_CONV will try to rename bound variables so that
    those bound variables that match bound variables of the same
    name in eq will receive the same name.  But the renaming
    strategy is very primitive.

(5) meta_REWR_CONV uses REWR_CONV, so it's better not to use an
    eq that have free variables on the RHS that do not appear on
    the LHS.  Same remark applies to bound variables.

(6) meta_REWR_CONV is probably not as efficient as hand-coded
    conversions like FORALL_AND_CONV.  But it saves you the time
    needed to write new conversions.

Again, all comments are welcomed!

Cheers,
- Ching Tsun