My Own Private Automath: the Lestrade Type Inspector

Inspector Lestrade makes an arrest...perhaps on suspicion of an invalid reasoning step?

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 original implementation in Moscow ML 2.01 of the Lestrade Type Inspector. The version date is shown in the files. As of 10/14/2017 this differs by one character from a LaTex document here (literate programming attempted): the idea is that I can maintain a readably commented source in this way.

I no longer support multiple versions. It is useful to be aware that after July 2019 what was the construct command is now the postulate command and rewritec has become rewritep. Those two string replaces will likely fix any old files. Most if perhaps not all of the Lestrade source files on this page have been edited and tested with the current version and should run. I might have missed one or two.

There have been significant updates to display and file handling during the development of the Zermelo implementation.

There is a complete reimplementation discussed below.

Substantial papers and manual drafts

Here is a paper I was 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. This is the best current approximation to a manual and qua manual has been kept up to date.

The files which follow embody the largest Lestrade implementation project, now underway (summer 2019). I am implementing Zermelo's 1908 papers on axiomatization of set theory and proof of the well-ordering theorem.

Here is a conference paper I submitted to a workshop in 2018, discussing both Lestrade and Automath. It was not accepted; I need to polish it up for a different market. But it is a good source for what I am up to here.

Here is a paper I was working on in fall 2017, simultaneously an account of Lestrade and a treatment of foundational topics; it is another pass at the aims of the paper just below, and discusses new additions to the capabilities of Lestrade. The .tex source in the same directory is an executable Lestrade script.

Here is a paper I was working on in summer 2017, simultaneously an account of Lestrade and a treatment of foundational topics. The .tex source in the same directory is an executable Lestrade script.

Here is another paper I was working on in summer 2016, focussed more narrowly on the philosophical approach. The .tex source in the same directory is an executable Lestrade script.

Here is an old manual (which I updated for a while but which doesn't have the latest changes; it does not say everything that the paper designated as the manual above says, but it has a different emphasis and I think it might still be useful). The .tex source in the same directory is an executable Lestrade script.

Local talks

Here are the slides (slightly improved) for the talk I gave to the Boise State graduate seminar Sept 27 2019.

Here are the slides (slightly improved) for the talk I gave to the Boise State logic seminar Oct 24 2017. Here is an older set of slides (misleadingly also dated Oct 24 due to the date function of LaTeX).

The two sets of slides above have .tex source in the same directory which can also be fed to Lestrade.

Here are the slides for a talk I am giving locally on October 25th 2016. Here is the supporting Lestrade script file.

Smaller LaTeX files/ Lestrade scripts

Here is a file with some development of primitive recursive arithmetic.

Here is my scratch work as I read through Mike Nahas's Coq tutorial and proved analogous things under Lestrade.

Here is a paper I am working on in fall 2017, outlining implementation of homotopy type theory under Lestrade. I'm not finished with this by any means, it is rather tricky.

Here is an axiomatization of ZFC in Lestrade. Not of much interest until I prove something with it!

Here is a paper I am working on in fall 2017, exhibiting the rewriting capabilities, and the ability to use rewrite rules provably valid in a theory to implement programming behavior: the file is intended to support computation of Fibonacci numbers (thus the name) but at the moment supports a fully implemented adder for binary numerals on top of a simple theory of arithmetic: all of its computations are theorems. The rewrited command, not witnessed so far in other files, is used extensively in this one.

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.

All pdfs above have corresponding .tex files which are Lestrade scripts as well as document source.

New release in preparation

Here are the slides for the seminars I have given in Zoom in March and April 2020.

Here is the source for the implementation in Moscow ML 2.01 of a reimplementation of the Lestrade Type Inspector.

Here is the source as a PDF, demonstrating my devotion to literate programming.

Here is the directory containing output files for the new version. The new version has the same input language (except that it does not support rewriting) but a quite different file format. There is a utility for exporting files from the first version, and files from the first version which do not use rewriting can now reliably be revised to run under the second version: all the files for the proof of the well-ordering theorem have been converted, as have the examples embedded in my large papers. There are some differences in the parser and in move saving and implicit argument inference which require occasional changes.

Here is the source for the implementation in Moscow ML 2.01 of the reimplementation of the Lestrade Type Inspector, adapted to PolyML.

Here is the source (adapted to PolyML) as a PDF, demonstrating my devotion to literate programming.

It is useful to remark that I am now thinking that PolyML is my preferred platform. I am maintaining source designed for PolyML, with partial implementation of rewriting which doesn't yet do anything, with a preamble which can be edited to make it work under Moscow ML (and under other MLs). There is another modification: the path LTXTs\ needs to be changed to LTXTs/ for this to work in Linux. This isn't currently handled in the posted files, though I expect to provide support for this in the preamble.

Here are the converted versions of the files for Zermelo's 1908 papers on axiomatization of set theory and proof of the well-ordering theorem.

Here is the tutorial on Lestrade which I am working on in March 2024.

Here is a paper I was 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, updated for the new implementation. This is the best current approximation to a manual and qua manual has been kept up to date (not quite as true for the new implementation, but it does have an updated command list).

Here is a paper I was working on in summer 2017, simultaneously an account of Lestrade and a treatment of foundational topics, updated for the new version.

An implementation of Automath itself

Here is the documentation and the (Python) source for an actual implementation of Automath. It runs the classic long Automath example, an implementation of Landau's little arithmetic book. It must be noted that it takes hours to run the Landau book, where Freek Wiedijk's implementation takes seconds; but it does have some interest. Here is a paper (submitted to a conference but not accepted) which discusses the relationship between Lestrade and Automath.

Script files

Lestrade scripts have the extension .lti (.ltxt for the new version) 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. The use of .lti files is superseded for the most part by the use of executable .tex files as Lestrade scripts.

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.