hol-info

[Hol-info] HOL Light set comprehensions

[Rob A. <rd...@le...>]

This is idle curiosity on my part about HOL Light: why are the constants that support set comprehensions defined in such a way that the parser has to generate an invisible bound variable? This results in surprising behaviour like:

# `{x | x > 9}` = `{x | x > 9}`;;
val it : bool = false

HOL4 defines set comprehensions the way I would expect (using a single constant GSPEC with type 'a -> 'b # BOOL -> 'b -> BOOL) and doesn't need to insert any invisible bound variables.

Regards,

Rob.

Re: [Hol-info] HOL Light set comprehensions

[Bill R. <ri...@ma...>]

Rob, I think the answer to your interesting question involves more complicated set abstractions like {y + 6 | y < 0}.  I think here we see the merit of the HOL Light invisible variables, as this simple proof shows: 

   g `EMPTY = {y + 6 | y < 0}`;;
   e(REWRITE_TAC[SETSPEC; GSPEC]);;
   e(REWRITE_TAC[LT; EMPTY]);;

   `{} = (\GEN%PVAR%459. ?y. y < 0 /\ GEN%PVAR%459 = y + 6)`

   # val it : goalstack = No subgoals

Let's replace the computer-generated invisible variable GEN%PVAR%451 with a for clarity: 

`{} = (\a. ?y. y < 0 /\ a = y + 6)`

I think that's correct, because I think the meaning of 
{y + 6 | y < 0}
is
{a | ?y. y < 0 /\ a = y + 6}
so HOL Light should generate an invisible variable automatically for {y + 6 | y < 0}.

BTW Michael Norish's response a year ago is quite relevant:
http://article.gmane.org/gmane.comp.mathematics.hol/2118
Sorry it took me so long to respond, and I still don't understand parser.ml well enough, but I bet Michael does.

RDA> This is idle curiosity on my part about HOL Light: why are the
RDA> constants that support set comprehensions defined in such a way
RDA> that the parser has to generate an invisible bound variable?

RDA> This results in surprising behaviour like:

RDA> # `{x | x > 9}` = `{x | x > 9}`;;
RDA> val it : bool = false

First, the constants SETSPEC and GSPEC are defined in sets.ml in a way that involves no invisible bound variables: 

let GSPEC = new_definition
  `GSPEC (p:A->bool) = p`;;

let SETSPEC = new_definition
  `SETSPEC v P t <=> P /\ (v = t)`;;

I bet Michael understands these definitions.  So the invisible bound variables that you and Michael's post refer to must come from the HOL Light parser making sense of the curly braces, and I think that involves these lines of parser.ml:

  || a (Resword "{") ++

  let pgenvar =
    let gcounter = ref 0 in
    fun () -> let count = !gcounter in
              (gcounter := count + 1;
               Varp("GEN%PVAR%"^(string_of_int count),dpty)) in

  let pmk_setcompr (fabs,bvs,babs) =
    let v = pgenvar() in
    let bod = itlist (curry pmk_exists) bvs
                     (Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs)) in
    Combp(Varp("GSPEC",dpty),Absp(v,bod)) in

So HOL Light must use parser.ml to turn a set abstraction
{ ... | ... }
into a combination involving GSPEC, SETSPEC and your invisible variables.  Here's evidence:

g `EMPTY = {y | y < 0}`;;
e(REWRITE_TAC[SETSPEC; GSPEC]);;

`{} = (\GEN%PVAR%450. ?y. y < 0 /\ GEN%PVAR%450 = y)`

Let's rewrite the lambda abstraction for clarity as, changing GEN%PVAR%450 to a:

(\a. ?y. y < 0 /\ a = y)

Maybe your point is that HOL Light should instead use this simpler lambda abstraction

(\y. y < 0)

There you'd be making a really good point, but with more complicated set abstraction above, I think we see the value of invisible variables.

