Tutorial 41

Temporal Tau, Part I

Learn how bounded LTL-style operators fit Tau, why finite-horizon temporal formulas are decidable on finite carriers, and how this creates a new optimizer layer without claiming full unbounded temporal reasoning.

View source Built 2026-05-20

This tutorial is about adding time to Tau without losing decidability.

The previous optimization tutorial focused on quantifier elimination. That was a solver-routing problem: choose the right qelim backend only when a fragment guard proves that the route is legal.

Temporal Tau is a different layer. It asks how a Tau expression should be read at time $t$, time $t+1$, and over a bounded future window. The checked result is not “all temporal logic is solved.” The checked result is narrower and more useful:

bounded LTL-style Tau expressions are decidable over finite Boolean-algebra carriers.

The proof chain is:

c133 adds explicit next and prev operators.
c135 adds bounded always and bounded eventually.
c136 adds bounded until.
c140 proves bounded satisfiability, validity, and equivalence are decidable when the carrier is finite and equality is decidable.

Scope

This tutorial explains a bounded temporal fragment. It does not claim unbounded LTL synthesis, infinite-time model checking, or full Tau runtime integration.

Bounded temporal Tau is finite-horizon reasoning. The formulas look forward only through a fixed window, which is why the decidability proof can stay finite.

Part I: The table is now time-indexed

The carrier used in the proof is a table:

\[\operatorname{Table}(n,\alpha) := (\operatorname{Fin}(n)\to\operatorname{Bool})\to\alpha.\]

Standard reading. A table of arity $n$ with values in $\alpha$ is a function from Boolean assignments over $n$ finite input positions to a Boolean-algebra value in $\alpha$.

Plain English. For each finite input pattern, the table returns a Boolean-algebra value.

Trap. The word “table” does not mean a spreadsheet of numbers. The output value is a Boolean-algebra element, so it can be met, joined, complemented, and compared by the Boolean order.

Temporal evaluation adds a time coordinate:

\[\operatorname{Eval}_T(e,t) : \operatorname{Table}(n,\alpha).\]

Standard reading. Evaluating temporal expression $e$ at time $t$ returns a table.

Plain English. The same expression can have different table meanings at different time steps.

Trap. The time coordinate is external to the table key. A key chooses a Boolean input pattern; the time coordinate chooses which tick of the trace is being read.

Part II: The one-step temporal operators

The first temporal operator is next:

\[\operatorname{Eval}_T(\operatorname{next}(e),t) = \operatorname{Eval}_T(e,t+1).\]

Standard reading. Evaluating next e at time $t$ is the same as evaluating $e$ at time $t+1$.

Plain English. next shifts the expression one tick into the future.

The prev operator has a boundary condition:

\[\operatorname{Eval}_T(\operatorname{prev}(e),0)=\bot, \qquad \operatorname{Eval}_T(\operatorname{prev}(e),t+1)=\operatorname{Eval}_T(e,t).\]

Standard reading. At time $0$, prev e evaluates to bottom. At successor time $t+1$, prev e evaluates to what $e$ evaluated to at time $t$.

Plain English. prev reads one tick backward, but there is no earlier tick before time $0$, so the proof chooses bottom there.

Trap. The bottom value at time $0$ is a design choice in the checked model. Another runtime could choose an explicit error or option type, but then the proof surface would be different.

Part III: Bounded always and bounded eventually

Unbounded temporal logic talks about all future time. That is powerful, but it is not the proof surface here.

The bounded always operator is:

\[\operatorname{Eval}_T(\Box_{<N}e,t) = \bigwedge_{i<N}\operatorname{Eval}_T(e,t+i).\]

Standard reading. Evaluating bounded always for $N$ steps is the meet of the evaluations of $e$ at times $t,t+1,\ldots,t+N-1$.

Plain English. The property must hold at every tick in the finite window.

The bounded eventually operator is:

\[\operatorname{Eval}_T(\Diamond_{<N}e,t) = \bigvee_{i<N}\operatorname{Eval}_T(e,t+i).\]

Standard reading. Evaluating bounded eventually for $N$ steps is the join of the evaluations of $e$ at times $t,t+1,\ldots,t+N-1$.

Plain English. The property must hold at least somewhere in the finite window.

Trap. These are bounded operators. $\Box_{<N}$ is not the unbounded LTL operator $\Box$, and $\Diamond_{<N}$ is not the unbounded LTL operator $\Diamond$. The finite bound is what keeps the evaluator structurally recursive.

The bounded De Morgan law has the expected form:

\[\neg\Box_{<N}e = \Diamond_{<N}\neg e.\]

Standard reading. The complement of “always $e$ within $N$ steps” equals “eventually not $e$ within $N$ steps.”

Plain English. A finite window fails an always-check exactly when the window contains a counterexample.

Part IV: Bounded until

The bounded until operator is the most important temporal connective for protocol specifications.

The recursive law is:

\[p\,U_{<0}\,q := \bot, \qquad p\,U_{<N+1}\,q := q\vee(p\wedge\operatorname{next}(p\,U_{<N}\,q)).\]

