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=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
