5.2. 構造的再帰（Structural Recursion）🔗

減少パラメータが関数の名前付きパラメータである場合、その名前を参照して指定することができます。

減少パラメータの名前がシグネチャに無い場合、 Lean.Parser.Command.declaration : commandtermination_by 句でローカルに名前を導入することができます。

減少パラメータは帰納型でなければなりません。 notInductive では、減少パラメータとして関数が指定されています：

cannot use specified parameter for structural recursion:
  its type is not an inductive

減少パラメータが添字付けられた型の族の場合、添字はすべて変数でなければなりません。 constantIndex では、代わりに添字付けられた型の族 Fin' が定数に適用されます：

cannot use specified parameter for structural recursion:
  its type Fin' is an inductive family and indices are not variables
    Fin' 100

減少パラメータの型のパラメータは、変化するパラメータや添字の後に来る関数パラメータに依存してはいけません。 afterVarying では、 fixed 接頭辞 は空です。なぜなら、最初のパラメータ n は変化するため、p は fixed 接頭辞の一部ではないからです：

cannot use specified parameter for structural recursion:
  its type is an inductive datatype
    WithParam' p n
  and the datatype parameter
    p
  depends on the function parameter
    p
  which does not come before the varying parameters and before the indices of the recursion parameter.

以下の例では、減少パラメータ n は入れ子のパターン .succ (.succ n) にマッチします。したがって、 .succ (.succ n) は n の（非厳密な）部分項であり、その結果 n と .succ n はともに厳密な部分項であるため、この定義は受け入れられます。

このことをわかりやすくするために、この例では Nat 固有の書き方である n+1 と n+2 の代わりに .succ n と .succ (.succ n) を使用しています。

以下の例では、減少パラメータ n は Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match 式の直接の 判別子 ではありません。したがって、 n' は n の部分項とはみなされません。

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    half n'

整礎再帰 を使うことで、判別子をマッチのパターンに明示的に結び付けることで、この定義は許容されます。

同様に、以下の例は失敗します： xs.tail は xs の厳密な部分項に簡約されるにもかかわらず、上記の規則によりこの事実を Lean が見ることができません。具体的には、 xs.tail は xs の厳密な部分項に対して definitionally equal ではありません。

停止性を証明するために使用される戦略の重要な帰結は、 2つの 判別子 の同時マッチはペアのマッチと同等ではない ということです。同時マッチは判別子とパターンの間の繋がりを維持し、その Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match における期待される型と同様に、ローカルコンテキストにおける仮定の型を絞り込むことを可能にします。基本的に、 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match に対するエラボレーションの規則では判別子を特別に扱っており、プログラムの実行時の意味を保持する方法で判別子を変更してもコンパイル時の意味が保持されるとは限りません。

2つの自然数の最小値を求めるこの関数は、最初のパラメータに対する構造的再帰によって定義されます：

両方のパラメータに対する同時マッチをペアのマッチに置き換えると停止分析が失敗します：

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    min' n' k'

これは、狭義により小さな引数の値への再帰呼び出しをマッチさせる際に、分析がパラメータの直接的なパターンマッチしか考慮しないためです。判別子をペアで包むと、そのつながりが断ち切られます。

ペアの2つの成分の最小値を求めるこの関数は、構造的再帰によってエラボレートすることができません。

failed to infer structural recursion:
Cannot use parameter nk:
  the type Nat × Nat does not have a `.brecOn` recursor

これは、パラメータの型 Prod が再帰的ではないからです。したがって、そのコンストラクタにはパターンマッチで公開できる再帰的なパラメータはありません。

しかし、この定義は 整礎再帰 を使うことで受け入れられます：

countdown の再帰的な出現が減少パラメータの厳密な部分項ではない項に適用されているにもかかわらず、以下の定義は許容されます：

これは n' + 0 が、 n の厳密な部分項である n' と definitionally equal であるからです。パターンマッチで得られる 部分項 は、definitional equality を考慮している マッチの一般化 の規則を用いて 判別子 に接続されます。

countdown' において、その再帰的な出現は 0 + n' に適用されますが、自然数の足し算は第2引数に対して構造的再帰であるため n' に definitionally equal ではありません：

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    countdown' (0 + n')

以下の例は非相互帰納データ型に対する相互再帰を示しています：

以下の例は相互帰納型に対する相互再帰を示しています。関数 Exp.size と App.size は相互再帰的です。

App.numArgs の定義は、 App 型に対して構造的再帰です。これは相互グループ内のすべての帰納型を処理する必要がないことを示しています。

Lean は関数 half が構造的再帰であることを自動的に推論します。 termination_by? 句を使用すると、推論された停止注釈が表示され、ワンクリックでソースファイルに自動的に追加されます。

Try this: termination_by structural x => x

自然数の足し算は、第2引数に対する再帰によって定義することができます。この関数は単純な構造的再帰です。

Nat.rec を使って定義すると、多くの人が慣れ親しんでいる表記からかけ離れています。

関数パラメータの直接の子要素ではないデータに対して行われる構造的再帰呼び出しには、創造性か、複雑ですが体系的なエンコーディングのどちらかが必要です。

この関数についての1つの考え方は、呼び出すたびにビットを反転させ、ビットがセットされたときだけ結果をインクリメントする構造的再帰です。

[0, 0, 1, 1, 2, 2, 3, 3, 4]

創造性の代わりに、 累積再帰 （course-of-values recursion）と呼ばれる一般的なテクニックを使用することができます。累積再帰では、再帰子で定義されたすべての帰納型に対して体系的に導出できる補助関数を使用します；Lean はこれらを自動で導出します。すべての Nat n に対して、 n.below (motive := mot) 型はすべての k < n に対して mot k 型の値を提供し、繰り返された依存ペア型として表現されます。累積再帰子 Nat.brecOn は関数が任意の小さい Nat に対して結果を使用することを可能にします。これを使用して関数を定義することは不便です：

この関数は Lean.Parser.Command.declaration : commandnoncomputable とマークされていますが、これはコンパイラが累積再帰のコード生成をサポートしていないためです。というのもこれは効率的なコードではなく推論用を意図されたものだからです。しかし、カーネルを関数のテストのために使用することができます：

[0, 0, 1, 1, 2, 2, 3, 3, 4]

必要に応じて half'' の本体で依存パターンマッチを再帰子（具体的には Nat.casesOn ）を使ってエンコードすることもできます：

この定義も動作します。

[0, 0, 1, 1, 2, 2, 3, 3, 4]

しかし、もはや本来の定義からかけ離れ、多くの人にとって理解しにくいものになっています。再帰子は優れた論理的基礎ですが、プログラムや証明を書くには簡単な方法ではありません。

以下の定義は List.below と同等です：

言い換えると、与えられた 動機 に対して、 List.below' はリストのすべての接尾辞に対する動機の実現を含む型です。

より再帰的な引数は直積型の反復をさらに入れ子にする必要があります。例えば、二分木には2つの再帰が出現します。

対応する累積テーブルにはすべてのサブツリーに対する動機の実現が含まれています：

リストと木のどちらについても、brecOn 演算子はコンストラクタごとに1つではなく、1つのケースだけを想定しています。このエースはリストまたは木を、すべての小さい値に対する結果のテーブルと一緒に受け入れます；これにより、このケースは与えられた値に対する動機を満たすべきです。提供された値の依存ケース分析によって、メモテーブルの型が自動的に絞り込まれ、必要なものがすべて提供されます。

以下の定義はそれぞれ List.brecOn と Tree.brecOn に同等です。プリミティブな再帰補助関数 List.brecOnTable と Tree.brecOnTable は最終結果と共に累積テーブルを計算し、実際の brecOn 演算子の定義は単に結果を射影します。

half のエラボレーションを進める最初のステップは、手作業でより単純な形に脱糖することです。これは Lean の動作方法とは一致しませんが、 OfNat インスタンスの数が少なければその出力はずっと読みやすくなります。この読みやすい定義：

は、以下のやや低レベルのバージョンに書き換えることができます：

エラボレータは、再帰はまだ存在するものの、それ以外は Lean のコア型理論に沿った事前定義をエラボレートすることから始めます。コンパイラの事前定義の追跡をオンにすると、プリティプリンタがより明示的になり、その結果事前定義が見えるようになります：

返される追跡メッセージは以下です：

[Elab.definition.body] half : Nat → Nat :=
    fun (x : Nat) =>
      half.match_1.{1} (fun (x : Nat) => Nat) x
        (fun (_ : Unit) => Nat.zero)
        (fun (_ : Unit) => Nat.zero)
        fun (n : Nat) => Nat.succ (half n)

この補助マッチ関数の定義は以下です：

def half.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x :=
fun motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n

より読みやすくフォーマットすると、この定義は以下のようになります：

つまり、 half で使用されるパターンの特定の構成は half.match_1 に取り込まれます。

以下の定義は half の事前定義をより読みやすくしたものです：

この関数を構造的再帰関数として定義するには、まず bRecOn の呼び出しを確立します。この定義は Lean.Parser.Command.declaration : commandnoncomputable とマークしなければなりません。なぜなら Lean は Nat.brecOn のような再帰子のためのコード生成をサポートしていないからです。

次のステップは、もとの関数本体にある x を brecOn が提供する n で置き換えることです。table の型は x に依存するため、 half.match_1 でケースを分割する際にも一般化する必要があり、追加のパラメータを持つ同期となります。

3つのケースのプレースホルダは以下の型を期待します：

don't know how to synthesize placeholder for argument 'h_1'
context:
x n : Nat
table : Nat.below n
⊢ Unit → (fun k => Nat.below k → Nat) Nat.zero

don't know how to synthesize placeholder for argument 'h_2'
context:
x n : Nat
table : Nat.below n
⊢ Unit → (fun k => Nat.below k → Nat) 1

don't know how to synthesize placeholder for argument 'h_3'
context:
x n : Nat
table : Nat.below n
⊢ (n : Nat) → (fun k => Nat.below k → Nat) n.succ.succ

事前定義にある最初の2つのケースは定数関数で、チェックする再帰はありません：

最後のケースには再帰呼び出しが含まれています。これは累積テーブルへの検索に変換されるべきです。最後のホールの型をより読みやすく表現すると次のようになります：

これは以下と同等です：

累積テーブルの最初の Nat は n + 1 に対する再帰の結果であり、2番目は n に対する再帰の結果です。したがって、再帰呼び出しは検索に置き換えることができ、エラボレーションが成功します：

実際のエラボレータは新しい名前を持つ番兵型を動機に挿入することによって、構造的再帰のためにチェックされるパラメータと累積テーブル内での位置との間の関係を追跡します。