問題タブ [formal-methods]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
proof - プログラムの等価性の証明
コンパイラを最適化する究極の方法は、プログラムの空間の中から元のプログラムと同等であるがより高速なプログラムを検索するものです。これは、非常に小さな基本ブロックに対して実際に行われています: https://en.wikipedia.org/wiki/Superoptimization
難しい部分は検索空間の指数関数的な性質のように思えますが、実際にはそうではありません。難しいのは、探しているものが見つかったとして、新しい高速なプログラムが元のプログラムと本当に同等であることをどのように証明するのかということです。
前回調べたとき、特定のコンテキストでプログラムの特定のプロパティを証明することで、特にスカラー変数や小さな固定ビットベクトルについて話しているときの非常に小さなスケールで、いくつかの進歩がありましたが、実際にはプログラムの同等性を証明することではありませんでした。複雑なデータ構造について話しているときは、より大きなスケールです。
「まだ解決方法がわからないこのNP困難な検索問題をモジュロで解決する」ことさえ、これを行う方法をまだ見つけた人はいますか?
編集: はい、停止の問題については誰もが知っています。一般的なケースで定義されています。人間は、関心のある多くの実際的なケースでこれを行うことができるという存在証明です。
specifications - Zed 仕様: 複数のスキーマの昇格と操作の適用
Arrayスキーマのシーケンスを追跡するスキーマがありますData。Incrementプロモーションを使用して、 で使用する操作をプロモーションできArrayます。
ArrayIncrement内の 1 つのデータのみをインクリメントしますArray。ごと Dataにインクリメントするようにするにはどうすればよい\ran dataですか?