Об интерпретации строго типизированных функциональных программ

• Автор: Будагян, Лусине Эдгаровна
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2006
• Место защиты: Ереван
• Количество страниц: 107 с.

СОДЕРЖАНИЕ
СОДЕРЖАНИЕ.
ВВЕДЕНИЕ.

ГЛАВА 1. ИСПОЛЬЗУЕМЫЕ ОПРЕДЕЛЕНИЯ И РЕЗУЛЬТАТЫ.

ТЕОРЕМА О ЗАМЕНЕ.

1.1. Используемые определения и результаты

1.2. Теорема о замене.

ГЛАВА 2. ФОРМАЛИЗАЦИЯ ПОНЯТИЯ 5РЕДУКЦИИ.

НОРМАЛЬНЫЕ ФОРМЫ

2.1. Понятие 5редукции. Теорема о редукции.

2.2. Сильная нормализуемость

2.3. Естественное понятие 5редукции
2.4. Единственность нормальной формы
ГЛАВА 3. РЕАЛЬНЫЕ ПОНЯТИЯ 5РЕДУКЦИИ. ПРАВИЛА
ВЫЧИСЛЕНИЯ
3.1. Реальное понятие 5редукции
3.2. Правила вычисления. Функция соответствующая правилу вычисления и реальному понятию 5редукции.
3.3. Полнота правила вычисления для фиксированного понятия редукции
3.4. Полнота правила вычисления.
3.5. Полные правила вычисления
3.6. Неполные правила вычисления
ЗАКЛЮЧЕНИЕ.
ЛИТЕРАТУРА


Для таких программ была доказана теорема о существовании наименьшего решения, главная компонента которого, функция /р, является семантикой программы Р, которая достигается на ординале со. Было показано, что для каждой программы Р можно построить программу Р' такую, что Р' не использует констант, порядок которых >2, и/р =/р'. Перед нами была поставлена задача исследовать вопросы, относящиеся к интерпретации строго типизированных функциональных программ общего вида, использующих переменные любого порядка и константы, порядок которых <1, причем интерпретация должна быть основана на правилах вычисления и р5-редукции. Исследованию этих вопросов посвящена данная работа. Диссертация состоит из введения, трех глав, заключения и списка используемой литературы. В главе 1 приводятся используемые определения и результаты, которые берутся нами, как правило, из работ [], [] и []. Это определения монотонного типа, терма (в монотонной модели типового Я-исчисления), значения терма, эквивалентности термов, понятия К-нормальной формы, К-нормализуемости и сильной К-нормализуемости для произвольного понятия редукции К. Приводится понятие редукции и формулируются теоремы О СИЛЬНОЙ Р-нормализуемости терма и о единственности его ^-нормальной формы. Определяется монотонная система уравнений как система уравнений с отделяющимися переменными в монотонной модели типового Я-исчисления и формулируется теорема о существовании наименьшего решения для такой системы уравнений. Семантика программы представляет собой функцию /р, которая являегся главной компонентой ее наименьшего решения. Формулируется теорема, которая утверждает, что по всякой программе Р можно построить программу Р' такую, что Р' не использует констант, порядок которых >7 и /р = /р'. Далее доказывается теорема о замене, позволяющая замену некоторого подтерма на ему эквивалентный; при этом полученный терм будет эквивалентен данному. Эта теорема носит технический характер и служит для получения основных результатов диссертации. Глава 2 посвящена формализации понятия ^-редукции и связанными с этим понятием результатами. В ней рассматриваются термы, которые используют переменные любого порядка и константы, порядок которых <1. Доказываются Теорема 2. I имеет конечную длину, и Теорема 2. Вводится, так называемое, естественное понятие 8-редукции, которое определяется наложением некоторых естественных ограничений на понятие (5-редукции. Если понятие (5-редукции обладает этими двумя свойствами, то мы говорим, что оно обладает ПН-свойством. Доказывается Теорема 2. ПН-свойством. В Главе 3 вводится реальное понятие ^-редукции, которое является эффективным, естественным, обладающим ПН-свойством и замкнутым относительно частичной подстановки понятием (5-редукции. Это именно то понятие (5-редукции, которое встречается на практике. Вводится понятие правила вычисления р, основанного на подстановке правых частей уравнений программы вместо некоторых свободных вхождений переменных терма. Приводятся примеры шести правил вычисления: правило самой левой внутренней замены, правило параллельной внутренней замены, правило самой левой замены, правило параллельной внешней замены, правило замены вхождений свободных для подстановки, правило полной замены. Дается определение последовательности вычисления для программы Р, некоторого реального понятия 3-редукции, правила вычисления р и начального значения. Определяется функция /р'р, соответствующая программе Р, реальному понятию (5-редукции и правилу вычисления р. Доказывается Теорема 3. Р, правила вычисления р и реального понятия 8-редукции функция /р является продолжением функции //,р. Дается определение полноты правила вычисления р для фиксированного понятия ^-редукции, как совпадение функций /р и /рр для любой программы Р. Доказывается Теорема 3. Дается определение полноты правила вычисления р как совпадение функций /р и /рр для любых Р и 8. Доказывается Теорема 3. Устанавливается полнота следующих правил вычисления: полной замены (Теорема 3. Теорема 3. Теорема 3. В заключении сформулированы результаты, воспринимаемые нами как основные.