* (63) J. P. Lasota, P. Haensel and M. A. Abramowicz, Astrophys. J. 456 (1996), 300 doi:10.1086/176650
  * (64) J. M. Lattimer and F. D. Swesty, Nucl. Phys. A 535 (1991), 331-376 doi:10.1016/0375-9474(91)90452-C
  * (65) L. Lehner, C. Palenzuela, S. L. Liebling, C. Thompson and C. Hanna, Phys. Rev. D 86 (2012), 104035 doi:10.1103/PhysRevD.86.104035 [arXiv:1112.2622 [astro-ph.HE]].
  * (66) B. P. Abbott et al. [LIGO Scientific, Virgo, Fermi GBM, INTEGRAL, IceCube, AstroSat Cadmium Zinc Telluride Imager Team, IPN, Insight-Hxmt, ANTARES, Swift, AGILE Team, 1M2H Team, Dark Energy Camera GW-EM, DES, DLT40, GRAWITA, Fermi-LAT, ATCA, ASKAP, Las Cumbres Observatory Group, OzGrav, DWF (Deeper Wider Faster Program), AST3, CAASTRO, VINROUGE, MASTER, J-GEM, GROWTH, JAGWAR, CaltechNRAO, TTU-NRAO, NuSTAR, Pan-STARRS, MAXI Team, TZAC Consortium, KU, Nordic Optical Telescope, ePESSTO, GROND, Texas Tech University, SALT Group, TOROS, BOOTES, MWA, CALET, IKI-GW Follow-up, H.E.S.S., LOFAR, LWA, HAWC, Pierre Auger, ALMA, Euro VLBI Team, Pi of Sky, Chandra Team at McGill University, DFN, ATLAS Telescopes, High Time Resolution Universe Survey, RIMAS, RATIR and SKA South Africa/MeerKAT], Astrophys. J. Lett. 848 (2017) no.2, L12 doi:10.3847/2041-8213/aa91c9 [arXiv:1710.05833 [astro-ph.HE]].
  * (67) B. P. Abbott et al. [LIGO Scientific and Virgo], Phys. Rev. Lett. 119 (2017) no.16, 161101 doi:10.1103/PhysRevLett.119.161101 [arXiv:1710.05832 [gr-qc]].
  * (68) Y. T. Liu, S. L. Shapiro, Z. B. Etienne and K. Taniguchi, Phys. Rev. D 78 (2008), 024012 doi:10.1103/PhysRevD.78.024012 [arXiv:0803.4193 [astro-ph]].
  * (69) D. R. Lorimer, Living Rev. Rel. 11 (2008), 8 doi:10.12942/lrr-2008-8 [arXiv:0811.0762 [astro-ph]].
  * (70) A. Mignone, M. Ugliano and G. Bodo, Mon. Not. Roy. Astron. Soc. 393 (2009), 1141 doi:10.1111/j.1365-2966.2008.14221.x [arXiv:0811.1483 [astro-ph]].
  * (71) A. Mignone and L. Del Zanna, J. Comput. Phys. 424 (2021), 109748 doi:10.1016/j.jcp.2020.109748 [arXiv:2004.10542 [physics.comp-ph]].
  * (72) H. K. Moffatt , ”Magnetic field generation in electrically conducting fluids”, Cambridge Monographs on Mechanics and Applied Mathematics, Cambridge: University Press, 1978
  * (73) K. P. Mooley, A. T. Deller, O. Gottlieb, E. Nakar, G. Hallinan, S. Bourke, D. A. Frail, A. Horesh, A. Corsi and K. Hotokezaka, Nature 561 (2018) no.7723, 355-359 doi:10.1038/s41586-018-0486-3 [arXiv:1806.09693 [astro-ph.HE]].
  * (74) C. Musolino, C. Ecker and L. Rezzolla, Astrophys. J. 962 (2024) no.1, 61 doi:10.3847/1538-4357/ad1758 [arXiv:2307.03225 [gr-qc]].
  * (75) E. R. Most, L. J. Papenfort and L. Rezzolla, Mon. Not. Roy. Astron. Soc. 490 (2019) no.3, 3588-3600 doi:10.1093/mnras/stz2809 [arXiv:1907.10328 [astro-ph.HE]].
  * (76) E. R. Most and A. A. Philippov, Astrophys. J. Lett. 893 (2020) no.1, L6 doi:10.3847/2041-8213/ab8196 [arXiv:2001.06037 [astro-ph.HE]].
  * (77) E. R. Most and A. A. Philippov, Mon. Not. Roy. Astron. Soc. 515 (2022) no.2, 2710-2724 doi:10.1093/mnras/stac1909 [arXiv:2205.09643 [astro-ph.HE]].
  * (78) E. R. Most and E. Quataert, Astrophys. J. Lett. 947 (2023) no.1, L15 doi:10.3847/2041-8213/acca84 [arXiv:2303.08062 [astro-ph.HE]].
  * (79) E. R. Most, Phys. Rev. D 108 (2023) no.12, 12 doi:10.1103/PhysRevD.108.123012 [arXiv:2311.03333 [astro-ph.HE]].
  * (80) P. Mösta, B. C. Mundim, J. A. Faber, R. Haas, S. C. Noble, T. Bode, F. Löffler, C. D. Ott, C. Reisswig and E. Schnetter, Class. Quant. Grav. 31 (2014), 015005 doi:10.1088/0264-9381/31/1/015005 [arXiv:1304.5544 [gr-qc]].
  * (81) P. Mösta, D. Radice, R. Haas, E. Schnetter and S. Bernuzzi, Astrophys. J. Lett. 901 (2020), L37 doi:10.3847/2041-8213/abb6ef [arXiv:2003.06043 [astro-ph.HE]].
  * (82) H. Mueller and B. D. Serot, Nucl. Phys. A 606 (1996), 508-537 doi:10.1016/0375-9474(96)00187-X [arXiv:nucl-th/9603037 [nucl-th]].
  * (83) D. Neilsen, S. L. Liebling, M. Anderson, L. Lehner, E. O’Connor and C. Palenzuela, Phys. Rev. D 89 (2014) no.10, 104029 doi:10.1103/PhysRevD.89.104029 [arXiv:1403.3680 [gr-qc]].
  * (84) E. O’Connor and C. D. Ott, Class. Quant. Grav. 27 (2010), 114103 doi:10.1088/0264-9381/27/11/114103 [arXiv:0912.2393 [astro-ph.HE]].
  * (85) C. Palenzuela, Mon. Not. Roy. Astron. Soc. 431 (2013), 1853-1865 doi:10.1093/mnras/stt311 [arXiv:1212.0130 [astro-ph.HE]].
  * (86) C. Palenzuela, L. Lehner, M. Ponce, S. L. Liebling, M. Anderson, D. Neilsen and P. Motl, Phys. Rev. Lett. 111 (2013) no.6, 061105 doi:10.1103/PhysRevLett.111.061105 [arXiv:1301.7074 [gr-qc]].
  * (87) C. Palenzuela, L. Lehner, S. L. Liebling, M. Ponce, M. Anderson, D. Neilsen and P. Motl, Phys. Rev. D 88 (2013) no.4, 043011 doi:10.1103/PhysRevD.88.043011 [arXiv:1307.7372 [gr-qc]].
  * (88) C. Palenzuela, S. L. Liebling, D. Neilsen, L. Lehner, O. L. Caballero, E. O’Connor and M. Anderson, Phys. Rev. D 92 (2015) no.4, 044045 doi:10.1103/PhysRevD.92.044045 [arXiv:1505.01607 [gr-qc]].
  * (89) C. Palenzuela, B. Miñano, D. Viganò, A. Arbona, C. Bona-Casas, A. Rigo, M. Bezares, C. Bona and J. Massó, Class. Quant. Grav. 35 (2018) no.18, 185007 doi:10.1088/1361-6382/aad7f6 [arXiv:1806.04182 [physics.comp-ph]].
  * (90) C. Palenzuela, R. Aguilera-Miret, F. Carrasco, R. Ciolfi, J. V. Kalinani, W. Kastaun, B. Miñano and D. Viganò, Phys. Rev. D 106 (2022) no.2, 023013 doi:10.1103/PhysRevD.106.023013 [arXiv:2112.08413 [gr-qc]].
  * (91) C. Palenzuela, S. Liebling and B. Miñano, Phys. Rev. D 105 (2022) no.10, 103020 doi:10.1103/PhysRevD.105.103020 [arXiv:2204.02721 [gr-qc]].
  * (92) D. Price and S. Rosswog, Science 312 (2006), 719 doi:10.1126/science.1125201 [arXiv:astro-ph/0603845 [astro-ph]].
  * (93) D. Radice, F. Galeazzi, J. Lippuner, L. F. Roberts, C. D. Ott and L. Rezzolla, Mon. Not. Roy. Astron. Soc. 460 (2016) no.3, 3255-3271 doi:10.1093/mnras/stw1227 [arXiv:1601.02426 [astro-ph.HE]].
  * (94) D. Radice, Symmetry 12 (2020) no.8, 1249 doi:10.3390/sym12081249 [arXiv:2005.09002 [astro-ph.HE]].
  * (95) F. A. Rasio and S. L. Shapiro, Class. Quant. Grav. 16 (1999), R1-R29 doi:10.1088/0264-9381/16/6/201 [arXiv:gr-qc/9902019 [gr-qc]].
  * (96) J. S. Read, B. D. Lackey, B. J. Owen and J. L. Friedman, Phys. Rev. D 79 (2009), 124032 doi:10.1103/PhysRevD.79.124032 [arXiv:0812.2163 [astro-ph]].
  * (97) L. Rezzolla, B. Giacomazzo, L. Baiotti, J. Granot, C. Kouveliotou and M. A. Aloy, Astrophys. J. Lett. 732 (2011), L6 doi:10.1088/2041-8205/732/1/L6 [arXiv:1101.4298 [astro-ph.HE]].
  * (98) C. E. Rhoades and R. Ruffini, Phys. Rev. Lett., 32 (1974) 324
  * (99) M. Ruiz, R. N. Lang, V. Paschalidis and S. L. Shapiro, Astrophys. J. Lett. 824 (2016) no.1, L6 doi:10.3847/2041-8205/824/1/L6 [arXiv:1604.02455 [astro-ph.HE]].
  * (100) M. Ruiz and S. L. Shapiro, Phys. Rev. D 96 (2017) no.8, 084063 doi:10.1103/PhysRevD.96.084063 [arXiv:1709.00414 [astro-ph.HE]].
  * (101) M. Ruiz, S. L. Shapiro and A. Tsokaros, Phys. Rev. D 97 (2018) no.2, 021501 doi:10.1103/PhysRevD.97.021501 [arXiv:1711.00473 [astro-ph.HE]].
  * (102) M. Ruiz, A. Tsokaros, V. Paschalidis and S. L. Shapiro, Phys. Rev. D 99 (2019) no.8, 084032 doi:10.1103/PhysRevD.99.084032 [arXiv:1902.08636 [astro-ph.HE]].
  * (103) M. Ruiz, A. Tsokaros and S. L. Shapiro, Phys. Rev. D 101 (2020) no.6, 064042 doi:10.1103/PhysRevD.101.064042 [arXiv:2001.09153 [astro-ph.HE]].
  * (104) M. Ruiz, A. Tsokaros and S. L. Shapiro, Phys. Rev. D 104 (2021) no.12, 124049 doi:10.1103/PhysRevD.104.124049 [arXiv:2110.11968 [astro-ph.HE]].
  * (105) V. Savchenko, C. Ferrigno, E. Kuulkers, A. Bazzano, E. Bozzo, S. Brandt, J. Chenevez, T. J. L. Courvoisier, R. Diehl and A. Domingo, et al. Astrophys. J. Lett. 848 (2017) no.2, L15 doi:10.3847/2041-8213/aa8f94 [arXiv:1710.05449 [astro-ph.HE]].
  * (106) Y. Sekiguchi, K. Kiuchi, K. Kyutoku and M. Shibata, Phys. Rev. D 91 (2015) no.6, 064059 doi:10.1103/PhysRevD.91.064059 [arXiv:1502.06660 [astro-ph.HE]].
  * (107) Y. Sekiguchi, K. Kiuchi, K. Kyutoku, M. Shibata and K. Taniguchi, Phys. Rev. D 93 (2016) no.12, 124046 doi:10.1103/PhysRevD.93.124046 [arXiv:1603.01918 [astro-ph.HE]].
  * (108) N. I. Shakura and R. A. Sunyaev, Astron. Astrophys. 24 (1973), 337
  * (109) H. Shen, H. Toki, K. Oyamatsu and K. Sumiyoshi, Nucl. Phys. A 637 (1998), 435-450 doi:10.1016/S0375-9474(98)00236-X [arXiv:nucl-th/9805035 [nucl-th]].
  * (110) D. M. Siegel, R. Ciolfi, A. I. Harte and L. Rezzolla, Phys. Rev. D 87 (2013) no.12, 121302 doi:10.1103/PhysRevD.87.121302 [arXiv:1302.4368 [gr-qc]].
  * (111) D. M. Siegel and B. D. Metzger, Astrophys. J. 858 (2018) no.1, 52 doi:10.3847/1538-4357/aabaec [arXiv:1711.00868 [astro-ph.HE]].
  * (112) D. M. Siegel and B. D. Metzger, Phys. Rev. Lett. 119 (2017) no.23, 231102 doi:10.1103/PhysRevLett.119.231102 [arXiv:1705.05473 [astro-ph.HE]].
  * (113) M. Shibata and Y. i. Sekiguchi, Phys. Rev. D 72 (2005), 044014 doi:10.1103/PhysRevD.72.044014 [arXiv:astro-ph/0507383 [astro-ph]].
  * (114) M. Shibata, M. D. Duez, Y. T. Liu, S. L. Shapiro and B. C. Stephens, Phys. Rev. Lett. 96 (2006), 031102 doi:10.1103/PhysRevLett.96.031102 [arXiv:astro-ph/0511142 [astro-ph]].
  * (115) M. Shibata and K. Taniguchi, Phys. Rev. D 73 (2006), 064027 doi:10.1103/PhysRevD.73.064027 [arXiv:astro-ph/0603145 [astro-ph]].
  * (116) M. Shibata, Y. Suwa, K. Kiuchi and K. Ioka, Astrophys. J. Lett. 734 (2011), L36 doi:10.1088/2041-8205/734/2/L36 [arXiv:1105.3302 [astro-ph.HE]].
  * (117) M. Shibata and K. Hotokezaka, Ann. Rev. Nucl. Part. Sci. 69 (2019), 41-64 doi:10.1146/annurev-nucl-101918-023625 [arXiv:1908.02350 [astro-ph.HE]].
  * (118) M. Shibata, S. Fujibayashi and Y. Sekiguchi, Phys. Rev. D 103 (2021) no.4, 043022 doi:10.1103/PhysRevD.103.043022 [arXiv:2102.01346 [astro-ph.HE]].
  * (119) M. Shibata, S. Fujibayashi and Y. Sekiguchi, Phys. Rev. D 104 (2021) no.6, 063026 doi:10.1103/PhysRevD.104.063026 [arXiv:2109.08732 [astro-ph.HE]].
  * (120) H. C. Spruit, Astron. Astrophys. 381 (2002), 923 doi:10.1051/0004-6361:20011465 [arXiv:astro-ph/0108207 [astro-ph]].
  * (121) A. W. Steiner, M. Hempel and T. Fischer, Astrophys. J. 774 (2013), 17 doi:10.1088/0004-637X/774/1/17 [arXiv:1207.2184 [astro-ph.SR]].
  * (122) B. C. Stephens, M. D. Duez, Y. T. Liu, S. L. Shapiro and M. Shibata, Class. Quant. Grav. 24 (2007), S207-S220 doi:10.1088/0264-9381/24/12/S14 [arXiv:gr-qc/0610103 [gr-qc]].
  * (123) L. Sun, M. Ruiz, S. L. Shapiro and A. Tsokaros, Phys. Rev. D 105 (2022) no.10, 104028 doi:10.1103/PhysRevD.105.104028 [arXiv:2202.12901 [astro-ph.HE]].
  * (124) A. Suresh and H. T. Huynh, J. Comp. Phys. 136 (1997), 83
  * (125) F. X. Timmes, and F. D. Swesty, Astrophys. J. Suppl. 126 (2000), Issue 2, 501-516
  * (126) H. Togashi, K. Nakazato, Y. Takehara, S. Yamamuro, H. Suzuki and M. Takano, Nucl. Phys. A 961 (2017), 78-105 doi:10.1016/j.nuclphysa.2017.02.010 [arXiv:1702.05324 [nucl-th]].
  * (127) S. D. Tootle, L. J. Papenfort, E. R. Most and L. Rezzolla, Astrophys. J. Lett. 922 (2021) no.1, L19 doi:10.3847/2041-8213/ac350d [arXiv:2109.00940 [gr-qc]].
  * (128) C. J. White, J. M. Stone and C. F. Gammie, Astrophys. J. Suppl. 225 (2016) no.2, 22 doi:10.3847/0067-0049/225/2/22 [arXiv:1511.00943 [astro-ph.HE]].
  * (129) J. Zrake and A. I. MacFadyen, Astrophys. J. Lett. 769 (201sp3), L29 doi:10.1088/2041-8205/769/2/L29 [arXiv:1303.1450 [astro-ph.HE]].


