5.1. 相互再帰（Mutual Recursion）🔗

再帰定義が定義本体にて定義されている名前を言及する定義であるのと同様に、 相互再帰 （mutually recursive）定義とは互いに再帰的または言及している定義のことです。複数の宣言の間で相互再帰を使用するには、それらを相互ブロック（mutual block）に配置する必要があります。

syntaxMutual Declaration Blocks

相互再帰の一般的な構文は以下です：

command ::= ...
    | mutual
        declaration*
      end

ここで宣言は定義か定理でなければなりません。

相互ブロック内の宣言は、互いのシグネチャにおいてはスコープに含まれませんが、互いの本体ではスコープ内となります。名前がシグネチャのスコープに無いとしても、自動的に束縛された暗黙パラメータとして挿入されることはありません。

相互ブロックスコープ

相互ブロックで定義された名前は、お互いのシグネチャのスコープに入りません。

mutual
  abbrev NaturalNum : Type := Nat
  def n : unknown identifier 'NaturalNum'NaturalNum := 5
end

unknown identifier 'NaturalNum'

相互ブロック外では、この定義は成功します：

abbrev NaturalNum : Type := Nat
def n : NaturalNum := 5

相互ブロックスコープと自動的な暗黙パラメータ

相互ブロックで定義された名前はお互いのシグネチャのスコープに入りません。それにもかかわらず、これらは自動的な暗黙パラメータとして使用することはできません：

mutual
  abbrev α : Type := Nat
  def identity (x : unknown identifier 'α'α) : unknown identifier 'α'α := x
end

unknown identifier 'α'

異なる名前であれば、暗黙パラメータが自動的に追加されます：

mutual
  abbrev α : Type := Nat
  def identity (x : β) : β := x
end

再帰定義のエラボレートは常に相互ブロックの粒度で行われ、そのようなブロックの一部ではない定義ではあたかもそれぞれの定義を囲む単一の相互ブロックがあるかのように扱われます。 Lean.Parser.Term.letrec : termlet rec と Lean.Parser.Command.declaration : commandwhere で導入されたローカル定義はそれらのコンテキストから持ち出され、必要に応じてキャプチャされた自由変数のパラメータを導入し、 Lean.Parser.Command.mutual : commandmutual ブロック内でも別の定義であるかのように扱われます。したがって Lean.Parser.Command.declaration : commandwhere ブロック内で定義された補助関数お互いに、またそれらが出現する定義の両方で相互再帰を使用することができますが、それらの型シグネチャでお互いに言及することはできません。

定義がまだ再帰的のままであるエラボレーションの最初のステップの後、上記のテクニックを使って再帰を翻訳する前に、Lean は相互ブロック内の定義の中から実際に再帰的なあつまりを特定し、それらを別々に依存関係順に処理します。