It's been a ruff month...
Worked out mostly theoretical aspect of implications and co-implications to get a better understanding of automated reasoner. Now I have theoretical indices that I got it right from the first implementation.
Did a bit of syntax refactoring, corrected the implementation (now it uses exactly the same algorithm - only on negated rules - for backward chaining), and eradicated some bugs. The implementation takes about 350 LOC.
Also made some decisions about the future of the project: I may choose it to be a logic database for programming symbolic AI. I'm also considering bundling it with IDE and system debugger.
project status:
[ ] alpha conception
[x] theorizing
[ ] implementing
[x] parsing input s-exprs
[x] extensional reasoning
[x] pattern matching involving write side disjunctions
[x] non-deterministic matching involving read side conjunctions
[x] non-deterministic matching involving write side disjunctions
[x] pairing input to output
[ ] intensional reasoning
[ ] untyped variables
[ ] typed variables
[ ] free variables
[ ] nested rules
[ ] finalizing tasks
[ ] sane error messages
[ ] packaging executables
[ ] beta testing and revising code
[ ] gamma release
As usual, playground link is here (https://symbolverse.github.io/reasoner.js/playground/).
I did a major refactoring of the main loop. Now the code is a lot cleaner, meaning there should be less bugs. Speed of execution is also improved by a multiple factor. I think the project finally entered the phase when actually it may be fun to play around with. I also added some intriguing examples with binary numbers in the playground.
There is still a lot work to do, but I'm on it. This is the current roadmap:
[ ] alpha conception
[x] theorizing
[ ] implementing
[x] main loop recognizing unrestricted grammars
[x] variables substitution (to do: [ ] unbound variables)
[x] gradual typing (to do: [ ] any depth metarules; [ ] deep variables)
[ ] improved s-expr meta capabilities: mandatory `PAIR` and `LIST`
[ ] non-deterministic sequent matching
[ ] `READ` side conjunction
[ ] `WRITE` side disjunction
[ ] error messages
[ ] stress test
[ ] beta testing and revising code
[ ] gamma release
As usual, there is online playground (https://contrast-zone.github.io/reasoner.js/playground/) and the project home page (https://github.com/contrast-zone/reasoner.js).
So, Reasoner.js would be a virtual device. Console also. Permanent and temporary memory also. This minimal set could be enriched by other devices like sound, vision, ... Note that every device has its input or output, or both.
In between of these devices, there would be a "coordinator". It would be a glue which mediates between devices, receiving messages from source devices and sending them to target devices. A coordinator could be also considered a kind of device.
There could be many coordinators, and each coordinator code would follow this pattern:
(
COORDINATE
(
CONDUCT
(
EVENTS
(RECEIVE (SOURCE ...) (DATA ...))
...
)
(
ACTIONS
(SEND (TARGET ...) (DATA ...))
...
)
)
...
)
The coordinator is a set of conductors that listens to device events and conducts related actions to devices.
The problem solved by coordinator is very important one: managing states. Managing states is needed when, for example, we want to change memory contents as inputs flow in. Code written in Reasoner.js is just a static conglomerate of referentially transparent functions, and if we would be solving states in Reasoner.js, we would have to deal with monads or other gimmicks I am not a big fan of. Other than that, it was also taken under consideration making a separate finite state machine for managing states. But it turned out we don't need anything else than the coordinator between devices which, internally, do or don't manage states.
So, when we want to receive a message from, say, console source, we listen from coordinator to console input event. Then, if we want to process the console input, we pair that event to an action of calling Reasoner.js target code, passing the console input as a parameter, and listening for a result message. The resulting message may raise a new event coupled with an action of sending the data to memory device. By the same event we may also want to write something back to console. To do that, we can put another action for it, next to the action of memorizing data. The whole cycle could repeat on every console input event. Maybe some other arbitrary device events could be also shown useful, like custom reminders, timers, attention requests, ...
With the coordinator I saved myself a bit of a trouble of writing a finite state machine which would be more complicated than implementing the coordinator listening and talking to different devices. It would be up to devices how to manage states. Less is better, right? Especially if there are no functionality trade offs.
[EDIT]
After some research, I discovered that what I'm planning to implement is exactly well known service oriented programming (SOP (https://en.wikipedia.org/wiki/Service-oriented_programming)) paradigm. Good to know. What I call "device", it is called "service" in SOP. I'll align my terminology with SOP terminology. Nevertheless, the process between receiving and sending messages in SOP reminds me very much of term rewriting. Actually it's exactly term rewriting if we are sending and receiving messages from and to the same coordinator/router. I plan to use here the same "variable" notion from reasoner.js, of course, but without nondeterminism.