论文标题
逻辑框架dedukti中的足够和计算编码
Adequate and computational encodings in the logical framework Dedukti
论文作者
论文摘要
Dedukti是一个非常表现力的逻辑框架，与大多数框架不同，例如爱丁堡逻辑框架（LF），允许在扣除范围内代表计算。但是，与LF编码不同，迄今为止提出的Dedukti编码还没有适当的定理 - 即编码系统中的术语和编码中的术语之间的培训。此外，其中许多也没有保守性结果，这损害了Dedukti检查在此类编码中编写的证明的能力。我们为Dedukti编码提供了另一种方法，该方法不仅允许更简单的保守性证明，还可以恢复编码的充分性。更确切地说，我们在这项工作中提出了足够（因此是保守的）编码功能性纯型系统。但是，与LF编码相反，我们的计算是计算，即直接代表计算作为计算。因此，我们的工作是第一个介绍并证明正确的方法，该方法允许在dedukti中既适当又计算的编码。
Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem -- i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity result, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with LF encodings, ours is computational -- that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti.
