• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

論理学のプログラム言語理論への応用

研究課題

研究課題/領域番号 05808030
研究種目

一般研究(C)

配分区分補助金
研究分野 計算機科学
研究機関慶応義塾大学

研究代表者

岡田 光弘  慶應義塾大学, 文学部, 助教授 (30224025)

研究期間 (年度) 1993 – 1994
研究課題ステータス 完了 (1994年度)
配分額 *注記
1,900千円 (直接経費: 1,900千円)
1994年度: 900千円 (直接経費: 900千円)
1993年度: 1,000千円 (直接経費: 1,000千円)
キーワードマルチ・パラダイム・プログラム言語 / タイプ理論 / 項書き換え論理 / 証明論 / 代数的仕様言語 / 証明の正規化定理 / π一計算 / 計算モデル / 項書き換えシステム / 高階等式言語 / 論理的プログラム言語 / プログラム検証
研究概要

本研究の目的は、論理学、特に論理学の一分野である証明論の手法を用いて、新しいマルチ・パラダイム・プログラム言語の計算モデルの理論を確立し、これに基づいて論理的マルチ・パラダイム・プログラム言語の設計を行うことにある。特に、証明論における証明の正規化概念が、論理的新世代プログラム言語(タイプ付関数型言語、論理言語、代数的仕様言語(項書換え言語))の計算概念と密接に関係していることに着目して、新しいマルチ・パラダイム・プログラム言語の計算理論を論理学における証明の正規化問題に還元して、新しい形の証明の正規化定理を与えることにより、新しいプログラム言語の計算モデルを確立する、という手法をとった。まず、強力なタイプ付関数型言語(MLやTheory of Constructions等)と項書き換えシステムに基づく代数的仕様言語(OBJ等)とを統合したマルチ・パラダイム言語の計算モデルを上の証明論的手法を用いて確立し、このマルチ・パラダイム言語がAbstract Data Type言語として非常に有用な性質を持つことを示した。又、我々が確立した計算モデルを基にして、このマルチ・パラダイム言語の実装を行い、PTA(Rewriting Technigues and Application)国際会議等の場でデモンストレーションを行なった。我々の確立したマルチ・パラダイム言語の計算モデルの理論をHuet-CoguentのTheory of CostructionsとGoguen等のOBJとの統合言語に適用することにより、OBJのフレームワークを用いてADTの代数的仕様を与え、Theory of Constructionsのタイプ推論を用いて、仕様の検証の証明を与えることができる。又上の言語は、Girardの線形論理をベースに置くことにより並行計算プログラム言語としての特徴も持つこととなる。特に、自己言及的述語を含む述語論理を線形論理上で与え(これをmobile linear logicと呼ぶ)ることにより、milnerのπ計算の表現力を持つ言語が確立さらた。

報告書

(2件)
  • 1994 研究成果報告書概要
  • 1993 実績報告書
  • 研究成果

    (22件)

すべて その他

すべて 文献書誌 (22件)

  • [文献書誌] Jouannaucl and岡田 光弘: "Abstract Data Type Systems" Theoretical Computer Sciense,special issue on Abstract Data Types. 近刊.

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 岡田 光弘: "線形論理に基づく並行計算モデル" 情報処理,並行計算特集号. 近刊.

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 岡田 光弘: "線形論理とその応用I,II,III,IV" ソフトウェア科学(日本ソフトウェア科学会誌). 近刊(計4号).

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 岡田 光弘: "A Note on the Strong Normalizability of self-referential Logic" Phylosophy(三田哲学会誌). 95. 1-14 (1993)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Gui and岡田 光弘: "LAMBDALG-Higher Order Algebraic Specification Language" Springer Lecture Notes in Computer Science. 690. 462-466 (1993)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 浜野-岡田: "A Direct Independence Proof of Buchholz′s Hydra Game" Archiev for Mathematical Logic. (近刊).

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 岡田 光弘: "ジラールの線形論理とその応用(日本ソフトウェア科学会チェ-トリアル・レクチャー・ノート" 日本ソフトウェア科学会, 42 (1993)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Jouannaud-Okada: "Abstract Data Type Systems, Theoretical Computer Science" Special Issue on Abstract Data Types (invited article). (to appear.).

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Hamano-Okada: "Gentzen's Proof Reduction, Kirby-Paris Hydra Game and Buchholz's Hydra Game" Proc.of Proof Theory Symposium, Mathematical Institute, Kyoto Univ. (to appear). (1995)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Hamano-Okada: "A Direct Independence Proof of Buhholz's Hydra Game" Archiev for Mathematical Logic. (to appear.).

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Okada: "Linear Logic I,II,III,IV (invited articles), in four successive issues of Journal of Software Science (in Japanese)" Software Science Society of Japan. (to appear.).

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Okada: "Concurrent Computation Models Based on Linear Logic" Journal of Information Processing Society of Japan. (to appear.). (1995)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Okada: "Proof Theory for Theoretical Computer Science (in Japanese)" Shokabo Publishing, Tokyo, in preparation. (This is a revised version of a lecture note under the same title, distributed in L.R.I., Univ.Paris-XI,1988.).

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Okada: "A Note on the Strong Normalizability of the Self-Referential Logic" Philosophy 95 (1993), Mita Philosophical Society. 1-14

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Gui-Okada: "LAMBDALG-Higher Order Algebraic Specification Language" Proc.of Rewriting Techniques and Applications, Springer LNCS. LNCS 690.(1993)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Okada: ""Girard's Linear Logic and Applications (in Japanese, partly in English)"" a JSSS Tutorial Lecture Note (41 pages). Software Science Society of Japan.(1993)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Gui-Okada: "System Description of LAMBDALG (with Y.Gui)" Proc.of Logic Programming and Automated Reasoning, Springer LNCS. (1993)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 岡田光弘: "Note on the Strong Normalizability of the Logic with Self‐Referential Predicates" Philosophy95(1993)Mita Philosophi cal Soc.95. 1-14 (1993)

    • 関連する報告書
      1993 実績報告書
  • [文献書誌] 岡田光弘: "Lambdaly-Higher Order Algebraic Specification Langvages" Springer Lecture Notes(Proc.RTA93). (1993June). 712-715 (1993)

    • 関連する報告書
      1993 実績報告書
  • [文献書誌] 岡田光弘: "線形論理とその応用I,II,III,IV" 日本ソフトウエア科学会誌. 近刊. (1994)

    • 関連する報告書
      1993 実績報告書
  • [文献書誌] 岡田光弘(共著): "Longuage,Information and Computation" Thaehaksa Publishing Co.Seoul, 234 (1993)

    • 関連する報告書
      1993 実績報告書
  • [文献書誌] 岡田光弘: "Girardの線形論理,チュートリアル レイチャーノート" 日本ソフトウエア科学会, 43 (1993)

    • 関連する報告書
      1993 実績報告書

URL: 

公開日: 1993-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi