Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Всё придумано до нас

(Черновик)

Конструктивные системы типов (с индуктивными или индуктивно-рекурсивными определениями типов) очень удобны для представления ординалов. Всякий тип в такой теории по построению снабжен фундированным лексикографическим порядоком. Доступные в теории ординалы суть классы эквивалентности типов по лексикографическому порядку. Все ординалы S < T можно реализовать как refinement-типы T|c "элементы T, лексикографически уступающие фиксированному элементу c".

В теориях типов, снабженных вычислительной интерпретацией, всякий конструктивный тип данных T строится не только с лексикографичесиким порядком ≤ на нём, но и функцией size(t: T*): Nat, сопоставляющая всем термам типа T и их подтермам натуральное число ("размер в памяти"). Если s подтерм терма t и size(t) = size(s) + 1, будем говорить что t формируется из s атомарным преобразованием. Функция size должна удовлетворять следующим двум условиям:
a) size(0_T) = 0, где 0_T нулевой с точки зрения лексикографического порядка элемент T;
б) количество термов меньше любого данного фиксированного размера конечно;
в) для любого терма t: T существует цепочка подтермов t = t_n >...> t_1 > t_0 = 0, таких что size(t_(i + 1)) ≤ size(t_i) + 1 для всех допустимых i.

Будем называть (T, n, size)-рекурсивной программой конструктивную эндофункцию step: T -> T, со свойствами
1) step(n) ≤ x;
2) size(step(n)) ≤ size(n) + 1.

Благодаря свойству 1 функция step имеет неподвижную точку для каждого аргумента. Будем называть (T, ≤, size)-Yкомбинатором комбинатор, находящий для любой такой функции step её неподвижную точку. Доказать существование тотального Yкомбинатора для каждого S=(T, ≤, size) можно просто доказав существование функции H_s(n), вычисляющую максимально-возможный размер множества {n, step(n), step(step(n))..} для каждого n. Нужно отметить, что это множество всегда конечно (потому что рано или поздно step, как уже было сказано, достигает неподвижной точки f = step(f)).

Для типов-перечислений E_k размера k функция H_(E_k)(n) = k, константа. Для типа натуральных чисел Nat очевидно H_Nat(n) = n (любая невозрастающая последовательность, начинающаяся с n становится постоянной за не более чем n шагов).

Рассмотрим тип E_2 * Nat = Nat + Nat, населённого значениями Left(n) и Right(n), причём любое left-значение больше любого right-значения. Тут получается, что кроме шагов по уменьшению параметра, допустим переход от Left(n) к Right(m), однако по условию (2) m не может быть больше n + 1. Несложно увидеть, что самая длинная возможная программа, стартуя с Left(n) (терм размера n) сразу преобразует его в Right(n + 1), а затем (n + 1) раз уменьшает аргумент. Таким образом получается H_(Nat + Nat)(n) = n + 2. В общем случае H_(E_k + Nat)(n) = n + 2k.

В качестве первого нетривиального примера рассмотрим тип пар (Nat, Nat). При использовании тривиального кодирования, size(a, b) = a + b. Функция step по условию (1) не может увеличивать a и не может увеличивать b, не уменьшив при этом a. Другими словами, у нас есть всего два типа шагов: "уменьшить второй элемент пары" и "уменьшить первый элемент пары, возможно с параллельным увеличением второго на 1 или 2 (больше не допускает свойство 2)". Шаг второго типа мы можем произвести не более чем a раз, причём значение второго элемента пары не может стать больше 2a + b, следовательно, шагов первого типа мы можем произвести не более чем 2a + b. итого, мы можем произвести не более чем 3a + b шагов, т.е. не более чем 3n шагов. Итого, H_(Nat, Nat)(n) = 3n.

Попробуем подойти к вопросу систематически: на каждом шаге функция step(x) может повысить размер size(x) на единицу, но ценой перехода из множества T|x во множество T|step(x). То есть H_T(n) = max {H_L(n + 1), L = T|c for some c, size(c) = n}.

Исходя из этого свойства немедленно получаем, что
H_Nat(n) = max {H_(E_n)(n + 1)} = n.

Внутри типа (E_k + Nat) есть термы Left(l: E_k) размера 1 и Right(n: Nat) размера n, стало быть H_(E_k + Nat)(n) = max {n + 1, k}.

Внутри типа T = (Nat + Nat) для каждого размера n есть ровно два терма этого размера: Left(n) и Right(n). Ограничение (Nat + Nat)|Right(n) = E_n, ограничение (Nat + Nat)|Left(n) = (E_n + Nat). Таким образом
H_(Nat + Nat)(n) = max {n + 1, H_(E_n + Nat)(n + 1)} = max {n + 1, n + 2} = n + 2

Внутри типа T = (Nat, Nat) имеется (n + 1) термов размера n: (0, n), (1, n - 1),..,(n, 0). Соответствующие ограничения выглядят как (E_k, Nat).
Стало быть,
H_(Nat, Nat)(n) = max {H_(E_n, Nat)(n + 1), ..} = max {n + 2n} = 3n

В статье A uniform approach to fundamental sequences and hierarchies (Buchholz, Cichon, Weiermann) показывается, что определённые вышеизложенным образом функции образуют иерархию Харди.
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments