問題タブ [equational-reasoning]

私は、Coursera での Scala の関数型プログラミングの講義に従っています。ビデオ 5.7 の最後で、Martin Odersky は次の方程式の正しさを帰納法によって証明するよう求めています。

複数のリストが含まれている場合、帰納法による証明をどのように処理するのですか?

xs が Nil で ys が Nil である基本ケースを確認しました。xs を x::xs に置き換えたときに方程式が成立することを帰納法によって証明しましたが、ys を y::ys に置き換えた方程式もチェックする必要がありますか?

そしてその場合（エクササイズをあまり台無しにすることなく...とにかく採点されません）、どのように処理します(xs ++ (y::ys)) map fか？

これは、私が同様の例で使用したアプローチであり、

証明 (基本ケースと簡単な x::xs ケースを省略):

これは正しいですか ？

このプログラムに注意してください：

合計の両方の定義は、等式の推論までは同じです。それでも、2 番目の定義のコンパイルは機能しますが、最初の定義はコンパイルされず、次のエラーが発生します。

RankNTypes等式の推論を破るようです。それを壊すことなく、Haskellで教会でエンコードされたリストを持つ方法はありますか??

moll n = doll nステートメントを確立するために誘導を行うにはどうすればよいですか?

n = 0 の基本ケースを証明しようとしました

についてn+1、それを示してください

しかし、今はどうですか？これ以上単純化するにはどうすればよいですか？

return a = return bもしそうなら、あなたはそれを証明できますa=bか？を使うときは、クラスの意味=ではなく、法則と証明の意味で意味します。Eq

私が知っているすべてのモナドはこれを満たすようであり、そうでない有効なモナドは考えられません (Const aはファンクターであり適用可能ですが、モナドではありません。)

Haskell の等式推論と証明に関するこの演習を見つけました。次のコードが与えられます。

今、私はそれを証明しなければなりませんexec(comp e) s = eval e : s。

だから私はこれまでにこの答えを見つけました：

それを証明しなければなりませんexec (comp e) s = eval e : s。

最初のケース: と仮定しe = (Val n)ます。では、それcomp (Val n) = [PUSH n]を証明しなければなりませんexec ([PUSH n]) s = eval ([PUSH n] : s)。exec ([PUSH n]) s = exec [] (n:s) = (n:s)exec の関数定義を使用するとわかります。

今eval (Val n) : s = n : s。初めてのケースでもOK！

2 番目のケース: と仮定しe = (Add x y)ます。それからcomp (Add x y) = comp x ++ comp y ++ [ADD]。

しかし今、私はこのcompの再帰的な使用に苦労しています。これを証明するために、何らかの形のツリーとこれらのツリーの帰納法を使用する必要がありますか? その方法が完全にはわかりません。

私はHaskellのセマンティクスを学んでおり、そこでこの質問に出くわしました:

私はそれを試しましたが、まだ答えを結論付けることができません。誰かがこれを証明する方法を私に説明してくれれば、それは素晴らしいことです. ありがとうございました。

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

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

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

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

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

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

f が厳密な場合、すべての xs リストで機能します。誰も私に例を挙げてもらえますか? 非厳密な f では機能しないのはなぜですか?