IsaWhelk: Whelk Interpreted in Isabelle
The MIT Press eBooks · 1994
In [1], Geraint Wiggins presents Whelk, an adaptation of the proofs-as-programs idea to logic program synthesis. Whelk is proposed as a new kind of logic and synthesis methodology where specifications are manipulated in a kind of “tagged” formal system where tags provide information on how to construct programs. I use Isabelle, a logical framework supporting proof construction by higher-order resolution, as a tool to reconstruct, simplify, implement, and use Whelk. In my interpretation, I formulate tagged formulas directly as equivalences between specifications and program schernas; hence the Whelk rules constitute a simple calculus for manipulating equivalences. I use Isabelle to formally derive these rules in the appropriate first-order theory, or, in several cases, to uncover flaws in the proposed rules. I show how application of these proof rules by higher-order resolution permits program synthesis from specification in the manner of Whelk. I call the resulting Isabelle theory IsaWhelk; it has functionality similar to Whelk but is formally verified and very simple to understand. Conceptually, the interpretation simplifies and clarifies. By stripping Whelk of its notational baggage and bringing us back to the familiar mathematical setting of first-order logic, I can use conventional means to address questions of derivabilit.y and correctness. The interpretation quickly exposes that some of the Whelk rules are invalid. Of course, these defects are present in the original Whelk theory, but their presence there is perhaps harder to ascertain. Pragmatically, IsaWhelk illustrates how proofs based on higher-order resolution can construct programs during proofs and the practical benefits of using Isabelle. For example, I directly employ standard tactics distributed with the Isabelle system. Using these, derivation of the Whelk rules is mostly automatic. I gi ve an example of program synthesis carrying out the same example as Wiggins (synthesizing the subset program) but my proof requires only 15 simple steps as opposed to 105 in Whelk where program development tactics are only now being developed.