The Halting Problem for Deductive Synthesis of Logic Programs

Kung-Kiu Lau
Department of Computer Science, University of Manchester
Oxford Road, Manchester M13 9PL, United Kingdom
kung-kiu@cs.man.ac.uk

Mario Ornaghi
Dipartimento di Scienze dell'Informazione
Universita' degli studi di Milano
Via Comelico 39/41, Milano, Italy
ornaghi@dsi.unimi.it

Sten-Ake Tarnlund
Computing Science Department, Uppsala University
P.O. Box 520, S-751 20 Uppsala, Sweden
stenake@csd.uu.se

Abstract:
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.