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

1999 年度 研究成果報告書概要

算術と計算の論理構造に関する研究

研究課題

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

基盤研究(B)

配分区分補助金
応募区分一般
研究分野 数学一般(含確率論・統計数学)
研究機関東北大学

研究代表者

田中 一之  東北大学, 大学院・理学研究科, 教授 (70188291)

研究分担者 鹿島 亮  東京工業大学, 大学院・情報理工学研究科, 講師 (10240756)
寳来 正子 (高橋 正子)  東京工業大学, 大学院・情報理工学研究科, 教授 (00015588)
赤間 陽二  東北大学, 大学院・理学研究科, 助教授 (30272454)
長谷川 立  東京大学, 大学院・数理科学研究科, 助教授 (20243107)
龍田 眞  京都大学, 大学院・理学研究科, 助教授 (80216994)
研究期間 (年度) 1997 – 1999
キーワード論理構造 / 計算論 / 型理論 / 形式算術 / 2階算術 / 逆数学 / 限定算術 / ラムダ計算
研究概要

本研究の実施計画に従って,研究代表者と研究分担者は相互に緊密な連絡を取り合い,また研究集会での発表や討論を通して,算術と計算の論理構造に関する研究を行った.主な研究成果を研究者毎にまとめると、以下の通りである。
田中一之は,数学の定理を証明するのにどれくらい複雑な集合が必要かという問題(逆数学)を研究した.逆数学においてとくに重要とされる2階算術の体系WKL_0に対して,その可算モデルの性質を分析することで,山崎武らと共に新しいメタ定理を得た.赤間陽二は,計算の停止性の概念に興味を持ち,関数型言語から派生する値呼びλ計算,名前呼びλ計算,Turnerのλ計算などにおいて,停止性を持つ項の特徴づけを行った.また,組合せ論理に対する型理論を導入し,組合せ論理の停止性を持つ項を特徴づけた.宝来(高橋)正子は,高階論理体系と高階型理論の関係を研究した.また,自由構造上の計算可能性とλ表現可能性について考察した.安本雅洋は,限定算術(Bounded arithmetic)の超準モデルMのブール値拡大M^B,およびgeneric拡大M[G]の構造に関する研究を行った.龍田真は,D-正規証明の概念を提案し,この概念を用いて構成的命題論理における正規証明の唯一性に関して次の結果を示した.(1)βηD-正規証明は唯一である.(2)PNN条件を満たす論理式のβη-正規証明は唯一である.(3)BCK論理における極小論理式のβη-正規証明の唯一性の別証明を与える.長谷川立は,解析関手の理論計算機科学への応用を研究した.鹿島亮は,含意のみを論理記号とするrelevant logicの証明論および意味論の研究でいくつかの重要な成果を得た.

  • 研究成果

    (16件)

すべて その他

すべて 文献書誌 (16件)

  • [文献書誌] Y.Akama: "SN combinators and partial combinatory algebras"Lec.Notes in Comp.Science. 1379. 302-316 (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] R.Hasegawa: "An Analysis of divisibility orderings and reaursive path orderings"Lec.Notes in Comp.Science. 1345. 283-296 (1997)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] R.Kashima and N.Kamide: "Substructural implicational logics including the relevant logic E"Studia Logica. 63. 181-212 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.(Horai)Takahashi: "Lambda-representable functions over term algelras"Int.J.of Foundations of Comp.Sci.. (印刷中). (2000)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] K.Tanaka and T.Yamazaki: "A non-standard constrnetion of Haar measare and WKLO"Journal of Symbolic Logic. (印刷中). (2000)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.Tatsuta: "Realizability of monotone conductive definitions and its application to program synthesis"Lec.Notes in Comp.Science. 1422. 338-364 (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 田中一之(編): "数学の基礎をめぐる論争"シュプリンガー・フェアラーク東京. 224 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 森田康夫: "整数論"東京大学出版会. 284 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] Y. Akama: "SN combinators and partial combinatory algebras"Lecture Notes in Computer Science. 1379. 302-316 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] R. Hasegawa: "An analysis of divisibility orderings and recursive path orderings"Lecture Notes in Computer Science. 1345. 283-296 (1997)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] R. Kashima and N. Kamide: "Substructural implicational logics including the relevant logic E"Studia Logica. 63. 181-212 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] S. Hirokawa, Y. Komori and M. Nagayama: "A lambda proof of the P-W theorem"Journal of Symbolic Logic. (to appear).

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. (Horai) Takahashi: "Lambda-representable functions over term algebras"Int. J. of Foundations of Computer Science. (to appear).

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] K. Tanaka and T. Yamazaki: "A non-standard construction of Haar measure and WKLo"Journal of Symbolic Logic. (to appear).

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Tatsuta: "Realizability of monotone coinductive definitions and its application to program synthesis"Lecture Notes in Computer Science. 1422. 338-364 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] T. Yamazaki: "Some more conservation results on the Baire category theorem"Mathematical Logic Quarterly. 46. ((to appear)

    • 説明
      「研究成果報告書概要(欧文)」より

URL: 

公開日: 2001-10-23  

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

Powered by NII kakenhi