I wish to use strings, and string substitutions, to implement a theorem prover
This would allow me to implement a full-fledged (symbolic) theorem prover using only a few lines of code
Given the following string composed of axioms
let a = "1 + 1 = 2 | 2 + 2 = 4 | 1 + 1 + 2 = 4"
I wish to use the first- and second axioms to prove the third by
string replace and expanding on both ends to obtain the following (inline) result
a = "| 1 + 1 + 1 + 1 = 1 + 1 + 1 + 1"
However, this is not possible, via current inline find-/replace-/match string substitution methods
I encounter the following issues
- string matching requires a bi-directional match option!
let a = "1 + 1 = 2 | 2 + 2 = 4 | 1 + 1 + 2 = 4"
Once the RE engine encounters "1 + 1" match, it cannot be called again to evaluate the new sub expression ( to obtain "| 2 + 2 = 4 | 2 + 2 = 4", )
- string matching requires an option to match in a concurrent manner!
let a = "1 + 0 = 1 | 0 + 0 = 0 | 0 + 1 + 0 + 0 = 1"
In the above example, string match could employ the second axiom replace indefinitely! This replace method is required yet it yields a non-determinism,
which can be cured if the replace instead spawns branches which can be evaluated in a concurrent (parallel?) manner
- string matching requires an option to match recursively, and or indefinitely!
let a = "1 + 1 = 2 | 2 + 2 = 4 | 0 + 0 = 0 | 1 + 1 + 2 = 4 + 0 + 0"
In the above example, the use of a replace callback ultimately fails because subsequent matching would not branch concurrently and as a result go deep enough to reach the available solution, which occurs in an isolated branch
- String.search, String.find, String.replace should return a (more) flexible list!
Because of the aforementioned limitations, the above methods currently return incomplete or incompatible lists for recursive use
My theorem prover library currently employs symbolic substitution
Implementing a full-fledged symbolic prover using inline string match would allow me to reduce my entire library to only a few lines of code!