Skip to content

Commit 02b3971

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(formal): Wave 2 — the affine/QTT layer (QttSemiring + AffineUsage)
Mechanizes the algebraic core that makes AffineScript *affine*, advancing P-4 (docs/PROOF-NEEDS.adoc) from prose. Axiom-free (Print Assumptions closed; lia introduces no axioms); no Admitted. QttSemiring.v — the QTT quantity semiring {0,1,ω}: qplus (context addition; 1+1 = ω), qmult (scaling), all semiring laws (assoc/comm/identity/distributivity) + the usage order 0 ≤ 1 ≤ ω, by exhaustive case analysis. Plus the bridge `qof (m+n) = qplus (qof m) (qof n)` — occurrence counts add under QTT addition — and the affine fact `qplus One One = Omega` with `~ qle (qplus One One) One`. AffineUsage.v — affine usage over the semiring: usage x t := qof (count x t); proves usage composes through application (usage x (app f a) = qplus (usage x f) (usage x a), from qof_plus); defines affine well-formedness (every binder consumes its var at most once). Payoff: `λx.x` is affine, `λx. x x` is NOT (its variable totals ω, exceeding the affine bound) — the mechanized statement of "a linear value may not be duplicated". Scope: the full *typed* QTT calculus (context splitting Γ = Γ₁ + Γ₂, progress+preservation tracking quantities, on top of P2_Stlc) is the next increment. Track now 12 files, 18 closure reports, no axioms. justfile/_CoqProject build both; .hypatia-ignore extends the Coq-not-V-lang carve-out; README gains a "Wave 2" section; PROOF-NEEDS P-4 row prose → partial. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
1 parent 65c2ae3 commit 02b3971

7 files changed

Lines changed: 250 additions & 3 deletions

File tree

‎.hypatia-ignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,3 +63,7 @@ cicd_rules/vlang_detected:formal/P3_BorrowGraph.v
6363
cicd_rules/banned_language_file:formal/P3_BorrowGraph.v
6464
cicd_rules/vlang_detected:formal/P2_Stlc.v
6565
cicd_rules/banned_language_file:formal/P2_Stlc.v
66+
cicd_rules/vlang_detected:formal/QttSemiring.v
67+
cicd_rules/banned_language_file:formal/QttSemiring.v
68+
cicd_rules/vlang_detected:formal/AffineUsage.v
69+
cicd_rules/banned_language_file:formal/AffineUsage.v

‎docs/PROOF-NEEDS.adoc‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -142,8 +142,12 @@ obligations. They are the "we might have missed" half of the brief.
142142
| P-4
143143
| **QTT affine usage.** Quantities `{0,1,ω}` are respected: `1`-vars used exactly
144144
once, `0`-vars erased, semiring laws hold.
145-
| L | `prose`
146-
| #513 must-have 3; prose `quantitative-types.md`
145+
| L | `partial`
146+
| #513 must-have 3; **semiring + affine-usage mechanized** in
147+
`formal/QttSemiring.v` (`{0,1,ω}` laws + occurrence homomorphism) and
148+
`formal/AffineUsage.v` (`λx.x` affine, `λx. x x` not). The full *typed* QTT
149+
calculus (context splitting, progress+preservation tracking quantities)
150+
remains; prose `quantitative-types.md`
147151

148152
| P-5
149153
| **HM inference soundness + principality.** Inferred types are well-typed and

