Word problems, logic, and regular expressions
Suppose you have a sequence of symbols and a set of rewriting rules for replacing some patterns of symbols with others. Now you're given two such sequences. Can you tell whether there's a way to turn one of them into the other?
This is known as the word problem, and in general it's undecidable. In general the problem cannot be solved by a program, but some instances can. We'll look at a word problem that can be solved with a few regular expressions.
Modal logicBasic modal logic has two symbols, (box") and (diamond"), and concatenations of these symbols. In general, there are infinitely many non-equivalent sequences of boxes and diamonds, depending on the axioms of your modal logic.
In the axiom system S4, every non-empty sequence of boxes and diamonds is equivalent to one of six possibilities:
An arbitrary sequence of boxes and diamonds can be reduced to one of the forms above by applying the following rules:
We can apply the reduction rules above using regular expressions with the following Perl code.
use utf8; $_ = ""; s/+//g; s/+//g; s/()+//g; s/()+//g; print;
The directive use utf8; tells Perl to be prepared for non-ASCII characters, namely boxes and diamonds. In Perl, $_ is the implicit variable; all the following substitution commands will modify this variable, and the print statement will output the final value of this variable.
The first substitution replaces one or more consecutive boxes with one box and the second does the analogous substitution for consecutive diamonds. The third and fourth substitution commands replace repetitions of or with a single instance.
The script above outputs
meaning that
p p
is a theorem in S4.
Word problems can't always be solved using regular expressions, or any other programming technique, but this one could.
Related postsThe post Word problems, logic, and regular expressions first appeared on John D. Cook.