{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R815",
  "content_hash": null,
  "slug": "twnfa-claim-current-frontier-2026-07-28",
  "type": "claim",
  "title": "The fixed-alphabet determinization question remains open",
  "summary": "The checked primary literature through 2026-07-28 still presents polynomial 2NFA-to-2DFA determinization as open. General conversion through a one-way DFA gives an exponential upper bound. Tight unary and recent one-way-liveness results give quadratic lower bounds.",
  "relevance": "For Polynomial determinization of two-way finite automata, record twnfa-claim-current-frontier-2026-07-28 (“The fixed-alphabet determinization question remains open”) records a bound, answer, status fact, or structural consequence. The record states: The checked primary literature through 2026-07-28 still presents polynomial 2NFA-to-2DFA determinization as open.",
  "relevance_source": "recorded",
  "body": "Sakoda and Sipser asked how many states are needed to replace nondeterminism by determinism when two-way head motion remains available. The canonical target fixes the input alphabet and asks whether the cost is polynomial in the number of source states.\n\nGuillon, Prigioniero, and Taheri describe the general determinization question as open in their STACS 2026 paper. They record an exponential upper bound obtained by eliminating two-way motion and passing to a one-way DFA. Their polynomial construction uses a stronger target device, a 1-limited automaton with a common-guess annotation, so it does not give a 2DFA.\n\nChrobak's Theorems 6.2 and 6.3 give a tight quadratic tradeoff for unary 1NFAs versus 2DFAs. This already supplies a fixed-alphabet quadratic lower bound for the one-way source subclass. Adeogun and Kapoutsis's arXiv v2, revised 2026-07-06, proves the explicit lower bound \\(h(h+1)/4\\) for every 2DFA solving one-way liveness of height \\(h\\), whose source language has an \\(h\\)-state 1NFA. The fixed-binary transfer recorded in this packet preserves that quadratic order and gives an explicit liveness-based binary family. These bounds remain within a polynomial cost and leave the canonical question unanswered.",
  "status": "reported",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "family",
    "statement": "2NFA-to-2DFA state complexity over each fixed finite input alphabet",
    "family": "all finite input alphabets fixed independently of the source state count"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.4230/LIPIcs.STACS.2026.48",
      "locator": "Guillon, Prigioniero, and Taheri, STACS 2026, Introduction, pp. 48:2-48:3. The separate July 2026 lower bound appears in metadata.references."
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4230/LIPIcs.STACS.2026.48",
    "locator": "Guillon, Prigioniero, and Taheri, STACS 2026, Introduction, pp. 48:2-48:3. The separate July 2026 lower bound appears in metadata.references."
  },
  "relations": [
    {
      "slug": "R811",
      "title": "Primary-source and duplicate audit through 2026-07-28",
      "object_type": "attempt",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R818",
      "title": "One-way liveness forces at least h(h+1)/4 deterministic states",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R819",
      "title": "Unary one-way NFAs have a tight quadratic two-way determinization cost",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R816",
      "title": "The one-way-liveness bound transfers to a fixed binary alphabet",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R812",
      "title": "The fixed-alphabet transfer stops at a quadratic lower bound",
      "object_type": "attempt",
      "relation": "constrains",
      "direction": "incoming"
    },
    {
      "slug": "R813",
      "title": "Test the proposed maximum length of the smooth-property chain",
      "object_type": "attempt",
      "relation": "addresses",
      "direction": "incoming"
    },
    {
      "slug": "R1818",
      "title": "The fixed-alphabet determinization question remains open",
      "object_type": "claim",
      "relation": "supersedes",
      "direction": "incoming"
    },
    {
      "slug": "two-way-nfa-polynomial-determinization",
      "title": "two way nfa polynomial determinization",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}