Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Интуиционистская лемма Цорна

Как известно, в интуиционистских теориях типов определимы только вычислимые тотальные `f : A -> B`. Теория типов не утверждает, что внутри типа функций `A -> B` не живёт ещё каких-нибудь (невычислимых) функций, но вот конкретно предьявить можно только тотально-вычислимые. А это означает, что у нас не может быть Тьюринг-полноты, т.е. как бы не была совершенна наша конкретная интуиционистская теория типов, найдутся такие (Тьюринг-)вычислимые функции из `A` в `B`, которые мы не сможем выразить термом `f : A -> B`. Тем не менее, в некоторых интуиционистских теориях типов, поддерживающих индуктивно-индуктивные фактортипы (гомотопическая теория типов и её близкие родственники) можно определить монаду ℧ частично-вычислимых функций, т.е. функций, которые могут в процессе вычисления значения “зависнуть”. И тут уж верно, что термом `f : A -> ℧(B)` можно выразить любую вычислимую функцию из `A` в `B`. Но этот тип, разумеется, содержит кроме тотально-вычислимых функций ещё и функции, которые на каких-то аргументах могут зависать.[1]

Разумеется, мы можем записать вот такой тип:
Property Totality[on f : X -> ℧(Y)]:
  ∀x : X, f(x) ≠ ⊥
Разумеется было бы прикольно иметь оператор
totalize(f : X -> ℧(Y) with Totality) : X -> Y
Правильно ли я понимаю, существование такого оператора это в точности интуиционистская Лемма Цорна?

(NB: Без закона исключённого третьего, из Леммы Цорна никак не доказываются Аксиома Выбора и её эквиваленты.[2])

(NB: Разумеется, наличие такого оператора “небесплатно”. Как минимум, его наличие превращает разрешимость проверки доказательств в полуразрешимость. Но вполне возможно, что оно ещё как-нибудь хитро ломает вычислимость.)

[1] https://arxiv.org/abs/1610.09254
[2] John L. Bell, “Some New Intuitionistic Equivalents of Zorn’s
Lemma”, http://publish.uwo.ca/~jbell/Some%20New%20Intuitionistic%20Equivalents%20of%20Zorn.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.
  • 5 comments