Monads for the formalization of a pattern matching procedure (Q2017780)

The article reports on the experience of the author in artificial intelligence, and formalises the pattern matching problem in a categorical framework. The first part of the paper, Sections 1, 2, and 3, introduces the problem and the fundamentals for its characterisation in category theory. Precisely, a rule is composed by a pattern and an action: the pattern describes to which situations the action should be applied to obtain another situation. For a fixed a category \(\mathbb{C}\), each object \(S\) represents a set of situations \(\alpha: A \to S\); a pattern is a morphism \(\phi: X \to S\), and a match occurs when there is \(\beta: A \to X\) such that \(\alpha = \phi \circ \beta\). Thus, the rule \((\phi,\psi)\) is a pair of morphisms \(\phi: X \to S\) and \(\psi: X \to T\), and its application yields the situation \(\psi \circ \beta: A \to T\) with \(\beta\) the match. Section 4 describes various examples of pattern matching and their development within the illustrated categorical framework. Although most of the propositions proved in the paper are elementary, well-known facts often found in most textbooks on category theory as exercises, their interpretation in the context is of interest since it shows how these abstract statements translate into significant cases of pattern matching. Sections 5 and 6 illustrate the standard notions of monad and related Kleisli category, and this part shows how these categorical structures are applied to the pattern matching problem. Section 7 complements this illustration with a number of examples of applications, providing an evidence that the formalisation, which takes the form of a mathematical language, is both flexible and robust. The article has been translated from the Russian original. Some expressions do not conform to the standards: for example, the term Cartesian square is used instead of the more common pullback, and a free functor becomes a freedom functor. Nevertheless, it is quite easy to overcome these problems in the translation as the basic concepts are clearly identified. Reviewer's remark: The potential reader should be aware that the paper sees itself in the tradition of theoretical computer science rather than mathematics. In this respect, the article is well motivated and provides a significant contribution. From the purely mathematical point of view, the results and their proofs are well-known and not original: in fact, as honestly stated in the paper, the original contribution lies in the application to a real problem, pattern matching.