Lax Lean Archive

The bounded configuration graph

Lax733996.ConfigurationGraph · concepts/Lax733996/ConfigurationGraph.lean · lax-733996

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 Lax733996.BoundedConfigurations
    2import Lax733996.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 Lax733996.ConfigurationGraph
    20
    21open Lax434930.PolynomialTime Lax434930.SpaceMachines BoundedConfigurations Reachability
    22
    23noncomputable def numbering (M : Machine) (n s : ℕ) :
    24 Config M n s ≃ Fin (Fintype.card (Config M n s)) := Fintype.equivFin _
    25
    26noncomputable def graph (M : Machine) (w : Word) (s : ℕ) :
    27 Graph (Fintype.card (Config M w.length s)) := by
    28 classical
    29 exact fun a b => decide (M.Step w (expand ((numbering M w.length s).symm a))
    30 (expand ((numbering M w.length s).symm b)))
    31
    32def AcceptsBounded (M : Machine) (w : Word) (s : ℕ) : Prop :=
    33 ∃ a b : Config M w.length s,
    34 expand a = M.initial ∧ M.Terminal w (expand b) ∧ M.accept b.state = true ∧
    35 Reachable (graph M w s) (numbering M w.length s a) (numbering M w.length s b)
    36
    37def SearchAccepts (M : Machine) (w : Word) (s : ℕ) : Prop :=
    38 ∃ a b : Config M w.length s,
    39 expand a = M.initial ∧ M.Terminal w (expand b) ∧ M.accept b.state = true ∧
    40 search (graph M w s) (Nat.clog 2 (Fintype.card (Config M w.length s)))
    41 (numbering M w.length s a) (numbering M w.length s b) = true
    42
    43end Lax733996.ConfigurationGraph
    44
    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…