We show that, aside from the semiring equations, three equations and two equation schemes characterize the semiring of regular sets with the Kleene star operation.

We focus attention on a language ℒ generated by a set of elementary actions under operations of sequential composition, external binary choice, iteration, and non-nested disjoint parallel composition: that is, on an especially simple parallel language without explicit internal, or ‘local’, nondeterminism. ℒ is nondeterministic, despite the restriction to external choice, since a given action may occur in both subterms F and G of the parallel composition F ║ G. We exhibit a single set of equations that axiomatizes both step bisimulation and pomset equivalence on ℒ Given that step bisimulation and pomset equivalence are incomparable on the language ℒ+ obtained from ℒ by relaxing just the constraint on choice, the coincidence of these equivalences on ℒ suggests that the elimination of explicit internal choice can result in simplifications at the semantic level. We reinforce this impression by showing for ℒ that step bisimulation (i) coincides with pomset bisimulation equivalence, (ii) is real-time consistent, and (iii) has step trees as concrete representatives of its equivalence classes. Moreover, we show that none of these results holds for the language ℒ+ Finally, step trace equivalence is proved not to coincide with step bisimulation equivalence on ℒ.

We present an algebraic approach to the syntax and semantics of Martin-Löf type theory and the calculus of constructions developed by T. Coquand and G. Huet. In our approach, models of this theory and this calculus are treated as three-sorted partial algebras, called ITSΠ-structures, described by essentially algebraic theories. We give a proof that derived statements of Martin-Löf type theory hold in appropriate ITSΠ-structures. In this proof, a formal translation from the language of terms and types into the language of terms of an appropriate essentially algebraic theory of ITSΠ-structures is used. A straightforward set-theoretic construction of ITSΠ-structures that are models of Martin-Löf type theory is demonstrated. We present a construction of a recursive ITSΠ-structure (i.e. its partial and total operations are recursive functions over some alphabet) that is a model of the calculus of constructions and demonstrates the decidability of this calculus.

The notion of semi-functor was introduced in Hayashi (1985) in order to make possible a category-theoretical characterization of models of the non-extensional typed lambda calculus. Motivated by the further use of semi-functors in Martini (1987), Jacobs (1991) and Hoofman (1992a), (1992b) and (1992c), we consider the general theory of semi-functors in this paper. It turns out that the notion of semi natural transformation plays an important part in this theory, and that various categorical notions involving semi-functors can be viewed as 2-categorical notions in the 2-category of categories, semi-functors and semi natural transformations. In particular, we find that the notion of normal semi-adjunction as defined in Hayashi (1985) is the canonical generalization of the notion of adjunction to the world of semi-functors. Further topics covered in this paper are the relation between semi-functors and splittings, the Karoubi envelope construction, semi-comonads, and a semi-adjoint functor theorem.