Formally Verify if a Sequence of Regex-Based Modifications is Idempotent

Question

I'm performing a sequence of text formatting using regex in Python.

I'm curious to know if it's possible to formally verify whether a single (or a sequence of) regex modification(s) is idempotent, which means that for every text, d ∘ d (text) = d (text), where d denotes the resulting total modification.

To be precise, by a single regex modification, I refer to the function f_regex_subst: text |-> re.sub(regex, sub, text, 0, re.MULTILINE). When a sequence of such modifications is applied, the resulting function is simply the composition of these functions.

The motivation is ensuring the formatting process yields stable result for any text.

Answer 1

This is likely to be a very hard problem, so hard that I don't think you should expect a useful solution that can handle all possible regexes.

The extended regular expressions supported by Python's re.sub are very expressive and powerful, which makes the verification problems involving them very hard. These advanced features (backreferences, capture groups, lookahead, lookbehind, etc.) make these regexes very expressive. For instance, it is known that the problem of testing whether a string matches a regex (that might contain backreferences) is NP-complete. As another example, it is known that testing equivalence of two such regexes is undecidable, as is testing whether such a regex matches every string, or testing whether such a regex matches a regular language. For proofs, see the following paper:

Extended Regular Expressions: Succinctness and Decidability. Dominik D. Freydenberger. Theory of Computing Systems, vol 53, pp.159-193, 2013.

The takeaway is that verification problems involving this type of regex tend to be very hard. I don't know of anyone who have studied idempotency of a sequence of re.sub operations, but I would imagine that likely it is also very hard... possibly also undecidable.

I would suggest that you figure out what your actual goals are, and then see if you can find some alternative approach to achieve your real goals. Perhaps you only need to reason about a subset of regexes (e.g., only those that can be represented by a finite-state machine / regular transducer)? Perhaps it suffices to use testing to check idempotency, without having any formal guarantees? Perhaps you can find a way to structure your code so you don't need to verify this property? It is hard to know, without more context.

See also https://cstheory.stackexchange.com/q/448/5038, https://www.npopov.com/2012/06/15/The-true-power-of-regular-expressions.html, Which languages do Perl-compatible regular expressions recognize?, What is the computational complexity of "real-life" regular expressions?.