Standard reading. At horizon $0$, bounded until is bottom. At horizon $N+1$, $p$ until $q$ holds if $q$ holds now, or if $p$ holds now and the bounded-until condition holds over the remaining $N$ future steps.

Plain English. Either the goal has already arrived, or the guard must hold now while the same question is passed to the next tick with one fewer step left.

Trap. The guard $p$ does not have to hold after $q$ appears. The word “until” means “keep $p$ true up to the first successful $q$-point,” not “keep $p$ true forever.”

This is the bounded version of the standard LTL idea:

\[p\,U_{<N}\,q \quad\text{means}\quad \exists j<N.\ \operatorname{Eval}_T(q,t+j)\ne\bot \ \wedge\ \forall i<j.\ \operatorname{Eval}_T(p,t+i)\ne\bot.\]

Standard reading. There is a future offset $j$ inside the $N$-step window where $q$ holds, and at every earlier offset $i<j$, $p$ holds.

Plain English. Reach $q$ before the window closes, while maintaining $p$ on the way there.

Trap. This existential reading is a helpful semantic explanation. The Lean proof uses the recursive definition because it gives a structurally terminating evaluator.

Part V: The decidability theorem

The decisive theorem in c140 is not a new temporal law. It is a finite decision boundary.

The assumptions are:

\[\operatorname{Finite}(\alpha) \quad\wedge\quad \operatorname{DecidableEq}(\alpha) \quad\wedge\quad \operatorname{BooleanAlgebra}(\alpha).\]

Standard reading. The value carrier alpha is finite, equality on that carrier is decidable, and the carrier is a Boolean algebra.

Plain English. There are finitely many possible output values, equality can be checked, and the values support the Boolean operations Tau needs.

Under those assumptions, pointwise equality of evaluations is decidable:

\[\operatorname{Decidable} \left( \operatorname{Eval}_T(e_1,t)=\operatorname{Eval}_T(e_2,t) \right).\]

Standard reading. For two temporal Tau expressions $e_1,e_2$ at a fixed time $t$, there is a decision procedure for whether their evaluated tables are equal.

Plain English. At a fixed tick, the checker can decide whether two bounded temporal expressions mean the same table.

Bounded satisfiability is decidable:

\[\operatorname{Decidable} \left( \exists t\le T.\ \exists k.\ \operatorname{Eval}_T(e,t)(k)\ne\bot \right).\]

Standard reading. There is a decision procedure for whether some time $t$ up to horizon $T$ and some Boolean input assignment $k$ make $e$’s evaluation non-bottom.

Plain English. Within the bounded horizon, the checker can decide whether the property is ever possible.

Bounded validity is decidable:

\[\operatorname{Decidable} \left( \forall t\le T.\ \forall k.\ \operatorname{Eval}_T(e,t)(k)=\top \right).\]

Standard reading. There is a decision procedure for whether every time $t$ up to horizon $T$ and every Boolean input assignment $k$ make $e$’s evaluation top.

Plain English. Within the bounded horizon, the checker can decide whether the property always holds.

Bounded equivalence is decidable:

\[\operatorname{Decidable} \left( \forall t\le T.\ \operatorname{Eval}_T(e_1,t)=\operatorname{Eval}_T(e_2,t) \right).\]

Standard reading. There is a decision procedure for whether $e_1$ and $e_2$ evaluate to the same table at every time up to horizon $T$.

Plain English. Within the bounded horizon, the checker can decide whether two temporal expressions are equivalent.

Trap. The theorem is finite twice: the time horizon is finite, and the carrier is finite. Removing either condition changes the problem.

Part VI: What this gives Tau

The qelim tutorial showed one optimizer shape:

recognize fragment
dispatch to exact backend
fall back outside the fragment

Temporal Tau gives a second optimizer shape:

make time explicit
bound the horizon
evaluate structurally
decide satisfiability, validity, or equivalence over the finite surface

This opens several practical compiler passes:

next can be pushed through Boolean operations.
alwaysWithin and eventuallyWithin can be unfolded into finite meet and join chains.
untilWithin can be unfolded into a finite recursive expression.
bounded equivalence can justify temporal simplification.
bounded satisfiability can support temporal counterexample search.

The important boundary is that these are bounded passes. They help Tau reason about a finite trace window. They do not replace unbounded temporal synthesis, omega-automata, or full infinite-trace LTL.

Part VII: What to remember

Temporal Tau is not another qelim backend. It is an execution and optimization layer for time-indexed expressions.

The core ladder is:

Add a time coordinate to evaluation.
Read next as a one-step future shift.
Read bounded always as a finite meet.
Read bounded eventually as a finite join.
Read bounded until as a recursive guarded search for a goal.
Use finiteness of the carrier and the horizon to obtain decidability.

The result is strong because it is modest. It gives a mechanically checked finite-horizon temporal fragment, and that is exactly the kind of fragment that can become a safe Tau optimizer layer.