线性相依类型与相对完备性
Linear Dependent Types and Relative Completeness
摘要：
本文介绍了一个具有完全高阶递归的λ演算的线性相关类型系统dlPCF，并证明了它是可靠的和相对完备的.完整性在很强的意义上成立：dlPCF不仅能够精确地捕获PCF程序的功能行为（即输出如何与输入相关），而且还能够捕获它们的一些内涵属性，即用Krivine机器评估它们的复杂性。dlPCF是围绕依赖类型和线性逻辑设计的，并在索引项的底层语言上进行参数化，索引项可以进行调优，从而牺牲完整性以换取易处理性。
英文摘要：
A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of PCF programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of evaluating them with Krivine's Machine. dlPCF is designed around dependent types and linear logic and is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
