Native arithmetic on fixed-length radix words #

The radix is a source element, but a word may represent a value much larger than the source universe. Native PLUS and TIMES check only individual digit equations. Bounded digits and zero initial and final carries make these equations exact rather than modular.

Main definitions #

Cslib.Logic.FO.Ordered.mulEq: apply native TIMES to arbitrary terms.
Cslib.Logic.FO.Ordered.Radix.digits: bound every digit by the radix.
Cslib.Logic.FO.Ordered.Radix.affine: multiply one word by a digit and add another word.

Main results #

Cslib.Logic.FO.Ordered.Radix.realize_affine: exact ordinary arithmetic, provided the radix is at least two and its cube fits in the source universe.

References #

N. Immerman, Descriptive Complexity, Exercise 1.33(3) and Theorem 1.17(1): the digit construction implements the suggested arithmetic with the native arithmetic of the theorem.

source

noncomputable def Cslib.Logic.FO.Ordered.mulEq (L : FirstOrder.Language) {α : Type u_1} (x y z : (language L).Term α) :

(language L).Formula α

Apply native TIMES to three arbitrary terms.

Instances For

source

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_mulEq {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (x y z : (language L).Term α) (v : α → Fin n) :

(mulEq L x y z).Realize v ↔ ↑(FirstOrder.Language.Term.realize v x) * ↑(FirstOrder.Language.Term.realize v y) = ↑(FirstOrder.Language.Term.realize v z)

source

noncomputable def Cslib.Logic.FO.Ordered.Radix.digits (L : FirstOrder.Language) {α : Type u_1} {d : ℕ} (B : (language L).Term α) (x : Fin d → (language L).Term α) :

(language L).Formula α

Every word digit is strictly below the radix.

Instances For

source

noncomputable def Cslib.Logic.FO.Ordered.Radix.cell (L : FirstOrder.Language) {α : Type u_1} (B a b y c z c' : (language L).Term α) :

(language L).Formula α

One exact affine digit equation, with all its scalar intermediate values checked.

Instances For

source

noncomputable def Cslib.Logic.FO.Ordered.Radix.affine (L : FirstOrder.Language) {α : Type u_1} {d : ℕ} (B b : (language L).Term α) (x y z : Fin d → (language L).Term α) :

(language L).Formula α

Multiply a word by a coefficient at most the radix and add another word, rejecting final overflow. Allowing the radix itself as coefficient also provides exact word shifts.

Instances For

source

@[simp]

theorem Cslib.Logic.FO.Ordered.Radix.realize_digits {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d : ℕ} (B : (language L).Term α) (x : Fin d → (language L).Term α) (v : α → Fin n) :

(digits L B x).Realize v ↔ ∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (x i)) < ↑(FirstOrder.Language.Term.realize v B)

source

theorem Cslib.Logic.FO.Ordered.Radix.realize_cell {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (B a b y c z c' : (language L).Term α) (v : α → Fin n) :

source

theorem Cslib.Logic.FO.Ordered.Radix.realize_affine {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d : ℕ} (B b : (language L).Term α) (x y z : Fin d → (language L).Term α) (v : α → Fin n) (hB : 1 < ↑(FirstOrder.Language.Term.realize v B)) (hBn : ↑(FirstOrder.Language.Term.realize v B) ^ 3 < n) :

When the radix B is at least two and B ^ 3 fits in the universe, affine L B b x y z holds exactly when b ≤ B, the words x, y and z have digits below B, and their values satisfy b x + y = z.

Documentation

Complexity.Logics.FirstOrder.Ordered.Radix.Arithmetic

Native arithmetic on fixed-length radix words #

Main definitions #

Main results #

References #