計算に潜む数理，計算としての数理 --- 証明はプログラミング！
日時：3月17日（火曜日）13:00-15:30
会場：第5イベント会場（吉田南総合館 2F 共北27）
【セッション概要】「計算」とはいったい何だろう？「プログラム」とはいったい何だろう？驚くべきことに，情報科学に携わるものが日常的に触れているであろうプログラミングという行為は，数学基礎論と深く結びついている．また，その結びつきは，数学者が「正しい」証明を書くことおよび，「正しい」プログラムの作成，そして高信頼ソフトウェア開発に応用されている．本イベントでは，計算の背後に潜む数理についての概説を述べ，その後，プログラミングと証明との対応関係について解説する，最後に，こうした対応関係が実際に高信頼ソフトウェアの開発に結びつくことを定理証明支援系Coqを用いて実演する．
| 司会：松田 一孝 （東京大学 大学院情報理工学系研究科 助教） |
 | 【略歴】2004年東京大学工学部計数工学科卒業．2009年東京大学大学院情報理工学系研究科数理情報学専攻博士課程修了．2008年より2年間日本学術振興会特別研究員．2010年より2年間東北大学大学院情報科学研究科助教．2012年より東京大学大学院情報理工学系研究科コンピュータ科学専攻助教．博士（情報理工学）．プログラミング言語理論，関数プログラミング，プログラム変換等に興味を持つ． |
| 13:00-13:50 講演（1） 決定問題の相転移について |
| 田中 一之 （東北大学 大学院理学研究科 教授） |
| 【講演概要】1920年代にヒルベルト学派が数理論理学の中心テーマとして掲げた「決定問題」は，狭義には1階論理における真偽を判定する手続きを求める問題である．これはゲーデルやチューリングによってすぐに否定的に解かれたが，その後も様々な角度から類似の問題が提起され，肯定的にも否定的にも豊富な結果と解決手法が生れた．肯定的な手法としては，オートマトンの強化がしばしば有効であるが，それをさらに非決定性にすると顕著に決定不能な結果が得られることがある．たとえば，決定性ω文脈自由言語のゲームは（計算的に）決定可能だが，非決定性の場合は通常の集合論で決定できない．本講演では，決定問題の大きな流れを振り返りつつ，決定可能性と不可能性の相転移現象についていくつかの例をもとに考察する．文献：田中一之『チューリングとメタパズル』東京大学出版会2013．田中一之『無限ゲームとオートマトン』数学セミナー2014年11月号． |
 | 【略歴】1978年東京工業大学卒．1980年同大学修士課程修了．1986年カリフォルニア大学バークレー校Ph.D.．1986年東京工業大学助手，1991年東北大学助教授，1997年より現職．科学基礎論学会理事．Association for Symbolic Logic 評議員．Annals of Pure and Applied Logic 編集委員．専門は数学基礎論． |
| |
| 13:50-14:40 講演（2） 計算と論理 |
| 佐藤 雅彦 （京都大学 名誉教授） |
| 【講演概要】プログラミングという行為の背景にある計算と論理について解説する．特に，「プログラム」，「計算」，「論理」という3つの概念に共通するキーワードである 「証明」に焦点を合せて，これら3概念の共通点，相異点を明きらかにし，プログラミングという行為の本質に迫ることを目標とする．直観主義的型理論において発見された「カリー・ハワード同型対応」は，命題と型の同型性に基づき，（命題の）「証明」と（型の要素としての）「プログラム」 を同一視するという「証明」の見方を与えた．これは確かに有力な「ものの見方」であり，型を持つプログラミング言語や型理論に基づく Coq 等の証明支援系の理論的基盤を与えている．本講演では，このような「カリー・ハワード同型対応」によるプログラム観を紹介し，その有用性と同時にそれが抱える問題点を指摘する．上の型理論的証明観の問題点を理解するために，型理論誕生の動機となった18世紀末から19世紀初頭にかけての，「数学の危機」とよばれた数学の基礎付けをめぐる問題とその解決策が何であったかを説明する．これにより型理論を絶対視することなく，より広い観点からプログラミングという行為の本質に迫りたい． |
 | 【略歴】1971年東京大学理学部数学科を卒業後，同大学大学院理学系研究科修士課程数学専攻を経て，京都大学大学院理学研究科博士課程数学専攻に進学し，1974年京都大学数理解析研究所助手に採用された．1977年東京大学教養学部数学教室助教授に昇任，1979年東京大学理学部情報科学科助教授を経て1986年東北大学電気通信研究所教授に就任し，1995年京都大学大学院工学研究科教授となった．1998年に新設された大学院情報学研究科に配置換，知能情報学専攻ソフトウェア基礎論分野担任となり，2012年定年退職した．この間およびその後も一貫して証明とは何かについて考えている． |
| |
| 14:40-15:30 講演（3） 定理証明支援系Coqによる形式検証 |
| AFFELDT Reynald （産業技術総合研究所 セキュアシステム研究部門・高信頼ソフトウェア研究グループ 主任研究員） |
| 【講演概要】ソフトウェアや数学の証明に誤りのないことを保証するのは重要な研究課題である．1970年代からカリー＝ハワード同型対応に基づく形式体系の研究が継続的に行われてきた．その形式体系が定理証明支援系という形式検証ツールとして実現された結果，厳密で現実的な形式検証が可能となった．例えば，クリティカルな基盤ソフトウェア（コンパイラやオペレーティングシステム等）と大規模な数学の証明（四色定理やケプラー予想等）の形式検証が近年相次いで成功し，IT業界でも形式検証はスマートカードの厳密な安全性評価に応用されている．本発表では，ソフトウェアと数学の形式検証の実例を通じて，定理証明支援系による形式検証の基本を説明する．特に，ACMによる受賞を契機に注目を集めているフランス国立情報学自動制御研究所（INRIA）で開発されているCoqという定理証明支援系を紹介する． |
 | 【略歴】2004年東京大学大学院情報理工科学研究科・コンピュータ科学専攻博士課程修了．現在，産業技術総合研究所・セキュアシステム研究部門・高信頼ソフトウェア研究グループ主任研究員．定理証明支援系Coqを用いて，安全なソフトウェアの構築方法を研究している．暗号スキームやセキュリティプロトコルや情報・符号理論への応用を目標として，アセンブリやC言語などの低レベルのプログラムの形式検証とセキュリティ用の数学の形式化を研究している． |
| |
