Skip to main content
main-content

Über dieses Buch

Recent developments in computer science clearly show the need for a better theoretical foundation for some central issues. Methods and results from mathematical logic, in particular proof theory and model theory, are of great help here and will be used much more in future than previously. This book provides an excellent introduction to the interplay of mathematical logic and computer science. It contains extensively reworked versions of the lectures given at the 1997 Marktoberdorf Summer School by leading researchers in the field.
Topics covered include: proof theory and specification of computation (J.-Y. Girard, D. Miller), complexity of proofs and programs (S. R. Buss, S. S. Wainer), computational content of proofs (H. Schwichtenberg), constructive type theory (P. Aczel, H. Barendregt, R. L. Constable), computational mathematics, (U. Martin), rewriting logic (J. Meseguer), and game semantics (S. Abramski).

Inhaltsverzeichnis

Frontmatter

Game Semantics

Abstract
The aim of this chapter is to give an introduction to some recent work on the application of game semantics to the study of programming languages.
Samson Abramsky, Guy McCusker

Notes on the Simply Typed Lambda Calculus

Abstract
The simply typed lambda calculus, of these notes, has types built up from atomic types using the function type operation that forms a new typeABfrom typesA,B.The calculus can be viewed as a refined version of the purely implicational fragment of intuitionistic logic. The refinement consists in using terms of the untyped lambda calculus to represent formal derivations of the logic.
Peter Aczel

Problems in Type Theory

Abstract
In this paper the reader will be introduced to type theories (predicative and impredicative, with and without inductive types) by a short section giving theoretical background and by another section with exercises about the calculus of constructions and its fine structure the lambda cube.
Henk Barendregt

Formal Correctness Proofs of Functional Programs: Dijkstra’s Algorithm, a Case Study

Abstract
One can argue that writing proofs might be better than writing programs, for the following simple reason: There is no algorithm that can check whether a program meets its specification, but it is easy to check whether a given proof is correct.
Holger Benl, Helmut Schwichtenberg

Propositional Proof Complexity an Introduction

Abstract
This article is an abridged and revised version of a 1996 McGill University technical report [15]. The technical report was based on lectures delivered by the author at a workshop in Holetown, Barbados and on the authors prepared overhead transparencies. The audience at this workshop wrote scribe notes which then formed the technical report [15]. The material selected for the present article corresponds roughly to the content of the author’s lectures at the NATO summer school held in Marktoberdorf, Germany in July-August 1997.
Samuel R. Buss

Formalizing Decidability Theorems About Automata

Abstract
Is it possible to create formal proofs of interesting mathematical theorems which are mechanically checked in every detail and yet are readable and even faithful to the best expositions of those results in the literature? This paper answers that question positively for theorems about decidable properties of finite automata. The exposition is from Hoperoft and Ullman’s classic 1969 textbookFormal Languages and Their Relation to Automata.This paper describes a successful formalization which is faithful to that book.
The requirement of being faithful to the book has unexpected consequences, namely that the underlying formal theory must include primitive notions of computability. This requirement makes a constructive formalization especially suitable. It also opens the possibility of using the formal proofs to decide properties of automata. The paper shows how to do this.
Robert L. Constable

On the Meaning of Logical Rules I: Syntax Versus Semantics

Abstract
« Oui c’est imbécile ce que je dis ! Seulement je ne sais pas comment concilier tout ça. Il est sûr que je ne me sens libre que parce que j’ai fait mes classes et que je ne sors de la fugue que parce que je la sais. »
Claude-Achille Debussy
Entretiens avec Ernest Guiraud1890.
Jean-Yves Girard

Complexity of Primitive Recursion

Abstract
Primitive recursion is the fundamental example of “recursive definition”. It is intimately related with “for-loops” in programming, and with the E1induction rule in proof theory. Though the primitive recursive functions contain many fast-growing “non-feasible” functions, recent work of Bellantoni-Cook and others shows how a natural two-sorted restriction of primitive recursion serves to characterize complexity classes such as polynomial time and linear space. The lectures presented here provide a technical introduction to this area.
W. G. Handley, S. S. Wainer

Computers, Reasoning and Mathematical Practice

Abstract
Computer aided formal reasoning, mathematical assistants which check complex arguments and automated proofs of new and interesting mathematical results have been part of the dream of computational logic for many years. This dream is in part being realised by the success of endeavours such as the Mizar project [110], which has produced many volumes of formalised mathematics, and McCune’s recent proof of the Robbins conjecture [79], cited, along with autonomous vehicle guidance and the chess program Deep Blue, as one of the five most significant achievements of artificial intelligence [114]. Yet it is still the case that few mathematicians use such programs, and their impact outside certain specialised communities has been less than might have been hoped.
Ursula Martin

Research Directions in Rewriting Logic

Abstract
Rewriting logic expresses an essential equivalence between logic and computation. Systemstatesare in bijective correspondence withformulas, and concurrentcomputationsare in bijective correspondénce withproofs.Given this equivalence between computation and logic, a rewriting logic axiom of the form t → t’ has two readings. Computationally, it means that a fragment of a system’s state that is an instance of the patterntcanchangeto the corresponding instance oft’concurrently with any other state changes; logically, it just means that we can derive the formulat’from the formulat.Rewriting logic is entirely neutral about the structure and properties of the formulas/statest.They are entirelyuser-definableas an algebraic data type satisfying certain equational axioms. Because of this ecumenical neutrality, rewriting logic has, from a logical viewpoint, good properties as alogical framework, in which many other logics can be naturally represented. And, computationally, it has also good properties as asemantic framework, in which many different system styles and models of concurrent computation and many different languages can be naturally expressed without any distorting encodings. The goal of this paper is to provide a relatively gentle introduction to rewriting logic, and to paint in broad strokes the main research directions that, since its introduction in 1990, have been pursued by a growing number of researchers in Europe, the US, and Japan. Key theoretical developments, as well as the main current applications of rewriting logic as a logical and semantic framework, and the work on formal reasoning to prove properties of specifications are surveyed.
José Meseguer

Sequent Calculus and the Specification of Computation

Abstract
The sequent calculus has been used for many purposes in recent years within theoretical computer science. In these lectures, we shall highlight some of its uses in the specification of and reasoning about computation.
During the search for cut-free sequent proofs, the formulas in sequents are re-arranged and replaced with other formulas. Such changes can be used to model the dynamics of computation in a wide range of applications. For various reasons, we shall be interested in “goal-directed proof search” and will examine intuitionistic logic and linear logic for subsets that support this particularly simple form of search. We will show, quite surprisingly, that with the appropriate selection of logical connectives, goal-directed search is complete for all of linear logic. This fact leads naturally to the design of a logic programming-like language based on linear logic. The resulting specification language, called Forum, is an expressive and rich specification language suitable for a wide range of computational paradigms.
After providing an overview of sequent calculus principles, we shall develop the notion of goal directed search for a variety of logics, starting with the intuitionistic logic theory of Horn clauses and hereditary Harrop formulas. We shall provide various example specifications in these logics, especially examples that illustrate how rich forms of abstractions can be captured. Finally, we briefly indicate how the notion of goal-directed proof search can be extended to linear logic.
No advanced knowledge of the sequent calculus or of linear logic will be assumed, although some familiarity with their elementary syntactic properties will be useful. Similarly, some acquaintance with the basic concepts of the lambda-calculus and intuitionistic logic will also be useful.
Dale Miller

Backmatter

Weitere Informationen