大家好我想問一下下面有沒有結構歸納的定義
init xs = take ( length xs - 1) xs
init :: [ a ] -> [ a ]
init ( x :[]) = []
init ( x : z : xs ) = x : init ( z : xs )
也有人能給我一個 Haskell 結構歸納的例子嗎？
uj5u.com熱心網友回復：
首先，您需要定義 what init do，以便您可以將實作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對于任何xs長度為 的串列都是正確的k > 1。歸納步驟是證明init對于(x:xs)長度串列k 1（即，通過向長度串列添加另一個元素創建的任何串列）是正確的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
轉載請註明出處，本文鏈接：https://www.uj5u.com/caozuo/386992.html
上一篇：使用megaparsec parser-combinators進行置換決議過于寬松
下一篇：如何操作Aeson值？