Arity-preserving renaming of second-order relation variables

A relation renaming maps indices while preserving their arities. Lifting fixes the newly bound relation and renames the older variables. Formula renaming thus avoids capture under both sorts of second-order quantifier. Element variables and vocabulary symbols are unchanged.

structure Complexity.DescriptiveComplexity.RelRenaming (rctx sctx : List Nat) : Type

A map between relation contexts that preserves the arity of every variable.

• index : Fin rctx.length → Fin sctx.length

  The target index of each source relation variable.

• arity (r : Fin rctx.length) : sctx.get (self.index r) = rctx.get r

  Renaming preserves the relation's arity.

def Complexity.DescriptiveComplexity.RelRenaming.id (rctx : List Nat) : RelRenaming rctx rctx

The identity renaming.

Equations

• Complexity.DescriptiveComplexity.RelRenaming.id rctx = { index := fun (r : Fin rctx.length) => r, arity := ⋯ }

def Complexity.DescriptiveComplexity.RelRenaming.comp {rctx sctx tctx : List Nat} (g : RelRenaming sctx tctx) (f : RelRenaming rctx sctx) : RelRenaming rctx tctx

Successive renamings compose in application order.

Equations

• g.comp f = { index := fun (r : Fin rctx.length) => g.index (f.index r), arity := ⋯ }

def Complexity.DescriptiveComplexity.RelRenaming.lift {rctx sctx : List Nat} (f : RelRenaming rctx sctx) (k : Nat) : RelRenaming (k :: rctx) (k :: sctx)

Lift a renaming through a relation binder of arity k.

Equations

• f.lift k = { index := fun (i : Fin (rctx.length + 1)) => Fin.cases 0 (fun (r : Fin rctx.length) => (f.index r).succ) i, arity := ⋯ }

def Complexity.DescriptiveComplexity.RelRenaming.weaken (rctx : List Nat) (k : Nat) : RelRenaming rctx (k :: rctx)

Make room for a fresh relation variable at index zero.

Equations

• Complexity.DescriptiveComplexity.RelRenaming.weaken rctx k = { index := Fin.succ, arity := ⋯ }

def Complexity.DescriptiveComplexity.RelRenaming.pull {rctx sctx : List Nat} (f : RelRenaming rctx sctx) {card : Nat} (ρ : REnv card sctx) : REnv card rctx

Read a target relation environment at the renamed source indices.

Equations

• f.pull ρ r args = ρ (f.index r) fun (i : Fin (sctx.get (f.index r))) => args (Fin.cast ⋯ i)

def Complexity.DescriptiveComplexity.SOFormula.renameRel {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} : RelRenaming rctx sctx → SOFormula V rctx n → SOFormula V sctx n

Rename the free relation variables, lifting the map beneath SO binders.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ (Complexity.DescriptiveComplexity.SOFormula.relApp i args) = Complexity.DescriptiveComplexity.SOFormula.relApp i args
• Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ (Complexity.DescriptiveComplexity.SOFormula.eq a b) = Complexity.DescriptiveComplexity.SOFormula.eq a b
• Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ φ.neg = (Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ φ).neg
• Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ (φ.conj ψ) = (Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ φ).conj (Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ ψ)
• Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ (φ.disj ψ) = (Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ φ).disj (Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ ψ)
• Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ φ.exist = (Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ φ).exist
• Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ φ.all = (Complexity.DescriptiveComplexity.SOFormula.renameRel x✝ φ).all