Consider HOL Light style set comprehension

[mn200]

As described in http://article.gmane.org/gmane.comp.mathematics.hol/2118 the HOL Light approach to this has the advantage over our current set up of not depending on pairs, and not using paired-abstractions.

It iterates mk_exists instead of mk_pabs, and uses another auxiliary constant, SET_SPEC.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[mn200]

A comment from Rob Arthan on the hol-info mailing list points out that one disadvantage of the HOL Light approach is that you will get

`{ x | x > 6}` <> `{x | x > 6}`;;

because each parse will use a fresh genvar. This makes me rather less keen on the idea of switching to this implementation (though I still hate paired abstractions).

[mn200]

Of course, one shouldn't be use = on terms anyway. One would still have

aconv ``{x | x > 6}`` ``{x | x > 6}``

in a possible HOL4 implementation of this idea.

[mn200]

Another argument in favour of this idea is that it seems impossible to make a congruence rule for GSPEC as we have it, but the congruence rule for HOL Light's approach is trivial. A congruence rule is critical to get termination conditions for things like

wave G i = MAX_SET { wave g j + 1 | j ∈ iters G ⋀ j -<G>-> i }

a function I want to define right now.

[mn200]

As the gmane link has died, here is a brief description of the HOL Light approach. There's a GSPEC constant outermost that is a signal to the printer (like our NUMERAL constant), but is semantically the identity. Then, there’s SETSPEC with definition

SETSPEC v P t <=> P /\ v = t

This is used to translate a simple case like { x | x < 6} into

GSPEC (\gv. ?x. SETSPEC gv (x < 6) x)

The P is the boolean expression to the right of the |; the t is the term to its left; the v is the genvar (gv above) that Rob Arthan complained about. In a more complicated case like { x + y | x * y = 20}, you get

GSPEC (\gv. ?x y. SETSPEC gv (x * y = 20) (x + y))

If you use the double | syntax, that just controls which variables get existentially quantified. So { x + y * z | x,y | x * y - z = 20} turns into

GSPEC (\gv. ?x y. SETSPEC gv (x * y - z = 20) (x + y * z))

with z free, as desired.

[mn200]

The Sourceforge archive has some/all of this stored. This link seems to work at the moment (2024).