函数组合VS函数应用程序 [英] Function Composition VS Function Application

问题描述

这是函数组合运算符的定义吗？

 （。）::（b  - > c） - > （a  - > b） - > a  - > c 
 f。 g = \ x  - > f（gx）
  

两个函数，并返回一个函数，但我记得有人已经表达了英语的逻辑像

男孩是人类 - >阿里是男孩 - >阿里是人类

1. 这个逻辑与函数组合有关吗？


2. 函数应用和组合的强绑定是什么意思，一个是比另一个更强的绑定？

请帮助。

谢谢。

第一次错过了几个问题的组成部分;请参阅我答案的底部。）

想想这种说法的方法是查看类型。你所拥有的论证形式被称为三段论;不过，我认为你错误地记住了一些事情。有很多不同类型的三段论，就我所知，你的三段论不符合功能组成。让我们考虑一种三段论：

1. 如果阳光明媚，我会变热。


2. 如果我变热，我会去游泳。
因此，如果阳光充足，我会去游泳。

这被称为 假想三段论 。在逻辑上，我们可以这样写：如果S 代表阳光明媚的主张，那么让H表示我会变热的主张， ，而让W 代表我会去游泳的主张。为β指定β，并为因此写∴，我们可以翻译α→β以上为：

1. S → H


2. H → W


3. S

当然，如果我们替换 S ， H ， 与任意α，β和γ。现在，这应该看起来很熟悉。如果我们将含义箭头→改为箭头 - > ，这就变成了

1. a - > b


2. b - > c


3. ∴ a - > c

另外，我们有组合运算符类型的三个组件！想想这是一个合乎逻辑的三段论，你可以考虑以下几点：

1. 如果我有一个类型值一个，我可以产生一个类型的值 b 。


2. 如果我有一个 b ，我可以生成一个类型为 c 的值
。

3. 因此，如果我有 a 类型的值，则可以生成类型为 c 的值。

这应该是有道理的：在 f中。 g ，存在一个函数 g :: a - > b 告诉你前提1为真，并且 f :: b - > c 告诉你前提2是正确的。因此，您可以总结最后的声明，其中函数 f。 g :: a - > c 是见证人。

我不完全确定你的三段论的意思。这几乎是 modus ponens 的实例，但并不完全。 Modus ponens参数采用以下形式：

1. 如果下雨，那么我会弄湿。
   
2. 正在下雨。


3. 因此，我会弄湿。
   

为it is raining写作 R ， w 为我会弄湿，这给了我们逻辑形式

1. R → W


2. R >


3. W

替换含义箭头功能箭头为我们提供了以下内容：

1. a - > b


2. a


3. ∴ b

这就是函数应用程序，正如我们从（$）::（a - > b） - > a - > B'/ code>。如果你想把它看作是一个逻辑论证，它可能是这样的形式：





1. 如果我有一个<$ c类型的值$ c> a ，我可以生成一个类型为 b 的值。
   
2. 键入 a 。


3. 因此，我可以生成 b 。

这里，考虑表达式 fx 。函数 f :: a - > b 证明了命题1的真实性;值 x :: a 是命题2的真相的见证;因此结果可以是类型 b ，证明结论。这正是我们从证明中发现的。

现在，您的原始三段论格式如下：

1. 所有男孩都是人。
。

让我们将其转换为符号。 Bx 表示 x 是男孩; x 表示 x 是人类; a 表示阿里;和∀ x 。 表示对于 x 的所有值，φ都是true。然后我们有

1. ∀ x 。 Bx → Hx


2. Ba


3. ∴ Ha

这几乎是modus ponens，但它需要实例化forall。虽然逻辑上有效，但我不确定如何在类型系统级别解释它;如果有人愿意帮忙，我就会全神贯注。一个猜测将是一个二级类型，如（forall x。B x - > H x） - > B a - > H a ，但我几乎可以肯定那是错误的。另一种猜测是简单的类型，如（B x - > H x） - > B Int - > H Int ，其中 Int 代表Ali，但我几乎可以肯定这是错误的。再说一遍：如果你知道，请让我知道！

最后一个音符。以这种方式来看事物 - 遵循证明和程序之间的联系 - 最终导致了库里霍华德同构，但这是一个更高级的话题。 （这真的很酷，但！！）

---

编辑1：您还需要一个示例的功能组成。这里有一个例子。假设我有一个人的中间名列表。我需要构建所有中间名首字母的列表，但要做到这一点，我首先必须排除每个不存在的中间名。排除中间名为空的所有人很容易;我们只是 中间名不是 的所有人都使用过滤器（\mn - >不是$ null mn）middleNames 。同样，我们可以很容易地用 head 获取某人的中间首字母，因此我们只需要 map head filteredMiddleNames 即可得到清单。换句话说，我们有以下代码：

  allMiddleInitials :: [Char] 
 allMiddleInitials = map head $ filter （\mn  - > not $ null mn）middleNames 
  

