The Ehrenfeucht conjecture: a compactness claim for finitely generated free monoids

We survey recent results on the so-called Ehrenfeucht Conjecture which states: For each language L over a finite alphabet Σ there exists a finite subset F of L such that for each pair (g, h) of morphisms on Σ¹ the equation g(x)=h(x) holds for all x in L if and only if holds for all x in F.We point out that the conjecture is closely related to the theory of equations in free monoids. We also state a suprising consequence of the conjecture: If it holds (even noneffectively) for all DOL languages, then the HDOL sequence equivalence problem is decidable. Furthermore, we give examples of when the conjecture is known to hold. In particular, we establish it for all binary languages, as well as for all languages when attention is restricted to bounded delay morphisms of some fixed delay.