Structured recursion schemes such as folds and unfolds have been widely used for structuring both functional programs and program semantics. In this context, it has been customary to implement denotational semantics as folds over an inductive data type to ensure termination and compositionality. Separately, operational models can be given by unfolds, and naturally not all operational models coincide with a given denotational semantics in a meaningful way. To ensure these semantics are coherent it is important to consider the property of full abstraction which relates the denotational and the operational model. In this paper, we show how to engineer a compositional semantics such that full abstraction comes for free. We do this by using distributive laws from which we generate both the operational and the denotational model. The distributive laws ensure the semantics are fully abstract at the type level, thus relieving the programmer from the burden of the proofs.
翻译：折叠和展出等结构性递解计划已被广泛用于构建功能性程式和程序语义结构。 在这方面,通常的做法是在一种感化数据类型上实施分解语义,作为折叠,以确保终止和组成性。 另外,操作模型可以由展出提供,而且自然并非所有操作模型都与特定脱记语义以有意义的方式相吻合。为确保这些语义的一致性,必须考虑与分解和操作模式相关的完全抽象属性。在本文中,我们展示了如何设计一种完全抽象的拼写语义,这样完全抽象就自由了。我们这样做的方法是使用分解法,我们从中产生操作和分解模式。分解法确保语义在类型层面完全抽象,从而减轻程序员的举证责任。</s>
相关内容
微信扫码咨询专知VIP会员