部分構造論理の研究

( 研究課題番号 10640103 )

平成 10 年度 ∼ 平成 11 年度科学研究費補助金 (基盤研究 (C)(2)) 研究成果報告書

平成 12 年 4 月

研究代表者古森雄一 ( 千葉大学理学部教授 )

はしがき

本研究は, 「部分構造論理の研究」の表題のもとに, 平成 10 年度から平成 11 年度にかけての二年間にわたり, 文部省科学研究費補助金の交付を受けて行われた。本研究の目的は, カテゴリー文法, relevant 論理, BCK 論理, 線形論理などの部分構造論理の性質を明らかにすることであった。この「はしがき」の末尾の「研究発表」にあるように, 研究分担者たちの活発な研究活動により, 部分構造論理の性質は明らかになりつつある。ここでは, 研究代表者の古森による２つの成果について述べる。

第一のものは P − W 問題のラムダ計算による解決である。これはもともと, 永山操の P −W 問題の Genzten 流体系による研究とほぼ同時期に, 廣川により始められたものである。永山の方法で 1993 年の夏に永山と古森は P − W 問題を解決するが, 廣川の方法では上手くいかなかった。古森は 1994 年 12 月 5 日の NSL’94 (Workshop on Non-standard Logic and Logical Aspects of Computer Science (金沢)) の講演で, 廣川の方法に永山の方法を取り入れれば容易にラムダ計算による解決が得られるとの見解を述べた。廣川はそれを実行したが, 古森が思っていたほど簡単ではなかった。しかし, 廣川は根気よく研究を続けラムダ計算による解決をほぼ達成した。最終的には, 永山が証明の吟味をして論文にまとめた。

第二のものは鹿島亮による古典論理の自然演繹の体系を古森が少し変えた体系についてのものである。この体系についての現在までの最もよい結果は, 鹿島による「与えられた任意の証明図を部分論理式特性をもつ証明図に変形することができる」というものである。唯一の結論を持つ古典論理の自然演繹の体系で正規形が部分論理式特性を持つというものは知られていなかったので, この結果はそのような最初の体系を示したことになる。しかし, この変形規則は Church-Rosser 性を持っていない。この体系の望ましい性質を保ったまま Church-Rosser 性を持つように変形規則を作り上げることと, その変形規則の計算規則としての意味 (Catch/Throw メカニズムとの関連など) を明らかにすることは非常に興味深い残された研究課題である。

なお, 本報告書の内容は全て http://www.math.s.chiba-u.ac.jp/˜ komori/kaken99/ で見ることができる。本報告書に収めることができなかった論文の幾つかも上記 URL (uniform resourse locator) から入手可能である。

2000 年 4 月 10 日古森雄一

研究組織

研究代表者古森雄一 (千葉大学理学部教授)
研究分担者中村吉邑 (千葉大学理学部教授)
研究分担者辻尚史  (千葉大学理学部教授)
研究分担者桜井貴文 (千葉大学理学部助教授)
研究分担者山本光晴 (千葉大学理学部助手)
研究分担者金沢誠  (千葉大学文学部助教授)
研究分担者廣川佐千男 (九州大学大型計算機センター教授)
研究分担者藤田憲悦 (九州工業大学情報工学部講師)
研究協力者杉山健一  (千葉大学理学部助教授)

研究経費

平成 10 年度  2,200 千円
平成 11 年度  1,600 千円
計  3,800 千円

研究発表

(1) 学会誌等

Sachio Hirokawa, Yuichi Komori and Misao Nagayama, A lambda proof of the P − W theorem, The Journal of Symbolic Logic ( to appear )

Masahiko Sato, Takafumi Sakurai, Rod Burstall, Explicit Environments, in Proceedings of Fourth International Conference on Typed Lambda Calculus and its Application (TLCA ’99), LNCS 1581, pp. 340 – 354, 1999

Takafumi Sakurai, Categorical Model Construction for Proving Syntactic Properties, International Journal of Foundations of Computer Science, to appear

Takafumi Sakurai, Categorical Model Construction for Proving Syntactic Properties, in Proceedings of Third Fuji International Symposium on Functional and Logic Programming (eds. M. Sato and Y. Toyama), World Scientific, pp. 187 – 206, 1998

Mitsuharu Yamamoto and Masami Hagiya, Evolution of Inductive Definitions, IWPSE99: International Workshop on Principles of Software Evolution, 17–21, 1999 山本光晴, 高橋孝一, 萩谷昌己, 西崎真也, 玉井哲雄, グラフ探索アルゴリズムの形式的検証とモデル検査への応用について, 数理解析研究所講究録 1125, 129–141, 2000

山本光晴, 高橋孝一, 萩谷昌己, モデル検査アルゴリズムの検証について, 日本ソフトウェア科学会第 16 回大会論文集, 1999

Makoto Kanazawa Lambek calculus: Recognizing power and complexity. In JFAK. Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday (Jelle Gerbrandy, Maarten Marx, Maarten de Rijke, and Yde Venema, editors), http://turing.wins.uva.nl/ j50/cdrom/ Amsterdam University Press, 1999

佐塚秀人, 長野大介, 廣川佐千男, 証明とモデルを生成するインターネットプルーバー, 九州大学大型計算機センター計算機科学研究報告 16, 1–6, 1999

Keiichi Mishima, Naoyuki Kato and Sachio Hirokawa, GUI for Geometric Inference Engine on Internet, Proceedings of Webnet’99, 1360–1361, 1999

