Chapter 21Optional

Disjoint Intersections, Merge Elaboration, and Coherence

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

The term $1,, 2$ offers two integers. If an integer is demanded, a type-directed compiler may select either component: $(1,, 2 : Int) ⇝ π_{1} (1, 2) or (1,, 2 : Int) ⇝ π_{2} (1, 2) .$ The target programs evaluate to $1$ and $2$ . Type preservation alone does not choose between them. A coherent merge calculus must exclude this overlap and must also prevent ambiguity introduced indirectly by subtyping.

This chapter fixes the top-free variant of the calculus $λ_{i}$ of Oliveira, Shi, and Alpuim. In particular, there is no $Top$ type and no appeal to either of that paper’s two notions of top-like type. This choice is part of every statement below.

The source and its pair target

The running merge is $1,, (λ x . x : Int \to Int)$ . Its two components have incompatible outer forms, so an integer demand selects the left branch and a function demand selects the right branch.

Definition 21.1 — The top-free merge calculus ¶

Source types and terms are $\begin{array}{rcl} A, B, C & ::= & Int ∣ A \to B ∣ A \times B ∣ A & B, \\ e & ::= & n ∣ x ∣ λ x . e ∣ e_{1} e_{2} ∣ (e_{1}, e_{2}) \\ ∣ π_{i} e ∣ e_{1},, e_{2} ∣ (e : A), i \in {1, 2} . \end{array}$ An ordinary type is a type whose outer constructor is not intersection: $Int ordinary, A \to B ordinary, A \times B ordinary .$ Contexts are finite lists of declarations with distinct variables.

The target is the simply typed call-by-value lambda calculus with integers and products: $\begin{array}{rcl} T, U & ::= & Int ∣ T \to U ∣ T \times U, \\ M, N & ::= & n ∣ x ∣ λ x . M ∣ M N ∣ (M, N) ∣ π_{i} M, \\ V, W & ::= & n ∣ λ x . M ∣ (V, W), \\ E & ::= & [] ∣ E M ∣ V E ∣ (E, M) ∣ (V, E) ∣ π_{i} E . \end{array}$ Its typing rules are

x : T \in Γ

Γ ⊢ x : T

DT-Var

Γ ⊢ n : Int

DT-Int

Γ, x : T ⊢ M : U

Γ ⊢ λ x . M : T \to U

DT-Lam

Γ ⊢ M : T \to U

Γ ⊢ N : T

Γ ⊢ M N : U

DT-App

Γ ⊢ M : T

Γ ⊢ N : U

Γ ⊢ (M, N) : T \times U

DT-Pair

Γ ⊢ M : T_{1} \times T_{2}

Γ ⊢ π_{i} M : T_{i}

DT-Proj

Root contraction and compatible call-by-value reduction are $(λ x . M) V ⇝_{0} M [V / x], π_{i} (V_{1}, V_{2}) ⇝_{0} V_{i}, \frac{M ⇝_{0} N}{E [M] ⟼ E [N]} .$ Source types are erased to target types by $\begin{aligned} | Int | & = Int, & | A \to B | & = | A | \to | B |, \\ | A \times B | & = | A | \times | B |, & | A & B | & = | A | \times | B | . \end{aligned}$ Context erasure applies this operation to every declaration.

Referenced from 4 locations

The target distinguishes a source product from a source intersection only through the elaboration that constructs it. A product is an explicit pair. An intersection is implemented by a pair whose projections are inserted by subtyping.

Definition 21.2 — Coercive subtyping ¶

The judgment $A <: B ⇝ c$ means that source subtyping constructs a target coercion $c : | A | \to | B |$ . It is generated by

Int <: Int ⇝ λ x . x

S-Int

B_{1} <: A_{1} ⇝ c_{1}

A_{2} <: B_{2} ⇝ c_{2}

A_{1} \to A_{2} <: B_{1} \to B_{2} ⇝ λ f . λ x . c_{2} (f (c_{1} x))

S-Arr

A_{1} <: B_{1} ⇝ c_{1}

A_{2} <: B_{2} ⇝ c_{2}

A_{1} \times A_{2} <: B_{1} \times B_{2} ⇝ λ p . (c_{1} (π_{1} p), c_{2} (π_{2} p))

S-Prod

A <: B_{1} ⇝ c_{1}

