Функция преобразования типа данных занимает очень много времени для доказательства - PullRequest
Новая
       55

Функция преобразования типа данных занимает очень много времени для доказательства

1 голос
/ 24 мая 2019

Изабель нужно много времени, чтобы доказать правильность (на мой взгляд) довольно простых функций преобразования типов данных.В качестве примера я создал типы данных для представления математических и логических выражений и функцию, которая упрощает такое выражение. 

datatype 'a math_expr =
  Num int |
  Add "'a math_expr" "'a math_expr" |
  Mul "'a math_expr" "'a math_expr" |
  Sub "'a math_expr" "'a math_expr" |
  Div "'a math_expr" "'a math_expr"

datatype 'a expr =
  True |
  False |
  And "'a expr" "'a expr" |
  Or "'a expr" "'a expr" |
  Eq "'a math_expr" "'a math_expr" |
  Ne "'a math_expr" "'a math_expr" |
  Lt "'a math_expr" "'a math_expr" |
  Le "'a math_expr" "'a math_expr" |
  Gt "'a math_expr" "'a math_expr" |
  Ge "'a math_expr" "'a math_expr" |
  If "'a expr" "'a expr" "'a expr"

function (sequential) simplify :: "'a expr ⇒ 'a expr" where
"simplify (And a True) = a" |
"simplify (And True b) = b" |
"simplify (Or a True) = True" |
"simplify (Or True b) = True" |
"simplify e = e"
by pat_completeness auto
termination by lexicographic_order

В моей записной книжке Изабель требуется довольно много времени для проверки функции (подпись и тело выделены) и дажегораздо больше времени, чтобы доказать его полноту (by pat_completeness auto выделено).Необходимое время вычислений сильно зависит от сложности типа данных expr и количества правил сопоставления с образцом в simplify.Чем больше конструкторов в типе данных и чем больше правил сопоставления с образцом, тем дольше это занимает.

В чем причина такого поведения?Есть ли способ сделать такую ​​функцию проще доказуемой?

1 Ответ

1 голос
/ 11 июня 2019

Опция sequential заставляет команду function специализировать перекрывающиеся уравнения так, чтобы они больше не перекрывались. Однако это только препроцессор для фактической внутренней конструкции, которая фактически поддерживает перекрывающиеся шаблоны (при условии, что можно доказать, что правые части обозначают одно и то же значение HOL для перекрывающихся экземпляров, то есть они согласованы). Это доказательство согласованности выражается в виде отдельных целей (которые auto решаются практически всегда, если используется опция sequential, поскольку достаточно доказать, что они не могут перекрываться). Тем не менее, в числе неоднозначных уравнений есть квадратично много целей. Поэтому, если вы добавите больше конструкторов, перекрывающиеся уравнения будут разбиты на большее количество случаев, и эти случаи приведут к квадратичному числу целей.

Существует два обходных пути, когда функция не является рекурсивной:

Для нерекурсивных функций я рекомендую использовать definition с выражением case справа. Затем вы можете использовать simps_of_case из HOL-Library.Simps_Case_Conv для получения простых правил. Тем не менее, вы не получите хорошего правила разграничения падежа. 

definition simplify :: "'a expr ⇒ 'a expr" where
  "simplify e = (case e of And a True => a | And True b => b | ... | _ => e)"

simps_of_case simplify_simps [simp]: simplify_def

Если вы хотите получить хорошие теоремы о различении регистра, вы можете разделить определение функции на несколько вспомогательных функций: 

fun simplify_add :: "'a expr => 'a expr => 'a expr" where
  "simplify_add a True = a"
| "simplify_add True b = b"
| "simplify_add a b = Add a b"

fun simplify_or (* similarly *)

fun simplify :: "'a expr => 'a expr" where
  "simplify (And a b) = simplify_and a b"
| "simplify (Or a b) = simplify_or a b"
| "simplify e = e"

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

fun simplify :: "'a expr ⇒ 'a expr" where
  "simplify (And a b) = (case b of True => a | _ => case a of True => b | _ => And a b)"
| ...

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

...