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

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

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

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

Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
1
0
57
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Параметр 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)"
| ...

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

Другие вопросы по теме