Zenn
🐣

TAPLとLeanの同時入門のススメ 予告編(締切に敗北しました)

2023/12/03に公開
math
初心者向け
tapl
lean4
tech

この記事は定理証明支援系 Advent Calendar 2023 の3日目の記事です。
https://adventar.org/calendars/9022

2日目は @elpinal さんの Isabelle/HOLで位相空間論の初歩を証明した でした。

注意

この記事は未完成のまま投稿されています。(筆者が締切に敗北したため)
投稿前にレビューをもらったところまだまだ説明が足りない部分が見つかったので、頑張って完成度を上げていく所存です。
あと、かなりの長編になりそうで本編は4~5回に分けて投稿することになるかも。

TAPLの3章をLeanで形式化したコードについてはここから参照できます。この内容が理解できるところまで解説するのが目標です。
https://gist.github.com/spinylobster/f7ef4a881db3ba42ee89de8079bb06b8

この記事は以下のような人を想定読者としています。怖くないよ！

  • Python、Java、TypeScriptなどの言語は使えるが、OCamlやHaskellのような関数型言語には馴染みがない
  • 大学で習うような高度な数学のことは全く知らない
  • TAPLに挑んだけど序盤(3章)でもう書いてあることが全然頭に入ってこない
  • というかまだ読んだことさえない。けどプログラミング言語や型の仕組みに興味がある

また、以下のことにご注意ください。

  • ごめんなさい、型の話はしません[1]。型に入門するんじゃなくて、TAPLに入門します
  • 前提とする知識をなるべく少なくしているため、説明がクソ長いです
  • プログラミング言語の機能や構文の知識を前提としています。ジェネリクス、インターフェース、列挙型、匿名関数などです。

TAPLって何？

TAPLとは、書籍「型システム入門」(原著名 "Types and Programming Languages")の略称です。
プログラミング言語の「型」や様々な言語機能の数学的に厳密な定義をまず考え、その性質について証明を述べるというスタイルで型に関するかなり広範な話題について基礎から丁寧に教えてくれる、計算機科学の大学院生向けの教科書です。

僕が最初に書いた想定読者は完全に対象外ですねこれ……
実際、書籍のタイトルに釣られて「型のことってそういえばちゃんと勉強したことないな。入門って書いてるし初心者にも優しそうだからこれで勉強しよう」と考えた向上心旺盛な良心的プログラマが数多くフルボッコにされているのではないでしょうか(※筆者の想像です)

実際、僕がまさにそんな感じで、「書いてあることが分かるようで分からない」「自分の解釈が合っているのか自信がない」というモヤモヤ感が1段落ごとに増していき、読み進めることができなくなってしまいました。
理解した上で読み直すとすごく丁寧に説明されていることが分かるので、本の内容や和訳には問題ありません。つまり問題は僕自身にあるということです。悲しいね……

しかし！TAPLの内容をプログラミング言語Leanのコードに翻訳することによって、数学に強くない人でもTAPLをちゃんと理解することができるよ！というのがこの記事の主張であり、試みです。

「Leanって何？」「他の言語じゃダメなの？」という疑問にはこの次でお答えします。

TAPLで具体的にどんな話題があるのかについてはsititou70さんのTAPLの読書感想文がとても分かりやすいので、ぜひ読んでみてください。
https://sititou70.github.io/よわよわエンジニアが-TAPL（型システム入門）を読んだら/

Leanって何？

ありがたいことに、Leanに関する情報をまとめてくれているlean-jaという日本語のコミュニティがあります。
この記事で必要になる知識は本文中で伝えるつもりですが、より詳しく知りたい方はご利用ください。

僕がLeanをざっくりと説明するならば、こうなります。

  • Haskellにかなり近い文法を持っている純粋関数型プログラミング言語
  • それに加えて依存型という型システムにより型で数学的な命題を表現できる
  • Leanで書いた式の型が「命題を表現した型」と一致するなら、その命題が正しく証明されたことになる
  • 証明を書くことを支援する機能がある

最初はともかく、後の3つは「どういうこと？」と疑問に思っていることでしょう。
まず「依存型」とは……って、ちょっと待った。この記事では型の話をしないって最初に言いましたよね？
依存型がどんなものかはこの時点では理解できないと思います。
ただ、Leanを読み書きして型の表現力がめっちゃ高いなぁと感じたら、その時あなたは依存型を体感しています😏
ちなみに僕はまだTAPLを読んでる途中なので依存型の説明はそもそもできません。ちゃんと知らなくても、Leanは使えます[2]
ここで重要なことは、Leanでは数学の証明が書けて、それが正しいかどうかコンパイラにチェックしてもらえる、という点です。

(ちょっと脱線)他の言語じゃダメなの？

