Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: Donald.Syme@cl.cam.ac.uk, info-hol@cs.uidaho.edu
In-Reply-To: <"swan.cl.cam.:118710:951010130544"@cl.cam.ac.uk> (message from Donald Syme on Tue, 10 Oct 1995 14:05:31 +0100)
Subject: Re: Unification/solving existential goals
Message-Id: <95Oct10.161623met.8083@sunbroy14.informatik.tu-muenchen.de>
Date: 	Tue, 10 Oct 1995 16:16:17 +0100


> I'm looking for a HOL88 or HOL90 routine which, given
> a term such as
>     (--`?a b c. P1[a,b,c] /\ ... /\ Pn[a,b,c]`--)
>
> and a list of available assumptions, will perform some
> kind of backtracking unification against the assumptions to
> find instances of a,b and c which satisfy all the conjuncts.  e.g. given
> 
>    [ |- P1 e f,
>      |- P2 f g,
>      |- !g. P3 e g]
> 
> and (--`?a b c. P1 a b /\ P2 b c /\ P3 a b`--)
> I would like the routine to select 
>  	a -> e
> 	b -> f
> 	c -> g

I don't think you need AC unification to get something relatively
useful. A really simple approach would be to "line up" the goal and the
antecedents (by sorting, plus throwing in wild cards when necessary) and
then just use first order matching modulo aconv. For the example, one
would get the problem

   match (P1 a b /\ P2 b c /\ P3 a b)   (* pattern *)
         (P1 e f /\ P2 f g /\ P3 e g)   (* object  *)

Matching treats all variables in the pattern as universal, and all
"free" variables in the object as "existential", i.e., as constants.

This won't fully solve the problem, since the variable "g" in the
assumption

    !g. P3 e g

should also be universal, hence Don's request for unification. To do
this, just replace the matching algorithm with a unification algorithm,
except that all existential variables have to be treated as constants
(in matching, this came for free, but unification needs more work). This
might be most easily accomplished by mapping to preterms, where
variables can be turned into constants without referencing the symbol
table. The resulting substitutions will of course need to be mapped back
into terms, but that shouldn't be any trouble.

Backtracking becomes necessary when there is more than one choice of how
to line the terms up, but I can't really say much more about it.

Konrad.