Я строю операторы программы из алгебраических структур, а не использую определения или функции. То есть для установки их свойств в Isabelle с помощью команд локали или класса.
Теперь мне нужно построить оператор while.
Я знаю, что могу определить его с помощью функций или с помощью алгебры Клини. Но, как я уже говорил, я просто хочу описать природу класса или локали.
Поэтому я написал этот код:
consts skip :: "'a" ("II")
type_synonym 'a proc = "'a "
class sequen =
fixes seq :: "'a proc ⇒'a proc ⇒'a proc " (infixl ";;" 60)
assumes seq_assoc : "(x ;; y) ;; z = x ;; (y ;; z)"
and seq_skip_left : "II ;; x = x"
and seq_skip_right : "x ;; II = x"
definition ifprog :: " 'a proc ⇒ bool ⇒ 'a proc ⇒ 'a proc " ("(_ ◃ _ ▹ _)" [52,0,53] 52)
where "x ◃ bexp ▹ y ≡ (THE z::'a proc . (bexp = True ⟶ z = x) ∧ (bexp = False ⟶ z = y))"
locale while_unfold =
sequen seq
for seq :: "'a proc ⇒'a proc ⇒'a proc " +
fixes while ::"bool ⇒ 'a proc ⇒ 'a proc" ("while _ do _ od")
assumes while_ltera : "while bexp do P od = (P ;; (while bexp do P od)) ◃ bexp ▹ II"
Если бы это было возможно, я бы не задавал здесь вопросов, у меня проблема :Type unification failed: Variable 'a::type not of sort sequen
И затем, эти детали:
Type unification failed: Variable 'a::type not of sort sequen
Type error in application: incompatible operand type
Operator: (;;) :: ??'a ⇒ ??'a ⇒ ??'a
Operand: P :: 'a
Как мне избежать этой проблемы, или можно ли использовать этот описательный метод для создания утверждений, которые имеют итеративную функцию, например while
.
Я не смотрел содержимое класса/локали, но сообщение об ошибке кажется самоочевидным: унификация типов не удалась из-за несовместимого ограничения сортировки для переменной типа 'a
. Если вы не полагаетесь на вывод типа, ограничение сортировки должно быть указано явно:
consts skip :: "'a" ("II")
type_synonym 'a proc = "'a "
class sequen =
fixes seq :: "'a proc ⇒'a proc ⇒'a proc " (infixl ";;" 60)
assumes seq_assoc : "(x ;; y) ;; z = x ;; (y ;; z)"
and seq_skip_left : "II ;; x = x"
and seq_skip_right : "x ;; II = x"
(*sequen_class.seq has the type
"'a::sequen ⇒ 'a::sequen ⇒ 'a::sequen",
which includes the sort constraint sequen for the type variable 'a:*)
declare [[show_sorts]]
term sequen_class.seq
definition ifprog :: " 'a proc ⇒ bool ⇒ 'a proc ⇒ 'a proc " ("(_ ◃ _ ▹ _)" [52,0,53] 52)
where "x ◃ bexp ▹ y ≡ (THE z::'a proc . (bexp = True ⟶ z = x) ∧ (bexp = False ⟶ z = y))"
(*note the sort constraint*)
locale while_unfold =
sequen seq
for seq :: "'a::sequen proc ⇒'a proc ⇒'a proc " +
fixes while ::"bool ⇒ 'a proc ⇒ 'a proc" ("while _ do _ od")
assumes while_ltera : "while bexp do P od = (P ;; (while bexp do P od)) ◃ bexp ▹ II"
(*alternatively, consider using a class instead of a locale, although,
most certainly, the best choice depends on your application*)
class while_unfold' =
sequen +
fixes while ::"bool ⇒ 'a proc ⇒ 'a proc" ("while _ do _ od")
assumes while_ltera : "while bexp do P od = (P ;; (while bexp do P od)) ◃ bexp ▹ II"
Для получения дополнительной информации о классах и ограничениях сортировки см. разделы 3.3.6 и 5.8 в Справочном руководстве Isabelle/Isar. Вы также можете взглянуть на раздел 2 в Реализации Isabelle/Isar.
Версия Изабель: Isabelle2020
Забыл сказать, эта проблема возникает в «locale while_unfold».