On Regular Expression Proof Complexity of Salomaa’s Axiom System $$F_1$$

Simon Beier¹⁰ &
Markus Holzer¹⁰

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14660))

224 Accesses

Abstract

We investigate the proof complexity of Salomaa’s axiom system $F_1$ for regular expression equivalence. We show that for two regular expression E and F over the alphabet $\varSigma $ with $L(E)=L(F)$ an equivalence proof of length at most $O\left( |\varSigma |^4\cdot \textsc {Tower}(\max \{h(E),h(F)\}+4)\right) $ can be derived within $F_1$, where h(E) (h(F), respectively) refers to the height of E (F, respectively) and the tower function is defined as $\textsc {Tower}(1)=2$ and $\textsc {Tower}(k+1)=2^{\textsc {Tower}(k)}$, for $k\ge 1$. In other words

It is well known that regular expression equivalence admits exponential proof length if not restricted to the axiom system $F_1$. From the theoretical point of view the exponential proof length seems to be best possible, because we show that regular expression equivalence admits a polynomial bounded proof if and only if ${\textsf{NP}}={\textsf{PSPACE}}$.

This paper is a completely revised and expanded version of the paper “On Regular Expression Proof Complexity” presented at the 21st International Conference Developments in Language Theory (DLT) held in Liège, Belgium, August 7–11, 2017.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic

£29.99 /Month

Get 10 units per month
Download Article/Chapter or eBook
1 Unit = 1 Article or 1 Chapter
Cancel anytime

Buy Now

Chapter: GBP 19.95; Price includes VAT (United Kingdom)

eBook: GBP 89.99; Price includes VAT (United Kingdom)

Softcover Book: GBP 109.99; Price includes VAT (United Kingdom)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

A Proof Theory of ( $$\omega $$ -)Context-Free Languages, via Non-wellfounded Proofs

Analysis of an Efficient Reduction Algorithm for Random Regular Expressions Based on Universality Detection

Derivation-Graph-Based Characterizations of Decidable Existential Rule Sets

Notes

1.
For convenience, parentheses in regular expressions are sometimes omitted and the concatenation is simply written as juxtaposition. The priority of operators is specified in the usual fashion: concatenation is performed before union, and star before both product and union.
2.
The notation $(E_1,E_2)\equiv (F_1,F_2)$, for regular expressions $E_1,E_2,F_1,F_2$, stands for $E_1\equiv F_1$ and $E_2\equiv F_2$. The equation $(E_1,E_2)=(F_1,F_2)$ is a shorthand notation for the system of the two equations $E_1=F_1$ and $E_2=F_2$. Furthermore, the expressions $(E_1,E_2)+(F_1,F_2)$ and $(E_1,E_2)\cdot F_1$ define $(E_1+F_1,E_2+F_2)$ and $(E_1\cdot F_1,E_2\cdot F_1)$, respectively.

References

Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. In: Mathematical Theory of Automata. MRI Symposia Series, vol. 12, pp. 529–561. Polytechnic Press, New York (1962)
Google Scholar
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symbol. Logic 44(1), 36–50 (1979)
Article MathSciNet Google Scholar
Ginzburg, A.: A procedure of checking equality of regular expressions. J. ACM 14(2), 355–362 (1967)
Article Google Scholar
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979)
Google Scholar
Hunt, H.B., III., Rosenkrantz, D.J., Szymanski, T.G.: On the equivalence, containment, and covering problems for the regular and context-free languages. J. Comput. System Sci. 12, 222–268 (1976)
Article MathSciNet Google Scholar
Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies. Annals of Mathematics Studies, vol. 34, pp. 2–42. Princeton University Press (1956)
Google Scholar
McNaughton, R., Yamada, H.: Regular expressions and state graphs for automata. IRE Trans. Electron. Comput. EC-9(1), 39–47 (1960)
Google Scholar
Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158–169 (1966)
Article MathSciNet Google Scholar
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proceedings of the 5th Symposium on Theory of Computing, pp. 1–9 (1973)
Google Scholar

Download references

Acknowledgement

Thanks to Christian Rauch for reading a preliminary version of this paper and for his useful comments.

Author information

Authors and Affiliations

Institut für Informatik, Universität Giessen, Arndtstr. 2, 35392, Giessen, Germany
Simon Beier & Markus Holzer

Authors

Simon Beier
View author publications
You can also search for this author in PubMed Google Scholar
Markus Holzer
View author publications
You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Markus Holzer .

Editor information

