Строка директора

В математике , в области лямбда-исчисления и вычислений , директора или управляющие строки представляют собой механизм отслеживания свободных переменных в термине . Грубо говоря, их можно понимать как своего рода запоминание свободных переменных; то есть как метод оптимизации для быстрого поиска свободных переменных в алгебре термов или в лямбда-выражении. Строки-директора были представлены Кеннауэем и Слипом в 1982 году и далее развиты Синотом, Фернандесом и Маки ^[1] как механизм для понимания и контроля стоимости вычислительной сложности бета-редукции .

Мотивация

При бета-редукции значение выражения слева определяется как значение справа:

${\displaystyle (\lambda x.E)y\equiv E[x:=y]\,}$или (Замените все x в E (body) на y ) ${\displaystyle (\lambda x.E)y\equiv E[y/x]}$

Хотя это концептуально простая операция, вычислительная сложность этого шага может быть нетривиальной: простой алгоритм сканирует выражение E на предмет всех вхождений свободной переменной x . Такой алгоритм явно имеет длину O ( n ) выражения E. Таким образом, возникает мотивация каким-то образом отслеживать появление свободных переменных в выражении. Можно попытаться отслеживать положение каждой свободной переменной, где бы она ни встречалась в выражении, но это, очевидно, может стать очень затратным с точки зрения хранения; более того, он обеспечивает уровень детализации, который на самом деле не нужен. Строки-директора предполагают, что правильной моделью является отслеживание свободных переменных в иерархическом порядке, отслеживая их использование в терминах компонентов.

Определение

Рассмотрим для простоты термин «алгебра» , то есть набор свободных переменных, констант и операторов, которые можно свободно комбинировать. Предположим, что терм t принимает вид

${\displaystyle t::=f(t_{1},t_{2},\dots ,t_{n})}$

где f — функция арности n без свободных переменных , а the — термины , которые могут содержать или не содержать свободные переменные. Обозначим через V множество всех свободных переменных, которые могут встречаться в множестве всех термов. Режиссер тогда карта ${\displaystyle t_{i}}$

${\displaystyle \sigma _{t}:V\to P(\lbrace 1,2,\dots ,n\rbrace )}$

от свободных переменных к степенному набору набора . Принимаемые значения представляют собой просто список индексов, в которых встречается данная свободная переменная. Так, например, если свободная переменная встречается в и, но ни в каких других терминах, то имеется . ${\displaystyle P(X)}$ ${\displaystyle X=\lbrace 1,2,\dots ,n\rbrace }$ ${\displaystyle \sigma _{t}}$ ${\displaystyle t_{i}}$ ${\displaystyle x\in V}$ ${\displaystyle t_{3}}$ ${\displaystyle t_{5}}$ ${\displaystyle \sigma _{t}(x)=\lbrace 3,5\rbrace }$

Таким образом, для каждого термина в наборе всех терминов T сохраняется функция , и вместо работы только с терминами t мы работаем с парами . Таким образом, временная сложность поиска свободных переменных в t заменяется пространственной сложностью поддержания списка термов, в которых встречается переменная. ${\displaystyle t\in T}$ ${\displaystyle \sigma _{t}}$ ${\displaystyle (t,\sigma _{t})}$

Общий случай

Хотя приведенное выше определение сформулировано в терминах алгебры термина , общая концепция применяется более широко и может быть определена как для комбинаторных алгебр , так и для собственно лямбда-исчисления , в частности, в рамках явной подстановки .

Смотрите также

• Система перезаписи терминов
• Явная замена
• Мемоизация

Рекомендации

1. Ф.-Р. Сино, М. Фернандес и И. Маки. Эффективные сокращения с помощью управляющих строк. В Proc. Техники и приложения переписывания . Springer LNCS, том 2706, 2003 г.

• Ф.-Р. Синот. «Возвращение к строкам директора: общий подход к эффективному представлению свободных переменных при переписывании высшего порядка». Журнал логики и вычислений 15 (2), страницы 201–218, 2005 г.