Peter, I have a quick question about one part of your email:
Do you know whether you could add dependent types (the third sort of
abstraction, of a type by a term variable) while still retaining backwards
compatibility with ordinary HOL?
On Fri, Jan 25, 2013 at 4:48 PM, Peter Vincent Homeier <
[email protected]> wrote:
> 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
