再帰データ型

コンピュータプログラミング言語において、再帰データ型（再帰的に定義された、帰納的に定義された、または帰納的データ型とも呼ばれる）は、同じ型の他の値を含むことができる値のデータ型です。再帰型のデータは通常、有向グラフとして表示されます^{[引用が必要]}。

コンピュータ サイエンスにおける再帰の重要な応用は、リストやツリーなどの動的データ構造の定義です。再帰データ構造は、実行時の要件に応じて任意の大きさに動的に拡大できます。対照的に、静的配列のサイズ要件はコンパイル時に設定する必要があります。

必ずしも再帰的ではない 代数データ型に対して、「帰納的データ型」という用語が使用されることがあります。

例として、Haskellのリスト型を挙げます。

データリストa = Nil | Cons a (リストa )         

これは、a のリストが空のリストであるか、または'a' (リストの「先頭」) と別のリスト (「末尾」) を含む コンス セルであることを示します。

もう 1 つの例は、Java の同様の単一リンク型です。

クラス List < E > { E値; List < E >次; } 
     
     

これは、E 型の空でないリストに、E 型のデータ メンバーと、リストの残りの部分に対する別の List オブジェクトへの参照 (または、これがリストの終わりであることを示す null 参照) が含まれていることを示します。

データ型は相互再帰によって定義することもできます。この最も重要な基本的な例はツリーです。これはフォレスト (ツリーのリスト) の観点から相互再帰的に定義できます。記号的には次のようになります。

f: [t[1], ..., t[k]]
t: ヴフ

フォレストf はツリーのリストで構成され、ツリーt は値vとフォレストf (その子)のペアで構成されます。この定義は簡潔で、抽象的に扱いやすいです (ツリーの特性に関する定理を証明する場合など)。ツリーを単純な言葉 (1 つのタイプのリストと 2 つのタイプのペア) で表現しているからです。

この相互再帰定義は、フォレストの定義をインライン化することで単一再帰定義に変換できます。

t: v[t[1], ..., t[k]]

ツリーt は、値vとツリーのリスト (その子) のペアで構成されます。この定義はより簡潔ですが、やや複雑です。ツリーは、あるタイプのペアと別のタイプのリストで構成され、結果を証明するにはそれらを分離する必要があります。

標準MLでは、ツリーとフォレストのデータ型は次のように相互に再帰的に定義され、空のツリーが許可されます。^[1]

データ型 'a  tree  =  Empty  |  'a * 'a forestのノード と'a forest = Nil | 'a tree * 'a forestの短所    
                 

Haskell では、ツリーとフォレストのデータ型を同様に定義できます。

データツリーa =空|ノード( a 、フォレストa )    
                

データフォレストa = Nil | Cons (ツリーa ) (フォレストa )    
                   

型理論では、再帰型の一般形式は μα.T です。ここで、型変数α は型 T に現れることがあり、型全体を表します。

たとえば、自然数 (ペアノ算術を参照) は、Haskell データ型によって定義されます。

データNat =ゼロ| Succ Nat      

型理論では、次のように言えます。ここで、和型の 2 つのアームはZero と Succ のデータ コンストラクターを表します。Zero は引数を取らず (したがって単位型で表される)、Succ は別の Nat (したがって の別の要素) を取ります。 ${\displaystyle nat=\mu \alpha .1+\alpha }$${\displaystyle \mu \alpha .1+\alpha }$

再帰型には、いわゆる等再帰型と等再帰型の 2 つの形式があります。この 2 つの形式は、再帰型の項の導入方法と削除方法が異なります。

等再帰型では、再帰型とその展開（または展開）（表記は、すべての Z のインスタンスが X 内の Y に置き換えられることを示します）は、通常rollおよびunrollと呼ばれる特殊な用語構成を持つ異なる（かつ互いに素の）型であり、それらの間で同型を形成します。正確には、および、およびは、これら 2 つが逆関数です。 ${\displaystyle \mu \alpha .T}$${\displaystyle T[\mu \alpha .T/\alpha ]}$${\displaystyle X[Y/Z]}$${\displaystyle roll:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T}$${\displaystyle unroll:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]}$

等再帰ルールでは、再帰型とその展開は同等です。つまり、これら 2 つの型式は同じ型を表すと理解されます。実際、等再帰型の理論のほとんどはさらに進んで、基本的に同じ「無限展開」を持つ 2 つの型式は同等であると規定しています。これらのルールの結果、等再帰型は、等再帰型よりも型システムに大幅に多くの複雑さをもたらします。型チェックや型推論などのアルゴリズムの問​​題も、等再帰型ではより困難です。等再帰型では直接比較は意味をなさないため、O(n log n) 時間で標準形式に変換でき、簡単に比較できます。^[2]${\displaystyle \mu \alpha .T}$${\displaystyle T[\mu \alpha .T/\alpha ]}$

等再帰型は、名目上のオブジェクト指向プログラミング言語に見られる自己参照型（または相互参照型）の定義の形式をとっており、オブジェクトとクラスの型理論的意味論にも現れています。関数型プログラミング言語では、等再帰型（データ型の形で）も一般的です。^[3]

TypeScriptでは、型エイリアスでの再帰が許可されています。^[4]したがって、次の例は許可されます。

Tree = number | Tree []と入力します。tree : Tree = [ 1 , [ 2 , 3 ]]とします。     
      

ただし、 Miranda、OCaml (フラグが使用されている場合、またはレコードまたはバリアントである場合を除く)、または Haskellの型シノニムでは再帰は許可されません-rectypes。そのため、たとえば次の Haskell 型は不正です。

型Bad = ( Int , Bad )型Evil = Bool -> Evil    
     

代わりに、代数データ型内にラップする必要があります (コンストラクターが 1 つしかない場合でも)。

データGood = Pair Int GoodデータFine = Fun ( Bool -> Fine )     
      

これは、C のtypedefのような型シノニムが、コンパイル時にその定義に置き換えられるためです。(型シノニムは「実際の」型ではなく、プログラマーの便宜のための単なる「エイリアス」です。) ただし、これを再帰型で実行しようとすると、エイリアスが何度置き換えられてもエイリアスは依然としてそれ自体を参照するため、無限ループが発生します。たとえば、「Bad」は無限に大きくなります: Bad→ (Int, Bad)→ (Int, (Int, Bad))→ ...。

別の見方をすると、等再帰型システムがロールとアンロールのタイミングを判断できるようにするには、間接レベル (代数データ型) が必要であるということです。

• 再帰定義
• 代数データ型
• 誘導型
• ノード（コンピュータサイエンス）

• Harper, Robert (1998)、データ型宣言、1999-10-01 にオリジナルからアーカイブ