A <: B_{2} ⇝ c_{2}

A <: B_{1} & B_{2} ⇝ λ x . (c_{1} x, c_{2} x)

S-&R

A_{1} <: B ⇝ c

B ordinary

A_{1} & A_{2} <: B ⇝ λ p . c (π_{1} p)

S-&L_1

A_{2} <: B ⇝ c

B ordinary

A_{1} & A_{2} <: B ⇝ λ p . c (π_{2} p)

S-&L_2

Write $A <: B$ when some $c$ makes the elaborating judgment derivable. The ordinary-type premises force a right intersection to be decomposed by S- $&$ R before either left projection can apply.

Referenced from 3 locations

Worked calculations display target coercions in beta-eta normal form. The syntactic uniqueness and coherence statements compare the raw coercions generated by the rules before this presentation convention is applied.

For example, $Int & (Int \to Int) <: Int ⇝ λ p . π_{1} p,$ whereas the function demand derives the coercion $λ p . π_{2} p$ . No search preference is involved.

Lemma 21.3 — Coercion typing ¶

If $A <: B ⇝ c$ , then $\cdot ⊢ c : | A | \to | B |$ in the target calculus.

Referenced from 4 locations

Proof of Lemma 21.3 — Coercion typing

Proof. Use rule induction. Rule S-Int is target identity. For S-Arr, the induction hypotheses type $c_{1} : | B_{1} | \to | A_{1} |$ and $c_{2} : | A_{2} | \to | B_{2} |$ ; therefore the displayed eta-expansion maps a function $f : | A_{1} | \to | A_{2} |$ to one of type $| B_{1} | \to | B_{2} |$ . Rule S-Prod applies the two coercions to the corresponding projections. Rule S- $&$ R pairs two results obtained from the same input. The two left rules project the indicated component before applying their induction-hypothesis coercion. These are all rules. ◻

Disjointness is absence of a common demand

Merely requiring $A ≮: B$ and $B ≮: A$ is too weak. The types $Int & (Int \to Int) and Int & (Int \times Int)$ are incomparable, but both can answer an integer demand. Merging values of these types would restore the original ambiguity one level down.

Definition 21.4 — Simple disjointness and well-formed types ¶

Two top-free types are disjoint, written $A * B$ , when they have no common supertype: $A * B : = \neg \exists C . A <: C \land B <: C .$ The witness $C$ ranges over raw types generated by definition 21.1; it need not itself satisfy well-formedness. Source typing admits only well-formed types, but this unrestricted witness makes the structural decision theorem below complete. An ill-formed intersection may therefore witness a common function domain without becoming a type of a term. Well-formedness is structural for integers, arrows, and products. Its intersection clause is

Γ ⊢ A type

Γ ⊢ B type

A * B

Γ ⊢ A & B type

WF-&

The type grammar has no $Top$ ; hence (21.1) does not require an exception for top-like common supertypes.

Referenced from 3 locations

Lemma 21.5 — Unique contributor ¶

Suppose $A_{1} & A_{2}$ is well formed and $B$ is ordinary. It is impossible to have both $A_{1} <: B$ and $A_{2} <: B$ .

Referenced from 5 locations

Proof of Lemma 21.5 — Unique contributor

Proof. Inversion of WF- $&$ gives $A_{1} * A_{2}$ . If both subtype judgments held, $B$ would be their common supertype, contradicting (21.1). ◻

The definition quantifies over types and is not yet a decision procedure. For the frozen grammar, structural rules decide it.

Definition 21.6 — Algorithmic disjointness ¶

Write $A *_{a} B$ for the least symmetric relation generated by the following clauses.

An intersection distributes: $\frac{A_{1} *_{a} B A_{2} *_{a} B}{A_{1} & A_{2} *_{a} B}, \frac{A *_{a} B_{1} A *_{a} B_{2}}{A *_{a} B_{1} & B_{2}} .$
Functions are disjoint exactly when their result types are: $\frac{A_{2} *_{a} B_{2}}{A_{1} \to A_{2} *_{a} B_{1} \to B_{2}} .$
Products are disjoint when either corresponding component is: $\frac{A_{1} *_{a} B_{1}}{A_{1} \times A_{2} *_{a} B_{1} \times B_{2}}, \frac{A_{2} *_{a} B_{2}}{A_{1} \times A_{2} *_{a} B_{1} \times B_{2}} .$
Two nonintersection types with distinct outer constructors are algorithmically disjoint.

