Subject: More on set comprehensions Newsgroups: gmane.comp.mathematics.hol Date: Sunday 29th December 2013 15:27:04 UTC (over 3 years ago) 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. |
|||