Writing an expansion's sentences with iterated block expansions #

An exponential expansion defines an n-ary symbol by a sentence over the base vocabulary expanded by DescriptiveComplexity.SOBlock.replicate – one block holding n copies. The rest of the library writes its multi-state sentences over iterated expansions instead: one copy of B.lang per state, stacked as nested sums (DescriptiveComplexity.SOBlock.structure₁, DescriptiveComplexity.SOBlock.structure₂ – the shape of an DescriptiveComplexity.SOTCSpec).

This file bridges the two presentations at the arities an expansion actually needs, one and two:

DescriptiveComplexity.SOBlock.oneLHom reads a sentence over L ⊕ B.lang inside L ⊕ (B.replicate 1).lang;
DescriptiveComplexity.SOBlock.twoLHom reads a sentence over (L ⊕ B.lang) ⊕ B.lang inside L ⊕ (B.replicate 2).lang, the first copy becoming copy 0 and the second copy 1.

Both transports are definitional on assignments – reading copy k of a replicated assignment is reading the k-th assignment – so their correctness lemmas are DescriptiveComplexity.SOBlock.realize_homSentence and one LHom.IsExpansionOn whose relation case is rfl.

One copy #

source

def DescriptiveComplexity.SOBlock.oneLHom (L : FirstOrder.Language) (B : SOBlock) :

L.sum B.lang →ᴸ L.sum (B.replicate 1).lang

Reading a sentence over one copy of a block inside the block replicated once.

Equations

DescriptiveComplexity.SOBlock.oneLHom L B = (FirstOrder.Language.LHom.id L).sumMap (DescriptiveComplexity.SOBlock.homLHom (fun (i : B.ι) => (0, i)) ⋯)

Instances For

Dependency graph

source

theorem DescriptiveComplexity.SOBlock.realize_oneLHom {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] (ρs : Fin 1 → B.Assignment A) (φ : (L.sum B.lang).Sentence) :

A ⊨ (oneLHom L B).onSentence φ ↔ A ⊨ φ

Correctness of the one-copy reading: the replicated assignment holds the original assignment in its single copy.

Dependency graph

Two copies #

source

def DescriptiveComplexity.SOBlock.twoLHom (L : FirstOrder.Language) (B : SOBlock) :

(L.sum B.lang).sum B.lang →ᴸ L.sum (B.replicate 2).lang

Reading a sentence over two stacked copies of a block inside the block replicated twice: the inner copy becomes copy 0, the outer copy 1.

Equations

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

Instances For

Dependency graph

source

theorem DescriptiveComplexity.SOBlock.twoLHom_isExpansionOn {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] (ρs : Fin 2 → B.Assignment A) :

(twoLHom L B).IsExpansionOn A

The two-copy reading is an expansion between the stacked structure and the replicated one. Stated at a family of two assignments rather than at a pair, since that is the shape a defining sentence of an expansion is realized against.

Dependency graph

source

theorem DescriptiveComplexity.SOBlock.realize_twoLHom {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] (ρs : Fin 2 → B.Assignment A) (φ : ((L.sum B.lang).sum B.lang).Sentence) :

A ⊨ (twoLHom L B).onSentence φ ↔ A ⊨ φ

Correctness of the two-copy reading: the replicated assignment holds the current state in copy 0 and the next one in copy 1.

Dependency graph

Two copies, the other way #

DescriptiveComplexity.SOBlock.twoLHom reads a stacked sentence inside a replicated one, which is what an expansion's defining sentence needs. A walk over an expanded universe needs the converse: an DescriptiveComplexity.SOTCSpec states its transition over two stacked copies of its state block, while everything said about two points of an expanded universe – their order, their equality, one being the successor of the other – is written over the block replicated twice.

source