Wen die verschieden combinator-Arten interessieren, dem kann ich da nur die Wikipedia ans Herz legen
Ich hab den Y-Combinator in meiner Bachelor-Arbeit gebraucht, um zu zeigen, dass meine rein funktionale Teilmenge von JavaScript turing-vollständig ist.
Seit einiger Zeit arbeite ich außerdem an einer kleinen Spielzeug-Programmiersprache, die rein auf kombinatorischer Logik basiert und für Theorem-Proving benutzt werden kann. Inspiriert durch Joy und Kitten, allerdings absichtlich nicht turing-vollständig, um die Konsistenz des Beweis-Systems zu bewahren. Das ist im Moment die größte Schwierigkeit des Problems. Man glaubt nicht, wie schnell man aus Versehen ein System turing-vollständig macht und die Logik dadurch inkonsistent wird.