smallseparation = .5em, label separation= .1em, right label template= ignore —
letter — letters ignore — word — words ignore — length ignore — language —
languages notion — language of a term ignore — composition ignore — Kleene
star notion — $S$-algebra — $S$-algebras notion — equation — equations notion
— inequation — inequations notion — equational theory w.r.t. languages notion
— valuation — valuations notion — language model — language models notion —
language valuation — language valuations — (language) valuations notion —
composition-free notion — star-free notion — words-to-letters valuation —
words-to-letters valuations — Words-to-letters valuations ignore — variable —
variables notion — KA term — KA terms commentynYN:

# Words-to-Letters Valuations for Language Kleene Algebras with Variable
Complements

Yoshiki Nakamura Tokyo Institute of Technology, Japan
<EMAIL_ADDRESS>Akita University, Japan Ryoma Sin’ya Akita
University, Japan<EMAIL_ADDRESS>
###### Abstract

We investigate the equational theory of Kleene algebra terms with _variable
complements_ —(language) complement where it applies only to variables—w.r.t.
languages. While the equational theory w.r.t. languages coincides with the
language equivalence (under the standard language valuation) for Kleene
algebra terms, this coincidence is broken if we extend the terms with
complements. In this paper, we prove the decidability of some fragments of the
equational theory: the universality problem is coNP-complete, and the
inequational theory $t\leq s$ is coNP-complete when $t$ does not contain
Kleene-star. To this end, we introduce _words-to-letters valuations_ ; they
are sufficient valuations for the equational theory and ease us in
investigating the equational theory w.r.t. languages. Additionally, we prove
that for words with variable complements, the equational theory coincides with
the word equivalence.

##  1 Introduction

Kleene algebra (KA) [7, 4] is an algebraic system for regular expressions
consisting of union ($\mathbin{\cup}$), composition ($\mathbin{\cdot}$),
Kleene-star ($\\_^{*}$), emptiness ($\bot$), and identity ($\mathsf{I}$). In
this paper, we consider KAs _w.r.t. languages_ (a.k.a., language models of
KAs, language KAs). Interestingly, the equational theory of KAs w.r.t.
languages coincides with the language equivalence under the standard language
valuation (see also, e.g., [2, 12]): for all KA terms (i.e., regular
expressions) $t,s$, we have

$\displaystyle\mathsf{LANG}\models t=s\quad\iff\quad[t]=[s].$ ($\dagger$)

Here, we write $\mathsf{LANG}\models t=s$ if the equation $t=s$ holds for all
language models (i.e., each variable $x$ maps to not only the singleton
language $\\{x\\}$ but also any languages); we write $[u]$ for the language of
a regular expression $u$ (i.e., each variable $x$ maps to the singleton
language $\\{x\\}$). Since the valuation $[\\_]$ is an instance of valuations
in $\mathsf{LANG}$, the direction $\Longrightarrow$ is trivial (this direction
always holds even if we extend KA terms with some extra operators). The
direction $\Longleftarrow$ is a consequence of the completeness of KAs (see
Appendix A for an alternative proof not relying on the completeness of KAs).
However, the direction $\Longleftarrow$ fails in general when we extend KA
terms with extra operators. Namely, the equational theory w.r.t. languages
does not coincide with the language equivalence in general (see below for
complements). The equational theory of KAs with some operators w.r.t.
languages was studied, e.g., with reverse [3], with tests [8] (where languages
are of guarded strings, not words), with intersection [2], and with
universality ($\top$) [12]. Nevertheless, to the best of authors’ knowledge,
_variable complements_ (and even complements) w.r.t. languages has not yet
been investigated, while those w.r.t. binary relations were studied, e.g., in
[11] (for complements; cf. Tarski’s calculus of relations [14]) and [10] (for
variable complements).

In this paper, we investigate the equational theory of KA terms with _variable
complements_ ($x^{-}$)—(language) complement, where it applies only to
variables (we use $x$ to denote variables)—w.r.t. languages. For KA terms with
variable complements, ($\dagger$ ‣ 1) fails. The following is an example:

$\displaystyle\mathsf{LANG}$ $\displaystyle\not\models
x^{-}=x^{-}\mathbin{\cdot}x^{-}$ $\displaystyle[x^{-}]$
$\displaystyle=[x^{-}\mathbin{\cdot}x^{-}].$

(For $\mathsf{LANG}\not\models$, consider a valuation such that $x^{-}$ maps
to the language $\\{a\\}$.) As the example above (see also Remark 1, for more
examples) shows, the equational theory of KAs with variable complements w.r.t.
languages significantly differs from the language equivalence under the
standard language valuation. While the language equivalence problem of KA
terms with variable complements is decidable in PSPACE by a standard automata
construction [15] (and hence, PSPACE-complete [9, 13, 6]), it remains whether
the equational theory w.r.t. languages is decidable.

We prove the decidability and complexity of some fragments of the equational
theory of KA terms with variable complements w.r.t. languages: the
universality problem is coNP-complete (Cor. 18), and the inequational theory
$t\leq s$ is coNP-complete when $t$ does not contain Kleene-star (Cor. 29). To
this end, we introduce _words-to-letters valuations_. Words-to-letters
valuations are sufficient for the equational theory of KA terms with variable
complements w.r.t. languages (words-to-letters-valuation property; Cor. 30):
for all terms $t,s$, if there is some language valuation such that it refutes
$t=s$, there is some words-to-letters valuation such that it refutes $t=s$.
This property eases us in investigating the equational theory w.r.t.
languages.

Additionally, by using words-to-letters valuations, we prove a completeness
theorem for words with variable complements: the equational theory coincides
with the word equivalence (Thm. 32). A limitation of words-to-letters
valuations is that the number of letters is not bounded; so, they cannot apply
to the equational theory over $\mathsf{LANG}_{n}$ (language models over sets
of cardinality at most a natural number $n$). Nevertheless, by giving another
valuation, we can show the coincidence for one-variable words (Thm. 36). We
leave open for the many-variable words.

### Outline

