Abstract
In this thesis we present a methodology for the synthesis of function free definite logic programs from incomplete specifications, background knowledge and programming knowledge. The methodology is implemented as system SKILit and sub-systems SKIL and MONIC. The specification consists of positive and negative examples (ground atoms) of the predicate to synthesize, together with its input/output mode declaration. It can also include the predicate type declaration and integrity constraints. The background knowledge contains auxiliary predicates that may be used in the definition of the target predicate. Programming knowledge can be expressed in the form of a clause structure grammar that defines the structure of clauses to be synthesized in terms of admissible sequences of predicates. The user can also partially describe how some particular positive examples are computed. This information is given to the system in the form of sketches.
The construction of each clause is made by searching for a relational link between the input arguments and the output arguments of one positive example. Examples with or without associated sketches are handled in a uniform way using a unique sketch refinement operator. The sketch refinement operator of SKIL is shown to be complete under appropriate assumptions. Our methodology is capable of synthesizing recursive programs from small and sparse sets of positive examples using the technique of iterative induction. This is an important result considering that there is no strong language bias imposed (the technique is successful in synthesizing programs with multiple recursive clauses and clauses with multiple recursive literals). The methodology can also perform multiple predicate synthesis.
Due to its expressiveness, one integrity constraint can replace a large number of ground negative examples. Typically, constraint handling is computationally heavy. In our methodology, integrity constraints are handled using a Monte Carlo strategy (MONIC). Although incomplete, the Monte Carlo approach provides an efficient solution to constraint handling, which is very important in the context of program synthesis.
The whole synthesis methodology has been empirically evaluated in a
systematic way showing that it is robust in the synthesis of recursive
definitions from randomly generated examples and that it competes well
with some state-of-the-art approaches.
Resumo
Nesta disseratção apresentamos uma metodologia para a síntese de programas lógicos definidos sem functores a partir de especificações incompletas, conhecimento de fundo e conhecimento de programação. A metodologia foi implementada no sistema SKILit e nos sub-sistemas SKIL e MONIC. A especificação consiste em exemplos positivos e negativos (átomos fechados) e na declaração de entrada/saída do predicado a sintetizar. Pode também incluir a declaração de tipo do predicado e restrições de integridade. O conecimento de fundo contém predicados auxiliares que podem ser utilizados na definição do predicado pretendido. O conhecimento de programação pode ser expresso sob a forma de uma gramática de estrutura clausal. Esta define a estrutura das cláusulas a sintetizar em termos de sequências amissíveis de predicados. O utilizador pode também descrever parcialmente a computação de determinados exemplos positivos. Esta informação é dada ao sistema através de esboços.
A contrução de cada cláusula é feita procurando uma ligação relacional entre os argumentos de entrada e os argumentos de saída de um exemplo positivo. Os exemplos são tratados de maneira uniforme quer tenham ou não um esboço associado. Mostra-se que o operador de refinamento do SKIL é completo sob os pressupostos adequados. A nossa metodologia é capaz de sintetizar programas recursivos a partir de conjuntos pequenos e esparsos de exemplos positivos usando a técnica da indução iterativa. Este é um resultado importante considerando que não são impostas fortes condições sintáticas aos programas (a técnica sintetiza com sucesso programas com várias cláusulas recursivas e cláusulas com vários literais recursivos). A metodologia também é capaz de fazer síntese múltipla de predicados.
Devido à sua expressividade, uma restrição de integridade pode substituir um grande número de exemplos negativos fechados. Tipicamente, verificar restrições é computacionalmente pesado. Na nossa metodologia, as restrições são tratadas usando uma estratégia de Monte Carlo (MONIC). Embora incompleta, a abordagem de Monte Carlo proporciona uma solução eficiente à verificação de restrições, o que é importante no contexto de síntese de programas.
A metodologia de síntese foi avaliada empiricamente de uma forma sistemática mostrando que é robusta na síntese de definições recursivas a partir de exemplos gerados aleatoriamente e que consegue competir com outras técnicas estado-da-arte.
Dans cette thèse nous introduisons une méthodologie pour la synthèse de programmes lógiques sans symboles de fonction a partir de spécifications incomplètes, théorie du domaine et connaissances de programmation. La méthodologie a été implementée dans le système SKILit ainsi comme dans les sous-systèmes SKIL et MONIC. La spécification consiste en des exemples positifs et négatifs (atomes clos) ainsi comme dans la déclaration d�entré/sortie du prédicat a synthétiser. Elle peut aussi incluire la déclaration de type du prédicat et restrictions d�intégrité. La théorie du domaine contien des prédicats auxiliaires qui peuvent êtres utilisés dans la définition du prédicat prétendu. La connaissance de programmation peut être exprimée comme une grammaire de structure clausale. Celle-ci définit la structure des clauses a synthétiser en terms de séquences de prédicats. L�utilisateur peut aussi décrire d�une façon partial la computation de certains examples positifs. Cette information est donnée au systéme a travers d�ébauches.
La construction de chaque clause é faite en cherchant une liaison relationnele entre les arguments d�entré et les arguments de sortie d�un exemple positif. Les exemples sont traités uniformement, indépendamment d�avoir ou non un ébauche associé. On montre que le opérator de raffinement de SKIL est complét sous les assumptions adéquates. Notre méthodologie est capable de synthétiser des programmes récursifs a partir d�ensembles petits et dispersés d�exemples positifs en utilisant la technique d�induction itérative. Ce résultat est important une fois que on n�impose pas des fortes conditions aux programmes (la technique synthétise avec succés des programmes avec multiples clauses recursives ainsi comme clauses avec multiple littérals recursifs). La méthodologie est aussi capable de faire la synthèse multiple de predicats.
Due a son expressivité, une restriction d�integrité peut remplacer un grand nombre d�exemples négatifs clos. Typiquement, vérifier restrictions est lourd du point de vue de la computation. Dans notre méthodologie, les restrictions sont traitées en utilisant une stratégie de Monte Carlo (MONIC). Bien qu�incomplète, la stratégie de Monte Carlo proporcionne une solution efficient pour la vérification de restrictions, ce qui est important dans le context de la synthèse de programmes.
La methodologie de synthèse a été évaluée d�une façon empirique et systématique, démontrant ainsi qu�elle est robuste dans la synthèse de définitons recursives a partir d�exemples engendrés d�une façon aléatoire; et qu�elle est aussi capable de compéter avec d�autres techniques �state-of-the-art�.