What is the simplest theorem prover/verifier/checker you know? This question is two fold: simplest implementation and simplest meta-theory.
Here are the ones I know:
Simplest implementation:
Victor Maia's implementation of Cedille Core: Based on the Aaron Stump's Calculus of Dependent Lambda Eliminations (CDLE). I believe this ties for the simplest implementation of a theorem prover with the next item on this list. Note that I mean simplest implementation, you gotta understand CDLE or it will seem like a quite weird extension of the Calculus of Constructions (CC).
Beckert and Posegga's leanTAP: its simple due to its size, but its written in quite compact Prolog which makes it harder to read. An interesting extension called alpha leanTAP exists, which is written in Scheme (using miniKanren, if I remember correctly). You can read more about it here.
Simplest theory:
Any implementation of Simply Typed Lambda Calculus. However, you can't prove many interesting things in it.
Metamath's formal grammar: Metamath is weird. I don't really understand its theoretical basis, it seems like it comes from the study of formal grammars. Mario Carneiro's paper Models for Metamath seems like a great resource, which unfortunately haven't had the time to read yet.
Hopefully, others can contribute for these lists. It is really hard to find truly small theorem provers (ones which you can hopefully read the entire source code in one sitting, from the ones above, only Morte doesn't fit this criteria). Also, if someone could please explain to me what exactly is going on with Metamath's meta-theory it would be much appreciated. :grinning_face_with_smiling_eyes:
Indeed. Formality is pretty cool. However, I don't believe its consistent. It has been a while since I've last checked it out, but back then, their goal had moved away from begin logically consistent to being nicer to program with.
I would be great news if what they are doing with self types/insanely dependent types (I don't know what they call, but it is kind of mix of both of these concepts) actually happens to be consistent, i.e., not allow one to inhabit false.
A system based on "Gentle art of levitation" would be pretty simple to implement (except for cumulative universe which I haven't figured out yet). You start with dependent functions and pairs, add finite types (unit + bool for example) and then you add descriptions and fixpoints on them. Using the descriptions you can define inductive datatypes (or indexed types and even recursive-inductive and inductive-inductive types based on what descriptions you use) and define a induction principle for them. I think this gives you a lot of expressivity in a small package. I also I found elaboration easier to implement than CDLE or self-types.
A system based on "Gentle art of levitation" would be pretty simple to implement [...]
I remember stumbling upon this paper about a year ago. It looked a bit convoluted, but I was way less familiar with this stuff back then. Is there an implementation of it's type theory around somewhere?
About (non-comulative) universes, Andrej Bauer implements them in his series How to Implement a Dependent Type Theory. I wonder how much more difficult comulative universes really are.
When I first looked at "Gentle art of levitation" I also found it convoluted, but after making some implementations of dependent type theories the implementation of datatypes using descriptions is actually much easier than native top-level datatype definitions. It's worth to give another look. Unfortunately I am unable to find any implementation of it, Epigram and Foveran (https://github.com/bobatkey/foveran) and Spire use them, but they are basically abandoned.
About universes, yes I've seen the implementation of Andrej Bauer but the difficulty I'm talking about is being able to lift definitions to different universes. You don't want to write the same definition multiple times just to use it in a higher level. This lifting operator is a bit tricky to implement from what I read, but I still need to spend more time on it.
And yeah, with descriptions you do not need to do any positivity checking, the description setup will ensure the datatypes are strictly-positive. The downside is that you are also more limited in which datatypes you can get.
I read that W-types are not good at all in an intensional setting, Conor McBride had a blog post on it that I am now unable to find.
I'd add Cur to this list. It's basic idea is "provide a minimal type theory, and then use macros to build things on top of this". It also has the advantage of being built using Turnstile, so its implementation looks a lot like type rules: https://github.com/wilbowma/cur
Ah that's very cool! Looks like Cur's core language is similar to the Calculus of Inductive Constructions. I will also link Dedukti/LambdaPi: https://github.com/Deducteam/lambdapi which is a type theory with rewrite rules. The core language is very simply, basically the Calculus of Constructions but I think the rewrite rules allow you to define more complicated theories inside of the language. I do wonder how consistency/canonicity is ensured though, if it is.
@Pedro Minicz I would also add to the list of simplest implementations the amazing turing machine written in an optimizing compiler called Not Quite Laconic (NQL) which was used to give a bound on the smallest undecidable busy beaver number. It was essentially a metamath kernel that enumerated proofs in ZFC looking for a contradiction
Also HOL light definitely deserves to be in the running for simplest kernel; IIRC John Harrison has the implementation written on a T-shirt. I'm not sure if the actual kernel in the hol light distribution is as small as it could be, but here it is
What is the simplest theorem prover/verifier/checker you know? This question is two fold: simplest implementation and simplest meta-theory.
Here are the ones I know:
Simplest implementation:
Simplest theory:
Hopefully, others can contribute for these lists. It is really hard to find truly small theorem provers (ones which you can hopefully read the entire source code in one sitting, from the ones above, only Morte doesn't fit this criteria). Also, if someone could please explain to me what exactly is going on with Metamath's meta-theory it would be much appreciated. :grinning_face_with_smiling_eyes:
I believe Formality is one of the simpler proof-languages implementation wise. But I haven't looked to closely at it.
Indeed. Formality is pretty cool. However, I don't believe its consistent. It has been a while since I've last checked it out, but back then, their goal had moved away from begin logically consistent to being nicer to program with.
I would be great news if what they are doing with self types/insanely dependent types (I don't know what they call, but it is kind of mix of both of these concepts) actually happens to be consistent, i.e., not allow one to inhabit
false
.I've managed to get math-phobic and recreational people hooked on http://incredible.pm/
A system based on "Gentle art of levitation" would be pretty simple to implement (except for cumulative universe which I haven't figured out yet). You start with dependent functions and pairs, add finite types (unit + bool for example) and then you add descriptions and fixpoints on them. Using the descriptions you can define inductive datatypes (or indexed types and even recursive-inductive and inductive-inductive types based on what descriptions you use) and define a induction principle for them. I think this gives you a lot of expressivity in a small package. I also I found elaboration easier to implement than CDLE or self-types.
James King said:
Oh, very interesting, looks pretty cool. It remembered be of this interactive sequent calculus tutorial (spoiler: its pretty good).
Albert ten Napel said:
I remember stumbling upon this paper about a year ago. It looked a bit convoluted, but I was way less familiar with this stuff back then. Is there an implementation of it's type theory around somewhere?
About (non-comulative) universes, Andrej Bauer implements them in his series How to Implement a Dependent Type Theory. I wonder how much more difficult comulative universes really are.
I personally haven't implement them(actually, I have), but they look simpler than positivity checking, W-types, etc.When I first looked at "Gentle art of levitation" I also found it convoluted, but after making some implementations of dependent type theories the implementation of datatypes using descriptions is actually much easier than native top-level datatype definitions. It's worth to give another look. Unfortunately I am unable to find any implementation of it, Epigram and Foveran (https://github.com/bobatkey/foveran) and Spire use them, but they are basically abandoned.
About universes, yes I've seen the implementation of Andrej Bauer but the difficulty I'm talking about is being able to lift definitions to different universes. You don't want to write the same definition multiple times just to use it in a higher level. This lifting operator is a bit tricky to implement from what I read, but I still need to spend more time on it.
Spire blog: http://spire-lang.org/blog/2014/01/15/modeling-elimination-of-described-types/
Another blog post about descriptions: http://effectfully.blogspot.com/2016/04/descriptions.html
And yeah, with descriptions you do not need to do any positivity checking, the description setup will ensure the datatypes are strictly-positive. The downside is that you are also more limited in which datatypes you can get.
I read that W-types are not good at all in an intensional setting, Conor McBride had a blog post on it that I am now unable to find.
I'd add Cur to this list. It's basic idea is "provide a minimal type theory, and then use macros to build things on top of this". It also has the advantage of being built using Turnstile, so its implementation looks a lot like type rules: https://github.com/wilbowma/cur
Ah that's very cool! Looks like Cur's core language is similar to the Calculus of Inductive Constructions. I will also link Dedukti/LambdaPi: https://github.com/Deducteam/lambdapi which is a type theory with rewrite rules. The core language is very simply, basically the Calculus of Constructions but I think the rewrite rules allow you to define more complicated theories inside of the language. I do wonder how consistency/canonicity is ensured though, if it is.
@Pedro Minicz I would also add to the list of simplest implementations the amazing turing machine written in an optimizing compiler called Not Quite Laconic (NQL) which was used to give a bound on the smallest undecidable busy beaver number. It was essentially a metamath kernel that enumerated proofs in ZFC looking for a contradiction
it was something around a 1500 state TM whose termination could not be proved in ZFC (EDIT: here it is, 1919 states)
Also HOL light definitely deserves to be in the running for simplest kernel; IIRC John Harrison has the implementation written on a T-shirt. I'm not sure if the actual kernel in the hol light distribution is as small as it could be, but here it is
Not simple but very cool: https://cicada-lang.org/