How to avoid the commuting conversions of IPC
CoRR(2024)
摘要
Since the observation in 2006 that it is possible to embed IPC into the
atomic polymorphic lambda-calculus (a predicative fragment of system F with
universal instantiations restricted to atomic formulas) different such
embeddings appeared in the literature. All of them comprise the Russell-Prawitz
translation of formulas, but have different strategies for the translation of
proofs. Although these embeddings preserve proof identity, all fail in
delivering preservation of reduction steps. In fact, they translate the
commuting conversions of IPC to beta-equality, or to other kinds of reduction
or equality generated by new principles added to system F. The cause for this
is the generation of redexes by the translation itself. In this paper, we
present an embedding of IPC into atomic system F, still based on the same
translation of formulas, but which maps commuting conversions to syntactic
identity, while simulating the other kinds of reduction steps present in IPC
betaη-reduction. In this sense the translation achieves a truly commuting
conversion-free image of IPC in atomic system F.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要