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 07.04.2018 08:23, michael.norr...@data61.csiro.au wrote:
>
> Thanks for digging out this material Larry! I’d be very happy to see
> it added to our examples directory.
>
>
>
> Ramana, let me know if you want to make the initial commits. I
> suggest we can have an examples/hardware with an appropriate README.
>
>
>
> Best,
>
> Michael
>
>
>
> *From: *Lawrence Paulson <l...@cam.ac.uk>
> *Date: *Friday, 6 April 2018 at 21:27
> *To: *Ramana Kumar <ramana.ku...@cl.cam.ac.uk>, HOL-info list
> <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] "Gordon Computer"
>
>
>
> I am not sure who is in charge of HOL4 these days. Would it be
> possible to add this as an example to HOL4? If people are interested,
> I found many other examples. Here are just two of them:
>
>
>
> * the specification and verification of some CMOS adders
>
> * Transistor Implementation of a n-bit Counter
>
>
>
> I also found Mike's original computer, which is a slightly larger
> example than Tamarack.
>
>
>
> Larry
>
>
>
> On 5 Apr 2018, at 14:31, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk<mailto:ramana.ku...@cl.cam.ac.uk>> wrote:
>
>
>
> Attached is a port of tamarack.ml<http://tamarack.ml/>, which
> seems to just be definitions. I guess the proofs might be harder
> to port, but I haven't looked...
>
> They could be added to HOL/examples in the HOL4 distribution -- if
> I find time to port them later (must leave it for now though..)
>
>
>
> On 5 April 2018 at 14:02, Lawrence Paulson
> <l...@cam.ac.uk<mailto:l...@cam.ac.uk>> wrote:
>
> It would be nice to give them a permanent home, perhaps as
> part of the HOL4 distribution. Also I may create a small
> memorial page for Mike and could include it there.
>
>
>
> I found mountains of old stuff in Mike's file space, though
> sadly, much of it is protected.
>
>
>
> Larry
>
>
>
> On 5 Apr 2018, at 13:41, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk<mailto:ramana.ku...@cl.cam.ac.uk>>
> wrote:
>
>
>
> It doesn't look too bad to me - happy to port them if you
> like.
>
>
>
>
>
> <tamarackScript.sml>
>
>
>
>
>
> ------------------------------------------------------------------------------
> 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
------------------------------------------------------------------------------
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
