Skip to main content

Über dieses Buch

For some years, specification of software and hardware systems has been influenced not only by algebraic methods but also by new developments in logic. These new developments in logic are partly based on the use of algorithmic techniques in deduction and proving methods, but are alsodue to new theoretical advances, to a great extent stimulated by computer science, which have led to new types of logic and new logical calculi. The new techniques, methods and tools from logic, combined with algebra-based ones, offer very powerful and useful tools for the computer scientist, which may soon become practical for commercial use, where, in particular, more powerful specification tools are needed for concurrent and distributed systems. This volume contains papers based on lectures by leading researchers which were originally given at an international summer school held in Marktoberdorf in 1991. The papers aim to give a foundation for combining logic and algebra for the purposes of specification under the aspects of automated deduction, proving techniques, concurrency and logic, abstract data types and operational semantics, and constructive methods.



Distributed Action Systems

From Sequential to Nonsequential Systems or From Transition Systems to Generalized Petri Nets
Traditionally theoretical informatics is based on the notion of a sequential machine for the stepwise computation of a function as a mechanization/abstraction of the activity of a human calculator. Due to developments in hardware, applications and theoretical informatics it is useful and possible to take a more general basis and consider a group of interacting humans as a paradigm for basic notions in theoretical informatics.
Such a group can be constituted by the need of several people to have organized access to common limited resources (this is the viewpoint taken in operating systems theory since a long time) or a group brings together people who want to achieve common goals by cooperation (this view was much used in artificial intelligence).
There are two basic ways of organizing the activities in the group: by central control based on hierarchy and force (this is the traditional approach in informatics) or by cooperative coordination using communication mechanisms for reaching consensus.
With these ideas in mind we can look at informatics in a new way, and we may recognize, that we need many new concepts but also that quite a number of known (traditional) concepts can well be interpreted in the new way and exhibit interesting properties.
In the following we will see how the classical theory of (finite and pushdown) automata and of (regular and context-free) formal languages and grammars can be built up from the point of view of specification of (structure and semantics) of distributed systems of actions (instead of considering them only from the viewpoint of a compiler writer). In the second part we develop this idea further and introduce Petri nets as a basic general model for distributed action systems and generalize them by including some sort of recursion.
Wilfried Brauer

Lectures on:Classical Proofs as Programs

In the 1970’s the idea of using constructive proofs of theorems as programs was advocated and studied theoretically [6, 24]. In the 1980’s the computer science community started to experiment with this concept [5, 29], and today there are several prototype systems that enable us to write programs in this way [10, 22, 7, 29, 12]. So for instance, from a constructive proof of the Intermediate Value Theorem, a system like Nuprl [10] can extract a program which computes the intermediate value to any precision required [8].
Robert L. Constable

Linear Logic: A Survey

This introduction to linear logic is organised in four chapters:
Thesyntaxof linearlogic Here the formal system is introduced, with a special emphasis on the treatment of structural rules: weakening and contraction become logical rules for new connectives, 7 and !. Informal examples are introduced to illustrate this shift of viewpoint: linear logic is not about situations but about actions.
Thedenotational semantics of linear logic Coherent spaces (a drastic simplification of Scott domains) are introduced; semantically speaking, linear logic appears as a refinement of intuitionistic logic.
Proof-nets The specificities of linear logic (e.g., symmetries I/O) suggest a new kind of syntax for proofs, with intrinsic parallel features. Proof-nets are graphs (and not trees as usual) without explicit sequentialization; the difficult question is precisely that of the correcmess criterion, i.e., of the existence of implicit sequentialisations.
On the unity of logic This chapter is about logic (without adjective): from the experience gathered in linear logic, it seems possible to put all (decent) logical systems together. A sequent calculus LU is introduced: classical, intuitionistic and linear logics appear as fragments of this unified system. Many aspects of linear logic (especially applied ones) have been excluded from this approach; not because they are inessential, but because they do not fit with our pattern. We shall not try to make an enumeration (necessarily superficial) of these missing topics. Maybe the approach to linear logic though other authors (especially [Sv] and [T] which contain good bibliographies) is the best way to complete this initiation.
Jean-Yves Girard

Some proof-theoretic aspects of logic programming

This article presents some proof-theoretic aspects of logic programming and relates logic programming to the theory of inductive definability. The general semantic framework is provided by closure conditions and inductive definitions over Herbrand bases and three-valued structures. Syntactically we work with a rule based sequent calculus and a three-valued subsystem thereof. Also some connections between quasi cut free provability in the sequent calculus and resolution for Horn clauses are mentioned.
Gerhard Jäger

The Safety-Progress Classification

We propose a classification of temporal properties into a hierarchy, called the safety-progress classification. The classes of the hierarchy are characterized through four views: a language-theoretic view, a topological view, a temporal logic view, and an automata view. In the topological view, the considered hierarchy coincides with the two lower levels of the Borel hierarchy, starting with the closed and open sets. For properties that are expressible by temporal logic and automata, we provide syntactic characterizations of the formulas and automata that correspond to properties in the different classes. We relate this classification to the well-known safety-liveness classification, and show that in some sense the two are orthogonal to one another.
Edward Chang, Zohar Manna, Amir Pnueli

The Polyadic π-Calculus: a Tutorial

The π-calculus is a model of concurrent computation based upon the notion of naming. It is first presented in its simplest and original form, with the help of several illustrative applications. Then it is generalized from monadic to polyadic form. Semantics is done in terms of both a reduction system and a version of labelled transitions called commitment; the known algebraic axiomatization of strong bisimilarity is given in the new setting, and so also is a characterization in modal logic. Some theorems about the replication operator are proved.
Justification for the polyadic form is provided by the concepts of sort and sorting which it supports. Several illustrations of different sortings are given. One example is the presentation of data structures as processes which respect a particular sorting; another is the sorting for a known translation of the λ-calculus into π-calculus. For this translation, the equational validity of β-conversion is proved with the help of replication theorems. The paper ends with an extension of the π-calculus to ω-order processes, and a brief account of the demonstration by Sangiorgi [27] that higher-order processes may be faithfully encoded at first-order. This extends and strengthens the original result of this kind given by Thomsen [28] for second-order processes.
Robin Milner

An Introduction to Action Semantics

Formal semantics is a topic of major importance in the study of programming languages. Its applications include documenting language design, establishing standards for implementations, reasoning about programs, and generating compilers.
These notes introduce action semantics, a recently-developed framework for formal semantics. The primary aim of action semantics is to allow useful semantic descriptions of realistic programming languages.
Peter D. Mosses

Minimal Logic for Computable Functions

We discuss a specification language with variables for higher order functional and constants for computable functional (cf. Plotkin [9]). In this language it is possible to represent functional objects (like programs or circuits transforming streams of data) by terms and carry out formal proofs that they meet a given specification.
Helmut Schwichtenberg

Infinite Synchronous Concurrent Algorithms The Algebraic Specification and Verification of a Hardware Stack

An infinite synchronous concurrent algorithm (isca) is an algorithm composed of infinitely many modules and channels, computing and communicating in parallel, and synchronised by a global clock. A theory of such algorithms will explore infinite parallelism and also help in understanding computation involving unbounded finite parallelism. The theory presented is a generalisation of a theory of finite synchronous concurrent algorithms, based on computable functions on many sorted algebras. We use algebras to model specifications and iscas, and epimorphisms and isomorphisms to model related notions of implementation.
We will model a hardware stack with unbounded capacity using an infinite synchronous concurrent algorithm and prove that the architecture is correct; special emphasis is placed on using algebras to formalise the various stages of the development.
First we specify equationally a class of hardware stacks that operate in time with streams of data and commands. We then present a specific algebraic model Str op (S(X)) of the hardware stack axioms that computes over an arbitrary data set X and which serves as a mathematical specification for the hardware stack. Next we define an isca and we prove that this isca implements the model Str op (S(X)) of the stack. Finally we consider the refinement of the general algebraic model and isca over the set X to an algebraic model and isca based on the set 0,1 of bits.
B. McConnell, J. V. Tucker

Four Lectures on Primitive Recursion

The history of primitive recursion traces back to Dedekind, Hubert, Gödel, Ackermann, Herbrand, Péter and Kleene. Some may consider it ‘old-hat’ but it is no less important for all that. The aim in these lectures is merely to present the basic ideas and four different characterizations, illustrating fundamental connections with complexity, term-rewriting and proof theory.
Stanley S. Wainer

Structured Specifications: Syntax, Semantics and Proof Calculus

In this paper, a small but expressive language is presented that allows to write algebraic specifications in a structured and modular way. Proof rules are developed for each construct of the language; in particular, proof systems are given for flat specifications, for structured specifications and the verification of implementations. The language consists of four constructs: one for constructing a flat specification (from a signature and a set of axioms) and three operators for exporting a subsignature, for renaming and for combining specifications.
The proof system for flat specifications extends the proof rules of first-order logic by an infinitary rule for relativized quantification w.r.t. standard interpretations of term generated models. Two different techniques for proving the validity of a formula in modular specifications are studied: The first one consists in constructing an equivalent normal form of a structured specification and using a proof system for normal forms, whereas in the second one proofs follow the syntactic structure of the specifications. Finally, a system for proving that a specification is a refinement of another specification is established
All proof systems are shown to be sound and relatively complete.
Martin Wirsing


Weitere Informationen