The calculus of relations turned into an important conceptual and methodological tool in computer science. The methods presented in this book include questions of relational databases, applications to program specification, resource-conscious linear logic, semantic and refinement consideration, nonclassical logics for reasoning about programs, tabular methods in software construction, algorithm development, linguistic problems, followed by a comprehensive bibliography. The reader gets an overview of the wide-ranging applicability of relational methods in computer science. ``... While this is a multi-authored volume, the authors have done an excellent job of making it read like a single-authored work ... The book can be viewed as a set of snapshots of a family of research and researchers at one point in time. If you are interested in relational problems, I can think of no better introduction ...'' — Computing Reviews

The calculus of relations turned into an important conceptual and methodological tool in computer science. The methods presented in this book include questions of relational databases, applications to program specification, resource-conscious linear logic, semantic and refinement consideration, nonclassical logics for reasoning about programs, tabular methods in software construction, algorithm development, linguistic problems, followed by a comprehensive bibliography. The reader gets an overview of the wide-ranging applicability of relational methods in computer science. ``... While this is a multi-authored volume, the authors have done an excellent job of making it read like a single-authored work ... The book can be viewed as a set of snapshots of a family of research and researchers at one point in time. If you are interested in relational problems, I can think of no better introduction ...'' — Computing Reviews

In this note a concise formulation of mathematical induction is presented. This formulation is in terms of relations only, without mentioning the related objects. It is shown that the induction principle in this form lends itself very well for use in calculational proofs. As a non-trivial example a proof of a generalization of Newman's lemma is given.

We give a criterion for the union of well-founded (i.e., noetherian) relations to be well-founded, generalizing results of Geser and of Bachmair-Dershowitz. The proof is written in a calculational style and is conducted entirely in regular algebra.

The calculus of relations turned into an important conceptual and methodological tool in computer science. The methods presented in this book include questions of relational databases, applications to program specification, resource-conscious linear logic, semantic and refinement consideration, nonclassical logics for reasoning about programs, tabular methods in software construction, algorithm development, linguistic problems, followed by a comprehensive bibliography. The reader gets an overview of the wide-ranging applicability of relational methods in computer science. ``... While this is a multi-authored volume, the authors have done an excellent job of making it read like a single-authored work ... The book can be viewed as a set of snapshots of a family of research and researchers at one point in time. If you are interested in relational problems, I can think of no better introduction ...'' — Computing Reviews

We consider equational theories of binary relations, in a language expressing composition, convers, and lattice operations. We treat the equaations valid in the standard model of sets and also define a hierarchy of equational axiomatisations stratifying the standard theory. By working directly with a presentation of relation-expressions as graphs we are able to define a notion of reduction which is confluent and strongly normalising, in sharp contrast to traditional treatments based on first-order terms. As consequences we obtain normal forms, decidability of the decision problem for equality for each theory. in particular we show a non-deterministic polynomial-time upper bound for the complexity of the decision problems.

Some varieties that are extensions of relational algebras with two constants that play the role of projections are studied. The classes have as a subvariety the abstract fork algebra (AFA) equivalent variety involving projections. They are obtained by weakening some laws valid in AFA. Some applications of the varieties in the literature and in the specification of abstract data types are exhibited. For each of the classes obtained, an answer is given to the question: ``Is the relational reduct of the class representable?''. For the subvarieties formed with the models that have a repressentable relational reduct, a repressentation theorem is proved. For them the finitization problem is studied. Next the varieties presented are compared by means of the inclusion order. For each class the problem of characterizing finite models is considered. Simple models in the varieties are studied. Finally, the existence of equivalent classes with a binary operation like fork is studied.

Libra is a general-purpose programming language based on the algebra of binary relations. It attempts to unify functional and logic programming, retaining the advantages of both, and avoiding some of the problems. It has all the features needed of a programming language, and a straightforward semantic interpretation. Since program specifications are easily expressed as relations, it offers a simple path from a specification to a program and from the program to its proof of correctness. The algebra of binary relations has several operators whose effects are like those of familiar procedural language constructs, for example, relational composition is analogous to sequential execution. The Libra language is illustrated by its application to a simple programming exercise. Some conclusions are drawn.

Parallel and distributed derivations are introduced and studied in the single-pushout approach, which models rewriting by pushout constructions in appropriate categories of partial morphisms. We present a categorical framework for this approach in an axiomatic way. Models of this categorical framework are among others: graphs, hypergraphs, relational structures, and algebraic specifications with suitable partial morphisms. Several new results concerning parallelism and distributed parallelism are presented which are even new in the example categories.

Map reasoning is concerned with relations over an unspecified domain of discourse. Two limitations w.r.t. first-order reasoning are: only dyadic relations are taken into account; all map formulas are equations, having the same expressive power as first-order sentences in three variables. The map formalism inherits from the Peirce-Schröder tradition, through contributions of Tarski and many others. Algebraic manipulation of map expressions (equations in particular) is much less natural than developing inferences in first-order logic; it may in fact appear to be overly machine-oriented for direct hand-based exploitation. The situation radically changes when one resorts to a convenient representation of map expressions based on labeled graphs. The paper provides details of this representation, which abstracts w.r.t. inessential features of expressions. Formal techniques illustrating three uses of the graph representation of map expressions are discussed: one technique deals with translating first-order specifications into map algebra; another one, with inferring equalities within map calculus with the aid of convenient diagram-rewriting rules; a third one with checking, in the specialized framework of set theory, the definability of particular set operations. Examples of use of these techniques are produced; moreover, a possible approach to mechanization of graphical map-reasoning is outlined.

