John McCarthy Artificial Intelligence and Mathematical Theory of Computation Papers in Honor of John McCarthy edited by Vladimir Lifschitz Department of Computer Sciences and Department of Philosophy university of Texas at Austin Austin, Texas ACADEMIC PRESS, INC. Harcourt Brace Jovanovich, Publishers Boston San Diego New York London Sydney Tokyo Toronto This book is printed on acid-free paper. Θ Copyright © 1991 by Academic Press, Inc. All rights reserved. No part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission in writing from the publisher. ACADEMIC PRESS, INC. 1250 Sixth Avenue, San Diego, CA 92101 United Kingdom Edition published by ACADEMIC PRESS LIMITED 24-28 Oval Road, London NW1 7DX Library of Congress Cataloging-in-Publication Data Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy / [edited by] Vladimir Lifschitz. p. cm. Includes bibliographical references and index. ISBN 0-12-450010-2 (acid-free paper) 1. Artificial intelligence. 2. Numerical calculations. 3. Computers. 4. Programming (Electronic computers) 5. McCarthy, John, 1927- I. McCarthy, John, 1927- II. Lifschitz, Vladimir. Q335.6.A77 1991 006.3-dc20 91-22565 CIP Printed in the United States of America 91 92 93 94 9 8 7 6 5 4 3 2 1 Preface This is a collection of papers by distinguished researchers, colleagues and former students of Professor John McCarthy, published on the occasion of his sixty-fourth birthday. The papers discuss technical, historical and philosophical problems related to two areas of computer science: artificial intelligence and the mathematical theory of computation. The range of subjects discussed here includes automated deduction, logic programming, and the logic approach to artificial intelligence; knowledge representation and com- monsense reasoning; nonmonotonic reasoning and circumscription; robotics and the commercial applications of artificial intelligence; func- tional programming, LISP and symbolic computation; the semantics of programming languages and proving properties of programs; abstract data types and parallelism. The book creates a broad picture of com- puter science research in 1991. It also shows how much the computer science of today owes to John McCarthy's ideas and leadership. Vladimir Lif schitz University of Texas ix Contributors List Numbers in parentheses indicate pages on which the authors ' contributions begin. Robert S. Boyer (7) Computational Logic, Inc., 1717 W. 6th Street, Suite 290, Austin, Texas 78703 Robert Cartwright (27) Department of Computer Science, Rice Univer- sity, Houston, Texas 77251-1892 Solomon Feferman (47) Department of Mathematics, Stanford Univer- sity, Stanford, California 94305 Jerome A. Feldman (65) International Computer Science Institute, 1947 Center Street, Suite 600, Berkeley, California 94704-1105 Robert E. Filman (73) IntelliCorp, Inc., 1975 El Camino Real West, Mountain View, California 94040 Richard P. Gabriel (91) Lucid, Inc., 707 Laurel Avenue, Menlo Park, California 94015 Chris Goad (109) Silma Incorporated, 1601 Saratoga-Sunnyvale Boule- vard, Cupertino, California 95014 David M. Goldschlag (7) Computational Logic, Inc., 1717 W. 6th Street, Suite 290, Austin, Texas 78703 xi xiv Contributors List Richard Weyhrauch (467) lbuki, Los Altos California 94022 Gio Wiederhold (345) Computer Science Department, Stanford Univer- sity, Stanford, California 94305 A Short Sketch of the Life and Career of John McCarthy David J. Israel1 AI Center SRI International Menlo Park, California 94025 John McCarthy was born on Sept. 4, 1927 in Boston, Massachusetts. He received his B.S. in Mathematics from the California Institute of Technol- ogy in 1948, and his Ph.D. in Mathematics from Princeton University in 1951. After a brief stint at Princeton as a research instructor (1951-1953), he taught at Stanford (1953-1955) and Dartmouth (1955-1958). In 1958, he moved to MIT as an Assistant Professor of Communication Science; he was promoted to Associate Professor in 1961. McCarthy then moved to Stanford as a Professor of Computer Science in 1962. In 1987, he became the Charles M. Piggot Professor of Engineering; in the fall of that year he was the Bobby R. Inman Professor of Computer Science at the Uni- versity of Texas at Austin. Other honors and distinctions include: Sloan Fellow in Physical Science (1957-1961), ACM National Lecturer (1961), A.M. Turing Award from the ACM (1971), Sigma Xi National Lecturer (1977), Research Excellence Award, International Joint Conference on Ar- tificial Intelligence (1985), the Kyoto Prize (1988). Professor McCarthy has received honorary degrees from Linköping University (1986), Colby College (1990), and Universidad Politecnica de Madrid (1991). He has been elected to the American Academy of Arts and Sciences, the National Academy of Engineering (1987), and the National Academy of Sciences (1989). He has been President of the American Association for Artificial Intelligence (1983-1984) and since 1975, a member of the editorial board of Artificial Intelligence Journal In November, 1990, Professor McCarthy was awarded the National 1 This note was prepared for, and a version first published in, the Notices of the American Mathematical Society, Volume 38, Number 4, April 1991, published by the American Mathematical Society. 1 Copyright © 1991 by Academic Press, Inc. All rights of reproduction in any form reserved. ISBN 0-12-450010-2 2 Israel Medal of Science by President Bush in a ceremony at the White House. The Medal of Science is the nation's highest honor in science. Professor McCarthy has made fundamental contributions to both the theory and practice of computer science. Perhaps more than that of any single researcher since Turing, his work has shaped ideas about Symbolic Computation. In particular, he can with some justice be said to have cre- ated the field of artificial intelligence (AI) and has long been among the most important researchers in the field. He coined the term artificial intelligence (1955), and organized the first major conference on AI, the Dartmouth Conference of 1956. While at MIT, he and Marvin Minsky organized and directed the Artificial Intelligence Project. Under their leadership, the MIT AI Lab became the locus of an extraordinary flowering of significant and pioneering work in a wide range of fields, from robotics to theory of compu- tation to computer music and research on human-computer interfaces. In 1963, Professor McCarthy organized the Artificial Intelligence Laboratory at Stanford University and was its director until 1980. In addition to his intellectual leadership, Professor McCarthy has long been active in support of the human rights of computer professionals, especially those from East- ern Europe and the Soviet Union. (For more on this, see Jack Minker's contribution at the end of Chapter 17.) In 1958, McCarthy developed the LISP (for LISt Processor) program- ming language. For over 30 years, LISP has been the principal program- ming language in AI. At the same time that he was developing LISP, Mc- Carthy was also a leading member of the groups that developed ALGOL 58 and ALGOL 60. The design of programming languages remains an im- portant concern for Professor McCarthy. Beginning in the early '80s, he began thinking about very high-level programming languages whose cen- tral features derived from aspects of the human use of natural languages in communication. His first such effort was the Common Business Communi- cation Language (1982). Most recently, he has been developing Elephant 2000, a progamming language based on ideas from the theory of speech acts. This work brings together McCarthy's research interests in the the- ory of programming languages and in the representation of common-sense knowledge. In 1962, McCarthy published the first fully worked out design proposal for time-sharing ("Time-Sharing Computing Systems") and played a crucial role in implementing the first widely used time-sharing system at BBN. Very soon after arriving at Stanford, Professor McCarthy led the group that developed THOR, the first display-oriented time-sharing system ( "THOR— A Display Based Time-Sharing System"). THOR represented an important advance over teletype-based systems and included many of the features Life and Career of John McCarthy 3 found in modern PCs and workstations. Indeed, by the early '70s, Professor McCarthy had already begun thinking about the potential of networks of personal computers in the home ( "The Home Information Terminal," first presented in 1972). Not content with developing two of the most important high-level pro- gramming languages, McCarthy also made pioneering contributions in the mathematical theory of computation and the formal semantics of program- ming languages. In 1960, he presented both an operational semantics and a recursion theoretic analysis of LISP, and proved its universality, more properly the universality of its apply function. In 1966, he applied similar techniques to an analysis of a fragment of ALGOL. This work introduced a number of important ideas for proving properties of recursive programs, in particular the use of fixed point properties to prove program equivalence by way of a rule of recursion induction. McCarthy's work on the mathematics of computation was strongly influenced by the research of another 1990 Na- tional Medalist, Professor Stephen Kleene; indeed, it represented the first attempt to apply a Kleene-style framework for recursion theory, based on systems of equations defining functions, to real programming languages. While McCarthy has continued doing important work in the mathemat- ical theory of computation, including further research on proof rules for recursive programs (1979) and on multiprocessing versions of LISP (1984), his attention has turned increasingly to fundamental problems in Artificial Intelligence. The original impetus for the development of LISP was to experiment with his ideas for an "Advice Taker" (1958), a program for representing and solving problems—both mathematical and everyday nonmathematical problems—by performing derivations in a formal language known as the situation calculus, which extends first-order languages in certain ways, e.g. by the addition of conditional expressions (of the form IF Ρ then a ELSE ft, where Ρ is a formula and a and b are terms) and first-order lambda expressions as function and predicate expressions. (The use of conditional expressions is also fundamental to both the design and the analysis of LISP.) The situation calculus is still widely used for representing nonmathematical problems, especially those that can be posed as involving a single agent. The "Advice Taker" was the first systematic attempt to describe and analyze what might be called a sentential automaton—the term itself may be McCarthy's. The central idea was that all the basic features of a problem and of the ways of solving the problem (the applicable heuristics) should be representable in a formal language. Some sentences of the language were to be treated as imperatives; these were to be obeyed. Others were declar- ative; these were intended to be treated as descriptions of various aspects 4 Israel of the problem situation. The basic cycle of the program was somehow to choose a list of declarative sentences (premises) to apply a deduction routine to. Thus, what the system knows—has been told—is represented as an axiomatic theory. The crucial point was that one did not have to write new programs as new problems were confronted; one simply told the system new things. For McCarthy the most interesting applications were to everyday problems; this meant expressing everyday common-sense con- ceptions about familiar objects and our interactions with them, especially those conceptions involving our beliefs and knowledge, our abilities, and the preconditions and effects of our actions. For more than 30 years, McCarthy has been pursuing, and has been urging others to pursue, the goal of a large, publicly accessible common- sense knowledge base, to be expressed in a logical formalism, and to be used in any one of a wide range of applications areas. Early on, it became clear to him that sound (truth-preserving) logical deduction was an inad- equate model of common-sense reasoning. Such reasoning often involves nonstrict or other things being equal generalizations and it exhibits a cer- tain nonmonotonicity. A set of premises Γ can be an adequate reason for inferring P, while a superset Γ' is not. For instance, Γ' might include the information that other things are not equal. This contrasts strikingly with the structure of deductive reasoning (proof). Much of McCarthy's work since 1980 has been devoted to analyzing and formally modeling such rea- soning. In 1977, he introduced the idea of circumscription, which is a rule of conjecture to be applied to first-order theories; the point of such a con- jecture is that a certain predicate, or more generally a certain formula, is to have the minimal extension consistent with the truth of the original the- ory. The intuitive force of the conjecture is that other things are indeed as equal as they can be, given the original premises (axioms). Thus, one can think of the strategy as minimizing exceptions or abnormalities. Professor McCarthy's working hypothesis is that the addition to first-order logic of this single schematic rule—and its intelligent use—is sufficient to provide a model of common-sense reasoning. A number of other formalisms for deal- ing with problems of common-sense reasoning have been introduced; but as with LISP and the situation calculus, McCarthy's contributions continue to be of central importance. We end by quoting the citation for Professor McCarthy's National Medal of Science: [F]or his fundamental contribution to computer science and ar- tificial intelligence, including the development of the LISP pro- gramming language, the mathematical theory of computation, the concept and development of time-sharing, the application