This work proposes a new method of deriving programs from their specifications in constructive type theory: the method of analysis-synthesis. It is new as a mathematical method only in the area of programming methodology, as it is modelled upon the most successful and widespread method in the history of exact sciences. The method of analysis-synthesis, also known as the method of analysis, was devised by Ancient Greek mathematicians for solving geometric construction problems with ruler and compass. Its most important subsequent elaboration is Descartes’s algebraic method of analysis, which pervades all exact sciences today. The present work expands this method further into one that aims at systematizing program derivation in a heuristically useful way, analogously to the way Descartes’s method systematized the solution of geometric and arithmetical problems. To illustrate the method, we derive the Boyer-Moore algorithm for finding an element that has a majority of occurrences in a given list. It turns out that solving programming problems need not be too different from solving mathematical problems in general. This point of view has been emphasized in particular by Martin-Löf (1982) and Dijkstra (1986). The idea of a logic of problem solving originates in Kolmogorov (1932). We aim to refine the analogy between programming and mathematical problem solving by investigating the mathematical method of analysis in the context of programming. The central idea of the analytic method, in modern terms, is to analyze the functional dependencies between the constituents of a geometric configuration. The aim is to determine how the sought constituents depend on the given ones. A Greek analysis starts by drawing a diagram with the sought constructions drawn on the given ones, in the relation required by the problem specification. Then the sought constituents of the configuration are determined in terms of the given ones. Analysis was the Greeks’ method of discovering solutions to problems. Their method of justification was synthesis, which cast analysis into standard deductive form. First it constructed the sought objects from the given ones, and then demonstrated that they relate as required to the given ones. In his Geometry, Descartes developed Greek geometric analysis-synthesis into the modern algebraic method of analysis.
Analogical program derivation based on type theory
