×

Programming from Galois connections. (English) Zbl 1257.68057

Summary: Problem statements often resort to superlatives such as in e.g. “\(\dots \) the smallest such number”, “\(\dots \) the best approximation”, “\(\dots \) the longest such list” which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting one particular such solution, optimal in some sense (the hard part).
This article introduces a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution.
The framework encompasses re-factoring of results previously developed by R. Bird and O. de Moor [Algebra of programming. London: Prentice Hall (1997; Zbl 0867.68042)] for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
06A15 Galois correspondences, closure operators (in relation to ordered sets)
18B10 Categories of spans/cospans, relations, or partial maps

Citations:

Zbl 0867.68042

Software:

Galculator
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] C. Aarts, R.C. Backhouse, P. Hoogendijk, E. Voermans, J. van der Woude, A relational theory of datatypes, December 1992. Available from: <http://www.cs.nott.ac.uk/∼;rcb>; C. Aarts, R.C. Backhouse, P. Hoogendijk, E. Voermans, J. van der Woude, A relational theory of datatypes, December 1992. Available from: <http://www.cs.nott.ac.uk/∼;rcb>
[2] Backhouse, K.; Backhouse, R. C., Safety of abstract interpretations for free, via logical relations and Galois connections, SCP, 15, 1-2, 153-196 (2004) · Zbl 1091.68069
[3] Backhouse, R. C., On a relation on functions, (Dijkstra, W., Beauty is Our Business: A Birthday Salute to Edsger (1990), Springer-Verlag: Springer-Verlag New York, NY, USA), 7-18
[4] Backhouse, R. C., Galois connections and fixed point calculus, (Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, LNCS, vol. 2297 (2002), Springer-Verlag), 89-148 · Zbl 1065.68030
[5] Backhouse, R. C., Program Construction: Calculating Implementations from Specifications (2003), John Wiley & Sons Inc.: John Wiley & Sons Inc. New York, NY, USA
[6] R. Bird, O. de Moor, Algebra of Programming, Series in Computer Science, Prentice-Hall International, 1997. Available from: http://progtools.comlab.ox.ac.uk/members/oege/publications/aop97; R. Bird, O. de Moor, Algebra of Programming, Series in Computer Science, Prentice-Hall International, 1997. Available from: http://progtools.comlab.ox.ac.uk/members/oege/publications/aop97
[7] Bird, R.; de Moor, O.; Hoogend, P., J. Funct. Programming, 6, 1, 1-28 (1996)
[8] Chung, K.-M.; Lu, H.-I., An optimal algorithm for the maximum-density segment problem, SIAM J. Comput., 34, 2, 373-387 (2004) · Zbl 1087.68120
[9] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall · Zbl 0286.00013
[10] Doornbos, H.; Backhouse, R.; van der Woude, J., A calculational approach to mathematical induction, TCS, 179, 1-2, 103-135 (1997) · Zbl 0901.68124
[11] K. Engelhardt, W.-P. de Roever, Simulation of specification statements in Hoare logic, in: Mathematical Foundations of Computer Science, LNCS, vol. 1113, 1996, pp. 324-335.; K. Engelhardt, W.-P. de Roever, Simulation of specification statements in Hoare logic, in: Mathematical Foundations of Computer Science, LNCS, vol. 1113, 1996, pp. 324-335.
[12] M.A. Ferreira, J.N. Oliveira, Variations on an alloy-centric tool-chain in verifying a journaled file system model, Technical Report DI-CCTC-10-07, University of Minho, January 2010.; M.A. Ferreira, J.N. Oliveira, Variations on an alloy-centric tool-chain in verifying a journaled file system model, Technical Report DI-CCTC-10-07, University of Minho, January 2010.
[13] Freyd, P. J.; Scedrov, A., Categories, Allegories, Mathematical Library, vol. 39 (1990), North-Holland · Zbl 0698.18002
[14] Jackson, D., Software Abstractions: Logic, Language, and Analysis (2012), The MIT Press: The MIT Press Cambridge, MA, ISBN 0-262-01715-2
[15] Jones, C. B., Software Development - A Rigorous Approach (1980), Prentice-Hall International · Zbl 0424.68019
[16] Knuth, D. E., The Art of Computer Programming (1997/98), Addison/Wesley · Zbl 0191.17903
[17] Kramer, J., Is abstraction the key to computing?, Commun. ACM, 50, 4, 37-42 (2007)
[18] Melton, A.; Schmidt, D. A.; Strecker, G. E., Galois connections and computer science applications, (Category Theory and Computer Programming. Category Theory and Computer Programming, LNCS, vol. 240 (1986), Springer), 299-312 · Zbl 0622.06004
[19] Oliveira, J. N., Extended static checking by calculation using the pointfree transform, (Language Engineering and Rigorous Software Development. Language Engineering and Rigorous Software Development, LNCS, vol. 5520 (2009), Springer-Verlag), 195-251 · Zbl 1250.68093
[20] J.N. Oliveira, A Look at Program ‘Galculation’, Presentation at the IFIP WG 2.1 #65 Meeting, January 2010.; J.N. Oliveira, A Look at Program ‘Galculation’, Presentation at the IFIP WG 2.1 #65 Meeting, January 2010.
[21] Oliveira, J. N.; Rodrigues, C. J., Pointfree factorization of operation refinement, (FM 2006: Formal Methods. FM 2006: Formal Methods, LNCS, vol. 4085 (2006), Springer-Verlag), 236-251
[22] Orłowska, E.; Rewitzky, I., Algebras for Galois-style connections and their discrete duality, Fuzzy Sets and Systems, 161, 9, 1325-1342 (2010), Foundations of Lattice-Valued Mathematics with Applications to Algebra and Topology · Zbl 1195.03059
[23] Schmidt, G., Homomorphism and isomorphism theorems generalized from a relational perspective, (Relations and Kleene Algebra in Computer Science. Relations and Kleene Algebra in Computer Science, LNCS, vol. 4136 (2006), Springer), 328-342 · Zbl 1135.08002
[24] Silva, P. F.; Oliveira, J. N., ‘Galculator’: functional prototype of a Galois-connection based proof assistant, (PPDP’08 (2008), ACM: ACM NY), 44-55
[25] Tarski, A.; Givant, S., A Formalization of Set Theory without Variables (1987), American Mathematical Society · Zbl 0654.03036
[26] Ullman, J. D., Principles of Database Systems (1981), Computer Science Press
[27] Winter, M., Products in categories of relations, J. Logic Algebr. Program., 76, 1, 145-159 (2008) · Zbl 1139.18003
[28] Wirth, N., Algorithms+Data Structures=Programs (1976), Prentice-Hall · Zbl 0375.68005
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.