Rekurzív adattípus

A programozási nyelvekben a rekurzív adattípus (angolul: recursive data type vagy inductive data type) olyan értékek adattípusa, amelyek tartalmazhatnak más, azonos típusú értékeket. A rekurzív típusokkal rendelkező adatok általában irányított gráfként vannak szemléltetve.

A számítástechnikában a rekurzió fontos alkalmazása a dinamikus adatszerkezetek, például a listák és a fák meghatározása. A rekurzív adatszerkezetek dinamikusan tetszőlegesen nagyra nőhetnek a futásidejű követelmények függvényében; ezzel szemben egy statikus tömb méretkövetelményeit a fordítási időben kell meghatározni.

Néha az „induktív adattípus” (inductive data type) kifejezést használják olyan algebrai adattípusokra (ADT), amelyek nem feltétlenül rekurzívak.

Példa

Egy példa a Haskell listatípusa:

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

Ez azt jelzi, hogy az a-k listája vagy üres lista, vagy egy cons cella amely egy a-t (a lista „feje”) és egy másik listát (a „farok”) tartalmaz.

Egy másik példa egy hasonló, egyszeresen összekapcsolt típus a Java-ban:

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

Ez azt jelenti, hogy az E típusú nem üres lista tartalmaz egy E típusú adattagot, valamint egy hivatkozást egy másik listaobjektumra a lista többi részéhez (vagy null pointert, amely jelzi, hogy ez a lista vége).

Kölcsönösen rekurzív adattípusok

Az adattípusok kölcsönös rekurzióval is meghatározhatók. Ennek legfontosabb alappéldája a fa, amely kölcsönösen rekurzív módon definiálható „erdőként” (fák listája). Szimbolikusan:

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

Az f erdő a fák listájából áll, míg a t fa egy v érték és egy f erdő (ennek gyermekei) párból áll. Ez a definíció elegáns és könnyen használható elvont módon (például a fák tulajdonságaira vonatkozó tételek bizonyításakor), mivel egy fát egyszerű kifejezésekkel fejez ki: egy adott típus listája, és két típus párja.

Ez a kölcsönösen rekurzív definíció átalakítható egyszeri rekurzív definícióvá az erdő definíciójának beillesztésével:

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

A t fa egy v érték párból és egy fák listájából (gyermekeiből) áll. Ez a definíció tömörebb, de némileg zavarosabb: egy fa egy adott típus, és egy másik típus listájából álló pár, amelyek szétválasztása szükséges az eredmények bizonyításához.

SML-ben a fa és erdő adattípusok kölcsönösen rekurzív módon definiálhatók az alábbiak szerint, lehetővé téve az üres fákat:^[1]

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

Haskellben a fa és az erdő adattípusai hasonlóan definiálhatók:

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

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

Elmélet

A típuselméletben a rekurzív adattípus általános alakja μα.T ahol az α típusváltozó megjelenhet a T típusban, és magát a teljes típust jelöli.

Például a természetes számokat (lásd Peano-aritmetika) a Haskell adattípus így határozhatja meg:

data Nat = Zero | Succ Nat

A típuselméletben ezt mondanánk: ${\displaystyle nat=\mu \alpha .1+\alpha }$ ahol az összegtípus két ága a Zero és a Succ adatkonstruktort jelöli. A Zero nem fogad el argumentumokat (tehát az egységtípust képviseli), a Succ pedig egy másik Nat-ot fogad (tehát a ${\displaystyle \mu \alpha .1+\alpha }$ egy másik elemét).

A rekurzív típusoknak két formája van: az úgynevezett izorekurzív típusok és ekvirekurzív típusok. A két forma abban különbözik, hogy a rekurzív típusok kifejezései hogyan kerülnek bevezetésre és felszámolásra.

Izorekurzív típusok

Izorekurzív típusoknál a ${\displaystyle \mu \alpha .T}$ rekurzív típus és annak kiterjesztése (vagy kibontása ) ${\displaystyle T[\mu \alpha .T/\alpha ]}$ (ahol ${\displaystyle X[Y/Z]}$ azt jelzi, hogy a Z minden előfordulása Y-ra van cserélve X-ben) különálló (és diszjunkt) típusok speciális kifejezésekkel, amelyeket általában roll és unroll nevekkel illetnek, és amelyek izomorfizmust alkotnak közöttük. Pontosabban: ${\displaystyle roll:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T}$ és ${\displaystyle unroll:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]}$, és ezek inverz függvények.

Az izorekurzív típusok a névleges Objektumorientált programozási nyelvekben megfigyelhető önhivatkozó (vagy kölcsönösen hivatkozó) típusdefiníciók formáját ragadják meg, és az objektumok és osztályok típuselméleti szemantikájában is előfordulnak. A funkcionális programozási nyelvekben is gyakoriak az izorekurzív típusok (adattípusok formájában).^[2]

Ekvirekurzív típusok

Az ekvirekurzív szabályok szerint a ${\displaystyle \mu \alpha .T}$ rekurzív típus egyenlő a ${\displaystyle T[\mu \alpha .T/\alpha ]}$ kibontással – vagyis ez a két kifejezés ugyanazt a típust jelenti. Valójában a legtöbb ekvirekurzív típuselmélet ennél tovább megy, és lényegében meghatározza, hogy bármely két azonos "végtelen kiterjesztésű" típuskifejezés egyenértékű. E szabályok eredményeként az ekvirekurzív típusok lényegesen nagyobb komplexitással járulnak hozzá egy típusrendszerhez, mint az izorekurzív típusok. Az algoritmikus problémák, mint például a típusellenőrzés és a típuskövetkeztetés, szintén nehezebbek az egyenes-kurzív típusok esetében. Mivel a közvetlen összehasonlításnak nincs értelme egy ekvirekurzív típuson, ezért O(n log n) idő alatt átalakíthatók egy kanonikus formába, amely könnyen összehasonlítható.^[3]

Rekurzív adattípusok szinonimái

A TypeScript típus-aliasában megengedett a rekurzió,^[4] például így:

type Tree = number | Tree[];
let tree: Tree = [1, [2, 3]];

A rekurzió azonban nem megengedett Mirandában, OCamlben (kivéve -rectypes jelzővel, vagy rekord vagy változat esetén) és Haskell típusszinonimákban; így például a következő Haskell típusok illegálisak:

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

Ehelyett ezt egy algebrai adattípusba kell csomagolni (még akkor is, ha csak egyetlen konstruktora van):

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

Ennek oka, hogy a típusszinonimák, például a C-ben használt typedef-ek, fordítási időben helyettesítődnek a definíciójukkal (a típusszinonimák nem „valódi” típusok, csak „aliasok” a programozó kényelme érdekében). Ha ezt egy rekurzív típussal próbáljuk meg, akkor végtelen ciklusba fog kerülni, mert függetlenül attól, hogy hányszor helyettesítjük az aliast, az továbbra is önmagára hivatkozik, például a „Bad” a végtelenségig növekedni fog: Bad → (Int, Bad) → (Int, (Int, Bad)) → ...

Másképp úgy is tekinthetjük ezt, hogy egy indirekciós szint (az algebrai adattípus) szükséges ahhoz, hogy az izorekurzív típusrendszer eldöntse, mikor kell becsomagolni (roll) és mikor kell kiterjeszteni (unroll) azt.

Jegyzetek

Fordítás

Ez a szócikk részben vagy egészben a Recursive data type című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.