LEGO Algebra Group

Contents of this page

• Outline of the LAG project
• Coercions, classes and subtyping
• Theory and associated mechanisms
• The GALOIS project
• Other large-scale formalisation case-studies
• Literate formalisation

Outline of the LAG project

The LEGO Algebra Group, or LAG, is my provisional title to refer to the group of us that met in Utrecht at CSL96 this autumn; i.e. Peter Aczel, Henk Barendreght, Gilles Barthe and Zhaohui Luo. I would also like to include Anthony Bailey.

We share a common interest in the use of LEGO and perhaps similar systems such as Coq and Alf that implement dependent type theories. We are interested in the development of machine checked abstract mathematics, particularly algebra. A key issue for us is how informal abstract mathematics should be represented in a dependent type theory. Another key concern is to make efforts to close the gap between informal mathematics and our formalisations as much as possible.

The reason for our meeting at CSL96 was our desire to give the above shared interests a focus. Here were some plans that were considered.

1. Set up a web page with a bibliography and url's for reports MSc, PhD theses, etc that are available. (Anthony Bailey is willing to do this at Manchester)
2. Initiate e-mail discussion to set the limits of what we want to focus attention on. My description, above, of our common interests, is only meant to be a start.
3. Work towards the creation of an electronic book to advertise our subject and already available published and unpublished work. This would probably involve the need to write abbreviated versions of material unlikely to be published in the usual way and chapters to create a coherent presentation. This electronic book could just be made available via our web page. But if we feel it is worthwhile we could consider a more formal publication, perhaps as a real book.
4. Organise a workshop, say for the autumn of 97, possibly as part of the Types WG, possibly supported by the British MathFit.

I am sure that there are many things that we discussed not yet included here, but I hope that this is a start in getting formulated our common aims and plans.

I suggest that, while Anthony sets up a web home page, we should send him what we each consider directly relevent references and url's. Also please communicate any comments and additions, so that we can achieve a good starting statement of our aims. There is probably a lot more detail I could add, but I prefer to get us all moving first. Of course a good title/acronym might be useful (not LAG).

This page is currently a fairly scratchy index of some of the electronically available resources that might be relevant. If you have some to add, then please send them to me. HTML source for a list of links is the best possible format so that I can just paste it into this page, but any other format, including an URL to a list of your own, is a quite acceptable alternative.

The references I have so far fall into several sections.

Coercions, classes and sub-typing

LEGO with implicit coercions

Anthony Bailey has hacked at the LEGO source to allow the application of some declared coercions to be left implicit in the input and output of LEGO expressions in a manner analagous to the way in which synthesisable arguments to functions can be left implicit.

There are two implementations. LEGO with coercions, or legowc, is the first. Some of you may have already worked with it. The second is a re-implementation, LEGO with coercion synthesis, or legowcs. This is much improved, and is based on modifications to the forth-coming beta-version of LEGO, on which work is still in progress. In time, all the changes, including the coercion synthesis ones, will be released as an official Alpha; in the mean time if you are keen then try the version here.

• DVI copy of LEGO with implicit coercions (Bailey)
  This document has two purposes. Firstly, it acts as a tutorial explaining the new features of a variant of the proof-checker LEGO that the author has written to extend the syntax of the type theory to allow impicit coercion functions. Secondly, it tries to make a more general point in showing how a type theory whose syntax has been extended in this way can be used to write mathematics, in particular algebra, in a way that makes a formal presentation easier to read.
• LaTeXLEGO source for LEGO with implicit coercions.
• DVI copy of LEGO with coercion synthesis (Bailey).
  A user manual and tutorial for using legowcs.
• LaTeX source for LEGO with coercion synthesis.
• Compiled Sun4 executable stand-alone lego with coercions, legowc.
• Compiled Sun4 executable legoML with coercions, legowc.
• SML source for LEGO with coercions, legowc.
• SML source for LEGO with coercion synthesis, legowcs.

Coq with implicit coercions

The latest version of Coq implements a similar coercion synthesis system, but takes a different approach to resolving competing paths through the graph of coercions.

• copy of Typing algorithms in type theory with inheritance (Saibi).
  We propose and study a new typing algorithm for dependent type theory. This new algorithm typechecks more terms by using inheritance between classes. This inheritance mechanism turns out to be powerful: it supports multiple inheritance, classes with parameters and uses new abstract classes of functions and sorts. We also define classes as records, particularly suitable for the formal development of mathematical theories. This mechanism, implemented in the proof checker Coq, can be adapted to all typed lambda-calculus.

Work on coercive subtyping within type-theories

• DVI copy of Coercive subtyping in type theory (Luo).
  We propose and study coercive subtyping, a formal extension with subtyping of dependent type theories such as Martin-Lof's type theory and the type theory UTT. In this approach, subtyping with specified implicit coercions is treated as a feature at the level of the logical framework; in particular, subsumption and coercion are combined in such a way that the meaning of an object being in a supertype is given by coercive definition rules for the definitional equality. It is shown that this provides a conceptually simple and uniform framework to understand subtyping and coercion relations in type theories with sophisticated type structures such as inductive types and universes.
• compressed copy of Implicit coercions in type systems (Barthes).
  We propose a notion of pure type system with implicit coercions. In our framework, judgements are extended with a context of coercions and the application rule is modified so as to allow coercions to be left implicit. The setting supports multiple inheritance and can be applied to all type theories with pi-types. One originality of our work is to propose a computational interpretation for implicit coercions. In this paper, we demonstrate how this interpretation allows a strict control on the logical properties of pure type systems with implicit coercions.

Subtyping using record types

This involves the incremental definition of subtypes of previous types.

