Program Synthesis from a Set of Definite Clauses and a Query

摘要

Given a set of definite clauses and a query, the program synthesis presented in this paper is to generate a correct and efficient program to answer the query. In logic programming, a set of definite clauses is regarded as a program, which is called a logic program. However, there are many logic programs that are not very efficient and some natural logic programs do not terminate and fail to find all solutions correctly. To overcome the difficulty, we use the "equivalent transformation (ET)" model, where computation is regarded as equivalent transformation of declarative descriptions (e.g., a set of definite clauses) by a number of equivalent transformation rules. Thus, generating ET rules that can transform a set of definite clauses equiv-alently is a foundation of the proposed method for program synthesis. A new concept of meta-descriptions, each of which represents infinite descriptions by instantiation, is introduced. Meta-descriptions are transformed equiva-lently by means of meta-rules to generate ET rules. An ET rule is obtained from each pair of meta-descriptions that are equivalent.