Рекурсивний тип даних
У комп'ютерних мовах програмування рекурсивний тип даних (також відомий як рекурсивно визначений, індуктивно визначений або індуктивний тип даних) — тип даних для значень, які можуть містити інші значення того самого типу. Дані рекурсивних типів зазвичай розглядаються як орієнтовані графи.
Важливим застосуванням рекурсії в інформатиці є визначення динамічних структур даних, таких як списки та дерева. Рекурсивні структури даних можуть динамічно збільшуватися до довільно великого розміру у відповідь на вимоги до виконання; на відміну від цього, вимоги до розміру статичного масиву повинні бути встановлені під час компіляції.
Іноді термін «індуктивний тип даних» використовується для алгебричних типів даних, які не обов'язково є рекурсивними.
Приклад ред.
Прикладом є тип списку в 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
У теорії типів ми сказали б: де дві гілки типу sum представляють конструктори даних Zero і Succ. Нуль не приймає аргументів (таким чином, представлений типом одиниці), а Succ бере інший Nat (таким чином, інший елемент ).
Існує дві форми рекурсивних типів: так звані ізорекурсивні типи та еквірекурсивні типи. Ці дві форми відрізняються тим, як вводяться та усуваються терміни рекурсивного типу.
Ізорекурсивні типи ред.
З ізорекурсивними типами — рекурсивним та його розширення (або розгортання) (Де позначення вказує на те, що всі екземпляри Z замінені на Y у X) — це різні типи (які не перетинаються) зі спеціальними терміновими конструкціями, які зазвичай називають roll і unroll (згортати і розгортати) що утворюють між собою ізоморфізм. Якщо бути точним: і , а ці дві є оберненими функціями.
![{\displaystyle T[\mu \alpha .T/\alpha ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/efbc5122f9ac522ed8a510aa156993f362d194ae)
![{\displaystyle X[Y/Z]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/00989088ec91a5662c617a728e9d8e5095ba39d3)
![{\displaystyle roll:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6b6f8d541d2489945bdb60a01c590421274564d2)
![{\displaystyle unroll:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7c8146ae5a168a59afea5f32932b583a4b67aa17)
Еквірекурсивні типи ред.
Відповідно до еквірекурсивних правил, рекурсивний тип та його розгортання рівні — тобто ці два вирази типу розуміються як один і той же тип. Насправді, більшість теорій еквірекурсивних типів йдуть далі і по суті вказують, що будь-які два вирази типу з однаковим «нескінченним розширенням» еквівалентні. В результаті цих правил еквірекурсивні типи вносять значно більшу складність у систему типів, ніж ізорекурсивні типи. Алгоритмічні проблеми, такі як перевірка типу та висновок типу, є складнішими також для еквірекурсивних типів. Оскільки пряме порівняння не має сенсу для еквірекурсивного типу, їх можна перетворити в канонічну форму за час O (n log n), яку легко порівняти.[2]
Еквірекурсивні типи охоплюють форму самореференційних (або взаємно референційних) визначень типів, що спостерігаються у процедурних та об'єктно-орієнтованих мовах програмування, а також виникають у теоретично-типовій семантиці об'єктів і класів. У функціональних мовах програмування набагато частіше зустрічаються ізорекурсивні типи (під виглядом типів даних).
У синонімах типу ред.
Рекурсія не дозволена в синонімах типів у 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)) → ....
Інший спосіб побачити це полягає в тому, що потрібен рівень опосередкованості (алгебричний тип даних) для того, щоб система ізорекурсивного типу могла зрозуміти, коли згортати і розгортати.
Див. також ред.
Примітки ред.
- ↑ Harper, 2000, "Data Types".
- ↑ Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types. CiteSeerX 10.1.1.4.2276.
Ця стаття заснована на матеріалі, взятому з безкоштовного онлайнового словника обчислювальної техніки[en] до 1 листопада 2008 року та включеному відповідно до умов «реліцензування» GFDL, версія 1.3 або пізнішої.