Basic Programming Language Theory
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.
\[\tau:=nat\tau_1\rightarrow\tau_2\\ e:=xzs(e)iter(e_0x.e_1)(e)\lambda x:\tau.ee_1(e_2)\]So the typing:
\[\Gamma\vdash e:\tau\]is inductively defined by rules, which is the least relation closed under under some rules
Note: \(\Gamma\) can be viewed as a “context”. It could be written as something like \(\Gamma=x_1:\tau_1,x_2:\tau_2,\ldots,x_n:\tau_n\)
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 \(x:\tau\vdash x:\tau\)

Transitivity \(if:\Gamma\vdash e:\tau\ and\ \Gamma,x:\tau\vdash e':\tau' \\ then:\Gamma\vdash[e/x]e':\tau'\)

Weakening \(if:\Gamma\vdash e':\tau'\ then\ \Gamma,x:\tau\vdash e':\tau'\)

Contraction \(if:\Gamma,x:\tau,y:\tau\vdash e':\tau' \\ then:\Gamma,z:\tau\vdash[z,z/x,y]e':\tau'\)

Exchange \(if:\Gamma,x:\tau,y:\tau\vdash e':\tau' \\ then:\Gamma,y:\tau,x:\tau\vdash e':\tau'\)
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
 \[\frac{e_1\mapsto e_1'}{e_1(e_2)\mapsto e_1'(e_2)}\]
 \[\frac{e\mapsto e'}{iter{\tau}(e_0;x.e_1)(e)\mapsto iter{\tau}(e_0;x.e_1)(e')}\]
 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
 \[z\mapsto^*z\ val\]
 \[s(e)\mapsto^*s(e)\ val\]
 \[\lambda x:\tau.e\mapsto^*\lambda x:\tau.e\ val\]
 But for \(e_1(e_2)\), even by inductive hypothesis, we know \(e_1\mapsto^*v_1\) and \(e_2\mapsto^*v_2\), and \(e_1:\tau_2\rightarrow \tau,e_2:\tau_2\), we can only do \(e_1(e_2)\mapsto^*v_1(e_2)=(\lambda x:\tau_2.e')(e_2)\mapsto[e_2/x]e'\), but we can’t get any further. We do need more info about $e’$!
Therefor we introduct a strong property called hereditary termination: \(HT_\tau(e)\)
 Want: $HT_{nat}(e)$ implies $T(e)$
 Define: $HT_\tau(e)$ by induction on type $\tau$ [Tait’s Method]
 \(HT_{nat}(e)\ iff\ e\mapsto^*z\) or \(e\mapsto^*s(e')\) with \(HT_{nat}(e')\) (it is welldefined because it is the strongest predicate satisfying these rules)
 \(HT_{\tau_1\rightarrow\tau_2}(e)\ iff\ e\mapsto^*\lambda x:\tau_1.e'\) and for every $e_1$ such that \(HT_{\tau_1}(e_1),HT_{\tau_2}([e_1/x]e')\) (meaning “type goes down”). To write this in another form, \(HT_{\tau_1\rightarrow\tau_2}(e)\ iff\ (if\ HT_{\tau_1}(e_1),then\ HT_{\tau_2}(e(e_1)))\)
And we have $Thm(v2)$:
If \(e:\tau\) then \(HT_\tau(e)\), and then therefore \(T_\tau(e)\)
So now for inductive hypothesis, we not only know \(e_1\mapsto^*v_1\) 15 and \(e_2\mapsto^*v_2\), but also \(HT_{\tau_2\rightarrow\tau}(e_1)\) and \(HT_{\tau_2}(e_2)\). And because we know that $e_1$ is a $\lambda$, we now know that \([e_2/x]e'\) is $HT$!
BUT! $Thm(v2)$ is only stating about $e$ being closed terms, but for $\lambda$: \(\frac{x:\tau_1\vdash e_2:\tau_2}{\lambda x:\tau_1.e_2:\tau_1\rightarrow\tau_2}\), $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 \(\Gamma\vdash e:\tau\) and \(HT_\Gamma(\gamma)\), then \(HT_\tau(\hat{\gamma}(e))\)
So \(HT_\Gamma(\gamma)\) means that if \(\Gamma=x_1:\tau_1,x_2:\tau_2,\ldots,x_n:\tau_n\), then $\gamma=x_1\hookrightarrow e_1,x_2\hookrightarrow e_2,\ldots,x_n\hookrightarrow x_n$ (substitution) such that \(HT_{\tau_1}(e_1),\ldots,HT_{\tau_n}(e_n)\), and \(\hat{\gamma}(e)\) means to do the substitution. So we are good now!