Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Rob Arthan <rda <at> lemma-one.com>
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.
 
CD: 3ms