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}$

[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 , alecałkowita liczba wyraźnych powiązanych nazw zmiennych w  t t = ( λ x . x ( λ y . y ) ) ( λ x . λ y . y x ) α t α t ′ = ( λ x . x ( λ y . y ) ) ( λ a . λ b . b a ) t $t$

$$\text{the total number of distinct bound variable names in }t$$ $t = (\lambda x.x(\lambda y.y))(\lambda x.\lambda y.yx)$$\alpha$$t$$\alpha$$t' = (\lambda x.x(\lambda y.y))(\lambda a.\lambda b.ba)$$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$ $$\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$