# Memoisation for term rewriting system

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.

• Are you using term indexing? If so, why wouldn't a simple (iterative deepening) depth-first search work? – pedagand Jul 5 '19 at 10:23
• 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. Jul 5 '19 at 14:37