search

Quelklef / fitch

Interactive proof assistant for Fitch-style natural deduction
https://maynards.site/fitch
3 stars 0 forks source link

Make serialization less bad #3

Closed Quelklef closed 2 years ago

Quelklef commented 5 years ago

The serialization code is pretty bad. It's a weird mix of readable and not readable and contains [ and ] which must be encoded.

It would be nice if a serialized proof would be human-readable and would contain no characters that need to be encoded in the URL. The issue is that the only grouping characters allowed in the URL are (), which are used for grouping and precedence. This means, for example, that if we want (P; Q; R) to be the 3-line proof assuming P and deriving Q then R, that (P; (Q); R) is ambiguous. Is (Q) an nested proof, or is it grouping? While a single-statement nested proof (Q) may not be present in a valid Fitch-style proof, it is a valid state of a Proof object and should therefore be accounted for.

Additionally, there's the issue of writing declarations as [x], since [] must be encoded in the URL.

One option is to encode all propositions as <kind>(<args>), e.g. +(~(P)~(Q)) for ~P+~Q. Proofs could then be, say, P(<statements>). While this is not as human-readable, it is unambiguous, and should be fairly easy for anyone familiar with parsing and ASTs to understand.

Alternatively, the focus could be on generating the smallest URL possible. Then static-arity AST nodes would be written in prefix form, predicate applications would be written as <target>(<args>), proofs as $(<lines>) (because $ is a valid URL character but not a valid predicate name), and so on.

Quelklef commented 3 years ago

gonna have to go with "readable URLs are not that important and a reasonable solution would be to rewrite the app in purescript and then derive ToJSON"