Dependent Intersections and Same-Subject Refinement

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

A dependent pair can store a program and a proof about that program, but its erasure still contains two components. Suppose a function $r$ already supports two interfaces. Packaging $r$ with a second copy or a certificate changes its runtime representation even though both interfaces describe the same untyped subject. The required type former must attach the second view without adding a runtime component.

The binder in $$x:A\cap B(x)$$ ranges over the subject inhabiting both $A$ and $B(x)$. It is not a path from $x$ to itself, a dependent pair, an object-oriented $\mathsf{Self}$ type, or a recursive DOT binder.

Erasure comes first

Two differently typed annotated terms can already denote one untyped term. For instance, if implicit abstraction is written ${\mathrm{\Lambda }}^{0}A.t$, then $$\mathrm{erase}({\mathrm{\Lambda }}^{0}A.\lambda x.x)=\lambda x.x=\mathrm{erase}(\lambda x.x).$$ The first term may have type ${\mathrm{\forall }}^{0}A:{\mathcal{U}}_0.A\to A$ and the second an ordinary instance $\mathsf{N}\to \mathsf{N}$. Equality of erasures is weaker than judgmental equality of typed expressions; it forgets annotations and implicit binders.

Let $u:{\mathrm{\forall }}^{0}A:{\mathcal{U}}_0.A\to A$ and $v:\mathsf{N}\to \mathsf{N}$ be the two identity annotations above. If $B(f)$ is the constant type $\mathsf{N}\to \mathsf{N}$, then

$\mathrm{\Gamma }⊢u:{\mathrm{\forall }}^{0}A:{\mathcal{U}}_0.A\to A$$\mathrm{\Gamma }⊢v:\mathsf{N}\to \mathsf{N}$$\mathrm{erase}(u){=}_{\beta \eta }\lambda x.x{=}_{\beta \eta }\mathrm{erase}(v)$

$\mathrm{\Gamma }⊢\mathsf{both}(u,v):f:({\mathrm{\forall }}^{0}A:{\mathcal{U}}_0.A\to A)\cap (\mathsf{N}\to \mathsf{N})$

is the required first derivation. Both projections erase to $\lambda x.x$.

The stuck case is equally important. If $z:x:A\cap B$ is a variable, neither $\mathsf{left}(z)$ nor $\mathsf{right}(z)$ contracts; the projections are neutral annotations. Their erasures are nevertheless the same variable $z$.

Why three neighboring formers fail

An ordinary intersection $A\cap C$ can express two views, but $C$ cannot mention the subject through a binder. A dependent sum $\sum _{x:A}B$ can express the dependency, but $\mathrm{erase}((a,b))=(\mathrm{erase}(a),\mathrm{erase}(b))$ contains two runtime components. A refinement $\{x:A\mid P(x)\}$ is same-representation only when $P$ is an erased logical predicate; it cannot in general attach a computational interface $B(x)$. Dependent intersection is determined by the conjunction of the two missing requirements: dependent second view and one erased subject.

Removing the last premise of DI-I admits $\mathsf{both}(\lambda x.x,\lambda x.0)$. Its first projection would erase to $\lambda x.x$ and its second to $\lambda x.0$, while the intersection itself has only one erasure. At least one projection equation would then be false.

Substitution preserves the shared subject

The binder in $B$ makes substitution the first nonformal metatheoretic case.

Proof of Lemma 93.3 — Erasure commutes with substitution

Proof. Proceed by structural induction on $e$. The variable and ordinary binder cases are the capture-avoiding substitution calculation. For the new introduction form, For either projection, apply the induction hypothesis to its argument. No other constructor changes erasure. ◻

Proof of Lemma 93.4 — Substitution

Proof. Induct on the typing derivation. In the DI-I case the induction hypotheses give $$\mathrm{\Gamma },\mathrm{\Delta }[u/x]⊢a[u/x]:A[u/x],\mathrm{\Gamma },\mathrm{\Delta }[u/x]⊢b[u/x]:B[a/x][u/x].$$ Choose bound names outside $\mathrm{FV}(u)\cup \mathrm{FV}(A)\cup \mathrm{FV}(B)$ before commuting the two substitutions. The old side condition and lemma 93.3 give Rule DI-I then reconstructs the conclusion. In the DI-E${}_2$ case, the induction hypothesis gives the substituted intersection premise, and capture avoidance gives $B[\mathsf{left}(d)/y][u/x]=B[u/x][\mathsf{left}(d[u/x])/y]$. The remaining cases are instances of the base substitution proof with the same substitution. ◻

Proof of Theorem 93.5 — Erasure preservation

Proof. Induct on the reduction context. Ordinary beta reduction maps to untyped beta reduction by lemma 93.3. At the first new redex, $$\mathrm{erase}(\mathsf{left}(\mathsf{both}(a,b)))=\mathrm{erase}(a)=\mathrm{erase}(a).$$ At the second, $$\mathrm{erase}(\mathsf{right}(\mathsf{both}(a,b)))=\mathrm{erase}(a){=}_{\beta \eta }\mathrm{erase}(b),$$ where the final step is precisely the premise of DI-I. Compatible contexts preserve beta-eta convertibility. ◻

The PER validates one subject

