Covalue

Сегодня ночью допилил на идрисе майкбрайдовский ко-де-Брёйн в интерпретации Dan Doel (ссылки в ридми): https://github.com/clayrat/PRSA/tree/master/src/Somewhere

Суть идеи - натянуть линейное обращение с переменными назад на интуиционистскую лямбду. Т.е., отталкиваемся от того факта, что в линейной логике стартовый секвент это A ⊢ A: конструкторы переменных не несут никакой дополнительной структурной информации, а только сигнализируют о том, что у нас в контексте единственная формула, которую мы и берем. Тогда нам нужно размазать weakening/contraction по остальным правилам, т.е., каждая лямбда должна сразу знать, используется ли её аргумент или нет, и каждая аппликация должна говорить, как распределены переменные между функцией и аргументом. По ходу дела оказывается, что мы попадаем в волшебный мир топосов Шануэля aka Клейсли-категорию свободных алгебр над монадкой включений. Все эти страшные слова означают тот факт, что мы по сути везде таскаем связку, показывающую как ослабить контекст до требуемого.

Профит от этой штуки не совсем понятен, но например hereditary substitution становится структурно-рекурсивным, что для тотальных языков всегда вин. В целом МакБрайд намекает на более эффективные и удобные тайпчекеры для пруверов.

GitHub

PRSA/src/Somewhere at master · clayrat/PRSA

Proof-relevant separation algebras from Rouvoet et al - clayrat/PRSA

www.tgoop.com/covalue/13

743 viewsedited  Jun 1, 2020 at 14:42

Сегодня ночью допилил на идрисе майкбрайдовский ко-де-Брёйн в интерпретации Dan Doel (ссылки в ридми): https://github.com/clayrat/PRSA/tree/master/src/Somewhere

Суть идеи - натянуть линейное обращение с переменными назад на интуиционистскую лямбду. Т.е., отталкиваемся от того факта, что в линейной логике стартовый секвент это A ⊢ A: конструкторы переменных не несут никакой дополнительной структурной информации, а только сигнализируют о том, что у нас в контексте единственная формула, которую мы и берем. Тогда нам нужно размазать weakening/contraction по остальным правилам, т.е., каждая лямбда должна сразу знать, используется ли её аргумент или нет, и каждая аппликация должна говорить, как распределены переменные между функцией и аргументом. По ходу дела оказывается, что мы попадаем в волшебный мир топосов Шануэля aka Клейсли-категорию свободных алгебр над монадкой включений. Все эти страшные слова означают тот факт, что мы по сути везде таскаем связку, показывающую как ослабить контекст до требуемого.

Профит от этой штуки не совсем понятен, но например hereditary substitution становится структурно-рекурсивным, что для тотальных языков всегда вин. В целом МакБрайд намекает на более эффективные и удобные тайпчекеры для пруверов.

BY Covalue