constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
internalization and categorical algebra
algebra object (associative, Lie, …)
internal category ($\to$ more)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In a cartesian closed category , given an object $S$, the selection monad, also known as the select monad, is the endofunctor $J_S(X) \mapsto [[X, S], X]$ (where $[-,-]$ denotes the internal hom).
This is a strong monad.
There is a monad homomorphism from the selection monad to the continuation monad for $S$, $K_S(X) = (X \to S) \to S$, which sends $\epsilon \in J_S(X)$ to $\bar{\epsilon} \in K_S(X)$, where $\bar{\epsilon}(p) = p(\epsilon(p))$.
If we understand the continuation monad as mapping an object to the generalized quantifiers over it, with $S$ a generalized truth value, a selection function for a generalized quantifier is an element of its preimage under the monad morphism.
For instance, a selection functional for the supremum functional $sup: (X \to S) \to S$, when it exists, applied to a function, $p: X \to S$, gives a point in $X$ at which $p$ attains its maximum value.
Due to the resemblance of an algebra, $J_S(A) \to A$, to Peirce's law in logic, $((p \Rightarrow q) \Rightarrow p) \Rightarrow p$, $J_S$ is also called the Peirce monad in (Escardó-Oliva 2012).
§2.5 of Kieburtz, Richard B., Borislav Agapiev, and James Hook. Three monads for continuations. Oregon Graduate Institute of Science and Technology, Department of Computer Science and Engineering, 1992.
Martín Escardó and Paulo Oliva, Selection Functions, Bar Recursion, and Backward Induction, Mathematical Structures in Computer Science, 20(2):127–168, 2010, (pdf)
Martín Escardó and Paulo Oliva, What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common, (pdf)
Martín Escardó and Paulo Oliva, The Peirce translation, Annals of Pure and Applied Logic, 163(6):681–692, 2012, (pdf).
Jules Hedges, The selection monad as a CPS transformation, (arXiv:1503.06061)
Martin Abadi, Gordon Plotkin, Smart Choices and the Selection Monad, (arXiv:2007.08926)
Marcelo Fiore, Fast-growing clones, (Talk at CT 2019)
Last revised on November 6, 2022 at 10:00:15. See the history of this page for a list of all contributions to it.