1994 • 458 Pages • 5.06 MB • English

Posted April 14, 2020 • Uploaded
by terrance96

PREVIEW PDF

Page 1

Lecture Notes in Computer Science 883 Edited by G. Goos, J. Hartmanis and J. van Leeuwen Advisory Board: W. Brauer D. Gries J. Stoer

Page 2

Laurent Fribourg Franco Turini (Eds.) Logic Program Synthesis and Transformation- Meta-Programming in Logic 4th International Workshops LOPSTR '94 and META '94 Pisa, Italy, June 20-21, 1994 Proceedings Springer-Verlag Berlin Heidelberg NewYork London Paris Tokyo Hong Kong Barcelona Budapest

Page 3

series Editors Gerhard Goos Universit~it Karlsruhe Vincenz-Priessnitz-StraBe 3, D-76128 Karlsruhe, Germany Juris Hartmanis Department of Computer Science, Cornell University 4130 Upson Hall, Ithaka, NY 14853, USA Jan van Leeuwen Department of Computer Science, Utrecht University Padualaan 14, 3584 CH Utrecht, The Netherlands Volume Editors Laurent Fribourg LIENS-CNRS 45 rue d'Ulm, F-75005 Paris, France Franco Turini Dipartimento di Informatica, Universit~ di Pisa Corso Italia, 40, 1-56125 Pisa, italy CR Subject Classification (1991): E4.1, E3.2-3, 1.2.2, 1.2.4, D.3.1, D.3.4 ISBN 3-540-58792-6 Springer-Verlag Berlin Heidelberg New York CIP data applied for This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer-Verlag. Violations are liable for prosecution under the German Copyright Law. �9 Springer-Verlag Berlin Heidelberg 1994 Printed in Germany Typesetting: Camera-ready by author SPIN: 10479332 45/3140-543210 - Printed on acid-free paper

Page 4

P r e f a c e This volume contains the proceedings of the LOPSTR'94 and META'94 workshops, which were held in Pisa on June 20-21, 1994. The two workshops took place in parallel and were attended by 69 persons coming from 16 coun- tries. LOPSTR'94 is the Fourth International Workshop on Logic Program Syn- thesis and Transformation. Previous workshops had taken place in Manchester (1991, 1992) and in Louvain-la-Neuve (1993). This year, 19 submitted papers were selected for presentation in Pisa, among which 15 were accepted for inclu- sion in these proceedings, after some revisions had been made by the authors. The main topics addressed by the papers are: unfolding/folding, partial deduc- tion, proofs as programs, inductive logic programming, automated program ver- ification, specification and programming methodologies. META'94 is the Fourth International Workshop on Metaprogramming in Logic. Previous workshops had taken place in Bristol (1988), in Leuven (1990), and in Uppsala (1992). This year, 21 papers were submitted and 11 were ac- cepted for presentation in Pisa and inclusion in the proceedings. The main top- ics addressed by the papers are: language extensions in support of Meta-logic, semantics of Meta-logic, implementation of Meta-logic features, performance of Meta-logic, and applications of Meta-logic to non-monotonic reasoning, program control, and programming in the large, In addition to LOPSTR-META regular contributions, two invited speakers gave very insightful and appreciated talks in Pisa: Giorgio Levi on "Abstract debugging of logic programs" (included in this book) and Burton Dreben on "Herbrand's contributions to logic " We would like to thank all the members of the Program Committees as well as the referees for their thorough job of reviewing. We also express our gratitude to all the members of the local organizing committee for their help in organizing these successful events. We gratefully acknowledge the financial support of the Compulog Network of Excellence. September 1994 Laurent Fribourg, Franco Turini

Page 5

vI O r g a n i z i n g C o m m i t t e e : Antonio Brogi, Paolo Mancarella, Dino Pedreschi, Franco Turini (U. Pisa) P r o g r a m C o m m i t t e e o f L O P S T R : Dmitri Boulanger (K.U. Leuven) Gerard Ferrand (U. Orleans) Pierre Flener (Bilkent U., Ankara) Laurent Fribourg (LIENS-CNRS, Paris)(Chair) Jean-Marie Jacquet (U. Namur) Maurizio Proietti (IASLCNR, Roma) Franco Turini (U. Pisa) Geraint Wiggins (U. Edinburgh) R e v i e w e r s for L O P S T R : Michel Bidoit Tadashi Kanamori Paolo Ciancarini Baudouin Le Charlier Ilyas ~i~ekli Christophe Lecoutre Koen De Bosschere Vincent Lombart Pierre Deransart Anne Mulkers Danny De Schreye Guy Alain Narboni Philippe Devienne Chet Murthy Yves Deville Anne Parrain Alexander Dikovsky Sophie Renault Maurizio Gabrielli Christel Vrain P r o g r a m C o m m i t t e e o f M E T A : L. Aiello (Rome, Italy) J. Barklund (Uppsala, Sweden) K. Bowen (Syracuse, USA) D. De Schreye (Leuven, Belgium) Y. Jiang (London, UK) J. Komorowski (Trondheim, Norway) G. Lanzarone (Milan, Italy) A. Martelli (Turin, Italy) L.M. Pereira (Lisbon, Portugal) A. Pettorossi (Rome, Italy) A. Porto (Lisbon, Portugal) T. Sato (Tsukuba, Japan) L. Sterling (Cleveland, USA) S.A. Tarnlund (Uppsala, Sweden) F. Turini (Pisa, Italy) (Chairman)

