Monads for the formalization of a pattern matching procedure.

*(English. Russian original)*Zbl 1325.68224
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.

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 |

##### 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 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.