[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.

[ivan.moony]

Done some rethinking about service virtual machines, and my framework conceptualization slowly fits into a shape decent enough for implementing: https://svm-suite.github.io/

[ivan.moony]

I had some experiments lately with symbolic algorithm synthesis. I had an input, and I had an output, and I had to clue up how can I brute force combine given rules to transform the input to the output. It works well with a small amount of steps, but eventually combinatorial explosion happens where I get stuck in almost endless loop that may take centuries to finally get an answer.

And that is where neural networks seem to do very good job: to quickly learn how to connect inputs to outputs, memorizing weights for future construction of outputs. Of course, there is an approximation error with neural networks, but given enough learning examples, it may work like a charm.

Basically, the two technologies should do the same thing, but with different advantages and drawbacks. The symbolic one brings certainty but it is slow while the neural one is fast but it brings randomness. Is combining them really the next big thing the world is waiting for?

[ivan.moony]

Assuming that "copy" part would work properly in every iteration, accumulating its interpretation of the "actual Universe", would you dare to run this thing without any constraints?

Code: text

                             the "mirror" algorithm

• • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • •
•                                                                                 •
•                                    I N P U T                                    •
•                                                                                 •
• • • • •  observe  • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • •
              •                                                     ▲
              •                                                     •
              •                                                     •
              •                               • • • • • • • observe •
              ▼                               •                     •
• • • • • • • • • • • • • • •                 •                     •
•                           •                 •                     •
•                           •                 •       • • • • • • • • • • • • • • •
•           CODED           •                 •       •                           •
•          UNIVERSE         • ◄ • • copy  • • •       •      ACTUAL UNIVERSE      •
•           MODEL           •                 •       •                           •
•                           •                 •       • • • • • • • • • • • • • • •
•                           •                 •                     ▲
• • • • • • • • • • • • • • •                 •                     •
              •                               •                     •
              •                               • • • • • • • observe •
              •                                                     •
              •                                                     •
              ▼                                                     •
• • • • •  respond  • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • •
•                                                                                 •
•                                   O U T P U T                                   •
•                                                                                 •
• • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • •

[HS]

Without any constraints I guess you'd get a backup/parallel universe, I'd be hesitant about running that because because of the sheer magnitude of what might happen and all the unknowns I'd be dealing with.

With unavoidable constraints added back, depending on how good the data organization systems were, it might either quickly fill up any available storage space with trivial and redundant information, distill things to their fundamental source code, or end up somewhere in between, much like all the intelligent beings on Earth...

Well, I might have a bias for our level of universe modeling... But like your previous observation suggests, there's often a bell curve with maximal power in the middle. So I wouldn't worry too much if data reorganization was complete or non existent, but mid-level/balanced data sorting might lead to the most complex and unpredictable results.

[ivan.moony]

Hi.

Just stopped by to share some musings. All over the same things, but from different perspective...

LLMs seem like "dream machines". From inside the dreams it is hard to tell the difference between imagination and reality. Likewise, I hear programmers struggle with "hallucination" problems in LLMs.

Symbolic AI I'm interested in just loops over all the possible combinations, and has a method to extract only the ones that match the reality. So it seems like "reality machine"

These two may complement each other, one colorfully dreaming a sense of life, and the other strictly restraining to the sane black and white reality. This synergy reminds me a bit of notions I observe in our brainworks. Who knows, maybe it would be worth to fuse them together. Added to my to-do list to check it out.