linearity.txt

Γ ⊢ e : A ⊣ Γ'
Γ' ⇓ Γ ↝ Γ''
Γ'' ⊢ e' : A ⊣ Δ
————————————————————
Γ ⊢ e || e' : A ⊣ Δ


Δ ⊢ e : A+B ⊣ Γ₀
Γ₀, x:A ⊢ e₁ : C ⊣ Γ₁, x:A, Γ'
Γ₀ ⇓ Γ₁ ↝ Γ₂
Γ₂, y:B ⊢ e₂ : C ⊣ Δ', y:B, Γ''
Δ' ∼ Γ₁ 
————————————————————————————————
Δ ⊢ case(e, x.e₁, y.e₂) : C ⊢ Δ'



Γ ::= · | Γ, α̂ | Γ, α̂=A | Γ, x:A | Γ, x∼A[+] | Γ, x∼A[-]

The judgment's invariant is that the set of term variables is the
same, but (1) more type variables may be introduced, and (2) evars may
get values, and (3) linear variables may go from + to - 


Γ, β̂, γ̂, α̂ =̱ β̂ → γ̂, Γ', x:α̂ ⊢ e ⇐ β̂ ⊣ Γ'', x:α̂, Γ'''
————————————————————————————————————————————————————
        Γ, α̂, Γ' ⊢ λx.e ⇐ α̂ ⊣ Γ''

To merge contexts:

Γ ⇓ Γ' ↝ Γ''
———————————————————————————————————
Γ, x∼A[±] ⇓ Γ', x∼A[_] ↝ Γ'', x∼A[±]


Γ ⇓ Γ' ↝ Γ''
———————————————————————————
Γ, x:A ⇓ Γ', x:A ↝ Γ'', x:A


Γ ⇓ Γ' ↝ Γ''
———————————————
Γ, α̂ ⇓ Γ' ↝ Γ''


Γ ⇓ Γ' ↝ Γ''
———————————————————
Γ ⇓ Γ', α̂ ↝ Γ'', α̂ 


Γ ⇓ Γ' ↝ Γ''
———————————————
Γ, α̂ ⇓ Γ' ↝ Γ''


Γ ⇓ Γ' ↝ Γ''
—————————————————
Γ, α̂=A ⇓ Γ' ↝ Γ''


Γ ⇓ Γ' ↝ Γ''
——————————————————————
Γ ⇓ Γ', α̂=A ↝ Γ'', α̂=A


When two contexts are resource-compatible?

Γ ∼ Δ


Γ ∼ Δ 
—————————————————————
Γ, x∼A[+] ∼ Δ, x∼A[+] 


Γ ∼ Δ 
—————————————————————
Γ, x∼A[-] ∼ Δ, x∼A[-] 


Γ ∼ Δ 
———————————————
Γ, x:A ∼ Δ, x:A 


Γ ∼ Δ 
—————————
Γ, α̂ ∼ Δ 


Γ ∼ Δ 
————————
Γ ∼ Δ, α̂ 


Γ ∼ Δ 
————————
Γ, α̂ ∼ Δ 


Γ ∼ Δ 
——————————
Γ, α̂=A ∼ Δ 


Γ ∼ Δ 
——————————
Γ ∼ Δ, α̂=A