| [Tags | | | algebra, computer science, denotational semantics, domain theory, formal analysis, karl popper, logic, math, memuar, philosophy, pointless topology, programming languages, theoretical computer science, theory of science, topology | ] |
| [ | Current Mood |
| |  sore | ] |
| [ | Current Music |
| | Leonard Cohen - Songs by Leonard Cohen | ] |
Cтивен Викерс
Топология через логику
1989
Я решил все-таки закончить разбирать книгу Джонстона «Пространства Стоуна». Последняя глава там посвящена топологическим решеткам. Вначале я не понимал к чему тут эта глава? Но в предпоследней главе появились профинитные решетки или решетки с тополгией Стоуна. Поэтому я решил все же разобрать эту главу. Там началась тема с топологией Скотта. А она была в самом начале. И я решил повторить. Но я решил использовать это как повод прочить книгу Стивена Викерса «Топология через Логика».
Эта книга была написана как введение в топологию для программистов. Поэтому набор тем там довольно специфический. И она меня давно интриговала. Эта книга фокусируется на приложениях теории Доменов, то есть к формальному анализу программ и денотационной семантики. Тон в этой книге довольно дружелюбный вначале. Поэтому я начал читать ее как роман, и дочитал до конца. Благо он не длинная. Но потом ее содержание тоже становится довольно забористой. Поэтому я разобрал те страницы, которые мне казались полезными. А теорию доменов не стал глубоко разбирать, потому что не очень понимаю, где ее дальше применять. Вряд ли я в ближайшие время, я еще вернусь к этой книге. Поэтому, я расскажу сейчас про то интересное, что я там видел.
читать дальше
Главная идея тут в том, что открытые множества — это полуразрешимые утверждения. Это значит, что если элемент лежит в открытом множестве, то это можно подтвердить за конечное число вычислений, но если он не принадлежит этому открытому множеству то необязательно это можно опровергнуть за конечное число вычислений. Например, возьмем открытый интервал
(0, 1) и число с десятичной записью 0.(9). Тогда, прочтя только конечное число цифр нельзя сделать вывод о принадлежности этого числа интервала. С другой стороны, у любого числа в интервале (0,1) будет десятичная запись с нулевой целой частью, и хотя бы одно не-девяткой дальше. Открытозамкнутые множества — это соответственно разрешимые (вычислимые) утверждения. Важность пространств Стоуна проистекает из того, что их топологии полностью порождены открыто замкнутыми множествами, то есть любое полурарзрешимое утверждение приближается разрешимыми снизу.
Викерс замечает, что для торологии естественными являются не все логические операции, а только конечные конъюнкции и произвольные дизъюнкции. Он называют такую логику логикой конечных (эмперических) наблюдений. При этом можно выделить афирмативные и рефьютативные высказывания. Афирмативные высказывания это ровно те утверждения, которые можно подтвердить за конечное время тогда ил только тогда, когда они верны. То есть это открытые множества. А рефьютативные — это соответственно замкнутые. В этом месте Викерс ссылается на Карла Поппера, который утверждал, что любая теория, чтобы быть научной, должна быть рефьютативной. Вот так мы нашли мостик между функциональным программированием и философией науки Карла Поппера. А еще это мостик к теории топосов! Потому что эта логика называется пропозиционной геометрической логики, и это часть геометрической логики первого порядка, логики топосов!
Главный модельный пример в этой книге это логика потоков битов. Эта логика порождается утверждениями типа в потоке не менее «n битов и бит номер n имеет значение 0» или «n битов и бит номер n имеет значение 0». В итоге получается топология множества последовательностей нулей и единиц, возможно пустых, возможно счетно-бесконечных. Там есть естественный порядок типа «продолжает». Эта конструкция называется Системой Кана или пространством Кана.
Кстати, Викерс активно использует бессмысленную, бесточечную топологию. Но чтобы сбалансировать точечный и бесточечный взгляд, Викерс вводит новую структуру, которую называет топологической системой. Топологическая система состоит из множества точек, моделей или программ, фрейма (пропозиционной геометрической логики) формальных открытых элементов, наблюдений, измерений или теорий, и бинарного отношения между ними типа «возможно при наблюдении» или " моделирует теорию» с аксиомами похожими на аксиомы топологии. В случае обычных топологических пространств, это бинарное отношение соответствует принадлежности точки множеству. Но, например, для топологии Кана, вместо потомков битов в качестве обобщенных точек можно брать программы, которые их выводят. Тогда существуют различные программы, которые выводят одинаковые последовательности бит.
Для формальных точек топологической системы можно ввести предпорядок, который называется порядком специализации. Одна точка является специализацией другой точки, если эта точка возможна при любом наблюдении, при котором возможна первая точка. В системе Кана это ровным счетом и есть отношение «продолжает». Этот предпорядок будет частичным порядком если выполняется аксиома отделимости Т0. Но хаусдорффовых систем порядок специализации всегда тривиальный. Поэтому далее Викерс концентрируется на не-хаусдорфовых системах с отделимостью Т0. Для упорядоченного множества можно ввести топологию Скотта, состоящая из замкнутых вверх множеств, недостижимых для направленных объединений. Встает вопрос: в каких топологических системах топология скота отношения специализации соответствует исходной? Вначале Викерс определяет когерентные системы, как системы, топология в которых порождена компактными открытыми множествами. Это то же самое, что фреймы в алгебраической презентации которых нет бесконечных дизъюнкций. Или что топология устроена как множество идеалов дистрибьютивной решетки.
Алгебраическими называются когерентные топологические системы, в которых любой компактный открытый представляется как конечное произведение ко-простых компактных открытых. Алгебраические топологические системы — это именно те системы, топология которых — топология Скотта порядка специализации их точек. То, есть для таких структур нет разницы думать о них как о топологических пространствах или как об упорядоченных пространствах. Мне не очень нравится термин «алгебраический», кажется, что лучше было бы называть такие системы атомарными или целостными. Понятно, что все бесконечные пространства геометрии и анализы не будут алгебраическими в этом смысле. Но алгебраической будет, например, система Кана.
Эти особые алгебраические системы являются предметом теории доменов. Теория доменов пытается найти методы формального анализа компьютерных программ, основанных на моделировании пространства компьютерных программ как топологического пространства. Основная идея в том, чтобы смоделировать это пространство как такое компактное топологическое пространство, что множество его автоморфизмов с открыто-замкнутой топологией вкладывается в него самого. На первый взгляд звучит весьма дико. Но, опять рассмотрим систему Кана. Ее автоморфизмы будут вычислимыми функциями, и можно представить, что каждая из них задается программой, которая в свою очередь записывается как конечная последовательность бит и так вкладывается в пространство Кана. И, наверное, это будет непрерывно. У этого есть несколько следствий. Во первых благодаря компактности у каждой программы будет неподвижная точка. Это ведет к идеи комбинаторов в функциональном программировании. То есть, если и не сама эта книга, то связанное с ней направление мысли повлияло на современные функциональные языки программирования типа Хаскелла и Раста. Во вторых значит, что программы могут принимать на вход другие программы и выдавать другие программы. В целом я не очень глубоко углублялся в эту тему. Викерс идет тут намного глубже и обсуждает домены множеств, что имеет определенное сродство с идеей пространства компактных подмножеств с метрикой Хаусдорффа в обычной топологии. Нужно сказать, что после выхода этой книги теория доменов активно развивалась. Появилась синтетическая теория доменов, которая активно использует теорию топосов.
В последней главе Викерс обсуждает связи с абстрактной алгеброй. Это не просто так, потому что спектральные пространства алгебраической геометрии обычно тоже когерентные и не Хаусдорфовы. Есть теорема Хохстера о том, что любое компактное когерентное пространство является спектром коммутативного кольца. И мы встречаем обычные определения спектров Зарисского и Пирса. Мы уже видели, что эти пространства будут когерентными и компактными. И любое когерентное компактное пространство будет спектром Зарисского какого-то коммутативного кольца. Интересно, когда спектр Зарисского будет алгебраическим в вышеприведенном смысле. Интересно, когда спектра Зарисского будет алгебраическим в приведенным выше смысле? Наверное, если кольцо является Артиновым. Но Викерс идет дальше, и рассказывает про матричный спектр Конна для некоммутативного кольца. Я так понял проблема с этим спектром в том, что он не функтореален. И там нельзя также легко перейти от некоммутативных колец к окольцованным пространствам. Но в целом я не очень понимаю зачем Викерса про это пишет после теории доменов? |
nervous