20240803_Lean紹介

すごい Lean 楽しく学ぼう ！ プログラミング言語＆証明支援系の Lean 入門 20240803

すごい Lean 楽しく学ぼう ！ Lean は楽しい。以上！ （『すごいHaskell楽しく学ぼう！』イントロダクションのリスペクト） …と言えるほどまだ Lean について詳しくありませんが、 最近興味を持って調べているので簡単に紹介します。 Miran Lipovača (2012) 『すごいHaskellたのしく学 ぼう！』(田中英行・村主祟 行訳) オーム社 ※これはHaskellの本です

今回の内容 ● ● Lean の簡単な紹介 Lean の証明のサンプルコード ※ Lean のプログラミング関連のことは詳しくやりません

Leanって何？ 「プログラミング言語 」であり「証明支援系 （Theorem Prover）」です。 証明支援系とは？ 人間と機械の共同作業で証明の開発を支 援するソフトウェアツール。 いろいろな証明支援系 公式サイト ( https://lean-lang.org/ ) リーン開発などの「lean」と同じなので、 ググるときは「lean lang」などで調べる。 2013 年に Microsoft Research に在籍して いた Leonardo de Moura 氏によって立ち上 げられたプロジェクト。Lean4が最新版。 Coq (1989~) Isabelle (1986~) Mizar (1973~) F* (2011~) Agda (1999~)

• https://lean-lang.org/

証明支援系の実用例 数学の証明の形式化 ● 四色定理 (Coq) ○ G. Gonthier. Formal proof—the Four-Color Theorem. Notices AMS, 55(11):1382–1393, 2008. ハードウェア開発 ● AMD や Intel の開発で使用された ○ D. M. Russinoff. A mechanically checked proof of correctness of the AMD K5 floating point square root microcode. Formal Methods in System Design, 14(1):75–125, 1999. ○ J. Harrison, J. Urban, and F. Wiedijk. History of interactive theorem proving. In J. H. Siekmann, editor, Computational Logic, volume 9 of Handbook of the History of Logic, pages 135–214. Elsevier, 2014. OS や コンパイラの検証 ● ● OS: seL4, CertiKOS コンパイラ: CompCert, JinjaThreads, CakeML WebAssembly の意味論と型システムの形式化 (Isabelle) ● C. Watt. Mechanising and verifying the WebAssembly specification. In J. Andronick and A. P. Felty, editors, CPP 2018, pages 53–65. ACM, 2018. 各種文献情報引用元: The Hitchhiker's Guide to Logical Verification (2024 Edition) https://github.com/lean-forward/logical_verification_2024

• https://github.com/lean-forward/logical_verification_2024

Lean のここが すごい！ ～機能面～ 汎用プログラミング言語として使える！（Haskell などに近い関数型） ● プログラミング言語として実用的かを試すために、Lean でリアルタイムロ ボット制御の実装する実験があった ○ Real-time Robotics Control in the Lean Language - Galois, Inc. (2021/3/29) 数学の証明が書ける！ ● 証明の正しさが機械的にチェックされるので、人為的なミスを防げる Lean の実用例 ● AWS が Cedar 言語の開発に Lean を使用した ○ Lean Into Verified Software Development | AWS Open Source Blog (2024/4/8)

• https://galois.com/blog/2021/03/real-time-robotics-control-in-the-lean-language/
• https://aws.amazon.com/jp/blogs/opensource/lean-into-verified-software-development/

Lean のここが すごい！ ～充実したサポート～ 学習リソースが豊富！ ● ● オンラインで無料で読める本がいくつかある ブラウザでゲーム感覚で遊べる Lean Game Server すぐに試せる！ ● ● ブラウザで試せる Lean4 Web GitHub リポジトリ GlimpseOfLean は GitPod を使ってブラウザで動かせる VSCode 拡張がある！ コミュニティがある！ ● ● 公式 Discord と Zulip がある lean-ja という日本語コミュニティでは英語の学習リソースの和訳や勉強会が行われている

• https://github.com/PatrickMassot/GlimpseOfLean

サンプルコード(1) ペアノの公理による自然数 MyNat を定義する。 -- 帰納型(inductive type)を使ってペアノの公理による自然数 MyNat を定義 -- add を中置記法で書けるようにする -- MyNat は zero か succ のどちらかを取る -- infixl は左結合の中置記法を定義する inductive MyNat where -- 55は演算子の優先順位で高いほど結合度が強くなる | zero : MyNat -- 等号(=)の優先順位は50なのでそれより高い値にしてい | succ : MyNat → MyNat る deriving Repr infixl:55 "[+]" => add -- open で名前空間を開くと、MyNatなしで zero, succ を使える open MyNat -- MyNat に足し算を定義する def add (a b : MyNat) : MyNat := match b with | zero => a | succ n => succ (add a n)

サンプルコード(2) -- add の定義から明らか -- rfl タクティク: reflexivity の意味で、左右の等号の値が同じときに使う theorem add_zero (n : MyNat) : n [+] zero = n :=by MyNat に定義した足し算が 0 + n = n を満たすかを証明する。 rfl theorem add_succ (a b : MyNat) : a [+] succ b = succ (a [+] b) :=by rfl -- add の定義からすぐに導けないので帰納法を使って証明する -- rw タクティク: rewrite の意味で、指定した定義などで goal を書き換える -- 任意の MyNat の要素 n について、 0 + n = n が成り立つことを示す theorem zero_add (n : MyNat) : zero [+] n = n :=by -- n に関する帰納法 induction n with -- 1. n が MyNat.zero の場合に成り立つことを示す | zero => rw [add_zero] -- 2. 任意の n : MyNat について、 n のとき成り立つと仮定したときに MyNat.succ n も成り立つことを示す -- ih は induction hypothesis （帰納法の仮定）の略 | succ n ih => rw [add_succ] rw [ih]

参考サイト ● 日本語コミュニティ: LEAN JA ○ ● Lean community ○ ○ ● Lean by Example : タクティクやコマンドの説明がまとめられている日本語資料 Lean 関連の情報がまとまっているサイト このページの Learning Lean 4 に各種学習リソースのリンクがある Natural Number Game ○ ブラウザでゲーム感覚で Lean を学べるチュートリアル。

• https://lean-ja.github.io/
• https://lean-ja.github.io/lean-by-example/
• https://leanprover-community.github.io/
• https://leanprover-community.github.io/learn.html
• https://adam.math.hhu.de/#/g/hhu-adam/NNG4