Ciąg reżyserski

W matematyce , w obszarze rachunku lambda i obliczeń , dyrektorzy lub ciągi dyrektorskie są mechanizmem śledzenia wolnych zmiennych w terminie . Mówiąc luźno, można je rozumieć jako rodzaj zapamiętywania zmiennych swobodnych; to znaczy jako optymalizacji do szybkiego lokalizowania zmiennych wolnych w algebrze terminów lub w wyrażeniu lambda. Ciągi Director zostały wprowadzone przez Kennawaya i Sleepa w 1982 roku, a dalej rozwijane przez Sinot, Fernández i Mackie jako mechanizm do zrozumienia i kontrolowania kosztu złożoności obliczeniowej redukcji beta .

Motywacja

W redukcji beta definiuje się wartość wyrażenia po lewej stronie jako wartość wyrażenia po prawej stronie:

${\ Displaystyle (\ lambda xE) y \ równoważnik E [x: = y] \,}$ lub ${\ Displaystyle (\ lambda xE) y \ równoważnik E [y/x]}$ (Zastąp wszystkie x w E (ciało) przez y )

Chociaż jest to koncepcyjnie prosta operacja, złożoność obliczeniowa tego kroku może być nietrywialna: naiwny algorytm przeszukałby wyrażenie E pod kątem wszystkich wystąpień zmiennej swobodnej x . Taki algorytm ma wyraźnie O ( n ) długości wyrażenia E . W ten sposób jest się zmotywowanym do śledzenia w jakiś sposób wystąpień wolnych zmiennych w wyrażeniu. Można próbować śledzić pozycję każdej wolnej zmiennej, gdziekolwiek występuje w wyrażeniu, ale może to oczywiście stać się bardzo kosztowne pod względem przechowywania; ponadto zapewnia poziom szczegółowości, który tak naprawdę nie jest potrzebny. Ciągi Director sugerują, że poprawnym modelem jest śledzenie wolnych zmiennych w sposób hierarchiczny, poprzez śledzenie ich użycia w terminach składowych.

Definicja

Rozważmy, dla uproszczenia, termin algebrę , czyli zbiór wolnych zmiennych, stałych i operatorów, które można dowolnie łączyć. Załóżmy, że wyraz t ma postać

${\ Displaystyle t:: = f (t_ {1}, t_ {2}, \ kropki, t_ {n})}$

gdzie f jest funkcją o arity n , bez wolnych zmiennych , a są to $.$ mogą zawierać lub nie zawierać wolnych zmiennych Niech V oznacza zbiór wszystkich zmiennych wolnych, które mogą wystąpić w zbiorze wszystkich terminów. Reżyserem jest więc mapa

${\ Displaystyle \ sigma _ {t}: V \ do P (\ lbrace 1,2, \ kropki, n \ rbrace)}$

od wolnych zmiennych do potęgi zbioru ${ \ Displaystyle X =$ X $nawias }$$lbrace 1,2, \ kropki$ . Wartości przyjmowane przez $prostu$ listą indeksów, $w$ których występuje dana zmienna ${5}},$ przykład, jeśli zmienna swobodna $t_$ w i ${\ Displaystyle$ ale w żaden inny sposób σ ${\ Displaystyle \ sigma _ {t} (x) = \ lbrace 3,5 \ rbrace$ .

Zatem dla każdego terminu $zbiorze$ wszystkich terminów ${\ displaystyle$ się funkcję i zamiast pracować tylko z terminami t , ∈ t \ in T } jeden działa z parami ${\ Displaystyle (t, \ sigma _ {t})}$ . Zatem złożoność czasowa znalezienia wolnych zmiennych w t jest wymieniana na złożoność przestrzenną utrzymywania listy terminów, w których występuje zmienna.

Sprawa ogólna

Chociaż powyższa definicja jest sformułowana w terminach algebry , ogólna koncepcja ma zastosowanie bardziej ogólne i może być zdefiniowana zarówno dla algebr kombinatorycznych , jak i dla właściwego rachunku lambda , w szczególności w ramach jawnego podstawienia .

Zobacz też

• System przepisywania terminów
• Wyraźne podstawienie
• Zapamiętywanie

• F.-R. Sinot. „ Director Strings Revisited: Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting ” Journal of Logic and Computation 15 (2), strony 201-218, 2005.