Event is FINISHED

マルゼミ 「論理学入門 II -- ラムダ計算と関数型言語」

Description
今回のセミナーは、ネット配信で行います。
全国どこにいらしても、受講できます。

この告知ページに記載されている「開催場所・日時」は、リモート開催のセミナーを、収録・配信する「場所・日時」を指しています。
当初、Zoom, Youtube Liveでのリアルタイムでのネット配信も、選択肢として考えていたのですが、利用者の使いやすさ(自由に試聴時間を選べる。アプリのインストールと設定を必要としない)を考えて、収録翌日の27日から、専用のURLを皆様にお知らせして、編集済みのコンテンツをYoutubeで配信するする方式を選択しました。26日には何もありませんので、ご注意ください。

講演資料を公開しました。ご利用ください。https://www.marulabo.net/docs/logic2/
先に、Part I 「型のないラムダ計算」、Part II 「型付きラムダ計算」を公開しましたが、Part III「ラムダ計算とLISP, Haskell, OCaml」、Part IV「Coqでの関数型プログラミング」を追加公開しました。

-----------------------------------------------
前回の「論理学 I」との関係について


前回の「論理学 I — 命題論理の演繹ルール」では、「推論する能力」の最も基本的な基礎である、論理的推論ルールにフォーカスしました。今回の対象は、数学的推論の基礎で、前回のセミナーの内容を前提とはしていません。前回のセミナーを受講していない人も、独立の内容として理解できると思います。「論理学 I」と今回の「論理学 II」で別々に展開してきた、論理的推論と数学的推論の接点については、次回の「論理学 III -- 型の理論」で統一的に扱う予定ですので、ご期待ください。

型のないラムダ計算

今回のセミナーで最初に学ぶのは、1930年代にチャーチが定式化した、「型のないラムダ計算」です。
基本的には、「引数」に対して値を返すものとして「関数」を捉えて、関数で表された式に対する「代入」と式の「変形」を、少し、抽象的に捉えたものです。見かけは単純ですが、強力な計算能力を持ちます。

型付きラムダ計算

今回のセミナーで二つ目に学ぶのは、同じくチャーチが1940年代に開発した、「型付きラムダ計算」のシステムです。
「型のないラムダ計算」を基礎としながら、AからBへの関数に、"A -> B" という「型」を与えるのが、大きな特徴です。
このシステムは、関数型言語の基礎になります。

関数型言語

今回のセミナーでは、こうした関数の「型」が、関数型言語でどのように利用されているのかを、みていきたいと思います。
Coqも関数型言語としての顔を持ちます。今回のセミナーでは、関数型言語としてのCoqのプログラミングについていくつかの例を紹介しようと思います。

なぜ、関数型言語を学ぶのか?

現在、多くのプログラマーがよく知っているのは、「オブジェクト指向」の言語です。いわゆる「上流」の開発の方法論も、多くは、「オブジェクト指向」の考えをベースにしています。「オブジェクト指向」言語には、クラスや型の概念があります。そこでは、型のチェックがプログラムの正しさを保証する有力な手段であることは、経験的によく知られていることです。

ただ、「オブジェクト指向」言語には関数の型という概念はありません。関数の型を含めて、型のチェックそのものが、プログラムの正しさの証明になるというのが、このセミナー・シリーズが志向する「論理・証明型言語」の基本的な考え方です。
その意味では、関数型言語での型の扱いを知ることは、「論理・証明型言語」への有益なステップになると考えています。
Updates
  • イベント詳細情報を更新しました。 Diff#536182 2020-03-22 14:07:59
More updates
Thu Mar 26, 2020
7:00 PM - 10:00 PM JST
Add to Calendar
Venue
Tickets
丸山レクチャーズ会員 SOLD OUT ¥1,500
丸山個人協賛会員 SOLD OUT ¥1,500
10代 -- 20代 SOLD OUT ¥1,500
一般 SOLD OUT ¥3,000
Venue Address
目黒区大橋2丁目22−42 地下1階 Japan
Organizer
マルレク
1,175 Followers