Graded bases, temporal typing, and soft logic

Chapter 54: two graded bases

Linear Base has types $K$, $A⊸B$, and ${◻}_{r}A$, with linear assumptions $x:A$ and graded assumptions $x:[A{]}_r$. Context sum is partial: linear domains must be disjoint, while repeated graded assumptions have equal types and add grades. Its complete rule signature is

$x:A{⊢}_{\mathsf{L}}x:A$

$\mathrm{\Gamma },x:A{⊢}_{\mathsf{L}}t:B$

$\mathrm{\Gamma }{⊢}_{\mathsf{L}}\lambda x.t:A⊸B$

${\mathrm{\Gamma }}_1{⊢}_{\mathsf{L}}t:A⊸B$${\mathrm{\Gamma }}_2{⊢}_{\mathsf{L}}u:A$

${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2{⊢}_{\mathsf{L}}tu:B$

$\mathrm{\Gamma }{⊢}_{\mathsf{L}}t:A$${\mathrm{gr}}_0({\mathrm{\Gamma }}^{\prime })$

$\mathrm{\Gamma }+{\mathrm{\Gamma }}^{\prime }{⊢}_{\mathsf{L}}t:A$

$\mathrm{\Gamma },x:A{⊢}_{\mathsf{L}}t:B$

$\mathrm{\Gamma },x:[A{]}_1{⊢}_{\mathsf{L}}t:B$

$\mathrm{\Gamma }{⊢}_{\mathsf{L}}t:A$$\mathrm{gr}(\mathrm{\Gamma })$

$r\cdot \mathrm{\Gamma }{⊢}_{\mathsf{L}}[t]:{◻}_{r}A$

${\mathrm{\Gamma }}_1{⊢}_{\mathsf{L}}t:{◻}_{r}A$${\mathrm{\Gamma }}_2,x:[A{]}_r{⊢}_{\mathsf{L}}u:B$

${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2{⊢}_{\mathsf{L}}\mathsf{let}[x]=t\mathsf{in}u:B$

$\mathrm{\Gamma },x:[A{]}_r{⊢}_{\mathsf{L}}t:B$$r{⊑}_{\mathsf{q}}s$

$\mathrm{\Gamma },x:[A{]}_s{⊢}_{\mathsf{L}}t:B$

Its principal call-by-name steps are $(\lambda x.t)u{⟶}_{\mathsf{L}}t[u/x]$ and $\mathsf{let}[x]=[t]\mathsf{in}u{⟶}_{\mathsf{L}}u[t/x]$, with function- and scrutinee-position congruence.

Graded Base has $A\stackrel{r}{\to }B$ and only assumptions $x{:}_{r}A$. Its complete rules are

$x{:}_{1}A{⊢}_{\mathsf{G}}x:A$

$\mathrm{\Delta }{⊢}_{\mathsf{G}}t:A$

$\mathrm{\Delta },0\cdot {\mathrm{\Delta }}^{\prime }{⊢}_{\mathsf{G}}t:A$

$\mathrm{\Delta },x{:}_{r}A{⊢}_{\mathsf{G}}t:B$$r{⊑}_{\mathsf{q}}s$

$\mathrm{\Delta },x{:}_{s}A{⊢}_{\mathsf{G}}t:B$

$\mathrm{\Delta },x{:}_{r}A{⊢}_{\mathsf{G}}t:B$

$\mathrm{\Delta }{⊢}_{\mathsf{G}}\lambda x.t:A\stackrel{r}{\to }B$

${\mathrm{\Delta }}_1{⊢}_{\mathsf{G}}t:A\stackrel{r}{\to }B$${\mathrm{\Delta }}_2{⊢}_{\mathsf{G}}u:A$

${\mathrm{\Delta }}_1+r\cdot {\mathrm{\Delta }}_2{⊢}_{\mathsf{G}}tu:B$

Its principal step is $(\lambda x.t)u{⟶}_{\mathsf{G}}t[u/x]$, and graded substitution concludes $\mathrm{\Delta }+r\cdot \mathrm{\Theta }{⊢}_{\mathsf{G}}t[u/x]:B$.

The direct translation sends $A\stackrel{r}{\to }B$ to ${◻}_r\mathcal{L}[[A]]⊸\mathcal{L}[[B]]$, boxes every argument, and unboxes at every abstraction. The reverse CPS translation sends ${◻}_{r}A$ to $(\mathcal{G}[[A]]\stackrel{r}{\to }K)\stackrel{1}{\to }K$.

The separate combined effect–coeffect calculus has $A::=o\mid A\to B\mid T_{e}A\mid D_{r}A$. Context sum repeats only discharged assumptions, adding their coeffect grades; $r\ast [\mathrm{\Gamma }]$ scales a fully discharged context. Its complete typing rules are

$x:A⊢x:A$

$\mathrm{\Gamma }⊢t:A$

${\mathrm{\Gamma }}^{\prime },[\mathrm{\Delta }{]}_0⊢t:B$

$\mathrm{\Gamma },x:A⊢t:B$

$\mathrm{\Gamma }⊢\lambda x.t:A\to B$

$\mathrm{\Gamma }⊢t:A\to B$$\mathrm{\Delta }⊢u:A$

$\mathrm{\Gamma }+\mathrm{\Delta }⊢tu:B$

$\mathrm{\Gamma }⊢t:A$

$\mathrm{\Gamma }⊢⟨t⟩:T_{1}A$

$\mathrm{\Gamma }⊢t_1:T_{e}A$$\mathrm{\Delta },x:A⊢t_2:T_{f}B$

$\mathrm{\Gamma }+\mathrm{\Delta }⊢\mathsf{let}⟨x⟩=t_1\mathsf{in}{t}_2:T_{e\bullet f}B$

$\mathrm{\Gamma },x:A⊢t:B$

$\mathrm{\Gamma },x:[A{]}_1⊢t:B$

$[\mathrm{\Gamma }]⊢t:B$

$r\ast [\mathrm{\Gamma }]⊢[t]:D_{r}B$

$\mathrm{\Gamma }⊢t_1:D_{r}A$$\mathrm{\Delta },x:[A{]}_r⊢t_2:B$

$\mathrm{\Gamma }+\mathrm{\Delta }⊢\mathsf{let}[x]=t_1\mathsf{in}{t}_2:B$

$⊢{\mathsf{dist}}_{r,e}^{\varphi }:F_{r,e}^{\varphi }A\to G_{r,e}^{\varphi }A$

$⊢\mathsf{op}:A_{\mathsf{op}}$

Subtyping is generated by reflexivity, arrow variance, pointwise context variance, and Linear substitution replaces $x:A$ and adds the substituted context; coeffectful substitution replaces $x:[A{]}_r$ and adds $r\ast [\mathrm{\Delta }]$.

Chapter 55: Simply RaTT

Contexts contain assumptions, one optional lock $▸$, and one optional tick $✓$, with the tick to the right of the lock. Its complete chapter rule card is

$\mathrm{tokenFree}({\mathrm{\Gamma }}^{\prime })$

$\mathrm{\Gamma },x:A,{\mathrm{\Gamma }}^{\prime }⊢x:A$

$\mathrm{\Gamma },x:A⊢t:B$$\mathrm{tickFree}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢\lambda x.t:A\to B$

$\mathrm{\Gamma }⊢t:A\to B$$\mathrm{\Gamma }⊢u:A$

$\mathrm{\Gamma }⊢tu:B$

$\mathrm{\Gamma },✓⊢t:A$

$\mathrm{\Gamma }⊢\mathsf{delay}t:◯A$

$\mathrm{\Gamma }⊢t:◯A$$\mathrm{\Gamma },✓,{\mathrm{\Gamma }}^{\prime }\mathsf{ctx}$

$\mathrm{\Gamma },✓,{\mathrm{\Gamma }}^{\prime }⊢\mathsf{adv}t:A$

$\mathrm{\Gamma },▸⊢t:A$

$\mathrm{\Gamma }⊢\mathsf{box}t:◻A$

${\mathrm{\Gamma }}^{\prime }⊢t:◻A$$\mathrm{tokenFree}({\mathrm{\Gamma }}^{″})$

${\mathrm{\Gamma }}^{\prime },▸,{\mathrm{\Gamma }}^{″}⊢\mathsf{unbox}t:A$

$\mathrm{\Gamma }⊢t:A$$A\mathsf{stable}$$\mathrm{\Gamma },✓,{\mathrm{\Gamma }}^{\prime }\mathsf{ctx}$

$\mathrm{\Gamma },✓,{\mathrm{\Gamma }}^{\prime }⊢\mathsf{progress}t:A$

$\mathrm{\Gamma }⊢t:A$$A\mathsf{stable}$$\mathrm{\Gamma },▸,{\mathrm{\Gamma }}^{\prime }\mathsf{ctx}$

$\mathrm{\Gamma },▸,{\mathrm{\Gamma }}^{\prime }⊢\mathsf{promote}t:A$

$\mathrm{\Gamma },▸,x:◯A⊢t:A$

$\mathrm{\Gamma }⊢\mathsf{fix}x.t:◻A$

Stable types are generated by unit, naturals, boxed types, products, and sums.

The source-gated temporal-resource calculus uses $\mathrm{\Gamma }⊢V:X$ and $\mathrm{\Gamma }⊢M:X!\tau$. Its four temporal typing rules are

$\mathrm{\Gamma }⊢M:X!\tau$$\mathrm{\Gamma },⟨\tau ⟩,x:X⊢N:Y!{\tau }^{\prime }$

$\mathrm{\Gamma }⊢\mathsf{let}x=M\mathsf{in}N:Y!(\tau +{\tau }^{\prime })$

$\mathrm{\Gamma },⟨\tau ⟩⊢M:X!{\tau }^{\prime }$

$\mathrm{\Gamma }⊢\mathsf{delay}\tau M:X!(\tau +{\tau }^{\prime })$

$\mathrm{\Gamma },⟨\tau ⟩⊢V:X$$\mathrm{\Gamma },x:[\tau ]X⊢N:Y!{\tau }^{\prime }$

$\mathrm{\Gamma }⊢{\mathsf{box}}_{[\tau ]}V\mathsf{as}x\mathsf{in}N:Y!{\tau }^{\prime }$

$\tau \le {\tau }_{\mathrm{\Gamma }}$$\mathrm{\Gamma }-\tau ⊢V:[\tau ]X$$\mathrm{\Gamma },x:X⊢N:Y!{\tau }^{\prime }$

$\mathrm{\Gamma }⊢{\mathsf{unbox}}_{[\tau ]}V\mathsf{as}x\mathsf{in}N:Y!{\tau }^{\prime }$

Its state rules for delay, box, and unbox are the three transitions printed in section 55.6; ordinary application, matching, let, operations, and handlers use the paper’s fine-grain call-by-value rules.

Chapter 56: SLL2

The non-exponential ${\mathsf{ILL}}_2$ rules retained by SLL2 are

$A⊢A$

$\mathrm{\Gamma }⊢A$$\mathrm{\Delta },A⊢C$

$\mathrm{\Gamma },\mathrm{\Delta }⊢C$

$\mathrm{\Gamma },A,B,\mathrm{\Delta }⊢C$

$\mathrm{\Gamma },B,A,\mathrm{\Delta }⊢C$

$\mathrm{\Gamma },A⊢B$

$\mathrm{\Gamma }⊢A⊸B$

$\mathrm{\Gamma }⊢A$$\mathrm{\Delta },B⊢C$

$\mathrm{\Gamma },\mathrm{\Delta },A⊸B⊢C$

$\mathrm{\Gamma }⊢A$$\mathrm{\Delta }⊢B$

$\mathrm{\Gamma },\mathrm{\Delta }⊢A\otimes B$

$\mathrm{\Gamma },A,B⊢C$

$\mathrm{\Gamma },A\otimes B⊢C$

$\cdot ⊢1$

$\mathrm{\Gamma }⊢C$

$\mathrm{\Gamma },1⊢C$

$\mathrm{\Gamma }⊢A$$\mathrm{\Gamma }⊢B$

$\mathrm{\Gamma },A⊢C$

$\mathrm{\Gamma },B⊢C$

$\mathrm{\Gamma }⊢A$$\alpha \notin \mathrm{fv}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢\mathrm{\forall }\alpha .A$

$\mathrm{\Gamma },A[B/\alpha ]⊢C$

$\mathrm{\Gamma },\mathrm{\forall }\alpha .A⊢C$

SLL2 replaces the ordinary exponential rules by exactly

$A_1,\dots ,A_m⊢B$

$!A_1,\dots ,!A_m⊢!B$

$\mathrm{\Gamma },\underset{n}{{\displaystyle \underbrace{A,\dots ,A}}}⊢C$

$\mathrm{\Gamma },!A⊢C$

There is no digging. Proof-net weight is defined by atomic right cells of weight $1$, left cells and multiplexors of weight $0$, and For a rank-$n$ net, every external reduction strictly decreases $W_u(n)$.