Trustworthy Tools
Higher Order Quotients
Home | About Us | Projects | HOL-Omega | Publications | Dissertation | Divine Support

Higher Order Quotients
in Higher Order Logic

Abstract

theknave1.jpg

The quotient operation is a standard feature of set theory, where a set is partitioned into subsets by an equivalence relation. We reinterpret this idea for higher order logic, where types are divided by an equivalence relation to create new types, called quotient types. We present a design and an implementation to mechanically construct quotient types as new types in the logic, and to support the automatic lifting of constants and theorems about the original types to corresponding constants and theorems about the quotient types. This design exceeds the functionality of Harrison's package, creating quotients of multiple mutually recursive types simultaneously, and supporting the equivalence of aggregate types, such as lists and pairs. Most importantly, this design supports the creation of higher order quotients, which enable the automatic lifting of theorems with quantification over functions of any higher order.

This page gives information about an implementation of higher order quotients for the Higher Order Logic theorem prover.

It provides postscript and PDF versions of the papers. It also provides the full source code for the Higher Order Logic theorem prover to perform all proofs described in the papers. In addition, this page describes packages of supporting software, which supply needed tools to support the automated proof in the Higher Order Logic theorem prover.

Talks

Papers

hline.gif

Software

Higher order quotients have been added as a standard library to the HOL4 Higher Order Logic theorem prover as of version Kananaskis-3 and above. The files may be found in <HOL-dir>/src/quotient.

The following packages are source code for the Higher Order Logic theorem prover, HOL4 version Kananaskis-2.

Higher Order Quotients package

Here is the Higher Order Quotient package for HOL. This makes use of the dependent rewriting package described below. Please note that these packages are now a standard part of the HOL4 system, versions Kananaskis-3 and above.

This is version 2.3 of this package, as of August 12, 2005.
quotient23.tar.gz. (Compressed tar archive, 61,171 bytes)

Relationship between the Axiom of Choice and Higher Order Quotients

This is a development of an alternative design for higher order quotients which avoids use of the Axiom of Choice, as presented in section 6 of the paper, A Design Structure for Higher Order Quotients.

This is version 1.0 of this proof, as of February 17, 2005.
axiomofchoice.tar.gz. (Compressed tar archive, 15,807 bytes)

Examples

The following examples of higher order quotients are presented in order from simplest to the most complex. They are present in the HOL4 system, versions Kananaskis-4 and above, in the directory <HOL-root>/src/quotient/examples.

Message Encryption and Decryption

This is a recreation using higher order quotients of an example of message encryption and decryption studied by Larry Paulson in his paper, "Defining Functions on Equivalence Classes," to be published in ACM Transactions on Computational Logic, in press as of August 2005, but available at Larry Paulson's website, at http://www.cl.cam.ac.uk/users/lcp/papers/Reports/equivclasses.pdf. This paper is exceptionally well written, and a pleasure to read.

msgScript.sml. (SML source code for HOL, 14,642 bytes)

Finite Sets

This creates finite sets as a new type in HOL4 as a quotient of lists, as described in the TPHOLs 2005 paper, "A Design Structure for Higher Order Quotients," available in the TPHOLs 2005 conference proceedings published by Springer-Verlag, LNCS 3603.

finite_setScript.sml. (SML source code for HOL, 24,267 bytes)

Alternative Development of Finite Sets

This contains another approach to using higher order quotients to form finite sets as a new type as a quotient of lists, composed by Michael Norrish. The equivalence relation is defined simply as extensionality. The reader is invited to compare this development with the first approach above.

ext_finite_setScript.sml. (SML source code for HOL, 11,985 bytes)

Proof of the Church-Rosser Theorem for the Lambda Calculus

As an example exercising the quotients package, here is a proof of the Church-Rosser theorem for the lambda calculus. This makes use of the higher order quotients package described above to lift the lambda calculus from a free algebra to a quotient version which identifies alpha-equivalent terms.

This proof was described in a Track B paper at TPHOLs'01 in Edinburgh, UK,and published in Richard J. Boulton and Paul B. Jackson, editors, TPHOLs 2001: Supplemental Proceedings, pages 207-222, Division of Informatics, University of Edinburgh, September 2001, available as Informatics Research Report EDI-INF-RR-0046. This paper is available here as postscript and PDF. The paper refers to a outdated version of the quotient library, but shows its usefulness.

This is version 2.3 of this proof, as of April 27, 2007.
lambda23.tar.gz. (Compressed tar archive, 87,209 bytes)

The source code for this proof includes some of the software packages mentioned at the bottom of this page.

Proof of the Church-Rosser Theorem for the Sigma Calculus

As an example exercising the quotients package, here is a proof of the Church-Rosser theorem for the sigma calculus. This is a nested mutually recursive object calculus, invented by Abadi and Cardelli in their book, "A Theory of Objects." This example makes use of the higher order quotients package described above to lift the sigma calculus from a free algebra to a quotient version which identifies alpha-equivalent terms.

There is no paper yet describing this proof. In that absence, the best guide to understanding it is the paper for the lambda calculus proof above, as the two have the same structure and use the same ideas, except that the sigma calculus proof uses mutual recursion in many forms.

This is version 2.1 of this proof, as of April 27, 2007.
sigma21.tar.gz. (Compressed tar archive, 91,966 bytes)

The source code for this proof includes some of the software packages mentioned below.

hline.gif

Additional Proof Tools

All of the tools below are superceded by the tools present as standard parts of HOL4 versions Kananaskis-4 and above.

Mutually Recursive Rule Induction

Myra Van Inwegen has written a package for defining relations by mutually recursive rule induction. This package automatically proves theorems for the new relations' rules, the inversions of the rules, and weak and strong rule induction principles. The package has been ported to HOL4, version Kananaskis-2. Myra's original version was for Hol90.
Code: ind_rel.sig and ind_rel.sml.

Mutually Recursive Structural Induction

Using HOL4 version Kananaskis-2, one can create mutually recursive types using the Hol_datatype function. In addition, one can define mutually recursive functions according to the recursive structure of the types. However, there is no automation provided in the standard HOL system to prove theorems about these functions by mutually recursive structural induction. This capability is now provided here as a tactic, MUTUAL_INDUCT_THEN.
Code: MutualIndThen.sig and MutualIndThen.sml.

Dependent Rewriting

Here is a package to do rewriting of goals by the conclusions of implications, even if the antecedents have not yet been proven. The author calls this "dependent rewriting." The instructions for use are in comments at the beginnings of the files.
Code: dep_rewrite.sig and dep_rewrite.sml.

Making formal methods into normal methods.