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 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.
--
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
