论文标题
刺激二元性双重性
Gentzen-Mints-Zucker duality
论文作者
论文摘要
咖喱 - 咖喱的对应关系通常被描述为将证据（以直觉自然扣除）与程序（简单型lambda conculus中的术语）相关联。然而，由于切割的计算内容和lambda conculus的逻辑起源，这种叙述几乎不是一个完美的拟合。我们重新审视霍华德的工作，并将其解释为直觉序列中的一类证明与简单型lambda cyculus中的术语类别之间的同构。在我们讲述故事时，基本二元性不是在证明和程序之间，而是在局部（序列微积分）和全球（lambda conculus或自然扣除）观点之间的观点，这是关于常见逻辑计算的数学结构的观点。
The Curry-Howard correspondence is often described as relating proofs (in intutionistic natural deduction) to programs (terms in simply-typed lambda calculus). However this narrative is hardly a perfect fit, due to the computational content of cut-elimination and the logical origins of lambda calculus. We revisit Howard's work and interpret it as an isomorphism between a category of proofs in intuitionistic sequent calculus and a category of terms in simply-typed lambda calculus. In our telling of the story the fundamental duality is not between proofs and programs but between local (sequent calculus) and global (lambda calculus or natural deduction) points of view on a common logico-computational mathematical structure.
