Modular, linear, quantitative, and graded dependent systems

The $\lambda \mathrm{\Pi }$-calculus modulo rewriting

The frozen framework rules are

$x:A\in \mathrm{\Gamma }$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢x:A$

$c:A\in \mathrm{\Sigma }$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢c:A$

$\mathrm{\Sigma };\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢\mathsf{Type}:\mathsf{Kind}$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢A:\mathsf{Type}$$\mathrm{\Sigma };\mathrm{\Gamma },x:A⊢B:s$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢\prod _{x:A}B:s$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢A:\mathsf{Type}$$\mathrm{\Sigma };\mathrm{\Gamma },x:A⊢t:B$$B\ne \mathsf{Kind}$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢\lambda x:A.t:\prod _{x:A}B$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢f:\prod _{x:A}B$$\mathrm{\Sigma };\mathrm{\Gamma }⊢u:A$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢fu:B[u/x]$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢t:A$$A{\equiv }_{\beta \mathrm{\Sigma }}B$$\mathrm{\Sigma };\mathrm{\Gamma }⊢B:s$

$\mathrm{\Sigma };\mathrm{\Gamma }⊢t:B$

$\ell ⟼r\in \mathrm{\Sigma }$$\theta :\mathrm{dom}(\mathrm{\Delta })\to \mathsf{Term}$

$C[\ell \theta ]{⟶}_{\mathrm{\Sigma }}C[r\theta ]$

$C[(\lambda x:A.t)u]{⟶}_{\beta }C[t[u/x]]$

For Mod-Rewrite, the declaration card also requires a constant-headed, lambda-free, left-linear, algebraic left side, exactly the variables of $\mathrm{\Delta }$, and $\mathrm{\Sigma };\mathrm{\Delta }⊢\ell :T$ together with $\mathrm{\Sigma };\mathrm{\Delta }⊢r:T$. Both reductions are raw and compatible under capture-avoiding one-hole contexts; typing enters only through subject reduction.

Linear dependent type theory

Formation sees only the shape of a state-bearing argument:

$\mathrm{\Phi },x:\mathrm{Sh}(A)⊢B[x]:\ast$

$\mathrm{\Phi }⊢(x:A)⊸B[x]:\ast$

$\mathrm{\Phi },x:\mathrm{Sh}(A)⊢B[x]:\ast$

$\mathrm{\Phi }⊢(x:A)\otimes B[x]:\ast$

$\mathrm{\Phi },x:P_1⊢P_2[x]:\ast$

$\mathrm{\Phi }⊢(x:P_1)\to P_2[x]:\ast$

$\mathrm{\Phi }⊢A:\ast$

$\mathrm{\Phi }⊢!A:\ast$

The term rules that expose resource splitting are

$0\mathrm{\Gamma },x{:}_{1}A,0{\mathrm{\Gamma }}^{\prime }\mathsf{ctx}$

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

$\mathrm{\Gamma },x{:}_{k}A⊢M:B[x]$$k\ne 1\Rightarrow A=P$

$\mathrm{\Gamma }⊢\lambda x.M:(x:A)⊸B[x]$

${\mathrm{\Gamma }}_1⊢M:(x:A)⊸B[x]$${\mathrm{\Gamma }}_2⊢N:A$

