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