21

RWH の読み取りに失敗しました。やめる人ではなく、Haskell: The Craft of Functional Programmingを注文しました。今、146 ページのこれらの機能証明に興味があります。具体的には、 8.5.1 を証明しようとしていsum (reverse xs) = sum xsます。私はいくつかの誘導証明を行うことができますが、行き詰まります..

ハイプ:

sum ( reverse xs ) = sum xs

ベース：

sum ( reverse [] ) = sum []

Left  = sum ( [] ) (reverse.1)
      = 0          (sum.1)

Right = 0          (sum.1)

誘導：

sum ( reverse (x:xs) ) = sum (x:xs) 

Left = sum ( reverse xs ++ [x] )    (reverse.2)

Right = sum (x:xs)   
      = x + sum xs                  (sum.2)

だから今、私はLeft sum ( reverse xs ++ [x] )が に等しいことを証明しようとRight x + sum xsしていますが、それは私が始めたところからそれほど離れていませんsum ( reverse (x:xs) ) = sum (x:xs)。

なぜこれを証明する必要があるのか​​ よくわかりませんが、（defnによる）の記号証明を使用することは完全に合理的reverse x:y:z = z:y:xであり、 + は可換（arth）であるため、reverse 1+2+3 = 3+2+1、

4

4 に答える 4

24 
sum (reverse [])     = sum []                     -- def reverse
sum (reverse (x:xs)) = sum (reverse xs ++ [x])    -- def reverse
                     = sum (reverse xs) + sum [x] -- sum lemma below
                     = sum (reverse xs) + x       -- def sum
                     = x + sum (reverse xs)       -- commutativity assumption!
                     = x + sum xs                 -- inductive hypothesis
                     = sum (x:xs)                 -- definition of sum

Floatただし、厳密には保証されていない結合性と可換性の根本的な仮定がありDouble、これらの仮定に違反している場合など、多くの数値型では適切に機能しません。

補題:sum (xs ++ ys) == sum xs + sum ys与えられた結合性(+)

証拠：

sum ([] ++ ys)     = sum ys           -- def (++)
                   = 0 + sum ys       -- identity of addition
                   = sum [] ++ sum ys -- def sum

sum ((x:xs) ++ ys) = sum (x : (xs ++ ys))  -- def (++)
                   = x + sum (xs ++ ys)    -- def sum 
                   = x + (sum xs + sum ys) -- inductive hypothesis
                   = (x + sum xs) + sum ys -- associativity assumption!
                   = sum (x:xs) + sum ys   -- def sum
于 2010-07-15T13:31:47.967 に答える
6

基本的にあなたはそれを示す必要があります

sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

それは簡単に

                        = x + sum (reverse xs)
                        = x + sum xs  -- by inductive hyp.

問題は、それsumがリスト連結を介して配布されることを示すことです。

于 2010-07-15T03:08:26.777 に答える
4

合計の定義を使用して (sum reverse xs ++[x]) を x + sum(reverse(xs)) に分解し、帰納的仮説を使用して sum(reverse(xs)) = sum(xs) を知ることができます。しかし、私は同意します。誘導は、このような問題にはやり過ぎです。

于 2010-07-15T03:08:26.063 に答える
3

ここが行き詰まっていると思います。という補題を証明する必要があります。

sum (xs ++ ys) == sum xs + sum ys

この法則を証明するには、加算が結合的であると仮定する必要があります。これは、整数と有理数にのみ当てはまります。

次に、加算が交換可能であると仮定する必要があります。これは、整数と有理数だけでなく、浮動小数点数にも当てはまります。

余談: あなたの証明のスタイルは私には非常に奇妙に見えます. Graham Hutton の本のスタイルを使えば、この種の証明を簡単に書けると思います。

于 2010-07-15T16:49:22.530 に答える