Language equation

Language equations are mathematical statements that resemble numerical equations, but the variables assume values of formal languages rather than numbers. Instead of arithmetic operations in numerical equations, the variables are joined by language operations. Among the most common operations on two languages "A" and "B" are the set union "A" ∪ "B", the set intersection "A" ∩ "B", and the concatenation "A"⋅"B". Finally, as an operation taking a single operand, the set "A"* denotes the Kleene star of the language "A". Therefore language equations can be used to represent formal grammars, since the languages generated by the grammar must be the solution of a system of language equations.
Language equations and context-free grammars.
Ginsburg and Rice
gave an alternative definition of context-free grammars by language equations. To every context-free grammar formula_1, is associated a system of equations in variables formula_2. Each variable formula_3 is an unknown language over formula_4 and is defined by the equation formula_5 where formula_6, ..., formula_7 are all productions for formula_8. Ginsburg and Rice used a fixed-point iteration argument to show that a solution always exists, and proved that i.e. any other solution must be a of this one.
For example, the grammar 
formula_9
corresponds to the equation system
formula_10
which has as solution every superset of formula_11.
Language equations with added intersection analogously correspond to conjunctive grammars.
Language equations and finite automata.
Brzozowski and Leiss studied "left language equations" where every concatenation is with a singleton constant language on the left, e.g. formula_12 with variable formula_8, but not formula_14 nor formula_15. Each equation is of the form formula_16 with one variable on the right-hand side. Every nondeterministic finite automaton has such corresponding equation using left-concatenation and union, see Fig. 1. If intersection operation is allowed, equations correspond to alternating finite automata.
Baader and Narendran studied equations formula_17 using left-concatenation and union and proved that their satisfiability problem is EXPTIME-complete.
Conway's problem.
Conway proposed the following problem: given a constant finite language formula_18, is the greatest solution of the equation formula_19 always regular? This problem was studied by Karhumäki and Petre who gave an affirmative answer in a special case. A strongly negative answer to Conway's problem was given by Kunc who constructed a finite language formula_18 such that the greatest solution of this equation is not recursively enumerable.
Kunc also proved that the greatest solution of inequality formula_21 is always regular.
Language equations with Boolean operations.
Language equations with concatenation and Boolean operations were first studied by Parikh, Chandra, Halpern and Meyer
 who proved that the satisfiability problem for a given equation is undecidable, and that if a system of language equations has a unique solution, then that solution is recursive. Later, Okhotin proved that the unsatisfiability problem is RE-complete and that every recursive language is a unique solution of some equation.
Language equations over a unary alphabet.
For a one-letter alphabet, Leiss discovered the first language equation with a nonregular solution, using complementation and concatenation operations. Later, Jeż showed that non-regular unary languages can be defined by language equations with union, intersection and concatenation, equivalent to conjunctive grammars. By this method Jeż and Okhotin proved that every recursive unary language is a unique solution of some equation.