Sorry, I copied my reply to another thread in the wrong message. Please
ignore it. Thomas
On 07.04.2018 08:43, Thomas Tuerk wrote:
>
> 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
