Manuscript En05-A@1 · En05-A.tex · section · f076e703
The compositional requirement
Finite programs, syntactic admissibility, and routing › The compositional requirement · lines 687–695
For a concrete strongly normalizing calculus, the relevant metatheoretic clauses are recorded in Appendix app:interface. Assumption ass:programinterface is explicit because separate evaluability of block terms does not by itself imply that arbitrarily concatenated block evaluations are reductions of one fixed original term.
Nearby in this section
- assumption: Assumption: Finite compositional program interface
- definition: Definition: Syntactic admissibility
- section: The compositional requirement
- proposition: Proposition: Finite path accounting
- section: The compositional requirement
- proposition: Proposition: Soundness of finite syntactic networks
- remark: Remark: Finite network versus one strongly normalizing term