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
