Manuscript En06-A@1 · En06-A.tex · section · e04c9892

Enter accounting and optional syntactic realization

Enter accounting and optional syntactic realization · lines 700–717

Back to manuscript

This is the comparison with En04-A thm:soundness, Hawk04-B thm:adequacy, and En02-C thm:C1 CheungEn04A,CheungHawk04B,CheungEn02C.

A block is calculus generated only if a well-typed program over the available library denotes its complete instrument. A finite network of such blocks realizes a composite program only when sequential composition, parallel ownership, and input/output wiring match. Those are additional syntactic requirements. Strong normalization concerns reductions of a fixed term, not externally inserted idle ticks or an indefinitely driven substrate.

No exact finite-gate compilation of arbitrary specified instruments, no efficiency claim, and no support-preserving normalization of arbitrary adaptive wiring are asserted here.

Nearby in this section