Dimension Types and Units of Measure

Proof. Pointwise integer addition is associative and commutative, the zero map is its identity, and $d+(-d)=0$ pointwise for every exponent map $d$. For the homomorphism law, add the two exponents belonging to each generator: Negating every exponent in the same formula gives $d^{-1}[\rho ]=d[\rho {]}^{-1}$. If $d{=}_{D}e$, then $d(g)=e(g)$ for every generator $g$; substituting those equal coefficients in the same formula gives $d[\rho ]{=}_{D}e[\rho ]$. For freeness, choose arbitrary images $h_g$ of the generators in an abelian group $H$, and define $$\varphi (d)=\prod _{g\in \mathcal{B}\cup D}{h}_g^{d(g)}.$$ The product is finite because $d$ has finite support. The calculation just used for substitution proves that $\varphi$ is a homomorphism. Every $d$ is the displayed finite product of generator powers; hence any homomorphism with the chosen generator images must have the displayed value $\varphi (d)$. This proves uniqueness. ◻

Proof. For the left-to-right direction, induct on the declarative typing derivation. Handle Inst and Gen as in theorem 3.34, first alpha-renaming the quantified ordinary and dimension variables away from every variable already in the derivation. In an arithmetic case, the induction hypotheses give syntax-directed premises at the numeric types shown in that rule; reapply the same arithmetic rule. A final D-Conv disappears because normalized dimensions satisfying $d{=}_D{d}^{\prime }$ are the same finite map, and the structural definition of type equivalence never changes an outer constructor. For the right-to-left direction, insert the declarative HM rules and reuse each arithmetic rule unchanged. ◻

Proof. Inspect the three defining clauses. Equal variables have the same variable head. For arrows, the definition compares the domains and codomains. For numeric types, it compares only their dimension annotations. No clause relates two different outer constructors. ◻

Proof. Bézout’s identity gives $p,q\in \mathbb{Z}$ with $pa+qb=g$. Take Its determinant is $(pa+qb)/g=1$, and direct multiplication gives both displayed equations. Thus the row or column pair $(a,b)$ can be replaced by $(g,0)$ using invertible integer operations. ◻

Proof. Move a nonzero entry to the upper-left corner. Apply lemma 6.9 successively to the pivot and each other entry of its column using row operations, then to the pivot and each other entry of its row using column operations. The row operations that clear the first column may reintroduce entries to the right of the pivot; the column operations that clear the first row may reintroduce entries below it. We therefore alternate these two clearing phases. If a phase exposes an entry not divisible by the positive pivot, the next two-entry reduction replaces that pivot by a strictly smaller gcd. If every exposed entry is divisible by the pivot, subtracting the corresponding integral multiples clears it without changing the pivot or the already-clear companion line. Thus either the pivot strictly decreases or both the first row and first column become clear. Only finitely many decreases are possible, so the process ends with a clear first row and column and a positive pivot $d$.

Suppose an entry $a$ of the remaining block is not divisible by $d$. Add its column to the first column. That first column now contains both $d$ and $a$. The two-entry reduction replaces the pivot by ; clear the first row and column again. Each repair strictly decreases the positive pivot, so only finitely many repairs occur. At termination the pivot divides every entry of the remaining block. ◻

Proof. Induct on $min(m,n)$. The zero matrix is already in the required form. For a nonzero matrix, lemma 6.10 gives Apply the induction hypothesis to $M_1$, using operations confined to its rows and columns. Because every entry of $M_1$ is a multiple of $s_1$, all integer combinations created by those operations remain multiples of $s_1$. The first new positive pivot $s_2$ is therefore divisible by $s_1$; the same argument repeats in each smaller block. This produces and a zero residual block.

Every operation used in lemma 6.9, lemma 6.10 has a unimodular elementary matrix. Multiplying the recorded row matrices and column matrices gives $U$ and $V$. Only existence of this diagonal form is used below; uniqueness of its invariant factors is not claimed here. ◻

Proof. Invertible integer row operations preserve the solution set of $Mz=c$, and the change of variables $z=V{z}^{\prime }$ is bijective because $V^{-1}$ is integral. The diagonal system separates into equations $(z_i^{\prime }{)}^{s_i}=c_i^{\prime }$. Such an equation has a solution in the free abelian group exactly when $s_i$ divides every generator coefficient of $c_i^{\prime }$; a zero row reads $1=c_i^{\prime }$. These are precisely the failure tests in definition 6.12.

