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.
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. 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
