Call-by-name reduction and cut-elimination in classical logic

研究成果: Article査読

3 被引用数 (Scopus)

抄録

We present a version of Herbelin's over(λ, -) μ-calculus in the call-by-name setting to study the precise correspondence between normalization and cut-elimination in classical logic. Our translation of λ μ-terms into a set of terms in the calculus does not involve any administrative redexes, in particular η-expansion on μ-abstraction. The isomorphism preserves β, μ-reduction, which is simulated by a local-step cut-elimination procedure in the typed case, where the reduction system strictly follows the " cut=redex" paradigm. We show that the underlying untyped calculus is confluent and enjoys the PSN (preservation of strong normalization) property for the isomorphic image of λ μ-calculus, which in turn yields a confluent and strongly normalizing local-step cut-elimination procedure for classical logic.

本文言語English
ページ(範囲)38-65
ページ数28
ジャーナルAnnals of Pure and Applied Logic
153
1-3
DOI
出版ステータスPublished - 2008 4

ASJC Scopus subject areas

  • Logic

フィンガープリント 「Call-by-name reduction and cut-elimination in classical logic」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル