computation

**constructive mathematics**, **realizability**, **computability**

propositions as types, proofs as programs, computational trinitarianism

**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**

logic | category theory | type theory |
---|---|---|

true | terminal object/(-2)-truncated object | h-level 0-type/unit type |

proposition(-1)-truncated objecth-proposition, mere proposition

proofgeneralized elementprogram

cut rulecomposition of classifying morphisms / pullback of display mapssubstitution

cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction

introduction rule for implicationunit for hom-tensor adjunctioneta conversion

logical conjunctionproductproduct type

disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)

implicationinternal homfunction type

negationinternal hom into initial objectfunction type into empty type

universal quantificationdependent productdependent product type

existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalencepath space objectidentity type

equivalence classquotientquotient type

inductioncolimitinductive type, W-type, M-type

higher inductionhigher colimithigher inductive type

completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set

setinternal 0-groupoidBishop set/setoid

universeobject classifiertype of types

modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation

proof netstring diagramquantum circuit

(absence of) contraction rule(absence of) diagonalno-cloning theorem

synthetic mathematicsdomain specific embedded programming language

</table>

basic constructions:

strong axioms

further

A program. A construction of a term of some type. The topic of computability theory.

type I computability | type II computability | |
---|---|---|

typical domain | natural numbers $\mathbb{N}$ | Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$ |

computable functions | partial recursive function | computable function (analysis) |

type of computable mathematics | recursive mathematics | computable analysis, Type Two Theory of Effectivity |

type of realizability | number realizability | function realizability |

partial combinatory algebra | Kleene's first partial combinatory algebra | Kleene's second partial combinatory algebra |

Last revised on March 2, 2014 at 03:50:45. See the history of this page for a list of all contributions to it.