Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Тоположество, проблема останова и закон исключённого третьего

Очень многим понравилась вводная статья про алгебраические типы данных, её вот даже перевели: http://wizzard0.livejournal.com/86142.html. В процессе обсуждения мне понадобилось объяснить, какое отношение топология имеет к вычислимости; снова. Выкладываю.

Тоположество в информатике возникает с размышлений о (совершенно дискретной) проблеме останова и в конечном итоге приводит к правильной формализации алгоритмов на непрерывных объектах вроде действительных чисел.

Начнём с проблемы останова. Известно, что про многие алгоримы (рекурсивные функции) нельзя заранее выяснить, завершатся они в конечное время или «войдут в бесконечный цикл». Если мы ограничиваемся в работе алгоритмами, которые заведомо выполняются за конечное время, наш мир — категория, где объекты — типы данных (X, Y, ...), а переходы f: X => Y между ними — алгоритмы, вычисляющие результат Y по вводу X за конечное время выполнения |f(x)| < ∞. Т-полные алгоритмы останавливаются не всегда, т.е. если мы хотим формализовать их как отображения, то нужно включить во множество результатов специальное значение ⊥, называемое Undefined или InfiniteLoop, оно кодирует случай когда алгоритм не завершается. Т-полные алгоритмы это таким образом отображения X => Possibly[Y], где Possibly[Y] = Y | ⊥ с дополнительным свойством *, что |f(x)| < ∞ ⇔ f(x) ≠ ⊥. Итак, категория конечных алгоритмов обобщается: добавляются новые объекты Possibly[_] и новые переходы, ограничение на конечность которых имеет другой вид, если их кодомен вида Possibly[_]. Впоследствие мы расширим нашу категорию ещё, впрочем не будем забегать вперёд.

Существует уйма случаев, когда верность какого-то высказывания всегда можно установить за конечное время, а ошибочность может потребовать бесконечности. Так например при сличении действительных чисел, заданных через аппроксимации (напр. как десятичные дроби), различие всегда устанавливается за конечное время, а равенство требует бесконечно долгой проверки. То есть функция сличения a <> b отображает из ℝ×ℝ в Ω = Possibly[⟙].

[Коротенько об отличии классической логики (т.е. с законом исключённого третьего) от конструктивной: отличие состоит в операторе, превращающем доказательство того факта, что a <> b никогда не завершится в доказательство того факта, что a <> b = ⊥. Конструктивно мы этого доказать не можем, т.к. прежде чем a <> b «завершится и выдаст ⊥», должно пройти бесконечное количество времени. Волшебный оператор (известный также как call/cc) позволяет схлопнуть бесконечное количество времени и «получить» результат.]

Знакомый с теоретикомножественной топологией глаз без труда углядит в Ω двухточечное пространство Серпинского и обратит внимание, что множество T(X) всех возможных «алгоритмов» из X в Ω задаёт топологию на X. Когда X определяется как алгебраический тип данных, топология на нём просто дискретная, а вот для коданных (в т.ч. функциональных типов, фактор-типов, вроде действительных чисел) топология может быть далеко не тривиальна. Это наводит на мысль о дополнительном расширении нашей категории! Отныне мы будем допускать в качестве переходов все алгоритмы f: X => Y, которые, будучи скомбинированы c g ∈ T(Y) дают переход gf ∈ T(X). Таким образом мы включаем в наш мир алгоритмы, работающие с действительными числами и другими непрерывными пространствами, которые требуют бесконечно много времени для выдачи абсолютно точного результата, но достигают любой конечной точности за конечное время.

Понял всё это ещё давно Dana Scott, и это имеет прямейшее отношение к взгляду на топологию с операционалистской точки зрения. Для дополнительного чтения по теме, снова приведу ссылочку http://www.cs.bham.ac.uk/~mhe/.talks/EWSCS2012/EWSCS2012.pdf. Глубокий и вдумчивый анализ подходов к топологии с точки зрения теории типов/теории топосов содержится в книжках Пола Тейлора «Practical Foundations of Mathematics» и П. Дж. Скотта с Дж. Ламбеком «Introduction to highter order categorical logic» (обе Cambridge Univ. Press), там много и очень-очень хорошо. Читайте на здоровье!
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