无点组合子中的模式,如何与SKI微积分相关



作为练习,我将以下组合符转换为无点符号:

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

通常约定fgh为函数,xyz为表达式。(这不是作业问题,只是为了好玩,看看我是否理解无点转换。)

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)

"组合"one_answers"反向组合"操作的结构(数目和顺序)似乎与原组合子的结构有某种联系。

我认为这与组合逻辑和SKI微积分有直接关系。我的问题是:

  1. 有没有更有见识的人能解释一下这里发生了什么:无点组合子中的"组合"one_answers"反向组合"的结构与有点组合子中的函数和表达式的结构有什么关系?

  2. 这是否可以推广到任意组合子(即函数的数量,表达式的数量及其顺序是任意的)?更具体地说,每个组合子都可以用"组合"one_answers"反向组合"来表示吗?是否有一种方案可以直接从指向组合子的结构派生出"组合"one_answers"反向组合"的组合(即不经过完整的重写过程)?例如,是否有可能直接从查看函数结构中派生出 f g x y z -> (f x y) g z的无点版本?

  3. cr的组合逻辑名称是什么

更新:

从B, C, K, W系统来看,cB组合子,rCB。但是我仍然很乐意得到更多关于我的问题的见解,特别是问题1和2。

首先,通过组合形式的直接操作派生定义通常更容易:

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)

但是,如果您优先考虑您的规则应用程序并使其具有确定性,那么您应该总是得到相同的结果——这将取决于您应用规则的顺序。

最新更新