问题标签 [equational-reasoning]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
haskell - 我是否使用合理的等式推理来根据 foldr 定义过滤器?
好吧,这是使用 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 章。
acl2 - acl2 等式推理,证明等式
我试图证明以下函数是正确的,并且很难弄清楚,即使它看起来很明显!
通过这样做,我只需要使用以下函数证明 (app (rev x) (rev y)) 等效于 (rev (app xy)))):
这就是我做另一个的方式(希望是正确的)
“反向附加东西”
= 转速的定义
= rev 的输出合约
= "反向追加事物"
= rev 的输出合约
= len 的定义
= rev 的输出合约
haskell - 了解不同的文件夹语句
我理解简单的 foldr 语句,例如
但是,我在处理更复杂的 foldr 语句时遇到了麻烦,即在函数中采用 2 个参数以及使用 / 和 - 计算的语句。谁能解释为获得这些答案而发生的步骤?
谢谢。
haskell - Haskell 如何评估这个取消列表插入的函数?
我试图了解 Haskell 如何评估sep [1, 2, 3, 4, 5]
以获取([1, 3], [2, 4, 5])
位置:
我是这样开始的:
但是之后?
haskell - Haskell 如何评估这个用偏应用定义的函数?
我试图了解 Haskell 是如何评估pp1 [1,2,3,4]
到[(1,2),(2,3),(3,4)]
这里的:
我是这样开始的:
有什么帮助吗?
haskell - 功能评估结果
我试图手动评估,fc [f1, f2] (\x -> 2) 3
但我不知道如何匹配三个参数:[f1,f2]、(\x -> 2) 和 3 与函数定义,有什么帮助吗?
函数定义:
谢谢,
塞巴斯蒂安。
haskell - Haskell - 如何将 map sum (map (x:) xss) 转换为 map (x+) (map sum xss)
阅读“使用 Haskell 进行功能思考”时,我遇到了一个程序计算的一部分,需要将map sum (map (x:) xss)
其重写为map (x+) (map sum xss)
直觉上我知道这是有道理的......
如果您有一些要求和的列表,但在求和之前,您还要向这些相同的列表添加一个元素“x”,那么这与获取原始列表总和的列表并添加 x 相同对他们每个人的价值。
但我想知道如何仅使用等式推理将一个转换为另一个。我觉得我错过了可以帮助我理解的法律或规则。
haskell - Haskell - 如何将最大值 (xs ++ map (x+) xs) 转换为最大值 (maximum xs) (x + maximum xs)
“用 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),没有像你通常用等式推理看到的那样容易理解的步骤。
那么请有人告诉我进行转换的步骤吗?
python - reduce(x+y, xs) 和 sum(xs) 在 python 中不等价?
但是,从函数方程的角度来看,我希望两者的含义相同:
为什么sum
在这里失败?