Indeks De Bruijna

Ten artykuł dotyczy metody unikania nazywania powiązanych zmiennych w rachunku lambda. Aby zapoznać się z alternatywną składnią wyrażeń lambda, zobacz notację De Bruijn .

W logice matematycznej indeks De Bruijna jest narzędziem wynalezionym przez holenderskiego matematyka Nicolaasa Goverta de Bruijna do reprezentowania terminów rachunku lambda bez nazywania powiązanych zmiennych. Terminy zapisane przy użyciu tych indeksów są niezmienne w odniesieniu do konwersji α , więc sprawdzenie równoważności α jest takie samo, jak w przypadku równości składniowej. Każdy indeks De Bruijna jest liczbą naturalną , która reprezentuje wystąpienie zmiennej w terminie λ i oznacza liczbę elementów wiążących , które znajdują się w zakresie między tym wystąpieniem a odpowiadającym mu elementem wiążącym. Oto kilka przykładów:

• Termin λ x . λ y . x , czasami nazywany kombinatorem K , jest zapisywany jako λ λ 2 z indeksami De Bruijna. Spoiwo dla wystąpienia x jest drugim λ w zakresie.
• Termin λ x . λ y . λ z . x z ( y z ) ( kombinator S ), z indeksami De Bruijna, wynosi λ λ λ 3 1 (2 1).
• Termin λ z . (λ y . y (λ x . x )) (λ x . z x ) to λ (λ 1 (λ 1)) (λ 2 1). Zobacz poniższą ilustrację, na której segregatory są kolorowe, a odniesienia są pokazane za pomocą strzałek.

Indeksy De Bruijna są powszechnie używane w systemach wnioskowania wyższego rzędu, takich jak zautomatyzowane dowodzenia twierdzeń i systemy programowania logicznego .

Definicja formalna

Formalnie λ-termy ( M , N , ...) zapisane przy użyciu indeksów De Bruijna mają następującą składnię (nawiasy dozwolone):

M , N , ... ::= n | MN | _ λ M

gdzie n — liczby naturalne większe od 0 — to zmienne. Zmienna n jest związana , jeśli mieści się w zakresie co najmniej n elementów wiążących (λ); w przeciwnym razie jest bezpłatny . Miejscem wiązania dla zmiennej n jest n- ty łącznik, którego dotyczy , zaczynając od wiązania najbardziej wewnętrznego.

Najbardziej prymitywną operacją na wyrazach λ jest podstawienie : zastąpienie wolnych zmiennych w wyrazie innymi wyrazami. Na przykład w β-redukcji (λ M ) N musimy

1. znajdź instancje zmiennych n ₁ , n ₂ , ..., n _k w M , które są ograniczone przez λ w λ M ,
2. zmniejsz wolne zmienne M , aby dopasować usunięcie zewnętrznego spoiwa λ, i
3. zamień n ₁ , n ₂ , ..., n _k na N , odpowiednio zwiększając każdorazowo zmienne wolne występujące w N , aby dopasować liczbę λ-segregatorów, pod którymi występuje odpowiednia zmienna, gdy N zastępuje jedno z n _ja .

Aby to zilustrować, rozważ zastosowanie

(λ λ 4 2 (λ 1 3)) (λ 5 1)

co może odpowiadać następującemu terminowi zapisanemu w zwykłej notacji

(λ x . λ y . z x (λ u . u x )) (λ x . w x ).

Po kroku 1 otrzymujemy wyraz λ 4 □ (λ 1 □), w którym zmienne przeznaczone do podstawienia zastępujemy prostokątami. Krok 2 zmniejsza wolne zmienne, dając λ 3 □ (λ 1 □). Na koniec w kroku 3 zastępujemy kwadraty argumentem, a mianowicie λ 5 1; pierwsze pudełko jest pod jednym segregatorem, więc zamieniamy je na λ 6 1 (czyli λ 5 1 ze zmiennymi wolnymi zwiększonymi o 1); drugi jest pod dwoma segregatorami, więc zastępujemy go λ 7 1. Ostateczny wynik to λ 3 (λ 6 1) (λ 1 (λ 7 1)).

Formalnie podstawienie to nieograniczona lista terminów zapisywana jako M ₁ . M ₂ ..., gdzie M _i jest zamiennikiem dla i- tej zmiennej swobodnej. Operacja zwiększania w kroku 3 jest czasami nazywana przesunięciem i zapisywana ↑ ^k , gdzie k jest liczbą naturalną wskazującą wielkość zwiększenia zmiennych i jest zdefiniowana przez

${\ Displaystyle \ uparrow ^ {k} = (k + 1). (k + 2)....}$

⁰ Na przykład ↑ jest podstawieniem tożsamości, pozostawiając termin niezmieniony. Skończona lista terminów M ₁ . M ₂ ... M _n skraca podstawienie M ₁ . M ₂ ... M _n .(n+1).(n+2)... pozostawiając wszystkie zmienne większe od n bez zmian. Zastosowanie podstawienia s do terminu M jest zapisywane jako M [ s ]. Złożenie dwóch podstawień s ₁ i s ₂ jest zapisywane jako s ₁ s ₂ i jest określone przez