${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2⊢MN:B[\mathrm{Sh}(N)]$

${\mathrm{\Gamma }}_1⊢M:A$${\mathrm{\Gamma }}_2⊢N:B[\mathrm{Sh}(M)]$

${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2⊢(M,N):(x:A)\otimes B[x]$

${\mathrm{\Gamma }}_1⊢M:(x:A)\otimes B[x]$${\mathrm{\Gamma }}_2,x{:}_{k_1}A,y{:}_{k_2}B[x]⊢N:C$$k_1=0\Rightarrow A=P_1$$k_2=0\Rightarrow B[x]=P_2[x]$

${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2⊢\mathsf{let}(x,y)=M\mathsf{in}N:C$

$\mathrm{\Phi }⊢M:A$

$\mathrm{\Phi }⊢\mathsf{lift}M:!A$

$\mathrm{\Gamma }⊢M:!A$

$\mathrm{\Gamma }⊢\mathsf{force}M:A$

$\mathrm{\Phi },x:P_1⊢R:P_2[x]$

$\mathrm{\Phi }⊢{\lambda }^{\prime }x.R:(x:P_1)\to P_2[x]$

$\mathrm{\Phi }⊢R_1:(x:P_1)\to P_2[x]$$\mathrm{\Phi }⊢R_2:P_1$

$\mathrm{\Phi }⊢R_1@R_2:P_2[R_2/x]$

$\mathrm{\Phi }⊢R:!A$

$\mathrm{\Phi }⊢{\mathsf{force}}^{\prime }R:\mathrm{Sh}(A)$

The evaluation and semantic-conversion roots are

$M\Downarrow \lambda x.M^{\prime }$$N\Downarrow V$$M^{\prime }[V/x]\Downarrow W$

$MN\Downarrow W$

$M\Downarrow (V_1,V_2)$$N[V_1/x,V_2/y]\Downarrow W$

$\mathsf{let}(x,y)=M\mathsf{in}N\Downarrow W$

$\mathrm{\Gamma }⊢M:A[R]$$R{\equiv }_{\mathrm{ev}}{R}^{\prime }$

$\mathrm{\Gamma }⊢M:A[R^{\prime }]$

Quantitative dependent type theory

For the selected semiring, the variable rule and the dependent function and tensor rules are

$0\mathrm{\Gamma },x{:}^{\sigma }S,0{\mathrm{\Gamma }}^{\prime }⊢$

$0\mathrm{\Gamma },x{:}^{\sigma }S,0{\mathrm{\Gamma }}^{\prime }⊢x{:}^{\sigma }S$

where $\sigma \in \{0,1\}$, followed by

$0\mathrm{\Gamma }⊢S$$0\mathrm{\Gamma },x{:}^{0}S⊢T$

$0\mathrm{\Gamma }⊢(x{:}^{\pi }S)\to T$

$\mathrm{\Gamma },x{:}^{\sigma \pi }S⊢M{:}^{\sigma }T$

$\mathrm{\Gamma }⊢\lambda x.M{:}^{\sigma }(x{:}^{\pi }S)\to T$

${\mathrm{\Gamma }}_1⊢M{:}^{\sigma }(x{:}^{\pi }S)\to T$${\mathrm{\Gamma }}_2⊢N{:}^{{\sigma }^{\prime }}S$${\sigma }^{\prime }=0⟺(\pi =0\text{ or }\sigma =0)$

${\mathrm{\Gamma }}_1+\pi {\mathrm{\Gamma }}_2⊢MN{:}^{\sigma }T[N/x]$

$0\mathrm{\Gamma }⊢S$$0\mathrm{\Gamma },x{:}^{0}S⊢T$

$0\mathrm{\Gamma }⊢(x{:}^{\pi }S)\otimes T$

${\mathrm{\Gamma }}_1⊢M{:}^{{\sigma }^{\prime }}S$${\mathrm{\Gamma }}_2⊢N{:}^{\sigma }T[M/x]$${\sigma }^{\prime }=0⟺(\pi =0\text{ or }\sigma =0)$

$\pi {\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2⊢(M,N){:}^{\sigma }(x{:}^{\pi }S)\otimes T$

$0{\mathrm{\Gamma }}_1,z{:}^0((x{:}^{\pi }S)\otimes T)⊢U$${\mathrm{\Gamma }}_1⊢P{:}^{\sigma }(x{:}^{\pi }S)\otimes T$${\mathrm{\Gamma }}_2,x{:}^{\sigma \pi }S,y{:}^{\sigma }T⊢N{:}^{\sigma }U[(x,y)/z]$$0{\mathrm{\Gamma }}_1=0{\mathrm{\Gamma }}_2$

${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2⊢\mathsf{let}(x,y)=P\mathsf{in}N{:}^{\sigma }U[P/z]$

Graded modal dependent type theory

The universe and variable roots are

$\mathrm{\Delta }\odot \mathrm{\Gamma }⊢$

$(\mathrm{\Delta }\mid 0\mid 0)\odot \mathrm{\Gamma }⊢{\mathsf{Type}}_l:{\mathsf{Type}}_{\mathsf{suc}l}$

${\mathrm{\Delta }}_1,\sigma ,{\mathrm{\Delta }}_2\odot {\mathrm{\Gamma }}_1,x:A,{\mathrm{\Gamma }}_2⊢$$|{\mathrm{\Delta }}_1|=|{\mathrm{\Gamma }}_1|$

$({\mathrm{\Delta }}_1,\sigma ,{\mathrm{\Delta }}_2\mid 0^{|{\mathrm{\Delta }}_1|},1,0\mid \sigma ,0,0)\odot {\mathrm{\Gamma }}_1,x:A,{\mathrm{\Gamma }}_2⊢x:A$

The exact function rules used in the chapter are

$(\mathrm{\Delta }\mid {\sigma }_1\mid 0)\odot \mathrm{\Gamma }⊢A:{\mathsf{Type}}_{l_1}$$(\mathrm{\Delta },{\sigma }_1\mid {\sigma }_2,r\mid 0)\odot \mathrm{\Gamma },x:A⊢B:{\mathsf{Type}}_{l_2}$

$(\mathrm{\Delta }\mid {\sigma }_1+{\sigma }_2\mid 0)\odot \mathrm{\Gamma }⊢(x{:}_{(s,r)}A)\to B:{\mathsf{Type}}_{l_1\bigsqcup l_2}$

$(\mathrm{\Delta },{\sigma }_1\mid {\sigma }_3,r\mid 0)\odot \mathrm{\Gamma },x:A⊢B:{\mathsf{Type}}_l$$(\mathrm{\Delta },{\sigma }_1\mid {\sigma }_2,s\mid {\sigma }_3,r)\odot \mathrm{\Gamma },x:A⊢t:B$

$(\mathrm{\Delta }\mid {\sigma }_2\mid {\sigma }_1+{\sigma }_3)\odot \mathrm{\Gamma }⊢\lambda x.t:(x{:}_{(s,r)}A)\to B$

$(\mathrm{\Delta },{\sigma }_1\mid {\sigma }_3,r\mid 0)\odot \mathrm{\Gamma },x:A⊢B:{\mathsf{Type}}_l$$(\mathrm{\Delta }\mid {\sigma }_2\mid {\sigma }_1+{\sigma }_3)\odot \mathrm{\Gamma }⊢f:(x{:}_{(s,r)}A)\to B$$(\mathrm{\Delta }\mid {\sigma }_4\mid {\sigma }_1)\odot \mathrm{\Gamma }⊢u:A$

$(\mathrm{\Delta }\mid {\sigma }_2+s{\sigma }_4\mid {\sigma }_3+r{\sigma }_4)\odot \mathrm{\Gamma }⊢fu:B[u/x]$

The dependent tensor rules are

$(\mathrm{\Delta }\mid {\sigma }_1\mid 0)\odot \mathrm{\Gamma }⊢A:{\mathsf{Type}}_l$$(\mathrm{\Delta },{\sigma }_1\mid {\sigma }_2,r\mid 0)\odot \mathrm{\Gamma },x:A⊢B:{\mathsf{Type}}_l$

$(\mathrm{\Delta }\mid {\sigma }_1+{\sigma }_2\mid 0)\odot \mathrm{\Gamma }⊢(x{:}_{r}A)\otimes B:{\mathsf{Type}}_l$

$(\mathrm{\Delta },{\sigma }_1\mid {\sigma }_3,r\mid 0)\odot \mathrm{\Gamma },x:A⊢B:{\mathsf{Type}}_l$$(\mathrm{\Delta }\mid {\sigma }_2\mid {\sigma }_1)\odot \mathrm{\Gamma }⊢t_1:A$$(\mathrm{\Delta }\mid {\sigma }_4\mid {\sigma }_3+r{\sigma }_2)\odot \mathrm{\Gamma }⊢t_2:B[t_1/x]$

$(\mathrm{\Delta }\mid {\sigma }_2+{\sigma }_4\mid {\sigma }_1+{\sigma }_3)\odot \mathrm{\Gamma }⊢(t_1,t_2):(x{:}_{r}A)\otimes B$

$(\mathrm{\Delta }\mid {\sigma }_3\mid {\sigma }_1+{\sigma }_2)\odot \mathrm{\Gamma }⊢t_1:(x{:}_{r}A)\otimes B$$(\mathrm{\Delta },{\sigma }_1+{\sigma }_2\mid {\sigma }_5,r^{\prime }\mid 0)\odot \mathrm{\Gamma },z:(x{:}_{r}A)\otimes B⊢C:{\mathsf{Type}}_l$$(\mathrm{\Delta },{\sigma }_1,({\sigma }_2,r)\mid {\sigma }_4,s,s\mid {\sigma }_5,r^{\prime },r^{\prime })\odot \mathrm{\Gamma },x:A,y:B⊢t_2:C[(x,y)/z]$

$(\mathrm{\Delta }\mid {\sigma }_4+s{\sigma }_3\mid {\sigma }_5+r^{\prime }{\sigma }_3)\odot \mathrm{\Gamma }⊢\mathsf{let}(x,y)=t_1\mathsf{in}{t}_2:C[t_1/z]$

The modality rules are

$(\mathrm{\Delta }\mid \sigma \mid 0)\odot \mathrm{\Gamma }⊢A:{\mathsf{Type}}_l$

$(\mathrm{\Delta }\mid \sigma \mid 0)\odot \mathrm{\Gamma }⊢{◻}_{s}A:{\mathsf{Type}}_l$

$(\mathrm{\Delta }\mid {\sigma }_1\mid {\sigma }_2)\odot \mathrm{\Gamma }⊢t:A$

$(\mathrm{\Delta }\mid s{\sigma }_1\mid {\sigma }_2)\odot \mathrm{\Gamma }⊢\mathsf{box}t:{◻}_{s}A$

$(\mathrm{\Delta },{\sigma }_2\mid {\sigma }_4,r\mid 0)\odot \mathrm{\Gamma },z:{◻}_{s}A⊢B:{\mathsf{Type}}_l$$(\mathrm{\Delta }\mid {\sigma }_1\mid {\sigma }_2)\odot \mathrm{\Gamma }⊢t_1:{◻}_{s}A$$(\mathrm{\Delta },{\sigma }_2\mid {\sigma }_3,s\mid {\sigma }_4,sr)\odot \mathrm{\Gamma },x:A⊢t_2:B[\mathsf{box}x/z]$

$(\mathrm{\Delta }\mid {\sigma }_1+{\sigma }_3\mid {\sigma }_4+r{\sigma }_1)\odot \mathrm{\Gamma }⊢\mathsf{let}\mathsf{box}x=t_1\mathsf{in}{t}_2:B[t_1/z]$

The beta roots are $\mathsf{let}(x,y)=(t,u)\mathsf{in}v{⟶}_{\beta }v[t/x,u/y]$ and $\mathsf{let}\mathsf{box}x=\mathsf{box}t\mathsf{in}u{⟶}_{\beta }u[t/x]$. No tensor or box eta rule is imported. Appendix D records that the strong-normalization use is restricted to ${\mathrm{GrTT}}^{0,1}$.