Projection semantics for rigid loops

TL;DR

This paper introduces a formal semantics for rigid loops in program algebra, providing two equivalent semantic projections and establishing their normative and algorithmic adequacy.

Contribution

It develops a novel semantic framework for rigid loops in program algebra, with two proven equivalent semantic projections and criteria for their adequacy.

Findings

Two semantic projections are proven equivalent.

Semantic projections meet normative and algorithmic adequacy criteria.

Framework enhances understanding of rigid loop semantics.

Abstract

A rigid loop is a for-loop with a counter not accessible to the loop body or any other part of a program. Special instructions for rigid loops are introduced on top of the syntax of the program algebra PGA. Two different semantic projections are provided and proven equivalent. One of these is taken to have definitional status on the basis of two criteria: `normative semantic adequacy' and `indicative algorithmic adequacy'.