Tarski-Givant's map calculus is briefly reviewed, and a plan of research is outlined aimed at investigating applications of this ground equational formalism in the theorem-proving field. The main goal is to create synergy between first-order predicate calculus and the map calculus. Techniques for translating isolated sentences, as well as entire theories, from first-order logic into map calculus are designed, or in some cases simply brought nearer through the exercise of specifying properties of a few familiar structures (natural numbers, nested lists, finite sets, lattices). It is also highlighted to what extent a state-of-the-art theorem-prover for first-order logic, namely Otter, can be exploited not only to emulate, but also to reason about, map calculus. Issues regarding ``safe'' forms of map reasoning are singled out, in sight of possible generalizations to the database area.

We propose a method which integrates program modification to the refinement calculus style of program development. Given a program developed through stepwise refinement of a specification, we propose an approach to specify modifications and to derive a new program from the existing refinement steps. This approach is based on the refinement lattice operator meet. A modification to a specification is represented by taking the meet of the old specification and the new feature to add. A solution to the new specification is constructed by coercing the new feature to match the structure of the existing refinement steps. The method fosters reuse of refinement steps and their proofs. We also show that program construction is streamlined by using coercion.

The representation theorem for fork algebras was always misunderstood regarding its applications in program construction. Its application was always described as ``the portability of properties of the problem domain into the abstract calculus of fork algebras''. In this paper we show that the results provided by the representation theorem are by far more important. We show that not only the heuristic power coming from concrete binary relations is captured inside the abstract calculus, but also design strategies for program development can be successfully expressed. This result makes fork algebras a programming calculus by far more powerful than it was previously thought.

This paper presents a set of rules for the transformation of GHC (Guarded Horn Clauses) programs based on unfolding. The proposed set of rules, called UR-set, is shown to preserve freedom from deadlock and to preserve the set of solutions to be derived. UR-set is expected to give a basis for various program transformations, especially partial evaluation of GHC programs.

Symmetric quotients, introduced in the context of heterogeneous relation algebras, have proven useful for applications comprising for example program semantics and databases. Recently, the increased interest in fuzzy relations has fostered a lot of work concerning relation-like structures with weaker axiomatisations. In this paper, we study symmetric quotients in such settings and provide many new proofs for properties previously only shown in the strong theory of heterogeneous relation algebras. Thus we hope to make both the weaker axiomatisations and the many applications of symmetric quotients more accessible to people working on problems in some specific part of the wide spectrum of relation categories.

In this paper we present an algebraic construction of the category of monotonic predicate transformaers from the category of relations which is similar to the standard algebraic construction of the integers from the natural numbers. The same construction yields the category of relations from the category of total functions. This provides a mechanism through which the rich type structure of the category of total functions can be promoted to successively weaker ones in the categories of relations and predicate transformers. In addition, it has exposed two complete rules for the refinement and composition of specifications in Morgan's refinement calculus.

We present a dynamic modelization of a database when submitted to a sequence of queries and updates, that allows us to study the evolution of the sizes of relations. While the problem of estimating the sizes of derived relations at a given time (``static'' case) has been the subject of several studies, to the best of our knowledge the evolution of the relation sizes under queries and updates (``dynamic'' cases) has not been studied so far. We consider the size of a relation as a random variable, and we study its probability distribution when the database is submitted to a sequence of insertions, deletions and queries. We show that it behaves asymptotically as a Gaussian process, whose expectation and covariance are proportional to the time. This approach also allows us to analyze the maximum of the size of the derived relation.

This is not the first book on rough set analysis and certainly not the first book on knowledge discovery algorithms, but it is the first attempt to do this in a non-invasive way. The term "non-invasive" in connection with knowledge discovery or data analysis is new and needs some introductory remarks. We have worked from about 1993 on topics of knowledge discovery and/or data analysis (both topics are sometimes hard to distinguish), and we felt that most of the common work on this topics was based on at least discussable assumptions. We regarded the invention of Rough Set Data Analysis (RSDA) as one of the big events in those days, because, at the start, RSDA was clearly structured, simple, and straightforward from basic principles to effective data analysis. It is our conviction that a model builder who uses a structural and/or statistical system should be clear about the basic assumptions of the model. Furthermore, it seems to be a wise strategy to use models with only a few (pre-)assumptions about the data. If both characteristics are fulfilled, we call a modelling process non-invasive. This idea is not really new, because the non-parametric statistics approach based on the motto of R.A. Fisher ``Let the data speak for themselves'' can be transferred to the context of knowledge discovery. It is no wonder that e.g. the randomisation procedure (one of the flagships of non-parametric statistics) is part of the non-invasive knowledge discovery approach. In this book we present an overview of the work we have done in the past seven years on the foundations and details of data analysis. During this time, we have learned to look at data analysis from many different angles, and we have tried not to be biased for — or against — any particular method, although our ideas take a prominent part of this book. In addition, we have included many citations of papers on RSDA in knowledge discovery by other research groups as well to somewhat alleviate the emphasis on our own work. We hope that the presentation is neither too rough nor too fuzzy, so that the reader can discover some knowledge in this book

