Équivalence jusqu'à une longueur

let equivalents a b longueur =
  let nb_sym = Array.length a.delta.(0) in
  let ok = ref true in
  let rec explore reste ea eb =
    if a.acceptants.(ea) <> b.acceptants.(eb) then ok := false;
    if reste > 0 then
      for s = 0 to nb_sym - 1 do
        explore (reste - 1) a.delta.(ea).(s) b.delta.(eb).(s)
      done
  in
  explore longueur a.initial b.initial;
  !ok

On fait avancer simultanément les deux automates (comme dans le produit) le long de tous les préfixes de longueur $\le$ longueur : à chaque étape, l'acceptation doit coïncider. Inutile de construire les mots — seuls comptent les deux états courants (ea, eb). Pour une équivalence exacte (toutes longueurs), on testerait le vide de intersection a (complement b) et réciproquement : l'équivalence des AFD est décidable.