In Sect. 2, we briefly give basic definitions, including the syntax and
semantics of KA terms with variable complements. Additionally, we give
languages for KA terms with variable complements (Sect. 2.3). In Sects. 3, 4,
5, we consider fragments of the equational theory of KA terms with variable
complements w.r.t. languages, step-by-step. In Sect. 3, we consider the
identity inclusion problem ($\mathsf{LANG}\models\mathsf{I}\leq t$?). This
problem is relatively easy but contains the coNP-hardness result (Cor. 6). In
Sect. 4, we consider the variable inclusion problem ($\mathsf{LANG}\models
x\leq t$?) and the universality problem ($\mathsf{LANG}\models\top\leq t$?).
In Sect. 5, we consider the word inclusion problem ($\mathsf{LANG}\models
w\leq t$?). This section proceeds in the same way as Sect. 4, thanks to words-
to-letters valuations (Def. 21). Consequently, the inequational theory $t\leq
s$ is coNP-complete when $t$ does not contain Kleene-star (Cor. 29).
Additionally, we prove the words-to-letters valuation property (Cor. 30) for
the equational theory of (full) KA terms with variable complements w.r.t.
languages. In Sect. 6, we consider the equational theory of words with
variable complements and show a completeness theorem (Thm. 32). Sect. 7
concludes this paper.

##  2 Preliminaries

We write ${\rm Nature}$ for the set of non-negative integers. For a set $X$,
we write $\mathop{\\#}(X)$ for the cardinality of $X$ and $\wp(X)$ for the
power set of $X$.

For a set $X$ (of *letters), we write $X^{*}$ for the set of *words over $X$:
finite sequences of elements of $X$. We write $\mathsf{I}$ for the empty word.
We write $wv$ for the concatenation of words $w$ and $v$. A *language over $X$
is a subset of $X^{*}$. We use $w,v$ to denote words and use $L,K$ to denote
languages, respectively. For languages $L,K\subseteq X^{*}$, the *composition
$L\mathbin{\cdot}K$ and the *Kleene star $L^{*}$ is defined by:

$\displaystyle L\mathbin{\cdot}K$
$\displaystyle\quad\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\quad\\{wv\mid
w\in L\ \land\ w\in K\\}$ $\displaystyle L^{*}$
$\displaystyle\quad\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\quad\\{w_{0}\dots
w_{n-1}\mid\exists n\in{\rm Nature},\forall i<n,\ w_{i}\in L\\}.$

###  2.1 Syntax: KA terms with variable complements

Let $\mathbf{V}$ be a set of *variables. The set of Kleene algebra (KA) terms
with variable complements ($x^{-}$) is defined by the following grammar:

$\displaystyle\mathbf{T}\ni t,s,u\quad\Coloneqq\quad
x\mid\mathsf{I}\mid\bot\mid t\mathbin{\cdot}s\mid t\mathbin{\cup}s\mid
t^{*}\mid x^{-}$ ($x\in\mathbf{V}$)

We use parentheses in ambiguous situations. We often abbreviate
$t\mathbin{\cdot}s$ to $ts$. We write $\top$ for the term
$x\mathbin{\cup}x^{-}$, where $x$ is any variable.

An *equation $t=s$ is a pair of terms. An *inequation $t\leq s$ is an
abbreviation of the equation $t\mathbin{\cup}s=s$.

###  2.2 Semantics: language models

Consider the signature
$S\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\\{\mathsf{I}_{(0)},\bot_{(0)},\mathbin{\cdot}_{(2)},\mathbin{\cup}_{(2)},{\\_^{*}}_{(1)},{\\_^{-}}_{(1)}\\}$.
An *$S$-algebra $A$ is a tuple $\langle|A|,\\{f^{A}\\}_{f_{(k)}\in S}\rangle$,
where $|A|$ is a non-empty set and $f^{A}\colon|A|^{k}\to|A|$ is a $k$-ary map
for each $f_{(k)}\in S$. A *valuation $\mathfrak{v}$ on an $S$-algebra $A$ is
a map $\mathfrak{v}\colon\mathbf{V}\to|A|$. For a valuation $\mathfrak{v}$, we
write $\hat{\mathfrak{v}}\colon\mathbf{T}\to|A|$ for the unique homomorphism
extending $\mathfrak{v}$.

The *language model $A$ over a set $X$ is an $S$-algebra such that
$|A|=\wp(X^{*})$ and for all $L,K\subseteq X^{*}$,

$\displaystyle\mathsf{I}^{A}$ $\displaystyle=\\{\mathsf{I}\\}$ $\displaystyle
L\mathbin{\cdot}^{A}K$ $\displaystyle=L\mathbin{\cdot}K$ $\displaystyle
L^{*^{A}}$ $\displaystyle=L^{*}$ $\displaystyle\bot^{A}$
$\displaystyle=\emptyset$ $\displaystyle L\mathbin{\cup}^{A}K$
$\displaystyle=L\mathbin{\cup}K$ $\displaystyle L^{-^{A}}$
$\displaystyle=X^{*}\setminus L.$

We write $\mathsf{LANG}$ for the class of all language models. A *language
valuation over a set $X$ is a valuation on some language model over $X$. For
an equation $t=s$, we let

$\mathsf{LANG}\models
t=s\quad\mathrel{\ensurestackMath{\stackon[1pt]{\iff}{\scriptscriptstyle\Delta}}}\quad\hat{\mathfrak{v}}(t)=\hat{\mathfrak{v}}(s)\mbox{
holds for all \kl{language valuations} $\mathfrak{v}$}.$

The *equational theory w.r.t. languages is the set of all equations $t=s$ such
that $\mathsf{LANG}\models t=s$.

Additionally, the *[language of a term]language $[t]\subseteq\mathbf{V}^{*}$
of a term $t$ is defined by:

$\displaystyle[x]$
$\displaystyle\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\\{x\\}$
$\displaystyle[\mathsf{I}]$
$\displaystyle\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\\{\mathsf{I}\\}$
$\displaystyle[t\mathbin{\cdot}s]$
$\displaystyle\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}[t]\mathbin{\cdot}[s]$
$\displaystyle[t^{*}]$
$\displaystyle\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}[t]^{*}$
$\displaystyle[\bot]$
$\displaystyle\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\emptyset$
$\displaystyle[t\mathbin{\cup}s]$
$\displaystyle\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}[t]\mathbin{\cup}[s]$
$\displaystyle[t^{-}]$
$\displaystyle\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\mathbf{V}^{*}\setminus[t].$

By definition, we have $[t]=\hat{\mathfrak{v}}(t)$ if $\mathfrak{v}$ is the
valuation on the language model over the set $\mathbf{V}$ defined by
$\mathfrak{v}(x)=\\{x\\}$ for all $x\in\mathbf{V}$. Hence, for all $t,s$, we
have

$\displaystyle\mathsf{LANG}\models t=s\quad\Longrightarrow\quad[t]=[s].$
($\ddagger$)

######  Remark 1.

The converse direction fails111The failure can be also shown by that the
universality $\top$ can be expressed by $x\mathbin{\cup}x^{-}$; see also [12,
Remark. 3.6].; for example, when $x\neq y$,

$\displaystyle\mathsf{LANG}\not\models y\leq x^{-}$
$\displaystyle[y]\subseteq[x^{-}].$

Here $t\leq s$ denotes the equation $t\mathbin{\cup}s=s$ (so, indeed, an
equation). For $\mathsf{LANG}\not\models y\leq x^{-}$, consider a language
valuation $\mathfrak{v}$ such that $a\in\mathfrak{v}(x)$ and
$a\in\mathfrak{v}(y)$; then we have
$a\in\hat{\mathfrak{v}}(y)\setminus\hat{\mathfrak{v}}(x^{-})$.
$[y]\subseteq[x^{-}]$ is shown by
$[y]=\\{y\\}\subseteq\mathbf{V}^{*}\setminus\\{x\\}=[x^{-}]$. More generally,
for any word $w$ over $\mathbf{V}$ such that $w\neq x$,

$\displaystyle\mathsf{LANG}\not\models w\leq x^{-}$
$\displaystyle[w]\subseteq[x^{-}].$

Moreover, for example, there are the following examples (for
$\mathsf{LANG}\not\models$, consider a valuation such that both $x$ and $y$
map to the language $X^{*}\setminus\\{a\\}$, where $X$ is a set and $a\in X$):

$\displaystyle\mathsf{LANG}$ $\displaystyle\not\models
x^{-}=x^{-}\mathbin{\cdot}x^{-}$ $\displaystyle[x^{-}]$
$\displaystyle=[x^{-}\mathbin{\cdot}x^{-}]$ $\displaystyle\mathsf{LANG}$
$\displaystyle\not\models\top=x^{-}\mathbin{\cdot}y^{-}$ $\displaystyle[\top]$
$\displaystyle=[x^{-}\mathbin{\cdot}y^{-}]$ $\displaystyle\mathsf{LANG}$
$\displaystyle\not\models\top=x^{-}\mathbin{\cup}y^{-}$ $\displaystyle[\top]$
$\displaystyle=[x^{-}\mathbin{\cup}y^{-}].$

As the examples above show, for KA terms with variable complements, the
equational theory w.r.t. languages ($\mathsf{LANG}\models t=s$?) significantly
differs from the language equivalence problem ($[t]=[s]$?).

In the sequel, we focus on the equational theory w.r.t. languages and
investigate its fragments. We prepare a useful tool (Lem. 2), which enables us
to decompose terms into languages of words.

###  2.3 Languages for KA terms with variable complements

Let $\mathbf{V}^{\prime}=\\{x,x^{-}\mid x\in\mathbf{V}\\}$. For a term $t$, we
write $[t]_{\mathbf{V}^{\prime}}$ for the [language of a term]language of $t$
where $t$ is viewed as the regular expression over $\mathbf{V}^{\prime}$. Each
word over $\mathbf{V}^{\prime}$ is a term such that both the union
($\mathbin{\cup}$) and the Kleene-star ($\\_^{*}$) do not occur. Note that
$[x^{-}]_{\mathbf{V}^{\prime}}=\\{x^{-}\\}$, cf.
$[x^{-}]=\mathbf{V}^{*}\setminus\\{x\\}$. For a language valuation
$\mathfrak{v}$ and a language $L$ over $\mathbf{V}^{\prime}$, we define

$\hat{\mathfrak{v}}(L)\quad\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\quad\bigcup_{w\in
L}\hat{\mathfrak{v}}(w).$

By using the distributive law of $\mathbin{\cdot}$ w.r.t. $\mathbin{\cup}$,
for all languages $L,K$ and language valuations $\mathfrak{v}$, we have:

$\displaystyle\hat{\mathfrak{v}}(L\mathbin{\cup}K)$
$\displaystyle=\hat{\mathfrak{v}}(L)\mathbin{\cup}\hat{\mathfrak{v}}(K)$
$\displaystyle\hat{\mathfrak{v}}(L\mathbin{\cdot}K)$
$\displaystyle=\hat{\mathfrak{v}}(L)\mathbin{\cdot}\hat{\mathfrak{v}}(K)$
$\displaystyle\hat{\mathfrak{v}}(L^{*})$
$\displaystyle=\hat{\mathfrak{v}}(L)^{*}.$

We can decompose each term $t$ to the set $[t]_{\mathbf{V}^{\prime}}$ of words
over $\mathbf{V}^{\prime}$ as follows:

######  Lemma 2.

Let $\mathfrak{v}$ be a language valuation. For all terms $t$, we have

$\hat{\mathfrak{v}}(t)\quad=\quad\hat{\mathfrak{v}}([t]_{\mathbf{V}^{\prime}}).$

###### Proof.

