Czy rachunek lambda i logika kombinacyjna są takie same?

Obecnie czytam „ Lambda-Calculus and Combinators ” Hindleya i Seldina. Nie jestem ekspertem, ale zawsze interesowałem się rachunkiem lambda ze względu na zaangażowanie w programowanie funkcjonalne (zaczynając od Lisp i SICP, a teraz od R i Haskell).

W „ Binary rachunek lambda i rachunek kombinatorów” , John Tromp stwierdza:

CL można postrzegać jako podzbiór rachunku lambda ... teorie są w dużej mierze takie same, stając się równoważne w obecności zasady ekstensywności.

W jakich warunkach należałoby zastosować logikę kombinacyjną zamiast rachunku lambda ?

Wszelkie referencje będą mile widziane.

To, co wyróżnia logikę kombinatoryczną, to brak zmiennej. Czasami jest to przydatne w metamatematyce i logice filozoficznej, gdzie status zmiennych jest trudny.

Może być również przydatny w implementacjach, ponieważ zarządzanie zmiennymi może być uciążliwe. Por. Np. Hughes, 1982, Super-kombinatory: nowa metoda implementacji języków aplikacji

Odwoływanie się do komentarza Jana Tromp, chcę uwagą, że rachunek kombinatorów czuje się bardzo różni się od rachunku lambda. Ponieważ twoje zainteresowanie wynika z programowania funkcjonalnego, tak naprawdę nie chcesz wiedzieć zbyt wiele o logice kombinatorycznej.

Mój ulubiony samouczek na temat logiki kombinatorycznej znajduje się w tych notatkach z wykładów na Uniwersytecie Cambridge.

Zostały one jednak wprowadzone w celu wyjaśnienia implementacji tak zwanych leniwych (lub aplikacyjnych) języków; jak wspomniano w poprzednim komentarzu, takie techniki są obecnie nieaktualne.