feat: Dyck words

[Parcly-Taxel]

---

[trivial1711]

Do you have a reference that uses the term "Dyck path" to refer to any sequence of U and D? I could not find one.

What you call a "Dyck path" is really called a "word" (although it isn't really necessary to have a abbreviation for it), and what you call a "balanced Dyck path" is really called a "Dyck word". A "balanced Dyck path" is something else altogether: see page 98 of The q,t-Catalan Numbers and the Space of Diagonal Harmonics.

[Shreyas4991]

A couple of broader suggestions:

1. I would suggest that DyckPath be renamed to DyckOnePath or something similar. Dyck languages can combine multiple kinds of brackets and you get Dyck 1 or Dyck 2 languages etc. In fact a Nat parameter could be attached to Step and DyckPath to signify the type of bracket. EDIT: Dyck word is more canonical terminology than Dyck path, at least in theoretical CS, so +1 to @trivial1711 's comment.
2. Some notation for constructing Dyck paths might be helpful, even if they have to be quoted like [Dyck1| UDUD]
3. If possible, the Dyck monoid instance could be added. This leads to nice theorems like Chomsky-Schutzenberger.

[trivial1711]

Please do not use the phrase "Dyck path" to refer to an unrestricted list consisting of the letters "U" and "D". The correct name for this concept is simply "list" or "word" (written as List Step in Lean); there is no need to use any abbreviation at all.

[trivial1711]

Here is what I believe to be the standard usage of these terms. Please tell me if you find a reference that suggests otherwise.

• A word on the alphabet $\{U, D\}$ is any finite sequence $w = w_1 \ldots w_\ell$, where each $w_i \in \{U, D\}$. Words are used in this PR, but they are not defined in this PR. They are called "lists" in mathlib, and they are defined in docs#Init.Prelude.List.
• We call a word on the alphabet $\{U, D\}$ a Dyck word if every prefix has at least as many $U$'s as $D$'s and the whole word has exactly as many $U$'s as $D$'s. Dyck words are defined in this PR and they are the primary object of study.
• A Dyck path is a sequence $v_0, \ldots, v_{2n}$ of points in the plane $\mathbb{N}^2$, where $v_0 = (0, 0)$, $v_{2n} = (2n, 0)$, and $v_{i+1} - v_i \in \{(1, 1), (1, -1)\}$ for $0 \leq i < 2n$. They can be thought of as paths in a particular directed graph whose vertex set is $\mathbb{N}^2$. Dyck paths are in bijection with Dyck words, but they are not the same thing as Dyck words. They are not defined at all in this PR. That is okay; the definition and the bijection can be added later.
• A balanced Dyck path is something else altogether: see page 98 of The q,t-Catalan Numbers and the Space of Diagonal Harmonics. Right now, balanced Dyck paths are probably too obscure for mathlib.