In this article, we indicate how the category theoretical approach to tree automata, due to Betti and Kasangian, can be fruitfully combined with Walters’ categorical approach to context-free grammars to provide a simple way of establishing the well-known correspondence between context-free languages and the behaviors of non-deterministic tree automata. The connecting link between the two notions is provided by the theory of relational presheaves.

Within a categorical framework for primitive recursion, equality between p.r. maps is shown to be definable by suitable p.r. equality predicates. Equivalence is shown between a direct categorical formalization of classical p.r. functions and p.r. maps in the sense of Lawvere and Freyd. An extension of the theory is shown to admit a ‘universal set’ containing all objects of the extended theory of subobjects.

We add extensional equalities for the functional and product types to the typed λ-calculus with, in addition to products and terminal object, sums and bounded recursion (a version of recursion that does not allow recursive calls of infinite length). We provide a confluent and strongly normalizing (thus decidable) rewriting system for the calculus that stays confluent when allowing unbounded recursion. To do this, we turn the extensional equalities into expansion rules, and not into contractions as is done traditionally. We first prove the calculus to be weakly confluent, which is a more complex and interesting task than for the usual λ-calculus. Then we provide an effective mechanism to simulate expansions without expansion rules, so that the strong normalization of the calculus can be derived from that of the underlying, traditional, non-extensional system. These results give us the confluence of the full calculus, but we also show how to deduce confluence directly form our simulation technique without using the weak confluence property.

This paper surveys several different variants of order sorted algebra (abbreviated OSA), comparing some of the main approaches (overloaded OSA, universe OSA, unified algebra, term declaration algebra, etc.), emphasising motivation and intuitions, and pointing out features that distinguish the original ‘overloaded’ OSA approach from some later developments. These features include sort constraints and retracts; the latter is particularly useful for handling multiple data representations (including automatic coercions among them). Many examples are given, for most of which, runs are shown on the OBJ3 system.

This paper also significantly generalises overloaded OSA by dropping the regularity and monotonicity assumptions, and by adding signatures of non-monotonicities, which support simple semantics for some aspects of object oriented programming. A number of new results for this generalisation are proved, including initiality, variety, and quasi-variety theorems. Axiomatisability results à la Birkhoff are also proved for unified algebras.