BTW note that my simple proof above did not use IN_ELIM_THM, and I got away with that because IN_ELIM_THM has a large intersection with 
REWRITE_TAC[SETSPEC; GSPEC].
-- 
Best,
Bill 

Re: [Hol-info] HOL Light set comprehensions

[Rob A. <rd...@le...>]

On 7 Dec 2013, at 07:19, Bill Richter <ri...@ma...> wrote:

> Rob, I think the answer to your interesting question involves more complicated set abstractions like {y + 6 | y < 0}.  I think here we see the merit of the HOL Light invisible variables, as this simple proof shows: 
> 
> …

> I think that's correct, because I think the meaning of 
> {y + 6 | y < 0}
> is
> {a | ?y. y < 0 /\ a = y + 6}
> so HOL Light should generate an invisible variable automatically for {y + 6 | y < 0}.
> 
> 
Sure, but my surprise is tthat the quantification isn't hidden inside a definition like it is in HOL4.
HOL4 defines a constant GSPEC : ('a -> 'b # bool) -> 'b -> bool with (essentially) the following defining
property:

	GSPEC f v = ?x. f x = (v, T)

and then the parser translates {y + 6 | y < 0} into GSPEC(\y.(y + 6, y < 0)). In HOL Light there is a
constant called GSPEC, but it is just the identify function, the semantics of the set comprehension
are given by something called SETSPEC, which has to appear in a context where a variable
representing a candidate for membership of the set comprehension is in scope. This seems
inside out to me.

Regards,

Rob.
\
> RDA> This is idle curiosity on my part about HOL Light: why are the
> RDA> constants that support set comprehensions defined in such a way
> RDA> that the parser has to generate an invisible bound variable?
> 
> RDA> This results in surprising behaviour like:
> 
> RDA> # `{x | x > 9}` = `{x | x > 9}`;;
> RDA> val it : bool = false
> 

Re: [Hol-info] HOL Light set comprehensions

[Bill R. <ri...@ma...>]

Thanks, Rob!  Can you explain how HOL4 performs the quantification with GSPEC?  I would think that GSPEC would have to choose a fresh variable, and I've never understood how that's to be done, because you have know that your new fresh variable hasn't already been chosen.  So I would think that the HOL Light method of having the parser choose the fresh variable was defensible.

   GSPEC : ('a -> 'b # bool) -> 'b -> bool with (essentially) the
   following defining property:

	   GSPEC f v = ?x. f x = (v, T)

So it's GSPEC that chooses the fresh variable, because we need x to not be free in v, right?  

   and then the parser translates {y + 6 | y < 0} into GSPEC(\y.(y + 6, y < 0)). 

How does GSPEC know to use the same variable y?  

   In HOL Light there is a constant called GSPEC, but it is just the
   identify function, 

Thanks!  I had wondered about the sets.ml definition: 

let GSPEC = new_definition
  `GSPEC (p:A->bool) = p`;;

   the semantics of the set comprehension are given by something
   called SETSPEC, which has to appear in a context where a variable
   representing a candidate for membership of the set comprehension is
   in scope.

Could you clarify?  Here's the sets.ml definition, which I would like to understand:

let SETSPEC = new_definition
  `SETSPEC v P t <=> P /\ (v = t)`;;

As I posted before, SETSPEC is used by parser.ml to create set abstractions 

    let v = pgenvar() in
    let bod = itlist (curry pmk_exists) bvs
                     (Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs)) in
    Combp(Varp("GSPEC",dpty),Absp(v,bod)) 

and I'd really like to understand this, as well as everything else in parser.ml.

Perhaps I can elaborate.  My RichterHilbertAxiomGeometry/readable.ml does I think a nice job of allowing readable HOL Light proofs, with a minimum of type annotations, double-quotes and back-quotes.  Basically it's a version of Freek's miz3 that allows full use of tactics like REWRITE_TAC.  I'm pretty happy with it, but I wonder if I couldn't substitute some straightforward camlp parsing for the exec I'm borrowing from update_database.ml.  So my first task is the understand parser.ml.

-- 
Best,
Bill 

Re: [Hol-info] HOL Light set comprehensions

[Rob A. <rd...@le...>]

On 13 Dec 2013, at 03:51, Bill Richter wrote:

> Thanks, Rob!  Can you explain how HOL4 performs the quantification with GSPEC?  I would think that GSPEC would have to choose a fresh variable, and I've never understood how that's to be done, because you have know that your new fresh variable hasn't already been chosen.  So I would think that the HOL Light method of having the parser choose the fresh variable was defensible.
> 
> >  GSPEC : ('a -> 'b # bool) -> 'b -> bool with (essentially) the
> >  following defining property:
> 
> >	   GSPEC f v = ?x. f x = (v, T)
> 
> So it's GSPEC that chooses the fresh variable, because we need x to not be free in v, right?  
> 
> >  and then the parser translates {y + 6 | y < 0} into GSPEC(\y.(y + 6, y < 0)). 
> 
> How does GSPEC know to use the same variable y?  

GSPEC is an object language constant. It is the parser that chooses the names
for the bound variable. As far as the parser is concerned GSPEC is just a piece
of data it uses to construct the parsed term. The resulting term GSPEC(\y.(y + 6, y < 0))
only contains one bound variable.

> 
> >  In HOL Light there is a constant called GSPEC, but it is just the
> >  identify function, 
> 
> Thanks!  I had wondered about the sets.ml definition: 
> 
> let GSPEC = new_definition
>  `GSPEC (p:A->bool) = p`;;
> 
> >  the semantics of the set comprehension are given by something
> >  called SETSPEC, which has to appear in a context where a variable
> >  representing a candidate for membership of the set comprehension is
>   in scope.
> 
> Could you clarify?  Here's the sets.ml definition, which I would like to understand:
> 
> let SETSPEC = new_definition
>  `SETSPEC v P t <=> P /\ (v = t)`;;

In words: SETSPEC has type 'a -> bool -> 'a -> bool and is true for a trio of arguments v, P and t
iff v is equal to t and P is true. In all the HOLs, you will find that the parser uses various constants
like this to represent derived syntactic constructs (like set comprehensions) in terms of primitive
constructs (like conjunction and equality) in such a way that the pretty-printer can recover the
structure of the derived construct from the primitive syntax. The details of the encoding are
not standardised, and I don't know why the above definition has been chosen in HOL Light.
(As I said, it seems inside out to me.)

> 
> As I posted before, SETSPEC is used by parser.ml to create set abstractions 
> 
>    let v = pgenvar() in
>    let bod = itlist (curry pmk_exists) bvs
>                     (Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs)) in
>    Combp(Varp("GSPEC",dpty),Absp(v,bod)) 
> 
> and I'd really like to understand this, as well as everything else in parser.ml.
> 

> Perhaps I can elaborate.  My RichterHilbertAxiomGeometry/readable.ml does I think a nice job of allowing readable HOL Light proofs, with a minimum of type annotations, double-quotes and back-quotes.  Basically it's a version of Freek's miz3 that allows full use of tactics like REWRITE_TAC.  I'm pretty happy with it, but I wonder if I couldn't substitute some straightforward camlp parsing for the exec I'm borrowing from update_database.ml.  So my first task is the understand parser.ml.


One way to find out what is going on is to example terms and then use the term destructor
functions dest_comb and dest_abs to pick apart what the parser produced.

Regards,

Rob.

Re: [Hol-info] HOL Light set comprehensions

[Bill R. <ri...@ma...>]

Thanks, Rob!  This is helpful info:

   In all the HOLs, you will find that the parser uses various
   constants like [the SETSPEC definition] to represent derived
   syntactic constructs (like set comprehensions) in terms of
   primitive constructs (like conjunction and equality) in such a way
   that the pretty-printer can recover the structure of the derived
   construct from the primitive syntax.

This won't help me understand parser.ml, but I it will help me understand sets.ml.  I tried your dest_comb and dest_abs tricks on your original example: 

# `{y | y > 6}`;;
val it : term = `{y | y > 6}`
# dest_comb it;;
val it : term * term =
  (`GSPEC`, `\GEN%PVAR%218. ?y. SETSPEC GEN%PVAR%218 (y > 6) y`)
# dest_abs it;;
Error: This expression has type term * term
       but an expression was expected of type term = Hol.term

I tried something like this when you first posted, but I didn't think to use dest_comb.  Do you have any general tips on how to recognize a term as say a combination (which worked here) on an abstraction (not here)?

-- 
Best,
Bill 

Re: [Hol-info] HOL Light set comprehensions

[Michael N. <mic...@ni...>]

On 18/12/13 14:56, Bill Richter wrote:
> I tried something like this when you first posted, but I didn't think to use
> dest_comb.  Do you have any general tips on how to recognize a term as say a
> combination (which worked here) on an abstraction (not here)?

Try using a match-expression:

    match tm with
      Var(_,_) -> "it's a var"
    | Const(_,_) -> "it's a const"
    | Comb(_,_) -> "it's an application"
    | Abs(_,_) -> "it's an abstraction"

You can also use the helper functions is_comb, is_abs, is_const, and is_var.

Michael

Re: [Hol-info] HOL Light set comprehensions

[Rob A. <rd...@le...>]

On 18 Dec 2013, at 04:21, Michael Norrish wrote:

> On 18/12/13 14:56, Bill Richter wrote:
>> I tried something like this when you first posted, but I didn't think to use
>> dest_comb.  Do you have any general tips on how to recognize a term as say a
>> combination (which worked here) on an abstraction (not here)?
> 
> Try using a match-expression:
> 
>    match tm with
>      Var(_,_) -> "it's a var"
>    | Const(_,_) -> "it's a const"
>    | Comb(_,_) -> "it's an application"
>    | Abs(_,_) -> "it's an abstraction"
> 
> You can also use the helper functions is_comb, is_abs, is_const, and is_var.
> 


That is of course the right approach if you are actually programming rather than just
playing around interactively. If you are looking at the pretty-printed term that you
want to destroy, then you should be able to see at a glance what to do (assuming
HOL4 and HOL Light are like ProofPower-HOL}, since in ProofPower-HOL, at least,
lambda-abstractions are never pretty-printed as anything other than lambda-abstractions.
lambda-abstractions where the "bound variable" is actually several variables combined
with a comma (like \(x, y).x + y) are actually applications (\(x, y). x + y is really Uncurry(\x y. x + y)).
So, if you are just interactively picking terms apart then the rule is use dest_comb
(actually called dest_app in ProofPower) unless the thing pretty--prints as a single
variable or constant or as "\v ..." where v is a plain variable.

Regards,

Rob.

Re: [Hol-info] HOL Light set comprehensions

[Bill R. <ri...@ma...>]

Michael, that's very helpful!  You taught me something about term.ml, and reminded me of that every HOL term is either a constant, a variable, a function (abstraction) or a function application (combination).  So pasting your code into HOL Light gives the right answers:

let PrintTermType tm =
 match tm with
   Var(_,_) -> "it's a var"
 | Const(_,_) -> "it's a const"
 | Comb(_,_) -> "it's an application"
 | Abs(_,_) -> "it's an abstraction";;

PrintTermType `\y. y > 6`;;
PrintTermType `{y | y > 6}`;;
PrintTermType `{y + 2 | y > 6}`;;
is_comb `\y. y > 6`;;
is_var `\y. y > 6`;;
is_const `\y. y > 6`;;
is_abs `\y. y > 6`;;
is_numeral `1`;;
is_const `1`;;
is_comb `1`;;
dest_comb `{y + 2 | y > 6}`;;
#   val it : string = "it's an abstraction"
# val it : string = "it's an application"
# val it : string = "it's an application"
# val it : bool = false
# val it : bool = false
# val it : bool = false
# val it : bool = true
# val it : bool = true
# val it : bool = false
# val it : bool = true

Now this last part surprised me.  I didn't know that numerals are combinations, and I would have guessed they were constants.  So let me practice my is_*/dest_* skills:

dest_comb `1`;;

  val it : term * term = (`NUMERAL`, `BIT1 _0`)

And I think this must be largely defined by this code in nums.ml:

(* ------------------------------------------------------------------------- *)
(* Syntax operations on numerals.                                            *)
(* ------------------------------------------------------------------------- *)

let mk_numeral =
  let Z = mk_const("_0",[])
  and BIT0 = mk_const("BIT0",[])
  and BIT1 = mk_const("BIT1",[])
  and NUMERAL = mk_const("NUMERAL",[])
  and zero = num_0 in
  let rec mk_num n =
    if n =/ num_0 then Z else
    mk_comb((if mod_num n num_2 =/ num_0 then BIT0 else BIT1),
            mk_num(quo_num n num_2)) in
  fun n -> if n </ zero then failwith "mk_numeral: negative argument"
           else mk_comb(NUMERAL,mk_num n);;

And I also see that your cool Ocaml code above isn't that different from the defs in term.ml: 

  let is_var = function (Var(_,_)) -> true | _ -> false
  let is_const = function (Const(_,_)) -> true | _ -> false
  let is_abs = function (Abs(_,_)) -> true | _ -> false
  let is_comb = function (Comb(_,_)) -> true | _ -> false


RDA> the [HOL4] parser translates {y + 6 | y < 0} into 
RDA> GSPEC(\y.(y + 6, y < 0))

Rob, thanks for explaining some HOL Light to me.  Can you (or Michael) explain better the HOL4 GSPEC?  You say that 

It's great that HOL4 isn't grabbing a fresh variable, but I don't get it.  I suppose HOL4 could check that there's only one free variable, y, in the 2 "sides" of the set comprehension, and then make an abstraction using the ordered pair.  But now GSPEC has to translate this ordered pair abstraction into the set we want.  Let's look at a more general case

{F x y z | R x y z}

for a function F and a predicate R.  HOL Light does what I think is the obvious thing, turning this into

λa. ∃ x y z. a = F x y z ∧ R x y z

That's the only abstraction I can think of.  Now in my case above, I can translate to a nice abstraction, because 

a ∈ {y + 6 | y < 0}  ⇔  ∃y. a = y + 6 ∧ y < 0

 ⇔ ∃y. y = a - 6 ∧ a - 6 < 0  ⇔ a - 6 < 0

and therefore {y + 6 | y < 0} should be equal to 

λa. a - 6 < 0 = λy. y - 6 < 0, so 

{y + 6 | y < 0} = λy. y - 6 < 0

But I don't know how to do that in general.  BTW it seems that HOL Light is doing a curried version of your ordered pair: 

dest_comb `{y + 2 | y > 6}`;;
  val it : term * term =
  (`GSPEC`, `\GEN%PVAR%1068. ?y. SETSPEC GEN%PVAR%1068 (y > 6) (y + 2)`)

Ah, and I finally understand this!  From sets.ml:

let GSPEC = new_definition
  `GSPEC (p:A->bool) = p`;;

let SETSPEC = new_definition
  `SETSPEC v P t <=> P /\ (v = t)`;;

So the above ordered pair coming from {y + 2 | y > 6} is is a combination where we're supposed to apply the first coordinate to the second.  Since, as you posted, GSPEC is the identity  this means (replacing the fresh variable GEN%PVAR%1068 with a)

(\a. ?y. SETSPEC a (y > 6) (y + 2))  =  (\a. ?y. (y > 6) /\ a = (y + 2))

which is what I wanted.  Now as I said above, this lambda is equal to 

(\a. ?y. (y > 6) /\ y = a - 2)  =  (\a. ?y. (y > 6) /\ y = a - 2)  =  
(\a. ?y. (a - 2 > 6) /\ y = a - 2)  =  (\a. a  > 8)  =  (\y. y  > 8)

after an alpha conversion, and this is correct, the set {y | y > 8}.

-- 
Best,
Bill

Re: [Hol-info] HOL Light set comprehensions

[Rob A. <rd...@le...>]

Bill,

On 27 Dec 2013, at 18:47, Bill Richter wrote:

> ...

> Now this last part surprised me.  I didn't know that numerals are combinations, and I would have guessed they were constants.  So let me practice my is_*/dest_* skills:
> 
> dest_comb `1`;;
> 
>  val it : term * term = (`NUMERAL`, `BIT1 _0`)
> 
Good point. In my earlier post giving a rule of thumb for recognising when dest_comb is applicable, I forgot that
(unlike ProofPower-HOL), numeric literals in HOL4 and HOL Light print as if they are atomic but are actually
nested applications representing an encoding of the number as a string of 0s and 1s. 

> And I think this must be largely defined by this code in nums.ml:
> 
> (* ------------------------------------------------------------------------- *)
> (* Syntax operations on numerals.                                            *)
> (* ------------------------------------------------------------------------- *)
> 
> let mk_numeral =
>  let Z = mk_const("_0",[])
>  and BIT0 = mk_const("BIT0",[])
>  and BIT1 = mk_const("BIT1",[])

The definitions should make it clear how these things work:

# ZERO_DEF;;
val it : thm = |- _0 = mk_num IND_0
# NUMERAL;;
val it : thm = |- !n. NUMERAL n = n
# BIT0_DEF;;
val it : thm = |- BIT0 0 = 0 /\ (!n. BIT0 (SUC n) = SUC (SUC (BIT0 n)))
# BIT1_DEF;;
val it : thm = |- !n. BIT1 n = SUC (BIT0 n)

IND_0 is the representative of zero in the type ind that provides the representation
type for the natural numbers. NUMERAL is just an alias for the identity function
that provokes the pretty-printer into recognising the term as a numeric literal.
BIT0 is \n.2n and BIT1 is \n.2n+1. Hence a string of BIT0s and BIT1 applied to
_0 gives the binary representation of a number in reverse order:

# `NUMERAL(BIT1(BIT1(BIT0(BIT1 _0))))`;;
val it : term = `11`

N.b., the above is specific to HOL Light. HOL4 uses a different representation
based on BIT1 and BIT2 = \n.2n + 2.

> Rob, thanks for explaining some HOL Light to me.  Can you (or Michael) explain better the HOL4 GSPEC?  You say that 
> 
> It's great that HOL4 isn't grabbing a fresh variable, but I don't get it.  I suppose HOL4 could check that there's only one free variable, y, in the 2 "sides" of the set comprehension, and then make an abstraction using the ordered pair.  But now GSPEC has to translate this ordered pair abstraction into the set we want.  Let's look at a more general case
> 
> {F x y z | R x y z}
> 
> for a function F and a predicate R.

Here is the equivalent of HOL4's GSPEC defined in HOL Light:

let HOL4_GSPEC = new_definition `HOL4_GSPEC f v = ?x. f x = (v, T)`;;

The following proof shows that this can be used to represent a set comprehension
without introducing any extra bound variables:

g `{f x | R x} = HOL4_GSPEC (\x.(f x, R x))`;;
e(REWRITE_TAC[SETSPEC; GSPEC; EXTENSION; HOL4_GSPEC; IN; PAIR_EQ]);;
e(MESON_TAC[]);;
let thm1 = top_thm();;


>  HOL Light does what I think is the obvious thing, turning this into
> 
> λa. ∃ x y z. a = F x y z ∧ R x y z
> 
> That's the only abstraction I can think of. 

The HOL4 design sees two abstractions here: `\(x, y, z). f x y z` and `\(x, y, z). R x y z`
and combines them together into one abstraction `\(x, y, z). (f x y z, R x y z)`.
This contains all the information needed to construct the set comprehension and the
HOL4 formulation of GSPEC captures that construction.

Regards,

Rob.