CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse

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

The Church numeral $n$ is an iterator: $$n:\mathrm{\forall }X:\star .X\to (X\to X)\to X.$$ It can compute $n$ applications of a step, but its result type cannot state a property of the numeral $n$ itself. Replacing $X$ by a motive $P:\mathsf{Nat}\to \star$ is ill typed: $X$ has kind $\star$, while $P$ has kind $\mathsf{Nat}\to \star$. The missing information is not another iterator but evidence that the same erased numeral satisfies its own induction principle.

The Cedille Core contract

The annotated terms and their erasures are with Here $t-u$ is application to an erased term argument; it is not subtraction. The two terms on either side of $\simeq$ need only have their free variables declared; equality is heterogeneous and untyped.

The retained and erased functions differ at runtime. Their rules are given in formation, introduction, elimination, and computation order.

$T{{⟶}^{\ast }}_{\mathrm{cbn}}\mathrm{\Pi }x:T_1.T_2$$\mathrm{\Gamma },x:T_1⊢t\Leftarrow T_2$

$\mathrm{\Gamma }⊢\lambda x.t\Leftarrow T$

$\mathrm{\Gamma }⊢f\Rightarrow \mathrm{\Pi }x:T_1.T_2$$\mathrm{\Gamma }⊢u\Leftarrow T_1$

$\mathrm{\Gamma }⊢fu\Rightarrow T_2[u/x]$

$(\lambda x.t)u⟶t[u/x]$

$T{{⟶}^{\ast }}_{\mathrm{cbn}}\mathrm{\forall }x:T_1.T_2$$\mathrm{\Gamma },x:T_1⊢t\Leftarrow T_2$$x\notin \mathrm{FV}(\mathrm{erase}(t))$

$\mathrm{\Gamma }⊢\mathrm{\Lambda }x.t\Leftarrow T$

$\mathrm{\Gamma }⊢f\Rightarrow \mathrm{\forall }x:T_1.T_2$$\mathrm{\Gamma }⊢u\Leftarrow T_1$

$\mathrm{\Gamma }⊢f-u\Rightarrow T_2[u/x]$

$\mathrm{erase}((\mathrm{\Lambda }x.t)-u)=\mathrm{erase}(t)$

Dependent intersections repeat the same-erasure condition of chapter 37 in bidirectional form.

$T{{⟶}^{\ast }}_{\mathrm{cbn}}\iota x:T_1.T_2$$\mathrm{\Gamma }⊢t_1\Leftarrow T_1$$\mathrm{\Gamma }⊢t_2\Leftarrow T_2[t_1/x]$$\mathrm{erase}(t_1){=}_{\beta \eta }\mathrm{erase}(t_2)$

$\mathrm{\Gamma }⊢[t_1,t_2]\Leftarrow T$

$\mathrm{\Gamma }⊢t\Rightarrow \iota x:T.T^{\prime }$

$\mathrm{\Gamma }⊢t.1\Rightarrow T$

$\mathrm{\Gamma }⊢t\Rightarrow \iota x:T.T^{\prime }$

$\mathrm{\Gamma }⊢t.2\Rightarrow T^{\prime }[t.1/x]$

$\mathrm{erase}([t_1,t_2].1)=\mathrm{erase}(t_1){=}_{\beta \eta }\mathrm{erase}(t_2)=\mathrm{erase}([t_1,t_2].2)$

For a neutral intersection variable $n$, the projections $n.1$ and $n.2$ do not reduce. Both erase to $n$, and their types provide the two views needed below.

Inductive naturals as an intersection

Put The type $\mathsf{NatC}$ supports iteration. It does not derive, for an arbitrary $P:\mathsf{NatC}\to \star$, a term of $P(n)$ from a base and step; the iterator quantifies over a single result type $X$. This nonderivability in second-order dependent type theory is the obstruction, not a missing clever choice of $X$.

Define the inductivity predicate and the inductive type $$\mathsf{Nat}:=\iota n:\mathsf{NatC}.\mathsf{IndNat}(n).$$

