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.
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
