ISSN: 0137-0782
Поступила: 21.02.2025
Принята к публикации: 19.03.2025
Ключевые слова: автомат-преобразователь, подстановка, эквивалентность, задача унификации
DOI: 10.55959/MSU/0137–0782–15–2025–49–3–74–84
Тяньсян Тан, Захаров В.А. Задача унификации для конечных параметризованных автоматов-преобразователей // Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика. 2025. № 3. С. 74-84 https://doi.org/10.55959/MSU/0137–0782–15–2025–49–3–74–84.
Задача унификации параметризованных автоматов-преобразователей состоит в том, чтобы для двух заданных автоматов найти такие значения их параметров, при которых эти автоматы будут вычислять одинаковые отношения трансдукции. В статье представлен квадратичный по времени алгоритм вычисления наиболее общих унификаторов конечных параметризованных детерминированных автоматов-преобразователей. Этот алгоритм построен на основе алгоритма Мартелли–Монтанари унификации термов и алгоритма проверки эквивалентности детерминированных автоматов-преобразователей.
R o b i n s o n J . A . A machine-oriented logic based on the resolution principle // Journal of the ACM. 1965. 12. N 1. P. 23–41.
B a a d e r F ., S n y d e r W. Unification theory // Handbook of Automated Reasoning. I. Eds. Robinson J.A., Voronkov A. 2001. P. 447–533.
M a r t e l l i A ., M o n t a n a r i U . An efficient unification algorithm // ACM Transactions on Program, Languages and Systems. 1982. 4. N 2. P. 258–282.
D w o r k D ., K a n e l l a k i s P. C ., M i c h e l l J . C . On the sequential nature of unification // Journal of Logic Programming. 1984. 1. P. 35–50.
G o l d f a r b W. D . The undecidability of the second-order unification problem // Theoretical Computer Science. 1981. 13. N 2. P. 225–230.
H e r o l d A ., S i e c k m a n n J . Unification in Abelean semigroups // Journal of Automated Reasoning. 1983. 3. P. 247–283.
L i n c o l n P., C h r i s t i a n J . Adventures in associative-commutative unification // Journal of Symbolic Computation. 1989. 8. P. 393–416.
S t i c k e l E . M . A unification algorithm for associative-commutative functions // Journal of the Association for Computing Machinary. 1981. 28. N 5. P. 423–434.
М а к а н и н Г . С . Проблема разрешимости уравнений в свободной полугруппе // Математический сборник. 1977. 103. N 2. С. 147–236.
P l a n d o w s k i W. Satisfiability of word equations with constants is in PSPACE // Journal of the ACM. 2004. 51. N 3. P. 483–496.
Н о в и к о в а Т. А ., З а х а р о в В . А . Унификация программ // Труды Института системного программирования РАН. 2012. 23. С. 455–476.
Н о в и к о в а Т. А ., З а х а р о в В . А . Двусторонняя унификация программ и ее применение для задач рефакторинга // Труды Института системного программирования РАН. 2014. 26. С. 245–268.
Ta n g T ., Z a k h a r o v V . A . On the complexity of decision problems for parameterized finite state synchronous transducers // Implementation and Application of Automata. CIAA 2024. Lecture Notes in Computer Science. Ed. Fazekas S. Z. Vol. 15015. Springer, 2024. P. 332–346.
G u r a r i E ., I b a r r a O . A note on finite-valued and finitely ambiguous transducers // Mathematical Systems Theory. 1983. 16. P. 61–66.
З а х а р о в В . А . Эффективные алгоритмы проверки эквивалентности для некоторых классов автоматов // Моделирование и анализ информационных систем. 2020. 27. № 3. С. 260–303.
B l a t t n e r M ., H e a d T . The decidability of equivalence for deterministic finite transducers // Journal of Computer and System Sciences. 1979. 19. P. 45–49.
B a u m g a r t n e r A ., K u t s i a T . A library of anti-unification algorithms // Logics in Artificial Intelligence. JELIA 2014. Lecture Notes in Computer Science. Eds. Ferme E., Leite J. Vol. 8761. Springer, 2014. P. 543–557.