The zero inductivity term is $$\mathsf{zeroI}:=\mathrm{\Lambda }P.\lambda z.\lambda s.z.$$ Its erasure is $\lambda z.\lambda s.z$, exactly the erasure of $\mathsf{zeroC}$. Therefore $$\mathsf{zero}:=[\mathsf{zeroC},\mathsf{zeroI}]:\mathsf{Nat}$$ by CDLE-Isect-I.

Assume $n:\mathsf{Nat}$. Its second projection gives induction for $n.1$. Define $$\mathsf{sucI}(n):=\mathrm{\Lambda }P.\lambda z.\lambda s.s-n.1(n.2-Pzs).$$ The argument $n.1$ to the step is erased. Hence $$\mathrm{erase}(\mathsf{sucI}(n))=\lambda z.\lambda s.s(\mathrm{erase}(n)zs)=\mathrm{erase}(\mathsf{sucC}(n.1)).$$ The dependent intersection $$\mathsf{suc}(n):=[\mathsf{sucC}(n.1),\mathsf{sucI}(n)]$$ therefore inhabits $\mathsf{Nat}$.

Proof of Theorem 96.4 — Derived induction

Proof. Let $n:\mathsf{Nat}$. Projection $n.2$ synthesizes $\mathsf{IndNat}(n.1)$. Instantiate that witness with $P$, then supply the zero and step premises. Its result is exactly $P(n.1)$. Abstract over $n$, $s$, $z$, and the erased motive $P$. A predicate on represented naturals is obtained only by composition with the first projection. This domain is deliberate: the stored witness proves induction for the Church subject of an intersection inhabitant, not an unrestricted eliminator for arbitrary host-language values. ◻

The computation claims have three different strengths. Untyped beta reduction gives $$\mathrm{erase}(\mathsf{indNat}-Pzs\mathsf{zero}){⟶}^{\ast }\mathrm{erase}(z).$$ Internal equality after rewriting gives $$\mathsf{indNat}-Pzs\mathsf{zero}{=}_{P(\mathsf{zeroC})}z.$$ For neutral $n$, the term $\mathsf{indNat}-Pzsn$ has no native eliminator redex.

Soundness without global normalization

Let $\mathcal{R}$ be the complete lattice of beta-eta-closed sets of closed untyped lambda terms. A retained product is interpreted as the set of lambdas mapping each argument candidate to the codomain candidate. An erased product is the intersection of all codomain candidates. The two clauses that do the new work are where $\zeta (E)$ chooses a representative of the nonempty equivalence class $E$ and $\mathcal{L}$ is the set of closed untyped terms.

Proof of Theorem 96.5 — Cedille Core soundness and consistency

Proof. The four semantic clauses are imported as Theorem 1 of Stump and Jenkins for the exact Cedille Core syntax and classification rules frozen in convention 96.1. Its hypotheses and conclusions are, respectively, an environment $(\sigma ,\rho )\in [[\mathrm{\Gamma }]]$ and the four clauses displayed here. Lemmas 9–14 on page 10 establish nonemptiness, representative selection, term and type substitution, and invariance under type reduction; Appendix A, pages 10–15, proves every kinding, synthesis, and checking case by mutual induction. We import that complete proof rather than infer soundness from only the two clauses displayed above.

Theorem 2 of the same source has the exact closed consistency conclusion. Its local final step is the empty-candidate calculation: if a closed $t$ had type $\mathrm{\forall }X:\star .X$, soundness would put its erasure in every candidate in $\mathcal{R}$, including the empty candidate. No term belongs to the empty set, yielding a contradiction [SJ18]. ◻

Global normalization is false. If $\mathsf{Top}:=\{\lambda x.x\simeq \lambda x.x\}$, then $\beta \{\mathrm{\Omega }\}:\mathsf{Top}$ for $\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$. Its erasure is $\mathrm{\Omega }$, which does not normalize. This does not contradict theorem 96.5: the greatest equality candidate contains non-normalizing terms. Closed functions retyped by an identity-erasing cast to a retained function type do satisfy the source’s qualified call-by-name normalization theorem; no stronger claim is used here.

