Rekurencyjny typ danych - Recursive data type

W komputerowych językach programowania , o rekurencyjny typ danych (znany również jako rekursywnie zdefiniowanego , indukcyjnie zdefiniowane lub indukcyjnym typu danych ) to typ danych dla wartości, które mogą zawierać inne wartości tego samego typu. Dane typu rekurencyjnego są zwykle postrzegane jako grafy skierowane .

Ważnym zastosowaniem rekurencji w informatyce jest definiowanie dynamicznych struktur danych, takich jak listy i drzewa. Rekurencyjne struktury danych mogą dynamicznie rosnąć do dowolnie dużego rozmiaru w odpowiedzi na wymagania środowiska wykonawczego; w przeciwieństwie do tego, wymagania dotyczące rozmiaru tablicy statycznej muszą być ustawione w czasie kompilacji.

Czasami termin „indukcyjny typ danych” jest używany dla algebraicznych typów danych, które niekoniecznie są rekurencyjne.

Przykład

Przykładem jest typ listy w Haskell :

data List a = Nil | Cons a (List a)

Oznacza to, że lista a jest albo pustą listą, albo komórką przeciw, zawierającą 'a' ("głowa" listy) i inną listę ("ogon").

Innym przykładem jest podobny typ jednokierunkowy w Javie:

class List<E> {
    E value;
    List<E> next;
}

Oznacza to, że niepusta lista typu E zawiera element członkowski danych typu E oraz odwołanie do innego obiektu List dla reszty listy (lub odwołanie o wartości null wskazujące, że jest to koniec listy).

Wzajemnie rekurencyjne typy danych

Typy danych mogą być również definiowane przez wzajemną rekurencję . Najważniejszym podstawowym przykładem tego jest drzewo , które można zdefiniować wzajemnie rekurencyjnie w kategoriach lasu (lista drzew). Symbolicznie:

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

Las f składa się z listy drzew, natomiast drzewo t składa się z pary o wartości v i lasu f (jego dzieci). Ta definicja jest elegancka i łatwa do pracy z abstrakcją (na przykład podczas dowodzenia twierdzeń o właściwościach drzew), ponieważ wyraża drzewo w prostych słowach: lista jednego typu i para dwóch typów.

Tę wzajemnie cykliczną definicję można przekonwertować na pojedynczą definicję cykliczną, podając definicję lasu:

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

Drzewo t składa się z pary o wartości v oraz listy drzew (jego dzieci). Ta definicja jest bardziej zwięzła, ale nieco bardziej nieuporządkowana: drzewo składa się z pary jednego typu i listy innego, które wymagają rozplątywania, aby udowodnić wyniki.

W Standard ML typy danych drzewa i lasu można wzajemnie rekurencyjnie definiować w następujący sposób, co pozwala na puste drzewa:

datatype 'a tree = Empty | Node of 'a * 'a forest
and      'a forest = Nil | Cons of 'a tree * 'a forest

W Haskell typy danych drzewo i las można zdefiniować w podobny sposób:

data Tree a = Empty
            | Node (a, Forest a)

data Forest a = Nil
              | Cons (Tree a) (Forest a)

Teoria

W teorii typów typ rekurencyjny ma ogólną postać μα.T , gdzie zmienna typu α może występować w typie T i oznacza cały sam typ.

Na przykład liczby naturalne (patrz Arytmetyka Peano ) mogą być zdefiniowane przez typ danych Haskell:

data Nat = Zero | Succ Nat

W teorii typów powiedzielibyśmy: gdzie dwa ramiona typu sum reprezentują konstruktory danych Zero i Succ. Zero nie przyjmuje żadnych argumentów (czyli reprezentowanych przez typ jednostki ), a Succ przyjmuje inny Nat (a więc kolejny element ). ${\ Displaystyle nat = \ mu \ alfa 0,1 + \ alfa}$ ${\ Displaystyle \ mu \ alfa 0,1+ \ alfa}$

