Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures. (English) Zbl 1329.68062
Summary: We show how to systematically derive simple purely functional algorithms for computing the reflexive-transitive closure of directed graphs. Directed graphs can be represented as binary relations and we develop our algorithms based on a relation-algebraic description of reflexive-transitive closures. This description employs the notion of rectangles and instantiating the resulting algorithm with different kinds of rectangles leads to different algorithms for computing reflexive-transitive closures. Using data refinement, we then develop simple Haskell programs for two specific choices of rectangles and show that one of them has cubic running time like Warshall’s standard algorithm. Finally, we apply our approach to other standard operations of relation algebra and present graph theoretic applications of our developments.
MSC:
| 68N18 | Functional programming and lambda calculus |
| 03G20 | Logical aspects of Łukasiewicz and Post algebras |
| 05C20 | Directed graphs (digraphs), tournaments |
| 05C85 | Graph algorithms (graph-theoretic aspects) |
Keywords:
directed graphs; relation algebra; reflexive-transitive closure; rectangle; functional programming; HaskellReferences:
| [1] | Aarts, A., Fixed point calculus, Inf. Process. Lett., 53, 131-136 (1996) · Zbl 0875.68201 |
| [2] | Berghammer, R., A transformational development of several algorithms for testing the existence of cycles in a directed graph (1986), Institut für Informatik, TU München, Report TUM-I8616 |
| [3] | Berghammer, R.; Ehler, H.; Zierer, H., Development of several reachability algorithms for directed graphs, (Göttler, H.; Schneider, H. J., Graph-Theoretic Concepts in Computer Science. Graph-Theoretic Concepts in Computer Science, LNCS, vol. 314 (1988), Springer), 206-218 · Zbl 0664.68018 |
| [4] | Berghammer, R.; von Karger, B., Algorithms from relational specification, (Brink, C.; Kahl, W.; Schmidt, G., Relational Methods in Computer Science, Advances in Computing (1997), Springer), 131-149 · Zbl 0884.68080 |
| [5] | Berghammer, R.; Hoffmann, T., Deriving relational programs for computing kernels by reconstructing a proof of Richardson’s theorem, Sci. Comput. Program., 38, 1-25 (2000) · Zbl 0957.68029 |
| [6] | Berghammer, R.; Hoffmann, T., Relational depth-first-search with applications, Inf. Sci., 139, 167-186 (2001) · Zbl 1004.68125 |
| [7] | Berghammer, R.; Neumann, F., RelView - an OBDD-based Computer Algebra system for relations, (Ganzha, V. G.; Mayr, E. W.; Vorozhtsov, E., Computer Algebra in Scientific Computing. Computer Algebra in Scientific Computing, LNCS, vol. 3718 (2005), Springer), 40-51 · Zbl 1144.68384 |
| [8] | Berghammer, R.; Fischer, S., Implementing relational specifications in a constraint functional language, Electron. Notes Theor. Comput. Sci., 177, 169-183 (2007) · Zbl 1279.68036 |
| [9] | Berghammer, R.; Struth, G., On automated program construction and verification, (Bolduc, C.; Desharnais, J.; Ktari, B., Mathematics of Program Construction. Mathematics of Program Construction, LNCS, vol. 6120 (2010)), 22-41 · Zbl 1286.68068 |
| [10] | Berghammer, R., A functional, successor list based version of Warshall’s algorithm with applications, (de Swart, H., Relational and Algebraic Methods in Computer Science. Relational and Algebraic Methods in Computer Science, LNCS, vol. 6663 (2011), Springer), 109-124 · Zbl 1329.68303 |
| [11] | Berghammer, R.; Fischer, S., Simple rectangle-based functional programs for computing reflexive-transitive closures, (Kahl, W.; Griffin, T. G., Relational and Algebraic Methods in Computer Science. Relational and Algebraic Methods in Computer Science, LNCS, vol. 7560 (2012), Springer), 114-129 · Zbl 1330.68044 |
| [12] | Berghammer, R., Ordnungen, Verbände und Relationen mit Anwendungen (2013), Vieweg-Teubner |
| [13] | Berghammer, R.; Höfner, P.; Stucke, I., Automated verification of relational while-programs, (Höfner, P.; Jipsen, P.; Kahl, W.; Müller, M., Relational and Algebraic Methods in Computer Science. Relational and Algebraic Methods in Computer Science, LNCS, vol. 8428 (2014), Springer), 173-190 · Zbl 1405.68070 |
| [14] | Bird, R.; Ravelo, J., On computing representatives, Inf. Process. Lett., 63, 1-7 (1997) · Zbl 1336.68272 |
| [15] | Bird, R., Introduction to Functional Programming Using Haskell (1998), Prentice Hall |
| [16] | Brunn, T.; Möller, B.; Russling, M., Layered graph traversals and Hamiltonian path problems - an algebraic approach, (Jeuring, J., Mathematics of Program Construction. Mathematics of Program Construction, LNCS, vol. 1422 (1998), Springer), 96-121 · Zbl 0907.05052 |
| [17] | Chen, Y., On the evaluation of large and sparse graph reachability queries, (Bhowmick, S.; Küng, J., Database and Expert Systems Applications. Database and Expert Systems Applications, LNCS, vol. 5181 (2008), Springer), 97-105 |
| [18] | Danilenko, N., Using relations to develop a Haskell program for computing maximum bipartite matchings, (Kahl, W.; Griffin, T. G., Relational and Algebraic Methods in Computer Science. Relational and Algebraic Methods in Computer Science, LNCS, vol. 7560 (2012), Springer), 130-145 · Zbl 1364.68129 |
| [19] | Erwig, M., Graph algorithms = iteration + data structures? The structure of graph algorithms and a corresponding style of programming, (Mayr, E. W., Graph-Theoretic Concepts in Computer Science. Graph-Theoretic Concepts in Computer Science, LNCS, vol. 657 (1992), Springer), 277-292 · Zbl 0789.68107 |
| [20] | Erwig, M., Functional programming with graphs, ACM SIGPLAN Not., 32, 52-65 (1997) · Zbl 1369.68095 |
| [21] | Erwig, M., Inductive graphs and functional graph algorithms, J. Funct. Program., 11, 467-492 (2001) · Zbl 0994.68032 |
| [22] | Floyd, R. W., Algorithm 97 (shortest path), Commun. ACM, 5, 345 (1962) |
| [23] | Fredmann, M. L., New bounds on the complexity of the shortest path problem, SIAM J. Comput., 5, 83-89 (1976) · Zbl 0326.68027 |
| [24] | Gibbons, J., An initial algebra approach to directed graphs, (Möller, B., Mathematics of Program Construction. Mathematics of Program Construction, LNCS, vol. 947 (1995), Springer), 282-303 |
| [25] | Hanus, M., The integration of functions into logic programming: from theory to practice, J. Log. Program., 19&20, 583-628 (1994) · Zbl 0942.68526 |
| [26] | Hanus, M., Curry: an integrated functional logic language (2006), available at |
| [27] | Kahl, W., Semigroupoid interfaces for relation-algebraic programming in Haskell, (Schmidt, R., Relations and Kleene Algebra in Computer Science. Relations and Kleene Algebra in Computer Science, LNCS, vol. 4136 (2006), Springer), 235-250 · Zbl 1134.68339 |
| [28] | King, D. J.; Launchbury, J., Structuring depth-first search algorithms in Haskell, (Proc. ACM Symposium on Principles of Programming (1995), ACM Press), 344-356 |
| [29] | Launchbury, J., Graph algorithms with a functional flavour, (Jeuring, J.; Meijer, E., Advances in Functional Programming. Advances in Functional Programming, LNCS, vol. 925 (2005), Springer), 308-331 |
| [30] | Penn, G., The algebraic structure of transitive closure and its application to attributed type signatures, Grammars, 3, 295-312 (2000) · Zbl 0973.68044 |
| [31] | Penn, G., Efficient transitive closure of sparse matrices over closed semirings, Theor. Comput. Sci., 354, 72-81 (2006) · Zbl 1088.68042 |
| [32] | Ravelo, J., Two graph algorithms derived, Acta Inform., 36, 489-510 (1999) · Zbl 0933.68157 |
| [33] | Russling, M., Deriving a class of layer-oriented graph algorithms, Sci. Comput. Program., 26, 117-132 (1996) · Zbl 0853.68142 |
| [34] | Schmidt, G.; Ströhlein, T., Relations and Graphs. Discrete Mathematics for Computer Scientists, EATCS Monographs on Theoretical Computer Science (1993), Springer · Zbl 0900.68328 |
| [35] | Schmidt, G., A proposal for a multilevel relational reference language, J. Relat. Methods Comput. Sci., 1, 314-338 (2004) |
| [36] | Schmidt, G., Rectangles, fringes and inverses, (Berghammer, R.; Möller, B.; Struth, G., Relations and Kleene Algebra in Computer Science. Relations and Kleene Algebra in Computer Science, LNCS, vol. 4988 (2008), Springer), 352-366 · Zbl 1139.03047 |
| [37] | Schmidt, G., Relational Mathematics, Encyclopedia of Mathematics and Its Applications (2011), Cambridge University Press · Zbl 1214.06001 |
| [38] | Spivey, J. M., The Z Notation: A Reference Manual (1992), Prentice Hall · Zbl 0777.68003 |
| [39] | Strassen, V., Gaussian elimination is not optimal, Numer. Math., 13, 354-356 (1969) · Zbl 0185.40101 |
| [40] | Tarski, A., On the calculus of relations, J. Symb. Log., 6, 73-89 (1941) · JFM 67.0973.02 |
| [41] | Tarski, A.; Givant, S., A Formalization of Set Theory without Variables, AMS Colloquium Publications, vol. 41 (1987) · Zbl 0654.03036 |
| [42] | Thomson, S., Haskell - The Craft of Functional Programming (2011), Addison-Wesley |
| [43] | Warshall, S., A theorem on Boolean matrices, J. ACM, 9, 11-12 (1962) · Zbl 0118.33104 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
