如何使用等式推理来简化这个表达式

Question

我有以下定义：

fibs = 1 : scanl (+) 1 fibs

scanl :: (a -> b -> a) -> a -> [b] -> [a] 
scanl f q ls =
    q : (case ls of 
            [] ->[]
            x:xs -> scanl f (f q x) xs
        )

take                   :: Int -> [a] -> [a]
take n _      | n <= 0 =  []
take _ []              =  []
take n (x:xs)          =  x : take (n-1) xs

我想减少以下表达式：

take 3 (fibs)

所以，我会继续：

take 3 (fibs)
= 
take 3 (1 : scanl (+) 1 fibs)
= 
1 : take 2 (scanl (+) 1 fibs)
= 
1 : take 2 (scanl (+) 1 (1 : (scanl (+) 1 fibs)))
=
...

我怎样才能继续推理？

编辑：我继续推理，但最后一行不正确，因为下一个计算的斐波那契数应该是 5。我该如何解决这个问题？

take 3 (fibs)
= 
take 3 (1 : scanl (+) 1 fibs)
= 
1 : take 2 (scanl (+) 1 fibs)
= 
1 : take 2 (scanl (+) 1 (1 : (scanl (+) 1 fibs)))
= 
1 : take 2 (1 : scanl (+) 2 (scanl (+) 1 fibs))
= 
1 : 1 : take 1 (scanl (+) 2 (scanl (+) 1 fibs))
= 
1 : 1 : take 1 (scanl (+) 2 (1 : scanl (+) 1 fibs))
= 
1 : 1 : take 1 (2 : scanl (+) 3 (scanl (+) 1 fibs))
= 
1 : 1 : 2 : take 0 (scanl (+) 3 (1 : scanl (+) 1 fibs))
= 
1 : 1 : 2 : take 0 (3 : scanl (+) 4 (1 : scanl (+) 1 fibs))
= 
...

Answer 1

通过等式推理，您通常可以按照您想要的任何顺序扩展项，并且通常会得到相同的结果。你发现了例外——如果你选择了一个特别糟糕的扩展顺序，比如不断扩展该项fibs而忽略该项scanl，你的解决方案可能会无限循环而不会产生任何结果，而 Haskell 对其进行评估没有问题。

如果你想以 Haskell 实际评估程序的方式扩展你的程序，你需要了解当且仅当模式匹配需要评估时，无论是在显式语句中case还是在函数定义的隐式 case 语句中，术语都会被评估有图案。

因此，当 Haskell 评估它需要评估/扩展该术语的原因take 3 fibs是因为每当第一个参数为正时，模式就与第二个参数上要求模式匹配的定义相匹配。详细来说，Haskell 首先尝试匹配模式：fibstake

take n _ | n <= 0 = ...

这需要评估n，其已被评估为3。由于守卫失败，Haskell 接下来尝试匹配模式：

take _ [] = ...

这需要评估第二个参数，因为这是 Haskell 判断它是否是空列表的唯一方法。

在您的（预编辑）扩展中，您实际上遵循了这条规则——即使您没有意识到自己正在遵循它——直到这个学期。

1 : take 2 (scanl (+) 1 fibs)

当 Haskell 尝试评估take这里的because2是正数时，它需要评估第二个参数。但是对第二个参数的评估并不立即从扩展开始fibs。scanl只有当模式匹配其第三个参数时才会发生这种情况，因此我们需要scanl先看看正在做什么。从代码来看，定义：

scanl f q ls = ...

可以在根本没有模式匹配的情况下应用，因此正确的扩展（意味着与 Haskell 实际尝试评估它的方式相匹配的扩展）是：

1 : take 2 (scanl (+) 1 fibs)
=
1 : take 2 (1 : (case fibs of { [] -> []; x:xs -> scanl (+) ((+) 1 x) xs }))

现在，take有足够的关于第二个参数的信息可以继续，因此可以通过应用 的定义来继续扩展take：

1 : 1 : take 1 (case fibs of { [] -> []; x:xs -> scanl (+) ((+) 1 x) xs })

