The arithmetic a sweep can do: comparison and addition, bit by bit

The base of a machine of DescriptiveComplexity.LogTime.Machine never evaluates a numeric predicate; if it is to compare or to add, it has to build the operation out of bits. This file does so, and the two constructions are the bit-level analogues of DescriptiveComplexity.HeadArith's plusP one resource bound higher:

• DescriptiveComplexity.leSweep – the comparison, one state bit carrying the verdict on the positions read so far, overwritten whenever the two registers differ (DescriptiveComplexity.leSweep_accepts);
• DescriptiveComplexity.plusSweep – the ripple-carry addition, one state bit for the carry and one for “every output bit has matched so far”, accepting when the last carry is out and nothing mismatched (DescriptiveComplexity.plusSweep_accepts).

Both are single passes from the lowest position upwards, both use a constant number of state bits, and neither reads the instance – so the machine model is not vacuous: the order and the addition of the numeric predicates are computed by it, from bits alone.

Where the arithmetic stops

Multiplication is not here, and not for lack of effort: a sweep carries a constant number of bits past each position, whereas the schoolbook product of two log n-bit numbers accumulates a column count that grows with the number of positions. That boundary is the honest limit of a sweep, and it is why the model has a second primitive that is not one: DescriptiveComplexity.BaseTest.bit reads a bit at an address instead of computing anything. Eliminating × in favor of that read is the classical theorem the model waits on, not a widening of this file; see DescriptiveComplexity.LogTime.

Peeling a bit off a remainder

Comparison

@[reducible]

def DescriptiveComplexity.leSweep : Sweep 2

The comparison sweep: one state bit, holding the verdict on the positions read so far. A position where the registers differ overwrites it; a position where they agree keeps it. Read from the lowest position upwards, the verdict left at the end is the comparison of the two registers.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.leSweep_accepts {A : Type} [LinearOrder A] [Finite A] (x : Fin 2 → A) : leSweep.Accepts x ↔ x 0 ≤ x 1

The comparison sweep decides the order: the machine model computes ≤, from bits alone.

Addition

@[reducible]

def DescriptiveComplexity.plusSweep : Sweep 3

The ripple-carry addition sweep: state bit 0 is the carry, state bit 1 records that every output bit has matched the third register so far. The sweep accepts when nothing has mismatched and the last carry is out – which is the statement that the sum does not overflow the universe.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.plusSweep_accepts {A : Type} [LinearOrder A] [Finite A] (x : Fin 3 → A) : plusSweep.Accepts x ↔ orank (x 0) + orank (x 1) = orank (x 2)

The addition sweep decides addition: the machine model computes the numeric predicate plus, from bits alone – the bit-level analogue of the head program DescriptiveComplexity.HeadProgram.plusP.

The trivial sweep

@[reducible]

def DescriptiveComplexity.trueSweep : Sweep 0

The trivial sweep: no state, no register, always accepting. It is what a constant of the bit-level logic compiles to, so that a trivially true kernel needs no dummy variable.

Equations

• DescriptiveComplexity.trueSweep = { σ := 0, init := Fin.elim0, step := Fin.elim0, acc := DescriptiveComplexity.BitExpr.tt }