Об интерпретации строго типизированных функциональных программ тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Будагян, Лусине Эдгаровна

• Будагян, Лусине Эдгаровна
• кандидат физико-математических наук
• 2006

Оглавление диссертации кандидат физико-математических наук Будагян, Лусине Эдгаровна

СОДЕРЖАНИЕ.

ВВЕДЕНИЕ.

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

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

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

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

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

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

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

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

2.3. Естественное понятие 8-редукции.

2.4. Единственность нормальной формы.

ГЛАВА 3. РЕАЛЬНЫЕ ПОНЯТИЯ 5-РЕДУКЦИИ. ПРАВИЛА

ВЫЧИСЛЕНИЯ.

3.1. Реальное понятие 8-редукции.

3.2. Правила вычисления. Функция соответствующая правилу вычисления и реальному понятию 8-редукции.

3.3. Полнота правила вычисления для фиксированного понятия ^-редукции.

3.4. Полнота правила вычисления.

3.5. Полные правила вычисления.

3.6. Неполные правила вычисления.

Введение диссертации (часть автореферата) на тему «Об интерпретации строго типизированных функциональных программ»

В предлагаемой диссертационной работе исследуются вопросы, относящиеся к интерпретации строго типизированных функциональных программ, использующих переменные и константы любых порядков. Строго типизированная функциональная программа представляет собой систему уравнений с отделяющимися переменными в монотонной модели типового Л-исчисления. Рассматриваемая нами интерпретация основана на правилах вычисления, использующих подстановку правых частей уравнений программы вместо некоторых свободных вхождений переменных, и последующей ^редукции терма.

Началом исследований такого рода является работа 3. Манны (Z. Manna) [16], глава 5 (русс. пер. [27]), где рассматривались функциональные программы, использующие переменные и константы, порядок которых <1 и которые не использовали Я-абстракцию. Для таких программ была доказана теорема о существовании наименьшего решения, главная компонента которого /р являлась семантикой программы Р. Далее рассматривались шесть правил вычисления, и проводилось сравнение функций, соответствующих этим правилам, с функцией, являющейся семантикой программы. В том случае, когда эти функции совпадали, правило вычисления называлось правилом неподвижной точки (мы такое правило будем называть полным). В том же случае, когда правило вычисления не являлось правилом неподвижной точки, функция, являющаяся семантикой программы, являлась продолжением функции, соответствующей этому правилу.

В работах [28], [29] рассматривались строго типизированные функциональные программы общего вида. Такие программы представляют собой системы уравнений с отделяющимися переменными в монотонной модели типового А,-исчисления, которые используют переменные и константы любых порядков, причем константы порядка 1 являются вычислимыми функциями, а константы, порядок которых >2, -эффективно представимыми. Для таких программ была доказана теорема о существовании наименьшего решения, главная компонента которого, функция/?, является семантикой программы Р, которая достигается на ординале со. Было показано, что для каждой программы Р можно построить программу Р' такую, что Р' не использует констант, порядок которых >2, и/р =/р'.

Перед нами была поставлена задача исследовать вопросы, относящиеся к интерпретации строго типизированных функциональных программ общего вида, использующих переменные любого порядка и константы, порядок которых <1, причем интерпретация должна быть основана на правилах вычисления и р5-редукции. Такое исследование должно включать:

• формализацию понятия ^-редукции, исследование этой формализации;

• формализацию понятия правила вычисления, исследование этого понятия;

• рассмотрению конкретных правил вычисления (аналогичных рассмотренным в [16]) и исследование этих правил на вопрос полноты.

Исследованию этих вопросов посвящена данная работа. Диссертация состоит из введения, трех глав, заключения и списка используемой литературы.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Будагян, Лусине Эдгаровна

Основные результаты диссертации следующие:

