WORKSHOPS IN COMPUTING Series edited by C: J. van Rijsbergen Also in this series ALPUK91, Proceedings of the 3rd UK Code Generation - Concepts, Tools, Techniques Annual Conference on Logic Programming, Proceedings of the International Workshop on Code Edinburgh, 10-12 April 1991 Generation, Dagstuhl, Germany, 20-24 May 1991 Geraint A.Wiggins, Chris Mellish and Robert Giegerich and Susan L. Graham (Eds.) Tim Duncan (Eds.) Z User Workshop, York 1991, Proceedings of the Specifications of Database Systems Sixth Annual Z User Meeting, York, International Workshop on Specifications of 16-17 December 1991 Database Systems, Glasgow, 3-5 July 1991 J.E. Nicholls (Ed.) David J. Harper and Moira C. Norrie (Eds.) Formal Aspects of Measurement 7th UK Computer and Telecommunications Proceedings of the BCS-FACS Workshop on Performance Engineering Workshop Formal Aspects of Measurement, South Bank Edinburgh, 22-23 July 1991 University, London, 5 May 1991 J. Hillston, P.J.B. King and R.J. Pooley (Eds.) Tim Denvir, Ros Herman and R.W. Whitty (Eds.) Logic Program Synthesis and Transformation AI and Cognitive Science '91 Proceedings of LOPS1R 91, International University College, Cork, 19-20 September 1991 Workshop on Logic Program Synthesis and Humphrey Sorensen (Ed.) Transformation, University of Manchester, 4-5 July 1991 5th Refinement Workshop, Proceedings of the 5th T.P. Clement and K..K. Lau (Eds.) Refinement Workshop, organised by BCS-FACS, London, 8-10 January 1992 Declarative Programming, Sasbachwalden 1991 Cliff B. Jones, Roger C. Shaw and PHOENIX Seminar and Workshop on Declarative Tim Denvir (Eds.) Programming, Sasbachwalden, Black Forest, Germany, 18-22 November 1991 Algebraic Methodology and Software John Darlington and Roland Dietrich (Eds.) Technology (AMAST'91) Proceedings of the Second International Conference Building Interactive Systems: on Algebraic Methodology and Software Architectures and Tools Technology, Iowa City, USA, 22-25 May 1991 Philip Gray and Roger Took (Eds.) M. Nivat, C. Rattray, T. Rus and G. Scollo (Eds.) Functional Programming, Glasgow 1991 ALPUK92, Proceedings of the 4th UK Proceedings of the 1991 Glasgow Workshop on Conference on Logic Programming, Functional Programming, Portree, Isle of Skye, London, 30 March-l April 1992 . 12-14 August 1991 Krysia Broda (Ed.) Rogardt He1dal, Carsten Kehler Holst and Philip Wadler (Eds.) Object Orientation in Z Susan Stepney, Rosalind Barden and David Cooper (Eds.) continued on back page ... Kung-Kiu Lau and Tim Clement (Eds.) Logic Program Synthesis and Transformation Proceedings of LOPSTR 92, International Workshop on Logic Program Synthesis and Transformation, University of Manchester, 2-3 July 1992 Sponsored by the Association for Logic Programming and ALPUK Springer-Verlag London Ltd. Kung-Kiu Lau, BSc, PhD Department of Computer Science The University Manchester M13 9PL, UK Timothy Paul Clement, MA, DPhil Department of Computer Science The University Manchester M13 9PL, UK ISBN 978-3-540-19806-2 British Library Cataloguing in Publication Data Logic Program Synthesis and Transformation: Proceedings of LOPSTR 92, International Workshop on Logic Program Synthesis and Transformation, University of Manchester, 2-3 July 1992. - (Workshops in Computing Series) I. Lau, K-.K. II. Clement, T.P. III . Series 005.1 ISBN 978-3-540-19806-2 ISBN 978-1-4471-3560-9 (eBook) DOI 10.1007/978-1-4471-3560-9 Library of Congress Cataloging-in-Publication Data A catalog record for this book is available from the Library of Congress Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this pUblication may only be reproduced, stored or transmitted, in any form, or by any means, with the prior permission in writing of the publishers, or in the case of repro graphic reproduction in accordance with the terms of licences issued by the Copyright Licensing Agency. Enquiries concerning reproduction outside those terms should be sent to the publishers. © Springer-Verlag London 1993 Originally published by Springer-Verlag Berlin Heidelberg New York in 1993 The use of registered names, trademarks etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant laws and regulations and therefore free for general use. The publisher makes no representation, express or implied, with regard to the accuracy of the information contained in this book and cannot accept any legal responsibility or liability for any errors or omissions that may be made. Typesetting: Camera ready by contributors 34{3830-543210 Printed on acid-free paper Foreword This volume consists of extended versions of selected papers originally presented at the LOPSTR 92 workshop held in Manchester in July 1992. The workshop followed LOPSTR 91 in what promises to be a very successful series, ably organised by Kung-Kiu Lau and his colleagues. The topic of both workshops (and hence this volume) was the synthesis and transformation of logic programs. This is a topic of central importance for the software industry. The demand for software can not be met by the current supply, in volume, in complexity or in reliability. The most promising solution to this multi-faceted problem is the increased automation of software production. Machine assisted program development can help us improve programmer productivity, take care of book-keeping, and apply mathematical methods to ensure correctness. Machine assistance is most effective when used to develop declarative programs, e.g. logic programs. The mathematical foundations of logic programs lend themselves to the use of mathematical methods of program development, and hence to automation. This volume describes some of the most recent advances in machine assisted development of logic programs. Among the new techniques described here are some for the transformation of an inefficient program into an equivalent, but more efficient, program, the synthesis of a program from a formal specification of its required behaviour, and the proof that a program terminates. As these techniques begin to leave the laboratory and become standard practice they promise to revolutionise the software industry. Edinburgh Alan Bundy August 1992 Preface Organising the second of a series of workshops brings its own particular concerns: those who attended the first workshop have made encouraging noises about another, but will this translate into submissions and attendance when the time comes, or is the field insufficiently active to support an annual event? In the event, we had eighteen talks, of which seventeen appear as papers in these proceedings and one as an extended abstract. What the proceedings can not show is the active discussion which went on around the formal presentations. The papers cover a broad range, from abstract models of logics to the details of register allocation in Prolog implementations, and including equational logics and database languages as well as the traditional Hom clauses of logic programming. The theme of partial deduction guided by abstract interpretation recurs in many different settings. Less clear is where the boundary between synthesis and transformation lies. A panel discussion at the end of the workshop addressed itself to this question, and resulted in not one but several equally convincing characterisations of the distinction. Once again, we should like to thank the Association for Logic Programming for supporting student travel to the workshop, ALPUK for their financial support for the workshop itself, and Lynn Howarth for her help with the organisation of the workshop. We should also like to thank the other Programme Committee members for their invaluable contribution and cooperatioq without which the workshop would not have been possible. We thank them and the other referees for their detailed and timely refereeing of the papers submitted to the workshop. LOPSTR 93 will take place in Louvain-la-Neuve, Belgium on 7-9 July. See you there! Manchester Kung-Kiu Lau and Tim Clement September 1992 Programme Committee Tim Clement University of Manchester, UK Danny De Schreye Katholieke Universiteit Leuven, Belgium Yves Deville Universite Catholique de Louvain, Belgium John Gallagher University of Bristol, UK Kung-Kiu Lau University of Manchester, UK (Chair) Referees Behnam Bani-Eqbal Dmitri Boulanger Maurice Bruynooghe Tim Clement Nicoletta Cocco Danny De Schreye Bart Demoen Philippe Devienne Yves Deville Pierre Flener John Gallagher Pat Hill Kung-Kiu Lan Bern Martens Maurizio Proietti Harold Simmons Geraint Wiggins Contents Logic Program Synthesis via Proof Planning I. Kraan, D. Basin and A. Bundy .......................................................... 1 Deductive Synthesis of Programs for Query Answering D. Nardi and R. Rosati ........................................................................ 15 Synthesis of Narrowing Programs C. Lorta-Saenz ......... ....... ........................................... .......................... 30 A Unifying View of Structural Induction and Computation Induction for Logic Programs L. Fribourg and H. Olsen .................................................................... 46 Proof Nets M. Ornaghi ........................................................................................... 61 The LOPS Approach: A Transformational Point of View (Extended Abstract) G. Neugebauer ..................................................................................... 80 Best-first Strategies for Incremental Transformations of Logic Programs M. Proietti and A. Pettorossi ............................... ................ ................ 82 Deriving Transformations of Logic Programs Using Abstract Interpretation D. Boulanger and M. Bruynooghe ...................................................... 99 A Rationalisation of the ATMS in Terms of Partial Evaluation E. Lamma and P. Mello ..................................................................... 118 Intensional Query Answering: An Application of Partial Evaluation G. De Giacomo .................................................................................. 132 Deletion of Redundant Unary Type Predicates from Logic Programs 1. Gallagher and D.A. de Waal.................................................. ....... 151 Automatic Termination Analysis K. Verschaetse, S. Decorte and D. De Schreye ................................ 168 xii Contents Applications of Unfolding in Prolog Programming J. Jones ............................................................................................... 184 An Unfold Rule for Full Prolog s. Prestwich ....................................................................................... 199 Logimix: A Self-Applicable Partial Evaluator for Prolog T.A!. Mogensen and A. Bondorf................................................. ....... 214 Towards Optimization of Full Prolog Programs Guided by Abstract Interpretation A. Parrain. P. Devienne and P. Lebegue ......................................... 228 On the Transformation of a Prolog Program to a More Efficient Binary Program B. Demoen .............................................................................................. 242 Efficient Compilation of Lazy Narrowing into Prolog J.A. Jimenez-Martin. J. Marino-Carballo and J.J. Moreno-Navarro ................................................................. 253 Author Index ..................................................................................... 271 Logic Program Synthesis via Proof Planning Ina Kraan Department of Artificial Intelligence University of Edinburgh Edinburgh, Scotland, U.K.