Page 6

Table of C o n t e n t s L O P S T R Logic Frameworks for Logic Programs D.A. Basin (Max-Planck.Institut fiir Informatik, Saarbriicken, Germany) An Extended Transformation System for CLP Programs 17 N. Bensaou, L Guessarian (LITP- Universitd Paris 6, France) Using Call/Exit Analysis for Logic Program Transformation 36 D. Boulanger, M. Bruynooghe (Katholieke Universiteit Leuven, Belgium) A Transformation System for Definite Programs Based on Termination Analysis 51 J. Cook, J.P. Gallagher (University of Bristol, United Kingdom) On the Use of Inductive Reasoning in Program Synthesis: Prejudice and Prospects 69 P. Flener (Bilkent University, Ankara, Turkey) L. Popel(nsk~ (Masaryk University, Brno, Czech Republic) Transforming Specifications of Observable Behaviour into Programs 88 D. Gilbert (City University, London, United Kingdom) C. Hogger (Imperial College, London, United Kingdom) J. Zlatu3ka (Masaryk University, Brno, Czech Republic) On Specification Frameworks and Deductive Synthesis of Logic Programs 104 K.-K. Lau (University o Manchester, United Kingdom) M. Ornaghi (Universith degli Studi di Milano, Italy) Partial Evaluation of the "Real Thing" 122 M. Leuschel (Katholieke Universiteit Leuven, Belgium) Schema-Based Top-Down Design of Logic Programs Using Abstract Data Types 138 E. Marakakis, J.P. Gallagher (University of Bristol, United Kingdom) Generalizing Extended Execution for Normal Programs 154 S. Renault (INRIA-Rocquencourt, Le Chesnay, France) Partial Deduction of Disjunctive Logic Programs: A Declarative Approach 170 C. Sakama (ASTEM Research Institute of Kyoto, Japan) H. Seki (Nagoya Institute of Technology, Japan)

Page 7

viii Avoiding Non-Termination when Learning Logical Programs: A Case Study with FOIL and FOCL 183 G. Semeraro, F. Esposito, D. Malerba (Universitd degli Studi di Bari, Italy) C. Brunk, M. Pazzani (University of California, Irvine, U.S.A.) Propagation of Inter-Argument Dependencies in Tuple-Distributive Type Inference Systems 199 C. Solnon, M. Rueher (I3S, UNSA/CNRS, Sophia Antipolis, France) Logic Programming and Logic Grammars with First-Order Continuations 215 P. Tarau (Universitd de Moncton, Canada) V. Dahl (Simon Fraser University, Burnaby, Canada) Improving the Whelk System: A Type-Theoretic Reconstruction 231 G. A. Wiggins (University of Edinburgh, United Kingdom) META A Model of Costs and Benefits of Meta-Level Computation 248 F. van Harmelen (University of Amsterdam, The Netherlands) A Basis for a Multilevel Metalogic Programming Language 262 J. Barklund, K. Boberg (Uppsala University, Sweden) P. DeU'Acqua (Universitd degli Studi di Milano, Italy) Logic Programs with Tests 276 M. Mircheva (Bulgarian Academy of Sciences, Sofia, Bulgaria) An Architecture with Multiple Meta-levels for the Development of Correct Programs 293 B. Dunin-Kgplicz (University of Warsaw, Poland) More on Unfold/Fold Transformations of Normal Programs: Preservation of Fitting's Semantics 311 A. Bossi, S. Etalle (Universitd di Padova, Italy) Formal Semantics of Temporal Epistemic Reflection 332 W. van der Hoek, J.-J. Meyer, (Utrecht University and Free University Amsterdam, The Netherlands) J. Treur (Free University Amsterdam, The Netherlands)

Page 8

J• Temporal Semantics of Meta-Level Architectures for Dynamic Control of Reasoning 353 J. Treur (Free University Amsterdam, The Netherlands) GSdel as a Meta-Language for Composing Logic Programs 377 A. Brogi, S. Contiero (Universitd di Pisa, Italy) A Module System for Meta-Programming 395 P.M. Hill (University of Leeds, United Kingdom) Building Proofs in Context 410 G. Attardi, M. Simi (Universith di Pisa, Italy) Introspective Metatheoretic Reasoning 425 F. Giunchiglia, A. Cimatti (IRST, Trento, Italy) Abstract Debugging of Logic Programs 440 M. Comini, G.Levi (Universith di Pisa, Italy) G. Vitiello (Universith di Salerno, Italy) Author Index 451

Page 9

Logic Frameworks for Logic Programs* David A. Basin Max-Planck-Institut f'dr Informatik Saarbrllcken, Germany Email:basin~ mpi-sb.mpg.de Abs t r ac t . We show how logical frameworks can provide a basis for logic program synthesis. With them, we may use first-order logic as a foundation to formalize and derive rules that constitute program development calculi. Derived rules may be in turn applied to synthesize logic programs using higher-order resolution during proof that programs meet their specifications. We illustrate this using Paulson's Isabelle system to derive and use a simple synthesis calculus based on equivalence preserving transformations. 1 Introduction Ba c k g r o u n d In 1969 Dana Scott developed his Logic for Computable Functions and with it a model of functional program computation. Motivated by this model, Robin Milner developed the theorem prover LCF whose logic PP)~ used Scott 's theory to rea- son about program correctness. The LCF project 13 established a parad igm of formalizing a programming logic on a machine and using it to formalize different theories of functional programs (e.g., strict and lazy evaluation) and their correct- ness; al though the programming logic was simple, within it complex theories could be developed and applied to functional program verification. This paradigm can be characterized as formal development from foundations. Type theory and higher-order logic have been also used in this role. A recent example is the work of Paulson with ZF set theory. Although this theory appears primitive, Paulson used it to develop a theory of functions using progressively more powerful derived rules 24. Most work in formalized program development starts at a higher level; founda- tions are part of an informal and usually unstated recta-theory. Consider, for exam- ple, t ransformation rules like Burstall and Darlington's well known fold-unfold rules 7. Their rules are applied to manipulate formulas and derive new onesl afterwards * This research was funded by the German Ministry for Research and Technology (BMFT) under grant ITS 9102. The responsibility for the contents lies with the author. I thanks Tobias Nipkow and Larry Paulson for advice on Isabelle. I also thank Alan Bundy, Ina Kraan, Scan Matthews, and members of the Edinburgh Mathematical Reasoning Group for helpful discussions and collaboration on related work.

