<p>I have a  (word) Term Rewriting System (TRS in short) and I want to check for a simple accessibility condition. </p>

<p>In symbols, let <span class="math-container">$\Sigma$</span> be a finite alphabet. For <span class="math-container">$a\in \Sigma$</span>, and any words <span class="math-container">$u,v,w \in \Sigma^*$</span>, then my rewriting system is simply: <span class="math-container">$(au,vaw)\to (uv, w)$</span>.</p>

<p>Starting from arbitrary configuration, I am searching for accessibility of <em>Identity</em>, that is, if for two words <span class="math-container">$u,v\in \Sigma^*$</span>, I check if there exists <span class="math-container">$w$</span> such that <span class="math-container">$(u,v)\to^*(w,w)$</span> where <span class="math-container">$\to^*$</span> denote the transitive closure of <span class="math-container">$\to$</span>. </p>

<p>The configuration space is exponential (the accessibility problem itself is NP-complete). I would like to add some memoisation policy for the non valid configurations met so far during the exploration. I can design an ad-hoc and specialized one but after some naive tries, it turns out to be more intricate.</p>

<p>To be slightly more precise, I am looking for proper data-structure to store the intermediate results. Simply caching the result of a configuration (pairs of string) is not efficient since there are many configurations that can be proved derived to be non valid with one non valid configurations. Furthermore, the efficiency of the naive caching highly depends on the exploration strategy and understanding that is already difficult to me.</p>

<p>It seems to me that it is a quiet natural question when one is trying to explore the derivation space of TRS, and I would suspect that some literature already exists on the subject, although I fail to find one in classical books and by duckduckgoing it rapidly. </p>

CC BY-SA 4.0
2019-07-05T10:23:38.727Z
Are you using [term indexing](https://en.wikipedia.org/wiki/Term_indexing)? If so, why wouldn't a simple (iterative deepening) depth-first search work?
pedagand
CC BY-SA 4.0
2019-07-05T14:37:42.383Z
Term indexing is indeed what I am looking for. The depth first search can have good or bad indexed performance depending on the order of application of the rewriting rules. I don't really understand that well.
C.P.
<term-rewriting-systems>
Memoisation for term rewriting system
C.P.
# Memoisation for term rewriting system

(Asked by: username_0 on 2019-07-05)

I have a (word) Term Rewriting System (TRS in short) and I want to check for a simple accessibility condition.

In symbols, let $\Sigma$ be a finite alphabet. For $a\in \Sigma$, and any words $u,v,w \in \Sigma^\*$, then my rewriting system is simply: $(au,vaw)\to (uv, w)$.

Starting from arbitrary configuration, I am searching for accessibility of *Identity*, that is, if for two words $u,v\in \Sigma^\*$, I check if there exists $w$ such that $(u,v)\to^\*(w,w)$ where $\to^\*$ denote the transitive closure of $\to$.

The configuration space is exponential (the accessibility problem itself is NP-complete). I would like to add some memoisation policy for the non valid configurations met so far during the exploration. I can design an ad-hoc and specialized one but after some naive tries, it turns out to be more intricate.

To be slightly more precise, I am looking for proper data-structure to store the intermediate results. Simply caching the result of a configuration (pairs of string) is not efficient since there are many configurations that can be proved derived to be non valid with one non valid configurations. Furthermore, the efficiency of the naive caching highly depends on the exploration strategy and understanding that is already difficult to me.

It seems to me that it is a quiet natural question when one is trying to explore the derivation space of TRS, and I would suspect that some literature already exists on the subject, although I fail to find one in classical books and by duckduckgoing it rapidly.

**Tags:** term-rewriting-systems

> **Comments:**
> **username_1**: Are you using [term indexing](https://en.wikipedia.org/wiki/Term_indexing)? If so, why wouldn't a simple (iterative deepening) depth-first search work?  
> **username_0**: Term indexing is indeed what I am looking for. The depth first search can have good or bad indexed performance depending on the order of application of the rewriting rules. I don't really understand that well.  

---

## 0 answers

