Two Canonical Forms for Programs

Since theories of computation provide (among other things) formal framework for practical program minimization, and since a distinction between program syntax and semantics can be based on the possibility of performing such minimization algorithmically, it is reasonable to formulate the theory of computation as a theory of machines controlled by programs which are in themselves purely syntactic. Here the algebraic structure of programs in such a theory is presented. Two canonical forms are exhibited, characterizing respectively strong (syntactic) and weak (computational) equivalence of programs.