Полиномиальная оценка в Изабель - PullRequest
Новая
       34

Полиномиальная оценка в Изабель

1 голос
/ 29 января 2020

В книге "Конкретная семантика" упражнение 2.11 пишет:

Определить арифметику c выражений в одной переменной над целыми числами (тип int) как тип данных: 

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

Определите функцию eval :: exp ⇒ int ⇒ int так, чтобы eval ex оценивал e по значению 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. Подсказка: рассмотрите подсказку в Упражнении 2.10.

В качестве первой попытки, и поскольку предыдущие упражнения поощряли написание итеративных версий функций, я написал следующее: 

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

fun eval :: "exp ⇒ int ⇒ int" where
  "eval Var x = x"
| "eval (Const n) _ = n"
| "eval (Add e1 e2) x = (eval e1 x) + (eval e2 x)"
| "eval (Mult e1 e2) x = (eval e1 x) * (eval e2 x)"

fun evalp_it :: "int list ⇒ int ⇒ int ⇒ int ⇒ int" where
  "evalp_it [] x xpwr acc = acc"
| "evalp_it (c # cs) x xpwr acc = evalp_it cs x (xpwr*x) (acc + c*xpwr)" 

fun evalp :: "int list ⇒ int ⇒ int" where
  "evalp coeffs x = evalp_it coeffs x 1 0"

fun add_coeffs :: "int list ⇒ int list ⇒ int list" where
  "add_coeffs [] [] = []"
| "add_coeffs (a # as) (b# bs) = (a+b) # (add_coeffs as bs)"
| "add_coeffs as [] = as"
| "add_coeffs [] bs = bs"

( для этого может быть какая-то функция zip) 

fun mult_coeffs_it :: "int list ⇒ int list ⇒ int list ⇒ int list ⇒ int list" where
  "mult_coeffs_it [] bs accs zeros = accs"
| "mult_coeffs_it (a#as) bs accs zeros = 
     mult_coeffs_it as bs (add_coeffs accs zeros@bs) (0#zeros)"

fun mult_coeffs :: "int list ⇒ int list ⇒ int list" where
  "mult_coeffs as bs = mult_coeffs_it as bs [] []" 

fun coeffs :: "exp ⇒ int list" where 
  "coeffs (Var) = [0,1]"
| "coeffs (Const n) = [n]"
| "coeffs (Add e1 e2) = add_coeffs (coeffs e1) (coeffs e2)"
| "coeffs (Mult e1 e2) = mult_coeffs (coeffs e1) (coeffs e2)"

Я пытался проверить искомую теорему 

lemma evalp_coeffs_eval: "evalp (coeffs e) x = eval e x"

, но не смог. Однажды я получил совет, что написание хороших определений очень важно для доказательства теорем, хотя советник не дал подробностей.

Итак, в чем проблема с моими определениями, концептуально? Пожалуйста, не пишите хорошие определения, но укажите концептуальные проблемы с моими определениями.

ОБНОВЛЕНИЕ: по совету я начал использовать 

fun evalp2 :: "int list ⇒ int ⇒ int" where
"evalp2 [] v = 0"|
"evalp2 (p#ps) v = p + v * (evalp2 ps v) "

и изучая src/HOL/Algebra/Polynomials.thy Я сформулировал 

fun add_cffs :: "int list ⇒ int list ⇒ int list" where
  "add_cffs as bs = 
     ( if length as ≥ length bs
         then map2 (+) as (replicate (length as - length bs) 0) @ bs
         else add_cffs bs as)"

но это не сильно помогло, simp add: algebra_simps или arith не решило соответствующую подцель.

1 Ответ

1 голос
/ 29 января 2020

Некоторые подсказки:

  1. Попробуйте запустить quickcheck и nitpick на лемме, пока не найдется больше контрпримеров. Для леммы в вашем вопросе я получаю следующий встречный пример: 

    Quickcheck found a counterexample:
  e = Mult Var Var
  x = - 2
Evaluated terms:
  evalp (coeffs e) x = - 10
  eval e x = 4

  2. Попробуйте сначала доказать несколько полезных лемм о ваших вспомогательных функциях. Например: 

    lemma "evalp (mult_coeffs A B) x = evalp A x * evalp B x"

  3. Прочитайте о вычислениях с полиномами (например, https://en.wikipedia.org/wiki/Polynomial_ring) и выберите определения, близкие к тому, что делают математики. Хотя это может испортить удовольствие от самостоятельного определения.

...