1. Формализовано понятие 5-редукции в монотонных моделях типового А,-исчисления, использующих константы порядка <1. Доказана Теорема 2.1.1, утверждающая, что любая 5-редукция терма приводит к терму эквивалентному данному. Получены результаты о сильной 5-нормализуемости и о сильной /?5-нормализуемости терма.

2. Введено, так называемое, естественное понятие 5-редукции, которое определяется наложением некоторых естественных ограничений на понятие (5-редукции. Описано ПН-свойство (свойство подстановочности и наследуемости) для понятия 5-редукции и доказана теорема, утверждающая, что для любого понятия (5-редукции терм редуцируется к единственной нормальной форме тогда и только тогда, когда понятие «5-редукции обладает ПН-свойством.

3. Дано определение реального понятия 5-редукции, которое является эффективным, естественным понятием 5-редукции, обладающим ПН-свойством и замкнутым относительно частичной подстановки. Это именно то понятие 5-редукции, которое встречается на практике. Введено понятие правила вычисления р (основанного на подстановке правых частей уравнений программы вместо некоторых свободных вхождений переменных терма) и последовательности вычисления (для программы Р, реального понятия 5-редукции, правила вычисления р и начального значения входных переменных). Определена функция fp'p, соответствующая программе Р, реальному понятию ^-редукции и правилу вычисления р. Доказана теорема, утверждающая, что для любой программы Р, правила вычисления р и реального понятия ^-редукции функция /р, являющаяся семантикой программы Р, есть продолжение функции fp,p.

4. Введено понятие полноты правила вычисления р для фиксированного реального понятия «5-редукции как совпадение функций /р и fp'p для любой программы Р. Доказана теорема, утверждающая, что так называемая существенность подстановки на каждом шаге построения последовательности вычисления является необходимым и достаточным условием полноты правила вычисления р при фиксированном реальным понятии ^-редукции.

5. Введено понятие полноты правила вычисления р как совпадение функций /р и fp,p для любых Рид. Доказана теорема, утверждающая, что всякое правило вычисления р является полным тогда и только тогда, когда оно полно для некоторого реального понятия ^-редукции.

6. Рассмотрены шесть правил вычисления: самой левой внутренней замены, параллельной внутренней замены, самой левой замены, параллельной внешней замены, замены вхождений свободных для подстановки, полной замены. Установлена полнота следующих правил вычисления: полной замены параллельной внешней замены и самой левой замены в случае программ, использующих естественно расширенные функции и функцию ifthenelse. Установлена неполнота следующих правил: самой левой внутренней замены, параллельной внутренней замены, самой левой замены, замены вхождений свободных для подстановки.

103

ЗАКЛЮЧЕНИЕ

Список литературы диссертационного исследования кандидат физико-математических наук Будагян, Лусине Эдгаровна, 2006 год

1. Barendregt Н.Р. The lambda calculus, its syntax and semantics.//Amsterdam: North Holland, 1981 (русск. пер. Барендрегт X. Ламбда-исчисление, его синтаксис и семантика.//М.: Мир, 1985,606 е.).

2. Barendregt Н.Р. Lambda calculi with types. // Hanbook of Logic in Computer Science, Volume 2, Edited by S. Abramsky, D.M. Gabbay and T.S.E. Maibaum, Oxford University Press, 1992, p. 117-309.

3. Barendregt H.P.The impact of the lambda calculus in logic and computer science. // The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.

4. Backus J.W. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs.//Communications of the ACM, v. 21, N 8, 1978, p. 613-641.

5. Budaghyan L.E. Formalizing the notion of S-reduction in monotonic models of typed ^-calculus.// Algebra, Geometry & Their Applications, Vol. 1, Yerevan State University Press, Yerevan, 2002, p. 48-57.

6. Budaghyan L. E. On 8-reduction in monotonic models of typed ^-calculus. // Proceeding of the Conference of Computer Science and Information Technologies (CSIT-2003), Publishings House of NAS of RA, 2003, pp. 65-67.

7. Dijkstra E.W. A discipline of programming.//Prentice Hall, Englewood Cliffs, 1976 (русск. пер. Дейкстра Э. Дисциплина программирования.//М.: Мир, 1978).

8. Field A.J., Harrison P.G. Functional programming.// Addison-Wesley Pub. Co., 1988 (русск. пер. Филд А., Харрисон П. Функциональное программирование.//М.: Мир, 1993,638 е.).

9. Graham P. ANSI Common Lisp. // Prentice Hall, 1995,432p.

10. Gunter C. A. Semantics of programming languages.//MIT Press, 1992,419p.

11. Henderson P. Functional programming. Application and implementation.//Prentice-Hall Int., 1980 (русск. пер.

12. Хендерсон П. Функциональное программирование. Применение и реализация.//М.: М, 1983,349 е.).

13. Hindley J.R., Seldin J.P. Essays on Combinatory Logic, Lambda-Calculus and Formalism. //Academic Press. New York and London, 1980.

14. Kleene S. C. Introduction to metamathematics.// D. Van Nostrand Co.,1952 (русск. пер. Клини С.К. Введение в метаматематику.// М.: Иностранная литература, 1957,526 е.).

15. Manna Z. Mathematical theory of computation.// McGraw-Hill Book Co., 1974,447p.

16. Maurer W.D. The Programmer's introduction to LISP.// Magdonald and American Elsevier Inc., 1972 (русск. пер. Maypep у. Введение в программирование на языке ЛИСП.//М.: Мир, 1976,104 е.).

17. Nigiyan S.A., Budagyan L.E. On execution of functional programs.// Proceedings of the Conference CSIT-99. Publishing House of NAS of RA, Yerevan, 1999, p. 33-35.

18. Nigiyan S.A. On equation systems in monotonic models of typed A- calculus.//Algebra, Geometry & Their Applications, YSU, Vol.1,2001, p. 11-19.

19. Rogers H. Theory of recursive functions and effective computability. McGraw-Hill Book Co., 1967 (русск. пер. Роджерс X. Теория рекурсивных функций и эффективная вычислимость.// М.: Мир, 1972,624 е.).

20. Scott D.S. Outline of a mathematical theory of computation.//Proc. Princeton Conf. on Information Sci., 1971.

21. Scott D.S. and Strachey C. Towards a mathematical semantics for computer languages.//In. J.Fox, editor, Computers and Automata, p.19-46, Politechnic Institute of Brooklyn Press. 1971.

22. Stoy J. Denotational semantics: the Scott-Strachey approach to programming language theory.//MIT Press, 1977.

23. Winskel G. The Formal Semantics of Programming Languages.// The MIT Press, 1994.

24. Будагян Л.Э. О формализации понятия 5-редукции в монотонных моделях типового ^-исчисления. // Учёные записки, ЕГу, №1,2003, стр. 27-36.

25. Мальцев А.И. Алгоритмы и рекурсивные функции. //М.: Наука, 1984,432 с.

26. Манна 3. Теория неподвижной точки программ.// Кибернетический сборник (новая серия), вып. 15, 1978, стр. 38100.

27. Нигиян С.А. Функциональные языки программирования. //Программирование, № 5,1991, стр. 77-86 (англ. пер. Nigiyan S.A. Functional languages, Programming and Computer Software, Vol. 17., N 5,1992, p. 290-297).

28. Нигиян С.А. Функциональная концепция языков программирования. //ДНАН Армении, том 94, № 3, 1993, стр. 131-137.

29. Нигиян С.А., Будагян Л.Э. Правила вычисления главной функции наименьшего решения для одного класса систем рекурсивных уравнений.//ДНАН Армении, том 99, № 3,1999, стр. 197-203.

30. Хювенен Э., Сепянен Й. Мир Лиспа. Том 1, 447 е., Том 2,319 с. // М.: Мир, 1990.