Chapter 63Optional

Contextual Modal Type Theory and Beluga

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

An LF derivation under assumptions is not determined by its conclusion alone. For example, a derivation object for $x : A ⊢_{st} x : A$ may use $x$ , whereas a closed object of the same object type may not. Reifying only the term loses this distinction. A contextual type records both the term’s type and the exact open context.

Definition 63.1 — Simply typed contextual modal calculus ¶

The simply typed contextual modal calculus has two variable levels: $\begin{array}{rcl} Ψ, Γ & ::= & \cdot ∣ Γ, x : A, \\ Δ & ::= & \cdot ∣ Δ, u :: A [Ψ], \\ A, B & ::= & a ∣ A \to B ∣ [Ψ ⊢ A] . \end{array}$ Ordinary variables $x$ are declared in $Γ$ ; meta-variables $u$ stand for open objects and are declared in the modal context $Δ$ . Terms and explicit contextual substitutions are $\begin{array}{rcl} M, N & ::= & x ∣ λ (x : A) . M ∣ M N ∣ box (Ψ . M) \\ ∣ letbox (M, u . N) ∣ clo (u, σ), \\ σ & ::= & \cdot ∣ σ, M / x . \end{array}$ The family $[Ψ ⊢ A]$ is a contextual type: its elements are terms of type $A$ whose free ordinary variables are declared by $Ψ$ .

Referenced from 6 locations

The ordinary STLC rules carry the two contexts $Δ; Γ$ . The contextual rules are $\frac{Δ; Ψ ⊢ M : A}{Δ; Γ ⊢ box (Ψ . M) : [Ψ ⊢ A]} Ctx - I$ $\frac{\begin{matrix} Δ; Γ ⊢ M : [Ψ ⊢ A] \\ Δ, u :: A [Ψ]; Γ ⊢ N : C \end{matrix}}{Δ; Γ ⊢ letbox (M, u . N) : C} Ctx - E$ $\frac{\begin{matrix} u :: A [Ψ] \in Δ \\ Δ; Γ ⊢ σ : Ψ \end{matrix}}{Δ; Γ ⊢ clo (u, σ) : A} Meta .$ Rule Ctx-I discards the ambient ordinary context $Γ$ : only declarations in $Ψ$ may occur in the boxed body. Rule Meta restores an occurrence of the open object by giving one term for every declaration in $Ψ$ .

Example 63.2 — An open identity derivation ¶

If $u :: A [x : A]$ , then $Δ; y : A ⊢ box (z : A . clo (u, z / x)) : [z : A ⊢ A] .$ The closure instantiates the formal variable $x$ of $u$ by the boxed variable $z$ . The ambient $y$ is intentionally unavailable inside the box. Thus $box (z : A . y)$ is rejected when $y$ belongs only to the ambient context: Ctx-I checks its body under $z : A$ , not under $y : A, z : A$ .

Referenced from 2 locations

Contextual Modal Type Theory and Beluga

Exercise 63.1 ¶

★☆☆ In the modal context $u :: A [x : A]$ and ambient ordinary context $y : A$ , derive the type of $box (z : A . clo (u, z / x))$ rule by rule. Then replace the body by $y$ and identify the first premise that fails. (Eight lines.)

Referenced from 3 locations

Proposition 63.3 — Ordinary and contextual substitution ¶

The following operations preserve typing:

if $Δ; Γ ⊢ M : A$ and $Δ; Γ, x : A, Γ^{'} ⊢ N : C$ , then $Δ; Γ, Γ^{'} ⊢ N [M / x] : C$ ;
if $Δ; Ψ ⊢ M : A$ and $Δ, u :: A [Ψ], Δ^{'}; Γ ⊢ N : C$ , then $Δ, Δ^{'}; Γ ⊢ N [Ψ . M / u] : C$ ;
if $Δ; Γ ⊢ σ : Ψ$ and $Δ; Ψ ⊢ M : A$ , then $Δ; Γ ⊢ M [σ] : A$ .

