论 Pitts 的域关系性质

Andrew Pitts 的域关系性质框架是一种在域上定义谓词或关系的强有力方法，其应用范围从程序等价性的推理原则到连接指称语义与操作语义的适切性证明。其主要吸引力在于处理并非显然良基的递归定义：只要相应域也以递归方式定义，且其递归模式与关系的定义适当对齐，该框架就能保证它们的存在。Pitts 最初的展开以 Knaster-Tarski 不动点定理为关键要素。在这些笔记中，我展示了他的构造如何被视为其他关键不动点定理的实例：逆极限构造、Banach 不动点定理与 Kleene 不动点定理。这一联系凸显了 Pitts 的构造与构造基础递归域本身的方法，以及与近二十年来流行的基于守卫递归或步索引的技术的紧密关联。