「Lean (証明アシスタント)」の版間の差分

2025年2月17日 (月) 03:22時点における版

2025年10月14日 (火) 04:01時点における最新版

(5人の利用者による、間の21版が非表示)

1行目:

{{Infobox programming language|name=Lean|logo=Lean logo2.svg|logo size=220|paradigm=[[関数型プログラミング]]|developer=[[Leonardo de Moura]]<br/> [https://lean-fro.org/ Lean FRO]|released={{Start date and age|2013}}|latest release version=v4.1624.0|latest release date={{Start date and age|2025|0209|0315}}|repo=|typing=[[型推論|推論される]], [[型システム#強い型付けと弱い型付け|強い]], [[静的型付け|静的]]|platform=|operating system=[[クロスプラットフォーム]]|language=English|genre=[[Proof assistant]]|license=[[Apache License 2.0]]|website={{URL|https://lean-lang.org/}}|influenced=koka|influenced_by=[[ML (プログラミング言語)|ML]]<br/>[[Coq]]<br/>[[Haskell]]<br/>Prolog<br/>Rust<br/>[[Scheme]]}}

[[ファイル:Cantor theorem.png|代替文=Lean4で Cantor の定理を示している様子|サムネイル|Cantorの定理をLeanで示している様子．右側の infoview に今使える仮定と示すべきゴールが常に表示される．]]

'''Lean''' は Calculus of Inductive Constructions (CIC) と呼ばれる型システムに基づく、純粋関数型[[プログラミング言語]]の一つである。 functional but in-place と呼ばれるプログラミングパラダイムに基づいており、従来の純粋関数型言語のパフォーマンス上の欠点を改善している。さらに、Lean は「衛生的かつでありながら非常に強力な[[メタプログラミング]]フレームワークを備えており、ユーザがパーサやエラボレータを自在に拡張することができる。Lean はまた、純粋[[関数型プログラミング]]言語」であるとり、同時に{{仮リンク|「Calculus of Inductive Constructions (CIC) と呼ばれる依存型の一種に基づく定理証明支援系|en|Proof assistant|preserve=1|label=」でもあるという２つの顔を持つ。この、汎用プログラミング言語でありながら定理証明支援系(theorem prover)}}でもあり、Mathlib るという点は Lean の大規模きな形式化された数学ライブラリを擁す特徴である。

Lean は純粋関数型プログラミング言語でありながら、標準でループや可変ローカル変数の構文を備えているほか、一定の条件の下で関数アクセスをフィールドアクセスのように書くことができるという構文上の特徴がある。また、「参照カウントに基づいて自動的に破壊的変更を行う」という、Functional but in-place と呼ばれる最適化を行う。総じて、従来の関数型言語のパフォーマンスと構文面における欠点を改善している。

また、定理証明支援系としての Lean は、Unicode の積極的な使用と高度な対話性、拡張性の高さによる構文定義の柔軟性により可読性と快適な UI を提供することにある程度成功しており、型システムの専門家や形式証明の研究者だけでなく、数学研究者や学生からも支持を集め、Mathlib という大規模な形式数学ライブラリを擁するに至った。

== 歴史 ==

189 ⟶ 193行目:

=== 拡張可能性 ===

Lean は強力なメタプログラミング機能を持っており、新しい記法の定義や証明の自動化が行えるようになっている。以下は、<code>notation</code> コマクロとしてンドで記法を定義する例である。<syntaxhighlight lang="lean" line="1">

def modulo (k n m : Int) : Prop := k ∣ (n - m)

196 ⟶ 200行目:

#check (1 ≃ 6 mod 5)

</syntaxhighlight><code>declare_syntax_cat</code> コマンドや <code>macro_rules</code> コマンドを使うことで、さらに複雑な構文も定義することができる。<ref>{{Cite web |url=https://lean-ja.github.io/lean-by-example/ |title=Lean by Example |access-date=2025年2月17日 |publisher=GitHub}}</ref><syntaxhighlight lang="lean" line="1">

/-- 2項演算の集合 -/

inductive Op where

/-- 加法 -/

| add

/-- 乗法 -/

| mul

deriving BEq

/-- 数式 -/

inductive Expr where

/-- 数値リテラル -/

| val (n : Nat)

/-- 演算子の適用 -/

| app (op : Op) (left right : Expr)

deriving BEq

namespace Expr

/- ## Expr の項を定義するための見やすい構文を用意する -/

/-- `Expr` のための構文カテゴリ -/

declare_syntax_cat expr

/-- `Expr` を見やすく定義するための構文 -/

syntax "expr!{" expr "}" : term

syntax:max num : expr

syntax:30 expr:30 " + " expr:31 : expr

syntax:35 expr:35 " * " expr:36 : expr

syntax:max "(" expr ")" : expr

macro_rules

| `(expr!{$n:num}) => `(Expr.val $n)

| `(expr!{$l:expr + $r:expr}) => `(Expr.app Op.add expr!{$l} expr!{$r})

| `(expr!{$l:expr * $r:expr}) => `(Expr.app Op.mul expr!{$l} expr!{$r})

| `(expr!{($e:expr)}) => `(expr!{$e})

-- 構文が正しく動作しているかテスト

#guard

let expected := Expr.app Op.add (app Op.mul (val 1) (val 2)) (val 3)

let actual := expr!{1 * 2 + 3}

expected == actual

end Expr

</syntaxhighlight>

=== 自動証明 ===

Lean は対話的に証明を書くことをサポートするだけでなく、タクティクによる自動証明機能も提供する。

以下は複雑な命題に見えるが、たった一つのタクティクで証明が終了する例である。<code>omega</code>は自然数や整数の線形算術の自動化に長けたタクティクで、面倒な証明も自動化してくれる。<syntaxhighlight lang="lean" line="1">

example (a₁ a₂ a₃ : Nat) : 3 ∣ a₁ + 10 * a₂ + 100 * a₃ ↔ 3 ∣ a₁ + a₂ + a₃ := by

omega

</syntaxhighlight>

</syntaxhighlight>また次は、直観主義論理（排中律を仮定しない論理）における証明を自動で行ってくれるタクティクの例である。<syntaxhighlight lang="lean">

import Mathlib.Tactic.ITauto

/-- 排中律の二重否定 -/

example (P : Prop) : ¬¬ (P ∨ ¬ P) := by

intro h

apply h

have : ¬ P := by

intro hp

have : P ∨ ¬ P := by left; assumption

contradiction

right

assumption

また次のコードも、複雑に見える命題の証明が一発で終わる例である。ここで使用している <code>grind</code> タクティクはカスタマイズ可能で汎用的かつ強力な証明自動化タクティクであり、この例では帰納的述語のケース分割などを行わせているが、線形算術なども行うことができる。<syntaxhighlight lang="lean">variable {S : Type} (R : S → S → Prop)

example (P : Prop) : ¬¬ (P ∨ ¬ P) := by

itauto

/-- 反射的閉包 -/

</syntaxhighlight>

inductive ReflClosure : S → S → Prop where

/-- `ReflClosure`は`R`を含む -/

| incl : ∀ x y, R x y → ReflClosure x y

/-- `ReflClosure`は反射的 -/

| refl : ∀ x, ReflClosure x x

/-- `Prime R := R ∪ {(s, s) ∣ s ∈ S}` -/

def Prime := fun x y => R x y ∨ x = y

example : ReflClosure R = Prime R := by

grind [Prime, ReflClosure]</syntaxhighlight>

== Lean の特徴 ==

224 ⟶ 273行目:

=== テーブル化型クラス解決(Tabled Typeclass Resolution) ===

[[ファイル:Diamonds perf.png|代替文=型クラス解決アルゴリズムの実行時間の比較|サムネイル|Lean 4 の型クラス解決アルゴリズムは、実行時間を指数的に改善した. <ref name=":2">{{CiteCitation|title=Tabled webTypeclass Resolution|last=Selsam|first=Daniel|last2=Ullrich|first2=Sebastian|last3=Moura|first3=Leonardo de|date=2020-01-21|url=https://arxiv.org/abs/2001.04301 |titledoi=Tabled Typeclass Resolution 10.48550/arXiv.2001.04301|access-date=2024/05/25 |publisher=arxiv2025-03-17}}</ref>]]

型クラスは、プログラミングと定理証明の両方において、'''アドホック多相性''' <ref>型に応じて、同じ処理に複数の実装を提供すること</ref> を実現してくれる。しかし、Lean の急成長中の数学ライブラリ Mathlib の中で、型クラスが広く使われるにつれ既存の型クラス解決手続きの理論的限界が進歩の妨げになるようになった。既存の型クラス解決手続きの主要な理論的限界とは、次のようなものである：

230 ⟶ 279行目:

* サイクルが存在する場合に発散が生じる

Lean 4 では、この２つの問題を解決する新しいアルゴリズムであるテーブル化型クラス解決が実装されている。このアルゴリズムは Prolog に対して1998年に <ref>{{Cite web journal|urllast=https://www.researchgate.net/publication/200034107_An_Abstract_Machine_for_Tabled_Execution_of_FixedSagonas|first=Konstantinos|last2=Swift|first2=Terrance|date=1998-Order_Stratified_Logic_Programs 05-01|title=An Abstractabstract Machinemachine for Tabledtabled Executionexecution of Fixedfixed-Orderorder Stratifiedstratified Logic Programslogic programs|access-dateurl=2024https:/05/04dl.acm.org/doi/10.1145/291889.291897|journal=ACM Trans. Program. Lang. Syst.|publishervolume=ResearchGate20|issue=3|pages=586–634|doi=10.1145/291889.291897|issn=0164-0925}}</ref> 提案された型クラス解決アルゴリズムに基づく<ref name=":2" />。

=== 拡張された do 記法 ===

Lean は純粋関数型言語であるため、手続き型言語では暗黙に扱われる副作用を、モナドという再利用可能な抽象的要素で再定義することで扱っている。この再定義によって、副作用をより厳密に制御したり、派生的な副作用を導入したりすることを可能にしている。モナドは Haskell の最もよく知られた抽象化機能であり、そのユビキタスな糖衣構文である do 記法と常に結びついている。

Lean では、メタプログラミングフレームワークによる高い拡張可能性を生かして、do 構文が Haskell と比べて拡張されている。具体的には以下のような記法を最初からサポートしている<ref>{{Cite web journal|urllast=https://dl.acm.org/doi/10.1145/3547640Ullrich|first=Sebastian|last2=de Moura|first2=Leonardo|date=2022-08-31|title=‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl) |access-dateurl=2024https:/05/25dl.acm.org/doi/10.1145/3547640|journal=Supplement of "'do' Unchained: Embracing Local Imperativity in a Purely Functional Language"|publishervolume=ACM6|issue=ICFP|pages=109:512–109:539|doi=10.1145/3547640}}</ref>。

* 可変な変数を <code>let mut</code> で宣言できるようにする Rust ライクな記法

241 ⟶ 290行目:

* <code>for</code> ループ、<code>break</code> や <code>continue</code> といった制御フロー

たとえば、以下は Lean 4 で実装したエラトステネスの篩である。<syntaxhighlight lang="lean" line="1">

/-- `n`以下の素数のリストを `Array Bool` の形で返す。

private def eratosthenesAux (n : Nat) : Array Bool := Id.run do

`i` 番目が `true` ならば `i` は素数で、`false` ならば合成数。 -/

let mut isPrime := Array.mkArray (n + 1) true

private def eratosthenesAux (n : Nat) : Array Bool := Id.run do

let mut isPrime := Array.mkArrayreplicate (n + 1) true

isPrime := isPrime.set! 0 false

254 ⟶ 305行目:

break

-- `p` の倍数を消していく

let mut q := p * p

while q <=≤ n do

isPrime := isPrime.set! q false

q := q + p

264 ⟶ 316行目:

def eratosthenes (n : Nat) : Array Nat :=

eratosthenesAux n

|>.zipIdx

|>.filterMap fun ⟨isPrime, i⟩ =>

if isPrime then some i else none

#guard eratosthenes 10 = #[2, 3, 5, 7]

#guard

#guard (eratosthenes 100).size = 25

let actual := eratosthenes 100

let expected := #[

2, 3, 5, 7, 11,

13, 17, 19, 23, 29,

31, 37, 41, 43, 47,

53, 59, 61, 67, 71,

73, 79, 83, 89, 97

]

expected == actual

</syntaxhighlight>

375 ⟶ 436行目:

* [[Coq]]

* [[Agda]]

* {{仮リンク|Isabelle (証明アシスタント)|en|Isabelle_(proof_assistant)|label=Isabelle}}

== 外部リンク ==

383 ⟶ 444行目:

* [https://reservoir.lean-lang.org/ Reservoir] Lean のパッケージレジストリ。パッケージをインデックスするだけでなく、ビルドとテストも行う。

* [https://marketplace.visualstudio.com/items?itemName=leanprover.lean4 vscode-lean4] [[Visual Studio Code|VS Code]] に Lean 言語のサポートを追加する拡張機能。Unicode 記号をサポートしていて、<code>×</code> に対する <code>\times</code> のような[[LaTeX]]に似たシーケンスを使用して入力ができるようにする。

* [https://www.ams.org/journals/notices/202507/noti3184/noti3184.html Paola Iannone, Gihan Marasingha and Athina Thoma: "Teaching Mathematics with Lean: Interactive Theorem Provers in the Classroom", Notices of AMS (Aug. 2025)]

{{Normdaten}}

[[Category:2013年に作られたプログラミング言語]]

[[Category:証明アシスタント]]

[[Category:定理証明ソフトウェア]]

[[Category:依存型言語]]

[[Category:数学教育ソフトウェア]]

[[Category:関数型プログラミング言語]]

[[Category:FLOSSFOSS]]

[[Category:C++でプログラムされた自由ソフトウェア]]

[[Category:マイクロソフトのフリーソフト]]

[[Category:マイクロソフトのプログラミング言語]]

[[Category:マイクロソフトリサーチ]]

[[Category:Apache Licenseのソフトウェア]]