Czy kombinacyjne terminy logiczne są zawsze większe?

Istnieje więc algorytm konwertujący warunki rachunku lambda na logikę kombinatoryczną za pomocą kombinatorów SK. Produkuje rzeczy, które eksplodują wielkością. Chciałbym dowiedzieć się więcej o tej eksplozji w rozmiarze. Nie mogę jednak wymyślić lepszego algorytmu. Słyszałem, że języki funkcjonalne są praktycznie kompilowane z kombinatorami, więc wydaje się, że musi istnieć lepszy algorytm. Przejrzałem artykuł Davida Turnera na ten temat, a on po prostu mówi, aby zastosować kilka optymalizacji i że powodują one „znaczną poprawę”.

Czy „znaczna poprawa” oznacza, że ​​rozmiar spada tylko do wielomianu? Czy istnieje znany sposób na przekształcenie terminów lambda w logikę kombinatoryczną przy jedynie zwiększeniu wielkości wielomianu (lub mniej?)? Jeśli taki algorytm istnieje, to czy jest on praktyczny?

nie jest ekspertem w tej dziedzinie, ale oto dwie prace historyczne, które wydają się być ściśle związane z pytaniem i jest to prawdopodobnie półaktywny obszar badań. Turner zaproponował zestaw kombinatorów, które można sprowadzić do kombinatorów SK. ten następny artykuł dowodzi, że kombinatory Turnera nawet nie zredukowane do kombinatorów SK prowadzą do wykładniczego wybuchu (i przypuszczalnie redukcja do SK byłaby jeszcze większa). ale drugi artykuł mówi, że istnieje wydajny algorytm kosmiczny O (n log n) oparty na kombinatorach Turnera. (wygląda na to, że poczyniono twierdzenia dotyczące wydajności wielomianowej, które są uważane za nie w pełni wykazane / niesprawdzone, a zatem są uważane za domniemania ...

• Co to jest skuteczne wdrożenie rachunku λ? / Frandsen, Sturtivant (1991) (patrz str. 18)

  Ponadto pokazujemy, że implementacje oparte na kombinatorach Turnera lub super-kombinatorach Hughesa mają złożoność , tj. Wykładniczą dolną granicę. Otwarte jest, czy istnieje jakakolwiek implementacja złożoności wielomianowej , chociaż domniemano, że niektóre implementacje mają tę złożoność.$2^{Ω(ν)}$$ν^{O(1)}$

• Tłumaczenie Turner Combinators w przestrzeni O (n log n) / Noshita (1985)

  Przedstawiono praktyczną metodę reprezentacji kombinatorów Turnera, która w najgorszym przypadku potrzebuje tylko przestrzeni O (n log n) do tłumaczenia wyrażeń lambda długości n.