The address a file's marks stand for

A program that seeks to a computed address holds that address on its file, one bit per register, and holds the address under its head there too – the mirror. At the elementwise file that is nothing to say: a register is an element, a mark on the registers is an address. At a coarser file it is something to say, and this file says it.

DescriptiveComplexity.ixAddr is the address a mark on the index stands for – each register carries the bit of one element (elt) – and DescriptiveComplexity.ixMark is the mark a file keeps of an address, its bits at the registers. The two are inverse on the addresses a file can hold (DescriptiveComplexity.IxHolds), and what makes the correspondence useful is that it carries the order, under three conditions:

• elt is injective and an order embedding (hinj, hmono), so comparing marks and comparing addresses is the same comparison;
• the elements it names are upward closed (hup): above one of them there is nothing the file has no register for. The addresses over them are then downward closed – an initial interval of the tape (DescriptiveComplexity.ixHolds_of_wmSetLe) – which is what makes an increment of the addresses an increment of the marks, with no address in between that the file could not have represented.

For a clocked program's file all three hold of the argument registers, because the argument tags are the last ones (DescriptiveComplexity.Draw.lt_arg) and therefore the least significant: the addresses over them are the logical ones.

def DescriptiveComplexity.ixAddr {A I : Type} (elt : I → A) (m : I → Prop) : A → Prop

The address a mark on a file's index stands for: the elements whose register is marked.

Equations

• DescriptiveComplexity.ixAddr elt m x = ∃ (u : I), elt u = x ∧ m u

def DescriptiveComplexity.ixMark {A I : Type} (elt : I → A) (s : A → Prop) : I → Prop

The mark a file keeps of an address: its bits at the registers.

Equations

• DescriptiveComplexity.ixMark elt s u = s (elt u)

def DescriptiveComplexity.IxHolds {A I : Type} (elt : I → A) (Use : I → Prop) (s : A → Prop) : Prop

An address a file can hold: every element of it is one of the file's.

Equations

• DescriptiveComplexity.IxHolds elt Use s = ∀ (x : A), s x → ∃ (u : I), Use u ∧ elt u = x

theorem DescriptiveComplexity.ixAddr_elt {A I : Type} {elt : I → A} (hinj : Function.Injective elt) (m : I → Prop) (u : I) : ixAddr elt m (elt u) ↔ m u

theorem DescriptiveComplexity.ixAddr_ixMark {A I : Type} {elt : I → A} {Use : I → Prop} {s : A → Prop} (hs : IxHolds elt Use s) : ixAddr elt (ixMark elt s) = s

A file's mark of an address stands for that address, when the file has a register for each of its elements.

theorem DescriptiveComplexity.ixMark_ixAddr {A I : Type} {elt : I → A} (hinj : Function.Injective elt) (m : I → Prop) : ixMark elt (ixAddr elt m) = m

A mark is the mark of the address it stands for.

theorem DescriptiveComplexity.ixHolds_ixAddr {A I : Type} {elt : I → A} {Use m : I → Prop} (hm : ∀ (u : I), m u → Use u) : IxHolds elt Use (ixAddr elt m)

The address of a mark is one the file can hold.

theorem DescriptiveComplexity.ixAddr_empty {A I : Type} {elt : I → A} : (ixAddr elt fun (x : I) => False) = fun (x : A) => False

theorem DescriptiveComplexity.ixHolds_of_wmSetLe {A I : Type} {Le : A → A → Prop} {elt : I → A} {Use : I → Prop} (hup : ∀ (u : I) (x : A), Use u → WMLt Le (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hLe : IsLinOrd Le) {s t : A → Prop} (hs : IxHolds elt Use t) (h : WMSetLe Le s t) : IxHolds elt Use s

The addresses a file can hold are downward closed: below one of them, every element is either one the file already has a register for, or one above such an element – and above is where the file's elements are.

theorem DescriptiveComplexity.wmSetLt_ixAddr {A I : Type} {ile : I → I → Prop} {Le : A → A → Prop} {elt : I → A} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt ile u u' ↔ WMLt Le (elt u) (elt u')) (m m' : I → Prop) : WMSetLt ile m m' ↔ WMSetLt Le (ixAddr elt m) (ixAddr elt m')

Comparing marks is comparing the addresses they stand for, strictly.

theorem DescriptiveComplexity.wmSetLe_ixAddr {A I : Type} {ile : I → I → Prop} {Le : A → A → Prop} {elt : I → A} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt ile u u' ↔ WMLt Le (elt u) (elt u')) (m m' : I → Prop) : WMSetLe ile m m' ↔ WMSetLe Le (ixAddr elt m) (ixAddr elt m')

Comparing marks is comparing the addresses they stand for.

theorem DescriptiveComplexity.wmIncr_ixMark {A I : Type} {ile : I → I → Prop} {Le : A → A → Prop} {elt : I → A} {Use : I → Prop} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt ile u u' ↔ WMLt Le (elt u) (elt u')) {s s' : A → Prop} (hs' : IxHolds elt Use s') (hi : WMIncr Le s s') : WMIncr ile (ixMark elt s) (ixMark elt s')

An increment of the addresses is an increment of the marks: the carry is an element the file has a register for, and so is everything above it.

theorem DescriptiveComplexity.wmIncr_ixAddr {A I : Type} {ile : I → I → Prop} {Le : A → A → Prop} {elt : I → A} {Use : I → Prop} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt ile u u' ↔ WMLt Le (elt u) (elt u')) (hup : ∀ (u : I) (x : A), Use u → WMLt Le (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) {m m' : I → Prop} (hm' : ∀ (u : I), m' u → Use u) (hi : WMIncr ile m m') : WMIncr Le (ixAddr elt m) (ixAddr elt m')

An increment of the marks is an increment of the addresses, the same correspondence read the other way.

theorem DescriptiveComplexity.ixAddr_id {A : Type} (m : A → Prop) : ixAddr id m = m

At the elementwise file the address is the mark: a register is an element, so the correspondence is the identity and every statement here is the one the space-bounded program already had.

theorem DescriptiveComplexity.ixMark_id {A : Type} (s : A → Prop) : ixMark id s = s