Code-with-CS-shape characterizes the context-sensitive languages

The bounded-search language contextSensitiveLanguageOf : Code T → Language T agrees with the actual grammar language only on context-sensitive codes. So the adequate, effective presentation of the CS class uses the subtype of codes whose decoded grammar is context-sensitive:

CSCode T := {c : Code T // grammar_context_sensitive (ofCode c)}.

This file:

• proves the shape predicate grammar_context_sensitive ∘ ofCode is a PrimrecPred (so the subtype is Primcodable);
• packages ComputableMembership CS contextSensitiveLanguageOf', where contextSensitiveLanguageOf' is the restriction to CSCode.

Boolean folds with clean specifications

def ContextSensitive.boolAll {β : Type} (p : β → Bool) (l : List β) : Bool

boolAll p l is true iff every element satisfies p.

Equations

• ContextSensitive.boolAll p l = List.foldr (fun (b : β) (acc : Bool) => p b && acc) true l

def ContextSensitive.boolAny {β : Type} (p : β → Bool) (l : List β) : Bool

boolAny p l is true iff some element satisfies p.

Equations

• ContextSensitive.boolAny p l = List.foldr (fun (b : β) (acc : Bool) => p b || acc) false l

theorem ContextSensitive.boolAll_eq_true {β : Type} (p : β → Bool) (l : List β) : boolAll p l = true ↔ ∀ b ∈ l, p b = true

theorem ContextSensitive.boolAny_eq_true {β : Type} (p : β → Bool) (l : List β) : boolAny p l = true ↔ ∃ b ∈ l, p b = true

theorem ContextSensitive.primrec_boolAll {β : Type} [Primcodable β] {p : ℕ → β → Bool} (hp : Primrec₂ p) : Primrec fun (x : ℕ × List β) => boolAll (p x.1) x.2

theorem ContextSensitive.primrec_boolAny {β : Type} [Primcodable β] {p : ℕ → β → Bool} (hp : Primrec₂ p) : Primrec fun (x : ℕ × List β) => boolAny (p x.1) x.2

The CS-shape decision procedure

def ContextSensitive.epsOrNc {T : Type} (init : ℕ) (r : grule T ℕ) : Bool

The single-rule "epsilon or noncontracting" check, relative to an initial index.

Equations

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

def ContextSensitive.isEps {T : Type} (init : ℕ) (r : grule T ℕ) : Bool

The single-rule "is an initial epsilon rule" check.

Equations

• ContextSensitive.isEps init r = (decide (r.input_L.length = 0) && decide (r.input_N = init) && (decide (r.input_R.length = 0) && decide (r.output_string.length = 0)))

def ContextSensitive.notOnRhs {T : Type} [DecidableEq T] (init : ℕ) (r : grule T ℕ) : Bool

The single-rule "initial nonterminal not on this rule's RHS" check.

Equations

• ContextSensitive.notOnRhs init r = ContextSensitive.boolAll (fun (s : symbol T ℕ) => !decide (s = symbol.nonterminal init)) r.output_string

def ContextSensitive.isCSCode {T : Type} [DecidableEq T] (c : Code T) : Bool

Boolean decision of grammar_context_sensitive (ofCode c).

Equations

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

Correctness of the decision procedure

theorem ContextSensitive.isEps_iff {T : Type} [DecidableEq T] (c : Code T) (r : grule T ℕ) : isEps c.2 r = true ↔ initial_epsilon_rule (ofCode c) r

theorem ContextSensitive.epsOrNc_iff {T : Type} [DecidableEq T] (c : Code T) (r : grule T ℕ) : epsOrNc c.2 r = true ↔ initial_epsilon_rule (ofCode c) r ∨ grule_noncontracting r

theorem ContextSensitive.notOnRhs_iff {T : Type} [DecidableEq T] (init : ℕ) (r : grule T ℕ) : notOnRhs init r = true ↔ symbol.nonterminal init ∉ r.output_string

theorem ContextSensitive.isCSCode_iff {T : Type} [DecidableEq T] (c : Code T) : isCSCode c = true ↔ grammar_context_sensitive (ofCode c)

Primitive recursiveness of the decision procedure

theorem ContextSensitive.primrec_isCSCode {T : Type} [DecidableEq T] [Primcodable T] : Primrec isCSCode

theorem ContextSensitive.primrecPred_isCS {T : Type} [DecidableEq T] [Primcodable T] : PrimrecPred fun (c : Code T) => grammar_context_sensitive (ofCode c)

The adequate, effective CS presentation

instance ContextSensitive.instDecidablePredCodeGrammar_context_sensitiveOfCode {T : Type} [DecidableEq T] : DecidablePred fun (c : Code T) => grammar_context_sensitive (ofCode c)

Equations

• ContextSensitive.instDecidablePredCodeGrammar_context_sensitiveOfCode c = decidable_of_iff (ContextSensitive.isCSCode c = true) ⋯

@[reducible, inline]

abbrev ContextSensitive.CSCode (T : Type) [DecidableEq T] [Primcodable T] : Type

The subtype of codes whose decoded grammar is context-sensitive. It is Primcodable because the CS-shape predicate is primitive recursive (primrecPred_isCS).

Equations

• ContextSensitive.CSCode T = { c : Code T // grammar_context_sensitive (ofCode c) }

noncomputable instance ContextSensitive.instPrimcodableCSCode {T : Type} [DecidableEq T] [Primcodable T] : Primcodable (CSCode T)

Equations

• ContextSensitive.instPrimcodableCSCode = Primcodable.subtype ⋯

def ContextSensitive.contextSensitiveLanguageOf' {T : Type} [DecidableEq T] [Primcodable T] (sc : CSCode T) : Language T

The language presented by a context-sensitive code.

Equations

• ContextSensitive.contextSensitiveLanguageOf' sc = contextSensitiveLanguageOf ↑sc

theorem ContextSensitive.csLang_eq {T : Type} [DecidableEq T] {c : Code T} (hcs : grammar_context_sensitive (ofCode c)) : contextSensitiveLanguageOf c = grammar_language (ofCode c)

On a context-sensitive code, the bounded-search language is the grammar language.

theorem ContextSensitive.characterizes_CS {T : Type} [DecidableEq T] [Primcodable T] : Characterizes CS contextSensitiveLanguageOf'

The CS code presentation is adequate: it denotes exactly the context-sensitive languages (the library's class CS).

theorem ContextSensitive.contextSensitive_membership_computablePred' {T : Type} [DecidableEq T] [Primcodable T] : ComputablePred fun (p : CSCode T × List T) => p.2 ∈ contextSensitiveLanguageOf' p.1

Uniform membership for the CS presentation is computable.

theorem ContextSensitive.contextSensitive_computableMembership {T : Type} [DecidableEq T] [Primcodable T] : ComputableMembership CS contextSensitiveLanguageOf'

Context-sensitive membership is uniformly computable as a statement about the class CS: the context-sensitive codes form an adequate, effective presentation with uniformly decidable membership.