![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Aug. 9th, 2010
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif){kind=small}
Если кто не знает
Aug. 9th, 2010 05:07 am(Маленький пост из серии “Если кто не знает”)
Существует такой “Язык программирования” под названием Jot, только он называется автором Крисом Бекером не языком программирования собственно, а «a better Gödel-numbering». Это взаимно-однозначный способ кодировать лямбда-выражения строками из единиц и нулей. Система декодирования проще некуда. Пустая строка означает id, т.е. лямбда-выражение [x|x]. Остальные строки последовательно расшифровываются с конца в дерево комбинаторов:
*0 → *SK
*1 → [x|y|*(x(y))].
Напоминаю, что константный комбинатор K = [x|y|x], а комбинатор обобщённого применения S = [x|y|z|x(z)(y(z))]. А Gödel numbering оно потому, что при добавлении к алфавиту из нуля и единицы ряда дополнительных символов, получается способ кодирования произвольных логических высказываний конечными строками символов конечного алфавита. Например для получения интуиционистской логики достаточно добавления символа отрицания, символа импликации и символа равенства. Для получения Observational Type Theory с ZFC-эквивалентной теорией множеств понадобится добавление 7 символов. Π, Σ, W, ⊥, ⊤, Ω, Set.
Существует такой “Язык программирования” под названием Jot, только он называется автором Крисом Бекером не языком программирования собственно, а «a better Gödel-numbering». Это взаимно-однозначный способ кодировать лямбда-выражения строками из единиц и нулей. Система декодирования проще некуда. Пустая строка означает id, т.е. лямбда-выражение [x|x]. Остальные строки последовательно расшифровываются с конца в дерево комбинаторов:
*0 → *SK
*1 → [x|y|*(x(y))].
Напоминаю, что константный комбинатор K = [x|y|x], а комбинатор обобщённого применения S = [x|y|z|x(z)(y(z))]. А Gödel numbering оно потому, что при добавлении к алфавиту из нуля и единицы ряда дополнительных символов, получается способ кодирования произвольных логических высказываний конечными строками символов конечного алфавита. Например для получения интуиционистской логики достаточно добавления символа отрицания, символа импликации и символа равенства. Для получения Observational Type Theory с ZFC-эквивалентной теорией множеств понадобится добавление 7 символов. Π, Σ, W, ⊥, ⊤, Ω, Set.
Ещё немножечко об интересном.
Aug. 9th, 2010 07:44 amНапомню, что категорией называется класс C, снабженный правилом, сопоставляющим каждой паре представителей этого класса множество “переходов” между ними. Дополнительно требуется, чтобы для каждого X существовал нулевой переход id: X → X и чтобы для двух переходов f: A → B и g: B → C можно было строить их (ассоциативную) композицию gf: A → C.
Категория называется малой, если класс её объектов задан множеством. Малая категория называется точной (терминология Лавера), если равенство элементов задающего её множества равносильно их неразличимости при помощи переходов. Категория называется группоидом, если все переходы обратимы.
Лавер ввёл понятие пространства длин. Он ввёл его категорно. Т.е. пространство длин это точная категория (более того, точный группоид), обладающая рядом свойств. Эти свойства, однако, удобнее вводить всё-таки на алгебраическом языке. Пространство длин — это (достаточно регулярное) частично-упорядоченное множество с минимальным элементом 0 и максимальным элементом ∞, снабжённое операцией +, совместимой с порядком и выполняющей аксиомы коммутативного моноида. Эталонное пространство длин — луч положительных действительных чисел с бесконечностью [0, ∞], снабжённый обычной операцией сложения. Ещё он ввёл понятие инволютивного пространства длин. Это соответственно то же самое с тем отличием, что операция + не обязательно коммутативна, однако дополнительно дана такая инволюция *, что (a + b)* = b* + a*. Коммутативные пространства длин являются частным случаем инволютивных с тривиальной инволюцией.
Обобщённым метрическим пространством называется группоид, обогащённый над некоторым пространством длин. Т.е. это множество объектов, называемых точками, таких что для каждой пары точек существует множество переходов между ними и каждому переходу сопоставлена длина, причём при соединении переходов их длины складываются. Соответственно некоммутативным метрическим пространством называется обогащённая над некоторым инволютивным пространством длин точная категория. Т.е. мы отказываемся от требования, что пути обратимы, а если два перехода f и g взаимнообратны, то требуем, чтобы length(f) = length(g)*. Показано, что всякая (обычная) топология порождается обобщённой метрикой на множестве.
Теория обобщённых метрических пространств обобщает идеи топологии и теории доменов. Некто Копперман в рамках указанного формализма ввёл понятие аппроксимируемых пространств, т.е. пространств, точки которых могут быть эффективно выделены итеративным сужением области вокруг них. Он же высказал гипотезу, что аппроксимируемые обобщённые метрические пространства формируют топос. Это очередной кандидат на роль универсального топоса «без сюрпризов», достаточно большого, чтобы делать в нём всю нужную в естественных науках математику.
Категория называется малой, если класс её объектов задан множеством. Малая категория называется точной (терминология Лавера), если равенство элементов задающего её множества равносильно их неразличимости при помощи переходов. Категория называется группоидом, если все переходы обратимы.
Лавер ввёл понятие пространства длин. Он ввёл его категорно. Т.е. пространство длин это точная категория (более того, точный группоид), обладающая рядом свойств. Эти свойства, однако, удобнее вводить всё-таки на алгебраическом языке. Пространство длин — это (достаточно регулярное) частично-упорядоченное множество с минимальным элементом 0 и максимальным элементом ∞, снабжённое операцией +, совместимой с порядком и выполняющей аксиомы коммутативного моноида. Эталонное пространство длин — луч положительных действительных чисел с бесконечностью [0, ∞], снабжённый обычной операцией сложения. Ещё он ввёл понятие инволютивного пространства длин. Это соответственно то же самое с тем отличием, что операция + не обязательно коммутативна, однако дополнительно дана такая инволюция *, что (a + b)* = b* + a*. Коммутативные пространства длин являются частным случаем инволютивных с тривиальной инволюцией.
Обобщённым метрическим пространством называется группоид, обогащённый над некоторым пространством длин. Т.е. это множество объектов, называемых точками, таких что для каждой пары точек существует множество переходов между ними и каждому переходу сопоставлена длина, причём при соединении переходов их длины складываются. Соответственно некоммутативным метрическим пространством называется обогащённая над некоторым инволютивным пространством длин точная категория. Т.е. мы отказываемся от требования, что пути обратимы, а если два перехода f и g взаимнообратны, то требуем, чтобы length(f) = length(g)*. Показано, что всякая (обычная) топология порождается обобщённой метрикой на множестве.
Теория обобщённых метрических пространств обобщает идеи топологии и теории доменов. Некто Копперман в рамках указанного формализма ввёл понятие аппроксимируемых пространств, т.е. пространств, точки которых могут быть эффективно выделены итеративным сужением области вокруг них. Он же высказал гипотезу, что аппроксимируемые обобщённые метрические пространства формируют топос. Это очередной кандидат на роль универсального топоса «без сюрпризов», достаточно большого, чтобы делать в нём всю нужную в естественных науках математику.
(no subject)
Aug. 9th, 2010 09:08 amА всякому, кто хочет разобраться в понятиях категоричности аксиоматических систем (теория) и универсальности универсальных объектов, и разобраться в теореме о неполноте Гёделя, советую вот эту штучку: //www.hss.cmu.edu/philosophy/techreports/118_Awodey.pdf. Естественно прежде надо почитать про теорию моделей и про топосы, как наиболее универсальные штуки, в которых можно интерпретировать (снабжать семантикой) аксиоматические теории, затем фкурить теоремы о поноте (Гёдель) и некатегоричности (Лёвенгейм-Сколем) всех богатых first order theories в Set-семантике, разобраться в исходном доказательстве Гёделя теоремы о неполноте всех богатых higher order theories в Set-семантике и об их полноте (Аводей-Бутц) в Top-семантике, которая чётко характеризует доказуемые и недоказуемые высказывания в higher order theories.