Agda中类型逻辑文法的形式化
Formalising Type-Logical Grammars in Agda
摘要：
近年来，使用证明助手来形式化和推理数学和程序设计语言的兴趣越来越大。类型逻辑语法与函数式编程中使用的类型论和系统密切相关，是下一个应用这种好奇心的完美候选者。使用证明助手的优点是，它们允许人们对自己的类型逻辑系统编写形式验证的证明，并且任何理论一旦实现，就可以立即计算。缺点是，在许多情况下，形式证明是作为事后的想法编写的，是不完整的，或者使用迟钝的语法。这使得验证过的证明往往比纸笔证明更难阅读，而且几乎从未直接发表过。在本文中，我们将尝试通过实例来弥补这一点。具体地说，我们使用Agda模型的Lambek-Grishin演算，语法逻辑与丰富的词汇表的类型形成的操作。然后，我们提出了一个验证的程序，在这个系统中的削减消除。然后，我们简要地概述了CPS的翻译证明在Lambek-Grishin演算程序在Agda。最后，我们将把我们的系统用于分析一个简单的例句。
英文摘要：
In recent years, the interest in using proof assistants to formalise and reason about mathematics and programming languages has grown. Type-logical grammars, being closely related to type theories and systems used in functional programming, are a perfect candidate to next apply this curiosity to. The advantages of using proof assistants is that they allow one to write formally verified proofs about one's type-logical systems, and that any theory, once implemented, can immediately be computed with. The downside is that in many cases the formal proofs are written as an afterthought, are incomplete, or use obtuse syntax. This makes it that the verified proofs are often much more difficult to read than the pen-and-paper proofs, and almost never directly published. In this paper, we will try to remedy that by example. Concretely, we use Agda to model the Lambek-Grishin calculus, a grammar logic with a rich vocabulary of type-forming operations. We then present a verified procedure for cut elimination in this system. Then we briefly outline a CPS translation from proofs in the Lambek-Grishin calculus to programs in Agda. And finally, we will put our system to use in the analysis of a simple example sentence.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
