Hi, I am trying to use SWI to debug/play with a proof system I am designing, hence I’m only interested in successful derivations.
I tried sldnfdraw and can run its member example, but it inexplicably doesn’t work on my rules, not sure why. Also it draws the entire tree, including failures.
Next, I tried trace/2, which somewhat works if I use trace(my_rule, exit)., but only if every successfully exited predicate appears in the successful derivation.
Is there some way I could filter the trace? Maybe a way to capture the trace from trace as a tree-like term for postprocessing? I am trying to avoid parsing the text of the trace like this.
Possibly the new add-on "ddebug" pack for SWI-Prolog could be of help. See the pack readme for details. Do not ignore this sentence:
This requires the current GIT version or SWI-Prolog 9.1.12 or later.
The package provides code to collect the successful derivation by hooking into the Prolog debugger. Next it provides a simple terminal browser to navigate the tree. It is quick and dirty work based on discussion with Włodzimierz Drabent at the ICLP in London.
A more roll-your-own way than the package recommended by Jan is to write a meta-interpreter that collects the goals derived during a proof. There’s an example of that in Markus Triska’s page on Prolog meta-interpreters, here:
?- mi_tree(g(natnum(X)), T).
T = true=>natnum(0), X = 0
; T = (true=>natnum(0))=>natnum(s(0)), X = s(0)
; T = ((true=>natnum(0))=>natnum(s(0)))=>natnum(s(s(0))), X = s(s(0))
Really cool stuff, thank you! I tried ddebug via Homebrew --head and it works well, exactly as I expected. ddebug:proof_tree/2 was more useful than the navigator in my case as I wanted to export the proof to another format.
I did some quick experiments with the metainterpreter approach. It’s definitely very flexible, but needs to be extended to handle things like builtins.
A full meta interpreter is not easy. You’ll find a fully ISO compliant alternative to call/1 in boot/init.pl as $meta_call/1. This is internally used for call/1 under delimited continuations as these cannot handle the normal compilation based call/1. $meta_call/1 is a good starting point for a full meta interpreter that can deal with cuts, etc.
Probably a proper meta interpreter based approach is faster than hooking the debugger. It is hard to get complete though.
Something I do sometimes is just add an explicit tracing parameter, or similarly write my proof rules using DCGs where the stream is a sequence of rule breadcrumbs. For example something like
prove(A > A) --> [id].
prove(A /\ _ > A) --> [fst].
prove(_ /\ B > B) --> [snd].
prove(A > A \/ _) --> [inj1].
prove(B > _ \/ B) --> [inj2].
prove(false > _) --> [initial].
prove( _ > true) --> [terminal].
prove(A > B /\ C) --> [pair], prove(A > B), prove(A > C).
prove(A \/ B > C) --> [case], prove(A > C), prove(B > C).
prove(A > C) --> [comp], prove(A > B), prove(B > C).
You can then pretty print the breadcrumbs to a bussproofs latex script like here
I did not mean anything deep by the term “breadcrumbs”. What I meant is that merely the storage of a prefix traversal is not the most elaborate proof object one could desire and may require post processing to fill in more details (such as the sequent at intermediate points in the tree). It does record all of the branching search required to prove the goal though (I think).
I believe your adding of curry and uncurry rules is correct if you want to include arrows. My point wasn’t to describe that particular system, I just copied it out of my notes as an example of the DCG proof recording technique. It is a very cute system though. A couple observations
prove could have been called typeof. The proof object is a functional programming expression made of categorical combinators and the theorem in question is a simple type. Our prove is a type checker, a type synthesizer, or a type directed program synthesizer depending on the mode we are using.
The key insight for this flavor of categorical logic is that one should consider sequents with only 1 slot before and after the turnstile. That this is a natural design point compared to sequent calculus (multiple slots on both sides) and natural deduction (multiple hypothesis slots, one consequent slot) is not stated clearly enough for me in most texts
Perhaps my main complaint about standard prolog is that it treats variable binding poorly. This is perhaps fine, except when you are trying to model domains where variable binding is where a lot of the trickiness lies. The nice thing about combinator approaches is that it avoids these issues.
I did not do this, but I note that the composition rule is begging to be tabled (being some relative of a transitive closure rule). If so, and if you want to record proofs, it is interesting to consider answer subsumption SWI-Prolog -- Answer subsumption or mode directed tabling since you probably do not want to record all proofs, only a “best” one (probably the shortest). One could subsumpt on the depth or height of the proof tree, or merely record this depth number for post processing later (a la using dynamic programming to find shortest paths. You do not typically record the path at every node. You record the length of the path and the traverse the table later to reconstruct the actual interesting path in question).This roughly how people record provenance in datalogs Provenance | Soufflé • A Datalog Synthesis Tool for Static Analysis[1907.05045] Provenance for Large-scale Datalog . The DCG method also feels like it becomes inappropriate (?) since you do not want to memoize on the full proof list, just as little of the proof as possible.
I kind of wish you wouldn’t edit away your thought process, because I find it very interesting. You could perhaps just edit to add a “Edit: I don’t think this is right anymore” if you think what you wrote is not correct. That tends to be what I do.
Categorical Logic, logic based on category theory is nice. It challenges
a little bit the notion of a proof, usually conceived as a tree. Was looking
for a library to render Categorical Logic proofs, and found this blog:
But then it occured to me that Cytoscape uses a HTML Canvas, which
I didn’t like. Alternatively you can also use HTML Scalable Vector
Graphics (SVG) and roll your own rendering in 100% pure Prolog.
Here is a rendering of a prove(p /\ q > q /\ p) via SVG:
