Рекурсивний тип даних

У комп'ютерних мовах програмування рекурсивний тип даних (також відомий як рекурсивно визначений, індуктивно визначений або індуктивний тип даних) — тип даних для значень, які можуть містити інші значення того самого типу. Дані рекурсивних типів зазвичай розглядаються як орієнтовані графи.

Важливим застосуванням рекурсії в інформатиці є визначення динамічних структур даних, таких як списки та дерева. Рекурсивні структури даних можуть динамічно збільшуватися до довільно великого розміру у відповідь на вимоги до виконання; на відміну від цього, вимоги до розміру статичного масиву повинні бути встановлені під час компіляції.

Іноді термін «індуктивний тип даних» використовується для алгебричних типів даних, які не обов'язково є рекурсивними.

Приклад

Прикладом є тип списку в Haskell :

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

Це вказує на те, що список a — це або порожній список, або Cons-комірка, що містить «a» («заголовок» списку) та інший список («хвіст»). Інший приклад — подібний однозв'язний тип у Java:

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

Це вказує на те, що непустий список типу E містить елемент даних типу E та посилання на інший об'єкт списку для решти списку (або нульове посилання, яке вказує на те, що це кінець списку).

Взаємно рекурсивні типи даних

Докладніше: Взаємна рекурсія

Типи даних також можна визначити шляхом взаємної рекурсії. Найважливішим базовим прикладом цього є дерево, яке можна визначити взаємно рекурсивно в термінах лісу (список дерев). Символьно:

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

Ліс f складається зі списку дерев, тоді як дерево t складається з пари значення v та лісу f (його нащадків). Це визначення елегантне і з ним легко працювати абстрактно (наприклад, при доведенні теорем про властивості дерев), оскільки воно виражає дерево простими термінами: список одного типу та пара двох типів.

Це взаємно-рекурсивне визначення можна перетворити на однорекурсивне визначення шляхом вбудованого визначення лісу:

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

Дерево t складається з пари значення v та списку дерев (його нащадків). Це визначення є більш компактним, але дещо заплутанішим: дерево складається з пари одного типу та списку іншого, які вимагають розплутування, щоб довести результати.

У Стандартному ML типи дерев та лісів можуть бути взаємно рекурсивно визначені наступним чином, дозволяючи порожні дерева: ^[1]

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

У Haskell типи дерев та лісів можна визначити аналогічним чином:

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

Теорія

У теорії типів рекурсивний тип має загальний вигляд μα.T, де змінна типу α може з'являтися в типі T і означає весь тип.

Наприклад, натуральні числа (див. Арифметику Пеано) можуть бути визначені типом даних в Haskell:

data Nat = Zero | Succ Nat 

У теорії типів ми сказали б: ${\displaystyle nat=\mu \alpha .1+\alpha }$ де дві гілки типу sum представляють конструктори даних Zero і Succ. Нуль не приймає аргументів (таким чином, представлений типом одиниці), а Succ бере інший Nat (таким чином, інший елемент ${\displaystyle \mu \alpha .1+\alpha }$).

Існує дві форми рекурсивних типів: так звані ізорекурсивні типи та еквірекурсивні типи. Ці дві форми відрізняються тим, як вводяться та усуваються терміни рекурсивного типу.

Ізорекурсивні типи

З ізорекурсивними типами — рекурсивним ${\displaystyle \mu \alpha .T}$ та його розширення (або розгортання)${\displaystyle T[\mu \alpha .T/\alpha ]}$ (Де позначення${\displaystyle X[Y/Z]}$ вказує на те, що всі екземпляри Z замінені на Y у X) — це різні типи (які не перетинаються) зі спеціальними терміновими конструкціями, які зазвичай називають roll і unroll (згортати і розгортати) що утворюють між собою ізоморфізм. Якщо бути точним: ${\displaystyle roll:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T}$ і${\displaystyle unroll:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]}$, а ці дві є оберненими функціями.

Еквірекурсивні типи

Відповідно до еквірекурсивних правил, рекурсивний тип ${\displaystyle \mu \alpha .T}$ та його розгортання ${\displaystyle T[\mu \alpha .T/\alpha ]}$ рівні — тобто ці два вирази типу розуміються як один і той же тип. Насправді, більшість теорій еквірекурсивних типів йдуть далі і по суті вказують, що будь-які два вирази типу з однаковим «нескінченним розширенням» еквівалентні. В результаті цих правил еквірекурсивні типи вносять значно більшу складність у систему типів, ніж ізорекурсивні типи. Алгоритмічні проблеми, такі як перевірка типу та висновок типу, є складнішими також для еквірекурсивних типів. Оскільки пряме порівняння не має сенсу для еквірекурсивного типу, їх можна перетворити в канонічну форму за час O (n log n), яку легко порівняти.

Еквірекурсивні типи охоплюють форму самореференційних (або взаємно референційних) визначень типів, що спостерігаються у процедурних та об'єктно-орієнтованих мовах програмування, а також виникають у теоретично-типовій семантиці об'єктів і класів. У функціональних мовах програмування набагато частіше зустрічаються ізорекурсивні типи (під виглядом типів даних).

У синонімах типу

Рекурсія не дозволена в синонімах типів у Miranda, OCaml (якщо не використовується прапорець -rectypes або це запис чи варіант) та Haskell; так, наприклад, такі типи Haskell є незаконними:

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

Натомість його потрібно загортати в алгебричний тип даних (навіть якщо він має лише один конструктор):

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

Це тому, що синоніми типів, як typedefs в C, замінюються їх визначенням під час компіляції. (Синоніми типів не є «справжніми» типами; вони просто «псевдоніми» для зручності програміста.) Але якщо це буде зроблено з рекурсивним типом, воно буде циклічно нескінченне, оскільки незалежно від того, скільки разів псевдонім замінено, він все одно посилається на себе, наприклад, «Bad» буде рости нескінченно довго: Bad → (Int, Bad) → (Int, (Int, Bad)) → ....

Інший спосіб побачити це полягає в тому, що потрібен рівень опосередкованості (алгебричний тип даних) для того, щоб система ізорекурсивного типу могла зрозуміти, коли згортати і розгортати.

Див. також

• Рекурсивне означення
• Алгебричний тип даних
• Вузол (інформатика)

Примітки

1. Harper, 2000, "Data Types".
2. Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types. CiteSeerX 10.1.1.4.2276.

Ця стаття заснована на матеріалі, взятому з [en] до 1 листопада 2008 року та включеному відповідно до умов «реліцензування» GFDL, версія 1.3 або пізнішої.