Cypher is Turing-Complete: A Formal Proof via 2-Counter Machine Simulation

TL;DR

This paper formally proves that Cypher, Neo4j's graph query language, is Turing-complete by demonstrating its ability to simulate a 2-counter machine through various constructions verified on a live database.

Contribution

The authors provide the first formal proof of Cypher's Turing-completeness using multiple simulation methods, including a novel graph-native approach.

Findings

Cypher can simulate any 2-counter machine.

All three simulation methods were verified on Neo4j Aura.

The proof addresses and resolves the bounded-step objection.

Abstract

We prove that Cypher 25, the graph query language of Neo4j, is Turing-complete. The proof shows that a single RETURN statement using reduce(), CASE expressions, and list comprehensions can simulate any 2-counter machine (Minsky 1967). We address the bounded-step objection via two complementary resolutions and present a third graph-native simulation using quantified path patterns (QPP) with allReduce. All three constructions were verified on a live Neo4j Aura instance.