Turing completeness of string_concat

[maowtm]

I've been playing around with this for a bit since we basically have all the core datalog logic stuff ready, and I made this thing:

output(S) :- run(S).
entry(S) :- anbncn(S), output("Accept!").

anbncn("") :- .
anbncn(S) :- abc_split(S, A, B, C), streq(A, B), streq(B, C).
streq(A, B) :- string_concat("", A, B).
charne("a", "b").
charne("a", "c").
charne("b", "c").
charne(A, B) :- charne(B, A).
abc_split(S, A, B, C) :-
    count_chars(S, "a", A, BC),
    count_chars(BC, "b", B, CC),
    count_chars(CC, "c", C, "").

# normal route
count_chars(S, C, O, R) :-
    string_concat(C, RR, S),
    count_chars(RR, C, O2, R),
    string_concat("1", O2, O).
# other char
count_chars(S, C, O, R) :-
    charne(C, C1),
    string_concat(C1, RR, S),
    streq(O, ""),
    streq(R, S).
# empty case
count_chars("", C, O, R) :-
    streq(C, C),
    streq(O, ""),
    streq(R, "").

The same strategy can be used to turn any turing machine into a modus program that takes entry(S) for some string S, and output a docker image iff TM accept (just use the string as a tape, have something like TM(q, tape_left, tape_current, tape_right)). This means that the claim that this language is not Turing complete in the doc repo is actually false.

[maowtm]

Note that for the purpose of this experiment I have temporarily increased the depth limit to 100, otherwise it fails aaabbbccc. I'm not sure exactly what the consequence of this proof is, but I guess maybe we can't really reliably determine a limit after all.

[mechtaev]

@maowtm, this is cool, thank you for the demonstration. a^n b^n c^n is not context-free, but why does it prove that Modus is Turing complete? Can you please elaborate?

[maowtm]

Closing - we have decided earlier to not allow string_concat to appear in rules which can have recursion on itself.

[maowtm]

A bit of fun before we disallow recursive string_concat:
https://play.modus-continens.com/#%7B%22q%22%3A%22mul(%5C%2211%5C%22%2C%20%5C%221101%5C%22%2C%20R)%22%2C%22m%22%3A%22add(%5C%22%5C%22%2C%20%5C%22%5C%22%2C%20%5C%22%5C%22).%5Cnadd(%5C%22%5C%22%2C%20X%2C%20X)%20%3A-%20X%20%3D%20X.%5Cnadd(X%2C%20%5C%22%5C%22%2C%20X)%20%3A-%20X%20%3D%20X.%5Cn%5Cnadd(X%2C%20Y%2C%20R)%20%3A-%5Cn%20%20string_concat(Xrest%2C%20%5C%220%5C%22%2C%20X)%2C%5Cn%20%20string_concat(Yrest%2C%20%5C%220%5C%22%2C%20Y)%2C%5Cn%20%20string_concat(Rrest%2C%20%5C%220%5C%22%2C%20R)%2C%5Cn%20%20add(Xrest%2C%20Yrest%2C%20Rrest).%5Cn%5Cnadd(X%2C%20Y%2C%20R)%20%3A-%5Cn%20%20string_concat(Xrest%2C%20%5C%221%5C%22%2C%20X)%2C%5Cn%20%20string_concat(Yrest%2C%20%5C%220%5C%22%2C%20Y)%2C%5Cn%20%20string_concat(Rrest%2C%20%5C%221%5C%22%2C%20R)%2C%5Cn%5Cn%20%20add(Xrest%2C%20Yrest%2C%20Rrest).%5Cn%5Cnadd(X%2C%20Y%2C%20R)%20%3A-%5Cn%20%20string_concat(Xrest%2C%20%5C%220%5C%22%2C%20X)%2C%5Cn%20%20string_concat(Yrest%2C%20%5C%221%5C%22%2C%20Y)%2C%5Cn%20%20string_concat(Rrest%2C%20%5C%221%5C%22%2C%20R)%2C%5Cn%20%20add(Xrest%2C%20Yrest%2C%20Rrest).%5Cn%5Cnadd(X%2C%20Y%2C%20R)%20%3A-%5Cn%20%20string_concat(Xrest%2C%20%5C%221%5C%22%2C%20X)%2C%5Cn%20%20string_concat(Yrest%2C%20%5C%221%5C%22%2C%20Y)%2C%5Cn%20%20string_concat(Rrestinc%2C%20%5C%220%5C%22%2C%20R)%2C%5Cn%20%20add(Xrest%2C%20Yrest%2C%20Rrest)%2C%5Cn%20%20inc(Rrest%2C%20Rrestinc).%5Cn%5Cninc(%5C%22%5C%22%2C%20%5C%221%5C%22).%5Cninc(%5C%220%5C%22%2C%20%5C%221%5C%22).%5Cninc(X%2C%20R)%20%3A-%5Cn%20%20string_concat(Xrest%2C%20%5C%220%5C%22%2C%20X)%2C%5Cn%20%20R%20%3D%20f%5C%22%24%7BXrest%7D1%5C%22.%5Cn%5Cninc(X%2C%20R)%20%3A-%5Cn%20%20string_concat(Xrest%2C%20%5C%221%5C%22%2C%20X)%2C%5Cn%20%20string_concat(Xrestinc%2C%20%5C%220%5C%22%2C%20R)%2C%5Cn%20%20inc(Xrest%2C%20Xrestinc).%5Cn%5Cnmul(X%2C%20%5C%22%5C%22%2C%20%5C%220%5C%22).%5Cnmul(%5C%22%5C%22%2C%20X%2C%20%5C%220%5C%22).%5Cnmul(X%2C%20%5C%220%5C%22%2C%20%5C%220%5C%22).%5Cnmul(%5C%220%5C%22%2C%20X%2C%20%5C%220%5C%22).%5Cn%5Cnmul(X%2C%20%5C%221%5C%22%2C%20X)%20%3A-%20X%20%3D%20X.%5Cnmul(%5C%221%5C%22%2C%20X%2C%20X)%20%3A-%20X%20%3D%20X.%5Cn%5Cnmul(Xinc%2C%20Y%2C%20R)%20%3A-%5Cn%20%20inc(X%2C%20Xinc)%2C%5Cn%20%20mul(X%2C%20Y%2C%20RlessY)%2C%5Cn%20%20add(RlessY%2C%20Y%2C%20R).%5Cn%5Cn%23%20definition%20for%20inc%20that%20allows%20inc(-x%2C%20%2By)%20(i.e.%20decrement)%5Cn%5Cninc(XlessOne%2C%20X)%20%3A-%5Cn%20%20string_concat(Xrest%2C%20%5C%221%5C%22%2C%20X)%2C%5Cn%20%20XlessOne%20%3D%20f%5C%22%24%7BXrest%7D0%5C%22.%5Cn%5Cninc(XlessOne%2C%20X)%20%3A-%5Cn%20%20string_concat(Xrest%2C%20%5C%220%5C%22%2C%20X)%2C%5Cn%20%20XlessOne%20%3D%20f%5C%22%24%7BXrestLessOne%7D1%5C%22%2C%5Cn%20%20inc(XrestLessOne%2C%20Xrest).%22%7D