Hi,
higher order matching is decidable, but has a very high complexity. (see
e.g. "An introduction to decidability of higher-order matching", Colin
Stirling, http://homepages.inf.ed.ac.uk/cps/newnewj.pdf). Higher order
unification is undecidable, but matching is decidable. As I understand
it, HOL supports higher-order patterns for higher-order matching. This
has polynomial complexity. In case you use anything else than a
higher-order pattern (slightly extended), all bets are off. It might
work or fail.
I can't remember, where I got this belief that HOL supports higher-order
patterns. Looking for some reference, I could not find much
documentation either, but Section 7.5.4.4 in the description manual
seems to hint in this direction
> The simplifier uses a special form of higher-order matching. If a
> pattern includes a
> variable of some function type (f say), and that variable is applied
> to an argument a
> that includes no variables except those that are bound by an
> abstraction at a higher
> scope, then the combined term f (a) will match any term of the
> appropriate type as long
> as the only occurrences of the bound variables in a are in sub-terms
> matching a.
>
A higher-order pattern means that in your term, all arguments of free
variables are distinct _bound_ variables.
In your first example, both "f" and "x" are free. "f x" is not a
higher-order pattern. If you bind "x" somehow, it works:
> ho_match_term [] empty_tmset ``(f :'a -> 'a) x`` ``y :'a``
Exception-
HOL_ERR
{message = "at Term.dest_comb:\nnot a comb", origin_function =
"ho_match_term", origin_structure = "HolKernel"} raised
> ho_match_term [] (HOLset.add (empty_tmset, ``x:'a``)) ``(f :'a -> 'a)
x`` ``y :'a``
val it =
([{redex = “f”, residue =
“λx. y”}], []):
{redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
> ho_match_term [] empty_tmset ``\x. (f :'a -> 'a) x`` ``\x:'a. y :'a``
val it =
([{redex = “f”, residue =
“λx. y”}], []):
{redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
I believe the restriction that all arguments need to be variables can be
lifted. So matching against "f (x+1) y" does work, if "x" and "y" are
distinct bound vars. However, "x+1" really has to occur literally. This
kind of higher order matching is what you normally need for rewriting
and it is efficiently implementable.
As for your example which returns an invalid solution:
>> ho_match_term [] empty_tmset “(λx :'a. t :'a)” “(λx :'a. x)”;
> val it =
>([{redex = “t”, residue = “x”}], []):
>{redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
>
Yes, ho_match_term can produce wrong results, in case no solution
exists. I'm not sure whether this is deliberate or a bug. In any case,
it does not effect rewriting and other tools, because it is caught later.
Best
Thomas
On 06.04.2018 18:28, Mario Xerxes Castelán Castro wrote:
> Hello.
>
> What variant of higher order matching is “ho_match_term” supposed to
> perform?. This function is undocumented, despite being at the core of
> the simplifier, and there are many variants of higher order unification
> described in the literature (unlike first order unification), so it is
> unclear what it is supposed to do. The general case is undecidable and
> there are no most general solutions[1].
>
> At first I thought that it was second order matching, but it does not
> solve a simple second order matching problem:
>
>> ho_match_term [] empty_tmset “(f :'a -> 'a) x” “y :'a”;
> Exception-
>HOL_ERR
> {message = "at Term.dest_comb:\nnot a comb", origin_function =
> "ho_match_term", origin_structure = "HolKernel"} raised
>
> A second order solution is f := «λz. y». Another one is x := «y». f :=
> «λx. x». Next is a case where “ho_match_term” gives an anomalous answer;
> the substitution returned is not a solution in the sense of [1] (because
> alpha-renaming would occur to avoid capture of “x”):
>
>> ho_match_term [] empty_tmset “(λx :'a. t :'a)” “(λx :'a. x)”;
> val it =
>([{redex = “t”, residue = “x”}], []):
>{redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
>
> I am asking this because:
>
> * I would find useful to use some notion of “higher order rewriting” in
> custom tactics and while “ho_match_term” empirically seems to work, it
> does not seem a good idea to use it if I do not really know what it is
> doing.
>
> * Since “ho_match_term” is used by several tacticals, I am concerned
> that the informal specification that “ho_match_term” was written for
> does not matches the expectation of the authors of those tacticals
> (e.g.: the simplifier of simpLib, metis). This is a possible source of
> errors (“bugs”).
>
> Thanks.
>
> [1] “Handbook of Automated Reasoning, vol. II”, A. Robinson, A.
> Voronkov, 2001, Chapter 16 “Higher-Order Unification and Matching”.
>
>
>
> --
> Check out the vibrant tech community on one
