и он таки применяется, но для языков запросов

Насколько я знаю, эта область довольно широкая. Я видел топологический анализ лямбда-калькулюса. Размерности там всякие.

прям топологический?

мне на ум приходит только теория доменов и свежие работы цайлбергера сотоварищи вокруг skew monoidal categories

но во втором случае там скорее комбинаторика, симплексы всякие

Прям топологический. Там какая-то теория плетений (webbing), и изучение структур множеств lambda-термов. Начинается с доменов, но потом переход был на графы функций.

а ок, всё же домены

Разве это не исследование их выразительной способности?

Или можете сказать что вы конкретно имели ввиду под «что языки могут, а что нет»?

А я про что написал

Так а что вас интересует? Если есть if/while то мы уже в тьюринг полноте и все выразимо. Вопрос того, что именно вы хотите выражать.

Кроме того, синтаксис всех полезных языков контекстно-зависимый, а грамматика, используемая для построения парсера (и указанные в стандартах грамматики), дают лишь контекстно-свободную аппроксимацию языка. Я подозреваю, что вас интересуют всякие ограничения на построение программ типа "в функцию by construction не передать число меньшее пяти". Но учитывая то, что кс грамматика не выражает даже свойства "переменная, которую мы используем, была объявлена", есть сомнения в том, что эта дорога нас куда-то приведет

Тьюринг-полнота не про выразимость, а про класс вычислительной сложности RE

complexity же

во, вспомнил слово - cost semantics

типа

http://dlicata.web.wesleyan.edu/pubs/dlr15inductive/dlr15inductive.pdf Danner, Licata, Ramyaa, [2015] "Denotational Cost Semantics for Functional Languages with Inductive Types"

http://lambda-the-ultimate.org/node/5021 еще

Спасибо, тоже посмотрю

А мне тоже кажется что вопрос тривиальный потому что большинство ЯП тьюринг полные. В дескриптивной сложности у нас есть формальная система и мы смотрим на то какие проблемы в ней разрешимы. В случае с ЯП получится что выражвется все что в R. Но кстати о выразимости - и так существует хороший математический критерий о котором тут часто скидывают презентацию

🤦‍♂

Есть такая тема occurence typing. Никому не встречались статьи с описанием реализации этих алгоритмов типизации? Мы накопали работы по теории, но там много всяких нестандартных конструкций в правилах вывода, и не очень понятно, как их реализовывать.

Возможно, конечно, можно применить NbE, который, вобщем-то, универсален. Но перед тем, как погружаться в эту реализацию, хотелось бы почитать других автров.