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”.
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
