部分構造論理の研究

研究課題番号 10640103
平成10年度 - 平成11年度科学研究費補助金 (基盤研究(C)(2)) 研究成果報告書
平成12年4月
研究代表者古森雄一(千葉大学理学部教授)
報告書類の dvi, TeX ファイルなど

はしがき

本研究は, 「部分構造論理の研究」の表題のもとに, 平成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 メカニズムとの関連など)を明らかにすることは非常に興味深い残された研究課題である。

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 (an extended abstract is here)
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, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki and Tetsuo Tamai, Formalization of Graph Search Algorithms and Its Applications, Theorem Proving in Higher Order Logics, LNCS 1479, Camberra 1998, 479-496
山本光晴, 萩谷昌己, 帰納的定義の発展, 日本ソフトウェア科学会第15回大会論文集, 電気通信大学 1998, 405-408
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), Amsterdam University Press, 1999
Sachio Hirokawa, Infiniteness of proof(alpha) is polynomial-space complete, Theoretical Computer Science, Vol. 206, 331-339, 1998
佐塚秀人, 長野大介, 廣川佐千男, 証明とモデルを生成するインターネットプルーバー, 九州大学大型計算機センター計算機科学研究報告 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 $\lambda\mu$-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 $\lambda\mu$-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 $\lambda 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
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
杉山健一 Siegel-Shintani-Borcherds $\Theta$ 関数について

(2)口頭発表

古森雄一, A Natural Deduction for Classical Logic, in which there exists a proof with the Subformula Property, MLG 研究集会(越後湯沢), 2000年1月10日LaTeX file
桜井貴文, Semantics and Cut-free Provability of Modal Substructural Logics, MLG 研究集会(越後湯沢), 2000年1月11日
山本光晴, On Formal Verification of Graph Search Algorithms and Its Application to Model Checking, Workshop on Refinement and Abstraction, 1999年11月16日
金沢誠, 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日
藤田憲悦: 2階古典論理に基づく多相型値呼び言語のCPS変換について, 日本ソフトウェア科学会第15回大会, 電気通信大学, pp.85-88, 1998年9月8日～11日
藤田憲悦: 2nd Order Lambda-Mu-Calculus of Call-by-Value, 第15回記号論理と情報科学研究集会(SLACA '98), 東北大学, 1998年10月14日～16日
藤田憲悦: 古典論理の証明を表現するある木構造について, 数理論理学研究集会(MLG), 静岡大学, 1998年11月26日～28日
野島歓之, 平田耕一, 藤田憲悦: 古典的証明に基づく関数型言語の構築, 電子情報通信学会研究会, 信学技報COMP98-51, pp.1-8, 1998年11月, 九州工大
藤田憲悦: {計算体系としての2階古典論理, 言語, 代数および計算機システム, 京都大学数理解析研究所, 1999年3月8日～10日
野島歓之, 平田耕一, 藤田憲悦: 古典論理に基づく関数型言語の構築, 情報処理学会九州支部研究会, pp.333-340, 1999年3月16日, 九州工大
Kensuke Baba, Sachio Hirokawa, Ken-etsu Fujita: Parallel Reduction in Type Free $\lambda\mu$-Calculus, 14th Term Rewriting Meeting, Nara Institute of Science and Technology, March 15-16, 1999
藤田憲悦: 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), pp. 1-11, Osaka University, August 3-4, 1999
藤田憲悦: 部分型推論の困難さに関する一考察, 日本ソフトウェア科学会第16回大会, 1999年9月19日～22日, 和歌山大学
藤田憲悦: Partially typed terms between Church-style and Curry-style, 第16回記号論理と情報科学研究集会(SLACA '99), 東北大学, 1999年10月26日～28日
藤田憲悦: Ground TRS, Simple Instances of 2nd-Order Unification, and Synchronization, 第15回項書換え系研究集会(TRS meeting), 1999年11月4日-6日, 湯布院
藤田憲悦: Multiple-Conclusion System as Communication Calculus, 証明論研究集会-証明論とその周辺-2000年1月18-20日, 東京大学
藤田憲悦, Multiple-conclusion system as communication calculus, Computing: the Australasian Theory Symposium (CATS 2000), 2000年2月1日
藤田憲悦, 小原誠一: 分散プログラミングのための安全な動的型, 情報処理学会九州支部研究会 3C-5, pp. 362-369, 2000年3月20日, 熊本大学
藤田憲悦: Multiple-Conclusion System as Communication Calculus (extended version), 「代数系, 形式言語および計算理論」研究集会, 数理解析研究所共同研究集会, 2000年3月21-23日, 京都大学
杉山健一, 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	Sachio Hirokawa, Yuichi Komori et al.	11
A Natural Deduction for Classical Logic, in which there exists a proof with the Subformula Property	Yuichi Komori	25
Lambek Calculus: Recognizing Power and Complexity	Makoto Kanazawa	29
Infiniteness of Proof($\alpha$) is Polynomial-Space Complete	Sachio Hirokawa	43
GUI for Geometric Inference Engine on Internet	Sachio Hirokawa et al.	53
A Binary-Conclusion Natural Deduction System	Ken-etsu Fujita	55
Multiple-Conclusion System as Communication Calculus	Ken-etsu Fujita	85

部 分 構 造 論 理 の 研 究

部分構造論理の研究