(Подтверждение моих теорий)
One syntax to rule them all. Andrej Bauer. (20 May 2022)
http://math.andrej.com/2022/05/20/one-syntax-to-rule-them-all/
(я deep_econom не являюсь докладчиком Andrej Bauer)
---(гугл-перевод)---
Я нахожусь на семинаре по синтаксису и семантике теории типов в Стокгольме, стартовом совещании для WG6 сети EuroProofNet COST, где я выступаю с докладом “Один синтаксис, чтобы управлять ими всеми”, основанным на совместной работе с Данелем Ахманом.
Аннотация: Необработанный синтаксис теории типов или, в более общем смысле, формальной системы с обязательными конструкциями включает в себя не только свободные и связанные переменные, но и мета-переменные, которые фигурируют в правилах вывода. Каждое понятие переменной имеет связанное понятие подстановки. Синтаксический перевод из одной теории типов в другую вводит еще один уровень подстановок, на этот раз отображая теоретико-типовые конструкторы на термины. Работа с тремя уровнями подстановки, каждый из которых зависит от предыдущего, является громоздкой и повторяющейся. Возникает ощущение, что должен быть лучший способ справиться с синтаксисом.
--
