5. 再帰定義（Recursive Definitions）🔗

任意の再帰関数定義を許してしまうと、Lean の論理は矛盾してしまいます。一般的な再帰は循環証明を書くことを可能にします：「命題 P は真である、なぜなら命題 P は真だからである」証明以外では、無限ループには Empty 型を割り当てることが可能です。これは Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if Lean can show that an empty set of patterns is exhaustive given `e`'s type, e.g. because it has no constructors.nomatch や Empty.rec などと一緒に使うことで任意の定理を証明することができます。

再帰関数定義を全面的に禁止した場合、Lean の有用性ははるかに低下してしまうでしょう：帰納型は述語とデータの両方を定義する鍵となる概念であり、再帰的な構造を持っています。さらに、ほとんどの有用な再帰関数は健全性を脅かすものではなく、無限ループは通常、意図的な動作ではなく定義の間違いを示しています。Lean では、再帰関数を禁止する代わりに、各再帰関数を安全に定義することを要求しています。再帰定義をエラボレートする際に、Lean のエラボレータはその関数が安全に定義されていることを示す正当性も提供します。エラボレーションの概要にあるエラボレータの出力の節は、エラボレータの全体的な文脈の中で再帰定義のエラボレーションを説明しています。

定義できる再帰関数には主に4種類あります：

構造的再帰関数: 構造的再帰関数は、関数が当該引数の厳密な部分コンポーネントに対してのみ再帰呼び出しを行うように引数を取ります。厳密に言えば、型が添字付けられた型の族である引数は、それらの添字と共にグループ化され、コレクション全体が1つの単位とみなされます。エラボレータは再帰を引数の再帰子の使用に変換します。型が正しい再帰子の使用は、すべての無限後退を回避することが保証されているため、この変換は関数が停止する根拠となります。再帰子を介して定義された関数の適用は再帰の結果と definitionally equal であり、カーネル内部において通常は比較的効率的です。

整礎関係上の再帰: 多くの関数は構造的再帰へと変換することも難しいです；例えば、ある関数について引数の配列のインデックスと配列のサイズの差がインデックスが増加するにつれて減少するような場合、この関数は停止できますが、 Nat.rec は、増加するインデックスが関数の引数であるため適用することができません。ここでは、再帰呼び出しのたびに減少する停止のための測度がありますが、この測度自体は関数の引数ではありません。このような場合、 well-founded recursion を使って関数を定義することができます。整礎再帰は、何かしらの測度が減少する再帰関数を、測度の簡約のすべての列が最終的に最小値で終了する証明上に定義される再帰関数へと体系的に変換する技術です。整礎再帰によって定義された関数適用とその戻り値と必ずしも definitionally equal とは限りませんが、この等しさは命題として証明することができます。definitionally equal である場合であっても、これらの関数はしばしば非常に大きい証明項を簡約する必要があるため、計算に時間がかかることが多いです。

空でない値域での部分関数: 多くのアプリケーションでは、特定の関数の実装を推論することは重要ではありません。ある再帰関数は、証明の自動化ステップの実装の一部としてのみ使用されるかもしれず、形式的に正しいことが証明されることのない普通のプログラムかもしれません。このような場合、Lean のカーネルは definitional equality と propositional equality の成立を必要としません；健全性が維持されていれば十分とします。 Lean.Parser.Command.declaration : commandpartial とマークされた関数は、カーネルによって不透明な定数として扱われ、展開も簡約もされません。健全性を保つために必要なことはその戻り値が存在することです。部分関数は通常通りコンパイルされたコードで使用することができ、命題や証明に出現させることができます；これらの Lean の論理における等価性の理論は非常に弱いものになります。

安全ではない再帰定義: 安全ではない定義には部分定義のような制限はありません。一般的な再帰を自由に使用することができ、キャストのためのプリミティブ（ unsafeCast ）・ポインタの等価性のチェック（ ptrAddrUnsafe ）・ reference counts の観察（ isExclusiveUnsafe ）など、Lean の等価理論の仮定を破る機能を使用することができます。しかし、安全ではない定義を参照する任意の宣言は、それ自身が Lean.Parser.Command.declaration : commandunsafe とマークされなければならず、これによってその定義は論理的な健全性が保証されていないことが明確になります。安全ではない操作は、カーネルがもとの定義を使用したまま、コンパイルされたコードで他の関数の実装をより効率的な変種に置き換えるために使用できます。置換された関数は、その関数名が論理内で自明な等価の理論を持つ不透明なものになるか、その関数がその論理内で使われる場合には普通の関数となります。この機能を使用する際には注意が必要です：論理的な健全性は損なわれませんが、安全でない実装が正しくない場合、Lean で記述されたプログラムの動作が検証済みの論理モデルと乖離する可能性があります。

エラボレータの出力の概要で説明したように、再帰関数のエラボレーションは2つのフェーズで進行します：

定義は Lean のコア型理論に再帰定義があるかのようにエラボレートされます。再帰の使用とは別に、この仮定義は完全にエラボレートされます。コンパイラはこの仮定義からコードを生成します。

停止性の分析では、4つの技法を使って Lean のカーネルに関数を正当化しようとします。定義が Lean.Parser.Command.declaration : commandunsafe または Lean.Parser.Command.declaration : commandpartial とマークされている場合、この技法が使用されます。明示的な Lean.Parser.Command.declaration : commandtermination_by 句が存在する場合、指定された技法のみが試みられます。この句がない場合、エラボレータは探索を実行し、構造的再帰の候補として関数への各パラメータをテストし、各再帰呼び出しで減少する整礎関係を持つ測度を見つけようとします。

本節では再帰関数を支配する規則について説明します。相互再帰についての記述の後に、4種類の再帰定義それぞれについて、推論の機能性と柔軟性のトレードオフについて説明します。