Editors and Affiliations

University of Oxford, Oxford, UK
Stefan Kiefer
Masaryk University, Brno, Czech Republic
Jan Křetínský
Masaryk University, Brno, Czech Republic
Antonín Kučera

Appendix

Here we give a more elaborated example of a derivation in the axiom system $F_1$.

Example 22

We have $L(a^*)=\{a\}^*=L({a^*}^*)$. To illustrate the previous definitions we show that the equation $a^*={a^*}^*$ is derivable in $F_1$. Axiom $A_6$ gives us ${a^*}^*+{a^*}^*={a^*}^*$. With rule $R_1$ we get

Axiom $A_{10}$ gives us $a^*=0^*+a^*a$ and $R_1$ leads to

Because of Axiom $A_{11}$ we have $(a^*a)^*=(0^*+a^*a)^*$. So with $R_1$ we get

Another use of $R_1$ gives us

Axiom $A_{10}$ leads to $(a^*a)^*=0^*+(a^*a)^*(a^*a)$ and $R_1$ implies

With one more use of $R_1$ we have

(14)

Axiom $A_2$ gives us ${a^*}^*(a^*a)=({a^*}^*a^*)a$. With $R_1$ we get

(15)

We use $A_6$ and $R_1$ again:

Because of Axiom $A_{10}$ we have $a^*=0^*+a^*a$. Now $R_1$ leads to

Axiom $A_5$ tells us ${a^*}^*(0^*+a^*a)={a^*}^*\cdot 0^*+{a^*}^*(a^*a)$. So with $R_1$ we get

We will show in Lemma 3 that the equation ${a^*}^*\cdot 0^*={a^*}^*$ is derivable with eleven uses of $R_1$ and two uses of $R_2$. Having this equation, rule $R_1$ shows

From (14) we have $0^*+{a^*}^*(a^*a)={a^*}^*$. Rule $R_1$ gives

Another use of $R_1$ leads to

$$(0^*+{a^*}^*(a^*a))+{a^*}^*(a^*a)={a^*}^*a^*,$$

as before. Because of Axiom $A_1$ we get

$$0^*+({a^*}^*(a^*a)+{a^*}^*(a^*a))=(0^*+{a^*}^*(a^*a))+{a^*}^*(a^*a).$$

One use of $R_1$ gives

$$(0^*+{a^*}^*(a^*a))+{a^*}^*(a^*a)=0^*+({a^*}^*(a^*a)+{a^*}^*(a^*a)).$$

Using $R_1$ again implies

$$0^*+({a^*}^*(a^*a)+{a^*}^*(a^*a))={a^*}^*a^*.$$

With $A_6$ we have

Axiom $A_3$ and $R_1$ lead to ${a^*}^*(a^*a)+0^*={a^*}^*a^*$. Then, $A_2$ and $R_1$ give $({a^*}^*a^*)a+0^*={a^*}^*a^*$. With one more use of $R_1$ we get ${a^*}^*a^*=({a^*}^*a^*)a+0^*$. Now, because $o(a)=0$, we can use $R_2$:

Rule $R_1$ gives us $0^*\cdot a^*={a^*}^*a^*$. With $A_7$ and $R_1$ we have $a^*={a^*}^*a^*$. Rule $R_1$ again leads to ${a^*}^*a^*=a^*$. From (15) we get $0^*+({a^*}^*a^*)a={a^*}^*$. Then, $R_1$ gives $0^*+a^*a={a^*}^*$. Axiom $A_{10}$ tells us $a^*=0^*+a^*a$ and $R_1$ implies $0^*+a^*a=a^*$. With one last use of $R_1$ we have

So, we have proven the equation $a^*={a^*}^*$ in the axiom system $F_1$. $\square $

Rights and permissions

Reprints and permissions

Copyright information

About this chapter

Cite this chapter

Beier, S., Holzer, M. (2024). On Regular Expression Proof Complexity of Salomaa’s Axiom System $F_1$. In: Kiefer, S., Křetínský, J., Kučera, A. (eds) Taming the Infinities of Concurrency. Lecture Notes in Computer Science, vol 14660. Springer, Cham. https://doi.org/10.1007/978-3-031-56222-8_4

Download citation

DOI: https://doi.org/10.1007/978-3-031-56222-8_4
Published: 20 March 2024
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-56221-1
Online ISBN: 978-3-031-56222-8
eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

On Regular Expression Proof Complexity of Salomaa’s Axiom System \(F_1\)