Детальная информация

Название: Полная головная линейная редукция // Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Сер.: Информатика. Телекоммуникации. Управление: научное издание. – 2017. – Т. 10, № 3
Авторы: Березун Павел Дмитриевич
Организация: Санкт-Петербургский государственный университет
Выходные сведения: Санкт-Петербург: Изд-во Политехн. ун-та, 2017
Коллекция: Общая коллекция
Тематика: Математика; Вычислительная математика; pseudovolume forms (mathematics); reduction; лямбда-термы; головные линейные редукции; полные головные линейные редукции; трассирующая нормализация; линейные редукции; псевдоголовные формы (математика); редукции; linear reduction; head linear reduction; full head linear reduction; tracer normalization; lambda baths
УДК: 519.6
ББК: 22.19
Тип документа: Статья, доклад
Тип файла: PDF
Язык: Русский
Ссылки: http://doi.org/10.18721/JCSTCS.10306

Разрешенные действия: Прочитать Загрузить (3,4 Мб) Для чтения документа необходим Flash Player

Группа: Анонимные пользователи

Сеть: Локальная сеть ИБК СПбПУ

Аннотация

The paper is dedicated to the generalization of head linear reduction to a complete head linear reduction which yields normal forms when they exist. The formal presentation of both head linear reduction and complete head linear reduction via transition systems is provided. We also proved that both reduction strategies are correct: head linear reduction with respect to head reduction, i.e., that head linear reduction terminates in quasi-head normal form if and only if head reduction terminates, and we proved that complete head linear reduction is an effective reduction strategy, i.e., it terminates if and only if the normal form exists.

Обобщены понятия головной линейной редукции до полной головной линейной редукции, позволяющей полностью нормализовать лямбда-терм и определить новый подход к вычислениям – трассирующую нормализацию. Оба подхода формализованы в виде систем переходов. Показана корректность обеих стратегий редукций: головной линейной редукции относительно головной редукции – головная линейная редукция завершается в псевдоголовной нормальной форме терма тогда, когда завершается головная, и полной головной линейной редукции относительно эффективной редуцирующей стратегии – головная линейная редукция завершается в нормальной форме терма тогда, когда последняя существует.

Права на использование объекта хранения

Место доступа Группа пользователей Действие
-> Локальная сеть ИБК СПбПУ Все Прочитать Печать Загрузить
Интернет Все Прочитать Печать Загрузить

Статистика использования документа

stat Количество обращений: 177
За последние 30 дней: 3
Подробная статистика