Reducibility and TT-Lifting for Computation Types
Reducibility and TT-Lifting for Computation Types
复制标题
计算类型的可归约性和 TT-Lifting
DOI：
10.1007/11417170_20
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Ian Stark
中科院分区：
文献类型：
--
作者：
S. Lindley;Ian Stark
我们提出了一种将运算谓词扩展到Moggi的一元计算类型的技术，这种技术与一元的选择无关。我们将该方法应用于Girard-Tait约化，用它来证明计算元语言λml的强归一化。可约性的特殊挑战是，当“计算”的确切含义（有状态的、副作用的、不确定的等）未指定时，将这个语义概念应用于计算类型。我们的解决方案是为延续定义可简化性，并使用它来支持从值类型到计算类型的跳转。该方法似乎是鲁棒的：我们应用它来显示具有和扩展的计算元语言的强规范化，以及例外。基于这些结果，以及先前对局部状态的研究，我们建议这种“跨越式”方法提供了一种通用方法，可以将在值类型上定义的概念提升到计算的可观察属性。
We propose ⊤⊤-lifting as a technique for extending operational predicates to Moggi's monadic computation types, independent of the choice of monad. We demonstrate the method with an application to Girard-Tait reducibility, using this to prove strong normalisation for the computational metalanguage λml. The particular challenge with reducibility is to apply this semantic notion at computation types when the exact meaning of “computation” (stateful, side-effecting, nondeterministic, etc.) is left unspecified. Our solution is to define reducibility for continuations and use that to support the jump from value types to computation types. The method appears robust: we apply it to show strong normalisation for the computational metalanguage extended with sums, and with exceptions. Based on these results, as well as previous work with local state, we suggest that this “leap-frog” approach offers a general method for raising concepts defined at value types up to observable properties of computations.