Page 10

some collection of the derived formulas defines the new program. The relationship of the new formulas to the old ones, and indeed which constitute the new program is part of their informal (not machine formalized) metatheory. So is the correctness of their rules (see 18, 8). In logic programming the situation is similar; for example, 30, 29 and others have analyzed conditions required for fold-unfold style transfor- mations to preserve equivalence of logic programs and indeed what "equivalence" means. Development from Foundations in Logic Programming We propose that, analogous to LCF, we may begin with a programming logic and derive within it a program development calculus. Derived rules can be applied to statements about program correctness formalized in the logic and thereby verify or synthesize logic programs. Logic programming is a particularly appropriate domain to formalize such development because under the declarative interpretation of logic programs as formulas, programs are formalizable within a fragment of first-order logic and are therefore amenable to manipulation in proof systems that contain this fragment. Indeed, there have been many investigations of using first-order logic to specify and derive correct logic programs 9, 10, 11, 17, 19. But this work, like that of Burstall and Darlington, starts with the calculus rather than the foundations. For example in 17 formulas are manipulated using various simplification rules and at the end a collection of the resulting formulas constitutes the program. The validity of the rules and the relationship of the final set of formulas (which comprise the program) to the specification is again part of the informal meta-theory. Our main contribution is to demonstrate that without significant extra work much of the informal metatheory can be formalized; we can build calculi from foundations and carry out proofs where our notion of correctness is more explicit. However, to do this, a problem must be overcome: first-order logic is too weak to directly formalize and derive proof rules. Consider for example, trying to state that in first-order logic we may replace any formula Vx.A by - ,3z .~A. We might wish to formulate this as Vx.A -4 -~3x.-~A. While this is provable for any instance A, such a generalized statement cannot be made in first-order logic itself; some kind of second-order quantification is required. 2 In particular, to formalize proof rules of a logic, one must express rules that (in the terminology of 15) are schematic and hypothetical. The former means that rules may contain variables ranging over formula. The latter means that one may represent logical consequence; in the above example consequence has been essentially internalized by implication in the object language. Rather than moving to a more powerful logic like higher-order logic, we show that one can formalize program development using weak logics embedded in logical frameworks such as Paulson's Isabelle system 25 or Pfenning's ELF 28. In our 2 First-order logic is too weak, but it is possible to formalize powerful enough first-order theories to express such rules by axiomatizing syntax, e.g., 32, 3, 23. However, such approaches require some kind of reflection facility to establish a link between the for- realized meta-theory and the desired theory where such rules are used. See 4 for a further discussion of this. Moreover, under such an approach unification cannot be used to identify program verification and synthesis.