Restriction in Program Algebra

TL;DR

This paper develops finite axiomatisations for various partial function operations in program algebra, including domain restriction, override, update, and intersection, motivated by computer science applications.

Contribution

It introduces new finite, often equational, axiomatisations for partial function signatures involving domain restriction and other operations.

Findings

Finite axiomatisations for domain restriction and related operations.

Many axiomatisations are equational and explicitly formalized.

Provides a foundational framework for reasoning about partial functions in programming.

Abstract

We present axiomatisations for a number of partial function signatures that include domain restriction, modelled as a right normal band operation. Other operations considered are override and update, difference, minus, intersection, composition and domain, all of which find motivation in computer science. All axiomatisations found are finite, many of them equational.