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

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

Мотивация [ править ]

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

(\lambda x.E)y\equiv E[x:=y]\,

или

(\lambda x.E)y\equiv E[y/x]

(Замените все x в E (body) на y )

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

Определение [ править ]

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

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

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

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

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

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

Общий случай [ править ]

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

См. также [ править ]

Ссылки [ править ]

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

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

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

[1]