ch:dimension-types: ch:dimension-types

Use additive exponent arithmetic inside the multiplicative notation: The exponent of $\delta$ is $-2+2=0$, so the dimension variable cancels. The remaining base exponents are $L:2$ and $T:-2$.

Similarly, Here $L$ cancels. The surviving base exponents are $M:1$ and $T:-1$.

Give $x$ type $\mathsf{Num}[\delta ]$. Two variable leaves and D-Mul give $$\frac{\begin{array}{c}x:\mathsf{Num}[\delta ]⊢x:\mathsf{Num}[\delta ]\\ x:\mathsf{Num}[\delta ]⊢x:\mathsf{Num}[\delta ]\end{array}}{x:\mathsf{Num}[\delta ]⊢x\ast x:\mathsf{Num}[{\delta }^2]}\mathrm{D}-\mathrm{Mul}.$$ Lambda introduction yields $$⊢\lambda x.x\ast x:\mathsf{Num}[\delta ]\to \mathsf{Num}[{\delta }^2].$$ Since $\delta$ is absent from the empty context, generalization gives $$\mathsf{square}:\mathrm{\forall }\delta .\mathsf{Num}[\delta ]\to \mathsf{Num}[{\delta }^2].$$

For the second term, run the algorithm rather than guessing its argument types. The two lambda clauses begin with fresh ordinary variables $x:\alpha$ and $y:\beta$. The multiplication clause introduces fresh dimension variables ${\delta }_1,{\delta }_2$ and generates $$\alpha \doteq \mathsf{Num}[{\delta }_1],\beta \doteq \mathsf{Num}[{\delta }_2].$$ For the division, its left operand has dimension ${\delta }_1{\delta }_2$, while the second occurrence of $y$ is already forced to $\mathsf{Num}[{\delta }_2]$. Renaming the two principal dimension parameters to $\delta ,ϵ$, the algorithm returns Thus the two lambdas have type $$\mathsf{Num}[\delta ]\to \mathsf{Num}[ϵ]\to \mathsf{Num}[\delta ],$$ and both dimension variables are generalized: $$\mathrm{\forall }\delta \mathrm{\forall }ϵ.\mathsf{Num}[\delta ]\to \mathsf{Num}[ϵ]\to \mathsf{Num}[\delta ].$$ Only the dimension annotation was normalized. The source term still contains the multiplication and division by $y$, so at run time division by zero can still produce $\mathsf{aritherr}$.

The lambda clause first gives $x$ a fresh ordinary type variable $\alpha$. The two variable calls return $\alpha$. The multiplication clause chooses fresh dimension variables ${\delta }_1,{\delta }_2$ and generates $$\alpha \doteq \mathsf{Num}[{\delta }_1],\alpha \doteq \mathsf{Num}[{\delta }_2].$$ Eliminating $\alpha$ leaves ${\delta }_1{=}_D{\delta }_2$. Its principal dimension solution names their common value by a fresh parameter $\eta$; equivalently the combined substitution sends $\alpha$ to $\mathsf{Num}[\eta ]$ and both ${\delta }_i$ to $\eta$. Thus the bound expression has monotype and generalized scheme $$\lambda x.x\ast x:\mathsf{Num}[\eta ]\to \mathsf{Num}[{\eta }^2],s:\mathrm{\forall }\eta .\mathsf{Num}[\eta ]\to \mathsf{Num}[{\eta }^2].$$ At the first application $s(3@\mathsf{m})$, instantiate $\eta$ by a fresh dimension variable ${\theta }_1$ and choose the application result variable ${\beta }_1$. Unifying $$\mathsf{Num}[{\theta }_1]\to \mathsf{Num}[{\theta }_1^2]\doteq \mathsf{Num}[L]\to {\beta }_1$$ generates the dimension equation ${\theta }_1{=}_{D}L$ and the type equation ${\beta }_1\doteq \mathsf{Num}[{\theta }_1^2]$. The resulting principal substitution sends ${\theta }_1$ to $L$ and ${\beta }_1$ to $\mathsf{Num}[L^2]$, so the inner let binds $a:\mathsf{Num}[L^2]$.

The second occurrence of $s$ is instantiated independently, with fresh ${\theta }_2,{\beta }_2$. Unifying $$\mathsf{Num}[{\theta }_2]\to \mathsf{Num}[{\theta }_2^2]\doteq \mathsf{Num}[T]\to {\beta }_2$$ generates ${\theta }_2{=}_{D}T$ and ${\beta }_2\doteq \mathsf{Num}[{\theta }_2^2]$. Its principal substitution sends ${\theta }_2$ to $T$ and ${\beta }_2$ to $\mathsf{Num}[T^2]$. Therefore the whole term has type $\mathsf{Num}[T^2]$. The four variables ${\theta }_1,{\beta }_1,{\theta }_2,{\beta }_2$ are pairwise distinct, while the scheme for $s$ is generalized once.

