Hi, Ramana.
I hate to speculate about experiments that have not been performed yet, but
my plan would be yes, to retain full backwards compatibility with HOL4, as
has been done so far with HOL-Omega. This does force certain design
choices, but I think it would still all work out all right.
For one thing, instead of having one fundamental ML type to represent both
Object Logic terms and types, I would retain the ML types term and hol_type,
and in the kernel write mutually recursive routines to work down through
both types and terms simultaneously. This would require a few coding tricks
but I think it would be fine.
Of course, you could simplify the logic by having certain restrictions
like, perhaps, no free term variables in a type? But I'm not sure whether
that would be needed or not. That's the sort of question that would be
answered by experimentation.
So yes, Ramana, backwards compatibility has always been a high priority for
me, and it has been almost completely achieved so far. I would not want to
give that up, since the value here is not just the new features of
HOL-Omega, but the joining of that power with the considerable wealth and
investment existing in the HOL4 libraries and examples. It would be madness
to throw that away. The backwards compatibility of HOL-Omega with HOL4 is
discussed more in the upcoming HOL-Omega TUTORIAL.
Peter
On Fri, Jan 25, 2013 at 11:55 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>wrote:
> 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 <
> palan...@trustworthytools.com> 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)
>>
>
>
--
"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
