Total Programming LanguagePermalink

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?Permalink

A PL consists of two parts:

• Statics: What are the programs?
• Dynamics: How do we run them?

Basic criterion: Coherence

StaticsPermalink

We will talk about abstract syntax and context-sensitive-conditions on well-formation.

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: $\Gamma$ can be viewed as a “context”. It could be written as something like $\Gamma =x_1:{\tau }_1,x_2:{\tau }_2,\dots ,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).

1. Reflexivity $x:\tau ⊢x:\tau$

2. Transitivity $if:\Gamma ⊢e:\tau and\Gamma ,x:\tau ⊢e^{\prime }:{\tau }^{\prime }then:\Gamma ⊢\left[e/x\right]e^{\prime }:{\tau }^{\prime }$

3. Weakening $if:\Gamma ⊢e^{\prime }:{\tau }^{\prime }then\Gamma ,x:\tau ⊢e^{\prime }:{\tau }^{\prime }$

4. Contraction $if:\Gamma ,x:\tau ,y:\tau ⊢e^{\prime }:{\tau }^{\prime }then:\Gamma ,z:\tau ⊢[z,z/x,y]e^{\prime }:{\tau }^{\prime }$

5. Exchange $if:\Gamma ,x:\tau ,y:\tau ⊢e^{\prime }:{\tau }^{\prime }then:\Gamma ,y:\tau ,x:\tau ⊢e^{\prime }:{\tau }^{\prime }$

DynamicsPermalink

Execute close code (no free variables)

We need to specify:

• $eval$
• States of execution $S$
• Transition $S\mapsto S^{\prime }$
• 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^{\prime }}{e_1\left(e_2\right)\mapsto e_1^{\prime }\left(e_2\right)}$$
• $$\frac{e\mapsto e^{\prime }}{iter\tau (e_0;x.e_1)\left(e\right)\mapsto iter\tau (e_0;x.e_1)\left(e^{\prime }\right)}$$
• 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\left(e\right)$ 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):

1. $e$ itself can’t be a variable becasue it is closed
2. $$z{\mapsto }^{\ast }zval$$
3. $$s\left(e\right){\mapsto }^{\ast }s\left(e\right)val$$
4. $$\lambda x:\tau .e{\mapsto }^{\ast }\lambda x:\tau .eval$$
5. But for $e_1\left(e_2\right)$, even by inductive hypothesis, we know $e_1{\mapsto }^{\ast }{v}_1$ and $e_2{\mapsto }^{\ast }{v}_2$, and $e_1:{\tau }_2\to \tau ,e_2:{\tau }_2$, we can only do $e_1\left(e_2\right){\mapsto }^{\ast }{v}_1\left(e_2\right)=(\lambda x:{\tau }_2.e^{\prime })\left(e_2\right)\mapsto \left[e_2/x\right]e^{\prime }$, but we can’t get any further. We do need more info about $e^{\prime }$!

Therefor we introduct a strong property called hereditary termination: $H{T}_{\tau }\left(e\right)$

• Want: $H{T}_{nat}\left(e\right)$ implies $T\left(e\right)$
• Define: $H{T}_{\tau }\left(e\right)$ by induction on type $\tau$ [Tait’s Method]
  • $H{T}_{nat}\left(e\right)iffe{\mapsto }^{\ast }z$ or $e{\mapsto }^{\ast }s\left(e^{\prime }\right)$ with $H{T}_{nat}\left(e^{\prime }\right)$ (it is well-defined because it is the strongest predicate satisfying these rules)
  • $H{T}_{{\tau }_1\to {\tau }_2}\left(e\right)iffe{\mapsto }^{\ast }\lambda x:{\tau }_1.e^{\prime }$ and for every $e_1$ such that $H{T}_{{\tau }_1}\left(e_1\right),H{T}_{{\tau }_2}\left(\right[e_1/x\left]e^{\prime }\right)$ (meaning “type goes down”). To write this in another form, $H{T}_{{\tau }_1\to {\tau }_2}\left(e\right)iff\left(ifH{T}_{{\tau }_1}\right(e_1),thenH{T}_{{\tau }_2}(e\left(e_1\right)\left)\right)$

And we have $Thm\left(v2\right)$:

If $e:\tau$ then $H{T}_{\tau }\left(e\right)$, and then therefore $T_{\tau }\left(e\right)$

So now for inductive hypothesis, we not only know $e_1{\mapsto }^{\ast }{v}_1$ 15 and $e_2{\mapsto }^{\ast }{v}_2$, but also $H{T}_{{\tau }_2\to \tau }\left(e_1\right)$ and $H{T}_{{\tau }_2}\left(e_2\right)$. And because we know that $e_1$ is a $\lambda$, we now know that $\left[e_2/x\right]e^{\prime }$ is $HT$!

BUT! $Thm\left(v2\right)$ is only stating about $e$ being closed terms, but for $\lambda$: $\frac{x:{\tau }_1⊢e_2:{\tau }_2}{\lambda x:{\tau }_1.e_2:{\tau }_1\to {\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\left(v3\right)$[Tait]:

If $\Gamma ⊢e:\tau$ and $H{T}_{\Gamma }\left(\gamma \right)$, then $H{T}_{\tau }\left(\hat{\gamma }\right(e\left)\right)$

So $H{T}_{\Gamma }\left(\gamma \right)$ means that if $\Gamma =x_1:{\tau }_1,x_2:{\tau }_2,\dots ,x_n:{\tau }_n$, then $\gamma =x_1\hookrightarrow e_1,x_2\hookrightarrow e_2,\dots ,x_n\hookrightarrow x_n$ (substitution) such that $H{T}_{{\tau }_1}\left(e_1\right),\dots ,H{T}_{{\tau }_n}\left(e_n\right)$, and $\hat{\gamma }\left(e\right)$ means to do the substitution. So we are good now!