Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.WordPredicates

Shared finite-state word predicates #

The nonempty-word transducer and its degree certificate are shared by direct Option and unary Degree certificates. Its machine clocks include the whole runtime input; it uses no work tapes.

Main results #

source
def Turing.MultiTapeTM.Internal.WordPredicates.nonemptyT :
Transducer Bool Bool

Emit a single Boolean indicating whether the input contains a symbol.

Instances For
    source
    theorem Turing.MultiTapeTM.Internal.WordPredicates.nonemptyT_run_true (w : List Bool) :
    nonemptyT.run true w = []

    After the first input symbol, no further output is emitted.

    source
    theorem Turing.MultiTapeTM.Internal.WordPredicates.computableInDegree_of_nonemptyT {α : Type u_1} {enc : α ↪ List Bool} {f : α → Bool} (h : ∀ (a : α), encBool (f a) = nonemptyT.run nonemptyT.q₀ (enc a)) :
    ComputableInDegree f enc encBool 1 0

    A Boolean test that nonemptyT computes on the encoded input runs in linear time, with output degree zero.