Могу ли я построить структуру while алгебраически, используя класс и локаль?

Я создаю программные операторы из алгебраических структур, а не использую определения или функции. То есть, чтобы установить их свойства в 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

А затем эти детали:

Ошибка объединения типов: переменная 'a :: type не соответствует последовательности сортировки

Ошибка типа в приложении: несовместимый тип операнда

Оператор: (;;) :: ?? 'a ⇒ ??' a ⇒ ?? 'a
Операнд: P ::' a

Как я могу избежать этой проблемы или можно ли использовать этот описательный метод для создания операторов, которые имеют итеративную функцию, например while.


isabelle formal-verification
person hidaidai    schedule 15.05.2019    source источник
comment
Забыл сказать, эта проблема возникает в locale while_unfold ».   -  person hidaidai    schedule 17.05.2019

Ответы (1)


arrow_upward
0
arrow_downward

Я не просматривал содержимое класса / локали, но сообщение об ошибке кажется самоочевидным: не удалось объединить типы из-за несовместимого ограничения сортировки для переменной типа '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

person user9716869    schedule 17.05.2019