The procedure first distributes intersections, then compares the remaining outer constructors. In the product case it succeeds if either recursive call succeeds; in the function case it inspects only results.

Referenced from 4 locations

Function domains do not decide disjointness. Although $Int * (Int \times Int)$ , the functions $Int \to Int and (Int \times Int) \to Int$ share the supertype $(Int & (Int \times Int)) \to Int$ . Contravariance creates the common domain.

Lemma 21.7 — Ordinary-leaf decomposition ¶

An ordinary leaf of a type is an ordinary type obtained by repeatedly choosing one component of an outer intersection. Every raw type has an ordinary leaf. For raw types $X, C$ , one has $X <: C$ if and only if $X <: D$ for every ordinary leaf $D$ of $C$ .

Referenced from 5 locations

Disjoint Intersections, Merge Elaboration, and Coherence

Proof of Lemma 21.7 — Ordinary-leaf decomposition

Proof. Induct on $C$ . If $C$ is ordinary, its only ordinary leaf is $C$ , so both implications are identities. If $C = C_{1} & C_{2}$ , its ordinary leaves are those of $C_{1}$ together with those of $C_{2}$ . In the forward direction, inversion fixes the last rule as S- $&$ R; its two premises and the induction hypotheses give subtyping to every leaf. In the reverse direction, the induction hypotheses give $X <: C_{1}$ and $X <: C_{2}$ , and S- $&$ R gives $X <: C$ . The same induction, choosing either component in the intersection case, proves existence of a leaf. ◻

Theorem 21.8 — Decision of simple disjointness ¶

For well-formed top-free types $A, B$ , $A *_{a} B ⟺ A * B .$ Consequently simple disjointness is decidable.

Referenced from 3 locations

Proof of Theorem 21.8 — Decision of simple disjointness

Proof. For soundness, induct on algorithmic disjointness and suppose that $C$ is a common supertype. Choose an ordinary leaf $D$ of $C$ . By lemma 21.7, both inputs subtype $D$ . In the function case, inversion fixes $D$ as an arrow and gives a result type common to both results. In either product case, inversion fixes $D$ as a product and gives common supertypes in both coordinates. Distinct ordinary outer constructors cannot both subtype $D$ , because no subtyping rule changes an ordinary outer constructor.

For distribution through $A_{1} & A_{2}$ , the derivation $A_{1} & A_{2} <: D$ selects one component because $D$ is ordinary. That component and $B$ both subtype $D$ , contradicting the corresponding premise $A_{i} * B$ . Exchanging the two arguments of $*$ gives right distribution: semantic disjointness is symmetric by (21.1), and $*_{a}$ was defined as a symmetric relation.

For completeness, induct on the total size of the pair. Suppose first that $A = A_{1} & A_{2}$ and algorithmic disjointness fails. One component $A_{i}$ then fails against $B$ . By the induction hypothesis, $A_{i}$ and $B$ have a common supertype $C$ . For each ordinary leaf $D$ of $C$ , lemma 21.7 gives $A_{i} <: D$ and $B <: D$ . Rule S- $&$ L $_{i}$ gives $A_{1} & A_{2} <: D$ ; rebuilding with lemma 21.7 makes $C$ a common supertype of $A$ and $B$ . Exchanging the two inputs proves the case in which $B$ is an intersection.

It remains to compare ordinary heads. Equal integer heads have the common supertype $Int$ , so semantic disjointness excludes that case. Distinct ordinary heads use the axiom. Two arrows can fail the algorithm only when their results have a common supertype $C$ ; then $(A_{1} & B_{1}) \to C$ is a raw common supertype of the arrows, whether or not its domain intersection is well formed, contrary to semantic disjointness. Two products can fail only when both coordinate pairs have common supertypes $C_{1}, C_{2}$ ; then $C_{1} \times C_{2}$ is common to the products. These cases exhaust the grammar. Every recursive call removes an outer constructor from at least one input, so it strictly reduces total pair size. ◻

Exercise 21.1 ¶

★★☆ Run definition 21.6 on $Int and Int \to Int, Int \times Int and (Int \to Int) \times Int,$ and on two arrows with the same result. Give the common supertype in every rejected case.

