Event is FINISHED

マルレク・サブゼミ「型の理論入門」

Description
このセミナーは、機械自身に数学的・論理的推論を行わせようとする技術を紹介することを目的としています。本セミナーのもう一つの目的は、こうした技術を実現する上での「型の理論」の役割を説明することです。

数学的知識は前提としません。基本的には、数学とコンピュータの「歴史物語」として聞いてもらうので構いません。興味を持っていただければ、ご自身でいろいろ調べることができると思います。 

「機械に、数学的推論行わせる」技術は、現在なら、人工知能技術の一部と見なされると思いますが(確かに、その通りなのですが)、この技術の源流は、人工知能技術どころかコンピュータ自身が存在しなかった時代の1930年代に、数学の基礎の反省の中で生まれた「証明可能性=計算可能性」という認識に遡ることができます。

それから40年後の1970年の前後に、コンピュータの普及の中で新しい型の理論「Dependent Type Theory」と「カリー=ハワード対応」理論が登場します。その理論のポイントは、数学的命題は「型」を持ち、数学的証明は、その「型」の「要素」とみなせると言うことでした。この認識は、やがて、コンピュータのプログラム自身が、ある定理の証明に他ならないという認識を生み出します。

「機械による数学的推論は可能か?」という問いは、意外な、しかも身近なところに答えを見つけることになります。「コンピュータのプログラムが行なっていることは、数学的推論に他ならない」と。

本セミナーでは、この辺りを詳しく説明したいと思います。

それから40年たった2010年代、数学者Voevodskyは、新しい型の理論「Homotopy Type Theory」を用いて、現代数学全体をコンピュータ・プログラムの形で記述しようというプログラムを立ち上げます。

数学とコンピュータの間には、長くて深いつながりがあり、両者の「結節点」が、「型の理論」であることを、わかりやすく説明できたらと思います。
Updates
  • イベント詳細情報を更新しました。 Diff#457966 2019-07-29 03:52:55
Tue Sep 3, 2019
7:00 PM - 10:00 PM JST
Add to Calendar
Venue
Tickets
7/29 マルレク参加者 SOLD OUT ¥1,500
マルレク個人協賛会員 SOLD OUT ¥1,500
丸山レクチャーズ会員 SOLD OUT ¥1,500
一般 SOLD OUT ¥3,000
Venue Address
目黒区大橋2丁目22−42 地下1階 Japan
Organizer
マルレク
1,165 Followers