Как создать конечный автомат из индуктивных типов в Coq? - PullRequest
Новая
       40

Как создать конечный автомат из индуктивных типов в Coq?

0 голосов
/ 21 июня 2019

Как можно создать правильный конечный автомат (без способа построить его недопустимым образом) в Coq полностью из индуктивных типов?

Начиная с чего-то вроде: 

Inductive Cmd :=
| Open
| Send
| Close.

Inductive SocketState :=
| Ready
| Opened
| Closed.

Например, переход из состояния готовности в открытое состояние должен происходить только после команды открытия.

Ответы [ 2 ]

2 голосов
/ 23 июня 2019

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

Inductive Valid_transition : SocketState -> SocketState  -> Type :=
| copen x : x = Open -> Valid_transition Ready Opened (* Input command Open *)
| cready x y : x = Send -> Valid_transition y Opened ->
             Valid_transition Opened Opened (* Send command would not change the 
                                               status of port *)
| cclose x y : x = Close -> Valid_transition y Opened ->
             Valid_transition Opened Closed. (* Close command would close it *)


Check (cready Send _ eq_refl (copen Open eq_refl)).

Единственный способ перейти от Ready to Opened - это первый конструктор с командой Open. Второй конструктор утверждает, что если ваша команда - Отправить, и вы находитесь в открытом состоянии, то вы продолжите оставаться в этом состоянии. Наконец, третий конструктор закрывает открытый порт после получения команды Close. Я закодировал такую ​​же функцию перехода, как ваша (подсчет голосов как конечный автомат), так что не стесняйтесь взглянуть на нее [1].

[1] https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/Workingcode/EncryptionSchulze.v#L718-L740

2 голосов
/ 21 июня 2019

Из формальное определение детерминированного конечного автомата :

Детерминированный конечный автомат M представляет собой 5-кортеж Q, Sigma, delta, q0, F, состоящий из

  • конечный набор состояний Q
  • конечный набор входных символов, называемый алфавитом Sigma
  • функция перехода delta: Q * Sigma -> Q
  • начальное или начальное состояние q0 в Q
  • набор состояний принятия F, являющийся подмножеством Q

Вы далидва из пяти, а именно Q = SocketState и Sigma = Cmd.Предполагая, что ваше приложение имеет неявное начальное состояние (вероятно, Ready) и не имеет определенных "принимающих состояний", единственной вещью, необходимой для вашего конечного автомата, является функция перехода .

ИзПо определению, функция перехода имеет тип (SocketState * Cmd) -> SocketState, но версия с карри SocketState -> Cmd -> SocketState не менее мощна.

Если у вашего конечного автомата есть внешние входы, добавьте их в качестве параметров в функцию.Если вам нужны побочные эффекты или какой-либо вывод, связанный с самим переходом, вы можете использовать SocketState -> Cmd -> (SomeOutput * SocketState).

Редактировать: Переход как отношение (Расширение до ответ keep_learning )

Если вы хотите рассуждать о серии допустимых команд и переходов, вы можете вместо этого закодировать их в троичное отношение.

Сначала давайте определим, чтосоставляет для действительных переходов. 

Previous state -> (Command) -> Next state
-----------------------------------------
Ready          -> (Open)    -> Opened
Opened         -> (Send)    -> Opened
Opened         -> (Close)   -> Closed

Затем закодируйте его как троичное отношение.Ниже приведен только пример, похожий на тройки Хоара из моделей языков программирования. 

Inductive Transition : SocketState -> Cmd -> SocketState -> Prop :=
  | t_open  : Transition Ready  Open  Opened
  | t_send  : Transition Opened Send  Opened
  | t_close : Transition Opened Close Closed.

Выше говорилось о одномоментном переходе.А как насчет серии переходов?Мы можем определить рефлексивно-транзитивное замыкание, принимая list команд (это очень аналогично тройкам Хоара, в том смысле, что оба определяют предусловие, последовательность шагов и постусловие):

From Coq Require Import List.
Import ListNotations.

Inductive TransitionRTC : SocketState -> list Cmd -> SocketState -> Prop :=
  | t_rtc_refl : forall s : SocketState, TransitionRTC s [] s
  | t_rtc_trans1 : forall s1 c s2 clist s3,
      Transition s1 c s2 ->
      TransitionRTC s2 clist s3 ->
      TransitionRTC s1 (c :: clist) s3.

Функциональным аналогом отношения RTC будет (у fold_left в Coq последние два аргумента поменялись местами, по сравнению с foldl Хаскелла или fold_left у Окамла): 

Axiom transition : SocketState -> Cmd -> SocketState.
Definition multistep_transition (state0 : SocketState) (clist : list Cmd) :=
  fold_left transition clist state0.
...