#матлог #учёба #спецсеминар

Семинар «Вероятностные и субструктурные логические системы» (www.mathnet.ru/conf2533) под руководством С.Л. Кузнецова (homepage.mi-ras.ru/~sk/) и С.О. Сперанского (homepage.mi-ras.ru/~speranski/)

Время: 22 апреля 2025, начало — в 16:00
Место: МИАН, ком. 303 + Контур.Толк

Павел Соколов (НИУ ВШЭ)

Утверждения как сессии

Классическое соответствие Карри-Говарда между интуиционистской логикой и простым типизированным лямбда-исчислением наталкивает на мысль, что это соответствие продолжается как на более сложные логики, так и на более интересные диалекты лямбда-исчисления. В частности, для интуиционистской линейной логики с экспоненциалом ! нетрудно выписать соответствующий субструктурный вариант лямбда-исчисления; полученный язык наделяет линейные типы "ресурсной" семантикой. Однако более естественной "логикой ресурсов" оказывается т.н. uniqueness logic [Harrington 2006], в то время как реализации линейных систем менее эффективны.

Оказывается, что у собственно линейной логики есть совершенно другая интерпретация — утверждений как сессий, в которых утверждения описывают некоторый протокол взаимодействия (сессию); соответствующим исчислением, позволяющим описывать "процессы", удовлетворяющие протоколам, оказывается π-исчисление, формализм для описания параллельных процессов.

В предлагаемом слушателям докладе будут изложены наиболее успешные результаты по реализации программы утверждений как сессий по мотивам статей Propositions as Sessions [Wadler 2014], Better late than never и Taking Linear Logic Apart [Kokke 2019].

➰ ВК