但是，我们确实需要一个中间初始化函数。所以让我们把它变成一个：

  getMiddleInitials :: [String]  - > [Char] 
 getMiddleInitials middleNames =地图标题$ filter（\mn  - > not $ null mn）middleNames 
  

现在，让我们看看一些有趣的事情。函数 map 的类型为（a - > b） - > [a] - > [b] ，并且自头的类型为 [a] - > a ，地图标题的类型为 [[a]] - > [α] 。类似地， filter 具有类型（a - > Bool） - > [a] - > [a] ，所以过滤器（\mn - >不是$ null mn）的类型为 [a] - > [α] 。因此，我们可以删除参数，而不是写入



   - 类型也更通用
 getFirstElements :: [[a]]  - > [a] 
 getFirstElements =地图头。过滤器（非空）
  

你看到我们有一个组合奖金实例： not 的类型为 Bool - > Bool 和 null 的类型为 [a] - > Bool ，所以不是。 null 的类型为 [a] - > Bool ：它首先检查给定列表是否为空，然后返回它是否不是。顺便说一下，这种转变将功能变成了无点式;也就是说，结果函数没有明确的变量。

你还问到了强绑定。我认为你指的是。和 $ 运算符（也可能是函数应用程序）的优先级）。在Haskell中，正如算术一样，某些运算符比其他运算符具有更高的优先级，因此绑定更紧密。例如，在表达式 1 + 2 * 3 中，这被解析为 1 +（2 * 3）。这是因为在Haskell中，以下声明有效：

  infixl 6 + 
 infixl 7 * 
  

数字越高（优先级别），该运算符被调用的越快，因此，运算符绑定。函数应用程序有效地具有无限的优先级，因此它最紧密地绑定在一起：表达式 fx％gy 将被解析为（fx）％（gy） code>用于任何操作符％。 。（composition）和 $ （应用程序）操作符具有以下固定声明：

  infixr 9。 
 infixr 0 $ 
  

优先级从零到九，所以这就是说。运算符比其他任何函数（函数应用程序除外）都紧密绑定，并且 $ 紧紧地 。因此，表达式 f。 g $ h 将解析为（f。g）$ h ;实际上，对于大多数运营商而言， f。 g％h 将是（f。g）％h 和 f％g $ h 将会是 f％（g $ h）。 （唯一的例外是罕见的其他零个或九个优先运算符。）

1. Do anyone can give example of function composition?

2. This is the definition of function composition operator?

   (.) :: (b -> c) -> (a -> b) -> a -> c
   f . g = \x -> f (g x)
   

This shows that it takes two functions and return a function but i remember someone has expressed the logic in english like

boy is human -> ali is boy -> ali is human

1. What this logic related to function composition?
2. What is the meaning of strong binding of function application and composition and which one is more strong binding than the other?

Please help.

Thanks.

解决方案

(Edit 1: I missed a couple components of your question the first time around; see the bottom of my answer.)

The way to think about this sort of statement is to look at the types. The form of argument that you have is called a syllogism; however, I think you are mis-remembering something. There are many different kinds of syllogisms, and yours, as far as I can tell, does not correspond to function composition. Let's consider a kind of syllogism that does:

1. If it is sunny out, I will get hot.
2. If I get hot, I will go swimming.
3. Therefore, if it is sunny about, I will go swimming.

This is called a hypothetical syllogism. In logic terms, we would write it as follows: let S stand for the proposition "it is sunny out", let H stand for the proposition "I will get hot", and let W stand for the proposition "I will go swimming". Writing α → β for "α implies β", and writing ∴ for "therefore", we can translate the above to:

1. S → H
2. H → W
3. ∴ S → W

Of course, this works if we replace S, H, and W with any arbitrary α, β, and γ. Now, this should look familiar. If we change the implication arrow → to the function arrow ->, this becomes

1. a -> b
2. b -> c
3. ∴ a -> c

And lo and behold, we have the three components of the type of the composition operator! To think about this as a logical syllogism, you might consider the following:

1. If I have a value of type a, I can produce a value of type b.
2. If I have a value of type b, I can produce a value of type c.
3. Therefore, if I have a value of type a, I can produce a value of type c.

This should make sense: in f . g, the existence of a function g :: a -> b tells you that premise 1 is true, and f :: b -> c tells you that premise 2 is true. Thus, you can conclude the final statement, for which the function f . g :: a -> c is a witness.

