Lax extensions of set functors play a key role in various areas including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is induced by a class of predicate liftings; we discuss several implications of this result.
翻译:集合函子的Lax扩张在拓扑学、并发系统以及模态逻辑等多个领域中扮演着关键角色,而谓词提升则为模态算子提供了通用语义。本文从富量化关系(quantale-enriched relations)的视角重新审视Lax扩张与谓词提升之间的关联。基于这一视角,我们特别论证了若干基础概念与结果可自然导出,且其证明过程极为简明。最终,我们证明了每个Lax扩张均可由一类谓词提升所诱导,并讨论了该结果的若干推论。