Re: [Hol-info] More on set comprehensions
Rob, I think Michael's IMAGE idea may show that I was wrong about your semantic
embedding idea. I said that I was happy with the HOL Light parser's definition
of the set comprension
{f x | R x} = {a | ∃x. a = f x ∧ R x}
and I didn't think that it made sense to talk about the semantic value of f x
and R x here. But maybe I was wrong, because this set comprension is an image,
the image of the function f on the set of x such that R x, and this set is in
fact equal to R. Let's look at HOL's IMAGE:
IMAGE;;
val it : thm = |- !s f. IMAGE f s = {y | ?x. x IN s /\ y = f x}
type_of `IMAGE`;;
Warning: inventing type variables
val it : hol_type = `:(?86076-?86077)-(?86076-bool)-?86077-bool`
So IMAGE has polymorphic type
(A-B)-(A-bool)-B-bool
Now I'm sorry I haven't pursued this myself. But I think your
HOL4/semantic-embedding ideas give a way to define IMAGE independently of {...}
which need to be parsed. Is that what you did, or something that you can do?
--
Best,
Bill
--
CenturyLink Cloud: The Leader in Enterprise Cloud Services.
Learn Why More Businesses Are Choosing CenturyLink Cloud For
Critical Workloads, Development Environments Everything In Between.
Get a Quote or Start a Free Trial Today.
http://pubads.g.doubleclick.net/gampad/clk?id=119420431iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] More on set comprehensions
Mark,
On 8 Jan 2014, at 03:22, Mark Adams wrote:
Not wanting to be too picky here (because I very much agree with the thrust
of what Rob is saying), but isn't ProofPower term quotation parsing
sensitive to the subgoal package state (specifically, free variables in term
quotations pick up the types of existing free variables in the subgoal
package proof)?
Yes. That's why I mentioned a context when I said the same string of symbols
should always parse to the same
term in any given context.
Regards,
Rob.
Mark.
on 7/1/14 5:04 PM, Rob Arthan r...@lemma-one.com wrote:
Bill,
On 4 Jan 2014, at 05:17, Bill Richter wrote:
...
On 7 Jan 2014, at 16:22, Rob Arthan wrote:
I think we will just have to agree differ about this. Let me just make
two
comments:
Something very odd happened with my e-mail client which caused it to
discard
the
two comments. They were as follows:
(a) Too much mathematical notation is explained away as short-hands, i.e.,
as syntactic abbreviations. This is a consequence of the traditional
pretence that mathematics is founded on first-order set theory and
of the inexpressiveness of first-order languages. In a higher-order
logic you can generally replace these short-hands by first class
mathematical
citizens that you can reason about in their own right. This often
fits in well with a categorical way of thinking about what you are
doing. In the case in point, the categorical account of set comprehensions
would be in the category of sets and relations. Let me write R : X - Y
to mean that R is a relation between the sets X and Y and let BOOL
be the two-point set {F, T}. Given a relation R:X - BOOL, we
associate the subset R^{-1}({T}). Given a function f : X - Y and
a function p : X - BOOL, we get a relation R : Y - BOOL
in the obvious way by defining R = p o f^{-1} and hence
the associated subset R^{-1}({T}) of Y. Note there are no bound variables
in this categorical description of {f x | p x}: they are all hidden in the
definitions of relational composition, relational image and
relational inverse. From what you say above you would
presumably object to that.
(b) My original objection was that something like
`{x | x 0}` = `{x | x 0}` evaluates to false in HOL Light
because the two terms use a different name for the
hidden bound variable that you are so fond of. I now
realise that things like `x` = `x` also evaluate false
because you get different type variables. I can only conclude
that the HOL Light parser does not share what I know was
a design goal of the ProofPower-HOL parser which was that
the same string of symbols should always parse to the same
term in any given context. I suspect this is also a design goal
of the HOL4 parser (which, like ProofPower-HOL, uses
'a, 'b, 'c etc. for invented type variables).
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=84349831iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
--
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=84349831iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] More on set comprehensions
Bill,
On 4 Jan 2014, at 05:17, Bill Richter wrote:
...
On 7 Jan 2014, at 16:22, Rob Arthan wrote:
I think we will just have to agree differ about this. Let me just make two
comments:
Something very odd happened with my e-mail client which caused it to discard the
two comments. They were as follows:
(a) Too much mathematical notation is explained away as short-hands, i.e.,
as syntactic abbreviations. This is a consequence of the traditional
pretence that mathematics is founded on first-order set theory and
of the inexpressiveness of first-order languages. In a higher-order
logic you can generally replace these short-hands by first class mathematical
citizens that you can reason about in their own right. This often
fits in well with a categorical way of thinking about what you are
doing. In the case in point, the categorical account of set comprehensions
would be in the category of sets and relations. Let me write R : X - Y
to mean that R is a relation between the sets X and Y and let BOOL
be the two-point set {F, T}. Given a relation R:X - BOOL, we
associate the subset R^{-1}({T}). Given a function f : X - Y and
a function p : X - BOOL, we get a relation R : Y - BOOL
in the obvious way by defining R = p o f^{-1} and hence
the associated subset R^{-1}({T}) of Y. Note there are no bound variables
in this categorical description of {f x | p x}: they are all hidden in the
definitions of relational composition, relational image and
relational inverse. From what you say above you would
presumably object to that.
(b) My original objection was that something like
`{x | x 0}` = `{x | x 0}` evaluates to false in HOL Light
because the two terms use a different name for the
hidden bound variable that you are so fond of. I now
realise that things like `x` = `x` also evaluate false
because you get different type variables. I can only conclude
that the HOL Light parser does not share what I know was
a design goal of the ProofPower-HOL parser which was that
the same string of symbols should always parse to the same
term in any given context. I suspect this is also a design goal
of the HOL4 parser (which, like ProofPower-HOL, uses
'a, 'b, 'c etc. for invented type variables).
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=84349831iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] More on set comprehensions
Not wanting to be too picky here (because I very much agree with the thrust
of what Rob is saying), but isn't ProofPower term quotation parsing
sensitive to the subgoal package state (specifically, free variables in term
quotations pick up the types of existing free variables in the subgoal
package proof)?
Mark.
on 7/1/14 5:04 PM, Rob Arthan r...@lemma-one.com wrote:
Bill,
On 4 Jan 2014, at 05:17, Bill Richter wrote:
...
On 7 Jan 2014, at 16:22, Rob Arthan wrote:
I think we will just have to agree differ about this. Let me just make
two
comments:
Something very odd happened with my e-mail client which caused it to
discard
the
two comments. They were as follows:
(a) Too much mathematical notation is explained away as short-hands, i.e.,
as syntactic abbreviations. This is a consequence of the traditional
pretence that mathematics is founded on first-order set theory and
of the inexpressiveness of first-order languages. In a higher-order
logic you can generally replace these short-hands by first class
mathematical
citizens that you can reason about in their own right. This often
fits in well with a categorical way of thinking about what you are
doing. In the case in point, the categorical account of set comprehensions
would be in the category of sets and relations. Let me write R : X - Y
to mean that R is a relation between the sets X and Y and let BOOL
be the two-point set {F, T}. Given a relation R:X - BOOL, we
associate the subset R^{-1}({T}). Given a function f : X - Y and
a function p : X - BOOL, we get a relation R : Y - BOOL
in the obvious way by defining R = p o f^{-1} and hence
the associated subset R^{-1}({T}) of Y. Note there are no bound variables
in this categorical description of {f x | p x}: they are all hidden in the
definitions of relational composition, relational image and
relational inverse. From what you say above you would
presumably object to that.
(b) My original objection was that something like
`{x | x 0}` = `{x | x 0}` evaluates to false in HOL Light
because the two terms use a different name for the
hidden bound variable that you are so fond of. I now
realise that things like `x` = `x` also evaluate false
because you get different type variables. I can only conclude
that the HOL Light parser does not share what I know was
a design goal of the ProofPower-HOL parser which was that
the same string of symbols should always parse to the same
term in any given context. I suspect this is also a design goal
of the HOL4 parser (which, like ProofPower-HOL, uses
'a, 'b, 'c etc. for invented type variables).
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=84349831iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] More on set comprehensions
Rob, thanks for correcting my variable capture mistake:
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.
Right, and you have to do the type inference. Here's a simpler version of what
puzzled me:
g `!t. t IN IMAGE f s == x IN t`;;
e(REWRITE_TAC[FORALL_IN_IMAGE]);;
`!x. x IN s == x IN f x`
t has type A-bool, so x has type A, so f has type B-A, so s has type B-bool.
Now we want to rewrite with FORALL_IN_IMAGE, which for convenience we'll
alpha-convert to
|- !f s. (!t. t IN IMAGE f s == P t) = (!b. b IN s == P (f b))
For us, P t = (x IN t), and rewriting with FORALL_IN_IMAGE gives us
!b. b IN s == x IN f b
But b has type B, and B and A are taken to be different, so we can replace b
with x, and get HOL Light's answer
!x. x IN s == x IN f x.
Thanks for explaining this, as it's been bothering me for some time. Your
example is even simpler, especially if we remove your type inferences:
BETA_CONV `(\x. (\y. x y)) y`;;
Warning: inventing type variables
val it : thm = |- (\x y. x y) y = (\y. y y)
That's
(\y. x y) [x/y] = (\y'. x y') [x/y] = (\y'. y y')
But the bound occurrence of y has type B, so x has type B-A, so the free y has
type B-A as well. So HOL Light's answer above is correct, because
(\y. y y)means
(\y:B. (y:B-A) (y:B)).
You're right about my first alpha-conversion problem:
Since the occurrence of r in f is bound, there's no problem substituting
f = (\x r. r + x)
into
(\v. ?r. f r = v /\ R r)
and we get
(\v. ?r. (\x r. r + x) r = v /\ R r)
and the alpha-conversion comes from your beta-conversion
(\x r. r + x) r = (\x. \r'. r' + x) r = \r'. r' + r.
Thanks, and I should have seen that.
That's because you expanded the definitions in a different order (f
then HOL4_GSPEC rather than HOL4_GSPEC then f).
I think that's wrong, because I get the same answer no matter which order I
expand HOL4_GSPEC and the definition of f.
Immediately after expanding the definition of HOL4_GSPEC the
right-hand side of the equation looked like this `(\f v. ?r. f r
=3D (v,T)) (\v. r + v,R v)` and beta-conversion must rename the
existentially quantified r.
That's right, but look:
needs RichterHilbertAxiomGeometry/readable.ml;; (* extensively commented *)
let HOL4_GSPEC = NewDefinition `; HOL4_GSPEC = (λf. (λv. ∃r. f r = (v, T)))`;;
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')`
interactive_goal `;
f = (λx. r + x) ⇒ {f x | R x} = HOL4_GSPEC (\v. (f v, R v))
`;;
interactive_proof `;
intro_TAC fDef;
rewrite HOL4_GSPEC PAIR_EQ;
rewrite fDef;
`;;
`{r + x | R x} = (\v. ?r'. r + r' = v /\ R r')`
So the expandsion order doesn't matter The real issue is that r is now free in
(f x, R x), unlike the first example.
Why do you need to calculate it?
We don't need to, but you I were discussing the merits of the two HOL defs of
{f x | R x}. I argued that that that HOL4 definition looks more elegant, the
Lambda Calculus is more complicated: if you want to understand the alpha
conversions, it takes work, while the HOL Light parser performs the one alpha
conversion you need automatically.
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.
Nice, and in Denotational Semantics one says that we have a compositional
semantic function. So there's more semantic embedding in HOL4 than Hol Light
here. But I would not have insisted on semantic embedding here. I would not
say that in {f x y z | R x y z}, the two expressions
f x y z and R x y z should have semantic values, nor would I say that their
semantic values were your abstractions. I would say that
{f x y z | R x y z}
is an expression that we understand really means is HOL Light's
{a | ∃x y z. a = f x y z ∧ R x y z}
To see this, think of a mathematical function f: X --- Y between sets and a
subset A of X. Then we speak of the image f(A), which is a subset of Y,
defined by
f(A) = {f(a) | a ∈ A}.
But what does that mean? I claim it's just a short-hand for
{b | ∃a ∈ A. b = f(a)}.
Or back to HOL, we of course
Re: [Hol-info] More on set comprehensions
On 4 Jan 2014, at 6:17 pm, Bill Richter rich...@math.northwestern.edu wrote:
To see this, think of a mathematical function f: X --- Y between sets and a
subset A of X. Then we speak of the image f(A), which is a subset of Y,
defined by
f(A) = {f(a) | a ∈ A}.
But what does that mean? I claim it's just a short-hand for
{b | ∃a ∈ A. b = f(a)}.
Or back to HOL, we of course know that sets are just a way of talking about
abstractions of type alpha-bool. So I say before finding the semantic
value, we must first turn
{f x y z | R x y z}
into an abstraction, and that means
λa. ∃x y z. a = f x y z ∧ R x y z
where a must not be free in f x y z or R x y z.
It is easy to see the connection between HOL4_GSPEC and image. The former has
type
:(A - bool # B) - (B - bool)
we know that functions into a product (the first argument above) are in
bijection with a pair of functions so that the type above is in bijection with
the type
:(A - bool) # (A - B) - (B - bool)
If you curry this type and reorder, then you get
:(A - B) - (A - bool) - (B - bool)
which is exactly the type you'd expect to see for image.
In other words, you might argue that given IMAGE (as it is called in HOL4),
GSPEC is actually redundant. However, forcing users to give up on the nice
syntax that we/they expect to be able to use is usually a bad idea. The exact
encoding used underneath the covers of that syntax is less important.
Incidentally, GSPEC in HOL4 predates my involvement in the system. If forced
to guess, I’d hazard that it’s due to Tom Melham, who did a lot of the early
work on that part of the system. He defined cardinality for example; comments
still in the sources suggesting this happened in early 1991.
Happy New Year.
Michael
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
--
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=84349831iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] More on set comprehensions
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
Re: [Hol-info] More on set comprehensions
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.
# 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. Let me make a two minor changes to your code:
# let HOL4_GSPEC = new_definition `HOL4_GSPEC = (\f. (\v. ?r. f r = (v, T)))`;;
Let's study your {f x | R x} = HOL4_GSPEC (λx. (f x, R x)) :
HOL4_GSPEC (λx. (f x, R x))
=
(λf. (λv. ∃r. f r = (v, T))) (λx. (f x, R x))
=
λv. ∃r. (λx. (f x, R x)) r = (v, T)
as long as v and r are not free in (λx. (f x, R x)). Assuming this, and that r
is not a bound variable in (f x, R x), we have
= λv. ∃r. (f r, R r) = (v, T)
=
λv. ∃r. f r = v ∧ R r
and that's correct! But if any of the assumptions above don't hold, we'll have
to alpha-convert if we want to make it this far. I couldn't figure the whole
story out, but here are three alpha-conversion examples, the first when r is
bound in (f x, R x).
needs RichterHilbertAxiomGeometry/readable.ml;; (* extensively commented *)
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.
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.
Here's an example where ¬(v = x), v is free in (f x, R x), and r is not free in
(λx. (f x, R x)).
interactive_goal `;
f = (λx. v + x) ⇒ {f x | R x} = HOL4_GSPEC (\x. (f x, R x))
`;;
interactive_proof `;
intro_TAC fDef;
rewrite fDef HOL4_GSPEC PAIR_EQ ;
`;;
`{v + x | R x} = (\v'. ?r. v + r = v' /\ R r)`
I finally got what I wanted, and HOL Light-type alpha-conversion. Let's make
it look even nicer:
interactive_proof `;
∀y. v + y = f y [fApplied] by fol fDef;
rewrite fApplied;
`;;
`{f x | R x} = (\v'. ?r. f r = v' /\ R r)`
Let me address my lack of skill/patience. Alpha-conversion will be needed iff
¬(v = x) and v is free in (f x, R x)
\/
¬(r = x) and r is free in (f x, R x)
\/
r is bound in (f x, R x).
I guess that's only 4 cases, as the 2nd and 3rd disjuncts are disjoint, and my
3 examples touched on all 4. I should try to work this exercise. I suppose
after all this I should re-prove your theorem:
let thm1 = theorem `;
{f x | R x} = HOL4_GSPEC (\x. (f x, R x))
proof
rewrite HOL4_GSPEC PAIR_EQ EXTENSION IN_ELIM_THM;
fol;
qed;
`;;
val thm1 : thm = |- {f x | R x} = HOL4_GSPEC (\x. f x,R x)
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. Here's two proof:
HOL4_GSPEC (λ(x, y, z). (f x y z, R x y z))
=
(λv. ∃r. (λ(x, y, z). (f x y z, R x y z)) r = (v, T))
=
Now r must be a triple r = (a, b, c), and then
=
(λv. ∃a b c. v = f a b c ∧ R a b c)
=
{f x y z | R x y z}
let thm3 = theorem `;
{f x y z | R x y z} = HOL4_GSPEC (λ(x, y, z). (f x y z, R x y z))
proof
rewrite HOL4_GSPEC PAIR_EQ IN_ELIM_THM EXISTS_PAIR_THM EXTENSION
Re: [Hol-info] More on set comprehensions
Rob,
On 29 Dec 2013, at 21:26, Rob Arthan r...@lemma-one.com wrote:
The code for HOL4 set abstractions says that the bound variables
of a set abstraction {t | p} are the intersection of the free variables
of t and p unless either side has no free vars, in which case the
bound variables are those of the other side. Also, if t has no free vars,
then fail.
Thanks - I couldn't find my way round the HOL4 parser code. However,
the last bit seems to be a bit more subtle: HOL4 doesn't fail the following
example where t has no free vars:
``{0 | a = b}``;
HOL message: inventing new type variable names: 'a
val it = ``{0 | a = b}``: term
The relevant bit of HOL4 code is “make_set_abs”, which can be found in
src/parse/Parse_support.sml (line 470).
The failure case comes into play when:
* Neither “t” nor “p” have free variables
e.g. {0 | T} fails.
* Both “t” and “p” have free variables and at least one of them intersects
e.g. {x /\ y | x /\ z} is fine but {x /\ y | w /\ z} fails.
Everything else seems to be accepted.
With regard to the {t | d | p} syntax, everything seems to be accepted,
provided that “d” is a comma separated list of variable names. For example,
{0 | a, b, c | T}
is accepted — it’s the term
GSPEC (\(a, b, c). (0, T))
Anthony--
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=84349831iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] More on set comprehensions
Hi Rob,
The code for HOL4 set abstractions says that the bound variables
of a set abstraction {t | p} are the intersection of the free variables
of t and p unless either side has no free vars, in which case the
bound variables are those of the other side. Also, if t has no free vars,
then fail.
Konrad.
On Sun, Dec 29, 2013 at 10:27 AM, Rob Arthan r...@lemma-one.com wrote:
Here are a few observations about the set comprehension syntax in HOL
Light and
HOL4.
The HOL4 Description manual says that {t | p} parses to: GSPEC(\(x1,. .
.,xn).(t,p)) where x1, . . . , xn are those free variables that occur in
both t
and p. It also says that it is an error if there are no such variables.
However, both HOL4 and HOL Light accepts {x + y | 0 = 1} and interpret it
as a
term with no free variables (GSPEC(\(x,y). (x + y,0 = 1) in HOL4 and
GSPEC(\GEN%PVAR%235. ?x y. SETSPEC GEN%PVAR%235 (0 = 1) (x + y)) in HOL
Light).
Is this intended? If so, what is the actual rule?
HOL4 and HOL Light disagree about the case where the term between { and |
has no
free variables. HOL Light allows both {0 | a = b} and {0 | 0 = 1}, while
HOL4
accepts the former but reports an error on the latter (no free
variables).
HOL4 and HOL Light also disagree about {x + y | z = z}. HOL4 reports no
free
variables, while HOL Light allows it, as in:
# REWRITE_CONV[] `{x + y | z = z}`;;
Warning: inventing type variables
val it : thm = |- {x + y | z = z} = {x + y | | T}
I can't find a description of the extended syntax {t | d | p} that lets you
provide a declaration d for the bound variables. However, HOL4 and HOL
Light
disagree about this: HOL4 requires d to be a single variable or variable
structure, while HOL Light allows a list of such things (possibly empty as
on
the RHS of the equation above). So HOL Light allows {x + y | x y | z = z}
but
HOL4 doesn't (but both allow {x + y | x, y | z = z}).
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=84349831iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
--
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=84349831iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
