任何功能都可以缩减为无点形式吗?

Cub*_*bic 8 haskell lambda-calculus pointfree

许多功能可以简化为自由形式 - 但这对所有人来说都是如此吗?

例如,我不知道如何做到:

apply2 f x = f x x 
Run Code Online (Sandbox Code Playgroud)

Eri*_*ikR 10

逻辑组合子(即S,K,I组合子)本质上是无点形式的函数,而lambda演算相当于组合逻辑,所以我认为这表明答案是肯定的.

你的apply2功能的组合器是(如果我正确阅读的话):

((S((S(KS))K))(K((S((SK)K))((SK)K))))
Run Code Online (Sandbox Code Playgroud)

也被称为"云雀",来自Raymond Smullyan的Combinatory Birds页面.

(编辑输入 :)原来1以上相当于\f x -> f (x x).据"@gereeter"这里下面这的确是被称为"百灵鸟",而功能评论\f x -> f x x中的问题要求是"莺"从上述书(又名"W"组合子)W f x = S(S(K(S(KS)K))S)(KK)SI f x = S(S(KB)S)(KK)SI f x = CSI f x = SfIx = f x x.


1在这里:

((S((S(KS))K))(K((S((SK)K))((SK)K)))) f x =
  S( S(KS) K) (K( S( SK K) ( SK K)))  f x =   -- SKK    == I
  S (S(KS) K) (K( S  I       I    ))  f x =   -- S(KS)K == B
  S B         (K( S  I       I    ))  f x =
  Bf (K(SII)f) x = Bf (SII) x = f (SII x) = f (x x)
Run Code Online (Sandbox Code Playgroud)

  • @AndrewC虽然数据有点超出了lambda演算的范围,但它并不是*远远超出:有各种数据编码作为可以模拟总和,产品和递归类型的函数. (4认同)

Pet*_*lák 9

SK基础

正如已经提到的,使用适当的固定组合器组合,任何lambda术语都可以转换为仅使用那些组合器和函数应用程序的形式 - 没有lambda抽象(因此没有变量).众所周知的一组组合器是SK.Se 组合逻辑/ SK基础的完整性,用于描述该过程.组合器定义为

K x y    = x
S x y z  = (x z) (y z)
Run Code Online (Sandbox Code Playgroud)

有时包含身份组合I器,但它是多余的I = S K K.

单个组合基础

有趣的是,即使使用单个组合器,您也可以做到这一点.该丝毫语言使用

U f = (f S) K
Run Code Online (Sandbox Code Playgroud)

并且可以证明

I = (UU)
K = (U(U(UU)))
S = (U(U(U(UU))))
Run Code Online (Sandbox Code Playgroud)

因此,我们可以将任何lambda术语转换为二进制树,除了它的形状之外没有其他信息(所有叶子包含U,而节点代表函数应用程序).

更有效的基础S,K,I,B,C

但是,如果我们想要有点高效并获得合理大小的转换,那么使用I和引入两个更多的冗余组合器是有帮助的,这些组合被调用B并且C:

C f x y  = f y x
B f g x  = f (g x)
Run Code Online (Sandbox Code Playgroud)

这里C颠倒了参数的顺序,f并且B是函数组合.

这种添加显着减少了输出的长度.

这些组合器在Haskell中

实际上Haskell已经包含了某种形式的所有标准组合器.特别是:

I = id
K = const
  = pure :: a -> (r -> a)
S = (<*>) :: (r -> a -> b) -> (r -> a) -> (r -> b)
B = (.)
  = (<$>) :: (a -> b) -> (r -> a) -> (r -> b)
C = flip
  = \k x -> k <*> pure x
Run Code Online (Sandbox Code Playgroud)

在那里pure,<*>并且<$>是从功能上Applicative仿函数类型的类,我们在这里专门为读者单子(->) r.

所以在你的情况下,我们可以写

apply2 = (<*>) `flip` id
Run Code Online (Sandbox Code Playgroud)

为什么读者monad?

在抽象消除的过程中,我们尝试将形式的术语?x -> M :: r -> a(其中r的类型xa类型M)转换为不具有的形式x.我们通过递归处理来完成此操作,M然后我们将其每个类型的子项b(可能包含x)转换为类型r -> b(不包含x)的函数,然后我们将这些子项组合在一起.这就是读者monad的设计目的:将类型的功能组合r -> something在一起.

有关详细信息,请参阅Monad Reader,第17期:读者Monad和抽象消除.

数据结构怎么样?

为了构造数据结构,我们只使用它们的构造函数,这里没有问题.

为了解构它们,我们需要一些方法来摆脱模式匹配.这是编译器在编译功能程序时必须执行的操作."功能编程语言的实现"第5章:模式匹配的有效编译中描述了这样的过程.我们的想法是,对于每种数据类型,我们都有一个案例函数,用于描述如何解构(折叠)数据类型.例如,对于列表来说foldr,对于Either它来说either,让我们说它是4元组

caseTuple4 :: (a -> b -> c -> d -> r) -> (a,b,c,d) -> r
caseTuple4 f (a,b,c,d) = f a b c d
Run Code Online (Sandbox Code Playgroud)

因此,对于每种数据类型,我们添加其构造函数,解构的case函数,并将模式编译到此函数中.

举个例子,我们来表达一下

map :: (a -> b) -> [a] -> [b]
map f []        = []   
map f (x : xs)  = f x : map f xs
Run Code Online (Sandbox Code Playgroud)

这可以用以下表达foldr:

map f = foldr (\x xs -> f x : xs) []
Run Code Online (Sandbox Code Playgroud)

然后使用我们之前讨论过的组合器进行转换:

map = (foldr . ((.) (:))) `flip` []
Run Code Online (Sandbox Code Playgroud)

您可以验证它确实符合我们的要求.

另请参见系统F数据结构,该结构描述了如果我们启用更高级别的类型,数据结构如何可以直接编码为函数.

结论

是的,我们可以构造一组固定的组合器,然后将任何函数转换为仅使用这些组合器和函数应用程序的无点样式.


And*_*ewC 5

有很多函数看起来可能不是,但是可以用点自由风格表达,但是为了得到一个没有的函数,你可以快速定义一个适用于没有任何标准的极大元组的函数.功能.

我认为这种事情不太可能是无表情的,不是因为复杂性,而是因为这个大小的元组功能不多:

weird (a,b,c,d,e,f,g,h,i,j) = (a<*>b,c++d,e^f+a,g ()-h 4+e,j <*> take f i)
Run Code Online (Sandbox Code Playgroud)

你的例子:

apply2 :: (b -> b -> a) -> (b -> a)
apply2 = join
Run Code Online (Sandbox Code Playgroud)

这是join读者monad((->) b)

join :: Monad m => m (m a) -> m a
Run Code Online (Sandbox Code Playgroud)

所以在这种情况下

join :: ((->) b) ((->) b a) -> ((->) b) a
join :: ((->) b) (b -> a) -> (b -> a)
join :: (b -> (b -> a)) -> (b -> a)
join :: (b -> b -> a) -> (b -> a)
Run Code Online (Sandbox Code Playgroud)

比我们预期的更多功能有无点版本,但是一些无点表达式完全混乱.有时最好是明确而不是简洁.