Шаблон в бессмысленном комбинаторе, как это связано с исчислением SKI

Question

В качестве упражнения я преобразовал следующий комбинатор в бессмысленную запись:

h f g x y z = f x (g y z)

с обычным соглашением f, g, h как функции, и x, y, z как выражения. (Это не домашняя проблема, а просто для удовольствия и для того, чтобы понять, понимаю ли я бессмысленные преобразования.)

После длительного ручного процесса переписывания ghciЯ закончил со следующим:

h = ((flip (.)) (flip (.)) . (flip (.))) . ((.)(.))

Я заметил, что h состоит только из двух комбинаторов, "составь" (.) и "обратное сочинение" flip (.), При этом оригинальный комбинатор можно записать кратко как:

c = (.) -- compose
r = flip c -- "reverse compose"
h = ((r r) . r) . (c c)
   = c(c(r r)r)(c c)

Структура (число и порядок) операций "составлять" и "обратное составление", похоже, как-то связаны со структурой исходного комбинатора.

Я считаю, что это напрямую связано с комбинаторной логикой и исчислением СКИ. Мои вопросы таковы:

1. Может ли кто-нибудь с большей проницательностью объяснить, что здесь происходит: как структура "составить" и "выполнить обратное построение" в бессмысленном комбинаторе связана со структурой функций и выражений в точечном комбинаторе?

2. Можно ли это обобщить на произвольные комбинаторы (т. Е. Количество функций, количество выражений и их порядок произвольно)? Более конкретно, может ли каждый комбинатор быть выражением в терминах "составлять" и "обратное составление", и существует ли схема для получения комбинации "составлять" и "обратное составление" непосредственно из структуры точечного комбинатора (т.е. без проходит полный процесс переписывания)? Например, можно ли напрямую получить бессмысленные версии \ f g x y z -> (f x y) g z просто глядя на структуру функции?

3. Какое имя в комбинаторной логике для c а также r?

Обновить:

Кажется, что c это B комбинатор и r является CB из системы B, C, K, W. Но я все равно был бы рад получить более глубокое понимание моих вопросов, особенно вопросов 1 и 2.

Answer 1

Во-первых, обычно проще получить определения путем прямого манипулирования в комбинаторной форме:

h f g x y z = f x (g y z)
            = B(fx)(gy)z     -- B rule
            = B(B(fx))gyz    -- B rule
h f g x = B(B(fx))g          -- eta-contraction
        = BBB(fx)g           -- B rule
        = B(BBB)fxg          -- B rule
        = C(B(BBB)f)gx       -- C rule
h f = C(B(BBB)f)             -- eta-contraction
    = BC(B(BBB))f            -- B rule
h   = BC(B(BBB))             -- eta-contraction
 -- = B(B(CB(CB))(CB))(BB)   -- your expression

Типы одинаковы, хотя мое выражение короче. Может ли это служить контрпримером к тому, должна ли комбинаторная форма каким-то образом следовать данному определению? В применении правил существует значительная свобода, поэтому могут быть получены различные формы. Я не думаю, что из определенного комбинаторного выражения можно получить много понимания.

Во всяком случае, комбинаторы, которые появляются в окончательном переводе, являются более репрезентативными для предпринятых шагов деривации, и их можно свободно выбирать среди тех, которые подходят, в любой заданной точке.

Например, следующий шаг при выводе выражения обычно делается следующим образом:

g(fx) = Bgfx = CBfgx 

B (B (CB(CB)) (CB)) (BB) f g x y z
   = B (CB(CB)) (CB) (BB f) g x y z
   = CB (CB) (CB (BB f)) g x y z     --   and here
   = CB (BB f) (CB g) x y z          --  here
   = CB g (BB f x) y z               -- here
   = BB f x (g y) z
   = B (f x) (g y) z
   = f x (g y z)

Но если вы расставите приоритеты в применении правил и сделаете их детерминированными, вы всегда должны получать один и тот же результат, который будет зависеть от порядка, в котором вы применяете правила.