In the second operation, $clo (u, τ) [Ψ . M / u] : = M [τ [Ψ . M / u] / Ψ];$ the inner operation recursively substitutes in every component of $τ$ . Substitution for a meta-variable therefore performs the postponed contextual substitution with those transformed components rather than constructing an ill-formed expression $clo (M, τ)$ .

Referenced from 2 locations

Contextual Modal Type Theory and Beluga

Proof of Proposition 63.3 — Ordinary and contextual substitution

Proof. Each clause is an induction on the second displayed typing derivation. Ordinary substitution commutes with every constructor except $box (Ψ . N)$ , whose body contains no free ambient ordinary variable; that form is unchanged. Simultaneous substitution extends beneath a lambda by the identity component for its bound variable.

For contextual substitution, the principal Meta case has head $u$ . The substitution $τ : Ψ$ is typed in the extended modal context $Δ, u :: A [Ψ], Δ^{'}$ . The induction hypotheses applied to its components give $τ [Ψ . M / u] : Ψ$ in $Δ, Δ^{'}$ . Simultaneous substitution then derives $M [τ [Ψ . M / u] / Ψ] : A$ , exactly the required result. A different meta-variable rebuilds its closure after applying the induction hypotheses to its substitution components. In the Ctx-E case, choose the bound meta-variable outside the finite set of meta-variables in $M$ and reapply the rule. The remaining cases commute with the operation. These cases also prove the third clause componentwise. ◻

The two principal reductions and two commuting conversions are $\begin{array}{rcl} (λ (x : A) . M) N & ⟶_{beta} & M [N / x], \\ letbox (box (Ψ . M), u . N) & ⟶_{box} & N [Ψ . M / u], \\ letbox (M, u . N) P & ⟶_{comm} & letbox (M, u . N P), \\ letbox (letbox (M, v . N), u . P) & ⟶_{comm} & letbox (M, v . letbox (N, u . P)), \end{array}$ with the bound meta-variable in each commuting conversion chosen outside the free meta-variables of the moved term.

Theorem 63.4 — Simply typed CMTT metatheory ¶

For the calculus of definition 63.1:

every principal reduction and commuting conversion preserves typing;
the union of those compatible reductions is strongly normalizing on well-typed terms.

Referenced from 2 locations

Contextual Modal Type Theory and Beluga

Proof of Theorem 63.4 — Simply typed CMTT metatheory

Proof. For subject reduction, invert the final typing rule at each principal redex. The beta case uses ordinary substitution; the box case uses contextual substitution; the commuting cases use weakening and rebuild Ctx-E.

For strong normalization, import Theorem 4.7(2) of Nanevski, Pfenning, and Pientka for the exact simply typed contextual modal syntax, typing judgments, principal reductions, and commuting conversions displayed here [NPP08]. Its interpretation theorem maps $[Ψ ⊢ A]$ to two copies of the function type from the translations of $Ψ$ to the translation of $A$ , maps $box$ to a sum injection, and maps $letbox$ to sum elimination. Theorem 4.7(1) proves that every source principal or commuting step maps to one or more target steps; Theorem 4.7(2) concludes directly that their union is strongly normalizing on well-typed source terms. Its proof imports de Groote’s strong normalization theorem for the simply typed lambda calculus with binary sums, beta-reduction, and the two case-permutation conversions. We use the stated source theorem rather than treating that target result as a local lemma. The source theorem treats meta-level application of explicit substitutions as one operation; it does not establish strong normalization for an arbitrary explicit-substitution calculus. ◻

Canonical dependent contextual objects

Dependent LF needs unique canonical forms, whereas the commuting conversions above admit several syntactic placements of $letbox$ . The canonical dependent calculus therefore has only normal and atomic terms and performs substitution hereditarily.

Definition 63.5 — Dependent contextual canonical forms ¶

