林晋（八杉晋）の経歴と研究業績 ver.2023.03.15

このページは、元京大文学研究科教授で京大名誉教授の歴史学者、林晋（本名は八杉晋、林は旧姓）の経歴と研究業績についての情報を提供するためのページです。林はプロの歴史学者ですが（定年退職しているので「でしたが」か？）、51歳で歴史学に転じるまでは、情報学者、数学者でした。

この様な林の経歴や研究業績に関する間違った情報が Wikipedia に掲載されてしまったことを受けて、それを誰かに修正してもらうために、このページを書きました。Wikipedia では、客観性のために自分に関する記事は自分では書いたり修正したりしないことになっているので、この Wikipedia記事を編集するのではなく、正しい情報を、このページに書いたのです。幸い非常に的確な修正をしていただけました。こちらが、そのWikipediaの記事です。

ただし、最初に間違えた Wikipedia の記事を書いてくださった方の名誉のために書いておきますが、このブログ投稿に書いたように、間違いは林の怠惰が原因で起たものです。

修正以前の古い記事の最大の問題点は、私が、情報学者、数学者、になっていたことです。本当は、すでに説明したように、歴史学者、情報学者、数学者、です。ただ、数学の様なことは、解説や一般向け講義は別として、この十数年まったくやっていません。情報の方は、共同研究者や競争資金の関係上、しばらくは情報学も続け、また、そういうのを止めた後も、史料研究用のソフトを作っていたので、いわゆる人文情報学、digital humanities の研究者と言えたので、情報学者と名のっても嘘にはならなかったでしょうが、ただ、定年退職してからも、続けるはずだったソフト開発はしなくなってしまいました。

私の経歴は、数学とITを中心にやっていた1972年から2005年の33年間の理系時代と、2005年に京大文学研究科（以下、京大文）に転職し2019年に定年退職するまでの、歴史学を中心にやっていた14年間の文系時代の二つに分かれます。理系時代の最後の方は、昼は工学部教授、夜は歴史家という生活でしたし、非常勤で歴史を教えたこともあります。また、京大文に転職した後も、暫くは理系時代にやっていたプロジェクトを継続していましたので、この二つの時代は綺麗に分かれてはいませんが、主な職場ということで言えば、2005年3月31日以前は理系、2005年4月1日以後は文系であったわけです。

そして、理系の学生・学者として過ごした年月は、文系の学者として過ごした年月よりずっと長いのですが、私自身は経歴の本体は、文系時代で、それ以前の理系時代は、文系時代に必要となった知識や能力を養い、また、研究テーマを用意するための、助走期間・準備期間だったと考えています。その文系時代に何をやっていたかというと、主には、このサイト shayashiyasugi.com で公開しようとしている論理学者クルト・ゲーデルの歴史観に端を発する歴史研究「ゲーデルと数学の近代」でした。

文系時代に自分自身の興味から行った研究は、すべてこの「ゲーデルと数学の近代」が発端になっています。例えば、ゲーデルや数学の近代化とは何の関係も無いようにみえる京都学派研究でさえ、「ゲーデルと数学の近代」の一環のヒルベルト数学ノート研究に端を発しています。ただ、二つの間にSMART-GSというヒルベルトの数学日記研究のために作った手書き史料研究用のツールの開発が挟まっているために、その関係が外からは見えないのです。その関係にご興味がある方は、2021年の西田田辺記念講演を参照してください。そして、結果としては、この京都学派研究を通して西谷啓治のニヒリズム論という、「ゲーデルと数学の近代」の重要な部品を知ることができたのでした。

また、学者は社会に対する貢献もしないといけないと考えていましたので、最初は自分が使うだけのために作ったSMART-GSを公開して開発を続けたり、京都学派研究の際には京都学派アーカイブを作成したりしました。また、その様な社会貢献のための研究では、「ゲーデルと数学の近代」が発端ではない研究も行っています。渕一博さんと第5世代コンピュータプロジェクトの歴史（1,2,3)、経産省のシンクタンクRIETIでのAIの社会影響の研究や文部科学省の政策研究を担うNISTEPにおけるIT政策に関する研究(1,2,3,4)と、それから派生したエッセイや講演などがそれです。ただ、これらも、結果としては、「ゲーデルと数学の近代」の重要な部品である Max Weber 系の近代化論と深く関係することになりました。少なくとも、「ゲーデルと数学の近代」の大変重要な部品である「近代化論」の私なりの理解が、これらの研究の背景になっています。

