Hi, Grant. That is a great question, and it has sparked my memory. In fact,
I'm going to copy this to the hol-info list since it is of general
interest, and because I made a mistake for which I must apologize.
First, I was wrong in saying that no one else had been doing this sort of
thing, stratifying types into ranks. I had completely forgotten some
extremely important theorem provers. Examples of some systems that include
this to at least some degree are Coq, ECC by Luo, and MetaPRL from Cornell.
Of course there may be others as well.
Coq is an interesting combination of both predicative and impredicative
types. Originally, based on the Calculus of Constructions, Coq had a type
structure where both Set and Prop were impredicative. However, Zhaohua Luo
improved that logic when he created his Extended Calculus of Constructions
(ECC), which had a base of impredicative types, but allowed for normal
datatype like lists to be formed on top of that base as predicative types
in a rank structure.
Sometime in the mid-2000's the Coq team considered this, and decided to
revise the core logic, making Set predicative and having all the Type(0),
Type(1), etc. hierarchy. But they decided to keep Prop impredicative, and
in fact I think the system as constructed uses this in some subtle ways in
the core. It's not quite as elegant as Luo's ECC, but it's close to the
same logic, and there was only modest disruption to the Coq community from
this change.
MetaPRL is an intuitionistic type theory theorem prover which is strictly
impredicative, just as HOL-Omega is. Bob Constable has described energetic
discussions that he had with the Coq people when they were forming their
theorem prover, advocating for strictly predicative types, but the Coq team
decided they wanted to include impredicativity. By the way, the MetaPRL
team uses an intuitionistic logic on philosophical grounds, and would not
want to use a classical logic even if Girard's Paradox did not prevent it.
So if you have impredicativity at all within your logic, in light of the
dangers posed by Girard's Paradox, you must pay for the impredicativity in
some way, usually by restricting the power of the logic to be
intuitionistic. The impredicative type calculus does look very simple and
elegant, and this can catch your heart if you are not careful. However,
that apparent lovely simplicity hides a world of complex trouble
underneath, typically by allowing the existence of things that are build
out of themselves, circularly. Proofs regarding such logics cannot be done
by the normal means of structural induction, but must use sophisticated
techniques such as induction by logical relations, as I heard Bob Harper
describe a couple of summers ago.
https://sites.google.com/site/oplss10/robert-harper
So this can be done, and it is perfectly sound and respectable, but it is a
lot of work.
But for the predicative portions of the logic, other issues arise. Similar
to the strong typing introduced in Pascal in 1970, the ranks give needed
structure but can get in your way. Just as successor languages after Pascal
found ways to wisely weaken the strong typing, practicality demands some
additional flexibility in the rank system. A feature that I found necessary
from a practical perspective is *universe polymorphism*, which says that
any type constant, term constant, or theorem has rank instances of itself,
both at its current rank and at every higher rank. In each case, the
instance is the same as the original except that all ranks everywhere in
the construct are lifted the same number of levels, simultaneously.
Intuitively, this is saying that any mathematical development that we could
do at one rank, with definitions and theorems, etc., we could have done
just as well one level up. All the resulting theorems would also be true
and would look almost the same except that their ranks were lifted by one,
uniformly. I have found that this is an absolutely necessary feature to
keep the logic as a usable tool.
Coq I believe does not have universe polymorphism, and this has caused some
problems in practical use. such as wanting to have lists of elements which
each have rank 1. But the normal list *nil* and *cons* in Coq are of rank
0, and all of the existing Coq theorems about lists are theorems at rank 0.
So they can't be used to create or reason about such lists. You'd have to
make a copy of the list theory file, edit it throughout to make the ranks
one higher, renaming the type, say, list1, and then compile it before you
could use this in your work. And then you'd have to worry about not
confusing the LENGTH operator for rank 1 with the one for rank 0, etc.
I have not studied MetaPRL much at all, but I understand it has an even
more complex rank system than HOL-Omega. In MetaPRL there are an unlimited
number of separate rank variables. In HOL-Omega, following a suggestion by
John Matthews, there is only one rank variable, in the interests of keeping
the semantics of HOL-Omega a simple as possible (not to mention the rank
inference algorithms!). I have found that this simpler system has been
sufficient for all the interesting problems I have tried so far.
I hope this clarifies the relationships between the logics of HOL-Omega and
Coq, ECC, and MetaPRL. I really do not claim to be an expert about any of
the other systems, so it's possible I have some errors in what I wrote
above. If so, please correct me.
Peter
On Fri, Jan 25, 2013 at 6:06 PM, Grant Olney Passmore <
grant.passm...@cl.cam.ac.uk> wrote:
> Hi, Peter --
>
> 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.
>
>
> How is this related to the type hierarchy in Coq? See, e.g.,
> http://adam.chlipala.net/cpdt/html/Universes.html . I'd be curious to
> know the differences.
>
> Best wishes,
> Grant
>
> On 25 Jan 2013, at 16:48, Peter Vincent Homeier 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 <john.harri...@cl.cam.ac.uk
> > 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
>> hol-info@lists.sourceforge.net
>> 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
> hol-info@lists.sourceforge.net
> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
