Programming from Galois Connections

Problem statements often resort to superlatives such as in eg. “... the smallest such number”, “... the best approximation”, “... 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 op-timization. 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 by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with