Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Effective topos
Résumé
In mathematics, the effective topos introduced by captures the mathematical idea of effectivity within the framework.
The topos is based on the partial combinatory algebra given by Kleene's first algebra . In Kleene's notion of recursive realizability, any predicate is assigned realizing numbers, i.e. a subset of . The extremal propositions are and , realized by and . However in general, this process assigns more data to a proposition than just a binary truth value.
A formula with free variables will give rise to a map in the values of which is the subset of corresponding realizers.
is a prime example of a realizability topos. These are a class of elementary topoi with an intuitionistic internal logic and fulfilling a form of dependent choice. They are generally not Grothendieck topoi.
In particular, the effective topos is . Other realizability topos construction can be said to abstract away the some aspects played by here.
The objects are pairs of sets together with a symmetric and transitive relation in , representing a form of equality. But the so called existence predicate can be empty, and so this is not generally reflexive.
Arrows amount to equivalence classes of functional relations appropriately respecting the defined equalities.
The classifier amounts to . The pair (or, by abuse of notation, just that underlying powerset) may be denoted as .
An entailment relation on makes it into a Heyting pre-algebra.
Such a context allows to define the appropriate lattice-like logic structure, with logical operations given in terms of operations of the realizer sets, making use of pairs and computable functions.
The terminal object is a singleton with trivial existence predicate (). The finite product respect the equality appropriately.
The classifier's equality is given through equivalences in its lattice.
Some objects exhibit a rather trivial existence predicate depending only on the validity of the equality relation "" of sets, so that valid equality maps to the top set and rejected equality maps to .
Source officielle
À 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.