Konrad,
On 29 Dec 2013, at 17:31, Konrad Slind wrote:
> Hi Rob,
>
> The code for HOL4 set abstractions says that the bound variables
> of a set abstraction {t | p} are the intersection of the free variables
> of t and p unless either side has no free vars, in which case the
> bound variables are those of the other side. Also, if t has no free vars,
> then fail.
Thanks - I couldn't find my way round the HOL4 parser code. However,
the last bit seems to be a bit more subtle: HOL4 doesn't fail the following
example where t has no free vars:
> ``{0 | a = b}``;
<<HOL message: inventing new type variable names: 'a>>
val it = ``{0 | a = b}``: term
I did find the relevant bit in the HOL Light code:
let evs =
let fvs = pfrees fabs []
and bvs = pfrees babs [] in
if length fvs <= 1 or bvs = [] then fvs
else intersect fvs bvs
where if the input is {t | p}, fabs is t and babs is p. So HOL Light has a
special
case when t has just 1 free variable:
# frees `{x + y + 1 | z > 0}`;;
val it : term list = [`z`; `x`; `y`]
# frees `{x + 1 | z > 0}`;;
val it : term list = [`z`]
I wonder why? HOL4 rejects both of the above.
Regards,
Rob.
>
> Konrad.
>
>
>
> On Sun, Dec 29, 2013 at 10:27 AM, Rob Arthan <r...@lemma-one.com> wrote:
> Here are a few observations about the set comprehension syntax in HOL Light
> and
> HOL4.
>
> The HOL4 Description manual says that {t | p} parses to: GSPEC(\(x1,. .
> .,xn).(t,p)) where x1, . . . , xn are those free variables that occur in both
> t
> and p. It also says that it is an error if there are no such variables.
> However, both HOL4 and HOL Light accepts {x + y | 0 = 1} and interpret it as a
> term with no free variables (GSPEC(\(x,y). (x + y,0 = 1) in HOL4 and
> GSPEC(\GEN%PVAR%235. ?x y. SETSPEC GEN%PVAR%235 (0 = 1) (x + y)) in HOL
> Light).
> Is this intended? If so, what is the actual rule?
>
> HOL4 and HOL Light disagree about the case where the term between { and | has
> no
> free variables. HOL Light allows both {0 | a = b} and {0 | 0 = 1}, while HOL4
> accepts the former but reports an error on the latter ("no free variables").
>
> HOL4 and HOL Light also disagree about {x + y | z = z}. HOL4 reports "no free
> variables", while HOL Light allows it, as in:
>
> # REWRITE_CONV[] `{x + y | z = z}`;;
> Warning: inventing type variables
> val it : thm = |- {x + y | z = z} = {x + y | | T}
>
> I can't find a description of the extended syntax {t | d | p} that lets you
> provide a declaration d for the bound variables. However, HOL4 and HOL Light
> disagree about this: HOL4 requires d to be a single variable or variable
> structure, while HOL Light allows a list of such things (possibly empty as on
> the RHS of the equation above). So HOL Light allows {x + y | x y | z = z} but
> HOL4 doesn't (but both allow {x + y | x, y | z = z}).
>
> 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
