Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Analyzing Array Manipulating Programs by Program Transformation Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Functional Kleene Closures

verfasst von : Nikita Danilenko

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Drill and Join: A Method for Exact Inductive Program Synthesis
Nächstes Kapitel On Completeness of Logic Programs
Fußnoten
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.
 
Literatur
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.
Metadaten
Titel
Functional Kleene Closures
verfasst von
Nikita Danilenko
Copyright-Jahr
2015
Buch
Logic-Based Program Synthesis and Transformation

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

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

Copyright-Jahr: 2015

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

Premium Partner

    Bildnachweise