線形論理に基づく計算モデルの理論概説
スポンサーリンク
概要
- 論文の詳細を見る
線形論理は1986年にJ-Y.Girardにより導入されて以来、並行性等の時間概念、計算資源の消費関係、計算環境の状態等の表現能力を内に含むまったく新しい論理体系として注目を集めており、今後計算機科学・情報科学の諸分野の論理的基礎を与えるものとして期待されている。本稿の目的は、線形論理を用いた計算モデルの概念の基本的な考え方を紹介することにある。一般的に言って論理的計算モデルの基本的パラダイムとしては、(1)証明探索(Proof-search)パラダイム、(2)証明簡約(Proof-reduction)パラダイム、(3)項書換え(Term-rewriting)パラダイムが重要である。例えば、プログラミング言語理論における例としては、(1)はプロローグ等の論理型プログラミング言語の計算モデルを、又(2)はLispやML等の関数型プログラミング言語の計算モデルを、又(3)はOBJ等の(実行可能)代数的仕様言語(等式型プログラミング言語)の計算モデルを各々与える。この基本的な三つの論理的計算モデルのパラダイムの構成において、これまでの伝統的論理体系(古典論理、ホーン節論理、直観主義論理、等式論理)のかわりに線形論理に基づく体系を用いると、並行計算や計算資源の消費等の線形論理の特徴的な表現力を備えた新しい計算モデルのパラダイムが構成されることになるわけである。以下において、線形論理に基づいて再構成された(1)(2)(3)の計算モデルの例を導入し、その基本的な考え方を示す。
- 1996-09-18
著者
-
岡田 光弘
慶應義塾大学文学部哲学専攻
-
岡田 光弘
慶雁義塾大学文学部哲学科
-
Okada Mitsuhiro
慶應義塾大学文学部
-
Okada Mitsuhiro
Department Of Philosphy Keio University
-
Okada Mitsuhiro
Department Of Philosophy Keio University
-
岡田 光弘
Department of Philosphy, Keio University
関連論文
- 現代応用オントロジーの哲学的・論理学的源泉(オントロジーの進化と普及(前編))
- 線形論理に基づく計算モデルの理論概説
- 線形論理に基づいたセキュリティ・プロトコルの論理的検証法(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- ウィトゲンシュタイン, 言語の限界, 飯田隆著, 講談社, 1997年.
- BAN論理からProtocol Composition Logicへ : セキュリティプロトコルの論理的検証法(数理的技法による情報セキュリティ)
- A Hierarchy of the Fragments of the System of Inductive Definition : Preliminary Report
- Semantic Characterizations for Reachability and Trace Equivalence in a Linear Logic-Based Process Calculus : Preliminary Report
- A Relationship among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game, and Buchholz's Hydra Game(Preliminary Report)(Mathematical Incompleteness in Arithmetic)
- 論理記号導入規則による論理的意味論について
- 矛盾は矛盾か (特集 ラッセルのパラドックス・100年)
- 歪んだ真珠(バロック) : 音楽における規則性VS反規則性,またはロゴスVSパトス
- オントロジー応用のための方法論の考察と展望(哲学とAIにおける対象世界モデリング)(〔第4回〕)
- 現代のフォーマルオントロジーの動向とオントロジー工学(「哲学とAIにおける対象世界モデリング」〔第3回〕)
- フッサールのフォーマルオントロジーとその影響(哲学とAIにおける対象世界モデリング〔第2回〕)
- オントロジーの哲学的・論理学的背景
- 「哲学とAIにおける対象世界モデリング」の企画にあたって
- 日本語の文末表現における意味解釈と音響特性
- フッサールの形式論理学分析における「多様体」概念の役割
- Characterization Theorems for Multiplicative Fragment of Intuitionistic Non-Commutative Linear Logic : Preliminary Report
- 3.線形論理に基づく並行計算モデル : 並行計算の論理的理解の試み (並行計算の理論の最近の動向)
- 倫理学入門のためのPersonal Guide
- デカルトにおける「論証」の概念と彼の形而上学的論証の論理的基準(100集記念号)
- A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic(Preliminary Report)(Non-Classical Logics and Their Kripke Semantics)
- 諸状況における終助詞「か」の意味解釈と音響特性
- 論理学入門のためのPersonal Guide
- 「普遍学」の夢と現実 : 論理推論体系の可能性を求めて(文学部創設百周年記念論文集I)
- フッサ-ル初期の「哲学的-数学的諸研究の終結テ-マ」とゲッチンゲン学派の論理哲学
- 論理的意味論と整合性証明
- Some Remarks on a Difference between Gentzen's Finitist and Heyting's Intuitionist Approaches toward Intuitionistic Logic and Arithmetic
- Completeness Proofs for Linear Logic Based on the Proof Search Method(Preliminary Report)(Type Theory and its Applications to Computer Systems)
- Note on the Strong Normalizability of the Logic with Self-Referential Predicates
- "The Concluding Theme of Philosophical-Mathematical Students" in the Early Husserl, and the Logical Philosophy of Goettingen School