wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

updated README

Browse source
This commit is contained in:
William Ball 2024-11-12 09:19:48 -08:00
parent 9e390c0ab6
commit aa05f3025e
2 changed files with 13 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
README.md
View file

@ -1,28 +1,6 @@
# Table of Contents
1. [Syntax](#org5c21ec8)
2. [Basic Usage](#org3caa2bf)
1. [Sample Session](#org206dc85)
3. [Goals](#org677567c)
1. [Substantive](#org6946354)
1. [DEFINITIONS](#orga4323f7)
2. [Inference](#org4a2e73d)
3. [Implicits](#orgd2f67c2)
4. [Universes?](#orgec0ab63)
5. [Inductive Definitions](#org2f139ca)
2. [Cosmetic/usage/technical](#orgf241f8d)
1. [Prettier pretty printing](#org8686345)
2. [Better usage](#orgee07e09)
3. [Improve error messages](#org9739c98)
4. [Improve β-equivalence check](#orgd3ee15c)
5. [Better testing](#orgb19926c)
A basic implementation of a dependently typed lambda calculus (calculus of constructions) based on the exposition in Nederpelt and Geuvers *Type Theory and Formal Proof*. Right now it is *technically* a perfectly capable higher order logic proof checker, though there is lots of room for improved ergonomics and usability, which I intend to work on. A basic implementation of a dependently typed lambda calculus (calculus of constructions) based on the exposition in Nederpelt and Geuvers *Type Theory and Formal Proof*. Right now it is *technically* a perfectly capable higher order logic proof checker, though there is lots of room for improved ergonomics and usability, which I intend to work on.
<a id="org5c21ec8"></a>
# Syntax # Syntax
The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as `megaparsec` calls them alphanumeric. Lambda and Pi abstractions can be written in many obvious ways that should be clear from the examples below. Additionally, arrows can be used as an abbreviation for a Π type where the parameter doesn&rsquo;t appear in the body as usual. The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as `megaparsec` calls them alphanumeric. Lambda and Pi abstractions can be written in many obvious ways that should be clear from the examples below. Additionally, arrows can be used as an abbreviation for a Π type where the parameter doesn&rsquo;t appear in the body as usual.
@ -34,15 +12,11 @@ All of the following examples correctly parse, and should look familiar if you a
fun (S : *) (P Q : S -> *) (H : Π (x : S) . P x -> Q x) (HP : forall (x : S), P x) => fun (x : S) => H x (HP x) fun (S : *) (P Q : S -> *) (H : Π (x : S) . P x -> Q x) (HP : forall (x : S), P x) => fun (x : S) => H x (HP x)
<a id="org3caa2bf"></a>
# Basic Usage # Basic Usage
For the moment, running the program drops you into a repl where you can enter terms in the calculus of construction, which the system will then type check and report the type of the entered term, or any errors if present. For the moment, running the program drops you into a repl where you can enter terms in the calculus of construction, which the system will then type check and report the type of the entered term, or any errors if present.
<a id="org206dc85"></a>
## Sample Session ## Sample Session
Here&rsquo;s a sample session. Suppose your goal is to prove that for every set $S$ and pair of propositions $P$ and $Q$ on $S$, if $\forall x \in S, P x$ holds, and $\forall x \in S, P x \Rightarrow Q x$, then $\forall x \in S, Q x$. A set $S$ corresponds to a type `S`, so our term will begin Here&rsquo;s a sample session. Suppose your goal is to prove that for every set $S$ and pair of propositions $P$ and $Q$ on $S$, if $\forall x \in S, P x$ holds, and $\forall x \in S, P x \Rightarrow Q x$, then $\forall x \in S, Q x$. A set $S$ corresponds to a type `S`, so our term will begin
@ -74,18 +48,12 @@ This output is a bit hard to read, but it is ultimately in the form `term : type
More complex and interesting proofs and theorems are technically possible (in fact, *all* interesting theorems and proofs are possible, for a certain definition of *interesting*, *theorem*, and *proof*), though practically infeasible without definitions. More complex and interesting proofs and theorems are technically possible (in fact, *all* interesting theorems and proofs are possible, for a certain definition of *interesting*, *theorem*, and *proof*), though practically infeasible without definitions.
<a id="org677567c"></a>
# Goals # Goals
<a id="org6946354"></a>
## Substantive ## Substantive
<a id="orga4323f7"></a>
### TODO DEFINITIONS ### TODO DEFINITIONS
Some kind of definition system would be a difficult and substantial addition, but man is it necessary to do anything. Likewise, I&rsquo;d probably want a way to define primitive notions/axioms, but that should be an easy extension of the definition system. Further following *Type Theory and Formal Proof* would additionally yield a nice context system, which would be handy, though I disagree with the choice to differentiate between parameterized definitions and functions. That distinction doesn&rsquo;t really make sense in full calculus of constructions. Some kind of definition system would be a difficult and substantial addition, but man is it necessary to do anything. Likewise, I&rsquo;d probably want a way to define primitive notions/axioms, but that should be an easy extension of the definition system. Further following *Type Theory and Formal Proof* would additionally yield a nice context system, which would be handy, though I disagree with the choice to differentiate between parameterized definitions and functions. That distinction doesn&rsquo;t really make sense in full calculus of constructions.
@ -93,70 +61,55 @@ Some kind of definition system would be a difficult and substantial addition, bu
Sidenote: With a definition system, I would greatly prefer Haskell-style type annotations to ML-style type annotations, though the latter are likely way easier to implement. It serves as a nice bit of documentation, de-clutters the function definition, and follows the familiar mathematical statement-proof structure. Sidenote: With a definition system, I would greatly prefer Haskell-style type annotations to ML-style type annotations, though the latter are likely way easier to implement. It serves as a nice bit of documentation, de-clutters the function definition, and follows the familiar mathematical statement-proof structure.
<a id="org4a2e73d"></a>
### TODO Inference ### TODO Inference
Obviously not fully decidable, but I might be able to implement some basic unification algorithm. This isn&rsquo;t super necessary though, I find leaving off the types of arguments to generally be a bad idea, but in some cases it can be worth it. Obviously not fully decidable, but I might be able to implement some basic unification algorithm. This isn&rsquo;t super necessary though, I find leaving off the types of arguments to generally be a bad idea, but in some cases it can be worth it.
<a id="orgd2f67c2"></a>
### TODO Implicits ### TODO Implicits
Much, much more useful than [inference](#org4a2e73d), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. Much, much more useful than [inference](#orgda125c7), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none.
<a id="orgec0ab63"></a>
### TODO Universes? ### TODO Universes?
Not really necessary without [inductive definitions](#org2f139ca), but could be fun. Not really necessary without [inductive definitions](#org0f7d084), but could be fun.
<a id="org2f139ca"></a>
### TODO Inductive Definitions ### TODO Inductive Definitions
This is definitely a stretch goal. It would be cool though, and would turn this proof checker into a much more competent programming language. It&rsquo;s not necessary for the math, but inductive definitions let you leverage computation in proofs, which is amazing. They also make certain definitions easier, by avoiding needing to manually stipulate elimination rules, including induction principles. This is definitely a stretch goal. It would be cool though, and would turn this proof checker into a much more competent programming language. It&rsquo;s not necessary for the math, but inductive definitions let you leverage computation in proofs, which is amazing. They also make certain definitions easier, by avoiding needing to manually stipulate elimination rules, including induction principles.
<a id="orgf241f8d"></a>
## Cosmetic/usage/technical ## Cosmetic/usage/technical
<a id="org8686345"></a>
### TODO Prettier pretty printing ### TODO Prettier pretty printing
Right now, everything defaults to one line, which can be a problem with how large the proof terms get. Probably want to use [prettyprinter](https://hackage.haskell.org/package/prettyprinter) to be able to nicely handle indentation and line breaks. Right now, everything defaults to one line, which can be a problem with how large the proof terms get. Probably want to use [prettyprinter](https://hackage.haskell.org/package/prettyprinter) to be able to nicely handle indentation and line breaks.
<a id="orgee07e09"></a>
### TODO Better usage ### TODO Better usage
Read input from a file if a filename is given, otherwise drop into a repl. Perhaps use something like [haskeline](https://hackage.haskell.org/package/haskeline) to improve the repl (though `rlwrap` is fine, so not a huge priority). Read input from a file if a filename is given, otherwise drop into a repl. Perhaps use something like [haskeline](https://hackage.haskell.org/package/haskeline) to improve the repl (though `rlwrap` is fine, so not a huge priority).
<a id="org9739c98"></a>
### TODO Improve error messages ### TODO Improve error messages
The error messages currently aren&rsquo;t terrible, but it would be nice to have, e.g. line numbers. `megaparsec` allows for semantic errors, so somehow hook into that like what I&rsquo;m doing for unbound variables? The error messages currently aren&rsquo;t terrible, but it would be nice to have, e.g. line numbers. `megaparsec` allows for semantic errors, so somehow hook into that like what I&rsquo;m doing for unbound variables?
<a id="orgd3ee15c"></a>
### TODO Improve β-equivalence check ### TODO Improve β-equivalence check
The check for β-equivalence could certainly be a lot smarter. This is much less of an issue without [inductive definitions](#org2f139ca)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it&rsquo;s certainly not a bad idea. The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn&rsquo;t the best strategy. This is much less of an issue without [inductive definitions](#org0f7d084)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it&rsquo;s certainly not a bad idea.
<a id="orgb19926c"></a>
### TODO Better testing ### TODO Better testing
Using some kind of testing framework, like [QuickCheck](https://hackage.haskell.org/package/QuickCheck) and/or [HUnit](https://hackage.haskell.org/package/HUnit) seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable. Using some kind of testing framework, like [QuickCheck](https://hackage.haskell.org/package/QuickCheck) and/or [HUnit](https://hackage.haskell.org/package/HUnit) seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable.
### TODO TUI
This is definitely a stretch goal, but I&rsquo;m imagining a TUI split into two panels. On the left you can see the term you are building with holes in it. On the right you have the focused hole&rsquo;s type as well as the types of everything in scope (like Coq and Lean show while you&rsquo;re in the middle of a proof). Then you can interact with the system by entering commands (e.g. `intros`, `apply`, etc.) which changes the proof term on the left. You&rsquo;d also just be able to type in the left window as well, and edit the proof term directly. This way you&rsquo;d get the benefits of working with tactics, making it way faster to construct proof terms, and the benefits of working with proof terms directly, namely transparency and simplicity. I&rsquo;ll probably want to look into [brick](https://hackage.haskell.org/package/brick) in order to make this happen.

6
README.org
View file

@ -1,4 +1,5 @@
#+title: Dependent Lambda #+title: Dependent Lambda
#+options: toc:nil
A basic implementation of a dependently typed lambda calculus (calculus of constructions) based on the exposition in Nederpelt and Geuvers /Type Theory and Formal Proof/. Right now it is /technically/ a perfectly capable higher order logic proof checker, though there is lots of room for improved ergonomics and usability, which I intend to work on. A basic implementation of a dependently typed lambda calculus (calculus of constructions) based on the exposition in Nederpelt and Geuvers /Type Theory and Formal Proof/. Right now it is /technically/ a perfectly capable higher order logic proof checker, though there is lots of room for improved ergonomics and usability, which I intend to work on.
@ -77,7 +78,10 @@ Read input from a file if a filename is given, otherwise drop into a repl. Perha
The error messages currently aren't terrible, but it would be nice to have, e.g. line numbers. =megaparsec= allows for semantic errors, so somehow hook into that like what I'm doing for unbound variables? The error messages currently aren't terrible, but it would be nice to have, e.g. line numbers. =megaparsec= allows for semantic errors, so somehow hook into that like what I'm doing for unbound variables?
*** TODO Improve β-equivalence check *** TODO Improve β-equivalence check
The check for β-equivalence could certainly be a lot smarter. This is much less of an issue without [[Inductive Definitions][inductive definitions]]/recursion, as far less computation gets done in general, let alone at the type level. That being said, it's certainly not a bad idea. The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn't the best strategy. This is much less of an issue without [[Inductive Definitions][inductive definitions]]/recursion, as far less computation gets done in general, let alone at the type level. That being said, it's certainly not a bad idea.
*** TODO Better testing *** TODO Better testing
Using some kind of testing framework, like [[https://hackage.haskell.org/package/QuickCheck][QuickCheck]] and/or [[https://hackage.haskell.org/package/HUnit][HUnit]] seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable. Using some kind of testing framework, like [[https://hackage.haskell.org/package/QuickCheck][QuickCheck]] and/or [[https://hackage.haskell.org/package/HUnit][HUnit]] seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable.
*** TODO TUI
This is definitely a stretch goal, but I'm imagining a TUI split into two panels. On the left you can see the term you are building with holes in it. On the right you have the focused hole's type as well as the types of everything in scope (like Coq and Lean show while you're in the middle of a proof). Then you can interact with the system by entering commands (e.g. =intros=, =apply=, etc.) which changes the proof term on the left. You'd also just be able to type in the left window as well, and edit the proof term directly. This way you'd get the benefits of working with tactics, making it way faster to construct proof terms, and the benefits of working with proof terms directly, namely transparency and simplicity. I'll probably want to look into [[https://hackage.haskell.org/package/brick][brick]] in order to make this happen.