The syntax of a formal language is effectively given. This is not immediately so for the semantics. This paper deals with the simple but sufficiently powerful applicative language (&lgr;-calculus) and studies effectiveness properties of its semantics. In particular it analyses the effectiveness of the interpretation of &lgr;-terms as well as different notions of computability over models.

Recently, J.Y. Girard discoverd that usual logic connectors such as zimp (implication) could be broken up into more elementary linear connectors. This provided a new linear logic [Girard86] where hypothesis are (in some sense) used once and only once. The most surprising is that all the power of the usual logic can be recovered by means of recursive logical operators (connector ``of course''). There are two versions of the linear logic: the intuitionistic one and the classical one. It seems that the second provides a appropriate formalism for parallelism and communication. This approach is entirely new and requires further development. Here we restrict out attention to the intuitionistic version and to the consequences os the linear constraint to the computation process. medskip We give two equivalent presentations of the (propositional part of) linear logic: a sequent calculus and a (categorical) combinator system. Then we introduce inductive and projective connectors, in particular the connector ! (read ``of course''). It plays a fundamental role in the encoding of usual intuitionistic logic into linear logic. There is a cut elimination theorem for the sequent calculus that corresponds to an evaluation mechanism for the combinator system. We present a very simple (abstract) machine that performs linear computations with the following features: begin itemize item A very natural lazy evaluation mechanism. item No need of garbage collector. end itemize Finally, we discuss the relevance of linear logic to implement functional languages.

In the context of the executable specification language OBJ3, an order-sorted completion procedure is implemented, providing automatically convergent specifications from user-given ones. This feature is of first importance to insure unambiguity and termination of the rewriting execution process. We describe here how we specified a modular completion design in terms of inference rules and control language, using OBJ3 itself. On another hand, the specific problems encountered to integrate a completion process in an already reduction-oriented environment are pointed out.

We represent concurrent processes as Boolean propositions or gates, cast in the role of acceptors of concurrent behavior. This properly extends other mainstream representations of concurrent behavior such as event structures, yet is defined more simply. It admits an intrinsic notion of duality that permits processes to be viewed as either schedules or automata. Its algebraic structure is essentially that of linear logic, with its morphisms being consequence-preserving renamings of propositions, and with its operations forming the core of a natural concurrent programming language.

A Chu space is a binary relation between two sets. In this thesis we show that Chu spaces form a non-interleaving model of concurrency which extends event structures while endowing them with an algebraic structure whose natural logic is linear logic. We provide several equivalent definitions of Chu spaces, including two pictorial representations. Chu spaces represent processes as automata or schedules, and Chu duality gives a simple way of converting between schedules and automata. We show that Chu spaces can represent various concurrency concepts like conflict, temporal precedence and internal and external choice, and they distinguish between causing and enabling events. We present a process algebra for Chu spaces including the standard combinators like parallel composition, sequential composition, choice, interaction, restriction, and show that the various operational identities between these hold for Chu spaces. The solution of recursive domain equations is possible for most of these operations, giving us an expressive specification and programming language. We define a history preserving equivalence between Chu spaces, and show that it preserves the causal structure of a process.

The calculus of relations turned into an important conceptual and methodological tool in computer science. The methods presented in this book include questions of relational databases, applications to program specification, resource-conscious linear logic, semantic and refinement consideration, nonclassical logics for reasoning about programs, tabular methods in software construction, algorithm development, linguistic problems, followed by a comprehensive bibliography. The reader gets an overview of the wide-ranging applicability of relational methods in computer science. ``... While this is a multi-authored volume, the authors have done an excellent job of making it read like a single-authored work ... The book can be viewed as a set of snapshots of a family of research and researchers at one point in time. If you are interested in relational problems, I can think of no better introduction ...'' — Computing Reviews

Much of the earlier development of abstract interpretation, and its application to imparative programming languages, has concerned techniques for finding fixed points in large (often infinite) lattices. The standard approach in the abstract interpretation of functional languages has been to work with small, finite lattices and this supposedly circumvents the need for such techniques. However, practical experience has shown that, in the presence of higher order functions, the lattices soon become too large (although still finite) for the fixed-point finding problem to be tractable. This paper develops some approximation techniques which were first proposed by Hunt and shows how these techniques relate to the earlier use of widening and narrowing operations by the Cousots.

Recursivity is well known to be a crucial and important concept in programming theory. The simplest scheme of recursion in the context of logic programming is the binary Horn clause P(l₁,...,l_n) gets P(r₁,...,r_n) . The decidability of the satisfiability problem of programs consisting of such a rule, a fact and a goal – called smallest binary program – has been a goal of research for some time. In this paper the undecidability of the smallest binary program is shown by a simple reduction of the Post Correspondence Problem.