By easy induction on $t$ using the equations above. Case
$t=x,x^{-},\mathsf{I}$: Clear, by $[t]_{\mathbf{V}^{\prime}}=\\{t\\}$. Case
$t=\bot$: By
$\hat{\mathfrak{v}}(\bot)=\emptyset=\hat{\mathfrak{v}}([\bot]_{\mathbf{V}^{\prime}})$.
Case $t=s\mathbin{\cup}u$, Case $t=s\mathbin{\cdot}u$, Case $t=s^{*}$: By IH
with the equations above. For example, when $t=s\mathbin{\cdot}u$, we have

$\displaystyle\hat{\mathfrak{v}}(s\mathbin{\cdot}u)=\hat{\mathfrak{v}}(s)\mathbin{\cdot}\hat{\mathfrak{v}}(u)$
$\displaystyle=\hat{\mathfrak{v}}([s]_{\mathbf{V}^{\prime}})\mathbin{\cdot}\hat{\mathfrak{v}}([u]_{\mathbf{V}^{\prime}})$
(IH)
$\displaystyle=\hat{\mathfrak{v}}([s]_{\mathbf{V}^{\prime}}\mathbin{\cdot}[u]_{\mathbf{V}^{\prime}})=\hat{\mathfrak{v}}([s\mathbin{\cdot}u]_{\mathbf{V}^{\prime}}).$
∎

##  3 The identity inclusion problem

We first consider the _identity inclusion problem_ w.r.t. languages:

Given a term $t$, does $\mathsf{LANG}\models\mathsf{I}\leq t$?

This problem is relatively easily solvable. Since
$\mathsf{LANG}\models\mathsf{I}\leq t$ iff
$\mathsf{I}\in\hat{\mathfrak{v}}(t)$ for all language valuation
$\mathfrak{v}$, it suffices to consider the membership of the empty word
$\mathsf{I}$. We use the following facts.

######  Proposition 3.

For all languages $L,K$, we have:

$\displaystyle\mathsf{I}\in L\mathbin{\cup}K$
$\displaystyle\quad\iff\quad\mathsf{I}\in L\lor\mathsf{I}\in K$
$\displaystyle\mathsf{I}\in L\mathbin{\cdot}K$
$\displaystyle\quad\iff\quad\mathsf{I}\in L\land\mathsf{I}\in K$
$\displaystyle\mathsf{I}\in L^{*}$ $\displaystyle\quad\iff\quad\mathsf{True}.$

###### Proof.

Clear, by definition. ∎

######  Lemma 4.

Let $\mathfrak{v},\mathfrak{v}^{\prime}$ be language valuations. Assume that
for all variables $x$, $\mathsf{I}\in\mathfrak{v}(x)$ iff
$\mathsf{I}\in\mathfrak{v}^{\prime}(x)$. For all terms $t$,

$\mathsf{I}\in\hat{\mathfrak{v}}(t)\quad\iff\quad\mathsf{I}\in\hat{\mathfrak{v}}^{\prime}(t).$

###### Proof.

By easy induction on $t$ using Prop. 3. Case $t=x,x^{-}$: Clear by the
assumption. Case $t$ is a constant: Trivial. For inductive cases, e.g., Case
$t=s\mathbin{\cup}u$: By using Prop. 3, we have

$\displaystyle\mathsf{I}\in\hat{\mathfrak{v}}(s\mathbin{\cup}u)\iff\mathsf{I}\in\hat{\mathfrak{v}}(s)\lor\mathsf{I}\in\hat{\mathfrak{v}}(u)$
$\displaystyle\iff\mathsf{I}\in\hat{\mathfrak{v}}^{\prime}(s)\lor\mathsf{I}\in\hat{\mathfrak{v}}^{\prime}(u)$
(IH)
$\displaystyle\iff\mathsf{I}\in\hat{\mathfrak{v}}^{\prime}(s\mathbin{\cup}u).$

(Similarly for the other inductive cases.) ∎

By using Lem. 4, it suffices to consider a finite number of valuations, as
follows.

######  Theorem 5.

For all terms $t$, the following are equivalent:

  1. 1.

$\mathsf{LANG}\models\mathsf{I}\leq t$ (i.e.,
$\hat{\mathfrak{v}}(\mathsf{I})\subseteq\hat{\mathfrak{v}}(t)$, for all
language valuations $\mathfrak{v}$);

  2. 2.

$\hat{\mathfrak{v}}(\mathsf{I})\subseteq\hat{\mathfrak{v}}(t)$, for all
language valuations $\mathfrak{v}$ over the empty set s.t. for all $x$,
$\mathfrak{v}(x)\subseteq\\{\mathsf{I}\\}$.

###### Proof.

1$\Rightarrow$2: Trivial. 2$\Rightarrow$1: We prove the contraposition. By
$\mathsf{LANG}\not\models\mathsf{I}\leq t$, there is a language valuation
$\mathfrak{v}$ s.t.
$\hat{\mathfrak{v}}(\mathsf{I})\not\subseteq\hat{\mathfrak{v}}(t)$ (i.e.,
$\mathsf{I}\not\in\hat{\mathfrak{v}}(t)$). Let $\mathfrak{v}^{\langle\rangle}$
be the language valuation over the empty set defined by:

$\mathfrak{v}^{\langle\rangle}(x)\quad\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\quad\\{\mathsf{I}\mid\mathsf{I}\in\mathfrak{v}(x)\\}.$

Then by Lem. 4, $\mathsf{I}\not\in\hat{\mathfrak{v}}^{\langle\rangle}(t)$
holds; thus, we have
$\hat{\mathfrak{v}}^{\langle\rangle}(\mathsf{I})\not\subseteq\hat{\mathfrak{v}}^{\langle\rangle}(t)$.
∎

######  Corollary 6.

The identity inclusion problem (given a term $t$, does
$\mathsf{LANG}\models\mathsf{I}\leq t$?) is decidable and coNP-complete for KA
terms with variable complements.

###### Proof.

(in coNP): Thm. 5 induces the following non-deterministic polynomial
algorithm:

  1. 1.

Pick up a language valuation $\mathfrak{v}$ over the empty set s.t. for all
$x$, $\mathfrak{v}(x)\subseteq\\{\mathsf{I}\\}$, non-deterministically.

  2. 2.

If $\hat{\mathfrak{v}}(\mathsf{I})\not\subseteq\hat{\mathfrak{v}}(t)$, then
return $\mathsf{True}$; otherwise return $\mathsf{False}$.

Then $\mathsf{LANG}\not\models\mathsf{I}\leq t$ if some execution returns
$\mathsf{True}$; and $\mathsf{LANG}\models\mathsf{I}\leq t$ otherwise. Hence,
the identity inclusion problem is decidable in coNP (as its complemented
problem is in NP).

(coNP-hard): Because this problem subsumes the validity problem of
propositional formulas in disjunctive normal form, which is a well-known coNP-
complete problem [5]. More precisely, given a propositional formula $\varphi$
in disjunctive normal form, let $t$ be the term obtained from $\varphi$ by
replacing each conjunction $\land$ with $\mathbin{\cdot}$ and each disjunction
$\lor$ with $\mathbin{\cup}$ (where we map each positive literal $x$ to the
variable $x$ and each negative literal $x^{-}$ to the complemented variable
$x^{-}$); for example, if $\varphi=(x\land y^{-})\lor(y\lor x^{-})$, then
$t=(x\mathbin{\cdot}y^{-})\mathbin{\cup}(y\mathbin{\cup}x^{-})$. Then, for all
language valuations $\mathfrak{v}$ (over the empty set s.t. for all
$x,\mathfrak{v}(x)\subseteq\\{\mathsf{I}\\}$), we have:
$\hat{\mathfrak{v}}(\mathsf{I})\subseteq\hat{\mathfrak{v}}(t)$ holds iff
$\varphi$ is $\mathsf{True}$ on the valuation $\mathfrak{v}^{\prime}$, where
$\mathfrak{v}^{\prime}$ is the map mapping each $x$ to $\mathsf{True}$ if
$\mathsf{I}\in\mathfrak{v}(x)$ and $\mathsf{False}$ otherwise. Thus by Thm. 5,
$\mathsf{LANG}\models\mathsf{I}\leq t$ iff $\varphi$ is valid. Hence, the
identity inclusion problem is coNP-hard. ∎

######  Remark 7.

Under the standard language valuation, the identity inclusion problem—given a
term $t$, does $[\mathsf{I}]\subseteq[t]$? (i.e., does $\mathsf{I}\in[t]$?)—is
decidable in P (because we can compute “$\mathsf{I}\in[t]$?” by induction on
$t$, as $\mathsf{I}\not\in[x]$ and $\mathsf{I}\in[x^{-}]$ for every variable
$x$). Hence, for KA terms with variable complements, the identity inclusion
problem w.r.t. languages is strictly harder than that under the standard
language valuation unless P = NP.

##  4 The variable inclusion problem and the universality problem

Next, we consider the _variable inclusion problem_ :

Given a variable $x$ and a term $t$, does $\mathsf{LANG}\models x\leq t$?

In the identity inclusion problem, if
$w\in\hat{\mathfrak{v}}(\mathsf{I})\setminus\hat{\mathfrak{v}}(t)$, then
$w=\mathsf{I}$ should hold; so it suffices to consider the membership of the
empty word $\mathsf{I}$. However, in the variable inclusion problem, this
situation changes: if
$w\in\hat{\mathfrak{v}}(x)\setminus\hat{\mathfrak{v}}(t)$, then $w$ is
possibly any word.

Nevertheless, we can overcome the problem above for KA terms with variable
complements; more precisely, from a language valuation $\mathfrak{v}$ s.t.
$w\in\hat{\mathfrak{v}}(x)\setminus\hat{\mathfrak{v}}(t)$ for some word $w$,
we can construct a language valuation $\mathfrak{v}^{\prime}$ s.t.
$\ell\in\hat{\mathfrak{v}}^{\prime}(x)\setminus\hat{\mathfrak{v}}^{\prime}(t)$
for some _letter_ $\ell$. If such $\mathfrak{v}^{\prime}$ can be constructed
from $\mathfrak{v}$, then considering the membership of letters suffices
because we have

$\displaystyle\mathsf{LANG}\not\models x\leq t$ $\displaystyle\iff
w\in\hat{\mathfrak{v}}(x)\setminus\hat{\mathfrak{v}}(t)\mbox{ for some
\kl{language valuation} $\mathfrak{v}$ and \kl{word} $w$}$ (By definition)
$\displaystyle\iff\ell\in\hat{\mathfrak{v}}^{\prime}(x)\setminus\hat{\mathfrak{v}}^{\prime}(t)\mbox{
for some \kl{language valuation} $\mathfrak{v}^{\prime}$ and
\emph{\kl{letter}} $\ell$}$ ($\Longrightarrow$: By the condition of
$\mathfrak{v}^{\prime}$. $\Longleftarrow$: Trivial by letting
$\mathfrak{v}=\mathfrak{v}^{\prime}$.)

Such a language valuation $\mathfrak{v}^{\prime}$ can be defined as follows:

######  Definition 8.

For a language valuation $\mathfrak{v}$ over a set $X$ and a word $w$ over
$X$, the language valuation $\mathfrak{v}^{w}$ over the set $\\{\ell\\}$
(where $\ell$ is a letter) is defined as follows:

$\mathfrak{v}^{w}(x)\quad\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\quad\\{\mathsf{I}\mid\mathsf{I}\in\mathfrak{v}(x)\\}\mathbin{\cup}\\{\ell\mid
w\in\mathfrak{v}(x)\\}.$

In the following, we prove that $\mathfrak{v}^{w}$ satisfies the condition of
$\mathfrak{v}^{\prime}$ above, that is, the following conditions:

  * •

