If we typechecked correctly, $omega_1$ and $omega_2$ would be disjoint as well.
*Soundness.* If $Gamma tack.r e : A tack.l Omega$ then $Omega tack.r e : A$ ($Omega subset Gamma$)
*Completeness.* If $Omega tack.r e : A$ and $Gamma supset Omega$ then $Gamma tack.r e : A tack.l Omega$
The $Omega tack.r e : A$ is a _precise_ judgement: $Omega$ _only_ contains the variables used in $e$.
You would need two different sets of typing rules, one that has the $Omega$ rules and one that doesn't.
Prove this by rule induction.
Change the original theorem:
*New Theorem.*
Under the conditions $Gamma tack.r e : A tack.l Omega$ and $eta : Gamma$ and $omega : Omega$,
then $eta tack.r e arrow.r.hook v tack.l omega$ and $dot tack.r v : A$.
This can now be proven with the new dynamics.
How to prove that there's no garbage?
For all top level computations, $eta tack.r e arrow.r.hook v tack.l eta$.
This means that everything is used.
This can be proven using rule induction.
Updated theorem, to point out that $e arrow.r.hook v$ may not necessarily be true because termination is not proven by rule induction.
*New Theorem.*
Under the conditions $Gamma tack.r e : A tack.l Omega$ and $eta : Gamma$ and $omega : Omega$,
#n[and $eta tack.r e arrow.r.hook v tack.l omega$] then $dot tack.r v : A$.
(under affine logic, the top-level judgment $Gamma tack.r e : A tack.l Omega$ requires only that $Omega subset Gamma$, not that $Omega = Gamma$)
Example of evaluation rule that matches the typing rule:
#tree(
axi[$eta tack.r e arrow.r.hook (v_1, v_2) tack.l omega$],
axi[$eta, x mapsto v_1 , y mapsto v_2 tack.r e' arrow.r.hook v' tack.l (omega', x mapsto v_1, y mapsto v_2)$],
bin[$eta tack.r "match" e "with" (x, y) arrow.r.double e' arrow.r.hook v' tack.l (omega, omega')$]
)
=== Looking at typing rules as logic
#rect[Natural Deduction]
$Gamma ::= (dot) | Gamma , A$
#tree(
axi[],
uni[$A tack.r A$]
)
#tree(
axi[$Delta tack.r A$],
axi[$Gamma tack.r B$],
bin[$Delta, Gamma, tack.r A times B$]
)
#tree(
axi[$Delta tack.r A times B$],
axi[$Gamma, A, B tack.r C$],
bin[$Delta, Gamma tack.r C$]
)
These are like a rule of logic. For plus:
#tree(
axi[$Delta tack.r A$],
uni[$Delta tack.r A + B$],
)
#tree(
axi[$Delta tack.r B$],
uni[$Delta tack.r A + B$],
)
Proof by cases:
#tree(
axi[$Delta tack.r A + B$],
axi[$Gamma , A tack.r C$],
axi[$Gamma , B tack.r C$],
tri[$Delta , Gamma tack.r C$],
)
Every assumption has to be used _exactly_ once. This is called *linear logic*.
(notation uses $times.circle$ and $plus.circle$ instead of $times$ and $plus$)
Linear logic is weak by itself, just as linear type system is weak without global definitions.
Summary of operators:
#image("lec1.jpg")
$!A$ is read "of course A", lets you re-use assumptions. We don't have this except by top-level definitions.
In the judgement $Sigma ; Gamma tack.r e : A$, $Sigma$ contains definitions that you can use however many times you want, and $Gamma$ contains the definitions that are created linearly.
Distinction between positive and negative types:
- Lambdas cannot be pattern-matched against, you have to apply it.
- However, for $times.circle$ and $plus.circle$ you can directly observe their structure.
In this case, $A with B$, read "A with B":
#tree(
axi[$Gamma tack.r A$],
axi[$Gamma tack.r B$],
bin[$Gamma tack.r A with B$],
)
This is sound because only one of them can be extracted:
#tree(
axi[$Gamma tack.r e_1:A$],
axi[$Gamma tack.r e_2:B$],
bin[$Gamma tack.r angle.l e_1,e_2 angle.r : A with B$],
)
#tree(
axi[$Gamma tack.r e : A with B$],
uni[$Gamma tack.r e.pi_1 : A$]
)
#tree(
axi[$Gamma tack.r e : A with B$],
uni[$Gamma tack.r e.pi_2 : B$]
)
"Lazy pair" you can only extract one side at a time. There are also "lazy records":
$with { l : A_l}_(l in L)$
#tree(
axi[$Gamma tack.r e_l : A_l (forall l in L)$],
uni[$Gamma tack.r {l = e_l}_(l in L) : with {l : A_l}_(l in L)$]
)
#tree(
axi[$Gamma tack.r e : with { l : A_l}_(l in L) (forall l in L)$],
