Помогите разобраться с разложением комбинатора в базисе

да зачем тебе это? просто накидай кнопочек на формочку

Сейчас осваиваю эссе Душкина

Уже ошибка.

Ψabcd = a(bc)(bd)

В смысле, \a b c d -> a (b c) (b d)? По какому базису? SKI?

Формальный алгоритм можно почитать здесь. Он будет чуть более общим, именно: любой терм M со свободными переменными a1, a2,..., an будет преобразовываться в эквивалентное ему выражение, содержащее только комбинаторы S, K, I и переменные a1...an (но не содержащее лямбда-абстракцию). В частности, если M — комбинатор, то результатом будет его разложение в базисе SKI.

Ну, поехали. Смотрим, каким может быть M. Он может быть

1) Переменной. Тогда это одна из переменных a1...an — значит, она же будет этим выражением.

2) Применением: M = N K. Преобразуем к нужному виду N и K по отдельности и запишем применение одного к другому.

3) Лямбда-абстракцией: M = \a -> N. Тогда N — некоторый лямбда-терм со свободными переменными a1, a2,..., an, a. Преобразуем его с помощью нашего алгоритма к некоторому выражению E с комбинаторами S, K, I и переменными a1...an, a. Теперь нам понадобится некая процедура (опишем её позже), которая преобразует выражение E в некое другое выражение вида F a, где F — выражение из комбинаторов S, K, I и переменных a1...an. Тогда терм M = \a -> N преобразуется в F.

Итак, процедура. На входе у нас выражение E (уже без лямбда-абстракций), состоящее из комбинаторов S, K и I, и переменных a1...an, a. На выходе — выражение F такого же вида, не содержащее переменную a, и такое, что F a эквивалентно E.

Смотрим, как устроено выражение E. Лямбда-абстракций нет, так что варианты следующие:

а) E = a. Тогда пусть F = I.

б) E — один из комбинаторов S, K, I, либо одна из переменных a1...an. Тогда F = K E.

в) E — применение одного выражения к другому: E = E1 E2. Применим нашу процедуру к E1 и E2, получив в результате выражения F1 и F2, такие, что E1 эквивалентно F1 a, а E2 эквивалентно F2 a. Тогда E эквивалентно (F1 a) (F2 a). Последнее эквивалентно S F1 F2 a, а значит можно взять F = S F1 F2.

Усё.

Применяем процедуру к терму \a b c d -> a (b c) (b d). Начнём с того, что это — лямбда абстракция по переменной a. Значит, надо начать с того, что преобразовать терм \b c d -> a (b c) (b d). Для этого надо сначала преобразовать терм \c d -> a (b c) (b d). Для этого, в свою очередь — терм \d -> a (b c) (b d). Ну, а для этого — терм a (b c) (b d). Этот терм уже в нужном виде, так что будут применены только шаги 1 и 2, которые оставят терм в том же виде.

Итак, в самом низу рекурсии мы преобразовали терм a (b c) (b d) к выражению a (b c) (b d). Поднимаемся на один шаг, продолжая преобразование терма \d -> a (b c) (b d). Нам нужно прогнать нашу процедуру для выражения a (b c) (b d), сведя его к виду F d. Мы немножко схалявим: в процедуре выражение, скажем, b c преобразуется к S (K b) (K c), а мы будем поступать проще, преобразуя его сразу к K (b c).

Наша процедура требует, для начала, прогнать её же отдельно для a (b c) и b d. Результат первого преобразования — K (a (b c)) (мы схалявили), второго — ну, тут тоже можно чуток схалявить, и взять не S (K b) I, а просто b. Третий шаг теперь даст для выражения a (b c) (b d) результат S (K (a (b c))) b. Итого, терм \d -> a (b c) (b d) сводится к S (K (a (b c))) b.