Extend canonical LF with contextual products $\prod_{u :: A [Ψ]} B$ and with meta-variables declared $u :: A [Ψ]$ . If $Ψ = x_{1} : A_{1}, \dots, x_{n} : A_{n}$ , write $\hat{Ψ} : = x_{1}, \dots, x_{n}$ for its list of variable names with the types erased. Normal terms include $mlam (u . M)$ ; atomic terms include contextual application $mapp (R, \hat{Ψ} . N)$ . Otherwise normal terms are ordinary lambdas or atomic terms, and atomic terms are headed by an ordinary variable, a constant, or a closure $clo (u, σ)$ . Typing is bidirectional: normal terms check against a given canonical family, while atomic terms synthesize a canonical family.

Hereditary substitution is written postfix using the global substitution notation: for example, $(B [\hat{Ψ} . N / u])_{A [Ψ]}^{a}$ substitutes the contextual object $\hat{Ψ} . N$ for $u$ in the type $B$ , using $A [Ψ]$ as termination index. The superscripts $n$ , $a$ , $γ$ , and $δ$ key the mutually defined operations on normal terms, types, ordinary contexts, and modal contexts. For a simultaneous substitution $σ$ , the corresponding notation is $(B [σ])_{Ψ}^{a}$ , with the same superscript keys.

The modal context, contextual product, meta-abstraction, and contextual application rules are $\frac{\begin{matrix} ⊢ Δ mctx \\ Δ ⊢ Ψ ctx \\ Δ; Ψ ⊢ A \Leftarrow type \end{matrix}}{⊢ Δ, u :: A [Ψ] mctx} MCtx$ $\frac{\begin{matrix} Δ ⊢ Ψ ctx \\ Δ; Ψ ⊢ A \Leftarrow type \\ Δ, u :: A [Ψ]; Γ ⊢ B \Leftarrow type \end{matrix}}{Δ; Γ ⊢ \prod_{u :: A [Ψ]} B \Leftarrow type} MPi$ $\frac{Δ, u :: A [Ψ]; Γ ⊢ M \Leftarrow B}{Δ; Γ ⊢ mlam (u . M) \Leftarrow \prod_{u :: A [Ψ]} B} MLam$ $\frac{\begin{matrix} Δ; Γ ⊢ R \Rightarrow \prod_{u :: A [Ψ]} B \\ Δ; Ψ ⊢ N \Leftarrow A \end{matrix}}{Δ; Γ ⊢ mapp (R, \hat{Ψ} . N) \Rightarrow (B [\hat{Ψ} . N / u])_{A [Ψ]}^{a}} MApp .$ Closures and simultaneous substitutions are checked by the following four rules; the second extension form records an atomic component with $R / / x$ : $\frac{Δ, u :: A [Ψ], Δ^{'}; Γ ⊢ σ \Leftarrow Ψ}{Δ, u :: A [Ψ], Δ^{'}; Γ ⊢ clo (u, σ) \Rightarrow (A [σ])_{Ψ}^{a}} MVar$ $\frac{}{Δ; Γ ⊢ \cdot \Leftarrow \cdot} SNil \frac{\begin{matrix} Δ; Γ ⊢ σ \Leftarrow Ψ \\ Δ; Γ ⊢ M \Leftarrow (A [σ])_{Ψ}^{a} \end{matrix}}{Δ; Γ ⊢ σ, M / x \Leftarrow Ψ, x : A} SNorm$ $\frac{\begin{matrix} Δ; Γ ⊢ σ \Leftarrow Ψ \\ Δ; Γ ⊢ R \Rightarrow A^{'} \\ A^{'} = (A [σ])_{Ψ}^{a} \end{matrix}}{Δ; Γ ⊢ σ, R / / x \Leftarrow Ψ, x : A} SAtom .$ The ordinary context-formation and ordinary bidirectional LF rules carry the same modal prefix $Δ$ . Thus the hereditary operation in MApp is part of the typing rules whose decidability is stated below, rather than an untyped meta-operation.

Referenced from 5 locations

