This article will be permanently flagged as inappropriate and made unaccessible to everyone. Are you certain this article is inappropriate? Excessive Violence Sexual Content Political / Social
Email Address:
Article Id: WHEBN0000237037 Reproduction Date:
In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in that their internal language is the simply typed lambda calculus. They are generalized by closed monoidal categories, whose internal language, linear type systems, are suitable for both quantum and classical computation.[1]
The category C is called Cartesian closed[2] if and only if it satisfies the following three properties:
The first two conditions can be combined to the single requirement that any finite (possibly empty) family of objects of C admit a product in C, because of the natural associativity of the categorical product and because the empty product in a category is the terminal object of that category.
The third condition is equivalent to the requirement that the functor –×Y (i.e. the functor from C to C that maps objects X to X×Y and morphisms φ to φ×idY) has a right adjoint, usually denoted –Y, for all objects Y in C. For locally small categories, this can be expressed by the existence of a bijection between the hom-sets
which is natural in both X and Z.
If a category is such that all its slice categories are Cartesian closed, then it is called locally Cartesian closed.
Examples of Cartesian closed categories include:
The following categories are not Cartesian closed:
In Cartesian closed categories, a "function of two variables" (a morphism f:X×Y → Z) can always be represented as a "function of one variable" (the morphism λf:X → ZY). In computer science applications, this is known as currying; it has led to the realization that simply-typed lambda calculus can be interpreted in any Cartesian closed category.
The Curry-Howard-Lambek correspondence provides a deep isomorphism between intuitionistic logic, simply-typed lambda calculus and Cartesian closed categories.
Certain Cartesian closed categories, the topoi, have been proposed as a general setting for mathematics, instead of traditional set theory.
The renowned computer scientist John Backus has advocated a variable-free notation, or Function-level programming, which in retrospect bears some similarity to the internal language of Cartesian closed categories. CAML is more consciously modelled on Cartesian closed categories.
In every Cartesian closed category (using exponential notation), (XY)Z and (XZ)Y are isomorphic for all objects X, Y and Z. We write this as the "equation"
One may ask what other such equations are valid in all Cartesian closed categories. It turns out that all of them follow logically from the following axioms:[4]
Bicartesian closed categories extend Cartesian closed categories with binary coproducts and an initial object, with products distributing over coproducts. Their equational theory is extended with the following axioms:
Note however that the above list is not complete; type isomorphism in the free BCCC is not finitely axiomatizable, and its decidability is still an open problem.[5]
Cryptography, Artificial intelligence, Software engineering, Science, Machine learning
Set theory, Logic, Model theory, Mathematics, Foundations of mathematics
Axiom of choice, Mathematical logic, Category theory, Mathematics, Foundations of mathematics
Computer science, Statistics, Set theory, Topology, Mathematical logic
Computer science, Mathematics, Topology, Combinatorics, Numerical analysis
Mathematical logic, Parallel computing, Computer science, Category theory, Linguistics
Theory of computation, Applicative computing systems, Combinatory logic, Evaluation strategy, Cartesian closed category
Lambda calculus, Programming language, Theoretical computer science, Category theory, ML programming language
Category theory, Hom functor, *-autonomous Category, Cartesian closed category, Closed category
Mathematics, Modus ponens, Boolean algebra, Topology, Oclc