# Allow match-branching and concurrent-match in Regular Expressions

**URL:** <https://es.discourse.group/t/allow-match-branching-and-concurrent-match-in-regular-expressions/504>\
**Category:** 💡 Ideas\
**Tags:** proposal\
**Created:** [October 18, 2020, 6:08am UTC](https://es.discourse.group/t/allow-match-branching-and-concurrent-match-in-regular-expressions/504 "2020-10-18T06:08:11Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![Seagat2011](https://yyz2.discourse-cdn.com/free1/user_avatar/es.discourse.group/seagat2011/32/367_2.png) [@Seagat2011](https://es.discourse.group/u/Seagat2011)\
**Post date:** [October 18, 2020, 6:08am UTC](https://es.discourse.group/t/allow-match-branching-and-concurrent-match-in-regular-expressions/504/1 "2020-10-18T06:08:11Z")

</div>

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

```javascript
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

```javascript
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

1. string matching requires a bi-directional match option!

```javascript
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", )

1. string matching requires an option to match in a concurrent manner!

```javascript
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

1. string matching requires an option to match recursively, and or indefinitely!

```javascript
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

1. 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!