The Halting Problem for Deductive Synthesis of Logic Programs
Kung-kiu Lau, Mario Ornaghi · The MIT Press eBooks · 1994
Deductive synthesis methods derive programs in an incremental manner, and therefore pose a halting problem -- when can synthesis stop with a correct program? We give a characterisation of this problem and state a halting principle as a solution. Another characteristic of deductive synthesis is that it may derive several correct programs, giving rise to another question -- which correct programs are desirable? We show that the answer is related to the halting problem, via the notion of steadfast, or reusable, programs as desirable programs. Our work also reveals that Clark's idea of the completion of a program is central to deductive synthesis, since it is the basis of our halting principle and our notion of steadfast programs. 1 Introduction Writing a correct program is a major problem in programming. It is theoretically interesting and practically significant. Incorrect programs may have dire consequences, and are unfortunately related to the software crisis in practice. Methods have...