Продвинулся на шажок в синтезе комбинаторов. Проблему останова решаю простейшим образом - разрешаю не более 20 редукций. Теперь за час генерируются все комбинаторы (точнее, термы) в базисе SKI с длиной 8 (их ~3 млн.).

Однако, половину времени уходит на сборку мусора. И если разрешить побольше редукций, то уже в 4 гигабайта не влазит, явно там какой-нибудь бесконечно разрастающийся комбинатор пасётся. Ограничить, что-ли, и по длине при редукции? Накладно, однако, получится.

Не пора ли заканчивать с брутфорсом здесь? "Изобрести" прямой вывод? Только что-то не придумывается оно. Придётся в литературу подглядывать. Или побаловаться ещё... параллельной редукцией, к примеру.