$w\in\hat{\mathfrak{v}}(x)\Longrightarrow\ell\in\hat{\mathfrak{v}}^{w}(x)$;

  * •

$w\not\in\hat{\mathfrak{v}}(t)\Longrightarrow\ell\not\in\hat{\mathfrak{v}}^{w}(t)$.

The first condition is clear by the definition of $\mathfrak{v}^{w}$. We prove
the second condition in Lem. 10. We prepare the following fact:

######  Proposition 9 (cf. Prop. 3).

For all languages $L,K$ and letters $a$, we have:

$\displaystyle a\in L\mathbin{\cup}K$ $\displaystyle\quad\iff\quad a\in L\lor
a\in K$ $\displaystyle a\in L\mathbin{\cdot}K$
$\displaystyle\quad\iff\quad(a\in L\land\mathsf{I}\in K)\lor(\mathsf{I}\in
L\land a\in K)$ $\displaystyle a\in L^{*}$ $\displaystyle\quad\iff\quad a\in
L.$

###### Proof.

Clear, by definition. ∎

######  Lemma 10 (cf. Lem. 4).

Let $\mathfrak{v}$ be a language valuation and $w$ be a word. For all terms
$t$, we have:

$\ell\in\hat{\mathfrak{v}}^{w}(t)\quad\Longrightarrow\quad
w\in\hat{\mathfrak{v}}(t).$

###### Proof.

By induction on $t$.

Case $t=x,x^{-}$: By the construction of $\mathfrak{v}^{w}$,
$\ell\in\hat{\mathfrak{v}}^{w}(x)$ iff $w\in\hat{\mathfrak{v}}(x)$. (Hence, we
also have $\ell\in\hat{\mathfrak{v}}^{w}(x^{-})$ iff
$w\in\hat{\mathfrak{v}}(x^{-})$.)

Case $t=\bot,\mathsf{I}$: By $\ell\not\in\hat{\mathfrak{v}}^{w}(t)$.

Case $t=s\mathbin{\cup}u$: We have:

$\displaystyle\ell\in\hat{\mathfrak{v}}^{w}(s)\mathbin{\cup}\hat{\mathfrak{v}}^{w}(u)$
$\displaystyle\Longleftrightarrow\ell\in\hat{\mathfrak{v}}^{w}(s)\lor\ell\in\hat{\mathfrak{v}}^{w}(u)$
(Prop. 9) $\displaystyle\Longrightarrow w\in\hat{\mathfrak{v}}(s)\lor
w\in\hat{\mathfrak{v}}(u)$ (IH) $\displaystyle\Longrightarrow
w\in\hat{\mathfrak{v}}(s)\mathbin{\cup}\hat{\mathfrak{v}}(u).$

Case $t=s\mathbin{\cdot}u$: We have:

$\displaystyle\ell\in\hat{\mathfrak{v}}^{w}(s)\mathbin{\cdot}\hat{\mathfrak{v}}^{w}(u)$
$\displaystyle\Longleftrightarrow(\ell\in\hat{\mathfrak{v}}^{w}(s)\land\mathsf{I}\in\hat{\mathfrak{v}}^{w}(u))\lor(\mathsf{I}\in\hat{\mathfrak{v}}^{w}(s)\land\ell\in\hat{\mathfrak{v}}^{w}(u))$
(Prop. 9)
$\displaystyle\Longrightarrow(w\in\hat{\mathfrak{v}}(s)\land\mathsf{I}\in\hat{\mathfrak{v}}(u))\lor(\mathsf{I}\in\hat{\mathfrak{v}}(s)\land
w\in\hat{\mathfrak{v}}(u))$ (IH with Lem. 4) $\displaystyle\Longrightarrow
w\in\hat{\mathfrak{v}}(s)\mathbin{\cdot}\hat{\mathfrak{v}}(u)$

Case $t=s^{*}$: We have:

$\displaystyle\ell\in\hat{\mathfrak{v}}^{w}(s)^{*}$
$\displaystyle\Longleftrightarrow\ell\in\hat{\mathfrak{v}}^{w}(s)$ (Prop. 9)
$\displaystyle\Longrightarrow w\in\hat{\mathfrak{v}}(s)$ (IH)
$\displaystyle\Longrightarrow w\in\hat{\mathfrak{v}}(s)^{*}$

∎

Thus we have obtained the expected condition for $\mathfrak{v}^{w}$ as
follows:

######  Corollary 11.

Let $\mathfrak{v}$ be a language valuation and $w$ be a word. For all
variables $x$ and terms $t$,

$w\in\hat{\mathfrak{v}}(x)\setminus\hat{\mathfrak{v}}(t)\quad\Longrightarrow\quad\ell\in\hat{\mathfrak{v}}^{w}(x)\setminus\hat{\mathfrak{v}}^{w}(t).$

###### Proof.

For $\ell\in\hat{\mathfrak{v}}^{w}(x)$: By the construction of
$\mathfrak{v}^{w}$, $\ell\in\hat{\mathfrak{v}}^{w}(x)$ iff
$w\in\hat{\mathfrak{v}}(x)$. For $\ell\not\in\hat{\mathfrak{v}}^{w}(t)$: By
Lem. 10. ∎

######  Theorem 12.

For all variables $x$ and terms $t$, the following are equivalent:

  1. 1.

$\mathsf{LANG}\models x\leq t$;

  2. 2.

$\hat{\mathfrak{v}}(x)\subseteq\hat{\mathfrak{v}}(t)$ for all language
valuations $\mathfrak{v}$ over the set $\\{\ell\\}$ s.t.
$\mathfrak{v}(y)\subseteq\\{\mathsf{I},\ell\\}$ for all $y$;

  3. 3.

$\hat{\mathfrak{v}}^{w}(x)\subseteq\hat{\mathfrak{v}}^{w}(t)$ for all language
valuations $\mathfrak{v}$ and words $w$.

###### Proof.

1$\Rightarrow$2, 2$\Rightarrow$3: Trivial, as
$\hat{\mathfrak{v}}^{w}(y)\subseteq\\{\mathsf{I},\ell\\}$ for all $y$.
3$\Rightarrow$1: The contraposition is shown by Cor. 11. ∎

######  Corollary 13.

The variable inclusion problem (given a variable $x$ and a term $t$, does
$\mathsf{LANG}\models x\leq t$?) is decidable and coNP-complete for KA terms
with variable complements.

###### Proof.

(in coNP): By the condition 2 of Thm. 12, we can give an algorithm as with
Cor. 6. (coNP-hard): We give a reduction from the validity problem of
propositional formulas in disjunctive normal form, as with Cor. 6. Given a
propositional formula $\varphi$ in disjunctive normal form, let $t$ be the
term obtained by the translation in Cor. 6; so, we have that $\varphi$ is
valid iff $\mathsf{LANG}\models\mathsf{I}\leq t$. Then we also have that
$\mathsf{LANG}\models\mathsf{I}\leq t$ iff $\mathsf{LANG}\models z\leq
z\mathbin{\cdot}t$ (where $z$ is a fresh variable); the direction
$\Longrightarrow$ is shown by the congruence law, and the direction
$\Longleftarrow$ is shown by the substitution law. Therefore, we have that
$\varphi$ is valid iff $\mathsf{LANG}\models z\leq z\mathbin{\cdot}t$; thus,
the variable inclusion problem is coNP-hard. ∎

###  4.1 Generalization from variables to composition-free terms

The proof above applies to not only variables but also terms $t$ having the
following property: For all language valuations $\mathfrak{v}$,

$\displaystyle\mbox{for all non-empty \kl{words} $w$,
\qquad}w\in\hat{\mathfrak{v}}(t)\Longrightarrow\ell\in\hat{\mathfrak{v}}^{w}(t).$
$(\mathsf{L}_{1})$

(This condition is intended for composition-free terms (Lem. 15). This is
generalized to $(\mathsf{L}_{n})$ in Sect. 5.1.) If $t$ satisfies the
condition $(\mathsf{L}_{1})$, then combining with Lem. 10 (and with Lem. 4 for
the empty word $\mathsf{I}$) yields that for all language valuations
$\mathfrak{v}$ and words $w$,

$\displaystyle w\in\hat{\mathfrak{v}}(t)\setminus\hat{\mathfrak{v}}(s)$
$\displaystyle\quad\Longrightarrow\quad\begin{cases}\ell\in\hat{\mathfrak{v}}^{w}(t)\setminus\hat{\mathfrak{v}}^{w}(s)&(\mbox{if
$w\neq\mathsf{I}$})\\\
\mathsf{I}\in\hat{\mathfrak{v}}^{w}(t)\setminus\hat{\mathfrak{v}}^{w}(s)&(\mbox{if
$w=\mathsf{I}$})\end{cases}.$

Hence, we have the following:

######  Theorem 14 (cf. Thm. 12).

For all terms $t,s$, if $t$ satisfies $(\mathsf{L}_{1})$, then the following
are equivalent:

  1. 1.

$\mathsf{LANG}\models t\leq s$;

  2. 2.

$\hat{\mathfrak{v}}(t)\subseteq\hat{\mathfrak{v}}(s)$ for all language
valuations $\mathfrak{v}$ over the set $\\{\ell\\}$ s.t.
$\mathfrak{v}(x)\subseteq\\{\mathsf{I},\ell\\}$ for all $x$;

  3. 3.

$\hat{\mathfrak{v}}^{w}(t)\subseteq\hat{\mathfrak{v}}^{w}(s)$ for all language
valuations $\mathfrak{v}$ and words $w$.

###### Proof.

As with Thm. 12 (use the above, instead of Cor. 11). ∎

Thm. 14 can apply to composition-free terms. We say that a term $t$ is
*composition-free if composition ($\mathbin{\cdot}$) nor Kleene-star
($\\_^{*}$) does not occur in $t$.

######  Lemma 15.

Every composition-free terms $t$ satisfies the condition $(\mathsf{L}_{1})$.

###### Proof.

By easy induction on $t$. Case $t=x,x^{-}$: By the definition of
$\mathfrak{v}^{w}$. Case $t=\mathsf{I}$: By that
$w\not\in\hat{\mathfrak{v}}(\mathsf{I})$ holds for all non-empty words $w$.
Case $t=\bot$: By $w\not\in\hat{\mathfrak{v}}(\bot)$ always. Case
$t=s\mathbin{\cup}u$: By IH, we have that
$w\in\hat{\mathfrak{v}}(s)\mathbin{\cup}\hat{\mathfrak{v}}(u)\iff
w\in\hat{\mathfrak{v}}(s)\lor
w\in\hat{\mathfrak{v}}(u)\Longrightarrow\ell\in\hat{\mathfrak{v}}^{w}(s)\lor\ell\in\hat{\mathfrak{v}}^{w}(u)\iff\ell\in\hat{\mathfrak{v}}^{w}(s)\mathbin{\cup}\hat{\mathfrak{v}}^{w}(u)$.
∎

######  Corollary 16.

The following problem is coNP-complete for KA terms with variable complements:

Given a composition-free term $t$ and a term $s$, does $\mathsf{LANG}\models
t\leq s$ hold?

###### Proof.

(coNP-hard): By Cor. 6, as $t$ is possibly $\mathsf{I}$. (in coNP): By Thm. 14
with Lem. 15, we can give an algorithm (from the condition 2 of Thm. 14) as
with Cor. 13. ∎

######  Remark 17.

Lem. 15 fails for non-composition-free terms. For example, when
$\mathfrak{v}(x)=\\{a\\}$, we have

$\displaystyle aa\in\hat{\mathfrak{v}}(xx)$
$\displaystyle\ell\not\in\hat{\mathfrak{v}}^{aa}(xx).$

