*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] Uses of type quantification*From*: Konrad Slind <slind at cs.utah.edu>*Date*: Wed, 7 Sep 2005 21:30:21 -0600*Cc*: isabelle-users at cl.cam.ac.uk, Tom Ridge <Thomas.Ridge at cl.cam.ac.uk>*In-reply-to*: <212ac0c8aba52d8fc321d0cb8c935d85@galois.com>*References*: <817439747567edb58bbd67d41ed34f6c@galois.com> <431EACCC.4080702@cl.cam.ac.uk> <212ac0c8aba52d8fc321d0cb8c935d85@galois.com>

"experimental kernel" that he's developed for HOL-4.

in April of this year,

(above path needs to have the carriage-return removed)

that are recognized by a DFA. So Regular (L) <=> ?M. DFA(M) /\ !w. w \in L <=> M accepts w On the lhs, the type of Regular is ('a -> bool) -> bool. But a general definition of DFA would be polymorphic in the state type and the

as pointed out in the ensuing discussion, it isn't actually crucial. Konrad. On Sep 7, 2005, at 6:26 PM, John Matthews wrote:

Hi Tom,Thanks for the pointers. I'm glad to hear you find type quantificationto be useful enough to add it to HOL light! I'll see if I can dig upthe type quantification thread on info-hol.-john On Sep 7, 2005, at 2:03 AM, Tom Ridge wrote:Hello John,I am currently in the process of adding type quantification to HOLLight, although I wouldn't expect to finish anytime soon. As you canprobably imagine, things like alpha conversion are slightly morecomplicated.I would guess it would be quite a lot of work to add to Isabelle, butperhaps others can provide more information.There are lots of uses for type quantification. I have one example at http://homepages.inf.ed.ac.uk/s0128214/doc/typeQuantification.pdf but I don't think it is a particularly good one.There was some discussion by Rob Arthan and others on this topic onthe HOL list, and this is probably the best place to look. Variouspeople (e.g. Harrison, in - I think -@INPROCEEDINGS{harrison-model, crossref = "hol98", author = "John Harrison",title = "Formalizing Basic First Order ModelTheory",pages = "153--170"} @PROCEEDINGS{hol98, editor = "Jim Grundy and Malcolm Newey", booktitle = "Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs'98", series = "Lecture Notes in Computer Science", volume = 1497, address = "Canberra, Australia", date = "September/October 1998", year = 1998, publisher = "Springer-Verlag"} ) mention it in various contexts.My own reasons for adding it are so that HOL becomes a closed system,in the sense that one can remove instances of axioms and replace themby related assumptions. FOL is a closed system. HOL is open, becauseI can assert an axiom "forall x:'a. I x = x", and via typeinstantiation, I can get "forall x:'b. I x = x" for any 'b. Thecorresponding assumption is "forall 'a. forall x:'a. I x = x", but ofcourse, this can't be expressed currently. The reason I want to dothis is another story.I would also imagine that it is possible to do without typequantification in many areas, and this may be the case with yourexample. For example, you could just assert the axiombind $ (unit $ (x::'a)) $ f = f $ xbut then you would not get the safety of the axclass mechanism, andwould have to manually track definitions of unit and bind to makesure they satisfied this axiom.Cheers Tom John Matthews wrote:Hello,Brian Huffman, Peter White, and I are interested in having a limitedform of type quantification added to Isabelle/HOLCF. It turns outthat many of Haskell's constructor classes (most notably functorsand monads) are associated with axioms that require quantifying overtype variables. For example, one of the axioms of the monad class isthe Left unit law. It states that for any monad instance 'm,containing methods for unit and bind with the following polymorphicsignatures:unit :: "'a -> 'a $ 'm" bind :: "'a $ 'm -> ('a -> 'b $ 'm) -> 'b $ 'm",(the infix ($) operator is a binary type constructor that we use tosimulate constructor classes in Isabelle/HOLCF). Then the following"left unit" axiom holds for the monad instance:"ALL_TY 'a. bind $ (unit $ (x::'a)) $ f = f $ x".Note that the outermost "ALL_TY" operator is quantifying over types,not terms. However, the result is still a Boolean term, not a newtype. Tom Melham worked out a consistent extension to higher orderlogic that incorporates this operator [1]. Without this quantifier,then the axiom for the monad class would have two type variables,which is disallowed by Isabelle's axclass mechanism. Even if theaxclass package allowed multi-parameter type classes, the axiomsbecome much more cumbersome to state and use without typequantification.We are wondering what other applications people have where thistype-quantification operator would be useful, either in Isabelle orother implementations of classical higher order logic?Thanks, -john[1]: T. F. Melham, "The HOL Logic Extended with Quantification overType Variables",Formal Methods in System Design, vol. 3, nos. 1-2 (August1993), pp. 7-24.

**References**:**[isabelle] Uses of type quantification***From:*John Matthews

**Re: [isabelle] Uses of type quantification***From:*Tom Ridge

**Re: [isabelle] Uses of type quantification***From:*John Matthews

- Previous by Date: Re: [isabelle] Uses of type quantification
- Next by Date: [isabelle] Some question about Auth library
- Previous by Thread: Re: [isabelle] Uses of type quantification
- Next by Thread: Re: [isabelle] Uses of type quantification
- Cl-isabelle-users September 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list