haskell的结构归纳

Posted 2023-02-22

【中文标题】haskell的结构归纳

【英文标题】：structural induction of haskell

【发布时间】：2022-01-20 15:27:54

【问题描述】：

大家好，请问下面的结构归纳有没有定义

init xs = take ( length xs - 1) xs

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

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

【问题讨论】：

您有两种init 的实现，一种使用take，一种使用结构归纳。

结构归纳更像是一种证明技术，而不是一种编程技术。也许你的意思是结构递归？

【参考方案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 都是正确的。归纳步骤是为了证明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