Продолжаем преобразовывать терм \c d -> a (b c) (b d). Нам нужно прогнать нашу процедуру для S (K (a (b c))) b, сведя это дело к виду F c. Процедура, прогоняемая почти честно, даст результат S (S (K S) (S (K K) (S (K a) b))) (K b). Схалявим мы тут только в одном месте, преобразовав b c не к S (K b) I, а просто к b.

Продолжаем преобразовывать терм \b c d -> a (b c) (b d). Для этого нашу процедуру надо прогнать для выражения S (S (K S) (S (K K) (S (K a) b))) (K b), сведя его к виду F b. Делаем:

S (S (K S) (S (K K) (S (K a) b))) (K b) — применение
1. S (S (K S) (S (K K) (S (K a) b))) — применение
    1.1 S — сводится к K S b
    1.2 S (K S) (S (K K) (S (K a) b)) — применение
        1.2.1 S (K S) — сводится к K (S (K S)) b
        1.2.2 S (K K) (S (K a) b) — применение
            1.2.2.1 S (K K) — сводится к K (S (K K)) b
            1.2.2.2 S (K a) b — уже в нужном виде
        S (K K) (S (K a) b)) сводится к S (K (S (K K))) (S (K a)) b
    S (K S) (S (K K) (S (K a) b)) сводится к S (K S) (S (K (S (K K))) (S (K a))) b
2. K b — можно бы преобразовать, но оно уже в нужном виде
Итого, результат — S (S (K S) (S (K (S (K K))) (S (K a)))) K

Наконец, терм \a b c d -> a (b c) (b d). Мы вернулись на верхний уровень рекурсии, и теперь выражение S (S (K S) (S (K (S (K K))) (S (K a)))) K нужно преобразовать к виду F a. Это самое F и будет ответом.

S (S (K S) (S (K (S (K K))) (S (K a)))) K — применение
1. S (S (K S) (S (K (S (K K))) (S (K a)))) — применение
    1.1 S сводится к K S a
    1.2 S (K S) (S (K (S (K K))) (S (K a))) — применение
        1.2.1 S (K S) сводится к K (S (K S)) a
        1.2.2 S (K (S (K K))) (S (K a)) — применение
            1.2.2.1 S (K (S (K K))) сводится к K (S (K (S (K K)))) a
            1.2.2.2 S (K a) — применение
                1.2.2.2.1 S сводится к K S a
                1.2.2.2.2 K a сводится к K a
            S (K a) сводится к S (K S) K a
        S (K (S (K K))) (S (K a)) сводится к S (K (S (K (S (K K))))) (S (K S) K) a
    S (K S) (S (K (S (K K))) (S (K a))) сводится к S (K (S (K S))) (S (K (S (K (S (K K))))) (S (K S) K)) a
2. K сводится к K K a
Итого, S (S (K S) (S (K (S (K K))) (S (K a)))) K сводится к:
    S (S (K (S (K S))) (S (K (S (K (S (K K))))) (S (K S) K))) (K K) a

Значит, окончательный ответ: S (S (K (S (K S))) (S (K (S (K (S (K K))))) (S (K S) K))) (K K)

Мм, сразу вопрос, почему Ψabcd - лямбда абстракция (λa.bcd -я ничего не путаю?), как я понял из задания - это просто комбинатор.

И вот такое обозначение \ - оно что значит?

Если честно, я выпал в осдадок.

Итак, в самом низу рекурсии мы преобразовали терм a (b c) (b d) к выражению a (b c) (b d).

Какая разница между «термом» и «выражением» ?

Что такое Ψ?

И вот такое обозначение \ - оно что значит?

Как всякий хаскеллист, я привык писать вместо лямбды бэкслэш.

Какая разница между «термом» и «выражением» ?

Я имею в виду выражение в комбинаторном исчислении. То есть, оно составляется из базовых элементов — комбинаторов SKI и переменных — с помощью только одной операции применения.

Спасибо, более менее разобрался. Ещё один, чисто формальный вопрос, что обозначают вот такие штуки? http://itmages.ru/image/view/1333702/36a3942f Меня интересуют B^2 и циферки в квадратных скобках.

А шут его знает.