English
The reduction operator on words in a free group is the maximal reduction; it is computable exactly when the base type α has decidable equality.
Русский
Оператор редукции слов в свободной группе даёт максимальное упрощение; он вычисляема тогда и только тогда, когда α имеет разрешимое равенство.
LaTeX
$$$$\operatorname{reduce}: \mathrm{List}(\alpha \times \{0,1\}) \to \mathrm{List}(\alpha \times \{0,1\})\quad\text{is the maximal reduction; computable iff } [\text{DecidableEq } \alpha].$$$$
Lean4
/-- The maximal reduction of a word. It is computable
iff `α` has decidable equality. -/
@[to_additive /-- The maximal reduction of a word. It is computable iff `α` has decidable equality. -/
]
def reduce : (L : List (α × Bool)) → List (α × Bool) :=
List.rec [] fun hd1 _tl1 ih =>
List.casesOn ih [hd1] fun hd2 tl2 => if hd1.1 = hd2.1 ∧ hd1.2 = not hd2.2 then tl2 else hd1 :: hd2 :: tl2
