Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:
(Черновик, неоформленные мысли)


Напомню, что такое представление Чёрча для натуральных чисел: натуральное число реализуется как функция, действующая на эндофункциях (функциях типа ∀T. T => T).
Функция n отображает f в f.f...f.f (n раз). В случае 0 функция f отображается в id_T.

Сложение чисел в представлении Чёрча это S-комбинатор, умножение композиция, а возведение n в степень m просто применение m к n. В этом смысле запись f^n = n(f) показывает всю красоту и внутреннюю согласованность представления Чёрча. Особенное внимание следует обратить на то, что комбинаторы сложения (S), умножения (композиция) и возведения в степень (аппликация) формируют полный базис лямбда-исчисления, т.ч. в том числе и сами чёрчевы нумералы представимы через эти комбинаторы без всяких абстраций.

В статье [1] автор пытается построить обобщение Черчева представления с натуральных чисел на все рекурсивные ординалы (ведь фон-Неймановское представление натуральных чисел расширяется до представления всех ординалов!).

Интересно, что кроме Чёрчевых нумералов сигнатуру ∀T. (T => T) -> (T => T) имеют комбинаторы стационарных точек. Кроме того известно [3], что имеется счётно-бесконечное неперечислимое множество нестандартных комбинаторов. Напрашивается идея в виде нестандартных комбинаторов стационарной точки представимы все рекурсивные ординалы. Каждый fixed-point-комбинатор F порождает семейство деревьев (обозначим их тип как #F), получающееся в результате применения редукций. Не является ли случайно лексикографический порядок на этом типе данных однозначно определяющим комбинатор?

[Ещё подсказка, как именно представлять ординалы даётся определением 4.5 из [2]:
f^o(m) = max(f^b(f^b(m)) | b < o, size(b) <= f(m + size(o)))]

Если мысля верна, то выйдет что любое типизированное лямбда-исчисление не может типизировать F_o начиная с какого-то ординала o меньше ординала Чёрча-Клини, и это o (при соблюдении пары граничных условий) является proof-theoretic ordinal этой теории типов.

[1] http://www.lfcs.inf.ed.ac.uk/reports/00/ECS-LFCS-00-421/ECS-LFCS-00-421.pdf
[2] http://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/1832-06.pdf
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.
  • 3 comments