Having started life as a way of reconstructing a topological space from a pair of complementary subspaces, the glueing construction has found employment in a wide range of different roles, from the construction of free distributive lattices to a supporting part in the 2-categorical analysis of types theories. In this latter role the construction appears to be a fundamental factor in the behaviour of higher order proof theory. What is going on here? Before that can be answered we need at least a less ad hoc description of the construction. In this paper I set down what is, I believe, the beginnings of a coherent account of the algebraic version of glueing. As well as the abstract theory, I give a good selection of different examples to illustrate the diverse nature of the uses of the construction.

The notion of a dynamic labeled 2-structure(dℓ2s) is introduced and investigated. It generalizes the notion of a labeled 2-structure (ℓ2s) (Ehrenfeucht and Rozenberg 1990), by making it possible to change the (label) relationships between the nodes. This is achieved by storing in the nodes of a ℓ2s output and input functions that can change the outgoing and incoming labels, respectively. The notion of a clan, which is central in the theory of ℓ2s's is transferred to the framework of dℓ2s's, and the basic properties of clans of dℓ2s's are investigated.

We introduce a new class of higher order rewriting systems, called Interaction Systems (IS's). IS's are derived from Lafont's (Intuitionistic) Interaction Nets (Lafont 1990) by dropping the linearity constraint. In particular, we borrow from Interaction Nets the syntactical bipartitions of operators into constructors and destructors and the principle of binary interaction. As a consequence, IS's are a subclass of Klop's Combinatory Reduction Systems (Klop 1980), where the Curry-Howard analogy still ‘makes sense’. Destructors and constructors, respectively, correspond to left and right logical introduction rules: interaction is cut and reduction is cut-elimination.

Interaction Systems have been primarily motivated by the necessity of extending the practice of optimal evaluators for λ-calculus (Lamping 1990; Gonthier et al. 1992a) to other computational constructs such as conditionals and recursion. In this paper we focus on the theoretical aspects of optimal reductions. In particular, we generalize the family relation in Lévy (1978; 1980), thus defining the amount of sharing an optimal evaluator is required to perform. We reinforce our notion of family by approaching it in two different ways (generalizing labelling and extraction in Levy (1980)) and proving their coincidence. The reader is referred to Asperti and Laneve (1993c) for the paradigmatic description of optimal evaluators of IS's.

The shuffle product of two words u and v, denoted u‖v, is the set of all words of the form x1y1x2y2…xnyn for some n and for some (possible empty) words x1, …xn, y1, …yn, such that u = x1x2…xn, and v = y1y2…yn. In other words, u‖v is the set of all possible words that can be obtained by merging u and v so that the letters of u and v separately maintain their original orders but are allowed to alternate arbitrarily. The shuffle product of languages L and M, denoted L‖M, is the union of all u‖v for u ∈ L and v ∈ M.