• DVI copy of Extension of Martin-Lof's theory of types with record types and subtyping: motivation, rules and type checking (Bertarte/Tasistro).
  We present an extension of Marin-Lof's type theory of types with record types and subtyping. We motivate the extension discussing the formalization of systems of algebras. Then we give its formal rules and discuss type checking, showing that this remains decidable for a class of expressions sufficiently large in practice, as it is in the original theory.
• DVI copy of Formalization of systems of algebras using dependent record types and subtyping: an example (Bertarte/Tasistro)
  We present an example of formalization of systems of algebras using an extension of Martin-Lof's theory of types with record types and subtyping. This extension is informally explained along the presentation of the example. We also provide code of the formalization as accepted by a type checker implemented for the extended theory.

Subtyping using refinement (or intersection) types

• gzipped copy of Refinement types for logical frameworks (Pfenning).
  We propose a refinement of the type theory underlying the LF framework by a form of subtypes and intersection types. This refinement preserves desirable features of LF, such as decidability of type-checking, and at the same time considerably simplifies the representations of many deductive systems. A subtheory can be applied directly to hereditary Harrop formulas which form the basis of lambda-Prolog and Isabelle.
• gzipped copy of Subtyping dependent types (Aspinnal/Compagnoni).
  The need for subtyping in type-systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as subject reduction. Here we investigate a subtyping extension of the system lambda-P, which is an abstract version of the Edinburgh logical framework LF. By using an equivalent formulation, we establish some important properties of the new system, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking.

Theory and associated mechanisms

More URLs and references are desired!
• DVI copy of A Higher-Order Calculus and Theory Abstraction (Luo).
  We present a higher-order calculus ECC which naturally combines Coquand-Huet's calculus of constructions and Martin-Lof's type theory with universes. ECC is very expressive, both for structured abstract reasoning and for program specification and construction. In particular, the strong sum types together with the type universes provide a useful module mechanism for abstract description of mathematical theories and adequate formalisation of abstract mathematics... theory abstraction in ECC is discussed as a pragmatic application.

The GALOIS project

• gzipped DVI copy of Galois: A Theory Development Project (Aczel).
  A report of work in progress, for the Turin meeting on the Representation of Mathematics in logical frameworks, January 20-23, 1993.
• gzipped DVI copy of Notes towards a formalisation of constructive Galois Theory (Aczel).
  We give a presentation of constructive Galois theory. This is intended, when completed, as a pre-formal blueprint for a machine checked formalisation and forms part of GALOIS, a long term experiment at an ambitious effort to formalise a significant body of abstract algebra.
• Anthony Bailey's Edinburgh MSc project involved LEGO work on polynomial rings. Unfortunately, I don't actually have an electronic copy at present - how daft is that? Oh well.
• And my PhD should involve a large bit of the LEGO formalisation of GALOIS, but, er, it isn't written yet.
• Alex Jones' Manchester MSc project involved LEGO work on finite vectorspaces.
  As part of the ongoing project to produce a machine checked development of Galois Theory, this document describes one way that a portion of linear algebra leading up to the decidable dependency theorem can be checked by the LEGO proof checker.

Other large-scale formalisation case-studies

• Mark Ruys has developed a large LEGO library.
  Many mathematical notions are formalized like a prime generator, the concept of universal algebra's, polynomials rings and the field of complex numbers. Also a lot of proofs are given, for example of the fact that for every complex number there exist a k-th root.
  Summaries of the LEGO files can be viewed on-line. The whole library is available by anonymous ftp.

Literate formalisation

It is possible to imagine more serious attempts at literate formalisation, which can be seen as applying the idiom of literate programming to computer-checked formalisations. Link ideas are welcome, as are implementations!

One now-completed project of interest is the proof-checker Deva, which had a DevaWEB assistant that produced such literate formalisations.

• The DevaWEB System: Introduction, Tutorial, User Manual, and Implementation (Biersack/Raschke/Simons).
  We focus on the literate and structured presentation of formal developments. We present an approach that is influenced by ideas from Leslie Lamport on how to write proofs, by Donald Knuth's paradigm of literate programming, and by the ideas of the "Dutch school" on formal reasoning. We demonstrate this approach by presenting the proofs of two mathematical theorems - the Knaster-Tarski fixpoint theorem and the Schroder-Bernstein theorem - formalized in Deva. We discuss to what degree our aims have been achieved and what is left to be done.
• Martin Simon's thesis The presentation of formal proofs .
  In this thesis we present an approach to the intelligible communication of formal proofs. Observing a close correspondence between the activities of formal-proof development and program development, and using this as a guideline, we apply well-known principles from program design to proof design and presentation, resulting in formal proofs presented in a literate style, are hierarchically structured, and emphasize calculation...
• Proof Style (John Harrison)
  We are concerned with how to communicate a mathematical proof to a computer theorem prover. This can be done in many ways, while allowing the machine to generate a completely formal proof object. The most obvious choice is the amount of guidance required from the user, or from the machine perspective, the degree of automation provided. But another important consideration, which we consider particularly significant, is the bias towards a `procedural' or `declarative' proof style. We will explore this choice in depth, and discuss the strengths and weaknesses of declarative and procedural styles for proofs in pure mathematics and for verification applications. We conclude with a brief summary of our own experiments in trying to combine both approaches.
• The Mizar project's Journal Of Formalised Mathematics
  The Mizar project started about 1973 with an attempt to reconstruct mathematical vernacular. Since 1989, the most important activity in the Mizar project is development of data base for mathematics... Journal of Formalized Mathematics is an electronic counterpart of Formalized Mathematics.
  The Journal presents many Mizar proof-scripts which have been designed to be "readable."