Thanks for mentioning HOL-Omega, Ramana and John.
For those who don't know, HOL-Omega extends the existing higher order logic
implemented in HOL4, HOL-Light, HOL-Zero, etc., with two new kinds of
abstraction:
1) abstraction of a type by a type variable, and
2) abstraction of a term by a type variable.
The first sort of abstraction gives you type operator variables and a
version of the lambda calculus completely within the type language. The
second sort of abstraction gives you type quantification over terms, as in
System F, and gives one a more precise and general form of polymorphism
than in classical higher order logic.
This is essentially the system Fω, as described in Benjamin PIerce's
book *Types
and Programming Languages*, but with one huge change. In Fω, when you
create a universal type by quantifying over all types, the range of that
quantification includes the very type that you are constructing. This is
circular, and this style of definition is called "impredicativity."
It turns out that if you naively try to combine these language features as
I have described, it doesn't work. The logic you get is inconsistent. This
was proven by Girard and is known as Girard's Paradox.
Coq and other similar systems avoid this inconsistency by restricting the
power of the logic to intuitionistic logic, not full classical higher order
logic. It turns out that this is enough to subdue the logic's power to be
consistent, in that one cannot prove false.
However, there is another possible design choice, which has not been
previously explored to my knowledge (any info to the contrary would be
appreciated!). That is the avoidance of impredicativity by classifying all
types into collections ordered by ranks, numbered 0, 1, 2, etc. Then when
one forms a universal type by quantifying over types, the quantification
takes place over all types of one rank, but the type being formed is of at
least the next higher rank. Thus the construction is not circular.
With this design choice, I have constructed a version of higher order logic
that does contain the two new forms of abstraction mentioned above, while
still retaining all of the power and expressivity of classical higher order
logic, with a semantics that is considerably simpler than that of Coq.
HOL-Omega's semantics, as presented in this new upcoming paper, fits well
within normal set theory, that is, Zermelo-Fraenkel set theory with choice.
I understand that Coq's semantics requires additional assumptions beyond
this, namely the existence of an infinite number of inaccessible cardinals.
Currently, HOL-Omega does not support dependent types as Coq does; this
would be a third fundamental sort of abstraction,
3) abstraction of a type by a term variable.
I do not see any fundamental difficulties with adding dependent types to
HOL-Omega, and could probably do it if I get the opportunity. It should
actually be easier than the abstraction of terms by type variables. But I
don't want to speculate on what could be, but rather present to you what is
actually working today, and that is HOL-Omega.
If people are interested in learning more, there are some new developments
soon appearing.
First, I have submitted a new paper to the ITP 2013 conference, that
substantially revises and improves the 2009 TPHOLs paper:
The HOL-Omega Logic
(PDF)<http://www.trustworthytools.com/holw/holw-lncs5674.pdf>
It explains how the logic has changed since 2009, most importantly by
making ranks attributes of kinds, rather than of types. I'm happy to share
a preprint with anyone interested, but I should warn you that it is dense,
highly compressed to fit within 16 pages. The 2009 paper above is still
useful to read first, as it provides motivation and several cool examples,
all of which still run unchanged in the newest version of HOL-Omega.
A more readable document is the HOL-Omega TUTORIAL, which I am happy to
announce has been completed (as far as writing goes) and is now awaiting
approval for distribution. I expect that this will be available sometime
early this spring, say about April, but the timing is out of my hands.
In the meantime, there is a nice and juicy TUTORIAL TEASER on the website,
which gives one chapter from the upcoming tutorial, showing in a light and
easy way how the new features of the logic can be used to good effect.
Enjoy!
Peter
On Thu, Jan 24, 2013 at 8:48 PM, John Harrison
<[email protected]>wrote:
>
> Ramana wrote:
>
> | HOL-Omega has type quantification, and is backwards compatible with
> | HOL4. http://www.trustworthytools.com/id17.html.
>
> Norbert Voelker's HOL2P also offers type quantification, and is
> essentially upward compatible with HOL Light:
>
> http://cswww.essex.ac.uk/staff/norbert/hol2p/
>
> Indeed, as Peter Homeier has noted, HOL2P was a major inspiration for
> his own further extension of the type theory in HOL-Omega.
>
> John.
>
>
> ------------------------------------------------------------------------------
> Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
> MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
> with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
> MVPs and experts. ON SALE this month only -- learn more at:
> http://p.sf.net/sfu/learnnow-d2d
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnnow-d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
