Program algebra with a jump-shift instruction

TL;DR

This paper introduces jump-shift instructions in program algebra, demonstrating their theoretical benefits in maintaining expressive power with bounded jumps and enabling finite-state execution mechanisms.

Contribution

It presents a novel extension to PGA with jump-shift instructions, showing they preserve expressive power and facilitate finite-state thread production.

Findings

Jump-shift instructions do not reduce expressive power.

Finite-state mechanisms can produce all finite-state threads.

Jump-shift instructions enable bounded jump reachability.

Abstract

We study sequential programs that are instruction sequences with jump-shift instructions in the setting of PGA (ProGram Algebra). Jump-shift instructions preceding a jump instruction increase the position to jump to. The jump-shift instruction is not found in programming practice. Its merit is that the expressive power of PGA extended with the jump-shift instruction, is not reduced if the reach of jump instructions is bounded. This is used to show that there exists a finite-state execution mechanism that by making use of a counter can produce each finite-state thread from some program that is a finite or periodic infinite sequence of instructions from a finite set.