> I just want to point out that the goalposts have shifted > slightly. The material pointed to by Michael shows that a fair > bit of basic abstract algebra can be cleanly done in HOL's type > theory, which I gather was the original point in question. > > re: Ken's questions. > > 1. The carrier is expressed as a predicate on a polymorphic type, > so it is indeed a term. Moreover, the UNIV operator can be > used to get the set of elements of a type. So I am not really > seeing this as an impediment, at least for the simple examples > being discussed. > > 2. Yes, there is no quantification of type variables in the HOL > logic. This has been discussed at length in earlier postings > on this list. Extensions of HOL with type quantification have > been proposed by Melham and, later, by Homeier. These have > been implemented and applied to interesting examples, but > HOL4 hasn't moved to type quantification yet. > > Konrad. >
(Deleted previous messages in thread because MailMan complains)
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
