haskell - 无点组合器中的模式，与 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 只包含两个组合子，“compose”(.) 和“reverse compose”flip (.)。有了这个，原来的组合器可以简洁地写成:

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

“组合”和“反向组合”操作的结构(数量和顺序)似乎与原始组合器的结构有某种关联。

我认为这与组合逻辑和 SKI 演算直接相关。因此，我的问题是:

1. 有更深入了解的人可以解释这里发生的事情吗:无点组合器中“组合”和“反向组合”的结构如何与有点组合器中的函数和表达式结构相关？

2. 这能否推广到任意组合器(即，函数的数量、表达式的数量，以及它们的顺序是任意的)？更具体地说，每个组合子都可以用“组合”和“反向组合”来表示吗？是否有一种方案可以直接从结构中导出“组合”和“反向组合”的组合pointful 组合器(即不经过完整的重写过程)？例如，是否可以仅通过查看函数结构直接导出 \f g x y z -> (f x y) g z 的无点版本？

3. c 和 r 在组合逻辑中的名称是什么？

更新:

似乎 c 是 B 组合器，r 是来自 B, C, K, W system 的 CB .但我仍然很乐意更深入地了解我的问题，尤其是问题 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)

但是，如果您确定规则应用的优先级并使其具有确定性，您应该始终会得到相同的结果——这将取决于您应用规则的顺序。