Re: [isabelle] Uses of type quantification



FWIW, I implemented type quantification for HOL90 about 10 years ago. It never made it into public release. Tom Melham still has the code, if you're interested. Michael Norrish and I occasionally think about adding this back into the
"experimental kernel" that he's developed for HOL-4.

Also, there was a recent thread about this sort of thing on the hol-info list
in April of this year,

http://sourceforge.net/mailarchive/forum.php? forum_id=34662&max_rows=25&style=ultimate&viewmonth=200504

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

sparked by my student's realization that a natural definition of the regular sets can't be made without type quantification. Recall that the regular sets are those
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
type of string elements (treating strings as 'a lists, say). Being able to type quantify the state type on the rhs of the definition would help although,
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 quantification to be useful enough to add it to HOL light! I'll see if I can dig up the 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 HOL Light, although I wouldn't expect to finish anytime soon. As you can probably imagine, things like alpha conversion are slightly more complicated.

I would guess it would be quite a lot of work to add to Isabelle, but perhaps 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 on the HOL list, and this is probably the best place to look. Various people (e.g. Harrison, in - I think -

@INPROCEEDINGS{harrison-model,
        crossref        = "hol98",
        author          = "John Harrison",
title = "Formalizing Basic First Order Model Theory",
        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 them by related assumptions. FOL is a closed system. HOL is open, because I can assert an axiom "forall x:'a. I x = x", and via type instantiation, I can get "forall x:'b. I x = x" for any 'b. The corresponding assumption is "forall 'a. forall x:'a. I x = x", but of course, this can't be expressed currently. The reason I want to do this is another story.

I would also imagine that it is possible to do without type quantification in many areas, and this may be the case with your example. For example, you could just assert the axiom

bind $ (unit $ (x::'a)) $ f = f $ x

but then you would not get the safety of the axclass mechanism, and would have to manually track definitions of unit and bind to make sure they satisfied this axiom.

Cheers

Tom

John Matthews wrote:
Hello,
Brian Huffman, Peter White, and I are interested in having a limited form of type quantification added to Isabelle/HOLCF. It turns out that many of Haskell's constructor classes (most notably functors and monads) are associated with axioms that require quantifying over type variables. For example, one of the axioms of the monad class is the Left unit law. It states that for any monad instance 'm, containing methods for unit and bind with the following polymorphic signatures:
  unit :: "'a -> 'a $ 'm"
  bind :: "'a $ 'm -> ('a -> 'b $ 'm) -> 'b $ 'm",
(the infix ($) operator is a binary type constructor that we use to simulate 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 new type. Tom Melham worked out a consistent extension to higher order logic 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 the axclass package allowed multi-parameter type classes, the axioms become much more cumbersome to state and use without type quantification. We are wondering what other applications people have where this type-quantification operator would be useful, either in Isabelle or other implementations of classical higher order logic?
Thanks,
-john
[1]: T. F. Melham, "The HOL Logic Extended with Quantification over Type Variables", Formal Methods in System Design, vol. 3, nos. 1-2 (August 1993), pp. 7-24.








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.