In computer science, one is interested mainly in finite objects. Insofar as infinite objects are of interest, they must be computable, i.e., recursive, thus admitting an effective finite representation. This leads to the notion of a recursive graph, or, more generally, a recursive structure or data base. In this paper we summarize our recent work on recursive structures and data bases, including (i) the high undecidability of many problems on recursive graphs, (ii) somewhat surprising ways of deducing results on the classification of NP optimization problems from results on the degree of undecidability of their infinitary analogues, and (ii) completeness results for query languages on recursive data bases.

This paper presents a theory of probabilistic programming based on relational calculus through a series of stages; each stage concentrates on a different and smaller class of program, defined by the healthiness conditions of increasing strength. At each stage we show that the notations of the probabilistic language conserve the healthiness conditions of their operands, and that every theory conserves the definition of recursion.

We introduce an implementation of rewriting for type and combinator terms called ATLAS. This system implements the algebraic and term rewriting theory for abstract types and combinators developed in [Meinke-1991,Meinke-1992b]. The system is intended to support the execution of equational specifications of abstract types and combinators. The type checking algorithms of the system also allow it to function as a framework for defining logics and proof checking. We present a short tutorial introduction to ATLAS by means of examples taken from first and higher order algebraic specifications and logics.

Usually, modal correspondences are investigated between monomodal and classical predicate logic formulas (van Benthem[76]). We want to propose a more algebraic view, concentrating on correspondences between general multimodal formulas (seen in the context of modal algebras), and relation algebraic formulas (which may be classified as restricted predicate logic formulas). Correspondences will be obtained quite systematically by means of relation algebraic principles of extensionality. For first order expressible correspondences, these will provide for the quantifier elimination, as well as they give the translation of all modal expressible relation algebraic primitives. This leads to a simple method of translation of certain relation algebraic formulas into their multimodal counterparts, which then have to be proved equivalent to the usual monomodal correspondences. Further, we discuss how (by the use of binary operators) the modal operator principle could be extended to capture the entire relation algebra by means of modal correspondences.

The family of terminological representation systems has its roots in the representation system KL-ONE. Since the development of this system more than a dozen similar representation systems have been developed by various research groups. These systems vary along a number of dimensions. In this paper, we present the results of an empirical analysis of six such systems. Surprisingly, the systems turned out to be quite diverse leading to problems when transporting knowledge bases from one system to another. Additionally, the runtime performance between different systems and knowledge bases varied more than we expected. Finally, our empirical runtime performance results give an idea of what runtime performance to expect from such representation systems. These findings complement previously reported analytical results about the computational complexity of reasoning in such systems.

Versions of constraint rewriting for completion of rewrite systems in the presence of associative commutative operators with identities have been proposed, in which constraints are used to limit the applicability of rewrite rules. We extend these approaches such that the initially given equations can contain constraints, and such that a suitable version of unification modulo associativity, commutativity and identity can be interleaved with the process of completion.

A mathematical model for communicating sequential processes is given, and a number of its interesting and useful properties are stated. The possibilities of non-determinism are fully taken into account.

A complete set of algebraic laws is given for Dijkstra's nondeterministic sequential programming language. Iteration and recursion are explained in terms of Scott's domain theory as fixed points of continuous functionals. A calculus analogous to weakest preconditions is suggested as an aid to deriving programs from their specifications.

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of familiar programming exercises.

A compiler is specified by a description of how each construct of the soure language is translated into a sequence of object code instructions. The meaning of the onject code can be defined by an interpreter written in the source language itself. A proof that the compiler is correct must show that interpretation of the object code is at least as good (for any relevant purpose) as the corresponding source program. The proof is conducted using standard techniques of data refinement. All the calculations are based on algebraic laws governing the source language. The theorems are expressed in a form close to a logic program, which may be used as a compiler prototype, or as a check on the results of a particular compilation. It is suggested that this formal framework provides appropriate interfaces for compiler implementors, and hardware designers, as well as users of the language.

This paper shows that the nice properties of logic programs extend to definite clause specifications over arbitrary constraint languages. The notion of a constraint language sees a constraint as a piece of syntax with unknown internal structure that constrains the values variables can take in interpretations. Examples of constraint languages are Predicate Logic and its sublanguages as well as attributive concept description languages developed for knowledge representation. Our framework generalizes the constraint logic programming scheme of Jaffar and Lassez to make it applicable to knowledge representation: the constraint language is not required to be a sublanguage of predicate logic and may come with more than one interpretation, and the interpretations of the constraint language are not required to be solution compact. We present a semantic type discipline for our generalized definite clause specifications and establish a notion of well-typedness that is decidable provided the underlying constraint language is decidable. Finally, we give a type inference rule for computing most general well-typed weakenings of specifications.

In this paper we demonstrate that the basic rules and calculational techniques used in two extensively documented program derivation methods can be expressed, and, indeed, can be generalised within a relational theory of datatypes. The two methods to which we refer are the so-called ``Bird-Meertens formalism'' (see [22]) and the ``Dijkstra-Feijen calculus'' (see [15]). The current paper forms an abridged, though representative, version of a complete account of the algebraic properties of the Boom hierarchy of types [19,18]. Missing is an account of extensionality and the so-called cross-product.

A collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: ``What are the possible values to which an expression might evaluate during program execution?'' Answering such questions in a denotational framework is akin to traditional data flow analysis and, when used in the context of abstract interpretation, allows one to infer properties that approximate the run-time behaviour of expression evaluation. Exact collection interpretations of expressions are developed for three abstract functional languages: a strict first-order language, a nonstrict first-order language, and a nonstrict higher order language ( the full untyped lambda calculus with constants). It is argued that the method is simple (in particular, no powerdomains are needed), natural (it captures the intuitive operational behaviour of a cache), yet more expressive than existing methods (it is the first exact collecting interpretation for either nonstrict or higher order languages). Correctness of the interpretations with respect to the standard semantics is shown via a generalization of the notion of strictness. It is further shown how to form abstractionsof these exact interpretations, using as an example a collecting strictness analysis which yields compile-time information not previously captured by conventional strictness analyses.

A representation changer is a function that converts a concrete representation of an abstract value into a different concrete representation of that value. Many useful functions can be recognised as representation changers; examples include compilers, and arithmetic functions such as addition and multiplication. Functions that can be specified as the right inverse of other functions are special cases of representation changers. In recent years, a number of authors have used a relational calculus to derive representation changers from their specifications. In this paper we show that the generality of relations is not essential, and representation changers can be derived within the more basic setting of functional programming. We illustrate our point by deriving a carry-save adder and a base-converter, two functions which have previously been derived relationally.

This paper presents the Centaur system through a tutorial describing the creation of an environment for a small language of mathematical expressions called Exp. With Centaur, the user may interactively generate programming language environments, including structured editors, debuggers, interpreters, and other tools. In this tutorial, all phases of language specification are covered: the design of the abstract and concrete syntax of Exp in Metal and Sdf, the pretty printing rules in Ppml, and the semantics of an Exp interpreter in Typol. The tools generated by Centaur based on these specifications are enhanced by a user interface built with Centaur graphic primitives.

The object of study of this paper is the categorical semantics of three impredicative type theories, viz. Higher Order &lgr;-calculus F&ohgr;, the Calculus of Constructions and Higher Order ML. The latter is particularly interesting because it is a two-level type theory with type dependency at both levels. Having described appropriate categorical structures for these calculi, we establish translations back and forth between all of them. Most of the research in the paper concerns the theory of fibrations and comprehension categories.

A comprehension category is defined as a functor cal P:E tfun B ^tfun satisfying (a) cod ø cal P is a fibration, and (b) f is cartesian in E implies that cal P f is a pullback in B. This notion captures many structures which are used to describe type dependency (like display-map categories (Taylor (1986), Hyland and Pitts (1989) and Lamarche (1988)), categories with attributes (Cartmell (1978) and Moggi (1991)), D-categories (Ehrhard (1988)) and comprehensive fibrations (Pavlovic (1990))). It also captures comprehension as occurring in topos theory and as described by Lawvere's (1970) hyperdoctrines. This paper is meant as an introduction to these comprehension categories. A comprehension category will be called closed if it has appropriate dependent products and sums. A few examples of closed comprehension categorieswill be described here; more of them may be found in Jacobs (1991); applications occur in Jacobs (1991) and Jacobs et al. (1991).

The calculus of relations turned into an important conceptual and methodological tool in computer science. The methods presented in this book include questions of relational databases, applications to program specification, resource-conscious linear logic, semantic and refinement consideration, nonclassical logics for reasoning about programs, tabular methods in software construction, algorithm development, linguistic problems, followed by a comprehensive bibliography. The reader gets an overview of the wide-ranging applicability of relational methods in computer science. ``... While this is a multi-authored volume, the authors have done an excellent job of making it read like a single-authored work ... The book can be viewed as a set of snapshots of a family of research and researchers at one point in time. If you are interested in relational problems, I can think of no better introduction ...'' — Computing Reviews

The calculus of relations turned into an important conceptual and methodological tool in computer science. The methods presented in this book include questions of relational databases, applications to program specification, resource-conscious linear logic, semantic and refinement consideration, nonclassical logics for reasoning about programs, tabular methods in software construction, algorithm development, linguistic problems, followed by a comprehensive bibliography. The reader gets an overview of the wide-ranging applicability of relational methods in computer science. ``... While this is a multi-authored volume, the authors have done an excellent job of making it read like a single-authored work ... The book can be viewed as a set of snapshots of a family of research and researchers at one point in time. If you are interested in relational problems, I can think of no better introduction ...'' — Computing Reviews

The calculus of relations turned into an important conceptual and methodological tool in computer science. The methods presented in this book include questions of relational databases, applications to program specification, resource-conscious linear logic, semantic and refinement consideration, nonclassical logics for reasoning about programs, tabular methods in software construction, algorithm development, linguistic problems, followed by a comprehensive bibliography. The reader gets an overview of the wide-ranging applicability of relational methods in computer science. ``... While this is a multi-authored volume, the authors have done an excellent job of making it read like a single-authored work ... The book can be viewed as a set of snapshots of a family of research and researchers at one point in time. If you are interested in relational problems, I can think of no better introduction ...'' — Computing Reviews

