Skip to content

Instantly share code, notes, and snippets.

@goretkin
Created February 6, 2025 16:37
Show Gist options
  • Save goretkin/623625fbeefe930a135d1390c81f70ce to your computer and use it in GitHub Desktop.
Save goretkin/623625fbeefe930a135d1390c81f70ce to your computer and use it in GitHub Desktop.
-- A Mealy machine is a 6-tuple ( S , S 0 , Σ , Λ , T , G ) {\displaystyle (S,S_{0},\Sigma ,\Lambda ,T,G)} consisting of the following:
-- a finite set of states S {\displaystyle S}
-- a start state (also called initial state) S 0 {\displaystyle S_{0}} which is an element of S {\displaystyle S}
-- a finite set called the input alphabet Σ {\displaystyle \Sigma }
-- a finite set called the output alphabet Λ {\displaystyle \Lambda }
-- a transition function T : S × Σ → S {\displaystyle T:S\times \Sigma \rightarrow S} mapping pairs of a state and an input symbol to the corresponding next state.
-- an output function G : S × Σ → Λ {\displaystyle G:S\times \Sigma \rightarrow \Lambda } mapping pairs of a state and an input symbol to the corresponding output symbol.
-- In some formulations, the transition and output functions are coalesced into a single function T : S × Σ → S × Λ {\displaystyle T:S\times \Sigma \rightarrow S\times \Lambda }.
-- A Moore machine is the same, except the output function can only depend on the state, and not the input
inductive StateMachineType
-- [tag:state_machine_type_cases_order]
| Moore
| Mealey
-- [tag:in_the_type_or_in_the_value]
-- In this formulation, the machine "type" is encoded in the type type.
-- An alternative formulation would just have a sum type over possible output types
-- but then you would carry a proof, too.
-- This is a design question about intrinsic versus extrinsic properties...
-- https://goosetaco.notion.site/Put-it-in-the-type-or-in-the-value-2d6b480b02ca44f79dffb8760a9ee8c8
structure StateMachine
(machine_type : StateMachineType)
(input_space : Type)
(output_space : Type)
where
state_space : Type
s0 : state_space
transition : state_space -> input_space -> state_space
output : match machine_type with
-- surprisingly, this has to match the order too?
-- [ref:state_machine_convoy_pattern]
-- [ref:state_machine_type_cases_order]
| .Moore => state_space -> output_space
| .Mealey => state_space -> input_space -> output_space
inductive TwoThings where
| zero
| one
inductive ThreeThings where
| zero
| one
| two
-- This is a machine that outputs the count, mod 3, of how many times a `one` came in
def counter_mod_3 :
StateMachine
.Mealey
(input_space := TwoThings)
(output_space := ThreeThings)
:= {
state_space := ThreeThings,
s0 := ThreeThings.zero,
transition := fun x y =>
match x, y with
| _, .zero => x
| .zero, .one => .one
| .one, .one => .two
| .two, .one => .zero,
output := fun x _ => x
}
def moore_to_mealey (i o: Type) (moore : StateMachine .Moore i o ) : StateMachine .Mealey i o
:= {
state_space := moore.state_space,
s0 := moore.s0,
transition := moore.transition
output := fun x _ => moore.output x
}
-- just debugging stuff
#check StateMachineType.casesOn
#check StateMachineType.recOn
def transduce_helper
(mt : StateMachineType)
(i o : Type)
(machine : StateMachine mt i o) -- this carries s0, but we do not need it
(current_state : machine.state_space)
(input : List i)
:=
match input with
| List.nil => List.nil
| List.cons y ys =>
let next_state := machine.transition current_state y
let s := machine.state_space
-- [tag:state_machine_convoy_pattern]
-- [ref:in_the_type_or_in_the_value]
let a_motive (mt2 : StateMachineType) :=
let machine_dot_output_type := match mt2 with
-- s->o and s->i->o are the types of machine.output
| .Moore => (s -> o)
| .Mealey => (s -> i -> o)
machine_dot_output_type -> o
let make_next_output :=
(
StateMachineType.casesOn
(
motive := a_motive
)
mt
-- [ref:state_machine_type_cases_order]
(fun f => f current_state)
(fun f => f current_state y)
)
let next_output := make_next_output machine.output
(List.cons next_output (transduce_helper mt i o machine next_state ys))
def transduce (mt : StateMachineType) (i o : Type) machine ys :=
transduce_helper mt i o machine machine.s0 ys
def input := [TwoThings.zero, .one, .one, .zero, .one, .one]
def output := transduce _ _ _ counter_mod_3 input
#reduce output
-- This is my first time seeing a dependent fold, where the "accumulator" changes type
-- (Yes, I have an imperative for-loop-y brain)
-- Some notes
-- fold : (motive : Type) -> (T : Type) -> List T -> (init : motive) -> (motive -> T -> motive) -> motive
-- fold :
-- (motive : List T -> Type)
-- -> (T : Type)
-- -> (a : List T)
-- -> (init : motive [])
-- -> ((tail : List T) -> motive tail -> (head: T) -> motive (cons head tail))
-- -> motive a
theorem moore_to_mealey_same_state_space
(i o: Type) (moore : StateMachine .Moore i o ) :
moore.state_space = (moore_to_mealey _ _ moore).state_space :=
Eq.refl _
theorem moore_to_mealey_same_io_behavior
(i o: Type) (moore : StateMachine .Moore i o ) (is : List i):
let mealey := (moore_to_mealey _ _ moore)
transduce _ _ _ moore is = transduce _ _ _ mealey is
:= by
induction is with
| nil => rfl
| cons head tail tail_ih =>
simp
unfold transduce
unfold transduce_helper
simp
apply And.intro
. unfold moore_to_mealey
simp
-- hmm this is not the right track
. unfold moore_to_mealey
simp
unfold transduce at tail_ih
unfold transduce_helper
simp
sorry
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment