伊莎貝爾書練習2.11：轉型表達式多項式形式

Question

我的問題是關於在書中具體語義練習2.11（http://concrete-semantics.org/）：

定義超過整數 （類型int）作爲數據類型的變量算術表達式：

datatype exp = Var | Const int | Add exp exp | Mult exp exp 

定義一個函數eval :: exp => int => int使得eval e x在 x的值的計算結果即 多項式可以表示爲係數列表，從 開始。例如，[4,2，-1,3]表示多項式4+2x-x^2+3x^3。

定義一個函數evalp :: int list => int => int，其計算給定值的多項式 。定義將 表達式轉換爲多項式的函數coeffs :: exp => int list。這可能需要輔助功能。證明 coeffs保留表達式的值：evalp (coeffs e) x = eval e x。

---結束

，直到你得到coeffs這一切都非常簡單。我們不得不處理像(X + X)*(2*X + 3*X*X)這樣的表達式，它必須使用分配律自底向上遞增擴展，直到它以多項式形式出現。由此產生的表達式可能仍然是類似於(X*X + X*2*X + 3*X*X + 4*X*X*X)的東西，因此它有必要對產品條款進行規範化（例如X*2*X變成2*X*X），像條款一樣收集起來，最後按順序遞增排列！這似乎比迄今爲止的任何練習都要複雜得多，我不知道我是否錯過了一些東西或者過於複雜。

Answer 1

我認爲這個練習比您想象的要容易得多。您可以編寫一個原始遞歸函數coeffs來完成這項工作：Var的係數是[0,1]，係數Const c是[c]。同樣，如果你有兩個子表達式，並且你知道他們的係數，你可以將這兩個係數列表組合成一個列表來進行加法/乘法。爲此，理想情況下應編寫兩個輔助函數add_coeffs和mult_coeffs，它們將兩個係數列表相加並相乘。 （後者可能會充分利用前者的）

你將不得不證明add_coeffs和mult_coeffs做正確的事（w.r.t. eval和evalp）。由此產生的引理也制定了好的[simp]規則。

證明都是簡單的導入，其中每個案例都是自動的。

作爲一般規則：一個好的定義通常會在冗長乏味的證明和直接甚至完全自動的證明之間產生差異。按照您在問題中提出的建議進行冗長的擴展，然後將加號等組合在一起，肯定會導致一個乏味的證明。

當然，我在這個答案中提出的方法效率不高，但是當你想在定理證明器中做事時，效率通常不是一個大問題 - 你希望事情變得簡單和優雅，以很好的證明。如果你需要高效的代碼，你仍然可以將你的漂亮和簡單的抽象公式發展成更高效的事情，並展現出等效性。