Structure Computer

Structure Computer computes the structure of systems whose state changes one step at a time by a fixed rule (discrete dynamical systems), exactly, and attaches to every answer a certificate that a third party can check.

A numerical simulation answers "what happens next?", approximately. Structure Computer answers the other side: "which states are reached, and which never are?" and "what never changes?" — with arithmetic that never rounds, and with mathematical theorems proved in advance.

Structure Computer is patent pending.

The systems

A state is a tuple of numbers, and the next state is given by formulas built from the four arithmetic operations (rational functions). For example, Lyness's recurrence

xₙ₊₁ = (1 + xₙ) / xₙ₋₁

becomes, with the state (x, y) = (xₙ₋₁, xₙ), the system whose step is

(x, y) ↦ (y, (1 + y) / x).

Rules like this appear in structure-preserving numerical methods (integrators), in the study of integrable maps, and in reversible computation. A system is either a known one chosen by name, or a short text listing its variables, parameters and step formulas (a system file; see Examples).

The central question: how many steps from s to t?

Run the system above from s = (1, 2):

(1, 2) → (2, 3) → (3, 2) → (2, 1) → (1, 1) → (1, 2)

It is back after 5 steps. So t = (2, 1) is reached in 3 steps, and also in 8, 13, …; and since the rule can be run backwards, going 2 steps back (n = −2) reaches it too. Structure Computer answers

t = σⁿ s ⇔ n ≡ 3 (mod 5)

where σ is one step and n ≡ 3 (mod 5) means "n leaves remainder 3 when divided by 5". In one statement it gives every step count that reaches t, forwards or backwards, and says that no other count does.

The answer is one of three:

Answer	Meaning
t = σⁿ s ⇔ n ≡ r (mod M)	n steps reach t exactly when n leaves remainder r on division by M
no path	no number of steps, forwards or backwards, reaches t
s is not regular	going forwards or backwards from s runs into a state where the formulas are undefined (a division by zero); if t is reached before that, the step count is given

On this site the question is written Id(s, t). The notation is borrowed from type theory, where it stands for the evidence that two things are equal; here it stands for the paths (step counts) from s to t.

Exact arithmetic: finite fields and the rationals

In floating-point arithmetic rounding errors pile up, and behaviour over long times can no longer be trusted. Structure Computer computes in two number systems where nothing is rounded:

𝔽_q (a finite field): arithmetic with the remainders on division by a prime q. Just as a clock hand goes back to 0 after passing 12, every value is a whole number from 0 to q − 1.
ℚ (the rationals): fractions, kept exactly as fractions.

For large q an orbit can be far too long to follow step by step. For the following known families, Structure Computer answers from theorems proved in Lean, without following the orbit:

the Lyness map
the Euler top (a rotating rigid body) discretised by Kahan's method
linear maps with determinant 1 (such as a discretised harmonic oscillator)
one discretisation of geodesics on a hyperboloid

For any other system it follows the orbit up to a set limit, and answers "no result" beyond it.

How the answers are guaranteed

Structure Computer is built so that the part that computes does not have to be trusted.

The computing part produces the answer and cheap hints to confirm it.
The question, the answer, the hints, the presuppositions and the names of the theorems relied on go into a certificate.
A separate program, the checker, re-checks the answer from the definitions, using only the certificate.
If the check fails, the answer is recomputed; if it fails again, the answer is "no result", with the reason.

For the main kinds of answer, the statement "if the conditions the checker confirms hold, the answer is correct" is proved in advance as a theorem in Lean, a proof assistant in which a computer checks a mathematical proof line by line. The certificate cites those theorems by name, so anyone who holds it can confirm the answer with the checker. Questions about the Lyness map over 𝔽_q can also be checked by a checking program whose own correctness is proved in Lean.

Every result carries a kind that says how far it can be trusted:

Kind	Meaning
Certain	correct by the check and the theorems
Probably certain	the chance of an error is guaranteed to be negligible
Reconstructed	a value found under the assumption of an upper bound on its size
Statistical	a judgement from samples
No result	no answer could be given; the reason is stated

Nothing that cannot be confirmed is called certain.

What is new about Structure Computer

There are already tools for studying discrete dynamical systems, but each falls short somewhere. A numerical simulation's answer is approximate, and it cannot say "never reached". Computer algebra gives answers, but no evidence with which others can confirm them independently. A proof assistant checks theorems, but does not compute the answer to a particular question about a particular system. Structure Computer brings the three together.

Exact answers: to "how many steps?", it answers without error with every step count that reaches t and the statement that no other count does. "No path", too, does not mean "not found within the steps followed"; it is the claim that no number of steps reaches t.
A certificate for every answer: every answer comes with a certificate that can be checked without trusting the side that computed it. Anyone, not only whoever ran the computation, can confirm it with the checker.
Backed by theorems: the correctness of the answers rests on theorems proved in Lean. They are not checked one q at a time but proved for finite fields in general, exceptional cases included.
Answers questions of enormous size: for the known families, it answers from theorems even for q so large that following the orbit step by step would never finish.
Says when it does not know: every result carries a kind that says how certain it is, and nothing that cannot be confirmed is called certain.

Intended uses

It is intended for uses such as:

in designing structure-preserving numerical methods, settling invertibility and conserved quantities exactly rather than by long floating-point test runs
in research on integrable maps, arithmetic dynamics and reversible computation, presenting periods and conserved quantities in a form anyone can re-check
keeping computed results as evidence that a third party can check without redoing the whole computation

What it does not do

It handles rules written with the four arithmetic operations (polynomials and rational functions).
A finite field has no order and no distance, so questions of nearness — how close orbits come, how errors grow — are outside its scope. It complements numerical simulation rather than replacing it.
For a system it does not recognise as a known family, questions over large q cannot be answered by a theorem: the orbit is followed up to the limit, and beyond it the answer is "no result".

Try it

Try: enter a system and two states; Id(s, t) and the other questions are computed together
Examples: systems and questions ready to try
The questions, Reading the results, and a glossary, Certificates and checking, Writing system files, Frequently asked questions: how to use it