Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Analyzing Array Manipulating Programs by Program Transformation Read chapter Read first chapter

2015 | OriginalPaper | Chapter

Functional Kleene Closures

Author : Nikita Danilenko

Published in: Logic-Based Program Synthesis and Transformation

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Drill and Join: A Method for Exact Inductive Program Synthesis
next chapter On Completeness of Logic Programs
Footnotes
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
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
\(\left( {\begin{matrix} 0 &{} 1\\ 1 &{} 0\end{matrix}}\right) \) is invertible over every semiring, thus omitting the invertibility is a restriction.
 
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
Gaussian elimination is indeed computationally similar to the Kleene closure.
 
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
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.
 
Literature
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) CrossRef
2.
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2004) CrossRef
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) CrossRef
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)
5.
6.
7.
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) CrossRef
9.
10.
11.
Pettorossi, A.: Techniques for Searching, Parsing, and Matching. Aracne, Roma (2013)
12.
Metadata
Title
Functional Kleene Closures
Author
Nikita Danilenko
Copyright Year
2015
Book
Logic-Based Program Synthesis and Transformation

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

Electronic ISBN: 978-3-319-17822-6

Copyright Year: 2015

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

Premium Partner

    Image Credits