On Pitts' Relational Properties of Domains

TL;DR

This paper explores Pitts' relational properties of domains, connecting his fixed-point construction to various fundamental fixed-point theorems and modern recursive domain techniques.

Contribution

It demonstrates that Pitts' construction can be viewed through the lens of multiple fixed-point theorems, linking classical and modern recursive domain methods.

Findings

Pitts' construction aligns with inverse limit, Banach, and Kleene fixed-point theorems.

The connection highlights the relationship between recursive domain construction and fixed-point methods.

The framework relates to guarded recursion and step-indexing techniques in modern semantics.

Abstract

Andrew Pitts' framework of relational properties of domains is a powerful method for defining predicates or relations on domains, with applications ranging from reasoning principles for program equivalence to proofs of adequacy connecting denotational and operational semantics. Its main appeal is handling recursive definitions that are not obviously well-founded: as long as the corresponding domain is also defined recursively, and its recursion pattern lines up appropriately with the definition of the relations, the framework can guarantee their existence. Pitts' original development used the Knaster-Tarski fixed-point theorem as a key ingredient. In these notes, I show how his construction can be seen as an instance of other key fixed-point theorems: the inverse limit construction, the Banach fixed-point theorem and the Kleene fixed-point theorem. The connection underscores how Pitts' construction is intimately tied to the methods for constructing the base recursive domains themselves, and also to techniques based on guarded recursion, or step-indexing, that have become popular in the last two decades.