(Note that $\hat{\mathfrak{v}}^{aa}(xx)=\emptyset$, as
$\hat{\mathfrak{v}}^{aa}(x)=\emptyset$ by $\mathfrak{v}(x)=\\{a\\}$.)

###  4.2 The universality problem

The _universality problem_ is the following problem:

Given a term $t$, does $\mathsf{LANG}\models\top\leq t$?

As a consequence of Cor. 16, the universality problem is also decidable and
coNP-complete.

######  Corollary 18.

The universality problem is decidable and coNP-complete for KA terms with
variable complements.

###### Proof.

(in coNP): We can apply Cor. 16 because the term $x\mathbin{\cup}x^{-}$ is
composition-free and $\mathsf{LANG}\models\top=x\mathbin{\cup}x^{-}$ holds.
(coNP-hard): Similar to Cor. 13. Given a propositional formula $\varphi$ in
disjunctive normal form, let $t$ be the term obtained by the translation in
Cor. 6; so, we have that $\varphi$ is valid iff
$\mathsf{LANG}\models\mathsf{I}\leq t$. Then we also have that
$\mathsf{LANG}\models\mathsf{I}\leq t$ iff
$\mathsf{LANG}\models\top\leq\top\mathbin{\cdot}t$, which is proved as
follows. $\Longrightarrow$: By the congruence law. $\Longleftarrow$: We prove
the contraposition. Assume $\mathsf{LANG}\not\models\mathsf{I}\leq t$; then
$\mathsf{I}\not\in\hat{\mathfrak{v}}(t)$ for some language valuation
$\mathfrak{v}$. Then
$\mathsf{I}\not\in\hat{\mathfrak{v}}(\top\mathbin{\cdot}t)$ holds; thus,
$\mathsf{LANG}\not\models\top\leq\top\mathbin{\cdot}t$. Hence, the
universality problem is coNP-complete. ∎

######  Remark 19.

In the standard language equivalence, because $[\mathbf{V}^{*}]=[\top]$ (and
the constant $\top$ is usually not a primitive symbol of regular expressions),
the universality problem is always of the form: $[\mathbf{V}^{*}]=[t]$.
However, $\mathsf{LANG}\models\mathbf{V}^{*}\leq t$ is different from
$\mathsf{LANG}\models\top\leq t$, as
$\mathsf{LANG}\not\models\mathbf{V}^{*}=\top$.

######  Remark 20.

Under the standard language equivalence, the universality problem—given a term
$t$, does $[\top]\subseteq[t]$? (i.e., does $[t]=\mathbf{V}^{*}$?)—is PSPACE-
hard [9, 13, 6]. Hence, for KA terms with variable complements, the
universality problem w.r.t. languages is strictly easier (cf. Remark 7) than
that under the standard language equivalence unless NP = PSPACE.

##  5 The word inclusion problem

Let $\mathbf{V}^{\prime}=\\{x,x^{-}\mid x\in\mathbf{V}\\}$. The _word
inclusion problem_ is the following problem:

Given a word $w$ over $\mathbf{V}^{\prime}$ and a term $t$, does
$\mathsf{LANG}\models w\leq t$?

As Remark 17 shows, we cannot apply the method given in Sect. 4
straightforwardly. Nevertheless, we can solve this problem by generalizing the
language valuation of Def. 8, as follows. The valuations in Defs. 8, 21 are
given by the first author.

######  Definition 21 (*words-to-letters valuations).

For a language valuation $\mathfrak{v}$ over a set $X$ and words
$w_{0},\dots,w_{n-1}$ over $X$ (where $n\geq 0$), the language valuation
$\mathfrak{v}^{\langle w_{0},\dots,w_{n-1}\rangle}$ over the set
$\\{\ell_{0},\dots,\ell_{n-1}\\}$ (where $\ell_{0},\dots,\ell_{n-1}$ are
pairwise distinct letters) is defined as follows:

$\mathfrak{v}^{\langle
w_{0},\dots,w_{n-1}\rangle}(x)\quad\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\quad\\{\ell_{i}\dots\ell_{j-1}\mid
0\leq i\leq j\leq n\ \land\ w_{i}\dots w_{j-1}\in\mathfrak{v}(x)\\}.$

(Note that the language valuation $\mathfrak{v}^{w}$ (Def. 8) is the case
$n=1$ of Def. 21 and the language valuation $\mathfrak{v}^{\langle\rangle}$ in
the proof of Thm. 5 is the case $n=0$ of Def. 21.)

By using words-to-letters valuations, we can naturally strengthen the results
in Sect. 4 from variables to words. We prepare the following fact:

######  Proposition 22 (cf. Prop. 9).

For all languages $L,K$ and words $w$,

$\displaystyle w\in L\mathbin{\cup}K$ $\displaystyle\quad\iff\quad w\in L\lor
w\in K$ $\displaystyle w\in L\mathbin{\cdot}K$
$\displaystyle\quad\iff\quad\exists v,v^{\prime}\mbox{ s.t.\ }w=vv^{\prime},\
v\in L\land v^{\prime}\in K$ $\displaystyle w\in L^{*}$
$\displaystyle\quad\iff\quad\exists n\in{\rm Nature},\exists
v_{0},\dots,v_{n-1}\mbox{ s.t.\ }w=v_{0}\dots v_{n-1},\forall i<n,\ v_{i}\in
L.$

###### Proof.

By definition. ∎

######  Lemma 23 (cf. Lem. 10).

Let $\mathfrak{v}$ be a language valuation and $w_{0},\dots,w_{n-1}$ be words
(where $n\geq 0$). For all terms $t$ and $0\leq i\leq j\leq n$, we have:

$\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t)\quad\Longrightarrow\quad w_{i}\dots
w_{j-1}\in\hat{\mathfrak{v}}(t).$

###### Proof.

By induction on $t$.

Case $t=x,x^{-}$: By the construction of $\mathfrak{v}^{\langle
w_{0},\dots,w_{n-1}\rangle}$,
$\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(x)$ iff $w_{i}\dots
w_{j-1}\in\hat{\mathfrak{v}}(x)$. (Hence, we also have
$\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(x^{-})$ iff $w_{i}\dots
w_{j-1}\in\hat{\mathfrak{v}}(x^{-})$.)

Case $t=\bot$, Case $t=\mathsf{I}$ where $i<j$: By
$\ell_{i}\dots\ell_{j-1}\not\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t)$.

Case $t=\mathsf{I}$ where $i=j$: By
$\mathsf{I}\in\hat{\mathfrak{v}}(\mathsf{I})$.

Case $t=s\mathbin{\cup}u$: We have

$\displaystyle\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s\mathbin{\cup}u)$
$\displaystyle\Longleftrightarrow\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s)\lor\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(u)$ (Prop. 22) $\displaystyle\Longrightarrow
w_{i}\dots w_{j-1}\in\hat{\mathfrak{v}}(s)\lor w_{i}\dots
w_{j-1}\in\hat{\mathfrak{v}}(u)$ (IH) $\displaystyle\Longrightarrow w_{i}\dots
w_{j-1}\in\hat{\mathfrak{v}}(s\mathbin{\cup}u).$

Case $t=s\mathbin{\cdot}u$: We have

$\displaystyle\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s\mathbin{\cdot}u)$
$\displaystyle\Longleftrightarrow\bigvee_{i\leq k\leq
j}(\ell_{i}\dots\ell_{k-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s)\land\ell_{k}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(u))$ (Prop. 22)
$\displaystyle\Longrightarrow\bigvee_{i\leq k\leq j}(w_{i}\dots
w_{k-1}\in\hat{\mathfrak{v}}(s)\land w_{k}\dots
w_{j-1}\in\hat{\mathfrak{v}}(u))$ (IH) $\displaystyle\Longrightarrow
w_{i}\dots w_{j-1}\in\hat{\mathfrak{v}}(s\mathbin{\cdot}u).$

Case $t=s^{*}$: We have

$\displaystyle\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s^{*})$ $\displaystyle\Longleftrightarrow\exists
m\in{\rm Nature},\bigvee_{i=k_{0}\leq k_{1}\leq\dots\leq
k_{m}=j}\bigwedge_{l=1}^{m}(\ell_{k_{l-1}}\dots\ell_{k_{l}-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s))$ (Prop. 22)
$\displaystyle\Longrightarrow\exists m\in{\rm Nature},\bigvee_{i=k_{0}\leq
k_{1}\leq\dots\leq k_{m}=j}\bigwedge_{l=1}^{m}(w_{k_{l-1}}\dots
w_{k_{l}-1}\in\hat{\mathfrak{v}}(s))$ (IH) $\displaystyle\Longrightarrow
w_{i}\dots w_{j-1}\in\hat{\mathfrak{v}}(s^{*}).$

∎

######  Corollary 24 (cf. Cor. 11).

Let $\mathfrak{v}$ be a language valuation, $w$ be a word,
$w_{0},\dots,w_{n-1}$ be words s.t. $w=w_{0}\dots w_{n-1}$. For all words $v$
over $\mathbf{V}^{\prime}$ of length $n$ and all terms $t$,

$w\in\hat{\mathfrak{v}}(v)\setminus\hat{\mathfrak{v}}(t)\quad\Longrightarrow\quad\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(v)\setminus\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t).$

###### Proof.

For $\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(v)$: Let $v=x_{0}\dots x_{n-1}$. For each $i<n$,
by the construction of $\mathfrak{v}^{\langle w_{0},\dots,w_{n-1}\rangle}$,
$\ell_{i}\in\hat{\mathfrak{v}}^{\langle w_{0},\dots,w_{n-1}\rangle}(x_{i})$
iff $w_{i}\in\hat{\mathfrak{v}}(x_{i})$. Thus, we have that
$\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(v)$. For
$\ell_{0}\dots\ell_{n-1}\not\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t)$: By Lem. 23. ∎

######  Theorem 25 (cf. Thm. 12).

For all words $v$ over $\mathbf{V}^{\prime}$ of length $n$ and all terms $t$,
the following are equivalent:

  1. 1.

$\mathsf{LANG}\models v\leq t$;

  2. 2.

$\hat{\mathfrak{v}}(v)\subseteq\hat{\mathfrak{v}}(t)$ for all language
valuations $\mathfrak{v}$ s.t.
$\mathfrak{v}(x)\subseteq\\{\ell_{i}\dots\ell_{j}\mid 0\leq i\leq j\leq n\\}$
for all $x$;

  3. 3.

$\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(v)\subseteq\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t)$ for all language valuations $\mathfrak{v}$ and
words $w_{0},\dots,w_{n-1}$.

###### Proof.

1$\Rightarrow$2, 2$\Rightarrow$3: Trivial. 3$\Rightarrow$1: The contraposition
is shown by Cor. 24. ∎

######  Corollary 26 (cf. Cor. 13).

The word inclusion problem (given a word $w$ and a term $t$, does
$\mathsf{LANG}\models w\leq t$?) is decidable and coNP-complete for KA terms
with variable complements.

###### Proof.

(coNP-hard): By Cor. 6, as $w$ is possibly $\mathsf{I}$. (in coNP): By the
condition 2 of Thm. 25, we can give an algorithm as with Cor. 13. ∎

###  5.1 Generalization from words to star-free terms

We can apply Thm. 25 to not only words over $\mathbf{V}^{\prime}$ but also
terms $t$ having the following property:

For all language valuations $\mathfrak{v}$ and non-empty words $w$, for some
$w_{0},\dots,w_{n-1}$ s.t. $w=w_{0}\dots w_{n-1}$, $\displaystyle
w\in\hat{\mathfrak{v}}(t)\Longrightarrow\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t).$ $(\mathsf{L}_{n})$

