| 12:43a |
Сделал синтез комбинаторов брутфорсом. Т.е. сгенерировать все термы длины < n+1, редуцировать их и сравнить правую часть с данной. Редукция на схемовских списках, в базисе SKI.
Пока не могу понять, как легче всего вычислить арность комбинатора. На данный момент применяю к k переменным (от 1 до K=26), и смотрю, остаются ли базисные комбинаторы в правой части. Но не все генерированные термы являются комбинаторами. Как их отличить от комбинаторов с арностью выше К?
Перебор для n=5 занимает 1 с. Для n=6 должно быть не более 10*25=250 с, но я не дождался. Значит, получился бесконечный цикл редукции.
Вот, где дебаггер пригодился. Таки да, классика жанра, комбинатор SII(SII), т.е. ММ - дупликатор, применённый к себе (Ma = aa).
Сейчас я останавливаю редукцию, когда она сходится (ещё одна редукция не меняет терм). А здесь она не сходится, а осциллирует: SII(SII) = I(SII)(I(SII)) = SII(SII) = I(SII)(I(SII)) = ... Надо продумать другую эвристику для проблемы останова. Но так, чтобы не сильно замедляла перебор. |