Recursive (Decidable) Languages

This file defines the class of recursive (decidable) languages, characterised by the existence of a Turing machine that decides the language: the machine always halts, and it accepts exactly the words in the language.

Main definitions

• is_Recursive — a language is recursive if there exists a TM₀ machine, with the same input/work alphabet convention as is_TM, that always halts together with a Boolean acceptance predicate on states, such that w ∈ L iff the machine halts in a state q with accept q = true.
• Recursive — the class of all recursive languages.

def is_Recursive {T : Type} (L : Language T) : Prop

A language L over alphabet T is recursive (decidable) if there exists a finite-work-alphabet, finite-state Turing machine (in Mathlib's Turing.TM0 model) that always halts, together with a Boolean predicate accept on states, such that w ∈ L iff the machine halts in a state q with accept q = true.

The machine uses the same tape convention as is_TM: Option (T ⊕ Γ), where none is blank, some (Sum.inl t) is an input symbol, and some (Sum.inr γ) is a work symbol. The input word w : List T is written as w.map (fun t => some (Sum.inl t)).

Equations

• One or more equations did not get rendered due to their size.

def Recursive {T : Type} : Set (Language T)

The class of recursive (decidable) languages.

Equations

• Recursive = setOf is_Recursive