On Fri, Jan 18, 2013 at 1:51 PM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> That's fine, Ramana, you're explanation was probably as good as mine:
>
> I think I was just trying to explain why you can't define
> [Fibration p E B] (without type quantification).
>
> BR> Any time you wish to write Fibration p E B, you must write instead
> BR> !M:A->bool. HLP p E B M.
>
> Though you'll have to be careful when writing that if the type
> variable A is already in your context.
>
> Good point. However, I think Milner type inference means we don't need
> the A at all, that we can just write
> !M. HLP p E B M
> The definition of HLP will require M to be not only a set (i.e. of type
> A->bool, for some type A) but a topological space, however that's define.
>
Just because you don't write the A doesn't mean it isn't there. And if
you'll still need to be careful if there's an A in context, whether you
write it explicitly or not, although hopefully type inference will pick
another type variable for you if there's already an A around (e.g. B).
>
> Anyway, I think !M. HLP p E B M is an acceptable annoyance at this point,
> when we've formalized so little of algebraic topology. Later maybe the HOL
> maintainers will think we've done such great work they will want to add in
> type quantification.
You seem to have missed the point that HOL Omega already has type
quantification. If you want type quantification, you should definitely be
using it.
> And maybe it will turn out that there are more serious problems to
> formalizing AT... I'm interested in Rob's challenge about free groups. I
> don't know how to define a free group in HOL, and mostly because I don't
> think it's an easy matter mathematically. Take a finite set
> S = {x1,...,xn}
> The free group on S consists of all possible expressions like
> x3^6 * x1^{-1} * x4.
> We just multiply these expression by concatenating them, but there may be
> cancellations, and we perform recursively as many of them as we can:
>
> x3^6 * x4 TIMES x5^{-1} * x1^{-1} = x3^6 *x4 * x5^{-1} * x1^{-1}
>
> x3^6 * x1^{-1} * x4 TIMES x4^{-2} * x3 = x3^6 * x1^{-1} * x4^{-1} * x3
>
> To me, that's hard HOL to define the free group, but I'm guessing someone
> has already coded this up.
>
> --
> Best,
> Bill
>
------------------------------------------------------------------------------
Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and
much more. Get web development skills now with LearnDevNow -
350+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122812
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
