μ冠頭形証明とそのプログラミングへの応用に関する一考察
スポンサーリンク
概要
- 論文の詳細を見る
古典命題論理のある特殊な形をした証明(μ冠頭形証明)の存在性の例外処理のプログラムへの応用について報告する.μ冠頭形証明は,シーケント計算LKにおける右減の規則の使われ方に関する考察から得られた概念である.任意の古典的命題論理の定理に対してこのμ冠頭形証明が存在することにより,シーケントの右側には高々2つの論理式の出現を許せば十分であることがわかった.カリー・ハーワードの同型により,このμ冠頭形証明に例外処理のプログラムとしての計算的意味が自然に割り当てられることを関数型言語MLでの例を用いて示す.
- 一般社団法人日本ソフトウェア科学会の論文
- 1997-03-17
著者
関連論文
- λμ計算のモデルについて
- 構成的プログラミング
- 古典的証明に基づく関数型言語の構築
- 古典的証明に基づく値呼びプログラミング言語の型推論アルゴリズムについて
- An Injective CPS-translation for the Extensional λ-calculus
- 安全な動的型と分散プロクラミング
- 部分型推論の困難さに関する一考察
- Domain-Free $\lambda\mu$-Calculus for Polymorphism and Call-by-Value (Languages, Algebra and Computer Systems)
- μ-Head Form Proofs with at Most Two Formulas in the Succedent
- μ冠頭形証明とそのプログラミングへの応用に関する一考察
- Martin-Lofの型理論に基づくプログラム支援システムの構築
- 類推における証明項の変換について
- Bengt Nordstrom, Kent Petersson and Jan M. Smith : Programming in Martin-Lof's Type Theory, An Introduction, Clarendon Press (1990). ISBN 0-19-853814-6
- Parallel Computation and Synchronized Term Rewriting Systems : Extended Abstract (Algebraic Semigroups, Formal Languages and Computation)
- $\gamma$-Calculus with Lazy Lists : Extended abstract (Algorithms in Algebraic Systems and Computation Theory)
- Multiple-Conclusion System as Communication Calculus : Informal meaning of proofs as communication terms (Algebraic Systems, Formal Languages and Computations)