Полипрограммы и бисимуляция полипрограмм

Полипрограмма — это обобщение программы, допускающее множественность определений одной и той же функции. Подобные объекты возникают в различных системах преобразования программ, таких как система Бёрстолла–Дарлингтона и насыщение равенствами. В данной работе мы вводим понятие полипрограммы на нестрогом функциональном языке первого порядка. Мы определяем денотационную семантику полипрограмм и описываем некоторые преобразования полипрограмм в двух разных стилях: в стиле системы Бёрстолла–Дарлингтона и в стиле насыщения равенствами. Преобразования в стиле насыщения равенствами осуществляются над полипрограммами в расчленённой форме, в которой стирается грань между функциями и выражениями и между подстановкой и раскрытием вызова функции. Расчленённые полипрограммы хорошо подходят для реализации и проведения рассуждений, но трудны для человеческого восприятия. Мы также вводим понятие бисимуляции полипрограмм, на котором основано преобразование — слияние по бисимуляции, соответствующее доказательству эквивалентности функций по индукции или коиндукции. Бисимуляция полипрограмм — понятие, вдохновлённое понятием бисимуляции размеченных систем переходов, но несколько от него отличающееся, поскольку бисимуляция полипрограмм рассматривает каждое определение как самодостаточное, т.е. функция полипрограммы задаётся любым своим определением, в то время как в размеченной системе переходов поведение системы в состоянии определяется всей совокупностью переходов, которые можно осуществить из этого состояния. Мы предлагаем алгоритм перечисления бисимуляций некоторого определённого вида. Алгоритм состоит из двух фаз: перечисление пребисимуляций и преобразование их в бисимуляции. Такое разделение требуется из-за того, что бисимуляции полипрограмм учитывают возможность перестановки параметров функций. Мы доказываем корректность данного алгоритма, а также формулируем некоторую слабую форму его полноты. Статья публикуется в авторской редакции.

1. Abel A., Altenkrich T., “A predicative analysis of structural recursion”, Journal of Functional Programming, 12:1 (2002), 1-41.

2. Ariola Z. M., Klop J. W., Plump D., “Bisimilarity in Term Graph Rewriting”, Information and Computation, 156 (2000), 2-24.

3. Burstall R. M., Darlington J., “A transformation system for developing recursive programs”, Journal of the ACM, 24:1 (1977), 44-67.

4. Emelyanov P., “Analysis of equality relationships for imperative programs”, CoRR, 2006, https://arxiv.org/abs/cs/0609092.

5. Grechanik S., “Inductive prover based on equality saturation (extended version)”, Proceedings of the Fourth International Valentin Turchin Workshop on Metacomputation, 2014, 26-53.

6. Nelson G., Oppen D.C., “Fast decision procedures based on congruence closure”, Journal of the ACM, 27:2 (1980), 356-364.

7. Sands D., “Total correctness by local improvement in the transformation of functional programs”, ACM TOPLAS, 18:2 (1996), 175-234.

8. Tate R., Stepp M., Tatlock Z., Lerner S., “Equality saturation: a new approach to optimization”, SIGPlAn Not., 44:1 (2009), 264-276.

9. Turchin V., “The concept of a supercompiler”, ACM TOPLAS, 8:3 (1986), 292-325.

10. Scott D.S., “Domains for Denotational Semantics”, Automata, Languages, and Programming: 9th Colloquium Aarhus, Denmark, Lecture Notes in Computer Science, 140, 1982, 577-610.

11. Klyuchnikov I., Romanenko S., “Towards Higher-Level Supercompilation”, Proceedings of the Second International Workshop on Metacomputation in Russia, 2010, 82-101.