Bill,
On 4 Jan 2014, at 05:17, Bill Richter wrote:
> 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.
Yes. My explanation of the phenomena you were observing was wrong.
>
> 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.
Who needs to understand these alpha-conversions? Variables get renamed as
necessary
to avoid capture when you do rewriting and it is hard to predict exactly what
will
get renamed to what. That's just the way things are. It is not specific to
GSPEC or
the representation of set comprehensions.
>
> 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.
I think we will just have to agree differ about this. Let me just make two
comments:
(1) Far too much mathematical notation is explained away as short-hands.
I.e., syntactic abbreviations. This is a consequence of the inexpressiveness of
first-order languages and the fact that mathematics is traditionally
asserted to be founded on first-order set theory. Higher-order
functions can express many of these short-hands directly as first-class objects
that you can
reason about. In the case in point, this corresponds to what I think is a nice
categorical
way of thinking of what's going on. In the category of sets and relations, let
me write
R: X <-> Y to mean R is a relation with domain X and codomain Y.
Then a relation R : X <-> BOOL, where BOOL is the 2-point set {T, F}
determines the subset R^{-1}({T}) of X. The set comprehension gives you the
obvious way
of combining a function f : Y -> X and a function P: Y -> BOOL to get a relation
S:X <-> BOOL and hence the subset S^{-1}({T}) of X, namely S = P o f^{-1}.
Notice there are no bound variables in this account - they are all hidden
in the definitions of relational image, inverse and composition.
Presumably, you would object to that.
(2) My original complaint was that something like `{x : num | p x}` = `{x : num
| p x}`
evaluates to false in HOL Light, because the parser makes a different choice
for the name
corresponding to the bound variable "a" above that you are so fond of. I
realise now
that even things like `x` = `x` evaluate to false because you get different
type variables.
I conclude that (doubtless for good reasons), the HOL Light parser just has
different
design goals from the ProofPower-HOL parser and, I believe, the HOL4 parsers
which
both make the same string of symbols parse to the same thing in any given
context.
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
