[ivan.moony]

Reasoner.js just got gradual typing

Reasoner.js is a conceptual term graph rewriting system I'm developing for a while now. It specifically takes an s-expr input (may be AST or other data), transforms the input, and outputs another s-expr (again may be AST or something else).

Until now, (1st step) input would be validated against grammar specifying input type, and output would be constructed (2nd step) from grammar specifying output type with additional transformation rules abducing backwards the inference line.

In this iteration, I separated transformation rules from output rules while input kept the same treatment. So now it does: (1st step) validating input forwards, (2nd step) applying transformation rules, and (3rd step) validating output backwards. All steps are performed using the same AST processing algorithm, changing only input, output, and direction parameters.

This separation enabled isolating the step of applying transformation rules from initially imbued output type checking, labelling the project as gradually typed system.

There is still some interesting work to do like non-deterministic inference with left side conjunctions and right side disjunctions, which would place this system side-by-side with Hilbert calculus, natural deduction calculus, and sequent calculus.

Nevertheless, already implemented functionality provides possibilities for many interesting definitions like rudimentary equality predicate implementation, branching choice decision, Boolean calculator, and a lot more since the internal AST processing algorithm is already Turing complete.

This iteration also provides rudimentary insight to AST construction path which will be advanced to simplified proof elaboration in the future versions.

So, things go on bit by bit, and I'm slowly approaching the production version, hoping to be finally used by hobby programmers researching and fastly prototyping custom formal systems.

To check out the current project iteration, please refer to online playground and the project home page.

[ivan.moony]

I took a break and invested some time in the future PR. This would be the new PR site: https://mind-child.github.io/.

I hope to offer a dream about building a true AI. I'd like users to invest enough effort in their creation to be able to finally say "I built it", or at least "I raised it". I believe that feeling they'd have after doing it would be worth of the effort. I'll try to do my best to provide them a solid foundations to create upon.

And I've got a cute new logo, look:

[ivan.moony]

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:

Code: text

    [ ] 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 and the project home page.

[ivan.moony]

Done more bug fixing, cleaning and refactoring to enter the new year fresh and clean. The code is another 2x faster now, and some important tests pas now, like, for example, proof checking. The speed is overall a lot slower than in initial rewrite.js experiment from a year and so ago, but I hope to justify that by open doors for additional features like type checking and nondeterminism which will be crucial in later automated theorem proving.

As for proof checking, there is a new example in the project playground. Consider each function as a rule, and function applications as proof steps. Function parameters take assumptions, and function result represents consequence. With stacking a proper beginning set of assumptions to function parameters, and composing such functions, the whole system conflue to the final proved theorem while the computing lines from starts to end represent the proof. For this occasion, I constructed a proof for De Morgan's law applied to logic instead of sets, and this proof check, fortunately, runs almost instantly. Automated proving is yet to be seen, but I hope the speed would be in acceptable range. The goal is that it should be at least faster than doing proofs by hand with pen and paper.

And not to forget, merry Christmas to everyone  .

[ivan.moony]

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:

Code: text

(
    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) 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.

[ivan.moony]

Something more from me writing things down and clearing up my thoughts. Read the almost finished paper here if you have the patience. Expect some serious stuff about functional-logic typing rules.