Monads for the formalization of a pattern matching procedure. (English. Russian original) Zbl 1325.68224

Zhozhikashvili, A. V.

Program. Comput. Softw. 40, No. 3, 117-127 (2014); translation from Programmirovanie 40, No. 3 (2014).

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.

Reviewer: Marco Benini (Buccinasco)

MSC:

68T30	Knowledge representation
18C15	Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
68Q65	Abstract data types; algebraic specification
68T10	Pattern recognition, speech recognition

Keywords:

pattern matching; Kleisli construction

Software:

Haskell

References:

[1]	Stefanyuk, VL; Zhozhikashvili, AV, Productions and rules in artificial intelligence, Kybernetes: Int. J. Syst. Cybern., 31, 817-826, (2002)
[2]	Zhozhikashvili, AV; Stefanyuk, VL, On the concept of production in artificial intelligence, 76-81, (2002)
[3]	Pospelov, DA, Production models, (1990), Moscow
[4]	Markov, A.A. and Nagornyi, N.M., The Theory of Algorithms, Moscow: Nauka, 1984; Dordrecht: Kluwer, 1988.
[5]	Chomsky, N; Luce, R (ed.); Bush, R (ed.); Galanter, E (ed.), Formal properties of grammars, (1963), NewYork · Zbl 0156.25303
[6]	Robinson J.A., Logic: Form and Function, New York: North-Holland, 1979. · Zbl 0428.03009
[7]	MacLane, S., Categories for the Working Mathematician, Berlin: Springer, 1971. · Zbl 0705.18001
[8]	Kleisli, H, Every standard construction is induced by a pair of adjoint functors, Proc. Am. Math. Soc., 16, 544-546, (1965) · Zbl 0138.01704
[9]	Cohn, P., Universal Algebra, New York: Harper and Row, 1965. · Zbl 0141.01002
[10]	Moggi, E, Computational lambda-calculus and monads, (1989) · Zbl 0716.03007
[11]	Wadler, P, Comprehending monads, Mathematical Structures in Computer Science, 2, 461-493, (1992) · Zbl 0798.68040
[12]	Hyland, M; Plotkin, GD; Power, AJ, Combining effects: sum and tensor, Theor. Comput. Sci., 357, 70-99, (2006) · Zbl 1096.68088
[13]	Rydeheard, D.E. and Burstall, R.M., Computational Category Theory, Englewood Cliffs: Prentice Hall, 1988. · Zbl 0649.18001
[14]	Eklund, P., Galan, M.A., Medina, J., Ojeda Aciego, M., and Valverde, A., A categorical approach to unification of generalised terms, Electron. Notes Theor. Comput. Sci., 2002, vol. 66, no. 5. · Zbl 1270.03141
[15]	Bulychev, PE; Kostylev, EV; Zakharov, VA, Anti-unification algorithms and their applications in program analysis, 413-423, (2010), Berlin · Zbl 1274.68066
[16]	Report on the Programming Language Haskell: Version 1.1, Hudak, P., Peyton Jones, S, and Wadler, P., Eds., Technical Report, Yale University and Glasgow University, 1991.
[17]	Schrijvers, T; Stuckey, PJ; Wadler, P, Monadic constraint programming, J. Funct. Programming, 19, 663-697, (2009) · Zbl 1184.68166