Lax Lean Archive

The bounded configuration graph

Lax362205.ConfigurationGraph · concepts/Lax362205/ConfigurationGraph.lean · lax-362205

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Vertices are configurations whose work tape has a fixed finite bound. Edges are machine transitions. Acceptance is reachability from the initial configuration to a terminal accepting configuration. The search predicate replaces reachability by the recursive finite graph test.

    Concept map
    5 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 1 of this submission's paper

    Lean source view on GitHub

    1import Lax362205.BoundedConfigurations
    2import Lax362205.Reachability
    3import Mathlib.Data.Fintype.EquivFin
    4import Mathlib.Data.Nat.Log
    5
    6set_option backward.isDefEq.respectTransparency false
    7
    8/-!
    9---
    10title: The bounded configuration graph
    11type: definition
    12---
    13Vertices are configurations whose work tape has a fixed finite bound.
    14Edges are machine transitions. Acceptance is reachability from the initial
    15configuration to a terminal accepting configuration. The search predicate
    16replaces reachability by the recursive finite graph test.
    17-/
    18
    19namespace Lax362205.ConfigurationGraph
    20
    21open scoped Classical
    22
    23open Lax434930.PolynomialTime Lax434930.SpaceMachines BoundedConfigurations Reachability
    24
    25/-- Label all bounded configurations consecutively from zero. -/
    26noncomputable def numbering (M : Machine) (n s : ℕ) :
    27 Config M n s ≃ Fin (Fintype.card (Config M n s)) := Fintype.equivFin _
    28
    29/-- Connect two numbered configurations exactly when the machine can move from the first to the second. -/
    30noncomputable def graph (M : Machine) (w : Word) (s : ℕ) :
    31 Graph (Fintype.card (Config M w.length s)) :=
    32 fun a b => decide (M.Step w (expand ((numbering M w.length s).symm a))
    33 (expand ((numbering M w.length s).symm b)))
    34
    35/-- Some accepting terminal configuration is reachable from the initial configuration within the tape bound. -/
    36def AcceptsBounded (M : Machine) (w : Word) (s : ℕ) : Prop :=
    37 ∃ a b : Config M w.length s,
    38 expand a = M.initial ∧ M.Terminal w (expand b) ∧ M.accept b.state = true ∧
    39 Reachable (graph M w s) (numbering M w.length s a) (numbering M w.length s b)
    40
    41/-- The finite reachability search finds a path from the initial configuration to an accepting terminal one. -/
    42def SearchAccepts (M : Machine) (w : Word) (s : ℕ) : Prop :=
    43 ∃ a b : Config M w.length s,
    44 expand a = M.initial ∧ M.Terminal w (expand b) ∧ M.accept b.state = true ∧
    45 search (graph M w s) (Nat.clog 2 (Fintype.card (Config M w.length s)))
    46 (numbering M w.length s a) (numbering M w.length s b) = true
    47
    48end Lax362205.ConfigurationGraph
    49
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…