节省空间的潜在合同
Space-Efficient Latent Contracts
摘要:
标准的高阶合约监控会破坏尾递归并导致空间泄漏,这可能会改变程序的渐近复杂度;空间效率会恢复尾递归并限制合约使用的空间量。对执行简单类型规则(a/k/a渐进类型)的合同进行空间有效的合同监控已经得到了很好的研究。先前的工作为没有依赖性的显式合约建立了一个空间有效的语义(Greenberg 2015);我们将这项工作适应于具有依赖性的潜在演算。当不使用依赖关系时,我们保证空间效率;当使用依赖关系时,我们通常不能保证空间效率,而是提供一个框架,使这些程序在逐个情况下具有空间效率。
英文摘要:
Standard higher-order contract monitoring breaks tail recursion and leads to space leaks that can change a program's asymptotic complexity; space-efficiency restores tail recursion and bounds the amount of space used by contracts. Space-efficient contract monitoring for contracts enforcing simple type disciplines (a/k/a gradual typing) is well studied. Prior work establishes a space-efficient semantics for manifest contracts without dependency (Greenberg 2015); we adapt that work to a latent calculus with dependency. We guarantee space efficiency when no dependency is used; we cannot generally guarantee space efficiency when dependency is used, but instead offer a framework for making such programs space efficient on a case-by-case basis.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。