Rob,
On 29 Dec 2013, at 21:26, Rob Arthan <r...@lemma-one.com> wrote:
>> 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.
>
> Thanks - I couldn't find my way round the HOL4 parser code. However,
> the last bit seems to be a bit more subtle: HOL4 doesn't fail the following
> example where t has no free vars:
>
> > ``{0 | a = b}``;
> <<HOL message: inventing new type variable names: 'a>>
> val it = ``{0 | a = b}``: term
The relevant bit of HOL4 code is “make_set_abs”, which can be found in
src/parse/Parse_support.sml (line 470).
The failure case comes into play when:
* Neither “t” nor “p” have free variables
e.g. {0 | T} fails.
* Both “t” and “p” have free variables and at least one of them intersects
e.g. {x /\ y | x /\ z} is fine but {x /\ y | w /\ z} fails.
Everything else seems to be accepted.
With regard to the {t | d | p} syntax, everything seems to be accepted,
provided that “d” is a comma separated list of variable names. For example,
{0 | a, b, c | T}
is accepted — it’s the term
GSPEC (\(a, b, c). (0, T))
Anthony------------------------------------------------------------------------------
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