Referenced from 3 locations

Bidirectional elaboration

Disjointness removes ambiguity between the components of a well-formed intersection. It does not choose the type of an unannotated application such as $(succ,, id) (3,, (λ x . x))$ . The program could demand an integer or a function at intermediate points. The source therefore synthesizes a unique type and requires annotations at the remaining choice points.

Definition 21.9 — Elaborating bidirectional typing ¶

The judgments $Γ ⊢ e \Rightarrow A ⇝ M, Γ ⊢ e \Leftarrow A ⇝ M$ mean that $e$ synthesizes $A$ , or checks against $A$ , while producing target term $M$ . Their rules are

x : A \in Γ

Γ ⊢ x \Rightarrow A ⇝ x

I-Var

Γ ⊢ n \Rightarrow Int ⇝ n

I-Int

Γ ⊢ e_{1} \Rightarrow A ⇝ M_{1}

Γ ⊢ e_{2} \Rightarrow B ⇝ M_{2}

Γ ⊢ (e_{1}, e_{2}) \Rightarrow A \times B ⇝ (M_{1}, M_{2})

I-Pair

Γ ⊢ e_{1} \Rightarrow A \to B ⇝ M_{1}

Γ ⊢ e_{2} \Leftarrow A ⇝ M_{2}

Γ ⊢ e_{1} e_{2} \Rightarrow B ⇝ M_{1} M_{2}

I-App

Γ ⊢ e \Rightarrow A_{1} \times A_{2} ⇝ M

Γ ⊢ π_{i} e \Rightarrow A_{i} ⇝ π_{i} M

I-Proj

Γ ⊢ e_{1} \Rightarrow A ⇝ M_{1}

Γ ⊢ e_{2} \Rightarrow B ⇝ M_{2}

A * B

Γ ⊢ e_{1},, e_{2} \Rightarrow A & B ⇝ (M_{1}, M_{2})

I-Merge

Γ ⊢ e \Leftarrow A ⇝ M

Γ ⊢ (e : A) \Rightarrow A ⇝ M

I-Ann

Γ, x : A ⊢ e \Leftarrow B ⇝ M

Γ ⊢ λ x . e \Leftarrow A \to B ⇝ λ x . M

I-Lam

Γ ⊢ e \Rightarrow A ⇝ M

A <: B ⇝ c

Γ ⊢ e \Leftarrow B ⇝ c M

I-Sub

All types appearing in a derivation are required to be well formed. In particular, I-Merge checks the same disjointness condition as WF- $&$ .

Referenced from 4 locations

The running merge synthesizes $Int & (Int \to Int)$ : $\frac{\begin{matrix} Γ ⊢ 1 \Rightarrow Int ⇝ 1 \\ \frac{Γ ⊢ λ x . x \Leftarrow Int \to Int ⇝ λ x . x}{Γ ⊢ (λ x . x : Int \to Int) \Rightarrow Int \to Int ⇝ λ x . x} I - Ann \\ Int * (Int \to Int) \end{matrix}}{Γ ⊢ 1,, (λ x . x : Int \to Int) \Rightarrow Int & (Int \to Int) ⇝ (1, λ x . x)} I - Merge .$ Checking this term against $Int$ appends the unique coercion $λ p . π_{1} p$ , so its target is $(λ p . π_{1} p) (1, λ x . x)$ .

Lemma 21.10 — Unique coercions ¶

If well-formed types satisfy $A <: B ⇝ c_{1}$ and $A <: B ⇝ c_{2}$ , then $c_{1}$ and $c_{2}$ are alpha equal.

Referenced from 6 locations

Proof of Lemma 21.10 — Unique coercions

Proof. Induct on the total number of constructors in $A$ and $B$ . If $B = B_{1} & B_{2}$ , the ordinary premises exclude both left rules, so both derivations end in S- $&$ R; the induction hypotheses identify the two component coercions. If $A = A_{1} & A_{2}$ and $B$ is ordinary, the last rule is one of the two left rules. Both derivations cannot choose different projections by lemma 21.5; when they choose the same projection, the induction hypothesis identifies their premises. For equal ordinary heads, inversion fixes S-Int, S-Arr, or S-Prod, and the component induction hypotheses identify every subcoercion. Distinct ordinary heads have no derivation. Thus every possible last-rule pair has equal target syntax up to bound names. ◻

