論理学入門 II -- ラムダ計算と関数型言語
2020/03/27 マルゼミ「論理学 II」概要
「論理学 I」との関係について
前回の「論理学 I — 命題論理の演繹ルール」では、「推論する能力」の最も基本的な基礎である、論理的推論ルールにフォーカスしました。今回の対象は、数学的推論の基礎で、前回のセミナーの内容を前提とはしていません。前回のセミナーを受講していない人も、独立の内容として理解できると思います。「論理学 I」と今回の「論理学 II」で別々に展開してきた、論理的推論と数学的推論の接点については、次回の「論理学 III -- 型の理論」(「型の理論」入門に改題しました)で統一的に扱う予定です。
型のないラムダ計算
今回のセミナーで最初に学ぶのは、1930年代にチャーチが定式化した、「型のないラムダ計算」です。
基本的には、「引数」に対して値を返すものとして「関数」を捉えて、関数で表された式に対する「代入」と式の「変形」を、少し、抽象的に捉えたものです。見かけは単純ですが、強力な計算能力を持ちます。
型付きラムダ計算
今回のセミナーで二つ目に学ぶのは、同じくチャーチが1940年代に開発した、「型付きラムダ計算」のシステムです。
「型のないラムダ計算」を基礎としながら、AからBへの関数に、"A -> B" という「型」を与えるのが、大きな特徴です。
このシステムは、関数型言語の基礎になります。
関数型言語
今回のセミナーでは、こうした関数の「型」が、関数型言語でどのように利用されているのかを、みていきたいと思います。
Coqも関数型言語としての顔を持ちます。今回のセミナーでは、関数型言語としてのCoqのプログラミングについていくつかの例を紹介しようと思います。
なぜ、関数型言語を学ぶのか？
現在、多くのプログラマーがよく知っているのは、「オブジェクト指向」の言語です。いわゆる「上流」の開発の方法論も、多くは、「オブジェクト指向」の考えをベースにしています。「オブジェクト指向」言語には、クラスや型の概念があります。そこでは、型のチェックがプログラムの正しさを保証する有力な手段であることは、経験的によく知られていることです。
ただ、「オブジェクト指向」言語には関数の型という概念はありません。関数の型を含めて、型のチェックそのものが、プログラムの正しさの証明になるというのが、このセミナー・シリーズが志向する「論理・証明型言語」の基本的な考え方です。
その意味では、関数型言語での型の扱いを知ることは、「論理・証明型言語」への有益なステップになると考えています。