‎formal/AffineUsage.v‎

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
(* SPDX-License-Identifier: MPL-2.0 *)
2+
(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
3+
4+
(*
5+
AffineUsage.v
6+
═════════════
7+
Wave 2: the affine-usage layer over the QTT semiring (QttSemiring.v).
8+
9+
Reads the multiplicity of a variable in a term as the QTT abstraction of its
10+
free-occurrence count: `usage x t := qof (count x t)`. Proves that usage is
11+
compositional under the semiring — through an application the usages ADD:
12+
13+
usage x (app f a) = qplus (usage x f) (usage x a) (from qof_plus)
14+
15+
— and defines **affine well-formedness** (every binder consumes its variable
16+
at most once, `usage x b ≤ 1`). The payoff theorems: the identity `λx.x` is
17+
affine, while self-application `λx. x x` is NOT — its variable totals `ω`,
18+
which exceeds the affine bound. That is the mechanized statement of "a
19+
linear/affine value may not be duplicated".
20+
21+
Advances **P-4** (docs/PROOF-NEEDS.adoc). Axiom-free, no `Admitted`. The full
22+
*typed* QTT calculus (context splitting Γ = Γ₁ + Γ₂, progress+preservation
23+
tracking quantities) is the next increment, on top of this + P2_Stlc.
24+
25+
`.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
26+
*)
27+
28+
Require Import PeanoNat.
29+
Require Import Lia.
30+
Require Import ASFormal.QttSemiring.
31+
32+
Definition id := nat.
33+
34+
Inductive tm :=
35+
| var (x : id)
36+
| app (f a : tm)
37+
| lam (x : id) (b : tm).
38+
39+
(* Free-occurrence count of x in t. *)
40+
Fixpoint count (x : id) (t : tm) : nat :=
41+
match t with
42+
| var y => if Nat.eqb x y then 1 else 0
43+
| app f a => count x f + count x a
44+
| lam y b => if Nat.eqb x y then 0 else count x b
45+
end.
46+
47+
(* The multiplicity at which x is used in t, as a QTT quantity. *)
48+
Definition usage (x : id) (t : tm) : quant := qof (count x t).
49+
50+
(* ── usage is compositional under the semiring ─────────────────────────── *)
51+
52+
(* Through an application, usages ADD (qplus) — the crux of the affine reading:
53+
a variable used once in `f` and once in `a` is used ω in `f a`. *)
54+
Theorem usage_app : forall x f a,
55+
usage x (app f a) = qplus (usage x f) (usage x a).
56+
Proof. intros x f a; unfold usage; simpl; apply qof_plus. Qed.
57+
58+
Lemma usage_var_same : forall x, usage x (var x) = One.
59+
Proof. intro x; unfold usage; simpl; rewrite Nat.eqb_refl; reflexivity. Qed.
60+
61+
Lemma usage_var_diff : forall x y, x <> y -> usage x (var y) = Zero.
62+
Proof.
63+
intros x y H; unfold usage; simpl.
64+
apply Nat.eqb_neq in H; rewrite H; reflexivity.
65+
Qed.
66+
67+
Lemma usage_lam_bound : forall x b, usage x (lam x b) = Zero.
68+
Proof. intros x b; unfold usage; simpl; rewrite Nat.eqb_refl; reflexivity. Qed.
69+
70+
(* ── affine well-formedness ────────────────────────────────────────────── *)
71+
72+
Fixpoint affine (t : tm) : Prop :=
73+
match t with
74+
| var _ => True
75+
| app f a => affine f /\ affine a
76+
| lam x b => qle (usage x b) One /\ affine b
77+
end.
78+
79+
(* The identity is affine: its bound variable is used exactly once. *)
80+
Example affine_id : forall x, affine (lam x (var x)).
81+
Proof.
82+
intro x; simpl; split.
83+
- rewrite usage_var_same; apply qle_refl.
84+
- exact I.
85+
Qed.
86+
87+
(* Self-application λx. x x is NOT affine: x is used twice, totalling ω, which
88+
exceeds the affine bound `≤ 1`. *)
89+
Example not_affine_selfapp : forall x, ~ affine (lam x (app (var x) (var x))).
90+
Proof.
91+
intro x; simpl; intros [Hle _].
92+
unfold usage, qle in Hle; simpl in Hle.
93+
rewrite !Nat.eqb_refl in Hle; simpl in Hle; lia.
94+
Qed.
95+
96+
Print Assumptions usage_app.
97+
Print Assumptions not_affine_selfapp.

‎formal/QttSemiring.v‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
(* SPDX-License-Identifier: MPL-2.0 *)
2+
(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
3+
4+
(*
5+
QttSemiring.v
6+
═════════════
7+
Wave 2: the **QTT quantity semiring {0, 1, ω}** — the algebraic core of
8+
AffineScript's affine / quantitative type system (the `Quantity` module of
9+
the Solo calculus). Mechanizes the multiplicity semiring with its `+`
10+
(context addition) and `·` (scaling) operations, the usage order
11+
`0 ≤ 1 ≤ ω`, and the bridge to occurrence counts:
12+
13+
qof (m + n) = qplus (qof m) (qof n)
14+
15+
i.e. *occurrences add under QTT addition*. So using a **linear** (`1`)
16+
variable in BOTH the function and the argument of an application totals `ω`
17+
(`qplus One One = Omega`), exceeding the affine bound — the algebraic reason
18+
a linear value cannot be used twice.
19+
20+
Advances **P-4** (docs/PROOF-NEEDS.adoc) from prose to a mechanized core.
21+
All laws hold by exhaustive case analysis — axiom-free, no `Admitted`.
22+
A usage-counted linear *calculus* (the "1-var used exactly once" typing
23+
theorem) builds on this in AffineUsage.v.
24+
25+
`.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
26+
*)
27+
28+
Require Import PeanoNat.
29+
Require Import Lia.
30+
31+
Inductive quant := Zero | One | Omega.
32+
33+
(* Context addition: how usages combine when a variable is used in two places.
34+
1 + 1 = ω is the crux — two linear uses exceed the affine bound. *)
35+
Definition qplus (p q : quant) : quant :=
36+
match p with
37+
| Zero => q
38+
| One => match q with Zero => One | _ => Omega end
39+
| Omega => Omega
40+
end.
41+
42+
(* Scaling: how a usage is multiplied when passing through a binder of a given
43+
multiplicity. *)
44+
Definition qmult (p q : quant) : quant :=
45+
match p with
46+
| Zero => Zero
47+
| One => q
48+
| Omega => match q with Zero => Zero | _ => Omega end
49+
end.
50+
51+
(* ── semiring laws (exhaustive case analysis) ──────────────────────────── *)
52+
53+
Lemma qplus_0_l : forall q, qplus Zero q = q. Proof. reflexivity. Qed.
54+
Lemma qplus_0_r : forall q, qplus q Zero = q. Proof. destruct q; reflexivity. Qed.
55+
Lemma qplus_comm : forall p q, qplus p q = qplus q p.
56+
Proof. destruct p, q; reflexivity. Qed.
57+
Lemma qplus_assoc : forall p q r, qplus p (qplus q r) = qplus (qplus p q) r.
58+
Proof. destruct p, q, r; reflexivity. Qed.
59+
60+
Lemma qmult_0_l : forall q, qmult Zero q = Zero. Proof. reflexivity. Qed.
61+
Lemma qmult_0_r : forall q, qmult q Zero = Zero. Proof. destruct q; reflexivity. Qed.
62+
Lemma qmult_1_l : forall q, qmult One q = q. Proof. reflexivity. Qed.
63+
Lemma qmult_1_r : forall q, qmult q One = q. Proof. destruct q; reflexivity. Qed.
64+
Lemma qmult_comm : forall p q, qmult p q = qmult q p.
65+
Proof. destruct p, q; reflexivity. Qed.
66+
Lemma qmult_assoc : forall p q r, qmult p (qmult q r) = qmult (qmult p q) r.
67+
Proof. destruct p, q, r; reflexivity. Qed.
68+
69+
Lemma qdistrib_l : forall p q r, qmult p (qplus q r) = qplus (qmult p q) (qmult p r).
70+
Proof. destruct p, q, r; reflexivity. Qed.
71+
Lemma qdistrib_r : forall p q r, qmult (qplus p q) r = qplus (qmult p r) (qmult q r).
72+
Proof. destruct p, q, r; reflexivity. Qed.
73+
74+
(* ── the usage order 0 ≤ 1 ≤ ω ───────────────────────────────────────── *)
75+
76+
Definition rank (q : quant) : nat :=
77+
match q with Zero => 0 | One => 1 | Omega => 2 end.
78+
Definition qle (p q : quant) : Prop := rank p <= rank q.
79+
80+
Lemma qle_refl : forall q, qle q q. Proof. intro; apply Nat.le_refl. Qed.
81+
Lemma qle_trans : forall p q r, qle p q -> qle q r -> qle p r.
82+
Proof. unfold qle; intros p q r H1 H2; eapply Nat.le_trans; eauto. Qed.
83+
Lemma qle_zero_min : forall q, qle Zero q. Proof. intro q; unfold qle; apply Nat.le_0_l. Qed.
84+
Lemma qle_omega_max : forall q, qle q Omega. Proof. destruct q; unfold qle; simpl; lia. Qed.
85+
86+
(* ── the affine facts ──────────────────────────────────────────────────── *)
87+
88+
(* Using a linear (1) value twice overflows to ω — i.e. exceeds the affine
89+
bound `≤ 1`. This is the algebraic heart of "a linear value is used once". *)
90+
Lemma linear_used_twice : qplus One One = Omega. Proof. reflexivity. Qed.
91+
Lemma affine_bound_exceeded : ~ qle (qplus One One) One.
92+
Proof. unfold qle; rewrite linear_used_twice; simpl; lia. Qed.
93+
94+
(* Erased (0) variables contribute nothing and absorb under scaling. *)
95+
Lemma erased_scales_away : forall q, qmult Zero q = Zero. Proof. reflexivity. Qed.
96+
97+
(* ── bridge: occurrence counts abstract to quantities ──────────────────── *)
98+
99+
Definition qof (n : nat) : quant :=
100+
match n with 0 => Zero | 1 => One | _ => Omega end.
101+
102+
(* `qof` is a semiring homomorphism on addition: occurrences add under qplus.
103+
So a variable used m times in `f` and n times in `a` is used (m+n) times in
104+
`f a`, abstracting to qplus — and if both are 1, the total is ω. *)
105+
Theorem qof_plus : forall m n, qof (m + n) = qplus (qof m) (qof n).
106+
Proof. intros m n; destruct m as [| [| m]]; destruct n as [| [| n]]; reflexivity. Qed.
107+
108+
Corollary qof_linear_twice : qof 1 = One /\ qof (1 + 1) = Omega.
109+
Proof. split; reflexivity. Qed.

‎formal/README.adoc‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,16 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
6969
| `F4_ErrorFaithful.v`
7070
| **F-4** — error rendering preserves class + referent
7171
| **mechanized**, axiom-free
72+
73+
| `QttSemiring.v`
74+
| **P-4** (Wave 2) — the QTT quantity semiring `{0,1,ω}`: operations, semiring
75+
+ order laws, occurrence-count homomorphism
76+
| **mechanized**, axiom-free
77+
78+
| `AffineUsage.v`
79+
| **P-4** (Wave 2) — affine usage over the semiring: `λx.x` affine, `λx. x x`
80+
not (variable totals `ω`)
81+
| **mechanized**, axiom-free
7282
|===
7383

7484
All mechanized theorems report *Closed under the global context* under `Print
@@ -114,6 +124,26 @@ the stated obligation and pin its meaning, not the full language:
114124
*class* and *referent*, changing only vocabulary, so no face can make error
115125
X read as a different error Y.
116126

127+
== Wave 2: the affine/QTT layer (P-4)
128+
129+
The quantities `{0,1,ω}` and their algebra are what make AffineScript *affine*:
130+
131+
* **`QttSemiring.v`** — the multiplicity semiring: `qplus` (context addition,
132+
with `1 + 1 = ω`) and `qmult` (scaling), all semiring + order laws by
133+
exhaustive case analysis, and the homomorphism
134+
`qof (m + n) = qplus (qof m) (qof n)` (occurrence counts add under QTT
135+
addition).
136+
* **`AffineUsage.v`** — reads a variable's multiplicity as `qof (count x t)`,
137+
proves usage composes under the semiring through application
138+
(`usage x (app f a) = qplus (usage x f) (usage x a)`), and defines affine
139+
well-formedness. Payoff: `λx.x` is affine; `λx. x x` is **not** — its variable
140+
totals `ω`, exceeding the affine bound. The mechanized statement of "a linear
141+
value may not be duplicated".
142+
143+
The full *typed* QTT calculus — context splitting `Γ = Γ₁ + Γ₂`, progress +
144+
preservation tracking quantities, on top of `P2_Stlc.v` — is the next
145+
increment.
146+
117147
== K-1 and its growth
118148

119149
`K1_CodegenPreservation.v` proves, for a minimal two-type fragment (nat + bool,

‎formal/_CoqProject‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,5 @@ P3_BorrowSound.v
99
P3_BorrowGraph.v
1010
P2_Progress.v
1111
P2_Stlc.v
12+
QttSemiring.v
13+
AffineUsage.v

‎formal/justfile‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ check:
1111
all=""
1212
for f in K1_CodegenPreservation K1Let_CodegenPreservation Siblings_Stated \
1313
F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \
14-
P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc; do
14+
P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc \
15+
QttSemiring AffineUsage; do
1516
echo "== coqc $f.v =="
1617
o="$(coqc -Q . ASFormal "$f.v")"
1718
printf '%s\n' "$o"

0 commit comments

Comments
 (0)