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

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

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. Чем больше конструкторов в типе данных и чем больше правил сопоставления с образцом, тем больше времени это занимает.

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


isabelle formal-verification
person user11516323    schedule 24.05.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Опция 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)"
| ...

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

person Andreas Lochbihler    schedule 11.06.2019