GaeBlogX Arista Networks, Software-Defined Networking

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 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: 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).

  1. Reflexivity

  2. Transitivity

  3. Weakening

  4. Contraction

  5. 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):

  1. $e$ itself can’t be a variable becasue it is closed
  2. 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 well-defined 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!


Similar Posts

上一篇 Garbage Collection

Comments

Search