Niekompletna podstawa kombinacji

Jest to inspirowane tym pytaniem. Niech będzie zbiorem wszystkich kombinacji, które mają tylko dwie powiązane zmienne. Czy kombinatorycznie kompletny? $\mathcal{C}$ $\mathcal{C}$

Uważam, że odpowiedź jest przecząca, jednak nie udało mi się znaleźć odniesienia do tego. Byłbym również zainteresowany referencjami na dowody kombinatorycznej niekompletności zestawów kombinatorów (rozumiem, dlaczego zestaw składający się z kombinatorów z tylko jedną zmienną powiązaną jest niekompletny, więc te zestawy powinny zawierać więcej niż tylko elementy ). $\mathcal{D}$ $\mathcal{D}$

lo.logic lambda-calculus combinatory-logic

— tci
źródło

Czy możesz wyjaśnić, co masz na myśli przez liczbę powiązanych zmiennych kombinatora (= zamknięty termin lambda)? Całkowita liczba abstrakcji lambda?

— Noam Zeilberger,

Tak, o to mi chodziło.

— tci 27.07.16

Właściwie może to nie jest dokładnie to, co miałeś na myśli ... może raczej masz na myśli całkowitą liczbę różnych zmiennych używanych w abstrakcjach lambda, tak że na przykład ma dwie różne zmienne powiązane, pomimo posiadania czterech abstrakcji lambda? W takim przypadku wydaje się, że Rick Statman odpowiedział dokładnie na to pytanie (negatywnie) w „ Dwie zmienne to za mało ”.

(λ x . x (λ y . y)) (λ x . λ y . x y)

$(\lambda x.x(\lambda y.y))(\lambda x.\lambda y.x y)$

— Noam Zeilberger,

Dobrze. Myślę, że to była odpowiedź, której szukałem i zdecydowanie spodziewałem się, że będzie to wynik Statmana. Jeszcze nie sprawdziłem, ale myślę, że dałoby to również negatywną odpowiedź na pytanie, o którym wspomniałem. Jeśli opublikujesz je jako odpowiedź, chętnie je zaakceptuję.

— tci

[Rozszerzanie komentarza na odpowiedź.]

Po pierwsze, wyjaśnienie na temat zliczania zmiennych powiązanych w kombinatorze (= termin zamknięty) . Interpretuję to pytanie jako pytające o tak że na przykład termin liczy się jako posiadająca dwie zmienne powiązane, mimo że ma cztery spoiwa (tj. abstrakcje lambda). Ten sposób liczenia początkowo był dla mnie trochę dziwny, ponieważ nie jest niezmienny w przypadku konwersji : na przykład jest ekwiwalentny dla , ale $t$

łączna liczba wyraźnie powiązanych nazw zmiennych w t

$\text{the total number of distinct bound variable names in }t$

t = (λ x . x (λ y . y)) (λ x . λ y . y x)

$t = (\lambda x.x(\lambda y.y))(\lambda x.\lambda y.yx)$

α

$\alpha$

t

$t$

α

$\alpha$

t^{'} = (λ x . x (λ y . y)) (λ a . λ b . b a)

$t' = (\lambda x.x(\lambda y.y))(\lambda a.\lambda b.ba)$

t^{'}

$t'$ ma cztery różne powiązane nazwy zmiennych. Nie stanowi to jednak problemu, ponieważ minimalna liczba odrębnych powiązanych nazw zmiennych potrzebnych do napisania terminu zamkniętego jest równa a to drugie pojęcie jest niezmienne pod konwersja.

t

$t$

maksymalna liczba wolnych zmiennych w podtermie wynoszącym t

$\text{the maximum number of free variables in a subterm of }t$

α

$\alpha$

Niech będzie zbiorem wszystkich kombinacji, które można zapisać przy użyciu co najwyżej dwóch różnych zmiennych powiązanych, lub równoważnie zbiorem wszystkich kombinacji, których podtermy mają co najwyżej dwie dowolne zmienne. $\mathcal{C}$

Twierdzenie (Statman) : nie jest kombinatorycznie kompletne. $\mathcal{C}$

Wygląda na to, że oryginalny dowód na to zawiera raport techniczny Ricka Statmana:

Kombinatory dziedzicznie drugiego rzędu. Carnegie Mellon Departament Matematyczny Raport techniczny 88-33, sierpień 1988. ( pdf )

Statman definiuje zasadniczo izomorficzny zbiór kombinatorów, który nazywa „GORĄCYM”, jako „dziedzicznie drugiego rzędu”. Raport techniczny faktycznie pokazuje, że słowo problem (tj. jakość) dla HOT jest nierozstrzygalne, mimo że nie jest ono kombinatorycznie kompletne. Później Statman napisał krótki samodzielny artykuł z dowodem, że HOT nie jest kombinatorycznie kompletny w: $\beta$

Dwie zmienne to za mało. Materiały z 9. włoskiej konferencji na temat informatyki teoretycznej, s. 406–409, 2005. ( acm )

W każdym razie, jak ujęto w streszczeniu oryginalnego raportu technicznego, celem dowodu jest wykazanie, że HOT jest „hierarchią według poziomu definicji”. Oznacza to, że definiuje pojęcie rangi na gorący combinator i rodzinę kombinatorów , tak, że każdy ma rangę i nie jest -equivalent do dowolnej kombinacji gorącego kombinatorów rangi . Oznacza to, że HOT nie jest kombinatorycznie kompletny, ponieważ jeśli kombinator można uzyskać z kombinacji kombinatorów HOT rangi dla niektórych $Hn$ $Hn$ $n+1$ $\beta$ $n$ $S = \lambda x.\lambda y.\lambda z.(xz)(yz)$ $n$ $n$ , to może również każdy inny kombinator, w szczególności kombinator rangi . $Hn$ $n+1$

— Noam Zeilberger
źródło