haskell 的结构归纳

Question

大家好我想问一下下面是不是结构归纳的定义

init xs = take ( length xs - 1) xs

init :: [ a ] -> [ a ]
init ( x :[]) = []
init ( x : z : xs ) = x : init ( z : xs )

也有人能给我一个结构归纳的例子吗Haskell？

Answer 1

首先，您需要定义 init 做什么 ，这样您就可以比较实现 take (length xs - 1) xs 的内容。这样的规范可能是

 init [x] = []
 init (x:xs) = x : init xs

（这基本上是一个有效的 Haskell 定义本身就是 Haskell 的优势之一。）

要证明init xs = take (length xs - 1) xs是正确的，您需要使用等式推理证明定义满足规范。

基本情况（每个单例列表）很简单：

init [x] == take (length [x] - 1) [x]  -- definition of init
         == take (1 - 1) [x]  -- definition of length
         == take 0 [x]  -- arithmetic
         == []  -- using the definition of take

已经证明 init 对于长度为 1 的列表是正确的，归纳假设是 init xs 对于任何长度为 k > 1 的列表 xs 都是正确的。归纳 step 是为了证明 init 对于长度为 k + 1 的列表 (x:xs) 是正确的（即，通过添加一个以上元素创建的任何列表到长度为 k).

的列表

init (x:xs) == take (length (x:xs) - 1) (x:xs)  -- definition of init
            == take (1 + length xs - 1) (x:xs)  -- definition of length
            == take (length xs) (x:xs)  -- arithmetic
            == x : take (length xs - 1) xs -- definition of take
            == x : init xs -- definition of init

haskell 的结构归纳

structural induction of haskell

haskell

currying

syntactic-sugar

induction