Types and impredicativity
Table of Contents
Decidability
why it matters?
Because your program can have more bits than there are atoms in universe.
Also when reduction doesn't normalize the expresssion
Function types in haskell for inststance aren't decidable, with due exceptions. Analogy
| Logic | TT | Haskell |
| P | A | a |
| P/\Q | A*B | (a,b) |
| P->Q | A->B | either(a,b) |
| ∀ x P(x) | ∏ a: a P(a) | |
| ∃ x P(a) | ∑ a: a P(a) | |
| proof | inhabitant | program |
Progamming construct as corresponding (ir of ) logic
| logic | construct |
| linear | rust borrow checker , cbpv |
| double negation, classical | csp, cbpv |
| mu calculus | call cc |
| system f | stlc + parametric polymorphism |
| modus ponens | eval map |
| material implication, currying adjunction | exponential object |
| tautology | terminal object has a global preposition |
| modality | provability in axiom-K |
| modus ponens : resolution | substitution,subtyping, function application |
| ch, aoc | imcrecdicative |
| skolem, unification, sequent | tebleaux prolog |
| modal logic | referential transparency |
| modal algebra | boolean algebra + unary op |
| prepositional | invariant in bisimulation |
| fol | no normal forms |
| terms:lamda calc to combinatory logic | ch-deduction meta theorem |
Type theory and Poperties
| tt | Property |
| mltt | everything terminates |
Questions
constuctivity is needed for computability , would you say that about predicativity ?
It turns out if you tweak ZF in the right way, and remove EM, you get a perfectly fine constructive logic, i.e. a theory in which every function nat -> nat can be realized by some lambda term.
Harder to say what happens at other function spaces though… tweet
table 1 reference
Papers
intuitionistic games : determinacy , completeness and normalization
automata theory approach to inutionistic logic
objects of interest
Axiom K
constructive
intutionistic
Induction
bar induction
l¨ob induction 🏿
Created: 2022-11-16 Wed 11:18