pith. machine review for the scientific record. sign in

arxiv: 2605.08555 · v1 · submitted 2026-05-08 · 💻 cs.FL · cs.CC

Recognition: 2 theorem links

· Lean Theorem

Entropy of pebble automata and space complexity

J. Andres Montoya
Authors on Pith no claims yet

Pith reviewed 2026-05-12 01:16 UTC · model grok-4.3

classification 💻 cs.FL cs.CC
keywords NLlogCFLpebble automataentropyspace complexityLPtime
0
0 comments X

The pith

NL differs from logCFL, which separates L from Ptime and NL from Ptime.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves NL is strictly larger than logCFL, the closure of context-free languages under logspace reductions. The argument relies on bounding the entropy of pebble automata to show that certain languages recognizable in nondeterministic logspace cannot be obtained from context-free languages via logspace reductions. If correct, the result immediately yields that deterministic logspace differs from polynomial time and that nondeterministic logspace differs from polynomial time.

Core claim

We prove that NL is different from logCFL. This result implies L different from Ptime and the stronger separation NL different from Ptime.

What carries the argument

Entropy of pebble automata, used to measure space complexity and establish that no logspace reduction maps an NL language into the context-free languages.

If this is right

  • L differs from Ptime
  • NL differs from Ptime
  • No logspace reduction can turn an NL-complete problem into a context-free language

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar entropy arguments on pebble automata might separate other space-bounded classes from their logspace closures.
  • The technique could be tested by checking whether specific NL problems such as reachability on graphs of bounded treewidth belong to logCFL.

Load-bearing premise

The entropy bound on pebble automata correctly prevents any logspace reduction from mapping certain nondeterministic logspace languages onto context-free languages.

What would settle it

Exhibiting an explicit logspace reduction from the directed s-t connectivity problem to any context-free language would falsify the separation.

read the original abstract

Let L denote the class Logpsace and NL the class NLogspace. We use logCFL to denote the closure under logspace reductions of the set of context-free languages. We prove that NL is different from logCFL. This result implies L different from Ptime and the stronger separation NL different from Ptime.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The manuscript asserts a proof that NL is distinct from logCFL (the logspace closure of context-free languages), implying L ≠ P and NL ≠ P, based on entropy of pebble automata.

Significance. If the proof is correct, this would constitute a significant advance by separating important complexity classes that have been open for decades. However, the manuscript supplies no technical details to evaluate the claim.

major comments (1)
  1. The abstract claims to prove NL ≠ logCFL but the manuscript contains no definitions of the automata models, entropy measures, no lemmas, no equations, and no derivation or proof sketch. This absence means the central claim is unsupported and cannot be assessed for correctness.
minor comments (1)
  1. The title references pebble automata entropy but these terms are not introduced or used in the provided text.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for reviewing our manuscript and for highlighting the need for technical details to support the central claim.

read point-by-point responses

  1. Referee: The abstract claims to prove NL ≠ logCFL but the manuscript contains no definitions of the automata models, entropy measures, no lemmas, no equations, and no derivation or proof sketch. This absence means the central claim is unsupported and cannot be assessed for correctness.

    Authors: The referee correctly observes that the submitted manuscript consists only of a brief statement of the result and supplies none of the required definitions for pebble automata or entropy measures, nor any lemmas, equations, or proof sketch. This omission means the claim cannot be evaluated from the text as provided. We will prepare a revised version that incorporates the missing definitions, formal measures, and a detailed derivation of the separation. revision: yes

Circularity Check

0 steps flagged

No derivation chain or equations present; separation claim asserted without proof steps

full rationale

The provided manuscript text consists solely of the abstract stating the claim that NL differs from logCFL (with implied consequences for L vs Ptime), without any definitions of pebble automata, entropy, reductions, lemmas, equations, or proof details. Since no derivation steps exist to inspect for self-definition, fitted predictions, or self-citation chains, no circularity is detectable. The result is simply ungrounded rather than circular.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No free parameters, axioms, or invented entities are described in the abstract; the claim rests entirely on an undescribed proof.

pith-pipeline@v0.9.0 · 5327 in / 1030 out tokens · 52088 ms · 2026-05-12T01:16:51.135273+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

6 extracted references · 6 canonical work pages

  1. [1]

    SIAM Journal on Computing

    Greibach, S.: The Hardest Context-Free Language. SIAM Journal on Computing. 2(4), 304-310 (1973)

    work page 1973

  2. [2]

    Journal of Computer and System Sciences

    Jones, N.: Space-bounded reducibility between combinatorial problems. Journal of Computer and System Sciences. 11(1), 68-85 (1975)

    work page 1975

  3. [3]

    Zeitschrift für mathematische Logik und Grundlagen der Mathematik

    Kreider, D., Ritchie, R.: Abasistheoremforaclassoftwo-wayautomata. Zeitschrift für mathematische Logik und Grundlagen der Mathematik. 12, 243–255 (1966)

    work page 1966

  4. [4]

    Bell Systems Technical Journal

    Shannon, C.: A Mathematical Theory of Communication. Bell Systems Technical Journal. 27(3), 379-423 (1948)

    work page 1948

  5. [5]

    Journal of the Association for Computing Machinery

    Sudborough, I.: On the complexity of context-free languages. Journal of the Association for Computing Machinery. 25(4), 670-681 (1978)

    work page 1978

  6. [6]

    Information and Control

    Younger, D.: Recognition and parsing of context-free languages in time n3. Information and Control. 10 (2), 189–208 (1967). 35

    work page 1967