Let $R_A$ be the PER interpreting $A$. For each $R_A$-related pair $a,a^{\prime }$, let $R_B^{a,a^{\prime }}$ interpret $B$ and be invariant under the $R_A$ equivalence class. The dependent-intersection PER is $$R_{x:A\cap B}(t,t^{\prime })⟺R_A(t,t^{\prime })\wedge R_B^{t,t^{\prime }}(t,t^{\prime }).$$ The same programs $t,t^{\prime }$ occur in both conjuncts. A Sigma interpretation would instead relate two pairs and project different components.

Proof of Theorem 93.6 — Kopylov semantic validation

Proof. Formation follows because $R_A$ is a PER and the functional-family premise makes the second conjunct independent of representatives. Symmetry of equation 93.1 uses symmetry of $R_A$ and $R_B^{t,t^{\prime }}$; transitivity uses their transitivity after replacing the middle representative by functionality. Introduction supplies both conjuncts for the same erased subject. The first elimination selects the $R_A$ conjunct. The second selects $R_B^{t,t^{\prime }}$ after the first view fixes the subject substituted for $x$. The computation rules do not change the subject, and extensional type equality follows by logical equivalence of both conjuncts under equal domain PERs and equal functional families. ◻

This theorem is the semantic Theorem 10 singled out by Kopylov. The paper reports MetaPRL checks for the remaining formal results, not for this semantic argument. The surrounding Nuprl calculus admits partial computations, so the theorem is not a normalization proof.

No annotation-normalization theorem follows merely by choosing a strongly normalizing erased target. A source step may contract an implicit binder, ascription, proof annotation, or a redex inside an erased view while inducing no target step. A normalization argument would therefore need the complete source reduction relation and a measure for every zero-erasure constructor; the frozen Kopylov signature supplies neither. Adding an untyped fixed point also leaves theorem 93.6 meaningful for partial terms. The chapter consequently makes no source- or annotation-normalization claim.

A dependent record with no wrapper

Fix labels $\mathsf{car}$ and $\mathsf{mul}$. A single-field record type is $\{\ell :A\}:=\{\ell \}\to A$, and a record is a function on labels. Define $$\mathsf{SemigroupSig}:=r:\{\mathsf{car}:{\mathcal{U}}_0\}\cap \{\mathsf{mul}:r.\mathsf{car}\to r.\mathsf{car}\to r.\mathsf{car}\}.$$ Let $s$ be the untyped label function whose $\mathsf{car}$ branch returns $\mathsf{N}$ and whose $\mathsf{mul}$ branch returns addition. Give it two annotations: $$s_c:\{\mathsf{car}:{\mathcal{U}}_0\},s_m:\{\mathsf{mul}:s_c.\mathsf{car}\to s_c.\mathsf{car}\to s_c.\mathsf{car}\}.$$ Both erase to $s$, so $\mathsf{both}(s_c,s_m)$ inhabits $\mathsf{SemigroupSig}$. The second field type computes after the first view: $$s_c.\mathsf{car}\equiv \mathsf{N},s_m.\mathsf{mul}:\mathsf{N}\to \mathsf{N}\to \mathsf{N}.$$ Both record projections erase to the same label function $s$; field selection chooses a branch, but dependent intersection itself inserts no pair or wrapper.

Associativity can be attached by one more dependent intersection whose second view is the set of the same record functions satisfying the associativity proposition. The runtime program remains $s$. A Sigma encoding would instead store $(s,p)$.

The terminology firewall

No row licenses a rule from another. In particular, dependent intersection does not permit $B$ to mention the function whose type is being formed unless that function is already the subject supplied by the left view.

Suggested first pass.

Begin with exercise 93.4, then complete exercise 93.6.

Exercise 93.4¶

★★☆ Prove, from equation 93.1, the extensional equality $$x:A\cap (y:B(x)\cap C(x,y))=z:(x:A\cap B(x))\cap C(z,z).$$ Expand membership on both sides until each is the conjunction of three PER relations on the same subject. Check the functionality premise used when a representative changes.

Referenced from 4 locations

• Dependent Intersections and Same-Subject Refinement
• ch:dependent-intersections: dependent intersections

Exercise 93.5¶

★★★ Reconstruct the DI-I and DI-E${}_2$ cases of semantic validation and the corresponding substitution cases. Then remove functionality of the PER family and give related representatives for which the second conjunct changes.

Referenced from 3 locations

• Dependent Intersections and Same-Subject Refinement
• ch:dependent-intersections: dependent intersections

Exercise 93.6¶

★★★ Practical project.dependent-intersection-erasure-checker Implement in Kappa a finite checker whose erasure grammar distinguishes identity, constant, and record shapes and whose annotations include $\mathsf{both}/\mathsf{left}/\mathsf{right}$. Maintain the invariant that each accepted $\mathsf{both}(a,b)$ has identical erased shape. It must accept two annotations of identity and two record views, reject an identity/constant pair, and confirm that both projections of each accepted pair erase to one shape. Removing the same-erasure conjunct must make the test fail.

Referenced from 5 locations

• Dependent Intersections and Same-Subject Refinement
• Logic enrichment and erased dependency: executable records
• ch:dependent-intersections: same-subject views