Skip to main content
SpringerLink
Log in

Functional Kleene Closures

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8981))

  • 540 Accesses

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Such a set where \(b_i < 1\) for all \(i \in \mathbb {N}_{< m}\) does not necessarily exist. However, if \(B\) is finite, we can simply choose the atoms of \(B\) (i.e. the upper neighbours of \(0\)) as \(B'\).

  2. 2.

    To ensure that the requirements are met, one can use tools like Coq (cf. [2]) to make certain functions applicable only once the preconditions are checked (i.e. proved). However, in Haskell one usually requires certain laws implicitly (e.g. for Monad or Functor), which is why we do not explore the mentioned approach further.

  3. 3.

    \(\left( {\begin{matrix} 0 &{} 1\\ 1 &{} 0\end{matrix}}\right) \) is invertible over every semiring, thus omitting the invertibility is a restriction.

  4. 4.

    In Kleene algebras there can be zero divisors, i.e. elements \(x, y \in K\) such that \(x \ne 0\) and \(y \ne 0\), but \(xy = 0\). This is why we need to filter the zero values.

  5. 5.

    Gaussian elimination is indeed computationally similar to the Kleene closure.

  6. 6.

    In a matrix with size \(1000\) a density of \(0.1\) means \(100000\) entries, which is likely to yield a fully filled transitive closure. This is why we use such seemingly small values.

  7. 7.

    The measurements were taken on an machine with an Intel Core i5-2520M CPU (4 \(\times \) 2.5 GHz) with 8 GB of DDR3 RAM, running Ubuntu 12.04 and using GHC 7.6.3.

References

  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)

    Chapter  Google Scholar 

  2. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2004)

    Book  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Hutton, G.: A tutorial on the universality and expressiveness of fold. J. Funct. Program. 9(4), 355–372 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  6. Johnsson, T.: Efficient graph algorithms using lazy monolithic arrays. J. Funct. Program. 8(4), 323–333 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  7. Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Chapter  Google Scholar 

  9. Marlow, S. The Haskell Report (2010). www.haskell.org/onlinereport/haskell2010

  10. O’Connor, R. (2011). http://r6.ca/blog/20110808T035622Z.html

  11. Pettorossi, A.: Techniques for Searching, Parsing, and Matching. Aracne, Roma (2013)

    Google Scholar 

  12. Sands, D.: A nave time analysis and its theory of cost equivalence. J. Log. Comput. 5, 495–541 (1995)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Acknowledgements

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

Author information

Authors and Affiliations

  1. Institut Für Informatik, Christian-Albrechts-Universität Kiel, Olshausenstraße 40, 24098, Kiel, Germany

    Nikita Danilenko

Authors
  1. Nikita Danilenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nikita Danilenko .

Editor information

Editors and Affiliations

  1. IASI-CNR, Rome, Italy

    Maurizio Proietti

  2. Nagoya Institute of Technology, Nagoya, Japan

    Hirohisa Seki

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Danilenko, N. (2015). Functional Kleene Closures. In: Proietti, M., Seki, H. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2014. Lecture Notes in Computer Science(), vol 8981. Springer, Cham. https://doi.org/10.1007/978-3-319-17822-6_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-17822-6_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-17821-9

  • Online ISBN: 978-3-319-17822-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation