Счётность типов
Запись от Mysterious Light размещена 01.05.2014 в 03:45
Обновил(-а) Mysterious Light 25.05.2014 в 00:53 (подправил формат, добавил тип функций, добавил ссылки на литературу)
Обновил(-а) Mysterious Light 25.05.2014 в 00:53 (подправил формат, добавил тип функций, добавил ссылки на литературу)
| Счётность Счётность — это свойство совокупности (типа, множества), которое заключается в потенциальной возможности взаимооднозначного сопоставления каждому объекту некоторого числа — его индекса. Например, множество чисел от 0 до 65535 не является счётным, оно конечно. А вот множество всех целых чисел очевидно счётно. Дадим такое определение счётности типа:
Арифметика типов Пусть есть типы A и B. Тогда обозначим A+B тип альтернативу (или A, или B) и A*B тип произведения (пара из компоненты A и компоненты B). Такое обозначение допускает некоторую вольность в реализации, но указывает на структуру типа. Синоним типа имеет ту же структуру, поэтому type MyInt = Integer и newtype MyInt = MyInt Integer говорят о том, что MyInt и Integer имеют одну структуру и мы будем писать MyInt = Integer. Тип из конечного числа вариантов будет обозначаться числом — количеством вариантов. Так, () = 1, Bool = 2, Char = 256 и т.п. В частности, Nothing = [] = 1.
Either a b = a + b Pair a = a * a = a2 (,) a b = a * b MyList a = EmptyList + MyCons a (MyList) = 1 + a * MyList a Да-да, рекурсивный тип порождает рекурсивное равенство. Арифметика типов довольно привычная. В частности, (A + B) + C = A + (B + C) (A * B) * C = A * (B * C) A + B = B + A A * B = B * A (A + B) * C = A * C + B * C 1 * A = A 0 + A = A Например, Either a a = a + a = (1 * a) + (1 * a) = (1 + 1) * a = 2 * a = (Bool, a) с естественными изоморфизмами
MyList a = 1 + a * (MyList a) = 1 + a * (1 + a * (MyList a)) = 1 + a + a * a * (MyList a) = Это означает не более, чем то, что каждый структурно определённый список имеет конечную длину, которая может быть либо 0, либо 1, либо 2 и т.д., и этому соотв. тип 1, a, a*a и т.д.= 1 + a + a * a + a * a * a * (MyList a) = 1 + a + a2 + a3 + a4 * (MyList a) = ... Под структурной определённостью понимается то, что невозможно написать функцию isFinit :: [a] -> Bool, которая бы всегда завершалась и выдавала бы True для конечных и False для бесконечных списков; бесконечные списки не имеют обозримой структуры, поэтому используется такая терминология. Счётность производных типов Пусть A и B счётны, тогда A+1, A+B и A*B также счётны. A+1 счётно просто потому, что можно весь ряд индексов сдвинуть на единицу для того, чтобы в начало добавить один элемент. Этот механизм был подмечен в парадоксе Гильберта о гостиннице (отель Гильберта, см. http://uk.wikipedia.org/wiki/Парадокс_Гільберта). Расположим все элементы A и B в два ряда (напр., используя map indexOf [1..] :: [A]) друг под другом и начнём обходить зигзагом: первый элемент первого ряда, первый второго ряда, второй первого, второй второго, третий первого, третий второго и т.д. Это будет обход A+B. Запишим таблицу A*B и будем обходить её в таком порядке змейкой: Код:
1 2 4 7 11 ... 3 5 8 12 ... 6 9 13 ... 10 14 ... ... Опишим это в коде:
Счётность конечного списка В свете этого оказывается возможным занумеровать элементы списка от счётного типа. Обратим внимание на то, что MyList a = 1 + a * (MyList a) = Maybe (a, MyList a) Это позволит нам перейти от головных форм (которых всего два типа) аргумента-списка [] или (x:xs) к соответствующему аналогу Nothing или Just (x,xs), для которых индексация уже определена, и обратно.
Бесконечные списки Бесконечные списки не образуют счётную совокупность. Это объясняет то, что процедура впадёт в бесконечный цикл. В действительности же, каждой последовательности чисел можно сопоставить вещественное число от 0 до 1 в десятичной записи (почти взаимооднозначно), а их несчётное количество. Последовательность же счётных объектов не менее объёмна, чем последовательность конечных объектов, так что такая совокупность тоже несчётна. Всем заинтересовавшимся советую почитать доказательство несчётности [0,1] с использованием алгоритма построение незанумеронанного числа. P.S. кому интересно поиграться с этим, можете в интерпретаторе написать что-то в духе
| ||||||||||||||||||||||||||||||
Всего комментариев 0
Комментарии
