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

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

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



Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление:
Год:
Том:
Выпуск:
Страница:
Найти






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


Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление, 2017, том 10, выпуск 3, страницы 59–82 (Mi ntitu184)  

Программное обеспечение вычислительных, телекоммуникационных и управляющих систем

Полная головная линейная редукция

Д. А. Березун

Санкт-Петербургский государственный университет

Аннотация: Головная линейная редукция (head linear reduction) представляет собой стратегию редукции лямбда-термов, производящую минимальное количество подстановок для достижения псевдоголовной нормальной формы (quasi-head normal form). Статья посвящена обобщению понятия головной линейной редукции до полной головной линейной редукции (complete head linear reduction), позволяющей полностью нормализовать лямбда-терм и определить новый подход к вычислениям – трассирующую нормализацию (traversal-based normalization). Оба подхода формализованы в виде систем переходов (transition system). В статье также показана корректность обеих стратегий редукций: головной линейной редукции относительно головной редукции – головная линейная редукция завершается в псевдоголовной нормальной форме терма тогда и только тогда, когда завершается головная, и полной головной линейной редукции относительно эффективной редуцирующей стратегии – головная линейная редукция завершается в нормальной форме терма тогда и только тогда, когда последняя существует.

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

DOI: https://doi.org/10.18721/JCSTCS.10306

Полный текст: PDF файл (3432 kB)

Тип публикации: Статья
УДК: 519.682.1

Образец цитирования: Д. А. Березун, “Полная головная линейная редукция”, Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление, 10:3 (2017), 59–82

Цитирование в формате AMSBIB
\RBibitem{Ber17}
\by Д.~А.~Березун
\paper Полная головная линейная редукция
\jour Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление
\yr 2017
\vol 10
\issue 3
\pages 59--82
\mathnet{http://mi.mathnet.ru/ntitu184}
\crossref{https://doi.org/10.18721/JCSTCS.10306}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/ntitu184
  • http://mi.mathnet.ru/rus/ntitu/v10/i3/p59

    ОТПРАВИТЬ: 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
  • Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Информатика. Телекоммуникации. Управление
    Просмотров:
    Эта страница:97
    Полный текст:30
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020