5
$\begingroup$

I am planning to implement a FOL proof assistant in Haskell. What are some useful libraries and implementations I should be looking at?

Here are some further details. I have a simple proof checker for propositional calculus implemented in Lean (see this and this). I am hoping to do the same for predicate logic. I then intend to create a proof assistant in Haskell and have the proofs created using it be exportable to a format that can be run through the Lean implementation of the checker. In this manner I hope to have a formal proof of the soundness of the trusted kernel, assuming that Lean is sound. The current state of this is here.

The issue at present is deciding if I should change to a different encoding for variables, for example locally nameless. The simplest to implement seems to be the substitution described here, but I am not certain if it has shortcomings that I have not seen yet.

Improve this question
$\endgroup$
12
  • $\begingroup$ IMHO this question is slightly too broad for a good answer, can you be more specific? For instance, what background knowledge and/or familiar proof assistants you have, and what part (macroscopic design? specific implementation details?) you would like to know about. $\endgroup$
    – Trebor ♦
    Commented Jun 18, 2022 at 4:42
  • $\begingroup$ @Trebor Updated. $\endgroup$
    – user695931
    Commented Jun 18, 2022 at 5:16
  • 1
    $\begingroup$ Do not write "EDIT" and stuff, just edit the question. $\endgroup$
    – Andrej Bauer
    Commented Jun 18, 2022 at 10:24
  • $\begingroup$ A "proof assistant" can mean many things. What mode of user interaction are you imagining? Would it be interactive, or would the proof assistant just process some files? $\endgroup$
    – Andrej Bauer
    Commented Jun 18, 2022 at 10:32
  • $\begingroup$ @AndrejBauer The proof checker in Lean would just process the files exported from the proof assistant as a final check. The proof assistant in Haskell would be interactive. $\endgroup$
    – user695931
    Commented Jun 18, 2022 at 16:02

3 Answers 3

Reset to default
4
$\begingroup$

Here's what uncle Google gave me:

It's difficult to give better advice since we do not know whether your project is just a hobby, a thesis, or a plan for world domination.

Improve this answer
$\endgroup$
3
$\begingroup$

I am planning to implement a FOL proof assistant in Haskell. What are some useful libraries and implementations I should be looking at?

Does this do the Haskell part of what you need? I ask because as others have noted your question is seeking more of a compass direction than a destination.

Port of the Objective Caml code supporting John Harrison's logic textbook Handbook of Practical Logic and Automated Reasoning to Haskell. (GitHub)

Also see the readme.

The Code and resources for "Handbook of Practical Logic and Automated Reasoning" (link) has the original OCaml code used for the book.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thank you. That has actually been the primary reference for what I have so far. $\endgroup$
    – user695931
    Commented Jun 18, 2022 at 15:57
  • $\begingroup$ What I have not been able to find in it is an algorithm for the substitution of predicates: proofassistants.stackexchange.com/questions/1487/… $\endgroup$
    – user695931
    Commented Jun 18, 2022 at 15:58
  • $\begingroup$ I do have a copy that I bought. $\endgroup$
    – user695931
    Commented Jun 18, 2022 at 16:14
  • $\begingroup$ Thank you for the link. I didn't realize there was also a port to Haskell. $\endgroup$
    – user695931
    Commented Jun 18, 2022 at 16:19
  • $\begingroup$ Let us continue this discussion in chat. $\endgroup$
    – Guy Coder
    Commented Jun 18, 2022 at 16:21
2
$\begingroup$

So I think the biggest difference here from other questions is your implementation techniques don't necessarily have to be so restricted as implementation within proof assistants.

Consider the question How to deal with Binders? . In an implementation in Haskell you can use non strictly positive HOAS like

data Term :=
| Var String
| App Term Term
| Lam (Term -> Term)

Which is all sorts of weird from a formal semantics perspective.

Aside from not proving things I would say non strictly positive datatypes and general recursion are really the biggest simplifications from implementation within a theorem prover I guess. You can use mutable state and side effects to make some things faster but I'm not really sure they simplify things in the end.

You might also want to look into the trick GHC uses for lazily generating variable names by threading a lazy tree of variables through.

Also a tagless final style is a lot more useful in a language you don't have to prove things about (tagless final means you lose induction over things.)

Unfortunately I just personally don't have the practical experience to recommend specific libraries.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.