Expressiveness and Extensions of an Instruction Sequence Semigroup
Stephan Schroevers

TL;DR
This paper analyzes the expressiveness of instruction sequence semigroups, introducing Cg with label and goto instructions, and explores how restrictions on instruction sets affect their expressive power.
Contribution
It introduces the Cg semigroup with label and goto instructions and compares its expressiveness to C, showing how instruction set restrictions impact expressiveness.
Findings
Cg is equally expressive as C, and can be translated to and from C.
Restricting instruction sets to finitely many instructions reduces expressiveness.
Infinite instruction sets maintain full expressiveness regardless of direction.
Abstract
PGA, short for ProGram Algebra, describes sequential programs as finite or infinite (repeating) sequences of instructions. The semigroup C of finite instruction sequences was introduced as an equally expressive alternative to PGA. PGA instructions are executed from left to right; most C instructions come in a left-to-right as well as a right-to-left flavor. This thesis builds on C by introducing an alternative semigroup Cg which employs label and goto instructions instead of relative jump instructions as control structures. Cg can be translated to C and vice versa (and is thus equally expressive). It is shown that restricting the instruction sets of C and Cg to contain only finitely many distinct jump, goto or label instructions in either or both directions reduces their expressiveness. Instruction sets with an infinite number of these instructions in both directions (not necessarily…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Software Testing and Debugging Techniques
