满射对终末型合流终末扩张型胆管结石
Confluent terminating extensional lambda-calculi with surjective pairing and terminal type
摘要：
对于具有满射对和终端类型的Adjuda演算，Curien和Di Cosmo受到Knuth-Benzen完备化的启发，引入了一个合流重写系统，该系统（1）扩展了朴素重写系统，（2）在上下文下是稳定的。重写系统具有（i）将终端类型的项重写为项常数 * 的规则，除非项不是 *，（ii）用于函数类型和产品类型的可拓性的重写规则，以及中介重写规则（i）和（ii）的重写规则。Curien和Di Cosmo假设，由于（iii），任何归约方法都不能证明Curien-Di Cosmo重写系统的强正规化（SN），并且他们将SN保持开放。通过将Girard的约化方法相对化到无 * 项上，证明了它们的重写的SN性和多态扩张的SN性。相对化之所以有效，是因为：对于任何SN项t，以及对于在$t$中未出现的终端类型的任何变量z，所有出现的终端类型的 * 被变量z替换的t是SN。
英文摘要：
For the lambda-calculus with surjective pairing and terminal type, Curien and Di Cosmo were inspired by Knuth-Bendix completion, and introduced a confluent rewriting system that (1) extends the naive rewriting system, and (2) is stable under contexts. The rewriting system has (i) a rule that rewrites term of a terminal type rewrites to a term constant *, unless the term is not *, (ii) rewrite rules for the extensionality of function types and product types, and rewrite rules mediating the rewrite rules (i) and (ii). Curien and Di Cosmo supposed that because of (iii), any reducibility method cannot prove the strong normalization (SN) of Curien-Di Cosmo's rewriting system, and they left the SN open. By relativizing Girard's reducibility method to the *-free terms, we prove SN of their rewriting, and SN of the extension by polymorphism. The relativization works because: for any SN term t, and for any variable z of terminal type not occurring in $t$, t with all the occurrences of * of terminal type replaced by the variable z is SN.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
