Bilattices were introduced and applied by Ginsberg and Fitting for a diversity of applications, such as truth maintenance systems, default inferences and logic programming. In this paper we investigate the structure and properties of a particularly important class of bilattices called interlaced bilattices, which were introduced by Fitting. The main results are that every interlaced bilattice is isomorphic to the Ginsberg-Fitting product of two bounded lattices and that the variety of interlaced bilattices is equivalent to the variety of bounded lattices with two distinguishable distributive elements, which are complements of each other. This implies that interlaced bilattices can be characterized using a finite set of equations. Our results generalize to interlaced bilattices some results of Ginsberg, Fitting and Jónsson for distributive bilattices.

We show that for every term graph in a left-linear but non-orthogonal term graph rewrite system, one can construct an event structure that represents all the possible reductions that can occur in reduction sequences starting from that term graph. Every finite reduction sequence from that graph corresponds to a configuration of the event structure, and Lévy-equivalent sequences correspond to the same configuration.

Garbage collection is modelled in the event structure by an ‘erases’ relation. The asymmetric conflicts that arise in non-orthogonal rewrite systems are modelled by introducing a ‘prevents’ relation. The configurations of the event structure then form the state space of an event automaton. Taking the directed completion of this space yields a prime algebraic domain.

Non-strict don't care functions, whose foremost representative is the ubiquitous if_then_else, play an essential role in computer science. As far as the semantics is concerned, they can be modelled by their totalizations with the appropriate use of elements representing undefinedness, as D. Scott has shown in his denotational approach. The situation is not so straightforward when we consider non-strict functions in the context of an algebraic framework; this point is discussed in the last section, where we explore the relationship between non-strict don't care and total algebras. The central part of this paper, after presenting the basic properties of the category of non-strict algebras, is an investigation of conditional algebraic specifications. It is shown that non-strict conditional specifications are equivalent to disjunctive specifications, and necessary and sufficient conditions for the existence of initial models are given. Since non-strict don't care specifications generalize both the total and the partial case, it is shown how the results for initiality can be obtained as specializations.

It has recently become evident that categories of representations of Hopf algebras provide fundamental examples of monoidal categories. In this expository paper, we examine such categories as models of (multiplicative) linear logic. By varying the Hopf algebra, it is possible to model several variants of linear logic. We present models of the original commutative logic, the noncommutative logic of Lambek and Abrusci, the braided variant due to the author, and the cyclic logic of Yetter. Hopf algebras provide a unifying framework for the analysis of these variants. While these categories are monoidal closed, they lack sufficient structure to model the involutive negation of classical linear logic. We recall work of Lefschetz and Barr in which vector spaces are endowed with an additional topological structure, called linear topology. The resulting category has a large class of reflexive objects, which form a *-autonomous category, and so model the involutive negation. We show that the monoidal closed structure of the category of representations of a Hopf algebra can be extended to this topological category in a natural and simple manner. The models we obtain have the advantage of being nondegenerate in the sense that the two multiplicative connectives, tensor and par, are not equated. It has been recently shown by Barr that this category of topological vector spaces can be viewed as a subcategory of a certain Chu category. In an Appendix, Barr uses this equivalence to analyze the structure of its tensor product.

It is shown that the category of fuzzy relations with values in a ∗-autonomous poset gives a ∗-autonomous category. It is also shown that this construction can be generalized by replacing the ∗-autonomous poset by a ∗-autonomous category. In both cases, cofree coalgebras exist so that there is a natural! operation.

Using a categorical semantics that has been developed recently as a basis, we study composition and refinement as horizontal and vertical structuring techniques for typed graph transformation systems. Composition of graph transformation systems with respect to common subsystems is shown to be compatible with the semantics, i.e., the semantics of the composed system is obtained as the composition of the semantics of the component systems. Moreover, the structure of a composed graph transformation system is preserved during a refinement step in the sense that compatible refinements of the components induce a refinement of the composition. The concepts and results are illustrated by a sample development of a small information system using entity relationship modelling techniques.

We present two type systems for term graph rewriting: conventional typing and (polymorphic) uniqueness typing. The latter is introduced as a natural extension of simple algebraic and higher-order uniqueness typing. The systems are given in natural deduction style using an inductive syntax of graph denotations with familiar constructs such as let and case.

The conventional system resembles traditional Curry-style typing systems in functional programming languages. Uniqueness typing extends this with reference count information. In both type systems, typing is preserved during evaluation, and types can be determined effectively. Moreover, with respect to a graph rewriting semantics, both type systems turn out to be sound.

We introduce term graph narrowing as an approach for solving equations by transformations on term graphs. Term graph narrowing combines term graph rewriting with first-order term unification. Our main result is that this mechanism is complete for all term rewriting systems over which term graph rewriting is normalizing and confluent. This includes, in particular, all convergent term rewriting systems. Completeness means that for every solution of a given equation, term graph narrowing can find a more general solution. The general motivation for using term graphs instead of terms is to improve efficiency: sharing common subterms saves space and avoids the repetition of computations.