この様に、京大文に転職して以後、ほぼすべて「ゲーデルと数学の近代」の研究を中心にまわっていた、私の経歴・業績が誤解されてしまった最大の理由は、「ゲーデルと数学の近代」の研究が、現在のところ、その「部品」しか発表できてないことです。このページに書きましたように、この研究は、歴史学（思想史、数学史、情報学史、哲学史）、社会学、哲学などの幾つかの異なる研究分野における複数の個別研究が有機的に組み合わさって、初めて成立するものです。その「複数の個別研究」を、それぞれの分野の研究として発表したもの、それが「部品」と呼んだものです。この様な次第で、京大文の時代に私が何をしていたのかは、shayashiyasugi.com が全く未完成である現在では説明するのは難しいのです。ただ、それを手短にまとめたものと、その一部分を話したものが、それぞれ、2021年の西田田辺記念講演と、2018年の応用哲学会のシンポジウムの報告としてあります。

このページの以下の部分では、この様な背景のもと、私の経歴と研究業績を説明するために学歴、職歴、文系の研究業績、理系の研究業績、の順に記述します。私の研究業績には、文系・理系のどちらに分類すべきかよく分からないものも多くありますが、一応、適当に判断して、どちらかに分類してあります。

記述の仕方は、文系と理系でかなり違っていて、理系の方は理系の標準に従い査読の有無などで分類していますが、査読というものがあまり意味を持たない、また、行わないことが多い文系の方の業績は、分類せずに時間順に並べています。また、文系の業績の方は、こちらのページに、それぞれの内容の説明を記述してありますので、それぞれのアイテムから、そちらへのリンクを張ってあり、それがどういう形で発表されたものなのか、また、その内容がどの様なものなのかがわかるようになっています。

学歴

職歴

文系の研究業績

主な著述物と依頼されて行った講演

  1. エッセイ「第五世代コンピュータープロジェクト－1980年代の日本」解説
  2. 講演「歴史学から見た京都学派―ある数理思想史家の観点」解説
  3. エッセイ「情報学者の人文学研究　その１と２」解説
  4. 講演「歴史学から見た京都学派－西田幾多郎と哲学の道－解説
  5. 講演「西田幾多郎新資料翻刻プロジェクトと京都学派アーカイブについて解説
  6. 講演「西田幾多郎　その人と思想　－京大時代を中心に―」解説
  7. 論文「西谷啓治と田辺元」解説
  8. 講演「種の論理と数理哲学－田辺元昭和9年講義メモからの新発見」解説
  9. 講演「人間　西田幾多郎」解説
  10. 講演 "How was Mathematics modernized?"解説
  11. 論文「AI と社会の未来 ―労働・グローバライゼーションの観点から―」解説
  12. 講演「西谷啓治と田辺元…空と種」解説
  13. 講演「失われた時のウェブを目指して」解説
  14. 講演「AIブームは本物か？ -米国の場合、日本の場合-」解説
  15. エッセイ「あるソフトウェア工学者の失敗 -日本のITは何故弱いか-」解説
  16. 講演「開かれた世界、開かれた心、開かれた社会」解説
  17. 論文「澤口昭聿・中沢新一の多様体哲学について　-田辺哲学テキスト生成研究の試み（二）-解説
  18. 講演「社会とソフトウェア：あるソフトウェア工学者の経験」解説
  19. 論文「田辺元の『数理哲学』」解説
  20. 講演「種の論理再考」解説
  21. 論文「「数理哲学」としての種の論理」解説
  22. エッセイ「情報技術の思想家　渕一博」解説
  23. レポート「日本の危機としてのIT人材問題」解説
  24. 講演「真のHilbert 像をもとめて-Hilbert 研究の現状-」解説
  25. 講演「渕一博の思想 ーなぜ論理だったのか？ー」解説
  26. 記事「ヒルベルトの数学手帳｣解説
  27. エッセイ「私は如何にして歴史家になったか」解説
  28. 岩波文庫 ゲーデル著「不完全性定理」、林・八杉訳解説 解説
  29. レポート「情報通信技術と「思想」 -科学技術の能力としての「思想」-」解説
  30. レポート「二つの合理性と日本のソフトウェア工学」解説

WEBサイト・デジタルアーカイブ・ソフトウェア

  1. 京都学派アーカイブ　解説
  2. 手書き史料翻刻・分析用ツール SMART-GS　解説
  3. サイト　"David Hilbert's Mathematical notebooks"　解説
  4. サイト「ゲーデルと数学基礎論の歴史」　解説

理系の研究業績

