In theoretical computer science and mathematics, especially in the area of combinatorics on words, the Levi lemma states that, for all strings u, v, x and y, if uv = xy, then there exists a string w such that either
- uw = x and v = wy (if |u| ≤ |x|)
- u = xw and wv = y (if |u| ≥ |x|)
Levi's lemma can be applied repeatedly in order to solve word equations; in this context it is sometimes called the Nielsen transformation by analogy with the Nielsen transformation for groups. For example, starting with an equation xα = yβ where x and y are the unknowns, we can transform it (assuming |x| ≥ |y|, so there exists t such that x=yt) to ytα = yβ, thus to tα = β. This approach results in a graph of substitutions generated by repeatedly applying Levi's lemma. If each unknown appears at most twice, then a word equation is called quadratic; in a quadratic word equation the graph obtained by repeatedly applying Levi's lemma is finite, so it is decidable if a quadratic word equation has a solution. A more general method for solving word equations is Makanin's algorithm. 
The above is known as the Levi lemma for strings; the lemma can occur in a more general form in graph theory and in monoid theory; for example, there is a more general Levi lemma for traces originally due to Christine Duboc. Several proofs of Levi's Lemma for traces can be found in The Book of Traces.
A monoid in which Levi's lemma holds is said to have the equidivisibility property. The free monoid of strings and string concatenation has this property (by Levi's lemma for strings), but by itself equidivisibility is not enough to guarantee that a monoid is free. However an equidivisibile monoid M is free if additionally there exists a homomorphism f from M to the monoid of natural numbers (free monoid on one generator) with the property that the preimage of 0 contains only the identity element of M, i.e. . (Note that f simply being a homomorphism does not guarantee this latter property, as there could be multiple elements of M mapped to 0.) A monoid for which such a homomorphism exists is also called graded (and the f is called a gradation).
- Levi, F. W. (1944), "On semigroups", Bulletin of the Calcutta Mathematical Society, 36: 141–146, MR 0011694, Zbl 0061.02405.
- Matiyasevich, Yu. V. (1968), "A connection between systems of word and length equations and Hilbert's tenth problem", Zap. Naučn. Sem. Leningrad. Otdel. Mat. Inst. Steklov. (LOMI), 8: 132–144.
- Makanin, G. S. (1977), English transl. in Math. USSR Sbornik 32 (1977), "The problem of solvability of equations in a free semigroup", Mat. Sbornik, 103 (2): 147–236, Bibcode:1977SbMat..32..129M, doi:10.1070/SM1977v032n02ABEH002376
- M. Lothaire (2002). "12". Algebraic Combinatorics on Words. Cambridge University Press. ISBN 0-521-81220-8.
- Duboc, Chr. (1986), "On some equations in free partially commutative monoids", Theoretical Computer Science, 46: 159–174, doi:10.1016/0304-3975(86)90028-9
- Volker Diekert; Grzegorz Rozenberg, eds. (1995). The Book of Traces. World Scientific. pp. 1–576. ISBN 981-02-2058-8.
- Aldo de Luca; Stefano Varricchio (1999). Finiteness and Regularity in Semigroups and Formal Languages. Springer Berlin Heidelberg. p. 2. ISBN 978-3-642-64150-3.
- M. Lothaire (1997). Combinatorics on Words. Cambridge University Press. p. 13. ISBN 978-0-521-59924-5.
- Sakarovitch, Jacques (2009), Elements of automata theory, Translated from the French by Reuben Thomas, Cambridge: Cambridge University Press, p. 26, ISBN 978-0-521-84425-3