[ivan.moony]

I would expect the state after inference-step to be represented in the same format. Currently, a ForeChain key is added, with the result as an array. This breaks the head/tail format. How do we represent the result of the inference in Implika syntax?

After a few thoughts, a solution may be in populating existing contexts with inference results, thus altering the original expression. This solution suffers from a lack of information about what conclusion came from what node, while this information may be valuable in theorem proving. I think it would be wise to separate conclusions from starting code as it is now, leaving the user possibility to flatten resulting JSON into pure head/tail format in the following way: There may be multiple conclusions from the same node. The solution to this is to replace a `node` with `(node ( result1 ( result2 ( result3 () ) ) ) )` with mandatory dummy at the end because this expression behaves like logical expression `(node -> (result1 -> (result2 -> (result3 -> ()))))`, which translates to `(node /\ result1 /\ result2 /\ result3) -> ()`. A function to make this flattening would take only a dozen lines of code with standard tree traversal and node reassignment.

How do we represent the result of the inference in Implika syntax?

In fact, implika (like logic) has a nice property of being able to detect internal inference. Inference process is homoiconic in implika, if that's the right word to use. For example, we can write `(a b) c` to derive `c` if in the same context may be implicitly derived `b` from `a`, even without explicitly stating `(a b)`. IMHO Logic in general is a true dragon that could be worth of studying even for its own sake, just like mathematics is.

[Zero]

It surely is a dragon! It's hard for me to study. For example, I don't understand yet the difference between material conditional and logical consequence. Logic is an entire world in itself.

The reason behind my question was a hope to build a system where forward chaining can be applied repeatedly, to obtain a tree-shaped cellular automaton, so to speak.

BTW, expressions like (a b c d) associate to the left, may I ask why you did choose left? Expressions like (a (b (c ())) seem to be everywhere...

[ivan.moony]

BTW, expressions like (a b c d) associate to the left, may I ask why you did choose left? Expressions like (a (b (c ())) seem to be everywhere...

Yes, I decided not to follow standards and to associate implications to the left for a reason. It is because `(a (b (c ())))` is commutative (since it is analog to logical conjunction) , while in `((((a) b) c ) d)` the order matters. I predicted that someone might want to construct sequences with more than two elements, and I wanted to avoid writing braces in those cases (i.e. expressions like `select <x> where <y> order by <z>`). I don't know if I made an optimal decision, but it's just a matter of parsing that is external to the library anyway, like in test suite. Internally the algorithm accepts `{head: ..., tail:...}` jsobjects (or alternatively two element arrays processed by `Conv` function) which require explicit grouping. The library itself actually is meant to be used as a bare essential for integrating with bigger projects which may decide their own grouping policy.

By the way, I think I know what to do with hierarchical context relations. It would be just a few more lines of code. I'll try it on Monday.

[ivan.moony]

The reason behind my question was a hope to build a system where forward chaining can be applied repeatedly, to obtain a tree-shaped cellular automaton, so to speak.

It should be already quite possible. For example, this expression never terminates:

Code

(
    (@a (@a + 1)) (
        0 (
        )
    )
)

`(@a (@a + 1))` turns `@a` to `@a + 1`. Then `@a + 1` is fed back to `(@a (@a + 1))` to produce `(@a + 1) + 1`, and the loop is going on forever after applying it to `0`. To terminate it, it is necessary to express a condition under which `@a` becomes `@a + 1`. For example:

Code

(
    ((@a < 10) (@a (@a + 1))) (
        0 (
        )
    )
)

This should loop only 10 times, starting from 0, but it won't work right away. On the first sight, the problem seems that we have to internally code predicate less than and a function of addition. But on the second thought, I believe it is possible to do with implika something like Church encoding with lambda calculus. This is what I only mentioned in the current implika documentation, but I'll try to shed more light on this problem in the next github update. I'll try to provide a simple example of implementing lambda calculus, which is now (without hierarchically related contexts) more complicated, but possible (I believe).

In other words, the above example would work only after defining comparison and addition operations on set of numbers within implika notions. Otherwise (and for a sake of speed performance), these definitions should be added internally by manually altering implika code.

By the way, are you aware of untyped lambda calculus? It possesses a hypnotic simplicity, while it reveals unbound power. It would be wise to take it under consideration as a base language. I plan to do it with etml because I think lambda calculus is simpler than implika, while implika inference automation is not a necessary accessory in raw document production.

[Zero]

Do you plan to introduce macros at some point?

[ivan.moony]

Do you plan to introduce macros at some point?

What kind of macros? I thought every implication is a kind of a macro. A result of a head pattern is a tail pattern, regarding to some rule.

[Zero]

You're right, it's a rewriting system (silly me). I think what's bothering me is having to nest things when I'd like to syntactically juxtapose them. I'm not sure I'm being clear.

[ivan.moony]

Yes, it is a kind of itchy when every bond is a consequence, when we need it, and when we do not. It was bothering me that much that I introduced a space separator aside from implication operators, but it all turned into Esperas, which I'm still developing.

[edit]
I only kept implika because I believe in minimalism.

[ivan.moony]

With introducing hierarchical context relationships, I experienced a major slowdown due to combinatorial interaction between newly drawn conclusions and growing set of assumptions. This new, still unpublished version is slowing down a lot, something like two minutes compile on fifty lines examples.

I don't know, I think I'll abandon this project. Optimization may complicate the code a lot, while code simplicity was one of the key advantages of this project.