Fundamenta Informaticae

The paper discusses, in a categorical perspective, some recent works on optimal graph reduction techniques for the λ-calculus. In particular, we relate the two “brackets” in [GAL92a] to the two operations associated with the comonad “!” of Linear Logic. The rewriting rules can be then understood as a “local implementation” of naturality laws, that is as the broadcasting of some information from the output to the inputs of a term, following its connected structure.

The first mathematical model of untyped lambda calculus was discovered by DANA SCOTT in the category of algebraic lattices and Scott continuous maps. The question then arises as to which other cartesian closed categories contain a model of the calculus. In this paper we show that any compact Hausdorff model of the calculus must satisfy the property that the semantic map from the calculus to the model is constant. In particular, any compact reflexive object in the category of Hausdorff k-spaces gives rise to a degenerate model of the calculus. We also explore the relationship of the results we derive to the notions of a combinatory model and of an environment model of the calculus.

In this paper a cut elimination theorem is proved for classical non-commutative linear logic without exponentials, presented as a dual Schütte style deductive system. The notion of equality between deductions is sketched and they are interpreted as relations, in the spirit of the formulas as types paradigm.

In this paper we show that there is no left adjoint to the inclusion functor from the full subcategory 𝒞₀ of Scott domains (i.e., consistently complete ω–algebraic cpo's) to 𝒮ℱ𝒫, the category of 𝒮ℱ𝒫-objects and Scott-continuous maps. We also show there is no left adjoint to the inclusion functor from 𝒞₀ to any larger category of cpo's which contains a simple five-element domain. As a corollary, there is no left adjoint to the inclusion functor from 𝒞₀ to the category of L-domains. We also investigate adjunctions between categories which contain 𝒞₀, such as 𝒮ℱ𝒫, and sub categories of 𝒞₀. Of course, it is well-known that each of the three standard power domain constructs gives rise to a left adjoint. Since the Hoare and Smyth power domains are Scott domains, we can regard each of these two adjunctions as left adjoints to inclusion functors from appropriate subcategories of 𝒞₀. But, our interest here is in adjunctions for which the target of the left adjoint is a lluf subcategory of 𝒞; such a subcategory has all Scott domains as objects, but the morphisms are more restrictive than being Scott continuous. We show that three such adjunctions exist. The first two of these are based on the Smyth power domain construction. One is a left adjoint to the inclusion functor from the category 𝒞 of consistently complete algebraic cpo's and Scott-continuous maps preserving finite, non-empty infima to the category of coherent algebraic cpo's and Scott-continuous maps. The same functor has a restriction to the subcategory of coherent algebraic cpo's whose morphisms also are Lawson continuous to the lluf subcategory of 𝒞 whose morphisms are those Scott-continuous maps which preserve all non-empty infima. The last adjunction we derive is a generalization of the Hoare power domain which satisfies the property that, if D is a nondeterministic algebra, then the image of D under the left adjoint enjoys an additional semigroup structure under which the original algebra D is among the set of idempotents. In this way, we expand the Plotkin power domain 𝒫(D) over the Scott domain D into a Scott domain.

This paper proposes an internal semantics for the modalities and evaluation predicate of Pitts' Evaluation Logic, and introduces several predicate calculi (ranging from Horn sequents to Higher Order Logic), which are sound and complete w.r.t. natural classes of models. It is shown (by examples) that many computational monads satisfy the additional properties required by the proposed semantics.

Categorical Combinators arose from the intertranslation between lambda-calculus and Cartesian Closed Categories. Their theory is fairly similar to classical Combinatory Logic, and they also have been used for the design of the so called Categorical Abstract Machine [2]. The latter is claimed to be more efficient than Landin's SEDC Machine [9], which has been based on classical combinators. There is, however, an intriguing problem with Categorical Combinators. Namely, their defining properties imply the existence of surjective pairing, which is known to be incompatible with the Church-Rosser property in the type-free lambda-calculus. The non-confluence of the type-free lambda-calculus with surjective pairing was shown by Klop in 1980 [5]. In March, 1991, Curien communicated an amazingly simple new proof. The confluence of Curien's Strong Categorical Combinatory Logic [3], which involves surjective pairing, is still an open problem. Therefore, Curien and others have studied various weaker systems. One of them appears to be closely related to a conservative extension of the type-free lambda-calculus, whose confluence has been shown by the author in a previous paper [11]. In this paper we study the relationship between categorical combinators and our Extended Lambda-Calculus with Explicit Products, which was first published in 1984 [10].

This paper describes an algebraic framework for the study of dataflow networks, which form a paradigm for concurrent computation in which a collection of concurrently and asynchronously executing processes communicate by sending messages between ports connected via FIFO message channels. A syntactic dataflow calculus is defined, having two kinds of terms which represent networks and computations, respectively. By imposing suitable equivalences on networks and computations, we obtain the free dataflow algebra, in which the dataflow networks with m input ports and n output ports are regarded as the objects of a category Sⁿ_m, and the computations of such networks are represented by the arrows. Functors defined on Sⁿ_m label each computation by the input buffer consumed and the output buffer produced during that computation, so that each Sⁿ_m is a span in Cat. It is shown that the free dataflow algebra construction underlies a monad in the category of collections S = {Sⁿ_m : m, n ≥ 0} of spans in Cat. The algebras of this monad, called dataflow algebras, have a monoid structure representing parallel composition, and are also equipped with an action of a certain collection of continuous functions, thereby representing the formation of feedback loops. The two structures are related by a distributive law of feedback over parallel composition. We also observe the following connection with the theory of fibrations: if S is a dataflow algebra, then each Sⁿ_m is a split bifibration in Cat.

In an earlier paper Walters introduced a family of imperative programming languages based on concepts from distributive categories. The development in that, and in a subsequent paper by Walters and Khalil, was carried out within the category Set of sets and total functions. In this paper we investigate the generalization of the results of those earlier papers to more general distributive categories using fix-point constructions to replace the specific calculations used earlier.