K.Fujita, Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value, Lecture Notes in Computer Science (Springer) Vol.1581, pp.162–176, 1999, Typed Lambda Calculi and Applications (TLCA ’99)

K.Fujita, A Binary-Conclusion Natural Deduction System, Logic Journal of the Interest Group in Pure and Applied Logics (Oxford University Press), Vol. 7, No. 4, pp.517–545, 1999

K.Fujita, Domain-Free λμ-Calculus for Polymorphism and Call-by-Value, 京都大学数理解析研究所講究録 Vol.1106, pp.37–49, 1999

K.Fujita, Multiple-Conclusion System as Communication Calculus, Electronic Notes in Theoretical Computer Science (Elsevier Science), Vol. 31, No. 1, pp. 167–182, 2000, Computing: the Australasian Theory Symposium 2000

藤田憲悦, 部分型推論の困難さに関する一考察, コンピュータソフトウェア, Vol.17, No.2, 2000 (予定)

K.Fujita, On Proof Terms and Embeddings of Classical Substructural Logics, Studia Logica (Kluwer Academic), An International Journal for Symbolic Logic, Vol.61, No.2, pp.199-221, 1998

K.Fujita, Calculus of Classical Proofs II, Transactions of Information Processing Society of Japan (情報処理学会論文誌), Vol. 39, No.12, pp. 3269–3281, 1998

K.Fujita, Polymorphic Call-by-Value Calculus based on Classical Proofs, Lecture Notes in Artificial Intelligence (Springer) Vol.1476, pp.170-182, 1998, Artificial Intelligence and Symbolic Computation Theory, Implementations and Applications (AISC ’98)

K.Fujita, Type Inference for Domain-Free λ2, Technical Reports in Computer Science and Systems Engineering, CSSE–5, Kyushu Institute of Technology, July, 1999

K.Fujita, A sequent-conclusion natural deduction system with bounded length, Proceedings of The Third Symposium on Algebra, Languages and Computation – 1999 JAMS Annual Meeting – (Ed. Teruo Imaoka), 1–11, Osaka University, 1999

K.Fujita, Multiple-Conclusion System as Communication Calculus, Electronic Notes in Theoretical Computer Science (Elsevier Science), Vol. 31, No. 1, pp. 167–182, 2000, Computing: the Australasian Theory Symposium 2000 (* http://www.elsevier.nl/locate/entcs/volume31.html *)

K. Fujita and S. Obara, Safe Dynamics for Distributed Programming, Technical Reports in Computer Science and Systems Engineering CSSE–8, Kyushu Institute of Technology, March, 2000

藤田憲悦, 小原誠一, 分散プログラミングのための安全な動的型, 情報処理学会九州支部研究会 3C–5, 362–369, 2000

(2) 口頭発表

古森雄一, A Natural Deduction for Classical Logic, in which there exists a proof with the Subformula Property, MLG 研究集会 (越後湯沢), 2000 年 1 月 10 日

金沢誠, Developments in Learnability Theory, Third International Conference on Information-Theoretic Approaches to Logic, Language, and Computation. Hsi-Tou, Taiwan, 1998 年 6 月 16 日

金沢誠, Learning Categorial Grammars: Identification in the Limit and Parameter Setting, Logical Aspects of Computational Linguistics. Grenoble, France, 1998 年 12 月 15 日

金沢誠, Algorithmic Learning of Grammars and the Language Acquisition Device, 11th International Congress of Logic, Methodology and Philosophy of Science. Krakow, Poland, 1999 年 8 月 22 日

廣川佐千男, WWW 上の幾何推論システム, 人工知能学会人工知能基礎論研究会資料 SIG-FAI-9801, 1998 年 5 月 28 日

廣川佐千男, Classical Formulas as Types of Lambda-Nu-Calculus, Logic Colloquium’98, 1999 年 8 月 9 日

廣川佐千男, クリプケモデル生成と Java アプレットとしての実現第 13 回人工知能学会全国大会, 1999 年 6 月 16 日

廣川佐千男, 初等幾何推論の多面的表示方式, 第 13 回人工知能学会全国大会, 1999 年 6 月 16 日藤田憲悦, Multiple-conclusion system as communication calculus, Computing: the Australasian Theory Symposium (CATS 2000), 2000 年 2 月 1 日

杉山健一, On zeta functions of smooth manifolds and elliptic cohomology, 多変数解析セミナー, 1999 年 7 月

杉山健一, Hodge あるいは Tate 予想の成立する例の構成 (Heisenberg 代数の表現論の観点から), 金沢大学数学談話会, 2000 年 3 月

目次

モデル検査アルゴリズムの検証について  … 1

山本光晴他著

証明とモデルを生成するインターネットプルーバー  … 5

廣川佐千男他著

A lambda proof of the P − W theorem  … 11

Sachio Hirokawa, Yuichi Komori et al. A Natural Deduction for Classical Logic, in which there exists a proof

with the Subformula Property  … 25

Yuichi Komori

Lambek Calculus: Recognizing Power and Complexity  … 29

Makoto Kanazawa

Infiniteness of Proof(α) is Polynomial-Space Complete  ⋯ 43

Sachio Hirokawa

GUI for Geometric Inference Engine on Internet  … 53

Sachio Hirokawa et al.

A Binary-Conclusion Natural Deduction System  … 55

Ken-etsu Fujita

Multiple-Conclusion System as Communication Calculus  … 85

Ken-etsu Fujita