Могу ли я построить структуру 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

И затем, эти детали:

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.

Забыл сказать, эта проблема возникает в «locale while_unfold».

hidaidai 17.05.2019 13:49
Стоит ли изучать 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 называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
2
1
103
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

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

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

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