On 16/05/11 16:10, Roger Bishop Jones wrote: > On Sunday 15 May 2011 15:08, Mark wrote: >> In fact HOL Zero is the only HOL system with a pretty >> printer specially designed to avoid all possible >> confusing results like that. For this situation, it >> returns Rob's "ideal output": >> >> # beta_conv `(\x. ?y. x = a /\ y = b) y`;; >> val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> >> (?(y:'2). (y:'1) = a /\ (y:'2) = b) > > Surely the ideal would be to avoid having ambiguous names by > renaming as necessary? > (though I agree that sufficient type information for > disambiguation is also desirable)
HOL4 does the renaming I demonstrated earlier when substitutions are performed
(there was a beta-conv). You could also imagine renaming when dest_abs was
used. Because HOL4 with the experimental kernel (which uses name-carrying
terms) doesn't do the latter, you get the following:
> val xa = mk_var("x",alpha);
- val xa = ``x`` : term
> val xb = mk_var("x", beta);
- val xb = ``x`` : term
> val Pa = mk_var("P", alpha --> bool);
- val Pa = ``P`` : term
> val Qb = mk_var("Q", beta --> bool);
- val Qb = ``Q`` : term
> mk_abs(xa, mk_conj(mk_comb(Pa,xa), mk_comb(Qb,xb)));
- val it = ``λx. P x ∧ Q x``: term
[The HOL4 colouring of free-versus-bound variables saves this particular
example, but of course, xb might be bound at a higher point in the term,
forcing the user to inspect types by doing mouse-overs.]
There are trade-offs: the prospect of the experimental kernel dest_abs being
non-constant time is pretty unappealing. But in the de Bruijn ("locally
nameless") kernel, you are already traversing the body when you do a dest_abs,
and so that kernel does rename in the above situation, making the printing
behaviours of the two kernels different. (I hope I haven't given Mark a heart
attack. :-)
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