著書

  1. 「お話・数学基礎論」八杉満利子・林晋、平成1４年６月２０日, 講談社
  2. 「パラドックス！」林晋編著、平成12年8月, 日本評論社
  3. 「論理パズルとパズルの論理」, 八杉満利子・林晋, 平成10年9月, 遊星社
  4. プログラム検証論 , 平成7年9月, 共立出版
  5. コンピュータ基礎理論ハンドブック, 8章「プログラミング言語における型理論」担当, 平成6年, 丸善出版, 分担訳
  6. ゲーデルの謎を解く , 平成5年11月, 岩波書店
  7. 情報系の数学入門 , 平成5年9月, オーム社, 林晋・八杉満利子
  8. 構成的プログラミングの基礎, 平成3年4月, 遊星社, 林晋・小林聡
  9. 現代数理科学辞典, 平成3年3月, 大阪書籍, 分担執筆
  10. 続・新しいプログラミング・パラダイム, 平成2年11月, 共立出版, 分担執筆
  11. 数理論理学, 平成元年12月, コロナ社
  12. PX: A Computational Logic, S. Hayashi and H. Nakano，1988, The MIT Press, free PDF volume

学術論文（査読論文・招待論文）

  1. Stefano, Berardi , Thierry, Coquand , Susumu, Hayashi?: Games with 1-backtracking, Annals of Pure and Applied Logic, vol.161-10, July 2010, pp.1254-1269.
  2. 文献研究と情報技術 : 史学・古典学の現場から(<特集>歴史知識学) , 人工知能学会誌, 25(1), pp.24-31, 2010年1月.
  3. Hayashi, S.: Can proofs be animated by games?, Fundamenta Informaticae 77 (2007), pp.1-13, in print, exteded journal version of 33.
  4. Hayashi, S.:Mathematics based on Incremental Learning -Excluded middle and Inductive inference-, Theoretical Computer Science 350 (1), 2006, pp. 125-139, exteded journal version of 28.
  5. Stefano Berardi, Thierry Coquand, Susumu Hayashi: Games with 1-backtracking. GALOP 2005: 210-225
  6. Hayashi, S.: Can proofs be animated by gamess?, in P. Urzyczyn ed., TLCA 2005, LNCS 3461, pp.11-22, 2005, invited paper.
  7. Hayashi, S., Pan Y., Sato M., et al.: Test Driven Development of UML Models with SMART modeling system, in Baars et al. eds.,UML 2004, LNCS. 3273,pp. 395-409, 2004.
  8. Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. LICS 2004: 192-201
  9. Hayashi S.: Mathematics based on Learning, Algorithmic Learning Theory, Lecture Notes in Artificial Intelligence 2533, Springer, pp.7-21.
  10. Towards Limit Computable Mathematics, Susumu Hayashi and Masahiro Nakata: in Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 2000, Selected Paper, P. Challanghan, Z. Luo, J. McKinna, R. Pollack, eds., Springer Lecture Notes in Computer Science 2277, pp.125-144.
  11. A limiting first order realizability interpretation, Masahiro Nakata and Susumu Hayashi: Scientificae Mathematicae Japonicae http://www.jams.or.jp/scmjol/5.html, paper number 5-49: dvi, ps, pdf, 2001
  12. Hayashi S., Sumitomo R., and Shii K.:Towards Animation of Proofs -testing proofs by examples-:, Theoretical Computer Science, 272, pp.177--195, 2002
  13. 証明アニメーション支援環境の構築、コンピュータソフトウェア、Vol.16, No.3 (1999), pp.71-74, 住友亮翼, 林晋
  14. Susumu Hayashi, Ryosuke Sumitomo; Testing Proofs by Examples, in Advances in Computing Science, Asian '98 : 4th Asian Computing Science Conference, Manila, the Philippines, December 1998, J. Xiang and Ohori, eds., Lecture notes in Computer Science No. 1538, pp.1-3, 1998.
  15. "山口昌哉「複雑系科学の哲学に不足しているもの」"に対するコメント、日本ファジイ学会誌, 9(5), 611-613, 1997.
  16. Constructive programming - a personal view -, in Combinatorics, Complexity, Logic, Proceedings of DMTCS'96, Springer-Verlag, Singapore, 1996, pp.38-51, D. S. Bridges, C. Calude, J. Gibbons, S. Reeves, I. Witten (eds.)
  17. Two extensions of PX system (extended abstract), in Linear Logic 96 Tokyo Meeting, Keio University, Tokyo, 1996, in Electronic Notes of Theoretical Computer Science, Vol. 3, http://www.elsevier.nl/mcs/tcs/pc/Menu.html, Elsevier-Science Publishing, S. Hayashi, M. Ishikawa, S. Kobayashi, H. Nakano, S. Nakazaki
  18. A New Formalization of Feferman's System of Functions and Classes and its Relation to Frege Structure , International Journal of Foundations of Computer Science, Vol. 6, No. 3, 1995, pp. 187-202, S. Hayashi and S. Kobayashi
    19. 科学基礎論研究 Vol. 22， No. 1，1994，pp. 1-6
  19. 変貌する数学観 -そのとき形式化は？-：
  20. Logic of refinement types, 1994, Proceedings of Esprit Basic Research Action, Types for Proofs and Programs workshop, Nijmegen, The Netherlands,Lecture Notes in Computer Science, Springer, vol. 806
  21. Interpretations of transfinite recursion and parametric abstraction in type, 1994, in Words, Languages and Combinatorics II, M. Ito and H. Jurgensen, eds. World Scientific Publish. Co., Singapore, pp. 452-464, M. Yasugi and S. Hayashi
  22. Singleton, Union, and Intersection Types for Program Extraction, , 1994, Information and Computation, vol. 109, pp. 174-210
  23. A functional system with transfinitely defined types, 1994, Festschrift for Prof. S. Takasu (N. Jones, M. Hagiya and M. Sato eds. Lecture Notes in Computer Science, Springer, vol. 792, pp. 31-60, M. Yasugi and S. Hayashi
  24. Lifschit'z Logic of Calculable Numbers and Optimizations in Program Extraction , 1994, Festschrift for Prof. S. Takasu (N. Jones, M. Hagiya and M. Sato eds.), Lecture Notes in Computer Science, Springer, vol. 792, pp. 1-9, S. Hayashi and Y. Takayama
  25. Constructive Mathematics and Computer-Aided Reasoning Systems , 1990, MATHEMATICAL LOGIC, P.P. Petkov ed., Plenum Press, pp.43-52
  26. An introduction to PX, 1990, Logical Foundations of Functional Programming, G. Huet ed., Addison-Wesley, pp. 432-486.
  27. Category theory for algebraic specifications, 1988, vol. 1, Advances in Software Science and Technology, pp. 169-185.
  28. PX: a system extracting programs from proofs, 1987, Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts, M. Wirsing ed., North-Holland, 3, pp. 99-124
  29. Adjunction of semifunctors: categorical structures in non-extensional lambda calculus, 1985, Theoretical Computer Sciences,41, pp.95-104
  30. Self-similar sets as Tarski's fixed points, 1985, Publications of the Research Institute for Mathematical Sciences, Kyoto University, 21, pp.1059-1066
  31. 代数仕様とカテゴリー, 1985, コンピュータ・ソフトウェア, vol. 2 pp.30-40
  32. Extracting Lisp programs from constructive proofs: a formal theory of constructive mathematics based on Lisp, 1983, Publications of the Research Institute for Mathematical Sciences, Kyoto University, vol. 19, pp.169-191
  33. A note on the bar induction rule, 1982, The L.E.J. Brouwer Centenary Symposium, North-Holland, Troelstra, A.S., van Dalen, D. (eds.), pp.149-163
  34. On set theories in toposes, 1981, Logic Symposia, Hakone 1979 -1980, Springer Lecture Notes in Math. 891, Springer-Verlag, Muller, G.H., Takeuti, G., Tugue, T. (eds), pp.23-29
  35. Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice, 1980, Annals of Mathematical Logic, 19, pp.33-65
  36. Existence property by means of a normalization method, 1978, Commentariorum Mathematicorum Universitatis Sancti Pauli, XXVII, pp.97-100.
  37. A note on provable well-orderings in first order systems with infinitary inference rules, 1977,Tsukuba Journal of Mathematics, vol.1, pp.125-135
  38. On derived rules of intuitionistic second order arithmetic 1977，Commentariorum Mathematicorum Universitatis Sancti Pauli, XXVI, pp.77-103

解説記事・エッセイなど（商業誌掲載分）

  1. 証明とプログラム： 数理科学，特集「応用論理」
  2. 構成的プログラミング： 平成元年, bit, 2月号
  3. 対角線論法とフラクタル： 平成元年, Computer Today, 8月号，特集「これがフラクタルだ」
  4. 計算機と無限： 平成2年, 数学セミナー, 8月号
  5. 証明は死んだ： 平成5年1, 日経サイエンス , 12月号, 共訳 (林・山岸・松木平)
  6. 計算機科学のすすめ：数学セミナー
  7. プリズム通り：三村昌泰，林晋らによるリレー連載，数学セミナー
  8. パズルの論理学： 平成7年, 数理科学, 特集「論理学のおもしろさ」
  9. 圏のファンクション： 平成8年, 数学セミナー 6月号
  10. 数学基礎論三つの神話： 平成11年, 数学セミナー 6月号
  11. 公理主義って知っていますか？: 平成１１年，数学セミナー??月号, pp.??-??
  12. 世界をまるごと理解できるだろうか、AERA Mook、「数学がわかる」、pp.30-33, 2000年
  13. モジュール化と科学、岩波書店雑誌「科学」2001年6月号, 特集2あなたが考える科学とは第２回、pp.800-801

主な招待講演等

国際会議・国際ワークショップ（国内含む）

  1. SMART-GS Project: a tool searching, marking up and linking historical documents, 科研費特定領域研究「日本の技術革新?経験蓄積と知識基盤化?」、第3回国際シンポジウム、2007年12月14-15日、東京、第１セッション講演とパネル。
  2. Proof Animation, Limit Computable Mathematics, and Hilbert’s　finite basis theoremMax-Planck-Institut fuer Mathematik, Bonn Conference “Methods of proof theory in mathematics” Hoersaal MPIM, June 2007, 3-10, a talk in an invitation-only conference.
  3. S. Hayashi, Can proofs be animated by proofs?, TLCA 05, Nara, Japan, April, 2005.
  4. S. Hayashi, Mathematics based on Learning, (Algorithmic Learning Theory 2002), Lubeck, Germany.
  5. S. Hayashi and Y. Akama, Limit-Computable Mathematics and its Applications, CSL'02 (Computer Science Logic 2002), Edinburgh, UK.
  6. Limit Computable Mathematics and Interactive Computation, The International Workshop on Rewriting in Proof and Computation (RPC'01), October 25-27, 2001, Itutsubashi-kaikan, Sendai, organized by Research Institute of Electrical Communication Tohoku University.
  7. S. Hayashi and K. Nakatogawa, Hilbert and Computation, Hilbert Workshop, Jan. 12, 2002, Keio University, Tokyo, organized by Dept. of Philosophy, Keio University, sponsored by Philosophy of Science Society, Japan, and Mita Philosophy Society.
  8. Limit Computable Mathematics and Proof Animation, TYPES 2000.
  9. Testing Proofs by Examples, Asian Computing Science Conference '98, Dec. 8-10, 1998, Manila, Philipin, published version.
  10. A series of invited lectures at MSJ Regional Workshop: Theories of Types and Proofs (TTP-Tokyo), Sept. 8-18, 1997,Tokyo Institute of Technology, Tokyo, Japan:
  11. Constructive programming - a personal view -, DMTCS'96, published version
  12. Two Extensions of PX system: 1996, Linear Logic 96, Tokyo Meeting, published version
  13. Feferman's theory and Frege Structure: 1993, The 5th Asian Logic Conference, Singapore, published version
  14. Representing logic in ATTT: Esprit Basic Research Action, Types for Proofs and Programs workshop, 1993, Nijmegen, The Netherlands, published version.
  15. Singleton, Union and Intersection Types for Program Extraction : 1991, Theoretical Aspects of Computer Science '91, Sendai, Japan, published version
  16. ATT: an optimized Curry-Howard isomorphism: 1989, Esprit Basic Research Action, The first Logical Framework Meeting, Sophia-Antipolis, France
  17. Kreisel-Troelstra realizability interpretation and program extraction: 1988, Workshop on Programming Logic, Bastad, Sweden, publisehd version.
  18. Constructive Mathematics and Computer-Aided Reasoning Systems: 1988, Heyting '88, Chaika, Bulgaria, published version
  19. An Introduction to PX: Institute of Logical Foundations of Functional Programming, 1987, Year of Programming, Texas University, Austin, published version.

国内会議・ワークショップなど

  1. ヒルベルトと２０世紀数学：平成11年3月29日、日本数学会、企画特別講演、早稲田大学
  2. 変貌する数学観 -そのとき形式化は？-： 平成6年6月， 日本学術会議科学基礎論研究連絡委員会主催， 科学基礎論学会共催, 前原昭二記念シンポジウム「形式化について」， published version
  3. 数学は完璧か？： 平成6年, 日本数学会, 平成６年度年会市民講座
  4. 証明工学： 平成5年, 日本応用数理学会, 平成５年度年会特別講演
  5. 論理学と計算機科学：平成2年，日本数学会，平成２年度総会数学基礎論分科会
  6. 計算機科学のための数理論理学： 平成2年， ソフトウェア科学会年会チュートリアル
  7. 構成的数学の諸相：1981，昭和５６年度総会数学基礎論分科会特別講演