Functional Kleene Closures

  • Nikita DanilenkoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8981)


We present a derivation of a purely functional version of Kleene’s closure algorithm for Kleene algebras (with tests) that contain a subset where the closure is already known. In particular, our result is applicable to the Kleene algebra of square matrices over a given Kleene algebra. Our approach is based solely on laws imposed on Kleene algebras and Boolean algebras. We implement our results in the functional programming language Haskell for the case of square matrices and discuss a general implementation. In this process we incorporate purely algebraic improvements like the use of commutativity to obtain a concise and optimised functional program. Our overall focus is on a functional program and the computational structures from which it is composed. Finally, we discuss our result particularly in light of alternative approaches.


Boolean Algebra Partial Identity Closure Function Closure Operation Algebraic Reasoning 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



I thank Rudolf Berghammer for encouraging this work, Insa Stucke for comments and the reviewers for their much appreciated feedback.


  1. 1.
    Berghammer, R.: A functional, successor list based version of warshall’s algorithm with applications. In: de Swart, H. (ed.) RAMICS 2011. LNCS, vol. 6663, pp. 109–124. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  2. 2.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2004) CrossRefGoogle Scholar
  3. 3.
    Danilenko, N.: Using relations to develop a haskell program for computing maximum bipartite matchings. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 130–145. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  4. 4.
    Dolan, S.: Fun with semirings: a functional pearl on the abuse of linear algebra. In: Morrisett G., Uustalu T. (eds.) ICFP, pp. 101–110. ACM (2013)Google Scholar
  5. 5.
    Hutton, G.: A tutorial on the universality and expressiveness of fold. J. Funct. Program. 9(4), 355–372 (1999)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Johnsson, T.: Efficient graph algorithms using lazy monolithic arrays. J. Funct. Program. 8(4), 323–333 (1998)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Kozen, D., Smith, F.: Kleene algebra with tests: completeness and decidability. In: van Dalen, D., Bezem, Marc (eds.) CSL 1996. LNCS, vol. 1258, pp. 244–259. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  9. 9.
    Marlow, S. The Haskell Report (2010).
  10. 10.
  11. 11.
    Pettorossi, A.: Techniques for Searching, Parsing, and Matching. Aracne, Roma (2013) Google Scholar
  12. 12.
    Sands, D.: A nave time analysis and its theory of cost equivalence. J. Log. Comput. 5, 495–541 (1995)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Institut Für InformatikChristian-Albrechts-Universität KielKielGermany

Personalised recommendations