Ah yes, point taken.
on 8/1/14 10:13 AM, Rob Arthan <r...@lemma-one.com> wrote:
> 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=84349831&iu=/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=84349831&iu=/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=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
