RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2018, том 25, номер 5, страницы 534–548 (Mi mais647)  

Синтез и преобразования программ

Polyprograms and polyprogram bisimulation

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

S. A. Grechanik

Keldysh Institute of Applied Mathematics, 4 Miusskaya sq., Moscow 125047, Russia

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

Ключевые слова: полипрограммы, преобразование программ, насыщение равенствами, бисимуляция.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 18-31-00412_мол_а
Работа выполнена при поддержке гранта РФФИ №18-31-00412.


DOI: https://doi.org/10.18255/1818-1015-534-548

Полный текст: PDF файл (584 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 519.681.3
Поступила в редакцию: 10.09.2018
Язык публикации: английский

Образец цитирования: S. A. Grechanik, “Polyprograms and polyprogram bisimulation”, Модел. и анализ информ. систем, 25:5 (2018), 534–548

Цитирование в формате AMSBIB
\RBibitem{Gre18}
\by S.~A.~Grechanik
\paper Polyprograms and polyprogram bisimulation
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 5
\pages 534--548
\mathnet{http://mi.mathnet.ru/mais647}
\crossref{https://doi.org/10.18255/1818-1015-534-548}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais647
  • http://mi.mathnet.ru/rus/mais/v25/i5/p534

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:35
    Полный текст:9
    Литература:7
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019