Ordinary substitution of a canonical lambda into a neutral application creates a beta-redex. A hereditary substitution contracts every such redex as it is created. Its termination index is the dependency-erasure $\begin{array}{rcl} a^{-} & : = & a, \\ (\prod_{x : A} B)^{-} & : = & A^{-} \to B^{-}, \\ (\prod_{u :: A [Ψ]} B)^{-} & : = & A^{-} [Ψ^{-}] \to B^{-} . \end{array}$ For the characteristic ordinary application case, $[M / x]_{α} (R N) : = {\begin{cases} R^{'} N^{'} & [M / x]_{α} R = R^{'} atomic, \\ [N^{'} / y]_{α_{1}} M^{'} & [M / x]_{α} R = λ y . M^{'} : α_{1} \to α_{2}, \end{cases}$ where $N^{'} : = [M / x]_{α} N$ and $α_{1}$ is a proper subexpression of $α$ in the second case. Contextual application has the same clause with a contextual approximation $α_{1} [ψ] \to α_{2}$ . The outer measure decreases when a created redex is contracted; otherwise the term structure decreases.

Theorem 63.6 — Qualified hereditary substitution and decidability ¶

For the dependent canonical calculus of definition 63.5:

ordinary, simultaneous, and contextual hereditary substitutions terminate on every raw input, returning a result or finite failure;
all formation, checking, synthesis, and equality judgments are decidable.
Ordinary substitution preserves a normal-object judgment under the following exact existence premises. If $Δ; Γ ⊢ M \Leftarrow A, Δ; Γ, x : A, Γ_{1} ⊢ N \Leftarrow C,$ $Γ_{1}^{'} = (Γ_{1} [M / x])_{A}^{γ}$ exists with $Δ ⊢ Γ, Γ_{1}^{'} ctx$ , and $C^{'} = (C [M / x])_{A}^{a}$ exists with $Δ; Γ, Γ_{1}^{'} ⊢ C^{'} \Leftarrow type$ , then $Δ; Γ, Γ_{1}^{'} ⊢ (N [M / x])_{A}^{n} \Leftarrow C^{'} .$
Modal substitution preserves a normal-object judgment if the substituted modal suffix, ordinary context, and result type all exist and are well formed. Explicitly, from $Δ; Ψ ⊢ M \Leftarrow A, Δ, u :: A [Ψ], Δ_{1}; Γ ⊢ N \Leftarrow C,$ put $\begin{array}{rcl} Δ_{1}^{'} & = & (Δ_{1} [\hat{Ψ} . M / u])_{A [Ψ]}^{δ}, \\ Γ^{'} & = & (Γ [\hat{Ψ} . M / u])_{A [Ψ]}^{γ}, \\ C^{'} & = & (C [\hat{Ψ} . M / u])_{A [Ψ]}^{a} . \end{array}$ If all three exist and $⊢ Δ, Δ_{1}^{'} mctx$ , $Δ, Δ_{1}^{'} ⊢ Γ^{'} ctx$ , and $Δ, Δ_{1}^{'}; Γ^{'} ⊢ C^{'} \Leftarrow type$ , then $Δ, Δ_{1}^{'}; Γ^{'} ⊢ (N [\hat{Ψ} . M / u])_{A [Ψ]}^{n} \Leftarrow C^{'} .$
Simultaneous substitution requires an underapproximation. Write $Ψ^{-} = (x_{1} : α_{1}, \dots, x_{n} : α_{n})$ for dependency erasure. A context approximation $ψ$ underapproximates $Ψ$ with respect to $σ$ when it differs from $Ψ^{-}$ only by replacing a declaration $x_{i} : α_{i}$ with the untyped declaration $x_{i} :$ , and only when the corresponding component of $σ$ is atomic, written $R_{i} / / x_{i}$ . If $Δ; Γ ⊢ σ \Leftarrow Ψ$ , $Δ; Ψ ⊢ N \Leftarrow C$ , and $ψ$ is an underapproximation of $Ψ$ with respect to $σ$ , then, whenever $C^{'} = (C [σ])_{ψ}^{a}$ exists and $Δ; Γ ⊢ C^{'} \Leftarrow type$ , $Δ; Γ ⊢ (N [σ])_{ψ}^{n} \Leftarrow C^{'} .$

Referenced from 3 locations

Proof of Theorem 63.6 — Qualified hereditary substitution and decidability

Proof. For termination, order recursive calls lexicographically: first by the strict subexpression ordering on the erased approximation $α$ , $α [ψ]$ , or $ψ$ , and second by the raw syntax. Compositional clauses retain the approximation and descend to a subterm. A clause that creates a redex may enter a larger body, but its new approximation is a proper subexpression, as in the displayed application clause. The ordering is well founded, so every operation returns or fails after finitely many calls.

For preservation, strengthen the claim mutually over normal terms, atomic terms, types, kinds, contexts, modal contexts, and substitutions. Induct first on the erased approximation and then on the typing derivation. The created-redex case uses the outer induction hypothesis at $α_{1} < α$ ; compositional cases use the derivation induction hypotheses. The context, modal-context, and type existence premises in clauses 3–5 are required because the raw terminating operation is permitted to fail; they establish that the reconstructed target judgments are defined.

The bidirectional rules are syntax directed. Their only non-structural computations are the hereditary substitutions just proved terminating, so structural recursion decides every judgment. Clauses 1–2 are exactly Theorems 5.1–5.2 on pp. 30–31 of [NPP08]. The source’s Theorem 5.3 states the three corresponding type-formation principles; clauses 3–5 are the normal-object principles of its Appendix Theorem C.4, including that theorem’s existence, well-formedness, and underapproximation hypotheses. The proof above exhibits their common measure without strengthening those imported claims. ◻

Exercise 63.2 ¶

★★☆ Let $f : A \to A$ and $y : A$ . Compute the hereditary substitution of the canonical object $λ (z : A) . z$ for $f$ in the neutral application $f y$ . Display the created beta-redex, its contraction, and the strict decrease from approximation $A^{-} \to A^{-}$ to $A^{-}$ . (Half a page.)

Referenced from 3 locations

A context-preserving transformation

For a neutral STLC object $R$ , define type-directed eta expansion by $\begin{array}{rcl} η_{ι} (R) & : = & R, \\ η_{A \to B} (R) & : = & λ (x : A) . η_{B} (R η_{A} (x)), \end{array}$ where $x$ is the ordinary variable introduced by the contextual binder. The recursive call $η_{A} (x)$ first expands the newly introduced neutral variable at its domain type, so the application to $R$ is well typed even when $A$ is itself a function type.

Proposition 63.7 — Context preservation of eta expansion ¶

If $D$ is a contextual LF derivation of a neutral object $[Ψ ⊢_{st} R \Rightarrow A]$ , then the syntax-directed transformation $η (D)$ is a derivation $[Ψ ⊢_{st} η_{A} (R) \Leftarrow A]$ . The output contains no ordinary variable outside $Ψ$ .

Referenced from 2 locations

Contextual Modal Type Theory and Beluga

Proof of Proposition 63.7 — Context preservation of eta expansion

Proof. Induct on $A$ . At $ι$ , the neutral-to-normal coercion returns $D$ . At $A \to B$ , extend $Ψ$ by $x : A$ . The contextual variable rule synthesizes $x : A$ , and the induction hypothesis at $A$ checks $η_{A} (x) : A$ . Application therefore synthesizes $R η_{A} (x) : B$ . The induction hypothesis at $B$ checks its eta expansion, and abstraction discharges $x$ , returning to the exact context $Ψ$ . Every introduced variable is discharged in this same recursive clause, so the free-variable set remains contained in $dom (Ψ)$ . ◻

This transformation internalizes open LF objects. It is not a universe of binding descriptions: its recursion is fixed to the displayed STLC syntax and its contextual type records one concrete LF context.

Beluga context schemas and recursive calls

Beluga programs manipulate contextual LF objects, so a recursive proof must preserve the shape of the open LF context as well as the conclusion family. For the type-uniqueness example, fix LF families $tp : type$ , $term : type$ , and $hastype : term \to tp \to type$ .

Definition 63.8 — Paired typing schema ¶

The context schema $xtG$ generates contexts by repeating blocks $b = (x : term, u : hastype x T)$ for an LF object type $T : tp$ . A projection $b . x$ denotes the term declaration and $b . u$ denotes its paired typing derivation. Every use of $b . u$ therefore has family $hastype (b . x) T$ in the context extended by the whole block.

Referenced from 3 locations

Contextual Modal Type Theory and Beluga

In the lambda case of type uniqueness, the two premise derivations are opened under the same extended schema context $g, b : xtG$ . A recursive call must pass both projections because the body derivations mention the new term and require its typing assumption.

Proposition 63.9 — Paired-block scope invariant ¶

Let $g$ satisfy $xtG$ and let $b$ be a block of definition 63.8. A contextual object with family $[g, b ⊢ hastype (b . x) T]$ may project $b . u$ . If a recursive call extends its contextual term argument by $b . x$ but omits $b . u$ from the corresponding derivation argument, that argument does not inhabit the displayed family.

Referenced from 2 locations

Contextual Modal Type Theory and Beluga

Proof of Proposition 63.9 — Paired-block scope invariant

Proof. Schema inversion gives exactly two declarations in $b$ : the object $b . x : term$ and $b . u : hastype (b . x) T$ . The LF variable rule derives the displayed family from the second declaration. After omitting $b . u$ , no declaration in $g, b . x : term$ has that family. Canonical-head inversion therefore has no variable case for the required derivation object, so the recursive argument is out of scope. ◻

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 63.3, then complete exercise 63.5.

Exercise 63.3 ¶

★★☆ Let $Ψ = (x : A, y : B)$ and let a simultaneous substitution contain a normal component $M / x$ and an atomic component $R / / y$ . List every context approximation that underapproximates $Ψ$ with respect to this substitution. Explain why erasing the type of $x$ is forbidden and why retaining the type of $y$ remains permitted. (Half a page.)

Referenced from 4 locations

Exercise 63.4 ¶

★★☆ Compare the simply typed box redex with the dependent contextual application of a canonical meta-abstraction. Give one well-typed instance of each. Normalize both, and identify why the first calculus needs commuting conversions while the second performs hereditary substitution during typing. Do not transfer strong normalization from one calculus to the other.

Referenced from 3 locations

Exercise 63.5 ¶

★★★ Practical project.beluga-context-scope Inspect the pinned Beluga file examples/literate_beluga/0Beginner/Type_Uniqueness.bel. Identify the schema block pairing an LF term variable with its typing assumption and the recursive call that extends that block under a lambda. In the Kappa companion, represent the paired declarations and check that both projected arguments refer to the same term and type. Then replace the typing projection by one for a different term. The accepted corpus must accept the source-shaped call and reject the altered call with the missing family $[g, b ⊢ hastype (b . x) -]$ . This finite check does not execute Beluga and does not establish either theorem card printed in the preceding contextual-modal development.

Referenced from 6 locations

Sources. The simply typed interpretation is Theorem 4.6 of Nanevski, Pfenning, and Pientka; its strong-normalization boundary is Theorem 4.7 [NPP08]. The raw termination and decidability statements are Theorems 5.1–5.2 on pp. 30–31. The exact well-formedness, existence, and underapproximation premises for preservation are Theorem C.4 on Appendix pp. 11–12 (physical PDF pp. 59–60). Pientka’s tutorial prints the paired schema on physical pp. 60–64 and the lambda-case recursive call with both block projections on physical p. 72 [Pie15]. Those pages and the pinned Beluga source are source-shape evidence only; they do not supply an LF adequacy or CMTT normalization theorem [Bel25].

Contextual modal objects

Canonical dependent contextual objects

A context-preserving transformation

Beluga context schemas and recursive calls

Suggested first pass.