Chapter 155Optional

Dependent PER-Enriched Domain Models

Prerequisites. Direct starred prerequisites: Chapter 153. Chapter 12 supplies the domain-theoretic interface. No later core chapter depends on this route.

A partial equivalence relation over a domain of realizers interprets a type that may contain divergent elements: proposition 153.31 already builds $Π$ and $Σ$ from PERs, and a least fixed point exists as soon as the relation is closed under suprema of chains and contains $⊥$ . Combine the two and something breaks.

Let $R$ be a PER on a pre-domain $A$ and let $S$ assign a PER $S_{x}$ to each $R$ -class $x$ . Interpret $Σ$ as usual: $Σ_{R} (S) : = {(⟨ a_{1}, b_{1} ⟩, ⟨ a_{2}, b_{2} ⟩) | a_{1} R a_{2} and b_{1} S_{[a_{1}]} b_{2}} .$ Suppose $R$ and every $S_{x}$ are chain-complete, and let $(⟨ a_{i}, b_{i} ⟩, ⟨ a_{i}^{'}, b_{i}^{'} ⟩)_{i \in N}$ be a chain in $Σ_{R} (S)$ . Completeness of $R$ gives $⨆ a_{i} R ⨆ a_{i}^{'}$ . For the second component one wants completeness of $S_{[⨆ a_{i}]}$ applied to the chain $(b_{i}, b_{i}^{'})$ — but each pair $(b_{i}, b_{i}^{'})$ lies in $S_{[a_{i}]}$ , and nothing so far says that the classes $[a_{i}]$ are all the same class. The argument stops, and it stops for a reason: the index of the second component moves along the chain.

This chapter fixes the gap by a single condition on the relations, and then develops the dependent model that condition supports.

The domain of realizers

Convention 155.1 — Domain interface ¶

Recall from chapter 12 only the following. A pre-domain is a poset with suprema of $ω$ -chains; a domain is a pre-domain with a least element $⊥$ ; $A_{⊥}$ adjoins one. A function is continuous when it is monotone and preserves suprema of chains, and $A \to_{c} B$ is the pre-domain of continuous functions under the pointwise order. For continuous $F : D \to D$ on a domain, $lfp (F) = ⨆_{n} F^{n} (⊥)$ is the least fixed point. A predicate is admissible when it holds of $⊥$ and is closed under suprema of chains, and admissible predicates support fixed-point induction. Nothing else from that chapter is used.

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Definition 155.2 — The universal pre-domain ¶

Fix a pre-domain $V$ with an isomorphism $V ≅ 1 + N + (V \times V) + (V \to_{c} V_{⊥}) + T (V),$ where $T (V) : = (V \times V)_{⊥}$ is the pre-domain of partial computations returning a value and a residual, and write ${in}_{1}, {in}_{N}, {in}_{\times}, {in}_{\to}, {in}_{T}$ for the injections. Define a partial application on $V$ by $a \cdot b : = {\begin{cases} f (b) & if a = {in}_{\to} (f) and f (b) \neq ⊥, \\ undefined & otherwise . \end{cases}$

Referenced from 6 locations

Dependent PER-Enriched Domain Models

Lemma 155.3 — V is a partial combinatory algebra ¶

There are $k, s \in V$ with $k \cdot a \cdot b = a$ and $s \cdot a \cdot b \cdot c = (a \cdot c) \cdot (b \cdot c)$ whenever the right-hand side is defined, so definition 153.27 applies to $(V, \cdot)$ .

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Proof of Lemma 155.3 — V is a partial combinatory algebra

Proof. Take $k : = {in}_{\to} (λ a . {in}_{\to} (λ b . a))$ and the analogous continuous term for $s$ ; both are continuous because they are built from projections, injections and application, each of which is continuous in the isomorphism of definition 155.2. The two equations hold by unfolding $\cdot$ , using that the outer applications produce non- $⊥$ values because their bodies are injections. ◻

Definition 155.4 — Complete, admissible, monotone ¶

Let $R$ be a PER on a pre-domain $A$ .

$R$ is complete when for all chains $(c_{i})$ , $(d_{i})$ with $c_{i} R d_{i}$ for every $i$ , also $⨆_{i} c_{i} R ⨆_{i} d_{i}$ ;
$R$ is admissible when it is complete, $A$ is a domain, and $⊥ \in | R |$ ;
$R$ is monotone when $x, y \in | R |$ and $x ⊑_{D} y$ imply $x R y$ .

Write $CMPer (A)$ for the complete monotone PERs on $A$ .

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Proposition 155.5 — Monotonicity repairs the Σ -argument ¶

Let $R \in CMPer (A)$ , and let $S$ assign a member of $CMPer (A)$ to each $R$ -class. Then $Σ_{R} (S)$ is complete and monotone. Without monotonicity of $R$ this fails: there are complete $R$ and $S$ for which $Σ_{R} (S)$ is not complete.

Referenced from 9 locations

Dependent PER-Enriched Domain Models

Proof of Proposition 155.5 — Monotonicity repairs the Σ -argument

Proof. Let $(⟨ a_{i}, b_{i} ⟩, ⟨ a_{i}^{'}, b_{i}^{'} ⟩)$ be a chain in $Σ_{R} (S)$ . Then $(a_{i})$ and $(a_{i}^{'})$ are chains in $| R |$ with $a_{i} R a_{i}^{'}$ , so $a : = ⨆ a_{i}$ and $a^{'} : = ⨆ a_{i}^{'}$ satisfy $a R a^{'}$ by completeness. Monotonicity now gives the missing step: for $i \leq j$ we have $a_{i} ⊑_{D} a_{j}$ with both in $| R |$ , hence $a_{i} R a_{j}$ , so all the classes $[a_{i}]$ coincide with $[a]$ . The pairs $(b_{i}, b_{i}^{'})$ therefore form a chain in the single PER $S_{[a]}$ , whose completeness gives $⨆ b_{i} S_{[a]} ⨆ b_{i}^{'}$ ; pairing is continuous, so $⨆ ⟨ a_{i}, b_{i} ⟩ = ⟨ a, ⨆ b_{i} ⟩$ and the two suprema are related. Monotonicity of $Σ_{R} (S)$ follows componentwise because the order on pairs is componentwise and both $R$ and $S_{[a]}$ are monotone.

For the counterexample let $A : = N \cup {\infty}$ with its usual order, an $ω$ -cpo. Let $R$ be the identity relation on $A$ : it is complete, since a chain related to itself has supremum related to itself, and it is not monotone, because $0 ⊑_{D} 1$ while $0 R 1$ fails. The $R$ -classes are the singletons. Put $S_{[n]}$ the total relation on $A$ for $n \in N$ and $S_{[\infty]}$ the empty relation; each is complete. Then $(⟨ n, 0 ⟩, ⟨ n, 1 ⟩)_{n \in N}$ is a chain in $Σ_{R} (S)$ , since $n R n$ and $0 S_{[n]} 1$ . Its supremum is the pair $(⟨ \infty, 0 ⟩, ⟨ \infty, 1 ⟩)$ , which is not in $Σ_{R} (S)$ , because $S_{[\infty]}$ is empty. So $Σ_{R} (S)$ is not complete. ◻

Remark 155.6 — What monotonicity costs ¶

Monotonicity is not free. If $R$ is monotone and $⊥ \in | R |$ then $⊥$ is related to every element of $| R |$ , hence by symmetry and transitivity all elements of $| R |$ are related: the type has at most one element up to equality. So the computation types — the ones whose domains contain $⊥$ — are forced to have trivial equality. The purely functional types are unaffected, because their realizers are injections ${in}_{\to} (f)$ with $f$ never $⊥$ on the domain, so $⊥ \notin | R |$ there. The model therefore distinguishes which computation type a realizer inhabits while identifying all elements within one such type.

Referenced from 7 locations

Dependent PER-Enriched Domain Models

Uniform families and the split structure

Contexts are not PERs. A context must carry enough structure to index a family of PERs and to have its own realizers, and the standard choice is an assembly.

Definition 155.7 — Assemblies and uniform families ¶

An assembly over $V$ is a pair $I = (| I |, E_{I})$ of a set and an assignment of a nonempty set $E_{I} (i) \subseteq V$ of realizers to each $i \in | I |$ . A morphism $u : I \to J$ is a function $| I | \to | J |$ for which some $α \in V$ satisfies $α \cdot e \in E_{J} (u (i))$ for all $i$ and $e \in E_{I} (i)$ . Write $Asm$ for the resulting category.

A uniform family of complete monotone PERs over $I$ is a family $X = (X_{i})_{i \in | I |}$ with each $X_{i} \in CMPer (V)$ . A morphism $(u, (f_{i})) : (I, X) \to (J, Y)$ consists of $u : I \to J$ in $Asm$ and functions $f_{i} : [X_{i}] \to [Y_{u (i)}]$ such that a single $α \in V$ satisfies $α \cdot e_{i} \cdot e_{v} \in f_{i} ([e_{v}]_{X_{i}}) for all i \in | I |, e_{i} \in E_{I} (i), e_{v} \in | X_{i} | .$ Write $UFam$ for this category, fibred over $Asm$ by $(I, X) \mapsto I$ .

Referenced from 3 locations

Dependent PER-Enriched Domain Models

The single realizer $α$ is what uniform means: the family of functions is realized once, not once per index.

Definition 155.8 — Reindexing ¶

For $u : J \to I$ in $Asm$ and $X$ over $I$ put $X [u] : = (X_{u (j)})_{j \in | J |}$ , and for a term $a = (a_{i})_{i}$ with $a_{i} \in [X_{i}]$ realized uniformly put $a [u] : = (a_{u (j)})_{j}$ .

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Lemma 155.9 — Split reindexing ¶

$X [{id}_{I}] = X$ and $X [u \circ v] = X [u] [v]$ , and the same two equations hold for terms; moreover reindexing preserves the property of being complete and monotone.

Referenced from 4 locations

Dependent PER-Enriched Domain Models

Proof of Lemma 155.9 — Split reindexing

Proof. Both sides of each equation are the same indexed family, since composition of the underlying index functions is strictly associative and unital and the PER assigned at $j$ is literally $X_{u (v (j))}$ in both cases. A realizer for the reindexed morphism is obtained from the given one by composing with a realizer of $u$ , which exists by definition 155.7. Completeness and monotonicity are properties of the individual PERs, which are unchanged. ◻

Theorem 155.10 — Comprehension ¶

For $I \in Asm$ and $X$ over $I$ define $\begin{aligned} | {X} | & : = {(i, x) ∣ i \in | I |, x \in [X_{i}]}, \\ E_{{X}} (i, x) & : = {⟨ e_{i}, e_{v} ⟩ ∣ e_{i} \in E_{I} (i), e_{v} \in x} . \end{aligned}$ Then ${X}$ is an assembly, the projection $p_{X} (i, x) : = i$ is a morphism, and for every $u : J \to I$ and every uniform $b = (b_{j})$ with $b_{j} \in [X_{u (j)}]$ there is a unique morphism $⟨ u, b ⟩ : J \to {X}$ over $u$ whose second component is $b$ . The resulting structure is split: comprehension commutes with reindexing on the nose.

Referenced from 4 locations

Dependent PER-Enriched Domain Models

Proof of Theorem 155.10 — Comprehension

Proof. Realizer sets are nonempty because each $E_{I} (i)$ is and each class $x$ is a nonempty subset of $| X_{i} |$ . The projection is realized by a first-projection combinator, which exists in $V$ by lemma 155.3 and the pairing injection. Given $u$ and $b$ realized by $α_{u}$ and $α_{b}$ , the morphism $⟨ u, b ⟩ (j) : = (u (j), b_{j})$ is realized by $e \mapsto ⟨ α_{u} \cdot e, α_{b} \cdot e ⟩$ , and it is unique because an element of $| {X} |$ is a pair whose components are recovered by the projection and by the second component. Splitness: both ${X} [u]$ and ${X [u]}$ have underlying set the pairs $(j, x)$ with $x \in [X_{u (j)}]$ and the same realizer sets, so they are equal, not merely isomorphic. ◻

Proposition 155.11 — Dependent products and sums ¶

For $X$ over $I$ and $Y$ over ${X}$ define, for $i \in | I |$ , $\begin{aligned} α Π_{X} (Y)_{i} β & iff for all e, e^{'} with e X_{i} e^{'}, α \cdot e Y_{(i, [e])} β \cdot e^{'}, \\ ⟨ a_{1}, b_{1} ⟩ Σ_{X} (Y)_{i} ⟨ a_{2}, b_{2} ⟩ & iff a_{1} X_{i} a_{2} and b_{1} Y_{(i, [a_{1}])} b_{2} . \end{aligned}$ Both are complete monotone PERs, both are strictly stable under reindexing, and they carry the $Π$ - and $Σ$ -structure of definition 54.21, definition 54.22.

Referenced from 8 locations

Dependent PER-Enriched Domain Models

Proof of Proposition 155.11 — Dependent products and sums

Proof. $Σ$ is proposition 155.5. For $Π$ : completeness holds because a chain $(α_{n}, β_{n})$ in $Π_{X} (Y)_{i}$ gives, for fixed related $e, e^{'}$ , a chain $(α_{n} \cdot e, β_{n} \cdot e^{'})$ in $Y_{(i, [e])}$ , and application is continuous in the function argument by definition 155.2, so the supremum of the applications is the application of the supremum. Monotonicity: if $α ⊑_{D} β$ with both in $| Π_{X} (Y)_{i} |$ then for related $e, e^{'}$ we get $α \cdot e ⊑_{D} β \cdot e$ with both in the domain of $Y_{(i, [e])}$ , hence related by monotonicity of $Y$ ; combining with $β \cdot e Y β \cdot e^{'}$ gives the claim. Stability is lemma 155.9 together with the observation that neither formula mentions the index set except through $X$ and $Y$ . The structure maps are abstraction and application of realizers, and their equations hold because morphisms are compared through their action on classes. ◻

Theorem 155.12 — Monotone completion is a reflection ¶

For a PER $R$ on $V$ let $\overset{―}{R} : = ⋂ {S \in CMPer (V) ∣ R \subseteq S}$ . Then $\overset{―}{-}$ is left adjoint to the inclusion $CMPer (V) ↪ Per (V)$ , the adjunction is fibred and split over $Asm$ , and for $T \in CMPer (V)$ , $\overset{―}{R} \to T = R \to T .$

Referenced from 6 locations

Dependent PER-Enriched Domain Models

Proof of Theorem 155.12 — Monotone completion is a reflection

Proof. $\overset{―}{R}$ is a complete monotone PER because both properties are preserved by intersections: a chain related in every $S$ has supremum related in every $S$ , and the monotonicity clause is a conjunction over pairs. It contains $R$ by construction and is contained in every complete monotone PER containing $R$ , which is the universal property of a reflection once the displayed equation is available.

For the equation, $\supseteq$ is immediate from $R \subseteq \overset{―}{R}$ . For $\subseteq$ , fix $α R \to T β$ and consider $S : = {(x, y) ∣ α \cdot x T β \cdot y} .$ It is a PER; it is complete because $T$ is and application is continuous; and it is monotone because $T$ is and application is monotone. It contains $R$ by assumption, so $\overset{―}{R} \subseteq S$ , which is exactly $α \overset{―}{R} \to T β$ . Fibredness and splitness hold because the construction is applied pointwise in the index and commutes with reindexing on the nose. ◻

Corollary 155.13 — Impredicative sums ¶

The coproducts induced by theorem 155.12 are strong, and for uniform families of complete monotone PERs they coincide with the $Σ_{X} (Y)$ of proposition 155.11.

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Proof of Corollary 155.13 — Impredicative sums

Proof. The induced coproduct is the monotone completion of the standard PER sum; by proposition 155.5 that sum is already complete and monotone, so the completion is the identity on it and the two agree. Strength is the statement that the comprehension of the coproduct is the comprehension of the family, which theorem 155.10 gives on the nose. ◻

Fixed points at a dependent type

Definition 155.14 — The fixed-point realizer ¶

Define $u : V \to_{c} (T (V) \to_{c} T (V))$ by $u (x) (y) : = {\begin{cases} z & if x \cdot {in}_{T} (y) = {in}_{T} (z), \\ ⊥ & otherwise, \end{cases}$ and put $lfp : = {in}_{\to} (λ x . {in}_{T} (⨆_{n} u (x)^{n} (⊥)))$ .

Referenced from 2 locations

Dependent PER-Enriched Domain Models

Lemma 155.15 — u is continuous ¶

The map $u$ is continuous in both arguments, so $⨆_{n} u (x)^{n} (⊥)$ exists and is the least fixed point of $u (x)$ .

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Proof of Lemma 155.15 — u is continuous

Proof. Application is continuous in each argument by definition 155.2, and ${in}_{T}$ is an isomorphism onto a summand, hence continuous with continuous partial inverse; the case split is by whether a continuous function returns a value in that summand, and the “otherwise” branch returns the least element, so the whole assignment is monotone and preserves suprema of chains. Kleene’s construction then applies. ◻

Theorem 155.16 — Fixed points at admissible types ¶

Let $R$ be an admissible PER on $T (V)$ , and write ${in}_{T} (R)$ for its image in $V$ . Then $lfp \in | ({in}_{T} (R) \to {in}_{T} (R)) \to {in}_{T} (R) |,$ and for every $α \in | {in}_{T} (R) \to {in}_{T} (R) |$ , $α \cdot (lfp \cdot α) {in}_{T} (R) lfp \cdot α .$

Referenced from 9 locations

Dependent PER-Enriched Domain Models

Proof of Theorem 155.16 — Fixed points at admissible types

Proof. Fix $α$ related to itself. By induction on $n$ , ${in}_{T} (u (α)^{n} (⊥)) \in | {in}_{T} (R) |$ : at $n = 0$ this is admissibility, $⊥ \in | R |$ ; at $n + 1$ it is the assumption on $α$ applied to the induction hypothesis. The sequence $(u (α)^{n} (⊥))_{n}$ is a chain because $u (α)$ is monotone and starts at $⊥$ , so completeness of $R$ gives $⨆_{n} u (α)^{n} (⊥) \in | R |$ , that is $lfp \cdot α \in | {in}_{T} (R) |$ . Relatedness of $lfp$ to itself is the same argument carried out on two related $α, α^{'}$ , using completeness of $R$ on the two chains simultaneously. The displayed equation is the fixed-point property of lemma 155.15 transported along ${in}_{T}$ : the supremum is a fixed point of $u (α)$ , and $α \cdot {in}_{T} (y)$ is ${in}_{T} (u (α) (y))$ whenever the left side lies in the computation summand, which it does because $α$ preserves ${in}_{T} (R)$ . ◻

Remark 155.17 — Where each hypothesis is used ¶

Admissibility supplies the base case $⊥ \in | R |$ and, through completeness, the passage to the supremum; monotonicity is not used in theorem 155.16, and by remark 155.6 it collapses the equality of exactly those types where fixed points live. Continuity of $u$ is used to know the supremum is a fixed point. Dropping any one of the three invalidates a named step.

Referenced from 2 locations

Dependent PER-Enriched Domain Models

Soundness, and one dependent partial program

Theorem 155.18 — Semantic substitution and soundness ¶

Let $T_{iH}$ be the dependent type theory with the structural rules of definition 54.2, $Π$ - and $Σ$ -types, a universe $set$ of small types, and a partial-computation former $T$ with a fixed-point rule at admissible types. Interpret contexts by assemblies, substitutions by their morphisms, types over $Γ$ by uniform families of complete monotone PERs over $[[Γ]]$ , terms by uniform families of classes, $set$ by the assembly of complete monotone PERs, and the fixed-point rule by theorem 155.16. Then

$[[A [γ]]] = [[A]] [[[γ]]]$ and $[[a [γ]]] = [[a]] [[[γ]]]$ ;
every derivable judgment holds under the interpretation, with the four equality judgments interpreted by equality of the corresponding semantic data.

Referenced from 7 locations

Dependent PER-Enriched Domain Models

Proof of Theorem 155.18 — Semantic substitution and soundness

Proof. Clause (1) is lemma 155.9 together with theorem 155.10, whose splitness makes the interpretation of a context extension commute with reindexing on the nose; the interpretation is therefore a strict morphism of the comprehension structure and the usual induction over derivations applies.

Clause (2) is that induction. The structural rules are the split structure. $Π$ and $Σ$ are proposition 155.11, with the impredicative sum handled by corollary 155.13; the PER cases are the two displayed formulas, and each equation between terms is checked on classes, where it reduces to an equation between realizers modulo the target PER. The universe is interpreted by an assembly whose underlying set is $CMPer (V)$ , which is a set because a PER is a subset of $V \times V$ ; decoding is the identity, and closure of $CMPer (V)$ under the two formers is proposition 155.11. The fixed-point rule is theorem 155.16: its premise is that the interpreting PER is admissible, and its conclusion is the displayed relatedness, which is exactly the required equation between the recursive term and its unfolding. ◻

Example 155.19 — A dependent partial program and its reindexing ¶

Let $I$ be the assembly of natural numbers with $E_{I} (n) = {{in}_{N} (n)}$ , and let $X$ over $I$ be the family with $X_{n}$ the complete monotone PER on $T (V)$ whose domain consists of the computations that, when run, either diverge or return a value below $n$ in the numeral order. Each $X_{n}$ is complete (a chain of such computations has such a supremum, since the bound is preserved) and monotone (any two of its elements are related, by remark 155.6, because $⊥$ is in the domain).

Let $search \in Tm (I, X)$ be interpreted by $lfp \cdot α$ where $α$ realizes “if the current candidate satisfies the test, return it, otherwise recurse on the next candidate”. By theorem 155.16 this is a well-formed element of $| X_{n} |$ for each $n$ , and it satisfies the unfolding equation in $X_{n}$ .

Now reindex along $u : J \to I$ , $u (j) : = j + 1$ . By definition 155.8, $X [u]_{j} = X_{j + 1}$ and $search [u]_{j} = {search}_{j + 1}$ , and the unfolding equation is inherited because it is an equation in $X_{j + 1}$ , which is one of the PERs of the original family. No new fixed point is taken: the semantic substitution lemma theorem 155.18(1) is what makes the reindexed program the reindex of the program.

The equality of $X_{n}$ is trivial by remark 155.6, so the model does not distinguish $search$ from the everywhere-divergent computation inside $X_{n}$ . What it does distinguish is the family: for $m \neq n$ the PERs $X_{m}$ and $X_{n}$ have different domains, so the two typings are different semantic facts.

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Exercise 155.1 ¶

★★☆ Verify directly that the family $X$ of example 155.19 is monotone, and then modify it so that it is complete but not monotone. Show that proposition 155.5 fails for your modification by exhibiting the chain, and identify which class of the base index moves.

Referenced from 2 locations

Dependent PER-Enriched Domain Models

Exercise 155.2 ¶

★★☆ Prove that the equation $\overset{―}{R} \to T = R \to T$ of theorem 155.12 fails if $T$ is merely complete and not monotone, by exhibiting $R$ and $T$ and a realizer in one side and not the other.

Referenced from 2 locations

Dependent PER-Enriched Domain Models

Exercise 155.3 ¶

★★☆ Give a complete monotone PER $R$ on $T (V)$ with $⊥ \notin | R |$ for which the conclusion of theorem 155.16 fails, and locate the first step of that proof that breaks.

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Comparison, boundary, and seminar

Only the domain-theoretic interface of convention 155.1 is shared with the adequacy development of chapter 154: pre-domains, continuity, chains, least fixed points and admissibility. Both chapters use $lfp$ and both reason with admissible predicates, and there the overlap ends. Theorem 154.24 equates the denotation of a term with the denotation of the effect tree its operational semantics builds; it is a theorem about a fixed simply typed language with a fixed algebraic signature, proved by a syntactic approximation argument. Nothing in the present chapter supplies an operational semantics, an effect tree, or an approximation language, so no adequacy statement follows here, and none is assumed. In the other direction, theorem 155.18 is a statement about dependent families and their reindexing; chapter 154 has no families, so it receives nothing from this chapter either. A dependent operational-adequacy theorem would require a matching source with its own language, its own observations and its own proof.

Four further boundaries are part of the results. Monotonicity is a hypothesis of proposition 155.5 and, by remark 155.6, it makes the equality of every computation type trivial; the model therefore proves soundness, not any statement distinguishing two convergent computations of the same specified type. Admissibility is a hypothesis of theorem 155.16 and cannot be dropped (exercise 155.3). The universe of theorem 155.18 is the assembly of complete monotone PERs, so it is closed under exactly the formers verified in proposition 155.11, and a former not verified there is not in the universe. And model soundness is neither normalization nor productivity for the syntax: no term is claimed to have a normal form, and no recursive definition is claimed to be productive.

The proof base is Svendsen, Birkedal and Nanevski’s split structure and its complete-monotone-PER instance [SBN11], whose monotonicity condition, monotone-completion reflection, uniform families, fixed-point operator and soundness statement are the results reconstructed above; the fibrational background is [Jac99]; and the computational reading of PERs and assemblies is the standard one of [Hyl82, AL91]. The Hoare-style specification layer of that source, and the state component of its realizer domain, are not developed here.

[4]

Suggested first pass.

Begin with exercise 155.4, then exercise 155.5, and finish with exercise 155.7.

Exercise 155.4 ¶

★★☆ Remark 155.6 shows that a monotone PER containing $⊥$ in its domain has a trivial equality. Prove this in full, and then prove that the purely functional types of proposition 155.11 avoid the collapse by showing that $⊥ \notin | Π_{X} (Y)_{i} |$ whenever $⊥ \notin | Y_{(i, x)} |$ for some $x$ .

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Exercise 155.5 ¶

★★★ Define $W$ -types in $UFam$ by taking, for $X$ over $I$ and $Y$ over ${X}$ , the least PER closed under the constructor $⟨ a, f ⟩$ with $a \in | X_{i} |$ and $f$ a realizer sending elements of $| Y_{(i, [a])} |$ into the PER being defined. Prove that the result is complete and monotone, and identify the place where the argument needs proposition 155.5.

Referenced from 3 locations

Dependent PER-Enriched Domain Models

Exercise 155.6 ¶

★★★ Write down, as precisely as you can, the statement of a dependent computational-adequacy theorem for the theory of theorem 155.18: an operational semantics, an observation, and the equality claimed. Then say which of its ingredients the present chapter supplies and which it does not, and explain why theorem 154.24 cannot be used to fill any of the gaps.

Referenced from 2 locations

Dependent PER-Enriched Domain Models

Exercise 155.7 — Practical: a complete-monotone PER checker ¶

★★★ Practical project.cmper-family-checker Implement the finite fragment of the model: a finite pre-domain given by an order table; a PER given by a relation table; and a uniform family given by a table of PERs indexed by a finite assembly. The program decides completeness, monotonicity and admissibility of a PER by exhaustive search over chains and comparable pairs, forms $Σ_{X} (Y)$ and $Π_{X} (Y)$ by the formulas of proposition 155.11, and computes the monotone completion $\overset{―}{R}$ of theorem 155.12 as the least fixed point of the closure operator. The invariant the program must maintain is that no table is reported complete, monotone or admissible unless every witness pair required by definition 155.4 has been checked. The program must print, for each named input, the three verdicts, the computed $Σ$ table, and the completion $\overset{―}{R}$ . The acceptance test is: the identity PER on ${0, 1, \dots, k, \infty}$ is reported complete and not monotone; the family of the counterexample in the proof of proposition 155.5 yields a $Σ$ table reported not complete, with the offending chain printed; after replacing the base PER by its monotone completion the same $Σ$ table is reported complete, illustrating proposition 155.5; and $\overset{―}{R} \to T$ and $R \to T$ print as the same table for a monotone $T$ , illustrating theorem 155.12. Finite tables are evidence on these inputs only: the realizer domain $V$ of definition 155.2 is infinite, so the program checks no instance of theorem 155.16 or theorem 155.18.

Referenced from 3 locations