Lemma 21.11 — Unique synthesis ¶

If $Γ ⊢ e \Rightarrow A ⇝ M$ and $Γ ⊢ e \Rightarrow B ⇝ N$ , then $A = B$ .

Referenced from 4 locations

Proof of Lemma 21.11 — Unique synthesis

Proof. Induct on $e$ . A variable has its unique context entry and an integer has type $Int$ . Pair and merge types are fixed by the two induction hypotheses. An annotation writes its result type. For application, the function induction hypothesis fixes the whole arrow and hence its codomain; checking the argument does not choose a result type. Projection is fixed by the synthesized product. A bare lambda has no synthesis rule. These cases cover the source grammar. ◻

Theorem 21.12 — Elaboration preserves types ¶

If $Γ ⊢ e \Rightarrow A ⇝ M$ , then $| Γ | ⊢ M : | A |$ .
If $Γ ⊢ e \Leftarrow A ⇝ M$ , then $| Γ | ⊢ M : | A |$ .

Referenced from 4 locations

Proof of Theorem 21.12 — Elaboration preserves types

Proof. Use rule induction on the combined bidirectional judgment. Variables, integers, pairs, applications, projections, and lambdas use the corresponding target typing rule and the induction hypotheses. Rule I-Merge creates a target pair of type $| A | \times | B | = | A & B |$ . Rule I-Ann uses its checking induction hypothesis. In I-Sub, lemma 21.3 gives $c : | A | \to | B |$ , so target application types $c M$ at $| B |$ . ◻

Theorem 21.13 — Coherence of the frozen elaboration ¶

For well-formed contexts and types:

if $Γ ⊢ e \Rightarrow A ⇝ M$ and $Γ ⊢ e \Rightarrow B ⇝ N$ , then $A = B$ and $M$ and $N$ are alpha equal;
if $Γ ⊢ e \Leftarrow A ⇝ M$ and $Γ ⊢ e \Leftarrow A ⇝ N$ , then $M$ and $N$ are alpha equal.

Referenced from 5 locations

Proof of Theorem 21.13 — Coherence of the frozen elaboration

Proof. Induct on the first derivation, proving both clauses together. Every synthesis rule is determined by the outer source term. Its mate must use the same rule, and the induction hypotheses identify its premise elaborations. In I-App, lemma 21.11 fixes the function’s arrow domain before the checking induction hypothesis is applied to the argument. In I-Merge, the source syntax fixes left and right order; disjointness is a proposition and contributes no target term.

For checking, a lambda must use I-Lam; alpha-rename both target binders to one fresh variable and apply the body induction hypothesis. A nonlambda must use I-Sub. Unique synthesis fixes its intermediate type, the synthesis induction hypothesis fixes its target term, and lemma 21.10 fixes the inserted coercion. Thus the two applications are alpha equal. No other last rules are possible. ◻

Corollary 21.14 — Safety and deterministic meaning ¶

If $\cdot ⊢ e \Leftarrow A ⇝ M$ , then target evaluation of $M$ either continues or ends in a target value of type $| A |$ ; it never gets stuck. Any other derivation of the same checking judgment produces the same target program up to alpha equality and hence the same value.

Referenced from 3 locations

Proof of Corollary 21.14 — Safety and deterministic meaning

Proof. Target typing follows from theorem 21.12. For preservation of one target step, induct on its evaluation context. At a root step, the substitution lemma proves the beta case, and inversion of DT-Pair proves the two projection cases. Every context case rebuilds the same typing rule around the induction hypothesis.

For progress, induct on a closed target typing derivation. The variable case is impossible. Integers and lambdas are values. A pair either is a value or one of its components steps in the displayed left-to-right contexts. In an application, the function steps, the argument steps after the function is a value, or arrow canonical forms make the function a lambda and beta contraction applies. A projection first steps its scrutinee; when the scrutinee is a value, product canonical forms make it a pair and projection contraction applies. Iteration of these two lemmas gives target safety. If $\cdot ⊢ e \Leftarrow A ⇝ N$ is another derivation, theorem 21.13 makes $M$ and $N$ alpha equal; deterministic call-by-value evaluation preserves alpha equality at every step. ◻

What the side conditions exclude

