In this paper we define a logical framework, called &;lambda;TT, that is well suited for semantic analysis. We introduce the notion of a fibration [Lscr]1 : [Fscr]1 [xrarr ] [Cscr]1 being internally definableThe definability as used in this paper should not be confused with Bénabou's ‘definability’ (Bénabou 1985). in a fibration [Lscr]2 : [Fscr]2 [xrarr ] [Cscr]2. This notion amounts to distinguishing an internal category Lin [Lscr]2 and relating [Lscr]1 to the externalization of L through a pullback. When both [Lscr]1 and [Lscr]2 are term models of typed calculi [Lscr]1 and [Lscr]2, respectively, we say that [Lscr]1 is an internal typed calculus definable in the frame language [Lscr]2. We will show by examples that if an object language is adequately represented in λTT, then it is an internal typed calculus definable in the frame language λTT. These examples also show a general phenomenon: if the term model of an object language has categorical structure S, then an adequate encoding of the language in λTT imposes an explicit internal categorical structure S in the term model of λTT and the two structures are related via internal definability. Our categorical investigation of logical frameworks indicates a sensible model theory of encodings.

For a finite set D of nodes let E2(D)={(x, y)[mid ]x, y∈D, x≠y}. We define an inversive Δ2-structure g as a function g[ratio ]E2(D)→Δ into a given group Δ satisfying the property g(x, y)=g(y, x)−1 for all (x, y)∈E2(D). For each function (selector) σ[ratio ]D→Δ there is a corresponding inversive Δ2-structure gσ defined by gσ(x, y)=σ(x)·g(x, y)·σ(y)−1. A function η mapping each g into the group Δ is called an invariant if η(gσ)=η(g) for all g and σ. We study the group of free invariants η of inversive Δ2-structures, where η is defined by a word from the free monoid with involution generated by the set E2(D). In particular, if Δ is abelian, the group of free invariants is generated by triangle words of the form (x0, x1)(x1, x2)(x2, x0).

Results of Anick (1986), Squier (1987), Kobayashi (1990), Brown (1992b), and others, show that a monoid with a finite convergent rewriting system satisfies a homological condition known as FP∞.

In this paper we give a simplified version of Brown's proof, which is conceptual, in contrast with the other proofs, which are computational.

We also collect together a large number of results and examples of monoids and groups that satisfy FP∞ and others that do not. These may provide techniques for showing that various monoids do not have finite convergent rewriting systems, as well as explicit examples with which methods can be tested.

This special issue of Mathematical Structures in Computer Science is devoted to the Proceedings of the International Workshop Logic, Domains, and Programming Languages that took place from May 24 to 27, 1995, in Darmstadt, Germany.

Milner's action calculus implements abstraction in monoidal categories, so that familiar λ-calculi can be subsumed together with the π-calculus and the Petri nets. Variables are generalised to names, which allow only a restricted form of substitution.

In the present paper, the well-known categorical semantics of the λ-calculus is generalised to the action calculus. A suitable functional completeness theorem for symmetric monoidal categories is proved: we determine the conditions under which the abstraction is definable. Algebraically, the distinction between the variables and the names boils down to the distinction between the transcendental and the algebraic elements. The former lead to polynomial extensions, like, for example, the ring ℤ[x]; the latter lead to algebraic extensions like ℤ[√2] or ℤ[i].

Building upon the work of P. Gardner, we introduce action categories, and show that they are related to the static action calculus in exactly the same way as cartesian closed categories are related to the λ-calculus. Natural examples of this structure arise from allegories and cartesian bicategories. On the other hand, the free algebras for any commutative Moggi monad form an action category. The general correspondence of action calculi and Moggi monads will be worked out in a sequel to this work.

We investigate the proof structure and models of theories of classes, where classes are ‘collections’ of entities. The theories are weaker than set theories and arise from a study of type classes in programming languages, as well as from comprehension schemata in categories. We introduce two languages of proofs: one a simple type theory and the other involving proof environments for storing and retrieving proofs. The relationship between these languages is defined in terms of a normalisation result for proofs. We use this result to define a categorical semantics for classes and establish its coherence. Finally, we show how the formal systems relate to type classes in programming languages.

A large number of observational semantics for process description languages have been developed, many of which are based on the notion of bisimulation. In this paper, we consider in detail the problem of defining a semantic framework to unify these. The discussion takes place in a purely algebraic setting. We introduce a special class of algebras called Structured Transition Systems. A structured transition system can be viewed as a transition system with an algebraic structure both on states and transitions. In this framework, observations of behaviours are dealt with by means of maps from the transitions to some algebra of observations.

