Изабель нужно много времени, чтобы доказать правильность (на мой взгляд) довольно простых функций преобразования типов данных. В качестве примера я создал типы данных для представления математических и логических выражений и функцию, которая упрощает такое выражение.
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
. Чем больше конструкторов в типе данных и чем больше правил сопоставления с образцом, тем больше времени это занимает.
В чем причина такого поведения? Есть ли способ упростить доказуемость такой функции?
Параметр 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)"
| ...
Опять же, это значительно уменьшает количество уравнений после того, как они не перекрываются, но вы больше не получаете одни и те же правила различения регистров (и правила индукции).