Four encodings perform four operations

CDLE does not make these encodings definitionally equal. Dependent intersection can attach induction to each, and zero-cost casts can relate representations only when the two coercions erase to identity.

Monotone recursion and constant-time boundaries

Define a zero-cost cast $$\mathsf{Cast}(A,B):=\iota f:(A\to B).\{f\simeq \lambda x.x\}.$$ If $c:\mathsf{Cast}(A,B)$, then $c.1:A\to B$ and $\mathrm{erase}(c.1){=}_{\beta \eta }\lambda x.x$. Casts form a preorder by identity and composition. A type scheme $F:\star \to \star$ is monotone when it has $${\mathsf{mono}}_F:\mathrm{\forall }A:\star .\mathrm{\forall }B:\star .\mathrm{\forall }c:\mathsf{Cast}(A,B).\mathsf{Cast}(F(A),F(B)).$$ Write ${\mathsf{Closed}}_F(X):=\mathsf{Cast}(F(X),X)$. Define the Tarski meet and its two universal casts by Both quantifiers in the definition of $\mathsf{Rec}$ are erased. Thus a term of $\mathsf{Rec}(F)$ is in every $F$-closed type without receiving a runtime dictionary.

Proof of Theorem 96.6 — Derived monotone recursive type

Proof. For $m:{\mathsf{mono}}_F$, the two casts are constructed by Indeed, ${\mathsf{recLB}}_F(c)$ casts $\mathsf{Rec}(F)$ to $X$; monotonicity casts $F(\mathsf{Rec}(F))$ to $F(X)$; composition with $c:\mathsf{Cast}(F(X),X)$ supplies the lower-bound family consumed by ${\mathsf{recGLB}}_F$. For unrolling, monotonicity sends the rolling cast to $\mathsf{Cast}(F(F(\mathsf{Rec}(F))),F(\mathsf{Rec}(F)))$, so the latter type is $F$-closed and ${\mathsf{recLB}}_F$ applies.

These definitions, including the identity-erasure proofs inside $\mathsf{recLB}$ and $\mathsf{recGLB}$, are the exact derived terms in Figure 12 of Jenkins and Stump; their greatest-lower-bound property is Theorem 8 on page 24. Figure 13 on page 25 defines retained $\mathsf{roll}$ and $\mathsf{unroll}$ by eliminating the two casts and proves both inverse equalities. Importing those derivations supplies the internal typing and equality premises omitted by the displayed mathematical notation. The erasure calculation is then $$(\lambda x.x)\circ (\lambda x.x)\stackrel{\beta }{⟶}\lambda x.x.$$ At runtime a roll or unroll is the identity function, so a constant number of beta steps exposes its argument independently of the recursive value’s size [JS21]. ◻

Without ${\mathsf{mono}}_F$, the $F$-image of a cast is unavailable and the two Tarski inequalities cannot be constructed. Positivity is one sufficient way to derive monotonicity; it is not built into $\mathsf{Rec}$ as a syntactic oracle.

A simulated large elimination

Large elimination asks a datatype value to compute a type. Cedille Core has no native type-level case reduction on an encoded value. It can instead produce an extensional equivalence of the desired types.

Define $$\mathsf{TpEq}(A,B):=\iota c:\mathsf{Cast}(A,B).\mathsf{Cast}(B,A).$$ The outer dependent intersection is nondependent in $c$, but its introduction rule forces the two cast witnesses to have the same identity erasure. If $e:\mathsf{TpEq}(A,B)$, the two coercions are the function views of $e.1$ and $e.2$, and both erase to $\lambda x.x$.

The source’s first concrete simulation is the family of $n$-ary function types over a fixed $T$. Native large elimination would postulate $$\mathsf{Nary}(0)\equiv T,\mathsf{Nary}(Sn)\equiv T\to \mathsf{Nary}(n),$$ but Cedille Core has no such type-level equations. Instead define a GADT-like relation by constructors and take $$\mathsf{Nary}(n):=\mathrm{\forall }X:\star .\mathrm{\forall }r:\mathsf{NaryR}(n,X).X.$$

