Periodic Single-Pass Instruction Sequences

TL;DR

This paper introduces a formal notation for periodic single-pass instruction sequences, relating them to program algebra and establishing a mathematical foundation for analyzing such programs.

Contribution

It develops a linear notation for periodic instruction sequences, connects them to program algebra, and provides axioms for their equivalence and extraction.

Findings

Characterizes periodic instruction sequences as a subsemigroup

Establishes axioms for single-pass congruence and structural congruence

Provides a basis for analyzing programs using PGA tools

Abstract

A program is a finite piece of data that produces a (possibly infinite) sequence of primitive instructions. From scratch we develop a linear notation for sequential, imperative programs, using a familiar class of primitive instructions and so-called repeat instructions, a particular type of control instructions. The resulting mathematical structure is a semigroup. We relate this set of programs to program algebra (PGA) and show that a particular subsemigroup is a carrier for PGA by providing axioms for single-pass congruence, structural congruence, and thread extraction. This subsemigroup characterizes periodic single-pass instruction sequences and provides a direct basis for PGA's toolset.