Divisible/Decidable instances for DA

[subttle]

I can write code which type checks for these instances (see below) but I need to explore what the correlations are and what the interpretation should be to operations on regular languages. For example, contramap is quite close to the definition of inverse homomorphism of a regular language (a constructive proof is typically given for DFA), except that the morphism function is usually given in textbooks as (s → [g]) or sometimes equivalently ([s] → [g]). I'm not sure it's okay to say contramap would suffice for invhom despite being polymorphic because morphisms which "erase" might be troublesome. Even if we let the co-domain of h be some finite list type for example, I think it would still need a way to concat, or perhaps it would not matter, I'll have to think more about that.

instance Contravariant (DA q) where
    contramap ∷ (s → g) → DA q g → DA q s
    contramap h m@(DA _ t) = m { transition = \q → t q . h }

-- some ideas to consider (non-exhaustive):
-- https://en.wikipedia.org/wiki/Krohn%E2%80%93Rhodes_theory
-- https://liacs.leidenuniv.nl/~hoogeboomhj/second/secondcourse.pdf
-- https://is.muni.cz/th/jz845/bachelor-thesis.pdf
-- https://drona.csa.iisc.ac.in/~deepakd/atc-2015/algebraic-automata.pdf
-- http://www.cs.nott.ac.uk/~psarb2/MPC/FactorGraphsFailureFunctionsBiTrees.pdf
-- https://cstheory.stackexchange.com/questions/40920/generalisation-of-the-statement-that-a-monoid-recognizes-language-iff-syntactic
instance Divisible (DA q) where
    divide ∷ (s → (g₁, g₂)) → DA q g₁ → DA q g₂ → DA q s
    divide f (DA o₁ t₁) (DA o₂ t₂) = DA { output     = undefined  -- \q → o₁ q ∧ o₂ q -- or even something way more complicated!
                                        , transition = undefined --  \q s → case f s of (b, c) → t₂ (t₁ q b) c  -- remember that the types also allow composition in the other direction too!
                                        -- , transition = \q s → uncurry (t₂ . t₁ q) (f s)
                                        --, transition = \q → uncurry (t₂ . t₁ q) . f
                                        }

    conquer ∷ DA q a
    conquer = DA { output     = const True
                 , transition = const
                 }

instance Decidable (DA q) where
    lose ∷ (a → Void) → DA q a
    lose _ = empty

    choose ∷ (s → Either g₁ g₂) → DA q g₁ → DA q g₂ → DA q s
    choose f (DA o₁ t₁) (DA o₂ t₂) = DA { output     = undefined -- \q → o₁ q ∨ o₂ q
                                        , transition = undefined -- \q → either (t₁ q) (t₂ q) . f
                                        }

May also want to consider making a data type for semi automata in case there are multiple good interpretations each with different output definitions. But that is just speculation for now.

[subttle]

I suppose it is also worth me mentioning/considering that the type variable order here for DA q s is arbitrary and could be defined the other way, i.e.

-- could define new type like this
data DA s q =
     DA { output     ∷ q → Bool
        , transition ∷ q → (s → q)
        }

-- (or even avoid that and just do a type level flip)

Although that would require some fancy work to map over states because a DA s instance is then both covariant and contravariant (i.e. invariant) in q for the transition function, but for some reason I suspect there might be a fancy math way around that?

[subttle]

Looked at this for a bit today, seems like bisimulation/perfect-shuffle and shuffle for Divisible and Decidable of DA q. I fought it for a bit because shuffle is typically defined using product of states, but finally finding an alternative definition:

h (h₁⁻¹ (L₁) ∩ h₂⁻¹ (L₂))

Looks like what I want :)

See 3.3 slide 18: https://liacs.leidenuniv.nl/~hoogeboomhj/second/secondcourse.pdf

Next I think I want to better understand shuffle in terms of the unique morphism from the final automaton of languages. See Section 7: https://homepages.cwi.nl/~janr/papers/files-of-papers/1998_CONCUR_automata_and_coinduction.pdf

[subttle]

(17) and (18) from https://homepages.cwi.nl/~janr/papers/files-of-papers/1998_CONCUR_automata_and_coinduction.pdf

This is in fact equivalent to the following classical theorem by Nerode and Myhill. Let Rₗ be an equivalence relation on A defined, for v and w in A, by

v Rₗ w iff ∀ u ∈ A*, vu ∈ L ⇔ wu ∈ L

[subttle]

Some properties of shuffle: https://www.planetmath.org/shuffleoflanguages

[subttle]

Unicode for shuffle: ⧢

"Shuffe factorization is unique" :) https://www.sciencedirect.com/science/article/pii/S0304397500004333 by Jean Berstel, Luc Boasson

And: "The shuffle product was introduced by Eilenberg & Mac Lane (1953). The name "shuffle product" refers to the fact that the product can be thought of as a sum over all ways of riffle shuffling two words together: this is the riffle shuffle permutation. The product is commutative and associative." https://en.wikipedia.org/wiki/Shuffle_algebra#Shuffle_product

u ⧢ ε = ε ⧢ u = u ua ⧢ vb = (u ⧢ vb)a + (ua ⧢ v)b

One question I need to resolve is the identity.