If $t$ satisfies the condition $(\mathsf{L}_{n})$, then combining with Lem. 23
(and with Lem. 4 for the empty word $\mathsf{I}$) yields that for all language
valuations $\mathfrak{v}$ and words $w$, for some words $w_{0},\dots,w_{n-1}$
s.t. $w=w_{0}\dots w_{n-1}$, we have:

$\displaystyle w\in\hat{\mathfrak{v}}(t)\setminus\hat{\mathfrak{v}}(s)$
$\displaystyle\quad\Longrightarrow\quad\begin{cases}\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t)\setminus\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s)&(\mbox{if $w\neq\mathsf{I}$})\\\
\mathsf{I}\in\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t)\setminus\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s)&(\mbox{if $w=\mathsf{I}$})\end{cases}.$

Hence, we have the following:

######  Theorem 27 (cf. Thm. 14).

For all terms $t,s$, if $t$ satisfies $(\mathsf{L}_{n})$, the following are
equivalent:

  1. 1.

$\mathsf{LANG}\models t\leq s$;

  2. 2.

$\hat{\mathfrak{v}}(t)\subseteq\hat{\mathfrak{v}}(s)$ for all language
valuations $\mathfrak{v}$ over the set $\\{\ell_{0},\dots,\ell_{n-1}\\}$ s.t.
$\mathfrak{v}(x)\subseteq\\{\ell_{i}\dots\ell_{j}\mid 0\leq i\leq j\leq n\\}$
for all $x$;

  3. 3.

$\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t)\subseteq\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s)$ for all language valuations $\mathfrak{v}$ and
words $w_{0},\dots,w_{n-1}$.

###### Proof.

As with Thm. 25 (use the above, instead of Cor. 24). ∎

By using Thm. 27, we can generalize Cor. 26 from words to star-free terms. We
say that a term $t$ is *star-free if the Kleene-star ($\\_^{*}$) does not
occur in $t$.

######  Lemma 28 (cf. Lem. 15).

Every star-free term $t$ satisfies $(\mathsf{L}_{n})$ for some $n$.

###### Proof.

Because the set $[t]_{\mathbf{V}^{\prime}}$ is finite as $t$ is star-free, let
$n$ be the maximal length among words in $[t]_{\mathbf{V}^{\prime}}$. Let
$\mathfrak{v}$ be a language valuation and let $w$ be a non-empty word such
that $w\in\hat{\mathfrak{v}}(t)$. Since
$\hat{\mathfrak{v}}(t)=\hat{\mathfrak{v}}([t]_{\mathbf{V}^{\prime}})$ (Lem.
2), there is a word $v\in[t]_{\mathbf{V}^{\prime}}$ such that
$w\in\hat{\mathfrak{v}}(v)$. Let $v=x_{0}\dots x_{m-1}$ (note that $m\geq 1$,
as $w$ is non-empty and $w\in\hat{\mathfrak{v}}(v)$). Since
$w\in\hat{\mathfrak{v}}(x_{0}\dots x_{m-1})$, there are $w_{0},\dots,w_{m-1}$
of $w=w_{0}\dots w_{m-1}$ such that $w_{i}\in\hat{\mathfrak{v}}(x_{i})$ for
every $i$. Let
$\mathfrak{v}^{\prime}\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\mathfrak{v}^{\langle
w_{0},\dots,w_{m-1},\mathsf{I},\dots,\mathsf{I}\rangle}$, where the length of
the sequence is $n$. Then, we have
$\ell_{i}\in\hat{\mathfrak{v}}^{\prime}(x_{i})$ for every $0\leq i\leq m-2$
and
$\ell_{m-1}\ell_{m}\dots\ell_{n-1}\in\hat{\mathfrak{v}}^{\prime}(x_{m-1})$;
thus, $\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}^{\prime}(x_{0}\dots
x_{m-1})=\hat{\mathfrak{v}}^{\prime}(v)\subseteq\hat{\mathfrak{v}}^{\prime}(t)$.
Hence, this completes the proof. ∎

######  Corollary 29.

The following problem is coNP-complete for KA terms with variable complements:

Given a star-free term $t$ and a term $s$, does $\mathsf{LANG}\models t\leq
s$?

###### Proof.

(coNP-hard): By Cor. 6, as $t$ is possibly $\mathsf{I}$. (in coNP): By Lem.
28, we can give an algorithm as with Cor. 26. ∎

###  5.2 words-to-letters valuation property

Finally, we show the following property; thus, we have that words-to-letters
valuations are sufficient for the equational theory of (full) KA terms with
variable complements.

######  Corollary 30 (words-to-letters valuation property).

For all terms $t,s$, the following are equivalent:

  1. 1.

$\mathsf{LANG}\not\models t\leq s$;

  2. 2.

there is a words-to-letters valuation $\mathfrak{v}$ such that
$\hat{\mathfrak{v}}(t)\not\subseteq\hat{\mathfrak{v}}(s)$.

###### Proof.

2$\Rightarrow$1: Trivial. 1$\Rightarrow$2: Since $\mathsf{LANG}\not\models
t\leq s$, there is a language valuation $\mathfrak{v}$ such that
$\hat{\mathfrak{v}}(t)\not\subseteq\hat{\mathfrak{v}}(s)$. Since
$\hat{\mathfrak{v}}(t)=\hat{\mathfrak{v}}([t]_{\mathbf{V}^{\prime}})$ (Lem.
2), there is a word $v\in[t]_{\mathbf{V}^{\prime}}$ such that
$\hat{\mathfrak{v}}(v)\not\subseteq\hat{\mathfrak{v}}(s)$ (i.e.,
$\mathsf{LANG}\not\models v\leq s$). Let $n$ be the length of $v$. By Thm. 25,
there are a words-to-letters valuation $\mathfrak{v}$ and words
$w_{0},\dots,w_{n-1}$ such that $\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(v)\not\subseteq\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s)$. Thus $\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(t)\not\subseteq\hat{\mathfrak{v}}^{\langle
w_{0},\dots,w_{n-1}\rangle}(s)$, as $v\in[t]_{\mathbf{V}^{\prime}}$ (Lem. 2).
Hence this completes the proof. ∎

##  6 On the equational theory of words with variable complements

We prove that the equational theory of words over $\mathbf{V}^{\prime}$
coincides with the word equivalence (Thm. 32). We give language valuations for
separating two distinct words based on words-to-letters valuations.

######  Lemma 31.

Let $w=x_{0}\dots x_{n-1}$ and $v=y_{0}\dots y_{m-1}$ be words over
$\mathbf{V}^{\prime}$, where $n\leq m$. Let $\mathfrak{v}$ be a language
valuation over $\\{\ell_{0},\dots,\ell_{n-1}\\}$ such that

  * •

for all $i<n$, $\ell_{i}\in\hat{\mathfrak{v}}(x_{i})$;

  * •

for all $i<m$ and $i\leq j\leq n$,
$\ell_{i}\dots\ell_{j-1}\in\hat{\mathfrak{v}}(y_{i})$ iff $(y_{i}=x_{i}\land
j=i+1)$.

If $w\neq v$, then
$\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}(w)\setminus\hat{\mathfrak{v}}(v)$.
Such a language valuation $\mathfrak{v}$ always exists.

###### Proof.

Since $\ell_{i}\in\mathfrak{v}(x_{i})$ for all $i$, we have
$\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}(w)$. Assume that
$\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}(y_{0}\dots y_{m-1})$. For $i=0$,
by the condition of $\hat{\mathfrak{v}}(y_{i})$ (i.e.,
$\ell_{i}\dots\ell_{j-1}\not\in\hat{\mathfrak{v}}(y_{i})$ unless $j=i+1$), we
should have $\ell_{i}\in\hat{\mathfrak{v}}(y_{i})$,
$\ell_{i+1}\dots\ell_{n-1}\in\hat{\mathfrak{v}}(y_{i+1}\dots y_{m-1})$, and
$y_{i}=x_{i}$. By using the same argument iteratively, the condition above
should hold for all $i<n$; thus, we have
$\mathsf{I}\in\hat{\mathfrak{v}}(y_{n}\dots y_{m-1})$ and $y_{0}\dots
y_{n-1}=x_{0}\dots x_{m-1}$. Since
$\mathsf{I}\not\in\hat{\mathfrak{v}}(y_{n})$, we have $y_{n}\dots
y_{m-1}=\mathsf{I}$; thus, $m=n$. However this yields $w=x_{0}\dots
x_{n-1}=y_{0}\dots y_{m-1}=v$, which contradicts the assumption. Hence
$\ell_{0}\dots\ell_{n-1}\in\hat{\mathfrak{v}}(w)\setminus\hat{\mathfrak{v}}(v)$.
Additionally, such a language valuation $\mathfrak{v}$ always exists as
follows. If some conditions conflict, then the first condition
($\ell_{i}\in\hat{\mathfrak{v}}(x_{i})$) and the second condition when $j=i+1$
($\ell_{i}\in\hat{\mathfrak{v}}(y_{i})$) are for some $i$. If $y_{i}=x_{i}$,
then $\ell_{i}\in\hat{\mathfrak{v}}(y_{i})=\hat{\mathfrak{v}}(x_{i})$, so it
does not conflict to the condition $\ell_{i}\in\hat{\mathfrak{v}}(x_{i})$; If
$y_{i}=x_{i}^{-}$ (or $y_{i}^{-}=x_{i}$), then
$\ell_{i}\not\in\hat{\mathfrak{v}}(y_{i})$, so it does not conflict to the
condition $\ell_{i}\in\hat{\mathfrak{v}}(x_{i})$. Otherwise, they are not
conflicted, as the variables occurring in $x_{i}$ and $y_{i}$ are different.
Thus, in either case, conditions are not conflicted. Hence, this completes the
proof. ∎

######  Theorem 32 (Completeness for words with variable complements).

For all words $w,v$ over $\mathbf{V}^{\prime}$,

$\mathsf{LANG}\models w=v\quad\iff\quad w=v.$

###### Proof.

$\Longleftarrow$: Clear. $\Longrightarrow$: The contraposition is shown by
Lem. 31. ∎

######  Remark 33.

Since $[w]_{\mathbf{V}^{\prime}}=\\{w\\}$, Thm. 32 also shows that: for all
words $w,v$ over $\mathbf{V}^{\prime}$,

$[w]_{\mathbf{V}^{\prime}}=[v]_{\mathbf{V}^{\prime}}\quad\iff\quad\mathsf{LANG}\models
w=v.$

However, for general terms, the direction $\Longleftarrow$ fails: For example,
when $x\neq y$,

$\displaystyle\mathsf{LANG}$ $\displaystyle\models
x\mathbin{\cup}x^{-}=y\mathbin{\cup}y^{-}$
$\displaystyle[x\mathbin{\cup}x^{-}]_{\mathbf{V}^{\prime}}\neq[y\mathbin{\cup}y^{-}]_{\mathbf{V}^{\prime}}.$

(The direction $\Longrightarrow$ always holds by Lem. 2.) Thus, we need more
axioms to characterize the equational theory.

######  Remark 34.

As ($\ddagger$ ‣ 2.2) and Remark 1, for all words $w,v$ over
$\mathbf{V}^{\prime}$,

$\mathsf{LANG}\models w=v\quad\Longrightarrow\quad[w]=[v].$

However, the converse direction fails even for words (e.g., $w=x^{-}$ and
$v=x^{-}x^{-}$).

###  6.1 Separating one-variable words with small number of letters

We write $\mathsf{LANG}_{n}$ for the class of language models over a set of
cardinality at most $n$. We write

$\mathsf{LANG}_{n}\models
t=s\quad\mathrel{\ensurestackMath{\stackon[1pt]{\iff}{\scriptscriptstyle\Delta}}}\quad\hat{\mathfrak{v}}(t)=\hat{\mathfrak{v}}(s)\mbox{
holds for all \kl{(language) valuations} $\mathfrak{v}$ on \kl{$S$-algebras}
in $\mathsf{LANG}_{n}$}.$

