Categorical logic

NOTOC Categorical logic is the branch of mathematics in which tools and concepts from are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a , and an interpretation by a functor. The categorical framework provides a rich conceptual background for logical and type-theoretic constructions. The subject has been recognisable in these terms since around 1970. There are three important themes in the categorical approach to logic: Categorical semantics Categorical logic introduces the notion of structure valued in a category C with the classical model theoretic notion of a structure appearing in the particular case where C is the . This notion has proven useful when the set-theoretic notion of a model lacks generality and/or is inconvenient. R.A.G. Seely's modeling of various impredicative theories, such as System F, is an example of the usefulness of categorical semantics. It was found that the connectives of pre-categorical logic were more clearly understood using the concept of adjoint functor, and that the quantifiers were also best understood using adjoint functors. Internal languages This can be seen as a formalization and generalization of proof by diagram chasing. One defines a suitable internal language naming relevant constituents of a category, and then applies categorical semantics to turn assertions in a logic over the internal language into corresponding categorical statements. This has been most successful in the theory of toposes, where the internal language of a topos together with the semantics of intuitionistic higher-order logic in a topos enables one to reason about the objects and morphisms of a topos "as if they were sets and functions". This has been successful in dealing with toposes that have "sets" with properties incompatible with classical logic. A prime example is Dana Scott's model of untyped lambda calculus in terms of objects that onto their own function space.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (9)

Personnes associées (1)

Concepts associés (16)

Séances de cours associées (7)

Filter quotients and non-presentable (∞,1)-toposes

Nima Rasekh

We define filter quotients of -categories and prove that filter quotients preserve the structure of an elementary -topos and in particular lift the filter quotient of the underlying elementary topos. We then specialize to the case of filter products of -ca ...

2021

We present the development of a multiphase adjoint for the Community Multiscale Air Quality (CMAQ) model, a widely used chemical transport model. The adjoint model provides location- and time-specific gradients that can be used in various applications such ...

2020

Compilation Techniques for Incremental Collection Processing

Daniel Lupei

Many map-reduce frameworks as well as NoSQL systems rely on collection programming as their interface of choice due to its rich semantics along with an easily parallelizable set of primitives. Unfortunately, the potential of collection programming is not ...

EPFL2017

Contexte catégorique des objets G

S'insère dans le cadre catégorique des actions de groupe et dans la correspondance entre les actions G sur c et les functeurs de BG à C.

Théorie de groupe: Vérification

Couvre la vérification des constructions dans le contexte des groupes abeliens et des sous-groupes Sylow.

Notation: Coproduct vs Produit

Explore la distinction entre coproduit et notation de produit dans les constructions catégoriques au sein des groupes abeliens.

Simply typed lambda calculus

The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus. The term simple type is also used to refer extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF).

Catégorie cartésienne

Une catégorie cartésienne est, en mathématiques — et plus précisément en théorie des catégories — une catégorie munie d'un objet terminal et du produit binaire. Dans une catégorie cartésienne, la notion de morphisme entre morphismes n'a pas encore de sens. C'est pourquoi l'on définit l'exponentiation, c'est-à-dire l'objet B qui représente l'« ensemble » des morphismes de A dans B. Munie de cette propriété de clôture qu'est l'exponentiation, une catégorie cartésienne devient une catégorie cartésienne fermée.

Sémantique des langages de programmation

En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques. Comme en linguistique, la sémantique, appliquée aux langages de programmation, désigne le lien entre un signifiant, le programme, et un signifié, objet mathématique. L'objet mathématique dépend des propriétés à connaître du programme. La sémantique est également le lien entre : le langage signifiant : le langage de programmation le langage signifié : logique de Hoare, automates.