«Не совсем так, если только не понимать под подстрокой подмножество символов строки. Правильнее так: если в правой части стереть все вызовы функций, то должна получиться конкатенация подстрок образца, взятых по одному разу в том порядке, в каком они входят в образец.»
Описка: я имел ввиду подпоследовательность. Если вычеркнуть из строки токенов образца некоторые токены и из строки токенов результата все угловые скобки (с именами функций), то должна получиться одинаковая строка. При этом круглые скобки должны вычёркиваться попарно. Как-то так. Но это необходимое условие. Более точное ограничение формулируется в терминах поддеревьев. «При выполнении линзы к термам, которые она выдаёт наружу, добавляется информация о том, каким исходным термам они соответствуют. Достаточно при этом аннотировать только те термы, которые отличаются от исходных.» Я так понимаю, что каждая функция должна компилироваться в двух режимах: в режиме линзы, когда она добавляет к термам аннотации, и в режиме линзированной функции (который ещё и общий случай), когда аннотации должны сохраняться (см. следующий абзац). Если функцию не удалось откомпилировать в первом режиме (она не соответствует синтаксическим требованиям, см. предыдущий абзац), то в её описателе добавляется соответствующий флаг и попытка использовать её в роли линзы приводит к аварийному завершению программы. «Надо только следить, чтобы код, порождённый компилятором для „линзированной“ функции, не потерял аннотации термов.» Собственно, вопрос в том, когда компилятор должен переносить аннотацию с терма из образца в терм результата. Из предыдущей беседы я понял так. Аннотация переносится, если терм в одном из результатных предложений аргумента (результате после «=» или результатных выражениях условий) текстуально совпадает с записью терма в одном из образцовых выражений предложения (образца аргумента или образца условия). Если совпадений несколько, то выбирается текстуально самое левое в предложении (?). Тогда, если аннотацию обозначить нижними индексами, получится следующее: (Ident e.Name)₁ (Ident e.Name)₂ = (Ident e.Name)₁ (Ident e.Name)₁ (Ident e.Name)₁; (Ident e.NameA)₁ (Ident e.NameB)₂, e.NameA : e.NameB = (Ident e.NameB)₂ (Ident e.NameA)₁; (Ident e.NameA), e.NameA : e.NameB = (Ident e.NameB); /* вообще не переносится */ «Несомненно. Я бы даже сказал, что такой показатель как сложность языка программирования не определяется каким-то объективным критерием, а является экспертным мнением. Но длина БНФ, на мой взгляд, влияет на экспертное мнение в сторону роста этого показателя, потому что когда мы добавляем новые синтаксические конструкции, возникают вопросы об их сочетании с уже имеющимися синтаксическими конструкциями и друг с другом, и объём документации, необходимой для их реализации в компиляторе и для их использования, в общем случае растёт нелинейно.» Согласен! Могу даже привести пример вопросов о взаимном сочетании. В Рефале есть встроенное в язык понятие равенства — два значения равны, если при сопоставлении с образцом их можно сопоставить с равными переменными. С точки зрения математики, две функции равны, если области определения совпадают и они одинаково отображают их на область значений. И при реализации вложенных функций у меня возникали вопросы, как же корректно в свете этих аксиом, определять их равенство, в том числе и с учётом оптимизаций (прогонки и специализации). Мы даже это обсуждали на семинаре в ИПМ РАН. Оказывалось, что имеющаяся реализация прогонки и специализации меняет поведение программ из-за вот этих тонкостей. Не помню, были Вы тогда на этом дистанционном семинаре или нет. В репозитории Рефала-5λ есть заявка с размышлениями о проблеме: https://github.com/bmstu-iu9/refal-5-lambda/issues/276 https://mazdaywik.github.io/direct-link/2021-05-17-Konovalov-Closures-and-Optimizations-Refal-5-lambda.pdf (слайды доклада) На мой экспертный😜 взгляд, простой синтаксический сахар не сильно повышает сложность, т.к. для него просто определяется эквивалентное преобразование в другие синтаксические конструкции. А значит, достаточно задокументировать эквивалентные преобразования синтаксического сахара в синтаксическое ядро и определить семантику только для последнего.
