1

これは課題のためだとすぐに言いますが、答えを探しているわけではありません。かなり長い間取り組んできたので、何らかの方向性を求めているだけです。次の末尾再帰合計関数があるとします。

sumTR [ ] acc = acc  
sumTR (x:xs) acc = sumTR xs (x + acc)

次のことを帰納法によって証明する必要があります。 

sumTR xs (sumTR ys acc) = sumTR (ys ++ xs) acc

基本ケースを証明した後 (xs を誘導し、ys を定数として扱う)、次のようになりました。 

sumTR x:xs(sumTR ys acc) = ... = sumTR xs (x + sumTR ys acc)  
sumTR (ys ++ x:xs) acc = ... = sumTR xs (sumTR ys (x + acc))

私たちの講師は、より単純な例 (sum1 xs = sum2 xs、sum1 は単純な再帰) を使用し、これ以上似たものにすることができない点に達したとき、次のようなことに注目して、「より強力なプロパティ」を証明しました。 sum2 xs acc = acc + xs の合計。次に、彼は「すべての acc に対して」を含む帰納的仮説を設定し、後で acc を 0 に設定しました。

私が抱えている主な問題は、 acc が既に LHS と RHS にあるため、近づいたように感じますが、より強力なプロパティを実際に証明していないことです (質問では具体的に求められていませんが、私は使用することになっていると思います）。また、関数から要素を取り出す (または要素を挿入する) ときに、加算の結合性をどの程度まで使用できるかわかりません。

どんな助けでも大歓迎です！

4

1 に答える 1

4

ysで帰納法を行う方がはるかに簡単ですys。

sumTR xs (sumTR [] acc) =  -- by first case of (inner) sumTR
sumTR xs acc =             -- by definition of (++)
sumTR ([] ++ xs) acc       -- Q.E.D.

そして についてはy:ys、

sumTR xs (sumTR (y:ys) acc) =    -- by second case of (inner) sumTR
sumTR xs (sumTR ys (y + acc)) =  -- by induction
sumTR (ys ++ xs) (y + acc) =     -- by second case of sumTR, "in reverse"
sumTR (y:(ys ++ xs)) acc =       -- by definition of (++)
sumTR ((y:ys) ++ xs) acc         -- Q.E.D.

は、左辺の引数の再帰によって定義されysているため、この場合は役に立ちました。(++)ys

于 2016-08-27T11:01:44.397 に答える