Repository navigation
Divisible/Decidable instances for DA #8
Description
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.
Activity
[-]Contravariant Functor instances for DA[/-][+]Divisible/Decidable instances for DA[/+]subttle commentedon Jun 1, 2019
I suppose it is also worth me mentioning/considering that the type variable order here for
DA q sis arbitrary and could be defined the other way, i.e.Although that would require some fancy work to map over states because a
DA sinstance is then both covariant and contravariant (i.e. invariant) inqfor the transition function, but for some reason I suspect there might be a fancy math way around that?subttle commentedon Jun 6, 2019
Looked at this for a bit today, seems like bisimulation/perfect-shuffle and shuffle for
DivisibleandDecidableofDA 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 commentedon Jun 6, 2019
(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 commentedon Jun 6, 2019
Some properties of shuffle:
https://www.planetmath.org/shuffleoflanguages
subttle commentedon Jun 7, 2019
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.
add experimental Divisible and Decidable DA