Bill,
On 1 Jan 2014, at 03:04, Bill Richter wrote:
> Rob, I learned a lot from your post! My conclusion is that in both HOL Light
> and HOL4,
> {f x | R x} = λa. ∃x. R x ∧ a = f x
> for some variable a than is not free in R x or f x. I judge both HOL
> approaches to have pluses & minuses, and can't rate one above the other:
>
> 1) In HOL Light, the proof of this equation is immediate, as parser defines
> {f x | R x} to be the RHS. However, we always generate a fresh variable,
> ones with odd-sounding (although unseen) names like GEN%PVAR%1066.
>
> 2) In HOL4, the parser's definition of {f x | R x} involves no fresh
> variables, but calculating a in the above equation was beyond my
> skill/patience here, as there are many cases to consider.
Why do you need to calculate it?
>
> # dest_comb `{f x | R x}`;;
> val it : term * term =
> (`GSPEC`, `\GEN%PVAR%1066. ?x. SETSPEC GEN%PVAR%1066 (R x) (f x)`)
>
> I like this approach for its simplicity: ``Let's choose a fresh variable,
> whether we need it or not, without studying the free & bound variables.''
> The HOL4 approach, as you explained it, looks more elegant, but if you want
> to understand what alpha-conversions take place, you need a serious
> investigation that I couldn't complete here.
When you rewrite with the definition, the system will use its standard
mechanisms for
renaming bound variables to avoid variable capture. The user shouldn't need to
second
guess what renamings take place.
> ...
> let HOL4_GSPEC = NewDefinition `; HOL4_GSPEC = (λf. (λv. ∃r. f r = (v, T)))`;;
>
> interactive_goal `;
> f = (λx. (λr. r + x)) ⇒ {f x | R x} = HOL4_GSPEC (\x. (f x, R x))
> `;;
> interactive_proof `;
> intro_TAC fDef;
> rewrite SETSPEC GSPEC HOL4_GSPEC PAIR_EQ;
> `;;
>
> `(\GEN%PVAR%479. ?x. R x /\ GEN%PVAR%479 = f x) = (\v. ?r. f r = v /\ R r)`
>
> The whole point is the next step, where I expected alpha-conversion of the
> outer (existential) r:
>
> interactive_proof `;
> rewrite fDef;
> `;;
>
> `(\GEN%PVAR%479. ?x. R x /\ GEN%PVAR%479 = (\r. r + x)) =
> (\v. ?r. (\r'. r' + r) = v /\ R r)`
>
> I was wrong; it was the inner (abstraction) r that was alpha-converted.
Rewriting works by picking terms apart looking for subterms that
can be transformed and then reconstructing the outer structure around
the transformed subterms. When it did the beta-conversion on `(\x.\r.r + x) r`,
the rewriter had to substitute `r` for `x` in `\r.r + x`. The result has to be
`\r'.r' + r` so that it has the right free variables, namely `r`, ready to be
bound by the existential quantifier when the outer structure is wrapped
around the result of the beta-conversion.
> Here's an example with ¬(r = x) and r free in (f x, R x):
>
> interactive_goal `;
> f = (λx. r + x) ⇒ {f x | R x} = HOL4_GSPEC (\v. (f v, R v))
> `;;
> interactive_proof `;
> intro_TAC fDef;
> rewrite fDef;
> rewrite HOL4_GSPEC PAIR_EQ;
> `;;
>
> `{r + x | R x} = (\v. ?r'. r + r' = v /\ R r')`
>
> Now the outer (existential) r was alpha-converted.
That's because you expanded the definitions in a different order
(f then HOL4_GSPEC rather than HOL4_GSPEC then f). Immediately
after expanding the definition of HOL4_GSPEC the right-hand side
of the equation looked like this `(\f v. ?r. f r = (v,T)) (\v. r + v,R v)`
and beta-conversion must rename the existentially quantified r.
This is a good example to show that you shouldn't be trying to
second guess the outcome of bound variable renaming. It is very
sensitive to the order in which things are done.
> ...
> 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.
>
> Wow, that's cool! Is this due to Konrad and Michael, or does it go way back?
> I never would have thought of such stunts.
I don't know who designed this particular bit of HOL4, but the
general idea goes way back: to give semantics to a language
construct, you identify the constituent parts of the construct
and express their semantics in such a way that you can define
a function that combines the semantic values of the constituents
to give the semantic value of the whole construct. This technique
is called "semantic embedding" and has been widely used,
e.g., to represent programming languages in HOL and similar systems.
Here the two abstractions `\(x, y, z). f x y z` and `\(x, y, z). R x y z`
represent the semantic values of the constituents of the set comprehension.
The semantic value of the set comprehension is obtained by combining
these two abstractions into one and applying HOL4_GSPEC.
> ...
> g `{f x y z | R x y z} = HOL4_GSPEC (\(x, y, z). (f x y z, R x y z))`;;
>
> e(REWRITE_TAC [HOL4_GSPEC; PAIR_EQ; IN_ELIM_THM; EXISTS_PAIR_THM; EXTENSION;
> IN_ELIM_THM]);;
>
> `!x. (?x y z. R x y z /\ x = f x y z) <=>
> (?p1 p1 p2. f p1 p1 p2 = x /\ R p1 p1 p2)`
>
> That looks like a variable capture error (on top of the repeated p1), one
> that we know (since the theorem was proved) didn't actually take place. The
> pretty-printer ought to have printed
>
> `!x'. (?x y z. R x y z /\ x' = f x y z) <=>
> (?p1 p1 p2. f p1 p1 p2 = x /\ R p1 p1 p2)`
> ...
> Does anyone understand the HOL Light pretty-printing of freshly generated
> variables, or know where it's done?
I think you will find the pretty-printer just prints the names of the actual
variables that
it finds in the terms - it is not the pretty-printer's job to resolve variable
capture problems.
In this case, the two instances of x have different types and there is no
variable
capture, since two variables with the same name but different types are
considered to
be distinct in the logic. Here is an extreme example of this phenomenon:
# BETA_CONV `(\(x : 'a -> 'b) (y : 'a).x y) y`;;
val it : thm = |- (\x y. x y) y = (\y. y y)
Aside: annoyingly,the pretty-printer has output the term on the right-hand side
of the
above equation in a form that will not be accepted by the parser. You would have
to jump through hoops with mk_var, mk_comb and mk_abs to enter that term.
You will have similar problems with the pretty-printer output in your example.
(In ProofPower, we have a tactic called rename_tac that renames variables in a
goal
as necessary so that distinct variables in the same scope have distinct names.
HOL Zero has a pretty-printer that checks for this kind of problem and always
outputs something that can be parsed back in again.)
If I modify your example so that the result of f has the same type as its first
argument,
then there is a potential variable capture problem and the renaming you expected
does happen (but it is the inner x that gets renamed):
# g `{f x y z : 'a | R (x : 'a) y z} = HOL4_GSPEC (\(x, y, z). (f x y z, R x y
z))`;;
Warning: inventing type variables
Warning: Free variables in goal: R, f
val it : goalstack = 1 subgoal (1 total)
`{f x y z | R x y z} = HOL4_GSPEC (\(x,y,z). f x y z,R x y z)`
# e(REWRITE_TAC [HOL4_GSPEC; PAIR_EQ; IN_ELIM_THM; EXISTS_PAIR_THM; EXTENSION;
IN_ELIM_THM]);;
val it : goalstack = 1 subgoal (1 total)
`!x. (?x' y z. R x' y z /\ x = f x' y z) <=>
(?p1 p1 p2. f p1 p1 p2 = x /\ R p1 p1 p2)`
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
