Covalue

Нашел два интересных обзорных эссе о теории доменов в прошлогоднем бюллетене от британской группы по формальным методам BCS-FACS:

* 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

www.tgoop.com/covalue/53

2.5K viewsedited  May 6, 2022 at 08:18

Нашел два интересных обзорных эссе о теории доменов в прошлогоднем бюллетене от британской группы по формальным методам BCS-FACS:

* Monahan, [2021] "Domain Theory - Revisited"
* Winskel, [2021] "Domain theory and interaction"

Первое эссе за авторством Монахана даёт обзор мотивации, контекста появления и основных идей теории доменов. Рассказывается о преодолении недоверия к нетипизированному лямбда-исчислению, поиске способов масштабирования и подходов к спецификации программ, о необходимости работы с частичными (из-за общей рекурсии) функциями.

Ключевая идея теории доменов - функции ЛИ соответствуют математическим функциям над особыми множествами (собственно, доменами, которые моделируют типы), упорядоченными по количеству содержащейся в них абстрактной информации, причем функции сохраняют этот порядок. Подобная структура функций позволяет конструировать неподвижные точки для них и таким образом моделировать рекурсию как предел нарабатывающего информацию процесса. Так впервые был выстроен топологический взгляд на вычисления, и информатика (точнее, теория языков программирования) оказалась полноценной математической теорией, а не просто "двиганием битов", что в свою очередь дало толчок развитию теорий типов и формальных семантик.

Эссе Винскеля более техническое и фокусируется на теме конкурентных и взаимодействующих вычислений. Начинается оно с введения в историю ТД с точки зрения её создателей, упоминает о создании LCF/PCF и ML, затем переходит к классическим проблемам ТД - работа с нондетерминизмом, проблема полной абстракции (конструкции в модели, для которых не существует синтаксиса). Пытаясь решить эти проблемы, теория доменов (и денотационная семантика в целом) перешла к созданию интерактивных моделей, в дальнейшем оформившихся в виде игровой семантики. С другой стороны, из-за проблем при работе с конкурентными программами, часть исследователей переключилась на алгебры процессов CCS/CSP с синхронизацией. Тем временем продолжение работ в рамках теории порядков привело к созданию понятия структуры событий (формализацию которых на Coq, кстати, можно найти тут).

Дальше эссе подчеркивает связи с теорией категорий - предпучки, моноидальные категории, затрагивает связи с работами Жирара, описывает появление игровой семантики и её конкурентной разновидности - где одновременно и игры (модели типов), и стратегии (модели программ) описываются структурами событий (в отличие от классических игр на деревьях), показывает как свести конкурентные игры к доменным моделям, геометрии взаимодействия и линзам.

BY Covalue