Difficulty: easy — 2 definitions, 0 abbreviations, 0 lemmas, 0 theorems.
Finite state machines: Mealy machines whose state, input, and output types are all finite. We build this up in stages: first the machine itself, then behavioural properties (such as predictability), and only afterwards do we say anything about Size, by instantiating a machine as an InformationSystem.
A finite state machine (a Mealy machine over finite types): given a state and an input, it produces an output and transitions to a new state.
sequential-circuits
structure FiniteStateMachine (State Input Output : Type)
[Fintype State] [Fintype Input] [Fintype Output]
[Nonempty State] [Nonempty Input] [Nonempty Output] where
step : State → Input → State × Output
Outer dependencies: (none)
A finite state machine is reversible when its step function is injective: no two distinct (state, input) pairs are ever collapsed onto the same (state, output) result. Equivalently, the result of a step always carries enough information to recover exactly which state and input led to it — nothing about where it came from is ever lost.
def FiniteStateMachine.Reversible (fsm : FiniteStateMachine State Input Output) : Prop :=
Function.Injective (fun p : State × Input => fsm.step p.1 p.2)
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.
definitiondeclared elsewheredependencyproof dependency
legend