I'd like to announce a major upgrade to the HOL-Omega logic and system. The major change is deep but important: whereas ranks were previously an attribute of types, they are now made an attribute of kinds, specifically of both the base kind and kind variables. This enables the kind of a type operator to have a specific rank for the kind of its domain. This rank can then be used to judge the appropriateness of a given type argument, to see if it is of the expected rank or lower.
This is a new restraint on the application of type operators to type arguments, and has required a considerable expansion and reworking of the whole type/kind/rank inference system, as well as other portions of the code. The benefit is that the rank of type expressions may be now much more accurately estimated than before, and that applications of type operators to arguments which do not respect rank are now detected immediately and rejected. In the previous system, such applications were allowed, but had no useful meaning according to the official semantics, and in practical terms, could not be beta-reduced. The HOL-Omega system is still almost perfectly backwards compatible with HOL4, so whatever builds on HOL4 should also build on HOL-Omega, with very few exceptions. The new version of HOL-Omega is available on SourceForge; it is revision 8987. This corresponds to HOL4 Kananaskis-7, revision 8608 from September 2010. I will be working gradually over the next few weeks to bring HOL-Omega up to date with the current revision of Kananaskis-7. To obtain a copy, give the Subversion command svn checkout https://hol.svn.sf.net/svnroot/hol/branches/HOL-Omega Peter -- "In Your majesty ride prosperously because of truth, humility, and righteousness; and Your right hand shall teach You awesome things." (Psalm 45:4) ------------------------------------------------------------------------------ Xperia(TM) PLAY It's a major breakthrough. An authentic gaming smartphone on the nation's most reliable network. And it wants your games. http://p.sf.net/sfu/verizon-sfdev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
