Постучалась в личку какая-то тня, — спросила что можно почитать по теории топосов..
the-village.ru Я проспал тот момент, когда РПЦ объявила себя наследницей лютеранской церкви Российской Империи?
Одная идея офигительней другой.
Берём simpled typed lambda calculus, расширяем его отношением порядка, основанном на принципе Барбары Лисков, а далее расширяем его конструкцией параметризированных универсумов. Естественно так как на Level и Set | есть вычислимой порядок, то на любом уровне Set будет задан вычислимый порядок. А теперь, ву-а-ля, добавим аксиому Set T === Level и радуемся получившемуся Логрусу.
Берём simpled typed lambda calculus, расширяем его отношением порядка, основанном на принципе Барбары Лисков, а далее расширяем его конструкцией параметризированных универсумов. Естественно так как на Level и Set | есть вычислимой порядок, то на любом уровне Set будет задан вычислимый порядок. А теперь, ву-а-ля, добавим аксиому Set T === Level и радуемся получившемуся Логрусу.
Типовая система с интенсиональным равенством на зависимых типах, расширенная экзистенсиональными свободно-полиморфными типами с экстенсиональным равенством на них.
Как Вы думаете, — отрежет ли гугол smtp и как скоро это произойдёт?
Let me be perfectly clear: it is not decidable whether I am a constructive mathematician.
За что я люблю диси так это за охуенную музыку на Арбате
В жуйке почему-то принято считать, что в Рашке фундаментальной науки нет, а между тем:
В мае 2006 года российские учёные под руководством Юрия Оганесяна из ОИЯИ объявили, что им удалось подтвердить существование первого долгоживущего изотопа элемента 114 и получить экспериментальное подтверждение существования Острова стабильности — в ходе этого эксперимента в дополнение к ранее проведённым физическим экспериментам была проведена химическая идентификация цепочек распада. Элемент флеровий (114) был признан IUPAC в декабре 2011 года и получил зарегистрированное официальное название в мае 2012 года.
ftp.qucis.queensu.ca
Забавный paper о физических основаниях тезиса Чёрча, из которого следует, что классическая механика неконструктивна, а релятивисткая механика при этом конструктивна и принимает расширенный тезис чёрча!
В конце автор замечает, что квантовая механика принимает тезис чёрча, но не принимает расширенный. У меня тут же возника логичный вопрос, — не решит ли полностью конструктивисткий квантмех автоматически проблемы совместности его с релятивизмом?
Забавный paper о физических основаниях тезиса Чёрча, из которого следует, что классическая механика неконструктивна, а релятивисткая механика при этом конструктивна и принимает расширенный тезис чёрча!
В конце автор замечает, что квантовая механика принимает тезис чёрча, но не принимает расширенный. У меня тут же возника логичный вопрос, — не решит ли полностью конструктивисткий квантмех автоматически проблемы совместности его с релятивизмом?
"А в прочем в памяти машины вручную догмы прописать ещё возможно (и не сложно). Вот только бы компьютер не сломать..." поют программисты в повести Аргонова. Похоже он знает толк в ERP'шниках.
Счастливые обладатели acer'а компиляют генту, — #2339350
Вместе с тем одна из самых полных и новых книжек по realizability in category theory. Тут есть практически все важные модели и результаты в области описания рекурсивной математики категориально-порядковым языком. Порог вхождения, правда, высокий, — автор предполагает, что читатель неплохо разбирается как в теории категорий, так и в теории порядка.
staff.science.uu.nl
P.S. Если хочется сначала вникнуть в эту область, то рекомендую начать с монографии Oosten'а "Realizability — An introduction to its categorical side". Тут есть основы и превосходно освещается привычная для рекурсивной математики категория Eff (По сути категория марковского конструктивизма)
staff.science.uu.nl
P.S. Если хочется сначала вникнуть в эту область, то рекомендую начать с монографии Oosten'а "Realizability — An introduction to its categorical side". Тут есть основы и превосходно освещается привычная для рекурсивной математики категория Eff (По сути категория марковского конструктивизма)
Computable and constructive mathematics is like the Matrix. Do you remember the film Matrix? Computable mathematics is the Matrix, a world built by intelligent computers to keep people from seeing the world as it really is. The realizers are the little green characters that keep falling down the screens. They seem infinitely more boring and less comprehensible than the Matrix. However, when Neo, the hero who saves humankind, reaches a higher level of awareness he sees the Matrix as it really is – made of little green characters. Intuitionistic logic and category theory are the Architect and the Oracle, but I am not telling which is which.
Andre Bauer (2005) "Realizability as the Connection between Computable and Constructive Mathematics", p. 33
Andre Bauer (2005) "Realizability as the Connection between Computable and Constructive Mathematics", p. 33
Васд привёз фиолетового слона!
Чят, есть ли какой-нибудь posix-совместимый shell с lua-like C API? Идея довольно банальна, а вот реализации я нигде так и не нашёл
