Finite-domain lookup machine (internal) #
Construction and correctness of a deterministic Turing machine computing a
function of the form fun s => if s ∈ S then g s else [], where S is a finite
set of "inputs of interest" and g an arbitrary target function. Such a
function differs from the constant empty-output function on only finitely many
inputs, so it can be computed by a table lookup that runs in linear time.
The machine has no work tapes. It works in two phases:
- Read phase. It scans the read-only input tape left to right, tracking in
its finite state the prefix read so far — as long as that prefix is still a
prefix of some element of
S; otherwise it enters a "dead" state. The output head bumps off the left marker on the first step and then idles at cell one. - Write phase. On reaching the first input blank it knows exactly which
element of
S(if any) the input was, hence which fixed output string to produce. It writes that string onto the output tape, one symbol per step, landing on the halting configuration.
Since the read phase takes |x| steps and the write phase is bounded by the
longest possible output, the runtime is linear.
The public statement (ite_mem_finset_mem_FP) lives in
Complexitylib.Classes.P.FinsetDomain.
Output finset #
The read phase tracks membership in S.prefixes and the write phase tracks
membership in (outputsFinset g S).suffixes; both finsets come from the
generic Finset.prefixes/Finset.suffixes API.
The lookup machine #
States of the lookup machine.
- read
{g : List Bool → List Bool}
{S : Finset (List Bool)}
(p : List Bool)
(hp : p ∈ S.prefixes)
: LookupState g S
Read phase: the viable prefix consumed so far, carried together with the proof that it is a prefix of some element of
S, so that the transition function can use the proof directly. - dead
{g : List Bool → List Bool}
{S : Finset (List Bool)}
: LookupState g S
Read phase, dead state: the input read so far has diverged from every element of
S. - write
{g : List Bool → List Bool}
{S : Finset (List Bool)}
(w : List Bool)
(hw : w ∈ (outputsFinset g S).suffixes)
: LookupState g S
Write phase: the output suffix still to be written.
- halt
{g : List Bool → List Bool}
{S : Finset (List Bool)}
: LookupState g S
The halt state.
Instances For
LookupState as a sum of two finite subtypes and two extra states. This
equivalence supplies the DecidableEq and Fintype instances, which cannot be
derived because the read/write constructors have dependent fields.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The read-phase state after consuming prefix p: the viable prefix p if it
is still a prefix of some element of S, otherwise the dead state.
Equations
- Complexity.TM.FinsetDomain.readState g S p = if h : p ∈ S.prefixes then Complexity.TM.FinsetDomain.LookupState.read p h else Complexity.TM.FinsetDomain.LookupState.dead
Instances For
The write-phase state carrying output suffix c.
Equations
Instances For
The halt state.