[logic-ml] 情報処理学会全国大会企画「計算に潜む数理，計算としての数理 --- 証明はプログラミング！」のご案内

[Kazutaka Matsuda]

logic-ml関係者の皆様，
東京大学の松田です．

複数受け取られた場合はご容赦ください．
この場をお借りして， 情報処理学会全国大会の企画の一つとして
3/17の13:00〜15:30より京都大学吉田キャンバス吉田南総合館 2F 共北26で開催される
「計算に潜む数理，計算としての数理 --- 証明はプログラミング！」
http://www.gakkai-web.net/gakkai/ipsj/77program/html/event/A-6.html
のご案内をさせていただきたく存じます．

情報処理学会全国大会は当日のご参加も受けつけており，
企画セッションのみの聴講は無料です．詳しくは以下をご欄下さい．
http://www.ipsj.or.jp/event/taikai/77/on_site_registration.html

本セッションでは，論理と計算に関する以下の3件の講演を企画しております．

# 田中一之 （東北大学 大学院理学研究科 教授）
 「決定問題の相転移について」

1920年代にヒルベルト学派が数理論理学の中心テーマとして掲げた「決
定問題」は，狭義には1階論理における真偽を判定する手続きを求める問
題である．これはゲーデルやチューリングによってすぐに否定的に解か
れたが，その後も様々な角度から類似の問題が提起され，肯定的にも否
定的にも豊富な結果と解決手法が生れた．肯定的な手法としては，オー
トマトンの強化がしばしば有効であるが，それをさらに非決定性にする
と顕著に決定不能な結果が得られることがある．たとえば，決定性ω文
脈自由言語のゲームは（計算的に）決定可能だが，非決定性の場合は通
常の集合論で決定できない．本講演では，決定問題の大きな流れを振り
返りつつ，決定可能性と不可能性の相転移現象についていくつかの例を
もとに考察する．

文献：田中一之『チューリングとメタパズル』東京大学出版会2013．田
中一之『無限ゲームとオートマトン』数学セミナー2014年11月号．


# 佐藤雅彦 （京都大学 名誉教授）
  「計算と論理」

プログラミングという行為の背景にある計算と論理について解説する．
特に，「プログラム」，「計算」，「論理」という3つの概念に共通する
キーワードである 「証明」に焦点を合せて，これら3概念の共通点，相
異点を明きらかにし，プログラミングという行為の本質に迫ることを目
標とする．直観主義的型理論において発見された「カリー・ハワード同
型対応」は，命題と型の同型性に基づき，（命題の）「証明」と（型の
要素としての）「プログラム」 を同一視するという「証明」の見方を与
えた．これは確かに有力な「ものの見方」であり，型を持つプログラミ
ング言語や型理論に基づく Coq 等の証明支援系の理論的基盤を与えてい
る．本講演では，このような「カリー・ハワード同型対応」によるプロ
グラム観を紹介し，その有用性と同時にそれが抱える問題点を指摘する．
上の型理論的証明観の問題点を理解するために，型理論誕生の動機となっ
た18世紀末から19世紀初頭にかけての，「数学の危機」とよばれた数学
の基礎付けをめぐる問題とその解決策が何であったかを説明する．これ
により型理論を絶対視することなく，より広い観点からプログラミング
という行為の本質に迫りたい．

# AFFELDT　Reynald （産業技術総合研究所 セキュアシステム研究部門・高信頼ソフトウェア研究グループ 主任研究員）
  「定理証明支援系Coqによる形式検証」

ソフトウェアや数学の証明に誤りのないことを保証するのは重要な研究
課題である．1970年代からカリー＝ハワード同型対応に基づく形式体系
の研究が継続的に行われてきた．その形式体系が定理証明支援系という
形式検証ツールとして実現された結果，厳密で現実的な形式検証が可能
となった．例えば，クリティカルな基盤ソフトウェア（コンパイラやオ
ペレーティングシステム等）と大規模な数学の証明（四色定理やケプラー
予想等）の形式検証が近年相次いで成功し，IT業界でも形式検証はスマー
トカードの厳密な安全性評価に応用されている．本発表では，ソフトウェ
アと数学の形式検証の実例を通じて，定理証明支援系による形式検証の
基本を説明する．特に，ACMによる受賞を契機に注目を集めているフラン
ス国立情報学自動制御研究所（INRIA）で開発されているCoqという定理
証明支援系を紹介する．

どうぞご参加を検討いただけますと幸いです．