A formal grammar is a free monoidal category with words and rules as boxes.

Formal grammars are also known as string rewriting or semi-Thue systems, they were introduced by Thue [Thu14], see [Pow13] for a translation.

The parsing problem is to decide, given two strings, whether there exists a diagram from one to the other. It has been shown to be undecidable by Post [Pos47] and Markov [Mar47].



A word is a rule with a name, a grammatical type as cod and an optional domain dom.


A rule is a box with monoidal types as dom and cod and an optional name.


>>> s, n, v, p = map(Ty, "SNVP")
>>> r0, r1 = Rule(n @ p, s), Rule(v @ n, p)
>>> Jane, loves, John = Word('Jane', n), Word('loves', v), Word('John', n)
>>> sentence = Jane @ loves @ John >> n @ r1 >> r0
>>> sentence.draw(figsize=(4, 3), path='docs/_static/grammar/cfg-example.png')