Both literals have dimension $L$. Their canonical coefficients in meters are $$12s_{\mathsf{inch}}=12\cdot \frac{127}{5000}=\frac{381}{1250},1s_{\mathsf{ft}}=\frac{381}{1250}.$$ Therefore elaboration produces $${\mathrm{elab}}_{\mathcal{U}}(D_{12\mathsf{in}+1\mathsf{ft}})={\overline{381/1250}}_L+{\overline{381/1250}}_L.$$ Here $D_{12\mathsf{in}+1\mathsf{ft}}$ is the syntax-directed derivation of $12@\mathsf{inch}+1@\mathsf{ft}$. Both core operands have annotation $L$, so the C-Add root reduces $${\overline{381/1250}}_L+{\overline{381/1250}}_L⟶{\overline{762/1250}}_L={\overline{381/625}}_L.$$ Hence the canonical result is $381/625$ meters, or $0.6096$ meters.

The coherent change of coordinates extends multiplicatively, hence $$\chi (ML{T}^{-2})=\chi (M)\chi (L)\chi (T{)}^{-2}=1000\cdot 100\cdot 1^{-2}=100000.$$ The coefficient $3$ therefore becomes $300000$ in gram–centimeter–second coordinates. Directly, $$3\mathsf{kg}\mathsf{m}{\mathsf{s}}^{-2}=3(1000\mathsf{g})(100\mathsf{cm}){\mathsf{s}}^{-2}=300000\mathsf{g}\mathsf{cm}{\mathsf{s}}^{-2},$$ which agrees with the invariance theorem.

Orient the first equation at the flexible ordinary variable and eliminate it: $$\alpha \mapsto \mathsf{Num}[\delta ].$$ Applying this substitution to the second equation leaves the numeric equation $\mathsf{Num}[\delta ]\doteq \mathsf{Num}[L]$, hence the dimension store is $\delta {=}_{D}L$. Its deterministic Smith solve returns $\delta \mapsto L$. Composition therefore gives $$\rho =\{\alpha \mapsto \mathsf{Num}[L],\delta \mapsto L\}.$$ Replay yields $$\alpha [\rho ]=\mathsf{Num}[L]=\mathsf{Num}[\delta ][\rho ],\alpha [\rho ]=\mathsf{Num}[L]=\mathsf{Num}[L][\rho ].$$ Now let $R$ solve both input equations. Ordinary-type constructor injectivity gives $R(\alpha )=\mathsf{Num}[R(\delta )]$ from the first equation and $R(\alpha )=\mathsf{Num}[L]$ from the second. Numeric constructor injectivity and normalized dimension equality give $R(\delta )=L$, hence $R(\alpha )=\mathsf{Num}[L]$. Take $T=R$. On the problem-variable set $\{\alpha ,\delta \}$, the required factorization is $$R{\upharpoonright }_{\{\alpha ,\delta \}}=(\rho ;T){\upharpoonright }_{\{\alpha ,\delta \}},$$ which is the required factorization.

Apply three recorded column operations: The corresponding column matrices give Direct multiplication checks $$[46]V=[20].$$ The determinant of $V$ is $1$, so this is a unimodular change of coordinates. Put $z=(\delta ,ϵ{)}^{\mathsf{T}}$ and $z=V{z}^{\prime }$. The Smith equation has pivot $2$ and right side $L^2$, hence $z_1^{\prime }=L$; write the free coordinate as $z_2^{\prime }=\eta$. Therefore $$\delta \mapsto L^2{\eta }^{-3},ϵ\mapsto L^{-1}{\eta }^2.$$ Substitution checks the answer: $$(L^2{\eta }^{-3}{)}^4(L^{-1}{\eta }^2{)}^6\stackrel{\text{distribute powers}}{=}{L}^8{\eta }^{-12}{L}^{-6}{\eta }^{12}\stackrel{\text{collect exponents}}{=}{L}^2.$$ Every solution is obtained by choosing $\eta$, because the second column of $V$ spans the integer kernel. Replacing the right side by $L$ makes the transformed pivot equation $(z_1^{\prime }{)}^2=L$. At generator $L$, the pivot $2$ does not divide the right-hand exponent $1$, so no dimension substitution exists.

If source addition is to elaborate homomorphically, then for all $p,q$, $$a(p+q)+b=(ap+b)+(aq+b)=a(p+q)+2b.$$ Thus $b=2b$, so $b=0$; conversely $b=0$ makes the equation immediate. Celsius-to-Kelvin conversion has $a=1$ and $b=27315/100$, so it does not preserve addition and cannot be a unit scale in definition 6.3. In a calculus extended with subtraction, differences would cancel the offset: $(p+b)-(q+b)=p-q$. Such an extension must distinguish affine temperature points, on which subtraction produces a difference, from vector- like temperature differences, on which addition and scaling remain valid.