( M ₁ . M ₂ ...) s = M ₁ [ s ]. M ₂ [ s ]...

zaspokojenie własności

M [ s ₁ s ₂ ] = ( M [ s ₁ ]) [ s ₂ ],

a substytucja jest zdefiniowana na warunkach w następujący sposób:

${\ Displaystyle {\ rozpocząć {wyrównane} n [N_ {1} \ ldots N_ {n} \ ldots] = & N_ {n} \\ (M_ {1} \; M_ {2})[s]=&(M_{1}[s])(M_{2}[s])\\(\lambda \;M)[s]=&\lambda \;(M[1. s'])\\&{\text{gdzie }}s'=s\uparrow ^{1}\end{wyrównane}}}$

Kroki opisane powyżej dla redukcji β są zatem bardziej zwięźle wyrażone jako:

(λ M ) N → _β M [ N ].

Alternatywy dla indeksów De Bruijna

Podczas korzystania ze standardowej „nazwanej” reprezentacji terminów λ, w której zmienne są traktowane jako etykiety lub łańcuchy, należy jawnie obsługiwać konwersję α podczas definiowania dowolnej operacji na terminach. W praktyce jest to kłopotliwe, nieefektywne i często podatne na błędy. Doprowadziło to zatem do poszukiwania różnych reprezentacji takich terminów. Z drugiej strony nazwana reprezentacja terminów λ jest bardziej wszechobecna i może być bardziej natychmiast zrozumiała dla innych, ponieważ zmiennym można nadać nazwy opisowe. Tak więc, nawet jeśli system używa wewnętrznie indeksów De Bruijn, będzie prezentował interfejs użytkownika z nazwami.

Alternatywnym sposobem przeglądania indeksów De Bruijna są poziomy De Bruijna, które indeksują zmienne od dołu stosu, a nie od góry. Eliminuje to potrzebę ponownego indeksowania zmiennych wolnych, na przykład przy osłabianiu kontekstu, podczas gdy indeksy De Bruijna eliminują potrzebę ponownego indeksowania zmiennych powiązanych, na przykład przy zastępowaniu wyrażenia zamkniętego w innym kontekście.

Indeksy De Bruijna nie są jedyną reprezentacją terminów λ, która rozwiązuje problem konwersji α. Wśród nazwanych reprezentacji techniki nominalne Pittsa i Gabbaya, w których reprezentacja terminu λ jest traktowana jako klasa równoważności wszystkich terminów, które można do niego przepisać przy użyciu zmiennych permutacji. Takie podejście jest stosowane przez Nominal Datatype Package of Isabelle/HOL .

Inną powszechną alternatywą jest odwołanie się do reprezentacji wyższego rzędu , w których spoiwo λ jest traktowane jako prawdziwa funkcja. W takich reprezentacjach kwestie równoważności α, podstawienia itp. są utożsamiane z tymi samymi operacjami w metalogice .

Podczas rozumowania na temat metateoretycznych właściwości systemu dedukcyjnego w asystencie dowodowym czasami pożądane jest ograniczenie się do reprezentacji pierwszego rzędu i posiadanie umiejętności nazywania lub zmiany nazw założeń. Podejście lokalnie bezimienne wykorzystuje mieszaną reprezentację zmiennych — indeksy De Bruijna dla zmiennych powiązanych i nazwy dla zmiennych wolnych — która w razie potrzeby może skorzystać z α-kanonicznej formy indeksowanych terminów De Bruijna.

Konwencja zmiennych Barendregta

Konwencja zmiennych Barendregta to konwencja powszechnie stosowana w dowodach i definicjach, w których zakłada się, że:

• zmienne związane różnią się od zmiennych wolnych i
• wszystkie wiązania wiążą zmienne, które nie są jeszcze w zakresie.

W ogólnym kontekście definicji indukcyjnej nie jest możliwe zastosowanie konwersji α w razie potrzeby do konwersji definicji indukcyjnej przy użyciu konwencji na taką, w której konwencja nie jest używana, ponieważ zmienna może występować zarówno w pozycji wiążącej, jak i nie -obowiązująca pozycja w regule. Zasada indukcji obowiązuje, jeśli każda reguła spełnia następujące dwa warunki:

• reguła jest równoważna w sensie logiki nominalnej, to znaczy, że jej ważność pozostaje niezmieniona przez zmianę nazw zmiennych
• przy założeniu przesłanek reguły zmienne na wiążących pozycjach w regule są różne i są dowolne we wnioskowaniu

Zobacz też

• Notacja De Bruijna dla wyrazów λ.
• Logika kombinacyjna , bardziej istotny sposób na wyeliminowanie nazw zmiennych.