Using several examples, we show that this framework allows us to describe a range of observational semantics within a single underlying presentation: it is enough to consider different mappings and algebras of observations. Furthermore, we introduce a notion of bisimulation that is parameterized with respect to the choice of the algebra of observations, and we find circumstances under which a Structured Transition System has good properties with respect to this parameterized bisimulation.

First, some general syntactic constraints, independent from the choice of the algebra of the observations, are given for Structured Transition System presentations. We show that these constraints ensure that parameterized bisimulation is always a congruence. Next, we address the problem of Minimal Realizations. We show that when the presentation satisfies the syntactic constraints there exists a minimal realization, i.e., there is a model of the presentation whose elements fully characterize congruence classes under bisimulation.

We study three comonads derived from the comma construction. The induced coalgebras correspond to the three concepts displayed in the title of the paper. The comonad that yields the *-autonomous categories is, in essence, the Chu construction, which has recently awaken much interest in computer science. We describe its couniversal property. It is right adjoint to the inclusion of *-autonomous categories among autonomous categories, with lax structure-preserving morphisms. Moreover, this inclusion turns out to be comonadic: *-autonomous categories are exactly the Chu-coalgebras.

We construct an approximating chain of simple valuations on the upper space of a compact metric space whose lub is a given probability measure on the metric space. We show that whenever a separable metric space is homeomorphic to a Gδ subset of an ω-continuous dcpo equipped with its Scott topology, the space of probability measures of the metric space equipped with the weak topology is homeomorphic with a subset of the maximal elements of the probabilistic power domain of the ω-continuous dcpo. Given an effective approximation of a probability measure by an increasing chain of normalised valuations on the upper space of a compact metric space, we show that the expected value of any Hölder continuous function on the space can be obtained up to any given accuracy. We present a novel application in computing integrals in dynamical systems. We obtain an algorithm to compute the expected value of any Hölder continuous function with respect to the unique invariant measure of the Feigenbaum map in the periodic doubling route to chaos.

Intersection types and bounded quantification are complementary extensions of a first-order programming language with subtyping. We define a typed λ-calculus combining these extensions, illustrate its unusual properties, and develop basic proof-theoretic and semantic results leading to algorithms for subtyping and typechecking.

This paper presents a new and self-contained proof of a result characterizing objects isomorphic in the free symmetric monoidal closed category, i.e., objects isomorphic in every symmetric monoidal closed category. This characterization is given by a finitely axiomatizable and decidable equational calculus, which differs from the calculus that axiomatizes all arithmetical equalities in the language with 1, product and exponentiation by lacking 1c=1 and (a · b)c=ac · bc (the latter calculus characterizes objects isomorphic in the free cartesian closed category). Nevertheless, this calculus is complete for a certain arithmetical interpretation, and its arithmetical completeness plays an essential role in the proof given here of its completeness with respect to symmetric monoidal closed isomorphisms.

We investigate Girard's calculus Fω as a ‘Curry style’ type assignment system for pure lambda terms. First we show an example of a strongly normalizable term that is untypable in Fω. Then we prove that every partial recursive function is nonuniformly represented in Fω (even if quantification is restricted to constructor variables of level 1). It follows that the type reconstruction problem is undecidable and cannot be recursively separated from normalization.

Place/transition (PT) Petri nets are one of the most widely used models of concurrency. However, they still lack, in our view, a satisfactory semantics: on the one hand the ‘token game’ is too intensional, even in its more abstract interpretations in terms of nonsequential processes and monoidal categories; on the other hand, Winskel's basic unfolding construction, which provides a coreflection between nets and finitary prime algebraic domains, works only for safe nets. In this paper we extend Winskel's result to PT nets. We start with a rather general category PTNets of PT nets, we introduce a category DecOcc of decorated (nondeterministic) occurrence nets and we define adjunctions between PTNets and DecOcc and between DecOcc and Occ, the category of occurrence nets. The role of DecOcc is to provide natural unfoldings for PT nets, i.e., acyclic safe nets where a notion of family is used to relate multiple instances of the same place. The unfolding functor from PTNets to Occ reduces to Winskel's when restricted to safe nets. Moreover, the standard coreflection between Occ and Dom, the category of finitary prime algebraic domains, when composed with the unfolding functor above, determines a chain of adjunctions between PTNets and Dom.