A language of relations and combining forms is presented in which to describe both the behaviour of circuits and the specifications which they must meet. We illustrate a design method that starts by selecting representations for the values on which a circuit operates, and derive the circuit from these representations by a process of refinement entirely within the language.

Butterfly networks arise in many signal processing circuits and in parallel algorithms for many sorts of message-passing computers. This paper attempts to explain why this should be, and what butterfly networks are, using a new and elegant formulation based on a language of relations. Most of the material covered by this paper has appeared in a less tractable form in earlier papers [7,8]. The novelty here is in the simplicity and elegance of presentation, which derives from an appropriate choice of high-level structures. These structures are represented by functions which are used to compose circuits from components, and are chosen to have simple mathematical properties. This presentation makes it easier to explain how the design comes about, showing that butterflies are natural implementations of divide-and-conquer algorithms.

This report presents a simple framework for performing calculations with the elements of (finite) lattices. A particular feature of this work is the use of type classes to enable the use of overloaded function sysmbols within a strongly typed language. Previous applications of type classes have been in areas that are of most interest to language implementors. This report suggests that type classes might also be useful as a general tool in the development of clear and modular programs.

In a language with a polymorphic type system, a term of type all t.f(t) can be treated (possibly after suitable instantiation) as having any of the types in the set: $ { f(a) | a is a type }. A natural extension of such systems supports a more restricted form of polymorphism in which, rather than simply taking on all possible values, the type a is constrained to satisfy a specified predicate &pgr;(a)$.

In a language with a polymorphic type system, a term of type all t.f(t) can be treated (possibly after suitable instantiation) as having any of the types in the set: $ { f(t) | t is a type }. It is natural to consider a more restricted form of polymorphism in which the value taken by t may be constrained to a particular subset of types. In this situation we write all t.&pgr;(t) Rightarrow f(t), where &pgr;(t) is a predicate of types, for the type of an object which can be treated (after suitable instantiation) as having any of the types in the set: { f(t) | t is a type such that &pgr;(t) holds }. A term with a restricted polymorphic type of this kind is often said to be overloaded, having different interpretations for different argument types. This paper presents a general theory of overloading based on the use of qualified types, which are types of the form &pgr; Rightarrow &sgr; denoting those instances of type &sgr; which satisfy the predicat &pgr;$. The main benefits of using qualified types are: begin itemize item A general approach which includes a range of familiar type systems as special cases. Results and tools developed for the general system are immediately applicable to each particular application. item A precise treatment of the relationship between implicit and explicit overloading. This is particularly useful for describing the implementation of systems supporting qualified types. item The ability to include local constraints as part of the type of an object. This enables the definition and use of polymorphic overloaded values within a program.

Structured methods are widely used in systems analysis and design for commercial data processing applications. One of the most important features of these methods is the use of entity-relationship diagrams as a data medelling technique. This paper contributes to the understanding of such methods by taking a typical one, LBMS systems Engineering, and providing a systematic translation of its diagrams into Z. We also demonstrate how the expressiveness and precision of structured methods can be enhanced by specifying in Z further constraints on the data model and the effect of transactions on the system state. In structured methods, the former is usually done by informal comments and the latte by pseudo-code, if at all. This work also has important consequences as far as the widespread adaption of formal methods is concerned. It provides a style of writing Z specifications that could easily be adopted by someone already familiar with entity-relationship modelling, and does so in a way that standardizes the use of schemas as much as possible.

HOPS and RALF are two interactive symbol manipulation systems — one for functional programming and program transformation, the other for proving relation algebraic formulae — that both implement interactive application of second-order rewriting rules, HOPS on term graphs and RALF on conventional terms and formulae. Both systems support a larger class of second-order rewriting rules than commonly found in other systems. In this paper we provide a homogeneous underpinning to second-order syntax and rewriting for easing the transition from terms to term graphs and vice versa, so that aspects that are easier to understand in one view also further understanding in the other view, altogether making a case for bringing second-order syntax more directly to the user interface than usual in most systems today.

During the last few years, relational methods have been gaining more and more acceptance and impact in computer science. Besides applications of concrete relations, also non-standard models of the relation algebraic axioms are important in fields as far apart as artificial intelligence and distributed computing. Also weaker structures have been considered, such as Dedekind categories in connection with fuzzy reasoning, and different kinds of allegories. indent In this report we present a library of Haskell modules that allows to explore relation algebras and several weaker structures by providing different means to construct and test such algebras. indent The kernel of our library is strictly conformant to the Haskell 98 standard, and can therefore be expected to be usable on future Haskell systems, too. For ease of use, we additionally provide a more elegant interface using non-standard extensions.

Modern functional languages all support higher-order functions. Nevertheless actual applications are mostly written in an applicative style. We show how working with a language based on slightly shifted concepts and embedded into a powerful environment can bring about change.