The dimension group is torsion-free: if $z^{s_i}=(z^{\prime }{)}^{s_i}$ for , then $z=z^{\prime }$, coefficient by coefficient in its free abelian basis. Hence a passing pivot equation has exactly one solution. Division fixes each pivot coordinate and the remaining coordinates are arbitrary. Naming them $\overline{\eta }$ gives ${\rho }_E$, so substitution back through $V$ proves soundness. Any solution of the diagonal system chooses values for exactly those free coordinates. Define $\psi$ by mapping each ${\eta }_i$ to the coordinate selected by $\theta$ and by fixing every declared rigid. Since $z=V{z}^{\prime }$ is bijective, substitution back gives $${\delta }_j[\theta ]={\delta }_j[{\rho }_E;\psi ](1\le j\le n).$$ Because the matrix construction never substitutes for a declared rigid, ${\rho }_E$ fixes ${\mathcal{G}}_{\mathrm{r}}$. This proves principality and completeness in the postfix convention of chapter 3. ◻

Proof. Smith reduction sends $D$ by invertible integer changes of basis to a matrix with $r$ nonzero pivots and $n-r$ zero columns: invertibility of $U,V$ over $\mathbb{Q}$ preserves rank, so the pivot count is $r$. Writing $UDV=S$ gives $Dv=0$ iff $S(V^{-1}v)=0$. Thus the last $n-r$ columns of $V$, rather than the literal zero columns of $S$, form a $\mathbb{Z}$-basis of the original integer kernel. Their coordinates freely parameterize that kernel, and $Dv=0$ says exactly that the monomial’s base-dimension exponents all vanish. This lattice statement is the integer-exponent form of the Buckingham $\pi$ theorem. ◻

Proof. Alpha-rename the finitely many parameters of ${\rho }_E$ away from $\mathrm{vars}(F)$ before forming the second problem. The renaming preserves the equations and the factorization clause of theorem 6.13. The composite fixes the common rigid set. It solves $E$ because every substitution composed after ${\rho }_E$ that fixes ${\mathcal{G}}_{\mathrm{r}}$ preserves its equations, and it solves $F$ because ${\rho }_F$ solves the image system. Let $\theta$ be a ${\mathcal{G}}_{\mathrm{r}}$-relative solution of $E\cup F$. Principality for $E$ factors $\theta {=}_{\mathrm{vars}(E)}{\rho }_E;\psi$; extend $\psi$ to agree with $\theta$ on variables occurring only in $F$. Then $\psi$ solves $F[{\rho }_E]$, so it factors through ${\rho }_F$. Composing the two factors gives the required factorization on the variables constrained by the second problem. If a fresh parameter $\eta$ introduced by ${\rho }_E$ does not occur in $F[{\rho }_E]$, then ${\rho }_F$ fixes it; extend the residual factor by $\eta \mapsto \eta [\psi ]$. If it does occur, the second factorization already determines the same image. This support extension preserves the first factorization and yields the required factorization through ${\rho }_E;{\rho }_F$ on every variable of $E\cup F$. ◻

Proof. Use the lexicographic triple from lemma 3.24 on the type equation list: its number of ordinary type variables, its constructor count, and its length. Ordinary-variable elimination and constructor decomposition decrease the first or second component. Moving a numeric equation to $D$ strictly shortens $E$; although $D$ grows, the procedure never recurses on that store. When $E$ is empty, Smith reduction terminates by lemma 6.11 and returns or fails. These clauses exhaust the recursion. ◻

Proof. Induct on the lexicographic termination measure of lemma 6.17. Maintain the stronger claim containing all four clauses.

Reflexive and arrow cases. A reflexive equation is deleted. An arrow equation is replaced by its domain and codomain equations. Structural type equality makes the old and new solution sets identical, so the induction hypothesis proves all four clauses.

Ordinary-variable elimination. Consider $\alpha \doteq \tau$ with $\alpha \notin \mathrm{ftv}(\tau )$. Every solution $Q$ satisfies $\alpha [Q]=\tau [Q]$ and therefore factors through $[\tau /\alpha ]$: define the residual to agree with $Q$ away from $\alpha$. Substitution of $[\tau /\alpha ]$ in the remaining equations is sound in both sorts because ordinary substitution acts structurally on every numeric type and leaves the dimension store sorted. Conversely, any solution of the substituted problem composed after $[\tau /\alpha ]$ solves the original equation and the remaining list. The occurs-check failure is exact: a finite type tree cannot equal a proper subtree containing itself. Orienting $\tau \doteq \alpha$ to this case does not change the solution set.

Numeric collection. Replacing $\mathsf{Num}[d]\doteq \mathsf{Num}[e]$ by $d{=}_{D}e$ in the store preserves the solution set by injectivity of the numeric type constructor. The induction hypothesis therefore applies to the shorter type list. Distinct outer constructors have no common instance by lemma 6.8, so constructor clash is exact failure.