Drop the disjointness premises from both I-Merge and WF- $&$ . Then $\cdot ⊢ 1,, 2 \Rightarrow Int & Int ⇝ (1, 2) .$ Both left subtyping rules apply when the result is checked against $Int$ : $λ p . π_{1} p and λ p . π_{2} p .$ Their applications to $(1, 2)$ evaluate to different integers. This counterexample removes only the two occurrences of the same disjointness condition; the syntax, target, evaluation order, and annotation discipline remain unchanged.

Annotations remove a different ambiguity. Even when both merges are disjoint, the source term $\begin{aligned} ((λ x . x : Int \to Int),, (λ x . x : (Int \to Int) \to (Int \to Int))) \\ (1,, (λ x . x : Int \to Int)) . \end{aligned}$ does not synthesize: its function position has an intersection type rather than a unique arrow. Annotating that position with the intended arrow makes the demanded projection explicit. Disjointness chooses a component once a type is demanded; it does not infer which demand the programmer intended.

Exercise 21.2 ¶

★☆☆ Write the two complete elaboration derivations for $(1,, 2 : Int)$ after deleting the disjointness premises from I-Merge and WF- $&$ . Reduce both target terms to values.

Referenced from 3 locations

Exercise 21.3 ¶

★★☆ Delete the ordinary-target premise from the two left subtyping rules. For a well-formed $A & B$ , construct a subtype query with an intersection target for which a left rule and S- $&$ R produce different target coercions. Show that both coercions typecheck, and identify the first metatheorem in this chapter that fails.

Referenced from 3 locations

Exercise 21.4 ¶

★★☆ Assume $A, B, C$ are pairwise disjoint. Derive coercions from $(A & B) & C$ and $A & (B & C)$ to $B$ . The target pair shapes differ; explain why theorem 21.13 does not identify programs whose source types are merely isomorphic.

Referenced from 3 locations

The theorem boundary is now exact. It covers the top-free grammar, well-formed disjoint intersections, the displayed coercive subtyping rules, and the bidirectional annotation discipline. It does not cover unrestricted merges, union types, polymorphism, either top-like variant, or later disjoint-intersection calculi.

Sources.

The calculus, simple-disjointness definition, algorithmic characterization, pair elaboration, and coherence boundary follow [OSA16]. The authors study three variants; this chapter deliberately uses only their top-free one. The pinned paper artifact and later thesis in the local dossier are corroborating material, not sources for a stronger theorem.

Suggested first pass.

Problems exercise 21.5, exercise 21.7, and exercise 21.9.

Exercise 21.5 ¶

★☆☆ Derive the elaboration of $(1,, (λ x . x : Int \to Int) : Int \to Int) 2$ and reduce the target program.

Referenced from 4 locations

Exercise 21.6 ¶

★★☆ Prove directly from (21.1) that two arrow types are disjoint exactly when their result types are disjoint. In the reverse direction, use the intersection of the two domains to build a common domain.

Referenced from 3 locations

Exercise 21.7 ¶

★★☆ Construct incomparable types $A, B$ with a common ordinary supertype $C$ . Choose closed terms of types $A, B$ whose coercions to $C$ produce different observations. This must refute the weaker test $A ≮: B \land B ≮: A$ , not merely repeat $Int & Int$ .

Referenced from 4 locations

Exercise 21.8 ¶

★★★ Reconstruct lemma 21.10 as a last-rule comparison table. For every pair of potentially overlapping rules, record whether the pair is excluded by ordinary targets, by lemma 21.5, or by outer-constructor inversion.

Referenced from 3 locations

Exercise 21.9 ¶

★★★ Practical project.disjoint-merge-checker Implement the frozen type grammar, algorithmic disjointness, coercive subtyping, merge formation, and ordinary-target contributor selection. Maintain the invariant that an accepted ordinary demand has at most one contributing branch. On the named corpus, accept $Int & (Int \to Int)$ , reject $Int & Int$ , classify arrows by their results, and print the two distinct projections obtained by deliberately disabling the disjointness check. Include the nested-product demand $Int \times (Int & (Int \to Int)) <: Int \times Int,$ which must select the left branch of a disjoint merge with $Int \to Int$ . Also test distribution through an intersection on each side of algorithmic disjointness. Acceptance is the eight named PASS lines and final summary recorded in appendix E.

Referenced from 5 locations