I'm not entirely sure what your syllogism translates to. It's almost an instance of modus ponens, but not quite. Modus ponens arguments take the following form:

1. If it is raining, then I will get wet.
2. It is raining.
3. Therefore, I will get wet.

Writing R for "it is raining", and W for "I will get wet", this gives us the logical form

1. R → W
2. R
3. ∴ W

Replacing the implication arrow with the function arrow gives us the following:

1. a -> b
2. a
3. ∴ b

And this is simply function application, as we can see from the type of ($) :: (a -> b) -> a -> b. If you want to think of this as a logical argument, it might be of the form

1. If I have a value of type a, I can produce a value of type b.
2. I have a value of type a.
3. Therefore, I can produce a value of type b.

Here, consider the expression f x. The function f :: a -> b is a witness of the truth of proposition 1; the value x :: a is a witness of the truth of proposition 2; and therefore the result can be of type b, proving the conclusion. It's exactly what we found from the proof.

Now, your original syllogism takes the following form:

1. All boys are human.
2. Ali is a boy.
3. Therefore, Ali is human.

Let's translate this to symbols. Bx will denote that x is a boy; Hx will denote that x is human; a will denote Ali; and ∀x. φ says that φ is true for all values of x. Then we have

1. ∀x. Bx → Hx
2. Ba
3. ∴ Ha

This is almost modus ponens, but it requires instantiating the forall. While logically valid, I'm not sure how to interpret it at the type-system level; if anybody wants to help out, I'm all ears. One guess would be a rank-2 type like (forall x. B x -> H x) -> B a -> H a, but I'm almost sure that that's wrong. Another guess would be a simpler type like (B x -> H x) -> B Int -> H Int, where Int stands for Ali, but again, I'm almost sure it's wrong. Again: if you know, please let me know too!

And one last note. Looking at things this way—following the connection between proofs and programs—eventually leads to the deep magic of the Curry-Howard isomorphism, but that's a more advanced topic. (It's really cool, though!)

---

Edit 1: You also asked for an example of function composition. Here's one example. Suppose I have a list of people's middle names. I need to construct a list of all the middle initials, but to do that, I first have to exclude every non-existent middle name. It is easy to exclude everyone whose middle name is null; we just include everyone whose middle name is not null with filter (\mn -> not $ null mn) middleNames. Similarly, we can easily get at someone's middle initial with head, and so we simply need map head filteredMiddleNames in order to get the list. In other words, we have the following code:

allMiddleInitials :: [Char]
allMiddleInitials = map head $ filter (\mn -> not $ null mn) middleNames

But this is irritatingly specific; we really want a middle-initial–generating function. So let's change this into one:

getMiddleInitials :: [String] -> [Char]
getMiddleInitials middleNames = map head $ filter (\mn -> not $ null mn) middleNames

Now, let's look at something interesting. The function map has type (a -> b) -> [a] -> [b], and since head has type [a] -> a, map head has type [[a]] -> [a]. Similarly, filter has type (a -> Bool) -> [a] -> [a], and so filter (\mn -> not $ null mn) has type [a] -> [a]. Thus, we can get rid of the parameter, and instead write

-- The type is also more general
getFirstElements :: [[a]] -> [a]
getFirstElements = map head . filter (not . null)

And you see that we have a bonus instance of composition: not has type Bool -> Bool, and null has type [a] -> Bool, so not . null has type [a] -> Bool: it first checks if the given list is empty, and then returns whether it isn't. This transformation, by the way, changed the function into point-free style; that is, the resulting function has no explicit variables.

You also asked about "strong binding". What I think you're referring to is the precedence of the . and $ operators (and possibly function application as well). In Haskell, just as in arithmetic, certain operators have higher precedence than others, and thus bind more tightly. For instance, in the expression 1 + 2 * 3, this is parsed as 1 + (2 * 3). This is because in Haskell, the following declarations are in force:

infixl 6 +
infixl 7 *

The higher the number (the precedence level), the sooner that that operator is called, and thus the more tightly the operator binds. Function application effectively has infinite precedence, so it binds the most tightly: the expression f x % g y will parse as (f x) % (g y) for any operator %. The . (composition) and $ (application) operators have the following fixity declarations:

infixr 9 .
infixr 0 $

Precedence levels range from zero to nine, so what this says is that the . operator binds more tightly than any other (except function application), and the $ binds less tightly. Thus, the expression f . g $ h will parse as (f . g) $ h; and in fact, for most operators, f . g % h will be (f . g) % h and f % g $ h will be f % (g $ h). (The only exceptions are the rare few other zero or nine precedence operators.)

这篇关于函数组合VS函数应用程序的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！