10 lines
2.3 KiB
Org Mode
10 lines
2.3 KiB
Org Mode
|
#+title: README
|
||
|
|
#+author: William Ball
|
||
|
|
|
||
|
|
* FOL Idris
|
||
|
|
I'm definitely not the first person to do this, but I had an idea a while back for correct by construction FOL terms and formulas in a dependently typed language, and finally got around to playing with it, and it is very cool. The idea is I have a type `Term` representing a term in some first order language, and a type `Formula` representing a formula in that language. Then, through some careful applications of dependent types, it is only possible to construct well-formed formulas. For example, suppose the signature `N` contains a binary function symbol `Plus`, a nullary function symbol (i.e.\nbsp{}constant symbol) `Zero`, and a unary function symbol `S`. Then you can construct the term `Plus(Zero, S(Zero))`, but `Plus(S(Zero(Zero), Zero))` doesn't type check.
|
||
|
|
|
||
|
|
Where things start to get really cool is that you can do the same thing with a proof object. So `Proof` is a type representing a proof, but only correct proofs can even be constructed. Typically you'd have representations of terms, formulas, and proofs, but then would have to write code to verify them; verify that the proof is correct and that the terms and formulas are well formed. You can also very easily play with different logics by just tweaking the constructors of `Proof`. For example, by removing the constructor `Contra` from `Proof`, and adding some other constructors that become necessary, you'd have an intuitionist logic. As it stands, the rules and connectives are extremely minimal, with derived rules existing as proofs in the `Logic` module[fn:: `EqRefl` and `EqTrans` are provable from `EqE`, but using `EqE` is quite difficult in general, at least without the theorem `elimBinder (inc t) s = t` stating that adding a variable you don't use to a term then substituting it doesn't do anything, but I was struggling to prove that, not being familiar with Idris's capabilities as a proof assistant.].
|
||
|
|
|
||
|
|
I don't really have a goal with this project, and have just been working on it for fun. There's tons more work that can be done. As it stands, this is far less capable/usable than [[https://forgejo.ballcloud.cc/wball/perga][my last proof assistant]], but I think it's pretty cool. It's pretty similar to [[https://github.com/epfl-lara/lisa][lisa]], but with a more trusted kernel and far less usability.
|