Documentation

CslibFrontier.Computability.Complexity.ImmermanVardi.Input

First-order input symbols for native deterministic machines #

The direct length and bit formulas for encStructure yield formulas for all three native input-tape symbols. Position zero is the left endmarker; the first data bit is at position one. The formulas include the right endmarker and padding, and use no guessed relations.

source
noncomputable def Cslib.Logic.Vocabulary.inputSymbol {L : FirstOrder.Language} (v : Vocabulary L) :
Option Bool → (FO.Ordered.language v.powerLanguage).Formula (Fin 1)

The native input-tape symbol, including both endmarkers, defined from the encoded input.

Instances For
    source
    theorem Cslib.Logic.Vocabulary.realize_inputSymbol {L : FirstOrder.Language} (v : Vocabulary L) {a : EncodedStructure} (ha : v.WellFormed a) {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B) (s : Option Bool) (p : Fin B) :
    (v.inputSymbol s).Realize ![p] ↔ Turing.inputAt (encStructure a) ↑p = s

    The first-order input-symbol formula agrees exactly with the native machine input lookup.