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