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
------------------------------------------------------------------------------
Rapidly troubleshoot problems before they affect your business. Most IT
organizations don't have a clear picture of how application performance
affects their revenue. With AppDynamics, you get 100% visibility into your
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