Proof of Theorem 96.7 — Simulated Nary computation

Proof. Figure 4 on page 5 of Jenkins, Marmaduke, and Stump defines $\mathsf{NaryR}$. Figure 5 and Propositions 1–4 on pages 7–8 give the exact signatures of $\mathsf{naryZEq}$ and $\mathsf{narySEq}$, prove respect and uniqueness of the type index, and construct $\mathsf{naryREx}(n):\mathsf{NaryR}(n,\mathsf{Nary}(n))$. Their linked Cedille source supplies the mechanically checked derivations behind those signatures; we import them for the frozen CDLE calculus. Figure 6 on page 8 eliminates the witnesses to identity-erasing coercions. Thus either $\mathsf{TpEq}$ projection is zero cost, but no native case reduction is added [JMS22]. ◻

The generic construction extends this simulation to signatures with codes and interpretation, but its equation is extensional type equivalence, not an unrestricted equality of types. Some recursive examples expose only one simulated computation step before another explicit witness is required.

Zero-cost reuse

Assume an indexed vector encoding $\mathsf{Vec}(A,n)$ and a list encoding $\mathsf{List}(A)$ whose erased constructors are identical. The forgetful cast $${\mathsf{forget}}_n:\mathsf{Cast}(\mathsf{Vec}(A,n),\mathsf{List}(A))$$ has function view $\lambda x.x$. Suppose list map has type $$\mathsf{mapL}:(A\to B)\to \mathsf{List}(A)\to \mathsf{List}(B)$$ and its output length theorem permits the reverse cast into $\mathsf{Vec}(B,n)$. Define vector map by the two casts around list map. Its erasure is Typing uses the length theorem; runtime uses exactly the list implementation. This is zero-cost reuse: the conversion functions erase to identity, not merely to linear traversals that happen to return equal data.

If vector and list constructors have different erasures, the cast equality premise is false and the reuse proof fails. Extensional isomorphism alone does not establish zero cost.

Evidence from Cedille developments

The v1.1.2 Cedille checker and pinned developments check concrete induction, recursive-representation, large-elimination, and reuse files. Surface constructs map to the core as follows: erased braces map to $\mathrm{\forall }$ and $t-u$; intersection introductions map to $[t,u]$; equality proofs map to $\beta$, $\rho$, and $\varphi$; and casts map to dependent intersections whose function view erases to identity. The developments do not check an unprinted global normalization theorem, automatic large-elimination computation, or the consistency proof itself. The implementation bounds conversion search, so acceptance is relative to the configured budget.

Suggested first pass.

Begin with exercise 96.4, then complete exercise 96.6.

Exercise 96.4¶

★★☆ Reconstruct the zero and successor intersection introductions. Write each erasure. Use $P(n):=n+0=n$ and distinguish erased computation from the equality rewrites in its result type.

Referenced from 4 locations

• CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
• ch:cdle-cedille: CDLE and Cedille

Exercise 96.5¶

★★★ Write the intersection and equality cases of theorem 96.5. Instantiate $\mathrm{\forall }X:\star .X$ with the empty candidate. Then type $\beta \{\mathrm{\Omega }\}:\mathsf{Top}$ and explain why it does not affect that argument.

Referenced from 3 locations

• CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
• ch:cdle-cedille: CDLE and Cedille

Exercise 96.6¶

★★★ Practical project.cdle-zero-cost-runtime Implement in Kappa a finite model of Church observations, same-erasure admission, identity roll/unroll, and list-map reuse. Construct two successors, observe $2$, preserve it through roll/unroll, and obtain $[2,3]$. Reject a copying/identity pair. Unconditional admission must make the test fail.

Referenced from 5 locations

• CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
• Logic enrichment and erased dependency: executable records
• ch:cdle-cedille: finite zero-cost observations