Майк Шульман анонсировал серию докладов "Towards Third-Generation HOTT" 14, 21 и 28 апреля: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html
Имеется в виду что первое поколение это "книжный HoTT", а второе - кубические теории. Аббревиатура гипотетического третьего поколения это сокращение от "Higher Observational Type Theory".
Имеется в виду что первое поколение это "книжный HoTT", а второе - кубические теории. Аббревиатура гипотетического третьего поколения это сокращение от "Higher Observational Type Theory".
www.math.uwo.ca
HoTTEST
Western University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Forwarded from Alexander Chichigin
Майкл Шульман выступит на другом семинаре: https://groups.google.com/g/homotopytypetheory/c/m3hQAKtypJs
(уже в PLT календаре 😊)
(уже в PLT календаре 😊)
Нашел два интересных обзорных эссе о теории доменов в прошлогоднем бюллетене от британской группы по формальным методам BCS-FACS:
* Monahan, [2021] "Domain Theory - Revisited"
* Winskel, [2021] "Domain theory and interaction"
Первое эссе за авторством Монахана даёт обзор мотивации, контекста появления и основных идей теории доменов. Рассказывается о преодолении недоверия к нетипизированному лямбда-исчислению, поиске способов масштабирования и подходов к спецификации программ, о необходимости работы с частичными (из-за общей рекурсии) функциями.
Ключевая идея теории доменов - функции ЛИ соответствуют математическим функциям над особыми множествами (собственно, доменами, которые моделируют типы), упорядоченными по количеству содержащейся в них абстрактной информации, причем функции сохраняют этот порядок. Подобная структура функций позволяет конструировать неподвижные точки для них и таким образом моделировать рекурсию как предел нарабатывающего информацию процесса. Так впервые был выстроен топологический взгляд на вычисления, и информатика (точнее, теория языков программирования) оказалась полноценной математической теорией, а не просто "двиганием битов", что в свою очередь дало толчок развитию теорий типов и формальных семантик.
Эссе Винскеля более техническое и фокусируется на теме конкурентных и взаимодействующих вычислений. Начинается оно с введения в историю ТД с точки зрения её создателей, упоминает о создании LCF/PCF и ML, затем переходит к классическим проблемам ТД - работа с нондетерминизмом, проблема полной абстракции (конструкции в модели, для которых не существует синтаксиса). Пытаясь решить эти проблемы, теория доменов (и денотационная семантика в целом) перешла к созданию интерактивных моделей, в дальнейшем оформившихся в виде игровой семантики. С другой стороны, из-за проблем при работе с конкурентными программами, часть исследователей переключилась на алгебры процессов CCS/CSP с синхронизацией. Тем временем продолжение работ в рамках теории порядков привело к созданию понятия структуры событий (формализацию которых на Coq, кстати, можно найти тут).
Дальше эссе подчеркивает связи с теорией категорий - предпучки, моноидальные категории, затрагивает связи с работами Жирара, описывает появление игровой семантики и её конкурентной разновидности - где одновременно и игры (модели типов), и стратегии (модели программ) описываются структурами событий (в отличие от классических игр на деревьях), показывает как свести конкурентные игры к доменным моделям, геометрии взаимодействия и линзам.
* Monahan, [2021] "Domain Theory - Revisited"
* Winskel, [2021] "Domain theory and interaction"
Первое эссе за авторством Монахана даёт обзор мотивации, контекста появления и основных идей теории доменов. Рассказывается о преодолении недоверия к нетипизированному лямбда-исчислению, поиске способов масштабирования и подходов к спецификации программ, о необходимости работы с частичными (из-за общей рекурсии) функциями.
Ключевая идея теории доменов - функции ЛИ соответствуют математическим функциям над особыми множествами (собственно, доменами, которые моделируют типы), упорядоченными по количеству содержащейся в них абстрактной информации, причем функции сохраняют этот порядок. Подобная структура функций позволяет конструировать неподвижные точки для них и таким образом моделировать рекурсию как предел нарабатывающего информацию процесса. Так впервые был выстроен топологический взгляд на вычисления, и информатика (точнее, теория языков программирования) оказалась полноценной математической теорией, а не просто "двиганием битов", что в свою очередь дало толчок развитию теорий типов и формальных семантик.
Эссе Винскеля более техническое и фокусируется на теме конкурентных и взаимодействующих вычислений. Начинается оно с введения в историю ТД с точки зрения её создателей, упоминает о создании LCF/PCF и ML, затем переходит к классическим проблемам ТД - работа с нондетерминизмом, проблема полной абстракции (конструкции в модели, для которых не существует синтаксиса). Пытаясь решить эти проблемы, теория доменов (и денотационная семантика в целом) перешла к созданию интерактивных моделей, в дальнейшем оформившихся в виде игровой семантики. С другой стороны, из-за проблем при работе с конкурентными программами, часть исследователей переключилась на алгебры процессов CCS/CSP с синхронизацией. Тем временем продолжение работ в рамках теории порядков привело к созданию понятия структуры событий (формализацию которых на Coq, кстати, можно найти тут).
Дальше эссе подчеркивает связи с теорией категорий - предпучки, моноидальные категории, затрагивает связи с работами Жирара, описывает появление игровой семантики и её конкурентной разновидности - где одновременно и игры (модели типов), и стратегии (модели программ) описываются структурами событий (в отличие от классических игр на деревьях), показывает как свести конкурентные игры к доменным моделям, геометрии взаимодействия и линзам.
Wikipedia
BCS-FACS
specialist Group of the BCS
Covalue
Майк Шульман анонсировал серию докладов "Towards Third-Generation HOTT" 14, 21 и 28 апреля: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html Имеется в виду что первое поколение это "книжный HoTT", а второе - кубические теории. Аббревиатура гипотетического…
Выложили записи всех трёх частей "Towards third generation HOTT":
* Part 1: Basic syntax (slides)
* Part 2: Symmetries and semicartesian cubes (slides)
* Part 3: Univalent universes (slides)
* Part 1: Basic syntax (slides)
* Part 2: Symmetries and semicartesian cubes (slides)
* Part 3: Univalent universes (slides)
YouTube
Mike Shulman: Towards Third-Generation HOTT, Part 1
CMU HoTT seminar, April 28, 2022
Mike Shulman - University of San Diego
Towards Third-Generation HOTT, Part 1
In Book HoTT, identity is defined uniformly by the principle of "indiscernibility of identicals". This automatically gives rise to higher structure;…
Mike Shulman - University of San Diego
Towards Third-Generation HOTT, Part 1
In Book HoTT, identity is defined uniformly by the principle of "indiscernibility of identicals". This automatically gives rise to higher structure;…
Андрей Бауэр выложил черновик лекций по реализуемости:
http://www.andrej.com/zapiski/MGS-2022/notes-on-realizability.pdf Bauer, [2022] "Notes on realizability"
Реализуемость можно понимать как более слабую/обобщенную версию соответствия Карри-Говарда, т.е. идеи о том что логические доказательства можно интерпретировать как программы - в случае реализуемости не обязательно тотальные или даже типизированные.
http://www.andrej.com/zapiski/MGS-2022/notes-on-realizability.pdf Bauer, [2022] "Notes on realizability"
Реализуемость можно понимать как более слабую/обобщенную версию соответствия Карри-Говарда, т.е. идеи о том что логические доказательства можно интерпретировать как программы - в случае реализуемости не обязательно тотальные или даже типизированные.
Shavit, [2011] "Data structures in the multicore age"
Относительно известная научно-популярная статья десятилетней давности одного из корифеев конкаренси о будущем многопоточного (библиотечного) программирования.
Начинается с мотивации законом Амдала о ботлнеке параллельных вычислений. Упоминает, что корректность в многопоточном сеттинге распадается на два аспекта: safety (относительно модели согласованности, например линеаризуемости) и liveness (условия прогресса - lock-free/wait-free и более экзотические). Также изменяются инструменты работы с complexity - добавляется модель stalls, нужно внимательно следить за contention. Делается предсказание, что развитие алгоритмов и структур данных пойдет по пути ослабления гарантий (кажется, спустя 10+ лет это до сих пор довольно нишевые вещи).
Основное время статья описывает в качестве примера процесс "ослабления" многопоточного стека на жаве, проходя несколько фаз:
1. стек под спинлоком - линеаризуем, не параллелен (deadlock-free), забивает шину из-за бесконтрольных спинов (обычно решается backoff-схемами)
2. lock-free стек - специализирует лок до CASа на голове стека
3. elimination backoff stack - убирает последовательный ботлнек, получая т.н. "дуальную" структуру - т.е. позволяя тредам оставлять "антиданные" (заявки) и передавать элементы напрямую без записи в стек, по прежнему линеаризуем
4. elimination tree - дуальность плохо работает в случае пакетов однотипных операций, поэтому можно ослабить согласованность до quiescent модели (иллюзия линейности только в периоды бездействия), разбив стек на несколько параллельных и прикрыв их балансировщиками
5. stack pool - в конечном счете проблемой является сама последовательная логика стека, поэтому дальнейшего роста быстродействия можно добиться, убрав балансирующую машинерию и превратив стек в тщательно подогнанную под архитектуру слабоупорядоченную структуру, которой, по мнению автора, должно хватать для большинства приложений
Подобным же образом предполагается ослаблять и другие структуры, например, переходя на хеширование вместо точных запросов. Кажется, это отчасти сбылось с популяризацией вероятностных структур типа фильтра Блума.
#concurrency
Относительно известная научно-популярная статья десятилетней давности одного из корифеев конкаренси о будущем многопоточного (библиотечного) программирования.
Начинается с мотивации законом Амдала о ботлнеке параллельных вычислений. Упоминает, что корректность в многопоточном сеттинге распадается на два аспекта: safety (относительно модели согласованности, например линеаризуемости) и liveness (условия прогресса - lock-free/wait-free и более экзотические). Также изменяются инструменты работы с complexity - добавляется модель stalls, нужно внимательно следить за contention. Делается предсказание, что развитие алгоритмов и структур данных пойдет по пути ослабления гарантий (кажется, спустя 10+ лет это до сих пор довольно нишевые вещи).
Основное время статья описывает в качестве примера процесс "ослабления" многопоточного стека на жаве, проходя несколько фаз:
1. стек под спинлоком - линеаризуем, не параллелен (deadlock-free), забивает шину из-за бесконтрольных спинов (обычно решается backoff-схемами)
2. lock-free стек - специализирует лок до CASа на голове стека
3. elimination backoff stack - убирает последовательный ботлнек, получая т.н. "дуальную" структуру - т.е. позволяя тредам оставлять "антиданные" (заявки) и передавать элементы напрямую без записи в стек, по прежнему линеаризуем
4. elimination tree - дуальность плохо работает в случае пакетов однотипных операций, поэтому можно ослабить согласованность до quiescent модели (иллюзия линейности только в периоды бездействия), разбив стек на несколько параллельных и прикрыв их балансировщиками
5. stack pool - в конечном счете проблемой является сама последовательная логика стека, поэтому дальнейшего роста быстродействия можно добиться, убрав балансирующую машинерию и превратив стек в тщательно подогнанную под архитектуру слабоупорядоченную структуру, которой, по мнению автора, должно хватать для большинства приложений
Подобным же образом предполагается ослаблять и другие структуры, например, переходя на хеширование вместо точных запросов. Кажется, это отчасти сбылось с популяризацией вероятностных структур типа фильтра Блума.
#concurrency
Papayannopoulos, [2020] "Unrealistic Models for Realistic Computations: How Idealisations Help Represent Mathematical Structures and Found Scientific Computing"
Научные вычисления (scientific computing / computational science), т.е. общие техники для всех вычислительных ветвей эмпирических наук, можно разделить на символьные и численные методы, в статье идёт речь о последних. Т.к. численные методы работают с непрерывными значениями (действительными/комплексными числами и их обобщениями), появляются вопросы сходимости, устойчивости и вычислимости алгоритмов над плавающей арифметикой (в частности проблема накопления ошибок округления). Для изучения этих вопросов нужен математический фреймворк вычислений над несчетными множествами, из наиболее популярных это BSS model (aka Real-RAM) и computable analysis (aka Type Two Effectivity), причем друг с другом они несовместимы. Статья посвящена разбору этих двух подходов.
CA/TTE - более фундаментальная и "низкоуровневая" теория, это разновидность матанализа, где сохраняется классическая теория, но дополнительно учитываются вычислительные представления объектов через бесконечные аппроксимации. Как правило, это делается через работу с некоторыми разновидностями машин Тюринга (с оракулом или более сложной машинерией репрезентаций). Её появление можно отследить к трудам Бореля, Банаха и Тюринга 1910-30х годов, где рассматривались вычислимые подмножества R (эта идея получила развитие в Марковской школе конструктивизма/синтетической вычислимости). Более поздние подходы ("Хагенская школа") перешли к рассмотрению всего R (ключевая идея TTE). В этой модели вычислимые функции должны быть непрерывными - как следствие, мы теряем возможность полноценно использовать "точечные" функции сравнения и округления (ср. https://twitter.com/andrejbauer/status/1400172747930718209).
BSS - модель вычислений с идеализированной RAM-машиной, способной хранить в памяти произвольные числа (в т.ч. и точные значения действительных) и мгновенно производить арифметические операции над ними. Тут не возникает проблем с разрывными функциями, но усложняется работа с функциями алгебраическими и трансцендентными (с которыми нет проблемы у CA), начиная с банальных квадратных корней.
Какой же фреймворк предпочтителен? BSS менее реалистична и хуже подходит для работы с ошибками округления и плохо обусловленными функциями, но тем не менее довольно популярна - она моделирует устойчивые алгоритмы (т.е. не вносит собственных ошибок) и позволяет работать с оценкой их сложности. Также BSS ближе к алгоритмам плавающей арифметики в том, что имеет фиксированную стоимость операций (в отличии от CA, где стоимость зависит от входа). С другой стороны, CA подходит для более глубоких вопросов вычислимости (в т.ч., например, квантовой) и работы с "плохо ведущими себя" функциями, но создает больше проблем при анализе стоимости и работе с хорошо изученными численными алгоритмами.
В конце статья проводит аналогию с физическими моделями, облегчающими работу за счет нереалистичных упрощений, например, плавающие числа можно рассматривать как аналог экспериментальных значений - т.е., классическая и вычислительная математики живут в разных реальностях.
#realnumbers
Научные вычисления (scientific computing / computational science), т.е. общие техники для всех вычислительных ветвей эмпирических наук, можно разделить на символьные и численные методы, в статье идёт речь о последних. Т.к. численные методы работают с непрерывными значениями (действительными/комплексными числами и их обобщениями), появляются вопросы сходимости, устойчивости и вычислимости алгоритмов над плавающей арифметикой (в частности проблема накопления ошибок округления). Для изучения этих вопросов нужен математический фреймворк вычислений над несчетными множествами, из наиболее популярных это BSS model (aka Real-RAM) и computable analysis (aka Type Two Effectivity), причем друг с другом они несовместимы. Статья посвящена разбору этих двух подходов.
CA/TTE - более фундаментальная и "низкоуровневая" теория, это разновидность матанализа, где сохраняется классическая теория, но дополнительно учитываются вычислительные представления объектов через бесконечные аппроксимации. Как правило, это делается через работу с некоторыми разновидностями машин Тюринга (с оракулом или более сложной машинерией репрезентаций). Её появление можно отследить к трудам Бореля, Банаха и Тюринга 1910-30х годов, где рассматривались вычислимые подмножества R (эта идея получила развитие в Марковской школе конструктивизма/синтетической вычислимости). Более поздние подходы ("Хагенская школа") перешли к рассмотрению всего R (ключевая идея TTE). В этой модели вычислимые функции должны быть непрерывными - как следствие, мы теряем возможность полноценно использовать "точечные" функции сравнения и округления (ср. https://twitter.com/andrejbauer/status/1400172747930718209).
BSS - модель вычислений с идеализированной RAM-машиной, способной хранить в памяти произвольные числа (в т.ч. и точные значения действительных) и мгновенно производить арифметические операции над ними. Тут не возникает проблем с разрывными функциями, но усложняется работа с функциями алгебраическими и трансцендентными (с которыми нет проблемы у CA), начиная с банальных квадратных корней.
Какой же фреймворк предпочтителен? BSS менее реалистична и хуже подходит для работы с ошибками округления и плохо обусловленными функциями, но тем не менее довольно популярна - она моделирует устойчивые алгоритмы (т.е. не вносит собственных ошибок) и позволяет работать с оценкой их сложности. Также BSS ближе к алгоритмам плавающей арифметики в том, что имеет фиксированную стоимость операций (в отличии от CA, где стоимость зависит от входа). С другой стороны, CA подходит для более глубоких вопросов вычислимости (в т.ч., например, квантовой) и работы с "плохо ведущими себя" функциями, но создает больше проблем при анализе стоимости и работе с хорошо изученными численными алгоритмами.
В конце статья проводит аналогию с физическими моделями, облегчающими работу за счет нереалистичных упрощений, например, плавающие числа можно рассматривать как аналог экспериментальных значений - т.е., классическая и вычислительная математики живут в разных реальностях.
#realnumbers
Wikipedia
Computational science
field concerned with constructing mathematical models and quantitative analysis techniques and using computers to analyze and solve scientific problems
Bornat, [2009] "Separation logic and concurrency"
Программирование это комбинация механических вычислений и формальной логики. Как правило, каждый новый формализм используется программистами для увеличения объема выразимых программ, а не корректности (насчет баланса между выразительностью и непротиворечивостью см также например https://twitter.com/aspiwack/status/1394012829464866819). Многопоточные вычисления - самая сложная разновидность программирования, и тут, как всегда, теория информатики одновременно и плетется за практикой, и обгоняет её.
Фундаментальная проблема конкаренси - синхронизация процессов, обменивающихся информацией, сама по себе является обменом информацией, т.е. мы как бы заперты внутри этой игры. Дейкстра предложил использовать примитивы синхронизации для структурирования параллельных программ, и задача корректности разделилась на проблемы верности того, что происходит при успешной синхронизации (обычно формулируемые как safety) и верности самой синхронизации (часто выражающиеся в форме liveness-свойств).
Конкурентная сепарационная логика (CSL) классически занимается safety, т.е. частичной корректностью многопоточной программы относительно спецификации и модели консистентности. Её предшественник это в первую очередь метод Owicki-Gries 70х - расширение аксиоматической логики Хоара на программы с примитивами параллельной композиции и синхронизации, основанное на доказательствах non-interference. Метод OG популяризировал идеи ресурсных инвариантов и вспомогательных (ghost) переменных. В 80х Cliff Jones доработал метод OG до rely-guarantee, добавив два одноименных условия к пред- и постусловиям. Одно из слабых мест обоих методов - работа с алиасингом, т.е. тем фактом, что одна ячейка памяти может индексироваться разными символьными выражениями. Для решения этой проблемы и была придумана сепарационная логика - параллельная ветка развития логики Хоара, где под "сепарацией" понимается двухместный предикат над ячейками, гарантирующий неравенство их адресов. Это позволяет иметь т.н. frame-правило (терминология, кстати, заимствована из ИИ), позволяющее отбрасывать "нерелевантные" логические условия, т.е. работать только с тем состоянием, которое напрямую затрагивается рассматриваемой частью программы.
Как и метод OG, CSL добавляет примитивы параллельной композиции и критических секций вида
Последняя секция посвящена доказательству для неблокирующего алгоритма 4-slot авторства Hugo Simpson - алгоритм реализует wait-free single-reader single-writer atomic register. Доказательство выполнено "а-ля моделчекинг", с явным перечислением состояний в инварианте. Было бы неплохо иметь алгоритмическую теорию ресурсов, которую мы могли бы использовать в компиляторах, говорит нам статья, и завершается оптимизмом насчет грядущей инкоропорации идей rely-guarantee и темпоральной логики в CSL.
#concurrency
Программирование это комбинация механических вычислений и формальной логики. Как правило, каждый новый формализм используется программистами для увеличения объема выразимых программ, а не корректности (насчет баланса между выразительностью и непротиворечивостью см также например https://twitter.com/aspiwack/status/1394012829464866819). Многопоточные вычисления - самая сложная разновидность программирования, и тут, как всегда, теория информатики одновременно и плетется за практикой, и обгоняет её.
Фундаментальная проблема конкаренси - синхронизация процессов, обменивающихся информацией, сама по себе является обменом информацией, т.е. мы как бы заперты внутри этой игры. Дейкстра предложил использовать примитивы синхронизации для структурирования параллельных программ, и задача корректности разделилась на проблемы верности того, что происходит при успешной синхронизации (обычно формулируемые как safety) и верности самой синхронизации (часто выражающиеся в форме liveness-свойств).
Конкурентная сепарационная логика (CSL) классически занимается safety, т.е. частичной корректностью многопоточной программы относительно спецификации и модели консистентности. Её предшественник это в первую очередь метод Owicki-Gries 70х - расширение аксиоматической логики Хоара на программы с примитивами параллельной композиции и синхронизации, основанное на доказательствах non-interference. Метод OG популяризировал идеи ресурсных инвариантов и вспомогательных (ghost) переменных. В 80х Cliff Jones доработал метод OG до rely-guarantee, добавив два одноименных условия к пред- и постусловиям. Одно из слабых мест обоих методов - работа с алиасингом, т.е. тем фактом, что одна ячейка памяти может индексироваться разными символьными выражениями. Для решения этой проблемы и была придумана сепарационная логика - параллельная ветка развития логики Хоара, где под "сепарацией" понимается двухместный предикат над ячейками, гарантирующий неравенство их адресов. Это позволяет иметь т.н. frame-правило (терминология, кстати, заимствована из ИИ), позволяющее отбрасывать "нерелевантные" логические условия, т.е. работать только с тем состоянием, которое напрямую затрагивается рассматриваемой частью программы.
Как и метод OG, CSL добавляет примитивы параллельной композиции и критических секций вида
with r when B do C (для которых подразумевается наличие более низкоуровневой имплементации). r - так называемый ресурс, для каждого из которых в логике вводится свой инвариант (также идея OG). Статья показывает пример доказательств для программ с семафорами, далее переходит к механизму permissions, нужному для отслеживания read-only вспомогательных переменных (существуют альтернативы этому механизму - subjective auxiliary state в FCSL и ghost objects/higher-order ghost code в Iris). Далее демонстрируется доказательство для readers-writer lock (запрет на гонку между чтением и записью) на семафорах, с использованием ghost ticket трюка.Последняя секция посвящена доказательству для неблокирующего алгоритма 4-slot авторства Hugo Simpson - алгоритм реализует wait-free single-reader single-writer atomic register. Доказательство выполнено "а-ля моделчекинг", с явным перечислением состояний в инварианте. Было бы неплохо иметь алгоритмическую теорию ресурсов, которую мы могли бы использовать в компиляторах, говорит нам статья, и завершается оптимизмом насчет грядущей инкоропорации идей rely-guarantee и темпоральной логики в CSL.
#concurrency
https://github.com/thery/FlocqLecture
Упражнения на работу с действительными числами и плавучкой в Coq с библиотекой Flocq - неравенства, режимы округления, форматы, лемма Стербенца, IEEE754.
#realnumbers
Упражнения на работу с действительными числами и плавучкой в Coq с библиотекой Flocq - неравенства, режимы округления, форматы, лемма Стербенца, IEEE754.
#realnumbers
GitHub
GitHub - thery/FlocqLecture
Contribute to thery/FlocqLecture development by creating an account on GitHub.
Известная в узких кругах take lemma для конечных списков через обобщенный take_take:
Lemma take_take_min {T} i j (s : seq T) : take i (take j s) = take (minn i j) s.
Proof. by elim: s i j => //= a l IH [|i] [|j] //=; rewrite minnSS IH. Qed.
Lemma take_lemma {T} (p r : seq T) : (forall i, take i p = take i r) <-> p = r.
Proof.
split; last by move=>->.
move=>H; move: (H (size p)) (H (size r)); rewrite !take_size=>{H} Hp Hr.
by rewrite Hp -Hr {2 3}Hp !take_take_min minnAC minnn minnC.
Qed.Forwarded from Sergey Kucherenko
https://serokell.io/blog/dependent-types-with-david-christiansen
In this month’s episode of Functional Futures, our guest is David Christiansen, the Executive Director of the Haskell Foundation, a contributor to a number of dependently typed languages, and a dependent type advocate that has managed to introduce many people to the topic today through his work, talks, and texts.
We cover topics such as dependent types, theorem proving, metaprogramming, and many more. We also discuss the book he co-authored with Daniel P. Friedman, The Little Typer, and his current work in progress: Functional Programming in Lean.
In this month’s episode of Functional Futures, our guest is David Christiansen, the Executive Director of the Haskell Foundation, a contributor to a number of dependently typed languages, and a dependent type advocate that has managed to introduce many people to the topic today through his work, talks, and texts.
We cover topics such as dependent types, theorem proving, metaprogramming, and many more. We also discuss the book he co-authored with Daniel P. Friedman, The Little Typer, and his current work in progress: Functional Programming in Lean.
Functional Futures: Dependent Types with David Christiansen
In this month’s episode of Functional Futures, our guest is David Christiansen – the Executive Director of the Haskell Foundation and the co-author of The Little Typer, a book on dependent types.
Семантика
Хоарова логика:
Сепарационная логика:
{P}c{Q}:Хоарова логика:
P s, s -(c)-> s' => Q s'Сепарационная логика:
P s, safe c s /\ s-(c)->s' => Q s'Forwarded from uAnalytiCon
Любители анализа данных, статистики, классификаций и прочего счетоводства выкатили новое занятное чтиво по поводу уже так всем надоевшего разделения на аналитическую философию и философию континентальную.
Исследование представленно в статье в журнале Metaphilosophy.
Также оно кратко освещёно в заметке в Daily Nous.
В этот раз исследователи подвергли кластерному анализу программы подготовки PhD из базы данных The Academic Philosophy Data and Analysis Project, которая ведётся с 2011 года. Всего рассмотрено 129 разных программ (актуальных на лето 2021 года), из которых, к сожалению, лишь 27 реализуются за пределами США. Кластеры составлялись на основе (1) области специализации и (2) ключевых слов, характеризующих образовательную программу. В итоге (для кого-то вполне ожидаемо) получилось, что разделение на аналитическую философию и философию континентальную имеет место, но представляет собой скорее упрощение действительного положения дел. Кластерный анализ даёт наилучшие результаты при выделении 3 кластеров: аналитическая философия (синий цвет на диаграммах, 72 программы), философия науки (фиолетовый цвет, 15 программ) и континентальная философия (жёлтый цвет, 40 программ). Хотя кластер философии науки находится как бы на границе между аналитической философией и философией континентальной, он более тяготеет именно к аналитической философии, и при выделении 2 кластеров сливается с последней.
Кроме того, авторы проанализировали выделение 6 кластеров, что не даёт достаточно хорошего результата при используемом количестве исходных данных. Однако это позволяет выделить в рамках аналитической философии дополнительно к философии науки и собственно аналитической философии (58 программ) кластер (из 14 программ) философии сознания и когнитивных наук, к которым (неожиданно!) примешиваются эстетика и философия религии, что можно считать погрешностью из-за недостаточности исходных данных, а в рамках континентальной философии — собственно континентальную традицию (15 программ), историко-философский и философско-религиозный кластер (17 программ), а также кластер (из 8 программ), связанный с этикой, политической философией и гендерными исследованиями.
Не спрашивайте, почему 72+15+40=127, если заявлено, что исходные данные содержат информацию о 129 программах. Ответ найдёте в разделе 3.1 статьи.
Исследование представленно в статье в журнале Metaphilosophy.
Также оно кратко освещёно в заметке в Daily Nous.
В этот раз исследователи подвергли кластерному анализу программы подготовки PhD из базы данных The Academic Philosophy Data and Analysis Project, которая ведётся с 2011 года. Всего рассмотрено 129 разных программ (актуальных на лето 2021 года), из которых, к сожалению, лишь 27 реализуются за пределами США. Кластеры составлялись на основе (1) области специализации и (2) ключевых слов, характеризующих образовательную программу. В итоге (для кого-то вполне ожидаемо) получилось, что разделение на аналитическую философию и философию континентальную имеет место, но представляет собой скорее упрощение действительного положения дел. Кластерный анализ даёт наилучшие результаты при выделении 3 кластеров: аналитическая философия (синий цвет на диаграммах, 72 программы), философия науки (фиолетовый цвет, 15 программ) и континентальная философия (жёлтый цвет, 40 программ). Хотя кластер философии науки находится как бы на границе между аналитической философией и философией континентальной, он более тяготеет именно к аналитической философии, и при выделении 2 кластеров сливается с последней.
Кроме того, авторы проанализировали выделение 6 кластеров, что не даёт достаточно хорошего результата при используемом количестве исходных данных. Однако это позволяет выделить в рамках аналитической философии дополнительно к философии науки и собственно аналитической философии (58 программ) кластер (из 14 программ) философии сознания и когнитивных наук, к которым (неожиданно!) примешиваются эстетика и философия религии, что можно считать погрешностью из-за недостаточности исходных данных, а в рамках континентальной философии — собственно континентальную традицию (15 программ), историко-философский и философско-религиозный кластер (17 программ), а также кластер (из 8 программ), связанный с этикой, политической философией и гендерными исследованиями.
Не спрашивайте, почему 72+15+40=127, если заявлено, что исходные данные содержат информацию о 129 программах. Ответ найдёте в разделе 3.1 статьи.
https://arxiv.org/abs/2209.07427 Boruch-Gruszecki, Wasko, Xu, Parreaux, [2022] "A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning"
https://github.com/Linyxus/cdot-calculus
крайняя версия формализации скального DOT calculus на Coq
https://github.com/Linyxus/cdot-calculus
крайняя версия формализации скального DOT calculus на Coq
GitHub
GitHub - Linyxus/cdot-calculus: Soundness proof for OOPSLA 2022 paper A case for DOT: Theoretical Foundations for Objects With…
Soundness proof for OOPSLA 2022 paper A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning. - Linyxus/cdot-calculus
Forwarded from Oleg ℕižnik
https://vxtwitter.com/EgbertRijke/status/1605798086462373888
https://mathstodon.xyz/@egbertrijke/109555699321931029
https://arxiv.org/abs/2212.11082
https://mathstodon.xyz/@egbertrijke/109555699321931029
https://arxiv.org/abs/2212.11082
vxTwitter / fixvx
Egbert Rijke (@EgbertRijke)
It is my pleasure to announce that my textbook Introduction to Homotopy Type Theory is finished and available on the ArXiv 🎉
It will be published by Cambridge University Press in the Cambridge Studies in Advanced Mathematics series.
https://arxiv.org/abs/2212.11082…
It will be published by Cambridge University Press in the Cambridge Studies in Advanced Mathematics series.
https://arxiv.org/abs/2212.11082…
Davenport, England, Griggio, Sturm, Tinelli, [2020] "Symbolic computation and satisfiability checking"
Небольшое введение в (относительно) современное состояние дел во взаимодействии SAT/SMT-солверов и систем компьютерной алгебры.
Небольшое введение в (относительно) современное состояние дел во взаимодействии SAT/SMT-солверов и систем компьютерной алгебры.
https://youtu.be/AaE1mV27XxA
Нашел наконец запись (версии) виденного в трансляции где-то с год назад доклада Джона Харрисона об истории развития пруверов и работе с формальной математикой, где он в частности проговаривает идею о том что автопрувинг был забеганием вперед, и отрасли стоило начинать с пруф-ассистентов.
Нашел наконец запись (версии) виденного в трансляции где-то с год назад доклада Джона Харрисона об истории развития пруверов и работе с формальной математикой, где он в частности проговаривает идею о том что автопрувинг был забеганием вперед, и отрасли стоило начинать с пруф-ассистентов.
YouTube
John Harrison - Formalization and Automated Reasoning: A Personal and Historical Perspective
Recorded 13 February 2023. John Harrison of Amazon Web Services presents "Formalization and Automated Reasoning: A Personal and Historical Perspective" at IPAM's Machine Assisted Proofs Workshop.
Abstract: In this talk I will try to first place the recent…
Abstract: In this talk I will try to first place the recent…
Manuell, [2023] "Pointfree topology and constructive mathematics"
Введение в конструктивную (бесточечную) топологию через механизм фреймов/локалей, обсуждает помимо прочего связь интуиционистской и геометрической логик, вводит компактность как "квантифицируемость" свойств.
Введение в конструктивную (бесточечную) топологию через механизм фреймов/локалей, обсуждает помимо прочего связь интуиционистской и геометрической логик, вводит компактность как "квантифицируемость" свойств.