Istnieją dwie formy typów rekurencyjnych: tak zwane typy izorekursywne i typy ekukursywne. Te dwie formy różnią się sposobem wprowadzania i eliminowania terminów typu rekurencyjnego.

Typy izokursywne

W przypadku typów izorekursywnych typ rekurencyjny i jego rozwinięcie (lub rozwijanie ) (gdzie notacja wskazuje, że wszystkie wystąpienia Z są zastąpione przez Y w X) są typami odrębnymi (i rozłącznymi) ze specjalnymi konstrukcjami terminów, zwykle nazywanymi roll and unroll , które tworzą między nimi izomorfizm . Aby być precyzyjnym: i , a te dwie są funkcjami odwrotnymi . ${\ Displaystyle \ mu \ alfa. T}$ $T[\mu \alfa .T/\alfa]$ ${\ Displaystyle X [Y/Z]}$ ${\ Displaystyle roll: T [\ mu \ alfa . T / \ alfa ] \ do \ mu \ alfa . T}$ ${\ Displaystyle rozwijać: \ mu \ alfa . T \ do T [ \ mu \ alfa . T / \ alfa ]}$

Typy ekwiwalentne

Zgodnie z regułami equirecursive typ rekurencyjny i jego rozwinięcie są równe — to znaczy, że te dwa wyrażenia typu są rozumiane jako oznaczające ten sam typ. W rzeczywistości większość teorii typów equirecursive idzie dalej i zasadniczo określa, że dowolne dwa wyrażenia typu z tym samym „nieskończonym rozwinięciem” są równoważne. W wyniku tych reguł typy equirecursive przyczyniają się znacznie do większej złożoności systemu typów niż typy izorekursywne. Problemy algorytmiczne, takie jak sprawdzanie typu i wnioskowanie o typie, są również trudniejsze w przypadku typów ekwikursywnych. Ponieważ bezpośrednie porównanie nie ma sensu na typie ekwikursywnym, można je przekształcić w formę kanoniczną w czasie O(n log n), co można łatwo porównać. ${\ Displaystyle \ mu \ alfa. T}$ $T[\mu \alfa .T/\alfa]$

Typy equicursive przechwytują formę samoodnoszących się (lub wzajemnie odwołujących się) definicji typów obserwowanych w proceduralnych i obiektowych językach programowania, a także pojawiają się w semantyce obiektów i klas z teorią typów . W funkcjonalnych językach programowania typy izorekursywne (pod postacią typów danych) są znacznie bardziej powszechne.

W typie synonimy

Rekursja nie jest dozwolona w synonimach typu w Miranda , OCaml (chyba że -rectypesużyto flagi lub jest to rekord lub wariant) i Haskell; więc na przykład następujące typy Haskella są niedozwolone:

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

Zamiast tego musi być opakowany w algebraiczny typ danych (nawet jeśli ma tylko jeden konstruktor):

data Good = Pair Int Good
data Fine = Fun (Bool -> Fine)

Dzieje się tak, ponieważ synonimy typów, takie jak typedefs w C, są zastępowane ich definicją w czasie kompilacji. (Synonimy typu nie są "prawdziwymi" typami; są tylko "aliasami" dla wygody programisty.) Ale jeśli spróbuje się tego użyć z typem rekurencyjnym, będzie zapętlić się w nieskończoność, ponieważ bez względu na to, ile razy alias zostanie podstawiony, nadal odnosi się do siebie, np. „Zły” będzie rósł w nieskończoność: Bad→ (Int, Bad)→ (Int, (Int, Bad))→ ....

Innym sposobem, aby to zobaczyć, jest to, że wymagany jest poziom niebezpośredniości (typ danych algebraicznych), aby umożliwić systemowi typów izorekursywnych ustalenie, kiedy zwijać i rozwijać .

Zobacz też

Uwagi

Ten artykuł jest oparty na materiale zaczerpniętym z bezpłatnego słownika komputerowego on-line sprzed 1 listopada 2008 r. i włączonym na warunkach „ponownego licencjonowania” GFDL w wersji 1.3 lub nowszej.

Languages

In other projects