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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

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

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

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

Приклад

[ред. | ред. код]

Прикладом є тип списку в 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 (згортати і розгортати) що утворюють між собою ізоморфізм. Якщо бути точним: і, а ці дві є оберненими функціями.

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

[ред. | ред. код]

Відповідно до еквірекурсивних правил, рекурсивний тип та його розгортання рівні — тобто ці два вирази типу розуміються як один і той же тип. Насправді, більшість теорій еквірекурсивних типів йдуть далі і по суті вказують, що будь-які два вирази типу з однаковим «нескінченним розширенням» еквівалентні. В результаті цих правил еквірекурсивні типи вносять значно більшу складність у систему типів, ніж ізорекурсивні типи. Алгоритмічні проблеми, такі як перевірка типу та висновок типу, є складнішими також для еквірекурсивних типів. Оскільки пряме порівняння не має сенсу для еквірекурсивного типу, їх можна перетворити в канонічну форму за час 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))....

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

Див. також

[ред. | ред. код]

Примітки

[ред. | ред. код]
  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 або пізнішої.