Режиссерская строка - Director string

В математика, в районе лямбда-исчисление и вычисление, директора или же режиссерские струны являются механизмом для отслеживания свободные переменные в срок. Грубо говоря, их можно понимать как своего рода мемоизация для свободных переменных; то есть как оптимизация техника для быстрого поиска свободных переменных в алгебра терминов или в лямбда-выражении. Режиссерские струны были представлены Kennaway и Sleep в 1982 году и в дальнейшем развиты Sinot, Fernández и Mackie.^[1] как механизм понимания и контроля вычислительная сложность стоимость бета-уменьшение.

Мотивация

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

${displaystyle (lambda x.E) yequiv E [x: = y],}$ или же ${displaystyle (lambda x.E) yequiv E [y / x]}$ (Заменить все Икс в E(тело) у)

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

Определение

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

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

куда ж это функция, из арность п, без свободные переменные, а ${displaystyle t_ {i}}$ - это термины, которые могут содержать или не содержать свободные переменные. Позволять V обозначают набор всех свободных переменных, которые могут входить в набор всех термов. Режиссер тогда карта

${displaystyle sigma _ {t}: V o P (lbrace 1,2, dots, nbrace)}$

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

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

Общий случай

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

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

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

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

• F.-R. Sinot. "Возвращение к Director Strings: общий подход к эффективному представлению свободных переменных при перезаписи более высокого порядка. " Журнал логики и вычислений 15(2), страницы 201-218, 2005.