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

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

A deterministic finite automaton M is a 5-tuple Q, Sigma, delta, q0, F, consisting of

• a finite set of states Q
• a finite set of input symbols called the alphabet Sigma
• a transition function delta: Q * Sigma -> Q
• an initial or start state q0 in Q
• a set of accept states F being a subset of 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 в Haskell или fold_left в Ocaml):

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

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

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)).

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

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