Categorical models for non-extensional λ-calculi and combinatory logic

1992 ◽  
Vol 2 (3) ◽  
pp. 327-357 ◽  
Author(s):  
Simone Martini
Keyword(s):  
Lambda Calculus ◽  
Second Order ◽  
Combinatory Logic ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Simple Generalization ◽  
Categorical Models ◽  
Closed Structure ◽  
Cartesian Closed

The notions of weak Cartesian closed category and very weak CCC are introduced by dropping the extensionality (and the naturality) requirements in the adjunction defining the closed structure of a CCC. A number of specific examples of these categories are given. The weak notions are shown to be equivalent from both the semantic and syntactic standpoint to the typed non-extensional lambda-calculus and to the typed Combinatory Logic, extended with surjective pairs. Type-free models are characterized as reflexive objects in wCCCs. Finally, categorical models for the second-order non-extensional calculus are defined, by introducing a simple generalization of the notion of PL-category.

Least fixpoints of endofunctors of cartesian closed categories

1993 ◽  
Vol 3 (2) ◽  
pp. 229-257 ◽  
Author(s):  
J. Lambek
Keyword(s):  
Propositional Calculus ◽  
Second Order ◽  
Equivalence Relations ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Congruence Relations ◽  
Partial Recursive Functions ◽  
Cartesian Closed Categories ◽  
Partial Equivalence Relations ◽  
Cartesian Closed

Least fixpoints are constructed for finite coproducts of definable endofunctors of Cartesian closed categories that have weak polynomial products and joint equalizers of arbitrary families of pairs of parallel arrows. Both conditions hold in PER, the category whose objects are partial equivalence relations on N, and whose arrows are partial recursive functions. Weak polynomial products exist in any cartesian closed category with a finite number of objects as well as in any model of second order polymorphic lambda calculus: that is, in the proof theory of any second order positive intuitionistic propositional calculus, but such a category need not have equalizers. However, any finite coproduct of definable endofunctors of a cartesian closed category with weak polynomial products will have a least fixpoint in a larger category with equalizers whose objects are right ideals (or sieves) of modulo certain congruence relations, and whose arrows are induced from .

An enrichment theorem for an axiomatisation of categories of domains and continuous functions

1997 ◽  
Vol 7 (5) ◽  
pp. 591-618 ◽  
Author(s):  
MARCELO P. FIORE
Keyword(s):  
Fixed Point ◽  
Continuous Functions ◽  
Domain Theory ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Cartesian Closed

Domain-theoretic categories are axiomatised by means of categorical non-order-theoretic requirements on a cartesian closed category equipped with a commutative monad. In this paper we prove an enrichment theorem showing that every axiomatic domain-theoretic category can be endowed with an intensional notion of approximation, the path relation, with respect to which the category Cpo-enriches.Our analysis suggests more liberal notions of domains. In particular, we present a category where the path order is not ω-complete, but in which the constructions of domain theory (such as, for example, the existence of uniform fixed-point operators and the solution of domain equations) are available.

Monad compositions II: Kleisli strength

2008 ◽  
Vol 18 (3) ◽  
pp. 613-643 ◽  
Author(s):  
ERNIE MANES ◽  
PHILIP MULRY
Keyword(s):  
Monoidal Category ◽  
Linear Equations ◽  
Large Collection ◽  
Data Types ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Symmetric Monoidal Category ◽  
Cartesian Closed

In this paper we introduce the concept of Kleisli strength for monads in an arbitrary symmetric monoidal category. This generalises the notion of commutative monad and gives us new examples, even in the cartesian-closed category of sets. We exploit the presence of Kleisli strength to derive methods for generating distributive laws. We also introduce linear equations to extend the results to certain quotient monads. Mechanisms are described for finding strengths that produce a large collection of new distributive laws, and consequently monad compositions, including the composition of monadic data types such as lists, trees, exceptions and state.

scholarly journals De Rham's theorem in a smooth topos

1984 ◽  
Vol 96 (1) ◽  
pp. 61-71 ◽  
Author(s):  
Ieke Moerdijk ◽  
Gonzalo E. Reyes
Keyword(s):  
Calculus Of Variations ◽  
Cartesian Closed Category ◽  
World Picture ◽  
Closed Category ◽  
Mathematical World ◽  
Cartesian Closed

It has been persuasively argued (e.g. by Lawvere[8]) that the mathematical world picture needed to develop the physics of continuous bodies and fields should involve a cartesian closed category of smooth morphisms between smooth spaces. As far as the foundations of the calculus of variations are concerned, the need for such a category was recognized by K. T. Chen(cf. [2]).

Sign in / Sign up

Export Citation Format

Share Document