TAPLはラムダ計算と呼ばれるとても小さい仕様(文法が変数 関数 関数適用(関数呼び出し) の3つしかありません！)のプログラミング言語をベースに機能を拡張していく、プログラミング言語の実装に関する本という側面もあります。
実際、TAPLには本の中で定義した言語を(OCamlで)実装する章がありますし、そのOCaml実装は公開されています。
公式以外でも「ラムダ計算をJavaScriptで実装してみた」みたいな例は探せばたくさん見つかることでしょう。

そういった 「言語の実装」に限って言えば RubyやC言語や他の何かでも可能ですが、 言語や型が持つ性質について証明 しようとすると、Leanのように 依存型のある言語を使う必要がある のです。
TAPL本文のかなりの割合が数学的な定義と証明になっているので、そういったパートを理解するためにこの記事ではLeanを使います。

(もうちょっと脱線)定理証明支援系について

Leanのように数学の定理を証明できるシステムを定理証明支援系(Theorem Prover)と呼びます。
僕がLeanの説明として挙げた特徴は、他の定理証明支援系にも共通します。
他の定理証明支援系の特徴について(僕の知る限りで)お伝えしましょう。
※AgdaとIdrisの良さが経験不足で説明できないので、これを読んだAgda使いやIdris使いがいたら教えてください🙇 TwitterやFediverseに投稿してもらえれば頑張って見つけるので

  • Coq: ユーザ数が日本で最も多く(※筆者の感覚値です)、日本語の情報も比較的豊富です。オンラインの勉強会が定期的に開かれているため(※2023年現在)、気軽に参加してみてください。Coqを仕事で日常的に使っているような人たちと話ができて最高ですよ。
  • Isabelle: 定理証明支援系で書かれた証明はプログラミング言語のコードに近いため証明の流れが一見して分かりにくいのですが、Isabelleを使うとまるで証明が自然言語で書かれているかのように工夫できます。Sledgehammerという、コンピュータが頑張って定理の証明に挑戦してくれる(自動定理証明と呼びます)強力な機能が標準で提供されていることも魅力です。
  • Agda: AgdaについてはEmacsと親和性が高いという印象がある以外ほとんど知りません。Agdaの魅力について教えてくださる方コメントください 🙇
  • Idris: Idrisは登場時期が2007年で比較的若い言語です。定理証明支援系としてというより、関数型プログラミング言語として「イケてる」機能を備えている印象があります(ふわっとしててごめんなさい🙇)

このように様々な選択肢がある中でLeanを選んだのは、ひとえに VSCodeとの親和性が高い ことが理由です。(Language Server Protocolに対応しているので他のエディタでも快適に使えると思います)
普通のプログラミングと同じく、定理や証明の書き方も一度慣れれば他の定理証明支援系にも応用が効くので、とりあえずLeanをちょっとお試ししてみてくださいな。

最後に紹介しておきたいものとして、定理証明支援系のユーザが集う毎年のイベントがあります。
TPP(Theorem Proving and Provers meeting) 2023
発表の概要を読んでもほとんど理解不能で、「これ専門家しか参加しないイベントじゃないの？」と思ったのですが、聞くところによると研究者の方以外もたくさん集まっていたようです。ちなみに2023年の参加者は41名とのこと。
一人で勉強していると分からないことだらけで辛くなることも多々あるので、こういったコミュニティの存在はありがたいですね。

Leanを使ってみよう

さて、Leanの話に戻ります。「数学の証明が書ける」って一体どういうことなんでしょうか？
百聞は一見にしかず。まずは「1 = 1」という命題を証明をしてみましょう！(「それ証明する意味ある？」って感じですが、説明のためなので許してください)

あ、その前にLeanの実行環境を整える必要がありますね。

https://lean-lang.org/lean4/doc/quickstart.html
こちらは公式ドキュメントで、英語ですが画像付きなので十分分かりやすくなっています。
念の為手順を日本語でも記しておきます。(古くなっている可能性があるので、なるべく公式ドキュメントを参照してください)

  • 公式のVSCode拡張をインストールする
  • VSCodeで新規にテキストファイルを開き、1行目に表示されている「Select a language」をクリックしてlean4を選択する (空の.leanファイルを作ってVSCodeで開くだけでも良いです)
  • 右下にエラーのポップアップが出るので、Install Lean using Elanをクリックする(ElanはLeanのバージョン管理ツールです)
  • 1行目に #eval Lean.versionString と入力する。Leanのバージョンが右のペインに表示されれば、無事インストール完了🎉

こちらの記事にEmacsでの設定例などがあります。
https://zenn.dev/labbase/articles/b24dca38e0420d

LeanはWeb上で動かすこともできます。
https://live.lean-lang.org/

Leanを使える環境は整いましたか？
leanとlakeとelanがお使いのシェルで使えていれば良いのですが、もし使えない場合は~/.elan/binにPATHを通せば大丈夫なはずです。
それでは、「1 = 1」という命題を証明する次のコードを入力してみてください。

theorem one_eq_one : 1 = 1 := Eq.refl 1

