Computability of the Grammar Membership Test

This file establishes that the grammarTest function is Computable₂.

Key results

• grammarTest_computable₂ — the grammar test function is Computable₂

Structure

1. Primcodable instances for symbol and grule
2. Primrec lemmas for symbol constructors and grule field projections
3. primrec_applyRuleAt — applyRuleAt is primitive recursive
4. computable_extractTerminals — extractTerminals is computable
5. primrec_applyRuleSeq_step / computable_applyRuleSeq — rule sequence application
6. grammarTest_computable₂ — the final result

Primcodable instances

noncomputable def symbolEquiv (T N : Type) : symbol T N ≃ T ⊕ N

Equations

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

noncomputable instance symbolPrimcodable {T N : Type} [Primcodable T] [Primcodable N] : Primcodable (symbol T N)

Equations

• symbolPrimcodable = Primcodable.ofEquiv (T ⊕ N) (symbolEquiv T N)

noncomputable def gruleEquiv (T N : Type) : grule T N ≃ List (symbol T N) × N × List (symbol T N) × List (symbol T N)

Equations

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

noncomputable instance grulePrimcodable {T N : Type} [Primcodable T] [Primcodable N] : Primcodable (grule T N)

Equations

• grulePrimcodable = Primcodable.ofEquiv (List (symbol T N) × N × List (symbol T N) × List (symbol T N)) (gruleEquiv T N)

Symbol constructors are primrec

theorem primrec_symbol_nonterminal {T N : Type} [Primcodable T] [Primcodable N] : Primrec symbol.nonterminal

theorem primrec_symbol_terminal {T N : Type} [Primcodable T] [Primcodable N] : Primrec symbol.terminal

theorem primrec_symbol_casesOn {T N σ : Type} [Primcodable T] [Primcodable N] [Primcodable σ] {α : Type} [Primcodable α] {f : α → symbol T N} {g : α → T → σ} {h : α → N → σ} (hf : Primrec f) (hg : Primrec₂ g) (hh : Primrec₂ h) : Primrec fun (a : α) => match f a with | symbol.terminal t => g a t | symbol.nonterminal n => h a n

Case analysis on symbol is primrec.

grule field projections are primrec

theorem primrec_grule_inputL {T N : Type} [Primcodable T] [Primcodable N] : Primrec fun (r : grule T N) => r.input_L

theorem primrec_grule_inputN {T N : Type} [Primcodable T] [Primcodable N] : Primrec fun (r : grule T N) => r.input_N

theorem primrec_grule_inputR {T N : Type} [Primcodable T] [Primcodable N] : Primrec fun (r : grule T N) => r.input_R

theorem primrec_grule_outputString {T N : Type} [Primcodable T] [Primcodable N] : Primrec fun (r : grule T N) => r.output_string

applyRuleAt is primrec

theorem primrec_applyRuleAt {T : Type} [DecidableEq T] {N : Type} [DecidableEq N] [Primcodable T] [Primcodable N] : Primrec fun (args : grule T N × List (symbol T N) × ℕ) => applyRuleAt args.1 args.2.1 args.2.2

extractTerminals is computable

theorem computable_extractTerminals {T N : Type} [Primcodable T] [Primcodable N] : Computable extractTerminals

applyRuleSeq with fixed args is computable

theorem primrec_applyRuleSeq_step {T : Type} [DecidableEq T] {N : Type} [DecidableEq N] [Primcodable T] [Primcodable N] (rules : List (grule T N)) : Primrec fun (p : Option (List (symbol T N)) × ℕ × ℕ) => match p.1 with | none => none | some sf => match rules[p.2.1]? with | none => none | some r => applyRuleAt r sf p.2.2

theorem computable_applyRuleSeq {T : Type} [DecidableEq T] {N : Type} [DecidableEq N] [Primcodable T] [Primcodable N] (rules : List (grule T N)) (init : List (symbol T N)) : Computable fun (seq : List (ℕ × ℕ)) => applyRuleSeq rules init seq

Main result

theorem grammarTest_computable₂ {T : Type} [DecidableEq T] (g : grammar T) [DecidableEq g.nt] [Primcodable T] [Primcodable g.nt] : Computable₂ (grammarTest g)