Форум программистов, компьютерный форум, киберфорум
Mysterious Light
Войти
Регистрация
Восстановить пароль
Оценить эту запись

Счётность типов

Запись от Mysterious Light размещена 01.05.2014 в 03:45
Обновил(-а) Mysterious Light 25.05.2014 в 00:53 (подправил формат, добавил тип функций, добавил ссылки на литературу)

Счётность

Счётность — это свойство совокупности (типа, множества), которое заключается в потенциальной возможности взаимооднозначного сопоставления каждому объекту некоторого числа — его индекса.

Например, множество чисел от 0 до 65535 не является счётным, оно конечно. А вот множество всех целых чисел очевидно счётно.

Дадим такое определение счётности типа:
Haskell
1
2
3
4
5
6
7
8
9
10
11
type PInteger = Integer
-- здесь и далее полагаю, что PInteger описывает натуральные числа
-- в принципе обычный Integer тоже подойдёт,
-- поскольку мн-во целых чисел равномощно мн-ву натуральных
 
class Countable a where
    indexOf :: a -> PInteger
    valueOf :: PInteger -> a
    -- возлагаем на честность программиста аксиомы
    -- indexOf . valueOf = id
    -- valueOf . indexOf = id
Индекс начинается с 1 для полной ясности, однако это не принципиально.


Арифметика типов

Пусть есть типы 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.

Haskell
1
2
3
4
5
data Maybe a = Just a | Nothing
data Either a b = Left a | Right b
data Pair a = Pair a a
data (,) a b = (,) a b
data MyList a = EmptyList | MyCons a (MyList a) -- полный аналог []
Maybe a = a + 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) с естественными изоморфизмами
Haskell
1
2
3
4
5
6
7
8
9
type Marked a = (Bool, a)
 
either2marked :: Either a a -> Marked a
either2marked (Left x) = (False, x)
either2marked (Right x) = (True, x)
 
marked2either :: Marked a -> Either a a
marked2either (False, x) = Left x
marked2either (True, x) = Right x
Пример со списком:
MyList a = 1 + a * (MyList a) = 1 + a * (1 + a * (MyList a)) = 1 + a + a * a * (MyList a) =
= 1 + a + a * a + a * a * a * (MyList a) = 1 + a + a2 + a3 + a4 * (MyList a) = ...
Это означает не более, чем то, что каждый структурно определённый список имеет конечную длину, которая может быть либо 0, либо 1, либо 2 и т.д., и этому соотв. тип 1, a, a*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 ...
...
Подробнее смотрите http://ru.wikibooks.org/wiki/Теория_...тные_множества (теоремы 2 про произведение, а также можно посмотреть: теорему 8 про добавление конечного числа элементов и теорему 10 про объединение счётного с бесконечным)

Опишим это в коде:
Haskell
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
-- Maybe a = a + 1
instance Countable a => Countable (Maybe a) where
    indexOf = maybe 1 (succ.indexOf)
    valueOf 1 = Nothing
    valueOf x = Just $ valueOf $ pred $ x
 
-- (a,b) = a * b
instance (Countable a, Countable b) => Countable (a,b) where
    indexOf ~(x,y) = let
        xi = indexOf x - 1
        yi = indexOf y - 1
        s  = xi + yi -- номер диагонали
        sp = s * (s + 1) `div` 2
        in sp + yi + 1
    valueOf ind = let
        -- s максимальное такое, что s(s+1)/2 < ind
        s = pred . head . filter (\s -> div (s*(s+1)) 2 > ind - 1) $ [0..]
        s2 = s * (s + 1) `div` 2
        yi = ind - s2
        xi = s - yi + 2
        in (valueOf xi, valueOf yi)
 
-- Either a b = a + b
instance (Countable a, Countable b) => Countable (Either a b) where
    indexOf (Left x)  = 2 * indexOf x - 1
    indexOf (Right x) = 2 * indexOf x
    valueOf ind = if rem ind 2 == 0
        then Right $ valueOf (div ind 2)
        else Left $ valueOf (div ind 2 + 1)

Счётность конечного списка

В свете этого оказывается возможным занумеровать элементы списка от счётного типа. Обратим внимание на то, что
MyList a = 1 + a * (MyList a) = Maybe (a, MyList a)
Это позволит нам перейти от головных форм (которых всего два типа) аргумента-списка [] или (x:xs) к соответствующему аналогу Nothing или Just (x,xs), для которых индексация уже определена, и обратно.
Haskell
1
2
3
4
5
6
7
instance Countable a => Countable [a] where
    indexOf list = indexOf $ case list of
        []     -> Nothing
        (x:xs) -> Just (x,xs)
    valueOf ind  = case valueOf ind of
        Nothing     -> []
        Just (x,xs) -> (x:xs)

Бесконечные списки

Бесконечные списки не образуют счётную совокупность. Это объясняет то, что процедура впадёт в бесконечный цикл.
В действительности же, каждой последовательности чисел можно сопоставить вещественное число от 0 до 1 в десятичной записи (почти взаимооднозначно), а их несчётное количество. Последовательность же счётных объектов не менее объёмна, чем последовательность конечных объектов, так что такая совокупность тоже несчётна.

Всем заинтересовавшимся советую почитать доказательство несчётности [0,1] с использованием алгоритма построение незанумеронанного числа.

P.S. кому интересно поиграться с этим, можете в интерпретаторе написать что-то в духе
Haskell
1
2
3
4
5
6
*Main> map valueOf [1..20] :: [[Integer]]
 
-- это нужно добавить в код
instance Countable Integer where
    indexOf = id
    valueOf = id
Размещено в Структуры данных
Просмотров 608 Комментарии 0
Всего комментариев 0
Комментарии
 
КиберФорум - форум программистов, компьютерный форум, программирование
Powered by vBulletin® Version 3.8.9
Copyright ©2000 - 2020, vBulletin Solutions, Inc.