接下来take还需要扩展其第二个论证才能取得进展。该case语句需要扩展fibs为模式匹配，因此扩展的下一部分应该是：

1 : 1 : take 1 (case (1 : scanl (+) 1 fibs) of { [] -> []; x:xs -> scanl (+) ((+) 1 x) xs })

这是足够的信息来继续（通过使用和case应用第二种情况）：x=1xs=scanl (+) 1 fibs

1 : 1 : take 1 (scanl (+) ((+) 1 1) (scanl (+) 1 fibs))

为了take取得进展，它需要检查其第二个参数，即scanl. 这scanl可以通过直接应用定义来进行，无需进一步评估：

1 : 1 : take 1 (((+) 1 1) : case scanl (+) 1 fibs of { [] -> []; x:xs -> scanl (+) ((+) ((+) 1 1) x) xs })

现在，take有足够的信息可以继续：

1 : 1 : ((+) 1 1) : take 0 (case scanl (+) 1 fibs of { [] -> []; x:xs -> scanl (+) ((+) ((+) 1 1) x) xs })

此时，假设所有列表元素都已按顺序要求，Haskell 的下一个业务顺序将是评估第三个元素：

1 : 1 : 2 : take 0 (case scanl (+) 1 fibs of { [] -> []; x:xs -> scanl (+) ((+) ((+) 1 1) x) xs })

最后一个任务是评估take，当它的第一个参数为零时，不需要进一步评估它的第二个参数，所以我们只得到：

1 : 1 : 2 : []

这是最终的答案。

正如我所说，这就是 Haskell 实际评估你的程序的方式。（嗯，由于优化，它可能会略有不同，但答案保证是相同的。）

尽管您所做的评估比 Haskell 多，但您在编辑中的替代顺序也将起作用。您得到错误答案的原因是这一步：

1 : 1 : take 1 (scanl (+) 2 (scanl (+) 1 fibs))
=
1 : 1 : take 1 (scanl (+) 2 (1 : scanl (+) 1 fibs))

是不正确的。如果您想在您的方法之后扩展第二个scanl，您需要fibs首先再次扩展：

1 : 1 : take 1 (scanl (+) 2 (scanl (+) 1 fibs))
=
1 : 1 : take 1 (scanl (+) 2 (scanl (+) 1 (1 : scanl (+) 1 fibs)))

现在您可以将 的定义应用于scanl第二次出现：

1 : 1 : take 1 (scanl (+) 2 (1 : scanl (+) (1 + 1) (scanl (+) 1 fibs)))

以及第一次出现的情况：

1 : 1 : take 1 (2 : scanl (+) (2 + 1) (scanl (+) (1 + 1) (scanl (+) 1 fibs))
=
1 : 1 : 2 : take 0 (scanl (+) (2 + 1) (scanl (+) (1 + 1) (scanl (+) 1 fibs))

不需要更多的评估，但如果您确实想更进一步，则必须在将出现次数从倒数第二个扩展到第一个之前fibs 再次扩展：scanl

1 : 1 : 2 : take 0 (scanl (+) (2 + 1) (scanl (+) (1 + 1) (scanl (+) 1 (1 : scanl (+) 1 fibs))))
=
1 : 1 : 2 : take 0 (scanl (+) (2 + 1) (scanl (+) (1 + 1) (1 : scanl (+) (1 + 1) (scanl (+) 1 fibs))))
=
1 : 1 : 2 : take 0 (scanl (+) (2 + 1) (2 : scanl (+) (2 + 1) (scanl (+) (1 + 1) (scanl (+) 1 fibs))))
=
1 : 1 : 2 : take 0 (3 : scanl (+) (3 + 2) (scanl (+) (2 + 1) (scanl (+) (1 + 1) (scanl (+) 1 fibs))))
=
1 : 1 : 2 : take 0 (3 : scanl (+) 5 (scanl (+) 3 (scanl (+) 2 (scanl (+) 1 fibs))))

您可以看到5, not 4, 正在慢慢进入计算中。