Total Programming Language
E.Coli of Total PLs  Godel’s T: It codifies higher order functions and inductive types (nat)
What does it mean for a PL to exist?
A PL consists of two parts:
 Statics: What are the programs?
 Dynamics: How do we run them?
Basic criterion: Coherence
Statics
We will talk about abstract syntax and contextsensitiveconditions on wellformation.
Formal = typing is inductively defined.
We only have information about the types but not the elements themselves.
So we only care about two things, higher order functions, and nat.
So the typing:
is inductively defined by rules, which is the least relation closed under under some rules
Note: can be viewed as a “context”. It could be written as something like
e.g. natural number
Hypothetical Judgement (Structural):
Note: 1 and 2 are indefeasible. 3, 4, 5 is defeasible (Will be different in substructural type systems).

Reflexivity

Transitivity

Weakening

Contraction

Exchange
Dynamics
Execute close code (no free variables)
We need to specify:
 $e\ val$
 States of execution $S$
 Transition $S\mapsto S’$
 Initial State and final state
Some rules:
 zero is a value
 successor is a value
 function is a value
 functions can be executed
 Values are stuck/finished
 Determinism/functional language
Note: dynamics doesn’t care about types!
Coherence of Dynamics/Statics/Type Safety($\infty$):
 Preservation
 Progress
 Termination
Here we proof Termination ($T(e)$ means $e$ terminates). According to Godel, if we proof termination, we are proving the consistency of the arithmetic, so we need methods that go beyong the arithmetic (Godel’s incompleteness):
 $e$ itself can’t be a variable becasue it is closed
 But for , even by inductive hypothesis, we know and , and , we can only do , but we can’t get any further. We do need more info about $e’$!
Therefor we introduct a strong property called hereditary termination:
 Want: $HT_{nat}(e)$ implies $T(e)$
 Define: $HT_\tau(e)$ by induction on type $\tau$ [Tait’s Method]
 or with (it is welldefined because it is the strongest predicate satisfying these rules)
 and for every $e_1$ such that (meaning “type goes down”). To write this in another form,
And we have $Thm(v2)$:
If then , and then therefore
So now for inductive hypothesis, we not only know 15 and , but also and . And because we know that $e_1$ is a $\lambda$, we now know that is $HT$!
BUT! $Thm(v2)$ is only stating about $e$ being closed terms, but for $\lambda$: , $e_2$ is an open term, meaning it is a variable, so our theorm doesn’t quite work. We must account for open terms!
$Thm(v3)$[Tait]:
If and , then
So means that if , then $\gamma=x_1\hookrightarrow e_1,x_2\hookrightarrow e_2,\ldots,x_n\hookrightarrow x_n$ (substitution) such that , and means to do the substitution. So we are good now!