Finite-graph Boolean semantic subtyping

The calculus ${\lambda }_{\mathsf{FG}}$ of chapter 9 has the finite type grammar $$A,B::=0\mid b\mid A\times B\mid A\to B\mid A\vee B\mid \mathrm{\neg }A,$$ with $1\equiv \mathrm{\neg }0$ and $A\wedge B\equiv \mathrm{\neg }(\mathrm{\neg }A\vee \mathrm{\neg }B)$. The relation $A\le B$ is semantic inclusion in the universal finite-graph domain of definition 9.5, definition 9.6; it is decided by the finite simulation procedure of definition 9.13. This appendix does not replace that semantic relation by a syntactic subtype table.

Runtime tests, terms, and values are Here $I=(A_1\to B_1;\dots ;A_n\to B_n)$ is nonempty. It is well shaped when $n=1$, or, for a multi-arrow interface, when no domain $A_i$ contains an arrow atom other than the universal function test $\mathsf{Fun}=0\to 1$. This is the exact side condition of T-Abs; “well shaped” is not the metatheoretic notion of an admissible rule. Evaluation is weak left-to-right call by value under $$E::=[]\mid (E,e)\mid (v,E)\mid {\pi }_{i}E\mid Ee\mid vE\mid \mathsf{caseType}E\mathsf{as}x\mathsf{in}U\Rightarrow e_1\mid e_2.$$ Its complete root table is

$({\lambda }^{I}x.e)v⟶e[v/x]$

$i\in \{1,2\}$

${\pi }_i(v_1,v_2)⟶v_i$

$v⊩U$

$\mathsf{caseType}v\mathsf{as}x\mathsf{in}U\Rightarrow e_{+}\mid e_{-}⟶e_{+}[v/x]$

$v⊮U$

$\mathsf{caseType}v\mathsf{as}x\mathsf{in}U\Rightarrow e_{+}\mid e_{-}⟶e_{-}[v/x]$

The structural test judgment is the following recursion on $U$: Thus $v⊮U$ is the decidable negation of the displayed recursion; it is not a second primitive judgment.

Write $F\circ S$ for the computable least application output of definition 9.22, and ${\mathrm{proj}}_i(P)$ for the computable least projection output of lemma 9.25. The ordinary rules are

$c\in B_b$

$\mathrm{\Gamma }⊢c:b$

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

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

$\mathrm{\Gamma }⊢e_1:A$$\mathrm{\Gamma }⊢e_2:B$

$\mathrm{\Gamma }⊢(e_1,e_2):A\times B$

$\mathrm{\Gamma }⊢e:A$$A\le B$

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

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

$\mathrm{\Gamma }⊢e:A\wedge B$

$\mathrm{\Gamma }⊢e:P$$P\le 1\times 1$

$\mathrm{\Gamma }⊢{\pi }_{i}e:{\mathrm{proj}}_i(P)$

$\mathrm{\Gamma },x:A_i⊢e:B_i(1\le i\le n)$

$\mathrm{\Gamma }⊢{\lambda }^{(A_1\to B_1;\dots ;A_n\to B_n)}x.e:{\displaystyle \underset{i=1}{\overset{n}{\bigwedge }}(A_i\to B_i)}$

$\mathrm{\Gamma }⊢e_1:F$$\mathrm{\Gamma }⊢e_2:S$$F\le S\to B$

$\mathrm{\Gamma }⊢e_1{e}_2:B$

The least-result form belongs to the fixed-annotation synthesizer, rather than replacing the preceding declarative rule:

${\mathrm{syn}}_{\mathrm{\Gamma }}(e_1)=F$${\mathrm{syn}}_{\mathrm{\Gamma }}(e_2)=S$$F\le 0\to 1$$F\le S\to 1$

${\mathrm{syn}}_{\mathrm{\Gamma }}(e_1{e}_2)=F\circ S$

The union introductions used in the prose are derived subsumption rules:

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

$\mathrm{\Gamma }⊢e:A\vee B$

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

$\mathrm{\Gamma }⊢e:A\vee B$

A typing judgment is formed only for a term well scoped by its context. The typecase rule makes the otherwise suppressible branch scope explicit:

$\mathrm{\Gamma }⊢e:S$$x\notin \mathrm{dom}(\mathrm{\Gamma })$$\mathrm{fv}(e_{+})\cup \mathrm{fv}(e_{-})\subseteq \mathrm{dom}(\mathrm{\Gamma })\cup \{x\}$$S\wedge U\not\simeq 0\Rightarrow \mathrm{\Gamma },x:S\wedge U⊢e_{+}:B_{+}$$S\wedge \mathrm{\neg }U\not\simeq 0\Rightarrow \mathrm{\Gamma },x:S\wedge \mathrm{\neg }U⊢e_{-}:B_{-}$$S\wedge U\simeq 0\Rightarrow B_{+}=0$$S\wedge \mathrm{\neg }U\simeq 0\Rightarrow B_{-}=0$

$\mathrm{\Gamma }⊢\mathsf{caseType}e\mathsf{as}x\mathsf{in}U\Rightarrow e_{+}\mid e_{-}:B_{+}\vee B_{-}$

The partial synthesizer ${\mathrm{syn}}_{\mathrm{\Gamma }}$ returns the basic tag for a constant, the context entry for a variable, the product of the two recursive results for a pair, and ${\mathrm{proj}}_i(P)$ for a projection when $P\le 1\times 1$. An abstraction checks every displayed interface premise and returns their intersection. Application checks $F\le 0\to 1$ and $F\le S\to 1$, then returns $F\circ S$. Typecase checks both scope premises, returns $0$ without typechecking an empty branch, recursively synthesizes each nonempty branch under its refined binder, and returns their union. Checking $e:A$ succeeds exactly when synthesis returns $S\le A$.