We propose a general theory of partial n-place operations based solely on the primitive notion of the application of a (possibly partial) operation to n objects. This theory is strongly selfdescriptive in that the fundamental manipulations of operations, that is, application, composition, abstraction, union, intersection and so on, are themselves internal operations. We give several applications of this theory, including implementations of partial n-ary λ-calculus, and other operation description languages. We investigate the issue of extensionality and give weakly extensional models of the theory.

Algebraic CPOs naturally generalize to finitely accessible categories, and Scott domains (i.e., consistently complete algebraic CPOs) then correspond to what we call Scott-complete categories: finitely accessible, consistently (co-)complete categories. We prove that the category SCC of all Scott-complete categories and all continuous functors is cartesian closed and provides fixed points for a large collection of endofunctors. Thus, SCC can serve as a basis for semantics of computer languages.

This paper studies the properties of the subnets of a proof-net for first-order Multiplicative Linear Logic without propositional constants (MLL−), extended with the rule of Mix: from [vdash ]Γ and [vdash ]Δ infer [vdash ]Γ, Δ. Asperti's correctness criterion and its interpretation in terms of concurrent processes are extended to the first-order case. The notions of kingdom and empire of a formula are extended from MLL− to MLL−+MIX. A new proof of the sequentialization theorem is given. As a corollary, a system of proof-nets is given for De Paiva and Hyland's Full Intuitionistic Linear Logic with Mix; this result gives a general method for translating Abramsky-style term assignments into proof-nets, and vice versa.

The traditional notions of strong and weak normalization refer to properties of a binary reduction relation. In this paper we explore an alternative approach to normalization, in which we bypass the reduction relation and instead focus on the normalization function, that is, the function that maps a term to its normal form. We work in an intuitionistic metalanguage, and characterize a normalization function as an algorithm that picks a canonical representative from the equivalence class of convertible terms. This means that we also get a decision algorithm for convertibility.Such a normalization function can be constructed by building an appropriate model and a function quote, which inverts the interpretation function. The normalization function is then obtained by composing the quote function with the interpretation function. We also discuss how to get a simple proof of the property that constructors are one-to-one, which is usually obtained as a corollary of Church–Rosser and normalization in the traditional sense.We illustrate this approach by showing how a glueing model (closely related to the glueing construction used in category theory) gives rise to a normalization algorithm for a combinatory formulation of Gödel System T. We then show how the method extends in a straightforward way when we add cartesian products and disjoint unions (full intuitionistic propositional logic under a Curry–Howard interpretation) and transfinite inductive types such as the Brouwer ordinals.

We define weak inclusion systems as a natural extension of inclusion systems. We prove that several properties of factorisation systems and inclusion systems remain valid under this extension and we obtain new properties as algebraic tools in abstract model theory.

A V-labelled poset P can induce an operation on the languages on any fixed alphabet, as well as an operation on labelled posets (as noticed by Pratt and Gischer (Pratt 1986; Gischer 1988)). For any collection X of V-labelled posets and any alphabet Σ we obtain an X-algebra ΣX of languages on Σ. We consider the variety Lang(X) generated by these algebras when X is a collection of nonempty ‘traceable posets’. The current paper contains several observations about this variety. First, we use one of the basic results in Bloom and Ésik (1996) to show that a concrete description of the A-generated free algebra in Lang(X) is the X-subalgebra generated by the singletons (labelled a∈A) in the X-algebra of all A-labelled posets. Equipped with an appropriate ordering, these same algebras are the free ordered algebras in the variety Lang(X)[les ] of ordered language X-algebras. Further, if one enriches the language algebras by adding either a binary or infinitary union operation, the free algebras in the resulting variety are described by certain ‘closed’ subsets of the original free algebras. Second, we show that for ‘reasonable sets’ X, the variety Lang(X) has the property that for each n[ges ]2, the n-generated free algebra is a subalgebra of the 1-generated free algebra. Third, knowing the free algebras enables us to show that these varieties are generated by the finite languages on a two-letter alphabet.

The purpose of this note is to show that the correctness of a multiplicative proof net with mix is equivalent to its semantic correctness: a proof structure is a proof net if and only if its semantic interpretation is a clique, where one given finite coherence space interprets all propositional variables.

This is just an example of what can be done with these kinds of semantic techniques; for more information and further results, the reader is referred to Retoré (1994).