Re: [Hol-info] "Gordon Computer"

[Thomas Tuerk]

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 
>> *Date: *Friday, 6 April 2018 at 21:27
>> *To: *Ramana Kumar , HOL-info list
>> 
>> *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
>> mailto:ramana.ku...@

Re: [Hol-info] "Gordon Computer"

[Thomas Tuerk]

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 
> *Date: *Friday, 6 April 2018 at 21:27
> *To: *Ramana Kumar , HOL-info list
> 
> *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
> 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
> mailto:l...@cam.ac.uk>> wrote:
>
> It would be nice to give them a permanent home, perhaps as
> part of the HO

Re: [Hol-info] "Gordon Computer"

[Michael.Norrish]

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 
Date: Friday, 6 April 2018 at 21:27
To: Ramana Kumar , HOL-info list 

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 
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 
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 
mailto:ramana.ku...@cl.cam.ac.uk>> wrote:

It doesn't look too bad to me - happy to port them if you like.





--
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

Re: [Hol-info] "Gordon Computer"

[Lawrence Paulson]

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  wrote:
> 
> Attached is a port of 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  > 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 > > wrote:
>> 
>> It doesn't look too bad to me - happy to port them if you like.
> 
> 
> 

--
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

Re: [Hol-info] "Gordon Computer"

[Ramana Kumar]

It doesn't look too bad to me - happy to port them if you like.

On 5 April 2018 at 12:36, Lawrence Paulson  wrote:

> I have just managed to locate Jeff Joyce's "Tamarack-2" files, which he
> describes as slightly simplified compared with the original Gordon
> computer. They are dated 1989 and the comments suggest that they are for
> HOL88. I guess they will bring back the memories for some people. But it
> would probably take a lot of work to get them to run in a modern version of
> HOL.
>
> http://www.cl.cam.ac.uk/~lp15/tmp/tamarack2.zip
>
> Larry
>
>
> 
> --
> 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