Non-definability: why pow must be primitive #
pow is a primitive constructor of Λs. The justification has been an
argument in prose: from an argument at u² and literals at 1, closure under
+ − × ÷ reaches exactly the subgroup generated by u², and u is not in it.
This file makes that a theorem.
Why the fundamental theorem is not enough #
Applying scaleLaw to a hypothetical term of type Q (u·u) → Q u gives
f(k²x) = k·f(x) for every k > 0, hence f(y) = √y · f(1) for y > 0. So
parametricity says any such function is a multiple of square root on
positive inputs; it does not say none exists. That is
exactly why Kennedy needs a strengthening for his semantic proof: "a more
generous notion of scaling environment (homomorphisms from subgroups of Unt)".
The shortcut #
The theorem governs the arithmetic fragment: terms built from variables,
rational literals, and the field operations, with no pow, no ucon, and no
recursion. (Λs has no rec at all, and its one branching form, ifle, is
outside this fragment.) Over that fragment a syntactic argument suffices and
gives a stronger conclusion: the fragment's type is uninhabited, not merely
uncomputable.
The key observation is that mul and div add and subtract exponent vectors,
so the reachable units form the ℤ-span of the arguments' units, not the
ℚ-span. Over ℚ we would have u = (u²)^(1/2) and the argument would collapse;
over ℤ, u ∉ {u^(2n)}. The argument turns entirely on the distinction between
what the unit algebra permits and what the term grammar can build, which is
why rational powers have to be given rather than derived.
Would recursion rescue square root? #
We might think the result stands only because Λs lacks recursion:
given a fixpoint construct, we could write the standard functional
implementation of Newton's method and compute square roots. Where would it
break? Not in the loop. The iteration x_(n+1) = (x_n + a/x_n)/2 is
unit-correct at every step: from x_n : Q u and a : Q u² we obtain
a/x_n : Q u, and the mean of two quantities at Q u is again at
Q u. The break is at the entry point. The iteration needs a seed
x₀ : Q u, and within the arithmetic fragment the theorem governs, no
term manufactures one from a : Q u²; that is the non-definability
theorem itself, and the artifact records this reading
(no_newton_seed; at the term grammar,
no_newton_seed_tm).
The full calculus, however, does offer a seed:
1_u inhabits Q u in any context. Does the seed defeat the
theorem? Run the seeded program on a = 4 m² and watch what the
seed costs. Measured in meters, one step from 1_u gives
(1 + 4/1)/2 = 2.5. Measured in centimeters, the same quantity is
40000 cm², and the same step gives 20000.5, which is
200.005 meters. The ideal square root commutes with rescaling, since
√(k² x) = k√x; iterates from a seed that itself rescaled
would commute too. But 1_u denotes 1 in every unit system
(it names a unit, exactly what parametricity excludes,
“The Price of Conversion” (Fundamental.lean)), so every finite run of the seeded program
depends on the unit system. Nor does a cleverer constant help: any
expressible seed q · 1_u denotes the fixed number q
everywhere, and what commuting with rescaling needs is not a better
constant but a seed
that transforms.
The obstruction is exact. Still supposing a fixpoint construct added, terminating runs of a recursive arithmetic program are piecewise rational in their inputs, and square root is not a rational function, so no definable program computes it exactly, whatever its seed strategy. The argument quantifies over the whole program, so it covers seeds tuned by hand, computed from a, or supplied as q · 1_u for any q.
For a positive input a, the relative stopping condition
|x_n² - a|/a < ε bounds the relative squared residual. It does not by itself
prove a bound on differences between outputs computed in rescaled unit systems.
An absolute residual threshold must have unit u²: a literal tolerance is a
multiple of 1_(u²), which contains a unit constant and is not parametric.
A tolerance supplied as an input instead rescales with its unit. The distinction
is how the tolerance is supplied, not whether it is absolute. The drift analysis
of Twist declines terms containing unit constants.
Supplying the seed gives the iteration body type Q u² → Q u → Q u.
That body, and every fixed finite unrolling of it, is parametric and invariant
by fundamental_free: an input seed rescales with the other inputs. Λs has no
recursion construct, so extending this result to recursive execution requires
an additional semantic argument. The discussion of recursive arithmetic above
is a mathematical interpretation, not a mechanized extension of the calculus.
The primitive rational power provides an exact real denotation; the numerical
accuracy of a chosen iteration and stopping rule is a separate question.
Rational powers of a single unit #
The reachable units #
InSpan S u says u can be built from the units in S using exactly the
operations the term grammar provides: the trivial unit (from a literal), the
generators (from variables), and multiplication and division.
The units reachable from S by the operations of the arithmetic fragment.
- one
{B : Type}
{k : ℕ}
{S : List (UExp B k)}
: InSpan S 1
A literal contributes the trivial unit.
- gen
{B : Type}
{k : ℕ}
{S : List (UExp B k)}
{u : UExp B k}
: u ∈ S → InSpan S u
A variable contributes its own unit.
- mul {B : Type} {k : ℕ} {S : List (UExp B k)} {u v : UExp B k} : InSpan S u → InSpan S v → InSpan S (Term.mul u v)
- div {B : Type} {k : ℕ} {S : List (UExp B k)} {u v : UExp B k} : InSpan S u → InSpan S v → InSpan S (Term.div u v)
Instances For
The square root of a unit is unreachable.
If u is nontrivial, then u is not in the span of u²: it would have to be
u^(2n) for an integer n, and 1 - 2n is a nonzero integer, so every
exponent of u (base or variable) would be zero. The hypothesis is exactly
u ≠ 1: a bare unit variable, the ∀u. Q u² → Q u reading, is covered.
The arithmetic fragment, intrinsically typed by its unit #
Expressions of the arithmetic fragment over a context of scalar units, indexed by the unit of their result: literals, variables, and the field operations.
- var {B : Type} {k : ℕ} {S : List (UExp B k)} {u : UExp B k} : u ∈ S → Arith S u
- lit {B : Type} {k : ℕ} {S : List (UExp B k)} : ℚ → Arith S 1
- mul {B : Type} {k : ℕ} {S : List (UExp B k)} {u v : UExp B k} : Arith S u → Arith S v → Arith S (Term.mul u v)
- div {B : Type} {k : ℕ} {S : List (UExp B k)} {u v : UExp B k} : Arith S u → Arith S v → Arith S (Term.div u v)
- add {B : Type} {k : ℕ} {S : List (UExp B k)} {u : UExp B k} : Arith S u → Arith S u → Arith S u
Instances For
Square root is not definable.
Given only a quantity of unit u², no arithmetic expression has unit u. The
type is uninhabited: not merely hard to reach, and not merely uncomputable.
So pow is not a convenience. Without it the field operations cannot express
the square root of a dimensioned quantity at all, because no expression they
build has the right unit. (For full Λs the syntactic claim needs the caveat that
ucon inhabits Q u in any context, so the type is inhabited; what this
result pins down is that arithmetic alone never reaches the unit.) Together with
the admissibility criterion (a primitive may take any type whose denotation is
scale-invariant, and √ is, by sqrt_scales) this says pow is both necessary and
permitted.
The same statement for Newton's iteration, which is where the intuition
usually goes. The iteration itself is well-typed ((x + a/x)/2 has unit u
whenever x does), but no seed of unit u exists to start it, so the whole
construction is unavailable. This is the hint to Exercise 14 of Kennedy's 2009 lecture notes, in miniature.
Lifting to the term grammar of Λs itself #
sqrt_not_definable speaks about Arith, a grammar defined in this file. The
design claim is about Λs: no term of the calculus built from variables,
rational literals, multiplication, division, and addition computes a square
root. This section closes the gap between the two. Tm.ArithOnly carves the
arithmetic fragment out of Tm, in the style of Tm.Parametric and
Tm.ConvertFree; arith_of_hasTy reflects every typing derivation of an
arithmetic term over a scalar context into Arith; and the grammar-level
theorem then transfers verbatim.
The caveat recorded at sqrt_not_definable, that ucon inhabits Q u in any
context so the bare type is inhabited, disappears here: ucon is not an
arithmetic operation and ArithOnly excludes it, so the term-level statement
needs no qualification.
A term of Λs lies in the arithmetic fragment when it is built from
variables, rational literals, multiplication, division, and addition, and
nothing else. In particular ucon, pow, convert, log, exp, and every
binder and application form are excluded. Same style as Tm.Parametric and
Tm.ConvertFree: a predicate on terms, not on derivations, which by uniqueness
of derivations loses nothing.
Equations
Instances For
Reflection. A typing derivation of an arithmetic term over a scalar
context lands in the Arith grammar. scalarCtx us assigns type Q us[n] to
de Bruijn variable n, and Arith.var records only membership of the unit in
the context, so the variable case collapses to a lookup. Everything else is the
observation that each arithmetic typing rule is an Arith constructor.
Square root is not definable in Λs. The paper's sentence, at the
calculus's own term grammar: given a single argument of unit u² with u ≠ 1, no Λs term
built from variables, rational literals, and the field operations has type
Q u. This is sqrt_not_definable lifted from the self-contained Arith
grammar to Tm via the reflection, and the ucon caveat is gone because
ArithOnly excludes ucon.
The Newton-iteration reading at the term level: any well-typed Λs candidate
for a seed of unit u from an argument at u² must step outside the field
operations. The iteration body (x + a/x)/2 is well-typed at Q u; the seed
is what cannot be written.
Conversion is not definable either #
The results above concern sqrt, and there they are weaker than the literature:
Atkey, Johann and Kennedy (POPL'13, Examples 6 and 8) prove non-definability of
square root semantically, in Coq, and go further: cube root stays undefinable
even if square root is added as a primitive.
This section proves something their framework cannot state, because their
calculus has no operation that reads a unit: convert is a genuine
primitive. Any parametric, convert-free closed term of type Q u → Q v
denotes zero whenever some scaling fixes u and moves v. Parametricity
matters, since λx. (x / ucon u) · ucon v is convert-free and denotes the
identity at that type. So conversion is not definable from the other
constructs, and the coherence hypothesis on fundamental is the price of a
primitive the calculus needs rather than of a redundant feature.
The proof is the semantic one (apply fundamental_free at a scaling that
fixes u and moves v), which is exactly AJK's technique, used on a question
that only arises once conversion exists.
The scale factor of a bare generator is the exponential of its entry.
A scaling that fixes one generator and doubles another. Two base units of the
same dimension are separated by such a scaling, which is exactly the freedom
Scaling.Coherent forbids, and the freedom that makes conversion observable.
Equations
Instances For
Conversion cannot be simulated. A parametric, convert-free closed term of
type Q u → Q v denotes the zero function as soon as one scaling fixes u and
moves v.
This is the statement fundamental_free was built to make: no coherence
hypothesis, so ψ may be chosen adversarially, and the adversarial choice
collapses the function.
So convert is primitive. No parametric, convert-free closed term denotes
conversion between two distinct base units, because conversion is multiplication
by a positive factor and every such term denotes zero (convertFree_eq_zero).
Together with fundamental this is the design claim, proved in both
directions: conversion cannot be removed from the language, and keeping it costs
exactly coherence.