问题标签 [equational-reasoning]

好吧，这是使用 foldr 的过滤器函数的定义：

例如，假设我有这个功能：

所以它将是：

这将是

这将是

这将是

这将是

foldr step [] []是这样的[]：

现在我们将真正进入step函数。
这是函数step内部的定义myFilter，从上面：

另外，我提醒您这p实际上是odd我们示例中的功能。

好吧，我们又来了：

和

x = 4在最里面step，4并不奇怪，所以我们返回ys，即[]

所以现在我们得到了这个：

现在，在最内在step的x = 3, 和3是奇数，所以我们返回x:ys，即3 : []，即[3]，现在我们得到：

现在，在内部step,x = 2和2不是奇数，所以我们返回ys，即[3]，所以现在我们将得到：

现在，x = 1和1是奇数，所以我们返回x : ys，即1 : [3]，即[1,3]。

结束 ：-）。

我的所有动作都正确吗？
多谢 ：-）。

ps 的定义myFilter来自《Real World Haskell 》一书第 4 章。

我试图证明以下函数是正确的，并且很难弄清楚，即使它看起来很明显！

通过这样做，我只需要使用以下函数证明 (app (rev x) (rev y)) 等效于 (rev (app xy))))：

这就是我做另一个的方式（希望是正确的）

“反向附加东西”

= 转速的定义

= rev 的输出合约

= "反向追加事物"

= rev 的输出合约

= len 的定义

= rev 的输出合约

我理解简单的 foldr 语句，例如

但是，我在处理更复杂的 foldr 语句时遇到了麻烦，即在函数中采用 2 个参数以及使用 / 和 - 计算的语句。谁能解释为获得这些答案而发生的步骤？

谢谢。

我试图了解 Haskell 如何评估sep [1, 2, 3, 4, 5]以获取([1, 3], [2, 4, 5])位置：

我是这样开始的：

但是之后？

我试图了解 Haskell 是如何评估pp1 [1,2,3,4]到[(1,2),(2,3),(3,4)]这里的：

我是这样开始的：

有什么帮助吗？

我试图手动评估，fc [f1, f2] (\x -> 2) 3但我不知道如何匹配三个参数：[f1，f2]、(\x -> 2) 和 3 与函数定义，有什么帮助吗？

函数定义：

谢谢，
塞巴斯蒂安。

阅读“使用 Haskell 进行功能思考”时，我遇到了一个程序计算的一部分，需要将map sum (map (x:) xss)其重写为map (x+) (map sum xss)

直觉上我知道这是有道理的......

如果您有一些要求和的列表，但在求和之前，您还要向这些相同的列表添加一个元素“x”，那么这与获取原始列表总和的列表并添加 x 相同对他们每个人的价值。

但我想知道如何仅使用等式推理将一个转换为另一个。我觉得我错过了可以帮助我理解的法律或规则。

“用 Haskell 进行函数式思考”中的一个练习是关于使用融合定律使程序更高效。我在尝试复制答案时遇到了一些麻烦。

计算的一部分需要您通过等式推理转换maximum (xs ++ map (x+) xs)为。max (maximum xs) (x + maximum xs)

maximum被定义为foldr1 max并且因为我不知道有关 foldr1 的许多规则，所以我什至坚持要转换foldr1 max (xs ++ map (x+) xs)为的第一部分，max (foldr1 max xs) (foldr1 max (map (x+) xs))所以这是我想了解的第一件事。

一旦我们克服了这一点，下一部分似乎更难，即转换foldr1 max (map (x+) xs)为x + foldr1 max xs. 直觉上是有道理的；如果您要找到一堆数字的最大值，这些数字都添加了“x”，那么这与在添加“x”之前找到所有数字的最大值并将“x”添加到结果中相同。

在第二阶段，我发现唯一对我有帮助的是这个堆栈溢出答案 ，答案基本上是给你的（如果你假设 p = q），没有像你通常用等式推理看到的那样容易理解的步骤。

那么请有人告诉我进行转换的步骤吗？

但是，从函数方程的角度来看，我希望两者的含义相同：

为什么sum在这里失败？