мучная машина в ocaml

Question

Я хочу взять композицию из двух машин Мили и двух конечных преобразователей . Как изобразить аппарат / преобразователь Мили в ocaml?

Answer 1

В чем проблема с ответом Николет на ваш предыдущий вопрос?Просто добавьте участника output : 'state * 'letter -> 'output в свою запись, и все готово.

Answer 2

Тип, который вы выбрали в своем ответе, не подходит.

type ('state,'letter) mealy = {
  initial    : 'state ;
  final      : 'state -> bool ;
  transition : 'letter  -> 'state -> 'letter -> 'state ;
}

Действительно, ваш переход не будет производить вывод, но будет использовать его, чтобы узнать, в какое состояние вы попадете.В математических словах вы предоставляете функцию перехода типа $ (I, Q, O) \ rightarrow Q $ вместо $ (I, Q) \ rightarrow (O, Q) $.Curryfication позволяет вам написать $ I \ rightarrow Q \ rightarrow (O, Q) $, но вы не можете раскрыть последний тип пары.Следовательно, ваша композиция ошибочна, поскольку вы ввели d, который не существует.

У вас есть два решения из решения для автоматов в этом посте :

1. с добавлением функции вывода, поскольку Гаш уже предложил
2. , изменяющуютип функции перехода в правильную, например 'state -> 'letter -> ('letter * 'state).

Поэтому вы сможете обеспечить функцию композиции.

Answer 3

Вы можете изучить python реализацию здесь преобразователей Мили в пакете tulip. Обратите внимание, что машины Мура являются строго причинно-следственными машинами Мили, подробности см. В этой книге (большинство авторов ошибаются, поэтому я упоминаю об этом здесь. Вы можете проверить, что машина Мура изначально была действительно определена так, ссылаясь на оригинальную статью Мура).

Когда дело доходит до композиции, все становится очень сложно. Если вы имеете в виду каскадную синхронную композицию, то результат может быть легко вычислен, потому что нет обратной связи. Но если под «составом» вы ссылаетесь на состав обратной связи , то вам нужно выбрать семантику. Например, в синхронно-реактивной семантике результат композиции определяется решением с фиксированной запятой для каждого временного шага (указатели по теме см. В цитированной выше книге).

Требуется решение с фиксированной запятой, потому что, если оба преобразователя являются Мили, то они могут быть не строго причинно-следственными (т. Е. Выходной ток может зависеть от входного тока). Напротив, машина Мура строго причинна (любая машина Мили, которая строго причинна, является машиной Мура, но для не строго причинной машины Мили не существует эквивалентной машины Мура). Таким образом, составление машины Мура с машиной Мили не требует вычисления с фиксированной запятой для имитации результата.