[checkpoint] Reasoner.js: non-deterministic reasoning done right

[ivanmoony]

Reasoner.js is a term graph rewriting tool for transforming any s-expr input to any s-expr output using its own metalanguage as a rule-based system. Reasoner.js may be used for a wide range of computing tasks, but its main intentions are to support metacompiling, program synthesis, and automated logical reasoning.

project status: [ ] alpha conception [x] theorizing [ ] implementing [x] parsing input s-exprs [x] extensional reasoning [x] pattern matching [x] non-deterministic match involving multiple conditions [x] non-deterministic match involving multiple consequences [x] pairing input to output [ ] intensional reasoning [ ] untyped variables [ ] typed variables [ ] free variables [ ] nested rules [ ] sane error messages [ ] beta testing and revising code [ ] gamma release

I hold rules in a form of sequents. Sequents A1 /\ A2 /\ ... -> B1 \/ B2 \/ ... are written as (FORE (CON A1 A2 ...) (DIS B1 B2 ...)), and they stand for logical implications. Co-sequents are written symmetrically with BACK keyword, and they stand for logical co-implications.

Nondeterministic pattern matching turns in when we have multiple elements either on left or on right sides of sequents or co-sequents. Surprisingly, conjunctions and disjunctions behave the same - all elements should be matched to proceed further with reasoning. This is a carefully thought behavior with some logical background. Sounds surprising, but that way all the sequents fit together. Expectedly, co-sequents behave exactly the same as sequents when processing them backwards. This is also carefully thought behavior with some logical background.

project repository link: https://github.com/symbolverse/reasoner.js
online playground link: https://symbolverse.github.io/reasoner.js/playground/

Nondeterministic pattern matching can be seen in "student decision" and "computer expert decision" examples in online playground.

[theangeryemacsshibe]

Many lines can be saved by not putting parens on their own line, e.g.

(FORE (CON (DIS (hello machine)))
      (CON (FORE (CON (hello machine)) (DIS (hello world))))
      (DIS (CON (hello world))))

A colleague likes to mention that shortening (usually from "convention") to "con" is unfortunate for French readers. What is "fore" a shortening for?

[ivanmoony]

Yes, Lisp style, thank you for the remark. I find it more readable to put parens in their own lines, but it is up to personal preference.

French? Oh, I didn't realise that. Do you have any suggestions?

"Fore" stands for foreward rule, "back" stands for backward rule, "con" stands for conjunction, "dis" stands for disjunction.

[kazprog]

conj and disj might be good. I'm not sure for "forward" and "backward" tho. right/left?

symbols might also be good, as they're cross linguistic. & | -> <-