My Own Private Automath: the Lestrade Type Inspector
This page provides resources related to a current little project of
mine, whose motivation is actually philosophical. I have in mind a view
of the philosophy of mathematics under which the objects of classical,
nonconstructive, impredicative mathematics with higher orders of
infinity are naturally accessible by finitary means, all the infinities
being merely potential. This view exploits the Curry Howard isomorphism
and some thoughts of mine about the nature of abstraction, and if it is
to be taken seriously should be implementable on a computer. The
implementation (given the intellectual ingredients I have mentioned)
should resemble Automath. And it does.
An implementation is now found here with documentation and examples.
The name is admittedly a bit of mischief: I am Holmes, I already have a prover called Watson, and my son suggested that I call this one Lestrade...
Here is the source for the implementation in Moscow ML 2.01 of the Lestrade Type Inspector.
Here is the manual (which I have updated; it does not say everything that the paper below says, but it has a different emphasis and I think it is still useful).
Here is the source for the implementation in Poly/ML of the Lestrade Type Inspector.
Here is the source for the implementation in Moscow ML 2.10.1 of the Lestrade Type Inspector.
Here is a paper I am working on in summer 2016, containing an outline of the philosophical approach, an account of the commands and the formal language of Lestrade, and extensive sample Lestrade books.
Here is another paper I am working on in summer 2016, focussed more narrowly on the philosophical approach.
And here is another paper I am working on in fall 2016, which pretends to be an initial segment of an elementary discrete math test supported by Lestrade text.
Here is the source for the implementation in Moscow ML 2.01 of a version of Lestrade without the new type inference capabilities, which I will continue to maintain. I'll leave this up, but maintenance of it is suspended: the main version now supports a command basic() which will give this behavior, and fullversion() to restore type inference functions.
Here are the slides for a talk I am giving locally on October 25th 2016. Here is the supporting Lestrade script file.
Lestrade scripts have the extension .lti and should be opened with a text editor. They are executable by Lestrade itself using the readfile command, and they are produced by Lestrade as log files. Some of these files are things I am working on which will continue to be updated.
- russell.lti is a self-contained implementation of Russell's paradox. Needless to say, there are assumptions which lead to the paradox; the logic of Automath itself is consistent.
- landau_axioms.lti is my ongoing implementation of Landau's Foundations of Analysis (following in the footsteps of the original Automath project). I'm currently in the middle of proposition 4. This is not a polished production; I am hacking as I go. It will get cleaned up later! [This is a stalled project from summer 2015, but I have made a little progress on it recently].
- summer2016book.lti is a new set of declarations I am working on in summer 2016. This includes general logic and now basic declarations for natural numbers and the simple typed theory of sets.
- rewrites.lti is a new set of declarations I am working on in summer 2016. This is to be run with the new version of Lestrade with rewriting, and exhibits elementary examples of rewrite rule programming, similar
in style to that found in Watson. I want to develop examples where rewrite rules are demonstrated on the basis of proofs rather than introduced by fiat, but the rewrite construction command is a perfectly reasonable way to introduce an equational axiom -- if one is willing for it always to be applied as a simplification.
- auto37.lti is another new summer 2016 file I am working on: I am translating file
37 in the Automath archive from Automath to Lestrade, which is quite instructive (for me at any rate).
- autoi37.lti is the auto37 translation as far as it goes, making full use of the implicit arguments feature.
- implicittest.lti contains some examples of implicit argument inference.
- maclane.lti contains a set of declarations for Mac Lane set theory (somewhat modified). >maclanetest.lti has a few more test declarations I am working on which motivated recent upgrades of implicit argument inference.
- geometry.lti contains a set of declarations for Euclidean plane geometry (in a very preliminary state).
- discretemath.lti contains the declarations supporting the purported discrete math text.
- pocket.lti contains the basic declarations for "pocket set theory"; before reading it, you need to read discretemath, which it imports.
- logicpackage.lti is a new logic file that I'm working on which is intended for use as a module via the import command: once it is ready I'll try eliminating logical preambles from some other files.
Classical Automath resources
Here is Freek
Wiedijk's Automath site, including the only currently available
implementation of standard Automath (as far as I know). What I present
here is not standard Automath!
Here is the official Automath archive site.