Created
February 6, 2025 16:37
-
-
Save goretkin/623625fbeefe930a135d1390c81f70ce to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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