同値再帰型
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/02/17 16:09 UTC 版)
同値再帰規則では、再帰型 μ α . T {\displaystyle \mu \alpha .T} とその展開結果の T [ μ α . T / α ] {\displaystyle T[\mu \alpha .T/\alpha ]} は「等価」である。ここで等価とは、この2つの型表現が同じ型を表していると理解されることを示す。実際、同値再帰型の理論ではさらに、無限に展開したときに等価となる2つの型表現は等価であるとするのが一般的である。型を木構造で表現したときに、当然であるが、無限の大きさの木構造同士が部分型関係にあるかどうかを有限時間で判定することは不可能である。しかしながら、再帰型の表現方法を正則型に制限すると、部分型関係にあるかどうかを、有限時間で判定出来るアルゴリズムが存在する。そして、そのアルゴリズムの正しさの証明は、無限を厳密に扱うために、余帰納法を使用する。正則型がなんであるかや、判定アルゴリズムとその証明は、書籍『型システム入門』の「第21章 再帰型のメタ理論」で解説されている。 このような規則の結果として、同値再帰型は同型再帰型よりも遥かに複雑な型システムを提供する。型検査のようなアルゴリズム上の問題や型推論も同値再帰型の方が難しい。
※この「同値再帰型」の解説は、「再帰データ型」の解説の一部です。
「同値再帰型」を含む「再帰データ型」の記事については、「再帰データ型」の概要を参照ください。
ウィキペディア小見出し辞書の「同値再帰型」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 同値再帰型のページへのリンク
