Haskell 中的结构归纳

Question

谁能给我一个Haskell中的结构归纳的例子？我在网上找不到任何关于它的信息，有人给了我一个假设，但在制定基本案例时遇到了问题。

假设是：对于 [a] 类型的所有列表 xs 和 a 类型的所有 x 是：

toLast (x:xs) = xs |++| [x]

|++| 是我自己的连接两个列表的版本，toLast 是列表的 header 到列表末尾的函数。我试图自己解决这个问题并得到 toLast [] = [] |++| [] 但我不确定这是否正确。

Answer 1

Can anyone give me an example of Structural induction in Haskell?

结构归纳总是需要两个步骤：

考虑基本情况
通过假设列表 xs 存在函数体来考虑一般情况，并使用该假设为下一步构建定义 (x :xs)。这就是所谓的归纳步骤。

让我们使用结构归纳的思想来定义您的 |++| 函数，在我看来这是一个更好的例子。

|++| 接受两个列表并输出一个列表，该列表是第一个列表与第二个列表的串联，因此类型签名为：

(|++|) :: [a] -> [a] -> [a]

第二个列表输入永远不变，所以我们说第一个列表是递归的参数。因此，基本情况是第一个列表为空时：

(|++|) [] ys = ys

现在，让我们考虑 |++| 的第一个参数不是空列表而是 xs 的情况。归纳步骤是假设我们的函数 (|++|) xs ys 有效（因为它在基本情况下被证明是有效的）并使用该假设来定义 |++| 的第一个输入是 (x:xs)。将这些放在一起，到目前为止，我们有：

(|++|) []     ys = ys -- base case
(|++|) (x:xs) ys = let assumedAlreadyConcatenatedList = ((|++|) xs ys) in *something...* assumedAlreadyConcatenatedList -- half-done general case

假设 ((|++|) xs ys) 工作正常，我们只需要定义要对 x 做什么，然后我们就完成了。我们如何将 x 连接到已连接项目的列表中？我们使用缺点：

(|++|) []     ys = ys -- base case
(|++|) (x:xs) ys = let assumedAlreadyConcatenatedList = ((|++|) xs ys) in x : assumedAlreadyConcatenatedList -- completed general case.

希望很明显，我们总是需要一个基本案例来支持我们在归纳步骤中的假设。

Haskell 中的结构归纳

Structual induction in Haskell

haskell

induction