Isabelle книга Упражнение 2.11: Преобразование выражений к полиномиальной форме

Question

мой вопрос относительно Exercise 2.11 в книге Железобетонные семантике (http://concrete-semantics.org/):

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

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

Определим функцию eval :: exp => int => int таким образом, что оценивает eval 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.

--- Конец

Это все довольно просто, пока вы не получите 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].

Доказательства - все простые индукции, где каждый случай является автоматическим.

Как правило, хорошее определение часто делает разницу между длинным и утомительным доказательством и прямым или даже полностью автоматическим доказательством. Выполнение длинного расширения, а затем группировка слагаемых и т. Д., Как вы предложили в своем вопросе, обязательно приведет к утомительному доказательству.

Конечно, метод, который я предложил в этом ответе, не очень эффективен, но когда вы хотите делать что-то в доказательстве теоремы, эффективность обычно не является большой проблемой - вы хотите, чтобы вещи были простыми, элегантными и удобными к хорошим доказательствам.Если вам нужен эффективный код, вы все равно сможете разработать свою красивую и простую абстрактную формулировку в нечто более эффективное и показать эквивалентность.