2

アルゴリズムの「正当性の証明」* について多くのことを読んでいます。

証明は実装ではなくアルゴリズムに適用されると言う人もいますが、デモはほとんどの場合、数学ではなくコード ソースで行われます。また、コード ソースには副作用がある場合があります。だから、誰かが不純な関数を正しく証明するのを妨げる基本原則があるかどうか知りたいです。

本当だと思いますが、理由は言えません。もしそのような原理が存在するなら、あなたはそれを説明できますか?

ありがとう

* 言葉遣いが間違っている場合は申し訳ありませんが、何が良いかわかりません。

4

1 に答える 1

2

答えは、数学に副作用はありませんが、副作用のあるコードを数学的にモデル化することは可能です。

実際、このトリックを使用して、純粋でないコードを純粋なコードに変換することもできます (最初から数学に行く必要はありません。つまり、 (psedocode) 関数の代わりに:

f(x) = {
  y := y + x
  return y
}

...次のように書くことができます:

f(x, state_before) = {
  let old_y = lookup_y(state_before)
  let state_after = update_y(state_before, old_y + x)
  let new_y = lookup_y(state_after)
  return (new_y, state_after)
}

...副作用なしで同じことを達成できます。もちろん、これらの状態値を明示的に渡すにはプログラム全体を書き直す必要があり、すべての変更可能な変数に対して適切な関数lookup_と関数を記述する必要がありますが、理論的には簡単なプロセスです。update_

もちろん、誰もこのようにプログラムしたいとは思いません。(Haskell は、副作用を言語の一部にせずにシミュレートするために同様のことを行いますが、これよりも人間工学的にするために多くの作業が行われました。)定義された概念。

これは、言語の仕様が、プログラムを状態渡しスタイルに書き換える方法を知るのに十分な情報を提供してくれれば、副作用のある言語について証明できることを意味します。

于 2013-08-27T19:12:22.610 に答える