Electricity is constructive : the equivalence between electrical propagation and constructive Boolean calculation for cyclic synchronous circuits

The proof requires the development of new intuitionistic logics of electrical stabilization, as well as the proof of several intermediate theorems establishing the equivalence of the electrical model obtained, and a system of purely syntactic deduction rules that allows circuit operation to be simulated, limited to voltage stabilization and ignoring transients. It is essentially due to Michel Mendler (U. Bamberg, Germany). It is stronger and more rigorous than previous proofs (Shiple-Berry-Touati 2001), based on event graphs analyzing transients in a more constrained and less natural delay model (Brzozowski-Seger model).

First, I'll recall the source of the problem: cyclic circuits appear naturally when high-level languages such as Esterel are translated into circuits, and they are quite natural for implementing fundamentally symmetrical algorithms. I'll mention S. Malik's example, which shows that cyclic circuits can be exponentially smaller than acyclic circuits for the same function, then the cyclic arbiter for token buses, and finally the new example of instruction slicing in Pentiums. But the analysis of their behavior is non-trivial, and cyclic circuits don't generally stabilize, hence the problem.

Next, I'll introduce the new UN logic(up-bounded non-inertial delays). Its model represents the electrical histories of wires, gates and delays, focusing solely on the stabilization of their voltages. It provides a simple way of encoding circuit logic and delays. I will then define the deduction rules used to symbolically simulate electrical execution. I'll present the theorems expressing the equivalence between model and deductive system, followed by the result demonstrating the intuitionism of logic. It is precisely this intuitionistic character that makes it possible to demonstrate the determinism of voltage stabilization, which can only take place on a single value per output.

Once these central results have been demonstrated, a simple sleight of hand makes the delays disappear altogether, by showing that output stability can be calculated in a simple constructive Boolean calculation (without excluded thirds), i.e. outside time. The simple corollary is that a circuit that stabilizes its outputs in constructive Boolean logic does so electrically for all wire and gate delays and at the same values, which is the desired end result.

This theory does not yet provide a simple algorithm for determining whether a cyclic circuit stabilizes or oscillates. Such an algorithm, based on Scott's ternary logic, will be demonstrated in the following lecture on April 2. It will be extended to the most general register circuits.