With the aim of extending algebraic term graph rewriting to the expressiveness of Combinatory Reduction Systems, we first introduce a novel definition of term graphs with primitive notions of variable binding and variable identity, and with metavariables with successors. hbox After discussing identification and sharing in these graphs, we introduce intervals and segments to serve as images of metavariables, including those with successors. Building on this we are able to establish a hierarchy of structure-preserving mappings between our term graphs, including at its top a concept of homomorphism avoiding ``capture of variables'' and catering for multiple instances of metavariables. The individual categories this gives rise to have different uses, namely in term graph rewriting, and the appendix provides an overview over a novel approach to algebraic term graph rewriting (fully presented in [Kahl, 1996]) together with the two crucial proofs concerning the viability of the constructions involved.

This thesis presents a first algebraic approach to term graph rewriting encompassing the treatment of bound variables. Building on a novel definition of term graphs with primitive notions of variable binding and variable identity, we present a concept of homomorphism avoiding ``capture of variables'' and catering for multiple instances of metavariables. Rewriting of these term graphs within the algebraic approach requires a new extension that is interesting in itself, the fibered approach to rewriting. As one result we obtain the first algebraic characterisation of graph reduction. Summing up, we have extended the algebraic approach to term graph rewriting, that so far only covered conventional term rewriting systems, to the expressive power of combinatory reduction systems and even slightly more general second-order rewriting systems. Thus we lay a theoretical foundation for implementations of functional programming languages, program transformation systems and other symbolic computation systems.

Relational formalisations can be very concise and precise and can allow short, calculational proofs under certain circumstances. [...] In situations corresponding to the simultaneous use of many variables in predicate logic, however, either a style using predicate logic with point variables has to be adopted or impractical and clumsy manipulations of tuples have to be employed inside relation calculus. In the application of relational formalisation to term graphs with bound variables [...] we have been forced to employ both methods extensively, and, independently of other approaches, have been driven to develop a graphical calculus for making complex relation algebraic proofs more accessible. It turns out that, although our approach shares many common points with those presented in the literature [...], it still is more general and more flexible than those approaches since we draw heavily on additional background in algebraic graph rewriting

We present a new approach to rewriting obtained by enhancing and unifying existing variants inside the algebraic (or better categorical) approach to (graph) rewriting. Our approach is motivated by second-order term graph rewriting and stresses on one hand the two-step nature of rule application consisting of deleting and adding items and on the other hand the heterogeneous nature of the rewriting setup where rule steps should be clearly distinguished from matching of rule sides into redexes. Complementing the existing opfibration approach with a dual fibration step turns out to yield a natural and flexible approach with useful new applications. The resulting fibred approach takes advantage of the heterogeneous setting and appropriately reflects the duality between deleting and adding in the course of rewriting, in contrast with the double-pushout approach which simplifies this duality into a symmetry. An important contribution is the universal characterisation of the host object, which has to be found as a pushout-complement in the double pushout approach. The fibred approach is presented in abstract and independent from any concrete application categories in the manner of High-Level Replacement Systems. Our original motivation for the development of the fibred approach comes from term graphs with bound variables where all other approaches failed; in this paper we present an unusual view on term rewriting as running example.

We present a typing concept for second-order term graphs that does not consider the types as an external add-on, but as an integral part of the term graph structure. This allows a homogeneous treatment of term-graph representations of many kinds of typing systems, including second-order &lgr;-calculi and systems of dependent types. Applications can be found in interactive systems and as typed intermediate representation for example in compilers.

We show how and why it makes sense to use a relational formalisation instead of the usual functional one in the treatment of term graphs. Special attention is paid to term graphs with bound variables, that have, to our knowledge, never been formalised with such a generality before. Besides the novel treatment of term graphs themselves, we present an innovative relational homomorphism concept that for the first time allows to consider terms, resp. null term trees as a special case of term graphs and still have the full power of (second-order) substitution available.

Galleys have been introduced by Jeff Kingston as one of the key concepts underlying his advanced document formatting system Lout. Although Lout is built on a lazy functional programming language, galley concepts are implemented as part of that language and defined only informally. In this paper we present a first formalisation of document formatting combinators using galley concepts in the purely functional programming language Haskell.

In many cases, linear notation systems can be seen to encode underlying, implicit graphs. This paper focusses on the way that making these graphs explicit is useful for human understanding, and on the use of computers to make handling of notations based on explicit graphs feasible, efficient and productive.

In this paper we extend an earlier approach to graphical relation calculi towards relational matching, thus allowing proofs with fewer auxiliary steps and concentrating more on the essential proof ideas. For facilitating the formal argument we introduce hierarchical relational diagrams as an intermediate structure and employ more of the algebraic graph rewriting repertoire for defining relational rewriting of these hierarchical diagrams.

[...] The bf Higher bf Object bf Programming bf System HOPS, which has been developed by a group led by Gunther Schmidt since the mid-eighties [...] is a graphically interactive term graph programming system designed for transformational program development. In HOPS, only syntactically correct and well-typed programs can be constructed. The choice of the language is only constrained by certain restrictions of the term graph formalism and of the typing system. [...] The design of this system relies on recent advances in the theories of untyped and typed second-order term graphs.

We propose stratified term graphs as enrichment of conventional term graph structures with synchronisation borders that intuitively capture constraints such as that values along these borders should be available simultaneously in distributed implementations. This additional structure requires a weakening of the algebraic characterisation, and we propose coherent unsharp ps-semigroup categories as generalisation of gs-monoidal categories. These capture exactly the essence of stratified term graphs with at least one root.

