Turing completeness of string_concat about modus HOT 4 CLOSED

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

from modus.

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.

from modus.

@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?

from modus.

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

from modus.