Интуиционистская лемма Цорна
Как известно, в интуиционистских теориях типов определимы только вычислимые тотальные `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
Разумеется, мы можем записать вот такой тип:
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