Investigating the interplay between demonic operators and direct products in abstract relation algebras against the background of gs-monoidal categories, we discover that the direct product gives rise to a gs-monoidal category with demonic composition, while a new concept of demonic product gives rise to a structure that fails to be gs-monoidal mostly through the lack of functoriality of the demonic product. However, this lack is interesting on its own account, since it is an example of what has been studied as unsharpness in the context of direct products in relation algebras, and there it can only occur if not all products exist. We show how an intuitive understanding of our demonic products coincides with the intuition behind the unsharpness research, and, generalising the approach of using term graphs as syntax for gs-monoidal categories, discuss the generalisation of stratified term graphs to be used for the unsharp variant.

The type-free &lgr;-calculus is powerful enough to contain all the polymorphic and higher-order nature of functional programming and furthermore types could be constructed inside it. However, mixing the type-free &lgr;-calculus with logic is not very straightforward (see Aczel [1] and Scott [15]). In this paper, a system that combines polymorphism and higher-order functions with logic is presented. The system is suitable for both the functional and logical paradigms of programming as from the functional paradigm's point of view, the system enables one to have all the polymorphism and higher order that exist in functional languages and much more. In fact even the fixed point operator Y which is defined as &lgr; f. (&lgr; x.f(x x))(&lgr; x.f(x x)) can be type checked to ((&agr; tfun &agr;) tfun &agr;) where &agr; is a variable type. (&lgr; x. x x)(&lgr; x. x x) can be type-checked too, something not allowed in functional languages. From the point of view of theorem proving, the system is expressive enough to allow self-referential sentences and those sentences that lead to Russel's and Curry's paradoxes. However, the paradoxes do not hold due to the notion of circular types which contain the type of propositions. In fact both sentences &lgr; x. lnot x x and &lgr; x.x x tfun bottom are ill-typed according to the system, because their resulting types are circular. Hence the application of either sentence to itself will not result in a proposition. The system is implementes in Milner's ML and can be seen as extending ML in two important ways. First, it extends the part related to the functional paradigm in taht it can type terms that could not be typed in ML, namely the terms that contain self-application such as the Y term above. Second, our system extends ML by adding logic to it in a consistent way.

The problem of program synthesis is considered. begin itemize item [1.] A computational semantics is introduced for relational knowledge bases. Our semantics naturally arises from practical experience of databases and knowledge bases. item [2.] It is stated that the corresponding logic coincides exactly with the intuitionistic one. item [3.] Our methods of proof of the general theorems turn out to be very useful for designing new efficient algorithms.In particular, one can construct a program synthesizer that runs in linear space.As a corollary, we can explain why there exist programs that solve PSPACE-complete problems ``in a reasonable time'' despite of their theoretical exponential uniform lower bound. end itemize

In this paper we present a basic notion of relational structures which includes simple graphs, labelled graphs and hypergraphs, and introduce a notion of partial morphisms between them. An existence theorem of pushouts in the category of relational structures and their partial morphisms is proved under a certain functorial condition, and it enables us to discuss single pushout rewritings of relational structures.

This paper provides a notion of Zadeh categories as a categorical structure formed by fuzzy relations with sup-min composition, and proves two representation theorems for Dedekind categories (relation categories) with a unit object analogous to one-point set, and for Zadeh categories without unit objects.

An existence theorem of pushout-complements is given in an elementary topos by using category theory of binary relations, called relational calculus, and it is also shown more explicitly in the category of directed graphs, which is a typical example of toposes, as an application. Moreover an embedding theorem and Church-Rosser theorem on grammars (derivations) in a topos are proved.

A fixed point semantics for nondeterministic data flow is introduced which refines and extends work of Park (1983). It can be seen also as an extension to the general case of Kahn's (1974) successful fixed point semantics for deterministic data flow. An associativity result for network construction is proved which shows that anomalies such as those of Brock and Ackerman do not arise in this semantics. The semantics is shown to be extensional, in the natural sense that nondeterministic processes which induce identical — output relations in all contexts are equal.

We model processes by means of a mathematical entity that we call a relational process. This model describes a process as an open system from which the description of the process as a closed system can be easily obtained. Also, it represents not only the actions of the process but also the resources needed to accomplish its behaviour. Using this model, we first define two operators. Each of these represents an extreme perception of concurrency. One, the interleaved parallel composition operator, reduces concurrency to interleaving and the other, the maximal totally synchronous parallel composition operator, reduces concurrency to a totally synchronous behaviour. Second, by combining these operators, we define the maximal true-concurrency composition operator, which is an operator expressing true concurrency. When many processes interfere on the same resource in order to modify it, each in its way, the two maximal operators express this situation by letting the final value of the variable modelling this resource be indeterminate. So, they allow the detection of interferences between processes. We present some of the properties of these operators.

The reader is introduced to Morgan's Refinement Calculus notation, by means of a simple case study. This example is taken all the way from an abstract specification down to a program in Dijkstra's language of guarded commands, using the laws of the refinement calculus to justify each step. This program is then transliterated into Pascal