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.

翻译：Andrew Pitts的域关系属性框架是界定域际上游或域际关系的有力方法,其应用范围从方案等同的推理原则到证明脱记语义和操作语义充分性的证据等各种应用。其主要吸引力是处理没有明显充分依据的循环定义:只要相应的域也连带地界定,其递归模式与关系定义适当挂钩,该框架就能保证其存在。 Pitts的原始开发将Knaster-Tarski固定点的定点定理作为关键成份。在这些注释中,我展示了如何将他的构造视为其他关键定点定点定理的范例:反边界限构造、Banach固定点定点定点和Kleene固定点定点定点。 连接强调了Pitts的构造如何与基础递归域本身的构建方法紧密相连,以及在过去20年中变得流行的基于稳妥递归定点或逐步索引的技术。