A block with one argument more

Two constructions want the same operation on a block of relation variables: an iteration run at a parameter (DescriptiveComplexity.FixedPointParam) gives every variable the parameter as a further argument, and a kernel whose variables must all have an argument (DescriptiveComplexity.Exponential.KernelArity) gives them a dummy one. The block, the symbol map and the way an assignment of the extended block is read at one value of the extra argument are the same in both, and are here.

def DescriptiveComplexity.SOBlock.withParam (B : SOBlock) : SOBlock

The block B with one extra argument on every relation variable: the parameter the iteration is run at.

Equations

• B.withParam = { ι := B.ι, ιFinite := ⋯, arity := fun (i : B.ι) => B.arity i + 1 }

def DescriptiveComplexity.SOBlock.paramSym (B : SOBlock) {m : ℕ} (r : B.lang.Relations m) : B.withParam.lang.Relations (m + 1)

A relation variable of the block, read at the extended block: one argument more.

Equations

• B.paramSym r = ⟨↑r, ⋯⟩

def DescriptiveComplexity.SOBlock.atParam {N : Type} (B : SOBlock) (ρ : B.withParam.Assignment N) (c : N) : B.Assignment N

An assignment of the extended block, read at one parameter.

Equations

• B.atParam ρ c i x = ρ i (Fin.cons c x)

theorem DescriptiveComplexity.SOBlock.relMap_paramSym {N : Type} (B : SOBlock) (ρ : B.withParam.Assignment N) (c : N) {m : ℕ} (b : B.lang.Relations m) (w : Fin (m + 1) → N) (hw : w 0 = c) : FirstOrder.Language.Structure.RelMap (B.paramSym b) w ↔ FirstOrder.Language.Structure.RelMap b fun (i : Fin m) => w i.succ

Reading a parameterized relation variable: the extended variable at a tuple whose first argument is the parameter is the original variable, read at the assignment taken at that parameter.