Japanese 字幕

← 01-09 Correctness: Naive

埋め込みコードを取得する
2言語

Showing Revision 1 created 03/11/2014 by Fran Ontanaya.

  1. それではアルゴリズムnaiveの正当性を
  2. 証明したいと思います
  3. まずは特定の観測結果を利用します
  4. ここで正当性を証明しようとしている仮説は
  5. naive(a,b)の結果はaとbの積であるというものです
  6. 私の観測ではnaiveの中の
    whileループの前でもあとでも
  7. ab=xy+zは常に真(true)です
  8. 変数xとyの積にzを足したものは
  9. aとbの積に等しいことを
    どのように証明すればよいでしょうか
  10. まずwhileループを通る前の段階では
  11. x=a、y=b、z=0です
  12. これらをab=xy+zに当てはめてみましょう
  13. 結果はab=ab+0となります 当たり前ですね
  14. 次に確かめたいのはwhileループの最初の段階でも
  15. ab=xy+zであるのならば
  16. ループを通りx、y、zが変わっても
    結果は変わらないということです
  17. つまりx'、y'、z'になったとしても
    ab=x'y'+z'だということです
  18. 前者が真であれば後者も真であるはずです
  19. なぜでしょうか コードを思い出してください
  20. ループの中では新しいzの値が計算されます
  21. 1つ前の値にyを足したものです
  22. それから新しいxの値も計算されます
  23. 新しいxは古いxから1を引いたものです
    yの値は変わりません
  24. 新しいzは古いzにyを足したものです
  25. ではこれらを使ってx'y'+z'を表すと
    どうなるでしょうか
  26. x'、y'、z'に該当するものを代入します
  27. (x-1)y+(z+y)となります
    ここでちょっとした代数学を使います
  28. 展開するとxy-y+z+yとなります
  29. -yと+yは消せるのでxy+zとなります
  30. 最初に仮定したことを思い出してください
    私たちはxy+z=abであれば
  31. x'y'+z'=abであろうと仮定しましたが
  32. 実際にx'y'+z'=abであることを
    確かめることができました
  33. ループの最初の段階でxy+z=abが真であれば
  34. ループを通ってもその条件は変わらないということです
  35. 最初に真であればループを通っても真のままです
  36. つまりコードを実行し
    whileループを繰り返している間中
  37. xy+z=abは変わらないまま
    最終的にループは終了します
  38. whileループはxがゼロになると終了します
  39. xy+z=abにx=0を当てはめると0y+z=abとなります
  40. 0y=0なのでループの最後にはz=abとなります
  41. xがゼロになるとz=abとなります
    このzこそ私たちが求めたかったものです
  42. つまり結果は常にaとbの積になります
  43. コードをもう1度見てみましょう
  44. ループを通る度にxの値は減りzの値は増えます
  45. xがゼロになった時zの値はaとbの積となります