Очень многим понравилась вводная статья про алгебраические типы данных, её вот даже перевели: 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), там много и очень-очень хорошо. Читайте на здоровье!
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