Dimension store. When the type list is empty, theorem 6.13 gives soundness, exact failure, and factorization for the accumulated store. Its substitution is the identity off the store variables and its fresh parameters. Those parameters avoid $P$ because the initial dimension-supply counter is larger than every index occurring in $P$. This proves the support clause in theorem 6.18(4).

Composing the one-variable eliminations in their execution order with the final dimension substitution proves items 1–3 for the initial problem. For item 4, let $\gamma \in P\setminus \mathrm{vars}(E,D)$. The returned substitution fixes $\gamma$, so extend $R$ by $\gamma [R]:=\gamma [Q]$. This changes no problem-variable image and gives $\gamma [S;R]=\gamma [Q]$. Repeating the construction for the finite set $P$ proves protected factorization. ◻

Proof. Prove soundness and protected completeness simultaneously by induction on the source term. The strengthened completeness statement quantifies over every finite protected set $P$ fixed before the induction begins. At each syntax node, invoke ${\mathsf{munify}}_P$ with this same $P$. Every generated variable avoids $P$, the target substitution, and the target derivation, while theorem 6.18(4) preserves the inherited images of variables in $P$. The algorithm stated in definition 6.16 is the instance $P=\varnothing$.

Variable and abstraction. The variable clause instantiates its stored prefix with fresh variables. A target instance determines the residual images of exactly those variables; the two prefixes are first standardized apart. For an abstraction, assign its binder a fresh ordinary variable $\alpha$ and apply the induction hypothesis to the body while protecting the image of the ambient protected set. The returned type is $\alpha [S]\to \tau$, and type substitution applied to the premise reconstructs both soundness and the target arrow.

Application. The recursive calls give $$\mathrm{\Gamma }[S_1;S_2]⊢e_1:{\tau }_1[S_2],\mathrm{\Gamma }[S_1;S_2]⊢e_2:{\tau }_2.$$ The mixed unifier $U$ solves ${\tau }_1[S_2]\doteq {\tau }_2\to \beta$ by theorem 6.18(1). Applying $U$ to both derivations and using App yields result $\beta [U]$ under $\mathrm{\Gamma }[S_1;S_2;U]$. For completeness, the first protected induction hypothesis factors the target through $S_1$. Apply the second while also protecting $\mathrm{ftv}({\tau }_1)$ and $\mathrm{fdv}({\tau }_1)$; the target substitution then solves the application equation. Items 2 and 4 of theorem 6.18 factor it through $U$ without changing an inherited protected image.

Let. Soundness of the definition gives $\mathrm{\Gamma }[S_1]⊢e_1:{\tau }_1$. Generalize exactly the ordinary and dimension variables absent from $\mathrm{\Gamma }[S_1]$, apply $S_2$ to that declarative derivation, and combine it with the body induction hypothesis by Let. For completeness, standardize both quantified sorts away from the target derivation. The target instance determines their residual images, while the body induction hypothesis preserves the variables free in the substituted environment. No arithmetic premise is hidden in generalization.

Addition. Put ${\mathrm{\Gamma }}_{12U}=\mathrm{\Gamma }[S_1;S_2;U]$. The recursive soundness derivations, after the indicated substitutions, have types $${\mathrm{\Gamma }}_{12U}⊢e_1:{\tau }_1[S_2][U],{\mathrm{\Gamma }}_{12U}⊢e_2:{\tau }_2[U].$$ The exact equations solved by $U$ give $${\tau }_1[S_2][U]=\mathsf{Num}[\delta [U]]={\tau }_2[U].$$ Rule D-Add therefore derives the returned type. Conversely, inversion of a target D-Add derivation gives one dimension $d^{\prime }$ for both operands. The two protected induction hypotheses make the residual target substitution solve the same mixed equations. The factorization clauses of theorem 6.18 produce the required residual after $U$.

Multiplication and division. The same context ${\mathrm{\Gamma }}_{12U}$ types the operands at $${\tau }_1[S_2][U]=\mathsf{Num}[{\delta }_1[U]],{\tau }_2[U]=\mathsf{Num}[{\delta }_2[U]].$$ D-Mul and D-Div return, respectively, $$\mathsf{Num}[{\delta }_1[U]{\delta }_2[U]]\text{and}\mathsf{Num}[{\delta }_1[U]{\delta }_2[U{]}^{-1}].$$ In the reverse direction, inversion exposes the two target operand dimensions. Protected recursive factorization handles the recursive calls. Items 2 and 4 of theorem 6.18 factor the two numeric equations. The group-homomorphism laws preserve product and inverse in the result.