LanglibLinear-bounded automata are closed under positive complement #
The marker-free is_LBA_pos model has no tape cells on the empty input, so its
complement operation is necessarily relative to the nonempty words. Given an LBA,
we expose its finite configuration graph as a CertifiedRowSystem, apply the
inductive-counting complement construction there, and compile the resulting row
system back to an input-sized LBA.
The full complement theorem for context-sensitive languages, including the empty
word, is derived in Classes/ContextSensitive/Closure/Complement.lean.
theorem
is_LBA_pos_complement
{T : Type}
[Fintype T]
[DecidableEq T]
{L : Language T}
(hL : is_LBA_pos L)
:
The nonempty complement of an input-sized LBA language is again recognized by
an input-sized LBA. Removing {[]} is unavoidable: every is_LBA_pos language
rejects the empty word.