[ivan.moony]

the idea

Experimentation with different custom made programming languages related to theorem proving has been one of my interests for a long time. Why theorem proving? Because it seemed like a logical step towards AI. In a meanwhile, deep learning ANNs (artificial neural networks) took over the world, and it could be a good thing. Similarity between an ANN and a theorem prover is that the starting point and ending result are the same in both cases, but the process in between is different. ANN utilizes pretty obscure weighted graph connecting input and output while theorem proving (in cases I'm considering) utilizes potentially human readable set of constructive theorems that need to be combined to connect input to output.

The theorem proving is still an area of my interest, but with addition of one missing link that ANNs seem to do pretty well (or at least in some extent). ANNs use the nowdays-all-present deep learning techniques to automatically form the connections between input and output. Analogously, the link I'm trying to explore is an alternative to deep learning in a form of automated semi-axiom construction. Here, I'm making a distinction between theorem proving and semi-axiom construction. In theorem proving, axioms need to be manually fed into the system to be used in further automated theorem construction. In semi-axiom construction, I'm seeking for a way to automatically construct semi-axioms, with semi-axioms being both axioms or theorems.

Googling around the web about this process (in 2022) gives somewhat rare and specialized results, so the space for a progress may be opened. I believe that appropriate term for the process I'm trying to explore could be "generalized theory synthesis". There are already some achievements on this process in a form of algorithm synthesis, and that is exactly direction I'm trying to head at, only applied also to theorems.

To finally explore the blurry cloud of theory synthesis and to see it in more focused features, the plan would be to fuse a selection of my existing languages, and present them in gradual form under the same language named Tricosm. The language should be applicable to theory synthesis, as well as to algorithm synthesis. In a simple example, from provided data:

input -> output
---------------
    2 -> 4
    4 -> 8
    8 -> 16
   16 -> 32

one of the generated theories (given that we already know how to handle integers and multiplication) would be:

input -> output
---------------
    x -> 2 * x

implementation

Co-rewrite takes an input file, an arbitrary metaprogram, and constructs an output file from the input file using the metaprogram. The metaprogram is actually a set of formulas similar to those in math science with the difference that the Co-rewrite formulas may transform not only math expressions, but also any kind of language expression.

It is possible to feed to Systelog a formula in a form of f(program(input) -> output) -> program where function program is being automatically constructed and returned by higher order function f, provided that we know what input -> output mappings hold.

The language goals are having minimal design, beginner friendly documentation, conveniently generating completely functional executable, multiplatform development environment, multiplatform runtime environment, and self hosting compiler.
progress

In this thread I plan to keep a log about the progress in programming the Systelog language for which I plan to be open sourced and hosted publicly on GitHub. Of course, I'd be delighted to hear any comments or to answer any questions in the same thread.

Project homepage is at : https://github.com/contrast-zone/co-rewrite

[MagnusWootton]

You need to write your autobiography and call it  "I, Ivan."   

[ivan.moony]

You need to write your autobiography and call it  "I, Ivan."   

I think more appropriate title would be: "A highway to madness". 

[ivan.moony]

I decided to do some cleanup of this project for the end of the year (I believe feng shui would recommend this at this time of year for attracting a success - not that I'm a fanatic of feng shui, but anyway... it says that dust slows down energy flow, and this is a kind of de-dusting, plus winter should be a great time for new beginnings).

I renamed the project to Tricosm  and created a nice logo:



Also did a set up of a new GitHub organization to keep all the details of this long term hobby project: https://github.com/tricosm

Worked out some implementation details (see updates of "implementation" section at the top post), and made some targeting audience decisions.

This would be a new general project outline from the Tricosm home page:

• description: AST transformation metalanguage featuring a novel graph rewriting method
• practical use: theorem proving, program synthesis, metacompiling
• status: work in progress - it's not completely engineering work; it's not completely academic work; it's something in between.

As always, looking forward for suggestions, comments, questions, and discussions

And happy New Year everyone!

[HS]

Happy New Year, Ivan!

[ivan.moony]

I renamed the project once again to: Systemath, and changed some design decisions. I hope this is it for a while. Seems no one is running a project with the same name on the web.

I'm about to update corresponding working draft.

[ivan.moony]

Working draft is updated, but expect some changes during further development.

Programming tasks done:

• parsing input s-exprs
• pattern matching with basic input
• non-deterministic reasoning
• pairing input to output

About half way to finished product, check out new updates at: https://github.com/contrast-zone/co-rewrite.

Direct playground link is here: https://contrast-zone.github.io/co-rewrite/playground/. Choose an example, pass an input, and watch it being paired to relevant output. Provided examples are covered up to extensional reasoning.

[MagnusWootton]

So with this theorem proving,   its about the robot building a working model of its environment!

So it needs to know,  "Is this theorem a part of where I live, or is it not?"

But how exactly are u getting this mechanism to actually happen with the computer causing it,  thats where ur talent is coming in!

[ivan.moony]

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.

Code: text

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.

[ivan.moony]

Been busy with my other project and making a new web page for my mother's business last month, but finally recently returned to reasoner.js to deal with variables. I thought it would be a two-working-days-solution, but I stumbled upon problems with combining variables with nondeterministic reasoning. The proof structure ramifies, and I know it has to join back somewhere, but tracking it becomes a nearly debugging hell. I based my algorithm on some optimizations not caring about back propagating variables, and now the algorithm chokes. I have to be an Einstein to fix it the right way, and I'm not the Einstein. Serves me right, when I program without planning, but who would plan that far, I had to start with something...

Anyway, the playground of what is finished is here (and it works "somehow" - still would be some things to fix), but I lean towards entirely resetting the project and start fresh. This would be my second project reset (since I'm counting in logs), but I feel like I have new ideas that I just have to implement from the start. The code now has more than 400 LOC, and I can't gather my thoughts around it, so I'll probably try to make it simpler, if not shorter if I opt for another reset.



Those were some bad news, but that's not all to report. Before programming I was paying a bit attention to the future promotion. Check out my new promo page to see if you like it. I have a new logo too. Not much, and maybe a bad timing, but it had to be done at some point in time. It may be useful later.

[WriterOfMinds]

Sometimes you just have to learn what the obstacles are by going ahead and trying to do something. Maybe it feels like wasted time (I know, I hate it when stuff like this happens to me), but it's really a step on the way.

[ivan.moony]

I'm not giving up: https://symbolverse.github.io/

[ivan.moony]

All right, taking a new approach. I'm inventing algorithm similar to those for parsing CFG, but only I want also to support unrestricted grammars, left side conjunctions and right side disjunctions, and variables. This would take some time in a matter of weeks, but this time I'm planning it all ahead not to fall into the same trap like from the last few days. Mitigating circumstance is that I'm not doing the full parser of flat text, yet verifier of ready-made AST in a form of s-exprs. I'm doing it on paper first, and when it's finished, I move onto programming. Result I'm hoping for? Constructive deductive system.

[ivan.moony]

Project reset done. Reprogrammed it to functionality that I had in previous version, but this time I have an idea how to proceed with variables. Postponed nondeterministic reasoning for later. Crux code size reduced from ~160 LOC to ~70 LOC.

[ivan.moony]

So far, so good, variables should more-or-less work. Here: https://mind-child.github.io/reasoner.js/playground/. Sure there are bugs I don't know about, but the further examples battery should do the job.

Not sure what to do with nondeterministic conjunctions and disjunctions. I left it for later, but... the thing is already Turing complete. Dunno... I might make that nondeterministic effort if it is not too complicated to implement. I try to cherish a minimalistic approach, so... maybe.