この文はそれぞれ以下の要素に分かれています。
lean_one_eq_one

最初に文法について説明し、その後で「なぜこのコードが1 = 1の証明になるのか？」を説明したいと思います。

変数宣言

theorem は変数宣言をする時に書くキーワードで、他の言語では var や let に相当します。RubyやPythonのように変数宣言にキーワードが不要で変数名から書き始める言語もありますが、Leanではキーワードが必要です。
theoremは日本語に訳すと「定理」という意味なので、変数宣言のキーワードとしてはかなり不思議な感じがすることでしょう。Leanには他にもdefという変数宣言のキーワードがあり、普通の変数や関数を定義する時にはこちらを使います。

以下の2つの文はどちらもコンパイラのチェックをパスしますが、いくつか違いがあります。

def nums : List Int := [0, 1, 2]
theorem nums : List Int := [0, 1, 2]

まず、defによる宣言では型注釈を省略可能で、def nums := [1, 2, 3]と書くことができます[3]が、theoremではできません。
theoremは命題を証明するために使うのに、型を省略できる(どんな命題か書かなくていい)なんておかしいですよね。

また、theoremで宣言した変数は実行時に計算されるということがありません。定理は型チェックが通っているかどうかが重要なので、実行する必要はないというわけです。
試しにnumsを宣言した次の行に#eval numsと書くと、defで宣言した場合は変数の値が表示されますが、theoremに変えると英語で何やら文句を言われます。numsを実行可能なコードと認識していないようです。
ということで、theorem nums : List Int := [0, 1, 2]は完全にナンセンスで、たまたまコンパイルに通るだけの役に立たないコードです。

もう一つの注意点は、Leanでは例えば以下のJavaScriptのコード

let x; // 変数を初期化せず、宣言だけ行う
x = 1;
x = 2; // 変数の値を変更する(再代入する)

のように未初期化の変数を宣言したり、変数に再代入することはできないということです。
これは「純粋関数型プログラミング言語」と呼ばれるものの特徴で、Haskellも同じです。
不便そうに思うかもしれませんが、実はそんなに困らないので気にしなくて大丈夫です。

まとめ

  • 変数宣言のキーワードにはdefやtheoremがある
  • defは普通の値や関数の定義に使い、theoremは数学の定理を定義する時に使う
  • #eval <式>というコマンドを使って式の計算結果を知ることができる
  • 一度宣言した変数の再代入はできない

型が 1 = 1 ってどういうこと？

one_eq_oneの話に戻りますが、このコードの最も奇妙な点は、普通ならIntのような型の名前を書くべき場所に 1 = 1 という式のようなものが登場しているところでしょう。
これを説明するために、先ほどの例をTypeScript風の文法で書いてみました。

const nums: Array<number> = [1, 2, 3];
const one_eq_one: Eq<1, 1> = Eq.refl(1);

Leanの1 = 1をTypeScript風に表現すると、Eq<1, 1>となりました。
つまり、1 = 1は実態としてはEqというジェネリックな型に2つのパラメータ(1と1)を渡しているのと同じであり、それを数学的な書式と一致するように=を使って書けるようにしているだけなのです。

これを確かめるために、何行目でもいいので式の型を確認するために#check Eq 1 1と書いてみましょう。1 = 1 : Propというメッセージが表示されたと思います。
Eq 1 1と書いたにも関わらず1 = 1と表示されるので、Leanは数学的な記法の方を優先して表示するようですね。

ついでに、Eq.refl 1についても説明しましょう。
TypeScript風の例でEq.refl(1)と書いたことから分かるように、これはEq.reflという関数に1という値を渡しています。
多くのプログラミング言語では関数は関数(引数1,引数2,...)と書いて実行しますが、関数型言語では 関数 引数1 引数2 ... と関数の後ろに空白区切りで引数を並べるスタイルがほとんどです。そういうものだと思って慣れてください。

まとめ

  • 1 = 1はEq 1 1の別の表記
  • #check <式>というコマンドを使って式の型を確認できる

どうしてこれが証明になるの？

……今回はここまでです🙇
12月中に続きが書けるように頑張りたい

最後に

定理証明支援系に興味がある人、数学に強い人と友達になりたいので仲良くしてください。
(色んなことに興味が移りがちなので、型とか数学の話をしてモチベを維持したい)

脚注

  1. プログラミング言語の構文(文法)と意味論(実行するとどうなるか)の形式化(数学的に厳密に定義する)の話をします。 ↩︎

  2. それでも依存型について知りたい人へ: https://aconite-ac.github.io/theorem_proving_in_lean4_ja/dependent_type_theory.html ↩︎

  3. 型注釈を省略した場合、 nums の型は List Nat になります。Leanでは整数(Int)や自然数(Nat)のように数を表す型が複数あり、1はデフォルトではNatとして解釈されるようですね。 ↩︎

Discussion