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]$. It 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).
There is a distributive law $T J_S \Rightarrow J_S T$ for every strong monad $T$ (Fiore 2019).
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 December 30, 2020 at 12:02:41. See the history of this page for a list of all contributions to it.