Notice that words-to-letters valuations need an unbounded number of letters;
so the proof of Thm. 32 cannot directly apply to the class
$\mathsf{LANG}_{n}$. Nevertheless, for _one-variable_ words (i.e., words over
the set $\\{z,z^{-}\\}$ where $z$ is a variable), we can show completeness
theorems (cf. Thm. 32) of the equational theory over $\mathsf{LANG}_{n}$, as
Thms. 35, 36. The valuation in the proof of Thm. 36 is given by the second
author.

For a word $w=x_{0}\dots x_{n-1}\in\\{z,z^{-}\\}^{*}$ and $x\in\\{z,z^{-}\\}$,
we write $\|w\|_{x}$ for the number $\\#(\\{0\leq i<n\mid x_{i}=x\\})$. For a
letter $a$ and $n\in{\rm Nature}$, we write $a^{n}$ for the word $a\dots a$ of
length $n$.

######  Theorem 35.

For all words $w,v\in\\{z,z^{-}\\}^{*}$, we have:

$\mathsf{LANG}_{1}\models
w=v\quad\iff\quad\|w\|_{z}=\|v\|_{z}\;\land\;\|w\|_{z^{-}}=\|v\|_{z^{-}}.$

###### Proof.

$\Longleftarrow$: By the following commutative law: for all language
valuations $\mathfrak{v}$ over a set of cardinality at most $1$,
$\hat{\mathfrak{v}}(zz^{-})=\hat{\mathfrak{v}}(z^{-}z)$. $\Longrightarrow$: If
$\|w\|_{z}<\|v\|_{z}$, then let $\mathfrak{v}$ be the language valuation
defined by $\mathfrak{v}(z)=\\{a\\}$. Then
$a^{\|w\|_{z}}\in\hat{\mathfrak{v}}(w)\setminus\hat{\mathfrak{v}}(v)$; thus
$\mathsf{LANG}_{1}\not\models w=v$. If $\|w\|_{z^{-}}<\|v\|_{z^{-}}$, then let
$\mathfrak{v}$ be the language valuation defined by
$\mathfrak{v}(z)=\\{a\\}^{*}\setminus\\{a\\}$. Then
$a^{\|w\|_{z^{-}}}\in\hat{\mathfrak{v}}(w)\setminus\hat{\mathfrak{v}}(v)$. If
$\|w\|_{z}>\|v\|_{z}$ (resp. $\|w\|_{z^{-}}>\|v\|_{z^{-}}$), then similarly to
the cases above. ∎

######  Theorem 36.

For all words $w,v\in\\{z,z^{-}\\}^{*}$, we have:

$\mathsf{LANG}_{2}\models w=v\quad\iff\quad\mathsf{LANG}\models
w=v\quad\iff\quad w=v.$

###### Proof.

The two $\Longleftarrow$ are clear by definition. We prove $w\neq
v\Longrightarrow\mathsf{LANG}_{2}\not\models w=v$. By Thm. 35, it suffices to
show the case when $\|w\|_{z}=\|v\|_{z}$ and $\|w\|_{z^{-}}=\|v\|_{z^{-}}$.
Let
$n\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\|w\|_{z^{-}}=\|v\|_{z^{-}}$
and let $w,v$ be as follows:

$\displaystyle w$ $\displaystyle=z^{c_{0}}z^{-}z^{c_{1}}\dots z^{-}z^{c_{n}}$
$\displaystyle v$ $\displaystyle=z^{d_{0}}z^{-}z^{d_{1}}\dots z^{-}z^{d_{n}}.$

Since $w\neq v$, there is $i\leq n$ such that $c_{j}=d_{j}$ for all $j<i$ and
$c_{i}\neq d_{i}$. Without loss of generality, we can assume $c_{i}<d_{i}$.
Now, we consider the following language valuation $\mathfrak{v}$ over
$A\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}\\{a,b\\}$:

$\displaystyle\mathfrak{v}(z)$
$\displaystyle\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptscriptstyle\Delta}}}[(aA^{*})\cap(A^{*}a)]=\\{c_{0}\dots
c_{n-1}\in\\{a,b\\}^{*}\mid n\geq 1,c_{0}=a,c_{n-1}=a\\}.$

Then
$a^{(\sum_{j=0}^{i}c_{j})}ba^{(\sum_{j=i+1}^{n}c_{j})}\in\hat{\mathfrak{v}}(w)$,
as $a\in\hat{\mathfrak{v}}(z)$ and $\mathsf{I},b\in\hat{\mathfrak{v}}(z^{-})$.
Assume, towards contradiction, that
$a^{(\sum_{j=0}^{i}c_{j})}ba^{(\sum_{j=i+1}^{n}c_{j})}\in\hat{\mathfrak{v}}(v)$.
Each $z$ occurring in $v$ should map to $a$, as
$(\sum_{j=0}^{n}c_{j})=(\sum_{j=0}^{n}d_{j})$ and every word in
$\mathfrak{v}(z)$ except for $a$ has at least two occurrences of $a$. The
$(\sum_{j=0}^{i}c_{j})$-th occurrence and $((\sum_{j=0}^{i}c_{j})+1)$-th
occurrence of $z^{-}$ are adjacent (since
$(\sum_{j=0}^{i}c_{j})<(\sum_{j=0}^{i}d_{j})$). Combining them yields
$b\in\hat{\mathfrak{v}}(\mathsf{I})$, thus reaching a contradiction. Hence,
$a^{(\sum_{j=0}^{i}c_{j})}ba^{(\sum_{j=i+1}^{n}c_{j})}\in\hat{\mathfrak{v}}(w)\setminus\hat{\mathfrak{v}}(v)$.
This completes the proof. ∎

The proof of Thms. 35, 36 only applies to one-variable words. We leave open
Thms. 35, 36 for many variables words (cf. Thm. 32).

##  7 Conclusion and future work

We have introduced words-to-letters valuations. By using them, we have shown
the decidability and complexity of the identity/variable/word inclusion
problems (Cors. 6, 13, 26) and the universality problem (Cor. 18) of the
equational theory of KA terms with variable complements w.r.t. languages; in
particular, the inequational theory $t\leq s$ is coNP-complete when $t$ does
not contain Kleene-star (Cor. 29). Additionally, we have proved a completeness
theorem for words with variable complements w.r.t. languages (Thm. 32);
moreover, for one-variable words, the equational theory over $\mathsf{LANG}$
coincides with that over $\mathsf{LANG}_{2}$ (Thm. 36).

A natural interest is to extend our decidability results, e.g., for full KA
terms with variable complements. As Cor. 30 shows, even for full terms, words-
to-letters valuations are sufficient valuations in investigating the
equational theory. The first author conjectures that the equational theory of
KA terms with variable complements is decidable, possibly by combining the
technique like _saturable paths_ [10] (which were introduced for the
equational theory w.r.t. binary relations). Additionally, we leave open the
(finite) axiomatizability of the equational theory (including that over sets
of bounded cardinality; cf. Sect. 6.1).

## Acknowledgement

We would like to thank the anonymous reviewers for their useful comments. This
work was supported by JSPS KAKENHI Grant Number JP21K13828 and JST ACT-X Grant
Number JPMJAX210B, Japan.

## References

  * [1]
  * [2] Hajnal Andréka, Szabolcs Mikulás & István Németi (2011): _The equational theory of Kleene lattices_.  Theoretical Computer Science 412(52), pp. 7099–7108, 10.1016/J.TCS.2011.09.024.
  * [3] S. L. Bloom, Z. Ésik & Gh. Stefanescu (1995): _Notes on equational theories of relations_.  algebra universalis 33(1), pp. 98–126, 10.1007/BF01190768.
  * [4] John H. Conway (1971): _Regular Algebra and Finite Machines_.  Chapman and Hall.
  * [5] Stephen A. Cook (1971): _The complexity of theorem-proving procedures_.  In: STOC, ACM, p. 151–158, 10.1145/800157.805047.
  * [6] Harry B. Hunt III, Daniel J. Rosenkrantz & Thomas G. Szymanski (1976): _On the equivalence, containment, and covering problems for the regular and context-free languages_.  Journal of Computer and System Sciences 12(2), pp. 222–268, 10.1016/S0022-0000(76)80038-4.
  * [7] S. C. Kleene (1951): _Representation of Events in Nerve Nets and Finite Automata_.  Technical Report, RAND Corporation.  Available at https://www.rand.org/pubs/research_memoranda/RM704.html.
  * [8] Dexter Kozen & Frederick Smith (1996): _Kleene algebra with tests: Completeness and decidability_.  In: CSL, LNCS 1258, Springer, pp. 244–259, 10.1007/3-540-63172-0_43.
  * [9] A. R. Meyer & L. J. Stockmeyer (1972): _The equivalence problem for regular expressions with squaring requires exponential space_.  In: SWAT, IEEE, pp. 125–129, 10.1109/SWAT.1972.29.
  * [10] Yoshiki Nakamura (2023): _Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations_.  In: LICS, IEEE, pp. 1–13, 10.1109/LICS56636.2023.10175811.
  * [11] Kan Ching Ng (1984): _Relation algebras with transitive closure_.  Ph.D. thesis, University of California.
  * [12] Damien Pous & Jana Wagemaker (2022): _Completeness Theorems for Kleene Algebra with Top_.  In: CONCUR, 243, Schloss Dagstuhl, pp. 26:1–26:18, 10.4230/LIPICS.CONCUR.2022.26.
  * [13] Larry J. Stockmeyer & Albert R. Meyer (1973): _Word problems requiring exponential time (Preliminary Report)_.  In: STOC, ACM, pp. 1–9, 10.1145/800125.804029.
  * [14] Alfred Tarski (1941): _On the Calculus of Relations_.  The Journal of Symbolic Logic 6(3), pp. 73–89, 10.2307/2268577.
  * [15] Ken Thompson (1968): _Programming Techniques: Regular expression search algorithm_.  Communications of the ACM 11(6), pp. 419–422, 10.1145/363347.363387.

##  Appendix A A direct proof of the coincidence between the equational theory
w.r.t. languages and the language equivalence for KA terms

(In this section, we use the notations of Sect. 2.)

We say that a term $t$ is a *KA term if the complement ($\\_^{-}$) does not
occur in $t$. Recall language valuations for languages in Sect. 2.3.

######  Lemma 37 (cf. Lem. 2).

Let $\mathfrak{v}$ be a language valuation. For all KA terms $t$, we have

$\hat{\mathfrak{v}}(t)\quad=\quad\hat{\mathfrak{v}}([t]).$

###### Proof.

By Lem. 2, as $[t]=[t]_{\mathbf{V}^{\prime}}$ (since KA terms do not contain
the complement). ∎

######  Theorem 38.

For all KA terms $t,s$,

$\mathsf{LANG}\models t=s\quad\iff\quad[t]=[s].$

###### Proof.

We have

$\displaystyle\mathsf{LANG}\models t=s$
$\displaystyle\quad\Longrightarrow\quad[t]=[s]$ ($[\\_]$ is an instance of
language valuations) $\displaystyle\quad\Longrightarrow\quad\mbox{for all
\kl{language valuations}
$\mathfrak{v}$},\hat{\mathfrak{v}}([t])=\hat{\mathfrak{v}}([s])$
$\displaystyle\quad\Longleftrightarrow\quad\mbox{for all \kl{language
valuations} $\mathfrak{v}$},\hat{\mathfrak{v}}(t)=\hat{\mathfrak{v}}(s)$ (Lem.
37) $\displaystyle\quad\Longleftrightarrow\quad\mathsf{LANG}\models t=s.$ (By
definition)

∎