年末は帰省していたのですが、有休含めて1/8までお休みにしたこともあり時間ができました。そこでLean 4を勉強してみることにしました。
Lean 4は以前このブログで紹介したLean 3と呼ばれる定理証明支援システムの後継システムです。
Lean 4からは関数型プログラミング言語としても使える、という触れ込みのようです。そこで今回はまず関数型プログラミング言語としてのLean 4を勉強してみました。勉強に使ったテキストは
Functional Programming in Lean - Functional Programming in Lean
です。このテキストを1章から4章まで読んでみました。その中で自分の勉強になったことをメモ書きしたのがこの記事です。またいくつかのネット上の資料を参考にもさせていただいたので記事の最後にまとめておきます。
関数型プログラミング言語なのでまずは関数を定義してそれを使って計算することができます。Lean 4では関数名の後ろに括弧なしで引数を並べて書くのでいきなりびっくりします。String.append "tako " "ika"のように書くと2引数の関数String.appendが"tako ika"を計算してくれるのです。演算子の優先順位が分からないので関数適用にカッコをつけていくとこんな感じになってしまいます。
(String.append "tako" (String.append "ika" "surume"))
まるでLispのようです。
また数字リテラルは自然数型(0以上の整数)です。自然数同士の引き算で第1引数が第2引数よりも小さい場合には結果は0になります。3-4は0になります。これが第２の驚きでした。コードを書く際にはInt型を意図するならきちんと型宣言必要があり要注意と思いました。
そして第３の驚きは自然数型Natがzeroとsuccから構成されていることです。理論的にはそのような構成を取るしLean 3の自然数の構成ではそのようになっていましたが、プログラミングの世界でこの構成をとる言語を見るのは初めてでした。例えば階乗関数は次のように定義できます。
def myFact (n :Nat) : Nat :=
match n with
| Nat.zero => 1
| Nat.succ k => n*myFact k
myFactはNat型のnを引数にとってNat型を返す関数です。そして引数nがNat.zeroにマッチすれば1を返しますし、succ kとマッチすればmyFact kとnをかけたものを返します。nとsucc kがマッチしているのでk=n-1であることに注意してください。
第４の驚きは、上記の階乗の定義を間違えて次のようにすると
def myFact (n :Nat) : Nat :=
match n with
| Nat.zero => 1
| Nat.succ k => k*myFact n
いきなりコンパイルエラーが起きます。正しい定義との違いは、最後の行でn*myFact kとすべきところk*myFact nとしてしまっています。エラーメッセージを読んでみると、myFactの停止性が証明出来ない、というものでした。それはその通りで最後の行でmyFactを再帰呼び出しする際に元のnをそのまま使っているので無限ループしてしまうはずです。大抵の言語では末尾再帰の最適化を行うので無限ループで実行が止まらないか、その最適化をしなくてスタックオーバーフローするかどちらかでしょう。
ということは最初に記載した正しいプログラムのようにこのエラーが出ないプログラムでは停止性を証明しているんですね。この辺は定理証明支援系と一体化しているメリットなのだと思いました。
第５の驚きは型の拡張性と実用性です。自分で型を拡張することやその拡張をリテラル値まで拡張できることにもびっくりしました。mod pの有限体を型として定義して、{0, 1, 2,,, p-1}で表示して加減乗除演算やリテラルをこの型専用に定義するようなこともできそうです。また有限体$GF(p^n)$も厳密に定義できそうです。というか多分定理証明支援系の方のライブラリにはすでにありそうです。
5章以降ではモナドという現代の関数型言語では必須の仕組みが解説されています。個人的な理解としては関数型言語で「計算の状態」を表すためのデザインパターンみたいなものと思っています。なのでLean 4のモナドを理解しなくてもその個々の応用(IO など)が使えれば十分かなと思っています。なのでここから先は必要に応じて読むことにしました。
この辺を読んでいて面白いなと思ったのは、自分が1987年頃に大学でプログラミングの理論を勉強したときはモナドは出てきませんでした。その原型の１つであろう「継続」やschemeのcall-cc (call with current continuation)を計算理論好きの友人が面白がって教えてくれたことを覚えています。今回勉強してみてモナドは1990年代以降に大きく取り上げられてさまざまな関数型言語に実装されてきたことを知りました。今30歳-40歳の人たちは大学でモナドを勉強してきているのでしょうか。
一旦これで関数型言語としてのLean 4はちょっとだけ分かった気になって、次は定理証明支援系のLean 4について勉強を進めていきます。
以下のネット上のリソースを参考にさせていただきました。ありがとうございました。
パンの木を植えて Lean4の記事がいくつもあります。
lean4 のコード例と(日本語)解説を作成する 証明支援の例がたくさんあります。
次に流行る※プログラミング言語「Lean」 - Speaker Deck スライドによるわかりやすい説明です。
