2013年11月2日、科学基礎論学会 2013年度秋の研究例会 http://phsc.jp/conference.html のワークショップ「シミュレーション科学の哲学的基礎」に出席した。わたしは会員ではないのだが、当日の朝知って間に合うことに気づき聞きに行った。シミュレーションによる知識が人間の知識の中でどんな立場にあるのか考える必要があるとかねがね思っているからだ。わたしにとってはなじみのない概念が多かったので、必ずしもよくわからなかった。講演者の意図を正しく伝えていない心配があるが、わたしなりに受け止めたことを書きとめておく。
田名部 元成「シミュレーションのシステム哲学的基礎」
参加する人の間の相互作用を含むゲーミングシミュレーションなどを考えている。
「デザイン科学的研究」という研究パラダイムが有用だ。人工物の科学 (science of the artificial、「システムの科学」を書いたSimonが提唱)と関連する。ものを構築し、評価することによって学ぶ。問題意識から提案、開発、評価して問題意識にもどるサイクルを形成する。
デザイン科学は(Deweyなどの)プラグマティズムに近い。
哲学的枠組みとして「批判的実在論」を考える。Bhaskarという人の著作がある。Real, actual, empiricalというレベルを区別する。realなメカニズムによって、actualな事象が生じ、それが観察できる(empiricalな)ものごととして現われる。
モデルの正当化(validation)の話題の例に大気モデルが出てきた。この件は別記事にした。
出口 弘「シミュレーションのプラグマティクス 数理言語-自然言語-シミュレーション」
感染症などの問題についてagent-based model (ABM)によるシミュレーションをしている。
モデルの真偽値よりも、pragmaticsのほうが大事。Pragmaticsは言語学の「語用論」だが、ここでは「知識運用論」。【この話の意味はよくわからなかったが、モデルが現実世界を正確に表わしているかよりも、モデルが社会的意志決定の役にたつかのほうが大事という、(哲学の流派ではなくてことば本来の意味の) pragmatismだと感じた。】
社会のシミュレーションでは対象に意志決定主体を含む。目標は未来を正しく予測することではなく、可能なシナリオについて関係者が討議することを支援することである。
マクロな変数からなるモデルを作って、パラメータを較正すれば、現実に合うモデルは作れるが、そのパラメータが意志決定主体の働きかけの目標に使えるものでなければ、validでない。そこで、意志決定主体と似たagentが含まれるABMを考える。ABMは個々のagentについて予言するわけではなく、多数のagentからなる構造を表現する。ABMは時間については差分方程式の形をとるが、それは微分方程式の近似とは限らない。
ABMを使って学ぶ場とモデルの妥当性を問いなおす場の2つの討議空間が構成される。
菊池 誠「シミュレーションと高性能計算における論理と計算」
講演者は数理論理学者。(物理学者の菊池誠さんではない。)
証明とは、公理から出発し、推論規則を適用した「形式的証明」だと考えられることが多いが、実際の数学の証明は形式的証明ではない。
形式的証明は無矛盾性の証明が目的の場合にのみ有効な概念ではないか?
現実の証明は、推論よりもむしろ、理解や納得のわくぐみではないか?
将来の並列計算機では、同期をとらないので、計算の再現性がなくなるという話がある。これまでの計算の理論で考えられてきた計算とは違うが、新たな証明の概念のもとで正当化できるのではないか?
3講演のあとの討論は、菊池氏の証明に関する話題に集中した。
【わたしはむしろ、計算の理論を考える人が対象を再現性のある計算に限っていたことに驚いた。確かに、機械語のレベルで同じプログラムで、同期をとった計算であれば、再現性があるのがあたりまえなのかもしれない。しかし、Fortranで「実数型」(実際は浮動小数点数)の数値計算をしてきた者からみると、同じFortranソースプログラムでもコンパイラしだいで機械語が違ってくるのがあたりまえだ。とくに1980年代に発達したコンパイラの「最適化」機能を使うと、実数の演算の交換法則・結合法則などを使って同値なうちで計算ステップ数の少ないアルゴリズムが選ばれるが、実数演算で同値でも浮動小数点近似では厳密には同値でない。このことによる計算結果の不確定を、多くのFortranユーザーは、浮動小数点近似を使うことに伴う必然として受けいれてきたと思う。浮動小数点演算は、原理にさかのぼれば論理演算から構成されているにちがいないのだが、ながらく数理論理学者の視野にははいっていなかったのかもしれない。】
