автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Об интерпретации строго типизированных функциональных программ

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ им. М. В. ЛОМОНОСОВА Факультет вычислительной математики и кибернетики

ОБ ИНТЕРПРЕТАЦИИ СТРОГО ТИПИЗИРОВАННЫХ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ

Специальность 05.13.11 -математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

БУДАГЯН Лусине Эдгаровна

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

МОСКВА • 2006

Работа выполнена на кафедре системного программирования Ереванского государственного университета

Научный руководитель: доктор физико-математических наук,

профессор Нигиян Семён Александрович

Официальные оппоненты: доктор физико-математических наук,

профессор Любимский Эдуард Зиновьевич

кандидат физико-математических наук, доцент Захаров Владимир Анатольевич

Ведущая организация: Вычислительный центр имени А. А. Дородницына

Российской академии наук

Защита диссертации состоится « 13 » октября 2006 года в 11°° часов на заседании диссертационного совета Д 501.001.44 в Московском государственном университете им М.В. Ломоносова по адресу: 119992, ГСП-2, Москва, Ленинские горы, МГУ им. М. В. Ломоносова, 2-ой учебный корпус, факультет ВМиК, ауд. 685.

С диссертацией можно ознакомиться в библиотеке факультета ВМиК МГУ.

Автореферат разослан «// » еемтлК?Л 2006 года

Ученый секретарь

диссертационного совета профессор Трифонов Н. П.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Диссертационная работа посвящена проблемам функционального программирования. Объектом исследований является понятие функциональной программы, называемой строго типизированной и использующей аппарат типового Л-исчисления, а основной рассматриваемой проблемой - фундаментальная задача вычисления реализуемой программой функции. В отличие от процедурных языков, где программа описывает процесс вычисления программируемой функции, функциональная программа определяет саму функцию, используя выражения. Эти выражения строятся из переменных и базовых функций с помощью операций аппликации и ^.-абстракции. Вычисление определяемой программой функции для конкретных входных данных производит интерпретатор данного языка. Интерпретирующий алгоритм должен быть непротиворечивым в том смысле, что если он останавливается, то вычисленное им значение должно совпадать со значением, определяемой функции. В случае, когда интерпретирующий алгоритм для. всяких входных данных вычисляет значение функции, реализуемой программой, он называется полным. Для исследования этих свойств интерпретаторов необходимы: формализация понятия программы, реализуемой данной программой функции (ее семантики) и процесса вычисления этой функции.

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

' Манда З.ТеормтгсдоижхгойточтпртгрйМмУ/Клберн ] 5,1978, С1р. 38-100.

могут содержать несколько вхождений функциональных переменных. Тогда возникает задача выбора подмножества заменяемых вхождений. Для этого использовалось понятие правила вычисления функции, определяемой программой. В случае, когда правило вычисляло эту функцию, оно было названо правилом неподвижной точки (мы такое правило будем называть полным). Далее рассматривались шесть правил вычисления и исследовались на вопрос полноты.

В работах1,2 рассматривались строго типизированные функциональные программы общего вида. Такие программы представляют собой системы уравнений в монотонных моделях типового А-исчисления, которые используют переменные и константы любых порядков, причем константы порядка 1 являются вычислимыми функциями, а константы, порядок которых >2, - эффективно представимыми. Для таких программ была доказана теорема о существовании наименьшего решения, главная компонента которого, функция /р, является семантикой программы Р. Было показано, что для каждой программы Р можно построить программу Р' такую, что Р'не использует констант, порядок которых >1 vifp = fp-. Таким образом актуальной является задача исследования вопросов аналогичных рассмотренным в работе 3. Манны3 для строго типизированных функциональных программ общего вида, использующих переменные любых порядков и константы, порядок которых <1. В рассматриваемом нами общем случае используются два вида правил упрощения выражений, называемые нами р и 5-редукциями термов. Заметим, что в работе3 рассматривались только упрощения по 8-правилам. Упрощение по ß-правилам соответствует применению выражения, являющегося описанием некоторого отображения, к выражениям-аргументам, ß-редукция термов является классическим понятием в ^.-исчислении. Основные результаты относящиеся к ß-редукции нами взяты из работ*'5. Понятие 5-редукции хотя и использовалось при реализациях языков программирования, но не было формализовано.

Цель диссертационной работы. Целью диссертационной работы является:

• Формализация понятия 6-редукции в монотонных моделях типового Я-исчисления, исследование этой формализации.

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

• Определение правил вычисления, аналогичных рассмотренным в работе6, и исследование этих правил на вопрос полноты.

* Кнгеян С А Функциональные языки 1фОтраммнрованкя.//Программироаание, Ks 5,1991, стр. 77-86.

а Нигиян сл. Об интерпретации функциональных гаыков программированияУЛ1рограммлровшие.Хв 2.] 993. стр. 58-68

3 Манна 'А Теория неподвижной точки программ. //Кибернегаческий сборник (новая серия); вып. 15,1978i cip. 38-100.

4 HindUy J. R-, Scldin J. P. Essays on Combinaiay Logic, Lambda£a] cuius and Fomudian. //Academic Press NY and Lcndüo, 1980.

1 Bartndregt HP. Lambda calculi with types. // Handbook of Logic in Computer Science, Volume 2, Edited by S. Abrarmky. D M Gabbay andTS.E Ма1Ъшщ,0^о^Шу««у111И4 1992.pi 117-309

* Макна 3. Теория неподвижной точки программ //Кибернетический сборник (новая с^мхХ вып. 15,1978, сгр. 38-100.

Научная новизна.

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

• Впервые формализовано понятие ¿-редукции в монотонных моделях типового Д-исчисления. Доказаны теоремы утверждающие конечность процесса упрощения терма как при использовании только ¿-редукции, так и при смешанном использовании /? и ¿-редукции (называемом /^¿-редукцией терма).

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

2. Получены результаты, относящиеся к вычислению функции, определяемой строго типизированной функциональной программой:

• Введены понятия правила вычисления (основанного на подстановке правых частей уравнений программы вместо некоторых свободных вхождений переменных терма) и последовательности вычисления (для конкретных входных данных). Введено понятие полноты правила вычисления для фиксированного реального понятия ¿-редукции. Найдено необходимое и достаточное условие полноты правила вычисления при фиксированном реальном понятии ¿-редукции. Введено понятие полноты правила вычисления. Доказано, что всякое правило вычисления является полным тогда и только тогда, когда оно полно для некоторого реального понятия ¿-редукции.

• Определены и рассмотрены шесть правил вычисления: самой левой внутренней замены, параллельной внутренней замены, самой левой (внешней) замены, параллельной внешней замены, замены вхождений свободных для подстановки, полной замены. Получены исчерпывающие результаты относительно их полноты.

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

Методика исследований. Методика исследований включает в себя методы алгебры, теории алгоритмов и типового /¡.-исчисления.

Апробация работы и публикации. Основные результаты диссертации докладывались на научных конференциях и семинарах, в частности на научной конференции Армянского математического общества (декабрь 1996), на международных конференциях CSIT-99, CSIT-03 и CSIT-05 (Conference of Computer Science and Information Technologies, Yerevan 1999, 2003, 2005) на семинаре кафедры системного программирования ЕГУ, на объединенном научно-исследовательском семинаре кафедр автоматизации систем вычислительных комплексов, алгоритмических языков и системного программирования МГУ. Основные результаты диссертации отражены в 6-ти публикациях.

Структура и объем работы. Диссертация состоит из введения, трех глав, заключения и списка используемой литературы (33 наименований). Объем диссертации 107 страниц.

СОДЕРЖАНИЕ РАБОТЫ

Во введении описывается задача диссертационного исследования и дается краткий обзор содержания работы.

В ГЛАВЕ 1 приводятся используемые определения и результаты, и доказывается Теорема 1.2.1 (о замене). Глава 1 состоит из разделов 1.1 и 1.2.

В разделе 1.1 даются определения монотонного типа, терма (в монотонной модели типового ?.-исчисления), значения терма, эквивалентности термов, понятия Я-редукции, Л-нормальной формы, сильной /{-нормализуемое™. Приводится понятие /2-редукции. Определяется монотонная система уравнений, вводится понятие программы и ее семантики. Формулируются некоторые результаты относительно этих понятий, которые используются в последующих разделах.

Частично упорядоченное множество называется полным, если всякое его линейно упорядоченное подмножество имеет точную верхнюю грань (sup). Всякое полное множество содержит наименьший элемент — sup 0. Пусть А и В — частично упорядоченные множества,/и g — некоторые отображения из А в В. Тогда/ с g, если для любого а е A, f(a) с g(a) (с - символ частичного порядка); /- монотонное отображение, если для любых а, Ь е А таких, что а С Ь, имеем: f(a) С f(b).

Пусть D - частично упорядоченное множество, содержащее наименьший элемент ± и каждый элемент из D сравним только с X и с самим собой.

Определим множество МТ монотонных типов:

1) D е МГ,

2) если fiai.....а* е МТ (к > 0), то множество всех монотонных

отображений из aix...xak в ß(обозначим [aix...xctk—*ß]) принадлежит МТ;

3) других монотонных типов, кроме определенных согласно 1-2, нет.

Пусть а е МТ. Тогда порядком типа а (обозначим ord(a)) будет натуральное число, определяемое следующим образом: если а = D, то ord(a)=0; если а = [ajx...xak—*ß], где ßa,,...,ak е МТ (к > 0), то ord(a) = max(ord(ai),.. .,ord(at),ord(ß) + 1.

Будем считать, что для каждого а е МТ мы имеем счетное множество переменных типа а (обозначим Va). Если переменная х е Уа и константа се а, то ord(x) = ord(c) - ord(a). Константы и переменные монотонных типов условимся называть монотонными.

Пусть V = (J Va- Определим множество монотонных термов (далее

а*ЛП

просто термов) Л = (J Ла.

аеМТ

1. Если с е а, а е МТ, то се Л&

2. Если* eVa а е МТ, тох е Ла.

3. Если t е U е Ла, Д а, е МТ, / = /.....к (к > 0), то

t(tj,:..,tk)eAp(ti,...,tkназовем областью действия аппликатора г).

4. Если t е Aß, xt е Аа , ß а) е МТ, i => Xf* хр i, j = I,...,к (k>0), то

Ax/..~xk[t] e -л (' назовем областью действия абстрактора Ax,...xt).

5. Никаких других термов, кроме определенных согласно 1-4, нет. Традиционным образом вводятся понятия свободного и связанного

вхождения переменной в терм, понятие свободной переменной терма. Множество всех свободных переменных терма t обозначим FV(t).

Пусть t е Л, t, е Ла, yt е V^, а, е МТ, i # j => у, ф ур ij = 1, ...,к (к>0). Тогда одновременную подстановку термов tl,...,tk в терм t вместо всех свободных вхождений переменных yj,...,yt соответственно назовем допустимой, если ни одно из рассматриваемых свободных вхождений переменной у, не находится в области действия абстрактора, использующего

некоторую свободную переменную терма //, i = 1.....к. Терм, полученный в

результате такой подстановки, условимся обозначать ф/у,,.. .,li/yij.

Заменой связанной переменной в терме t называется замена подтерма Äxi...xj...xk[r], где Xj е Va , щ е МТ, 1 < j < к (к>0), на терм

Ах/...Xj...хк[т{х'/xj}], где x'j£Va, Xj-ft {xt,...,x/j, x'j не свободна в терме г.

Термы ti и г2 назовем конгруэнтными (обозначим это t; з t2), если терм t2 получается из терма tl серией замен связанных переменных. Далее условимся отождествлять конгруэнтные термы и также считать, что все рассматриваемые далее подстановки являются допустимыми.

Бинарное отношение R с Л2 есть понятие Ä-редукции на Л. Будем говорить, что терм ¿'получен посредством одношаговой Ä-редукции из терма

t (обозначим это t-^ t% если существуют термы г/ и г2 такие, что / есть

терм tri, t' есть терм ftj и < zh т2> е R, где через tu обозначен терм t с

некоторым фиксированным вхождением подтерма Ту,- а через tT — терм, полученный в результате замены данного вхождения подтерма г> на терм т2.

Будем говорить, что терм /'получен посредством R-редукции из терма t (или терм t Л-редуцируется к терму t'a обозначим это / —t), если либо терм t конгруэнтен терму /', либо существует такая последовательность

одношаговых Л-редукций, что t-^ ti-¡к ...-fc tk-sr /', где f( е Л, i -

1,,..,к (к£0). Эта последовательность одношаговых Л-редукций называется Л-редукционной цепочкой для терма t. Число одношаговых Л-редукций в R-редукционной цепочке называется ее длиной. Напомним, что если <rJ}r2> е R, то Г; называется Д-редексом, г2 - Л-сверткой и если терм t не имеет таких подтермов, которые являются Л-редексами, то он является Л-нормальной формой. Множество Л-нормальных форм обозначим R-NF. Терм t называется /{-нормализуемым, если существует терм t' е R-NF такой, что t —/' Терм t называется сильно Я-нормализуемым, если любая Я-редукционная цепочка для терма t имеет конечную длину.

Будем говорить, что понятие Л-редукции обладает слабым свойством Черча-Россера, если для любого терма t из того, что / —t' я t —& t" следует, что существует терм t "'такой, что t '—/ '"и t "—/ "'.

Напомним понятие /?-редукции. Р= {<tei..jxjT](th...,tk),T{t/xh...,tK/xk}> \х,е¥щ. t,eА,- ъеМТ, ...,к(к>1)}

Напомним теорему о сильной /9-нормализуемости утверждающую, что для любого терма любая /f-реду купонная цепочка конечна, и лемму утверждающую, что понятие ^-редукции обладает слабым свойством Черча-Россера. Их следствием является теорема о единственности /Анормальной формы, которая утверждает, что для любого терма t имеет место следующее: / —t —t "и /', /" е fi-NF=>/'s t".

Каждому терму t £ Л сопоставим константу Valyjt), где FV(t) сг

{у1.~;у»},у,еУа >у0 = <у",...,у">, у° eaj,ateMT,i = l,...,n(n>0).

1. Если t = с, с е а, а е МТ, то Val% (t) =с.

2. Если l = x,x е V,to Val^ (t) = у], где х = yh lâ<n, rt>0.

3. Если / s t(t,.....t0 e Л/h t, e fi a, e MT, .....к

(k>0), то ValP) (iflj.....tj) = Val?i (x)(Valy> (t,).....Val% (t0).

4. Если (s Àx,..jfk[r] e ^»...««.-.л» теЛ/ьх, eVa,fi a, e MT, i = I.....к

(k>0), то ValyJXx,...xt[l]) : aix...xak->f} и для всяких x0 = <x° ,...,x°>, Xj° eqj = 1.....к имеем: Val-y/te,...xk[t])(x0) = Val^.fl), где FV(Àx,...xJt])

~{yt,.....yJ.K-^l.....yl>(0<to<h).

Рассмотрим систему уравнений Р:

ГF, г,

\ (1) [-^я = ?„

где F, е Va , i => F, tFp т, e Aa , FV(tJ <= {F,.....F„}, a, e МГ, ij = 1.....n,

n>l.

Отображение 4'p;atx...xan-+a.ix...xa„ такое, что Vpfg) = <Valt(zi), .... Vali(r,J>, где g e aix...xa,n назовем отображением, соответствующим системе уравнений (1). Через (g)i (1 <i < и) условимся обозначать i-тую компоненту вектора g. Будем говорить, что / е atx...xa„ является решением системы (1), если Yp(f) = /. Системы уравнений вида (1), назовем монотонными системами уравнений.

Пусть А - полное множество и Ол - множество всех ординалов соответствующих мощностям, которые не превышают мощность множества А. Пусть f: А А — монотонное отображение. Определим отображение Г/Оа—>Л следующим образом: T/0J = ±, где ± наименьший элемент множества А; если для некоторого ц е ОА, то Y/E) =

f(Y/ri))\ если % е Ол, 0 и не существует такого t] е Ол, что £=»;+/, тогда r/Q=sup{r/k)\k<Q.

В работе1 была доказана теорема о наименьшем решении системы уравнений: каждая монотонная система уравнений (1) имеет наименьшее решение / =sup{Y ч> (к) \ к<Од}, где Ч'р — отображение соответствующее системе (1), А = aix...xa„.

Монотонная константа <р, порядок которой £ 2, называется эффективно представимой, если существует система уравнений вида (1) такая, что все используемые в системе константы порядка 1 являются вычислимыми функциями и не используются константы, порядок которых > 1, и если / — наименьшее решение системы (1), то <р - (/)).

Монотонная система уравнений вида (1) называется программой, если все используемые ею константы порядка 1 являются вычислимыми функциями, константы порядка ¿2 — эффективно представимы и а/ = > 1. Уравнение F]~Ti называется главным уравнением программы Р, а функция fp=(f)h где / - наименьшее решение программы Р, -семантикой программы Р. Из работы2 следует, что для любой программы Р, ее наименьшего решения </}, ...,/„> и i е {1, ..., п} имеем:

а) если ord(f) <2, то sup {CPр' (П)), \ j < со} =/„• . б) если ordtfd > 2, юsup {(¥{(П)),\)<'а$ с/,, •

' Нигиян С. А. Функциональные языки программирования. //Программирование, № 5,1991, стр. 77-86.

2 Нигиян С-А. Об интерпретации функциональных языков программирования. Шрограляиирование, № 2,1993, стр. 58-68.

где ГР°(Л) = П, Уу41 (О) = У, (О)),] П - наименьший элемент множества а1х...ха„, — отображение соответствующее программе Р, со — ординал, соответствующий натуральному ряду. В работе1 показано, что для всякой программы Р можно построить программу Р' такую, что Р' не использует констант, порядок которых >1 и /р=/р-. Отсюда следует, что для любой программы Р, где а, = к > 0, и а? имеем: ^(Л) =

зир{СР{.(П)),(3) < со}.

Раздел 1.2 посвящен доказательству Теоремы 1.2.1 (о замене).

Пусть термы и РУ(1,) и = {у,, ..., у,,}, у, е а, е МТ, /

=1.....п, п ¿0. Термы и 12 назовем эквивалентными (обозначим ~ Г2), если

для любого у0 = <у°,..., ,у®>, где у° е я„ I = 1,...,п, имеем: =

Уа!^. ' ;

Теорема 1.2.1 (о замене). Пусть г>, т2 — термы, - терм с некоторым фиксированным вхождением подтерма Т;, тогда: Т/ ~ г2=> ~ .

ГЛАВА 2 посвящена формализации понятия ^редукции и связанными с этим понятием результатами. В ней рассматриваются термы, которые используют переменные любого порядка и константы, порядок которых <7. Глава 2 состоит из разделов 2.1 - 2.4.

В разделе 2.1 формализуется понятие «^редукции и доказывается, Теорема 2.1.1 (о редукции) утверждающая, что любая ДО-редукция терма приводит к эквивалентному терму.

Пусть I в Аа а е МТ, РУ(1) с {у,,.. „у,,}, у, е Уа, а, е МТ, г = 1.....п, п >

0. Терм I назовем константным термом со значением с е а, если для любого У0~<у0/1--,у'„>, у", еа,, /=/,...,« имеем: Ка/Л (I) = с. Введем понятие ¿►-редукции: Пусть

А — {</(¡¡,...,¡1), г> \/— константа, т, //, ..., гк (к>0) — термы и либо т— константа и/(//, ...,/*) является константным термом со значением г, либо г— собственный подтерм термаУ(7/.....к/(11,...,1ь)~т}

Любое подмножество 8 множества А назовем понятием ¿-редукции.

Мы будем исследовать понятие редукции 3, которую обозначим ¡36. Условимся /?<5-редукцию называть просто редукцией, /Анормальную форму — просто нормальной формой, рд-ЫР обозначать просто одношаговую /?<5-редукцию обозначать-/?<5-редукцию-->->.

Теорема 2.1.1 (о редукции). Пусть /, t' <= Л, тогда: г —I

В разделе 2.2 доказываются две теоремы: Теорема 2.2.1 (о сильной 6-нормализуемости) утверждающая, что любая 5-редукционная цепочка для терма имеет конечную длину, и Теорема 2.2.2 (о сильной

1 Ннгижн С. А. Об инт^ифегати функциональных языков программирования. //Программирование, Ка 2,1993, стр. 5&68.

и

/?5нормализуемости) утверждающая, что любая /^редукционная цепочка для терма имеет конечную длину.

Теорема 2.2.1 (о сильной 5-нормализуемости). Любой терм сильно 5нормализуем.

Теорема 2.2.2 (о сильной рб-нормализуемости). Любой терм сильно /?5-нормализуем.

В разделе 2.3 вводится, так называемое, естественное понятие 6-редукции, которое определяется наложением некоторых естественных ограничений на понятие 5редукции, введенное в разделе 2.1. Дается определение эффективного понятия <5-редукции.

Обозначим Д> следующее подмножество множества А\ Л0 = {</(<1,г>1</Г';.....е Ли г либо константа, либо гз (1<1^к)}.

Понятие 5-редукции назовем естественным, если:

\)6сгАо,

2) 5-однозначное отношение, т.е. если </, Г/> е 3 и </, т2> е 3, то т>= т2, где Г;, т2 е Л (это свойство понятия 6-редукции мы будем называть однозначностью);

3) для любого константного терма /(/у,...,/*) со значением с1 е Д где/константа, ..., е Л. имеем: /(0,...,^ —с/ (это свойство понятия 5-редукции мы будем называть разумностью).

Приводятся четыре примера понятий «5-редукции. В трех из них понятия 5-редукции не являются естественными: в первом примере - 5 <г Д>, во втором -5не является однозначным отношением, в третьем —5не разумно. В четвертом примере приводится пример естественного понятия ¿-редукции.

Пусть 8 некоторое естественное понятие (5-редукции и Ф5: А Ло и {нет} - отображение такое, что:

. . . _ Г г, если/-5-редекс и г-его свертка

нет, если / не является 5редексом

Будем говорить, что естественное понятие 5-редукции является эффективным, если отображение Фа вычислимо.

В разделе 2.4 описываются два свойства понятия 5-редукции: подстановочность и наследуемость. Доказывается Теорема 2.4.1 (о единственности нормальной формы) утверждающая, что для любого естественного понятия 5-редукции терм Г редуцируется к единственной нормальной форме тогда и только тогда, когда понятие 5-редукции обладает свойством подстановочности и наследуемости.

Будем говорить, что понятие 5редукции обладает свойством подстановочности, если из того, что </((,,..., с*), Ц> е 5, где/- константа,

.......е А к <> 1, ] £ к, и /0/.....не является константным термом,

следует, что для любой подстановки {т/х^ ..., т„/хт), где т, е Ла , х, е Уа ,

а,еМТ, =>>7* х}, у = 1,...,т, т> 0, существуют термы /у,...,/* такие, что

{х,/хи....тЛхт}-I',. ..., ¡к{т,/х,,.... тУхт}-г'* и </(?...,/у,/;> в <5

Будем говорить, что понятие 5-редукции обладает свойством наследуемости, если из того, что </((/,...,?*), /,> е где / - константа, ^ еД кк1>1<]< к, к /(11,..., ¡ь) не является константным термом, г, = г, для некоторого /' (/ <£), где г — редекс следует, что существует термы /у, ..., /'¿такие, что—..., > > /', .... /*—/1 и </С/',,.е 5, где гсвертка редекса г.

Если понятие 5редукции обладает свойством подстановочности и наследуемости, то будем говорить, что оно обладает ПН-свойством.

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

Теорема 2.4.1 (о единственности нормальной формы). Пусть 8 некоторое естественное понятие 5-редукции. Тогда для любого терма г имеет место следующее:

/ —/ —/"и /', /"- нормальные формы => /'= /", в том и только в том случае, если понятие 5-редукции обладает ПН-свойством. -

Доказательство Теоремы 2.4.1 использует следующую Лемму 2.4.1. Лемма 2.4.1. Пусть 6 - некоторое естественное понятие 5-редукции, которое обладает ПН-свойством. Тогда /35редукция обладает слабым свойством Черча-Россера.

Приводится пример естественного понятия 5-редукции обладающего ПН-свойством. ...

В ГЛАВЕ 3 введено, так называемое, реальное понятие 5редукции, которое обычно встречается на практике. Дано определение правила вычисления, полноты правила вычисления при фиксированном реальном понятии 5редукции, найдено необходимое и достаточное условие полноты правила вычисления при фиксированном реальном понятии 5-редукции. Дано определение полноты правила вычисления и найдено необходимое и достаточное условие полноты правила вычисления. Приведены конкретные примеры правил вычисления и получены результаты относительно их полноты. Глава 3 состоит из разделов 3.1 - 3.6.

Раздел 3.1 посвящен определению реального понятия 5-редукции.

Введем понятие частичной подстановки. Пусть t е Л, РУр) с {у!.....у,,},

х<еУа1, а, е МТ, I * ] => у/ * у? ) = 1,...,п (п>0). Зафиксируем в терме / некоторые подмножество свободных вхождений переменных у/,...,у„.

Обозначим этот терм 1[РО], где РО - множество фиксированных вхождений переменных. Пусть т, е Ла , 1 = 1.....п. Одновременную подстановку термов

Т1,.,.,Т„ вместо фиксированных свободных вхождений переменных у!,...,у„, соответственно, назовем частичной подстановкой. Терм, полученный в результате частичной подстановки, обозначим 1[РО]{т1/у/1..., т,/у„).

Пусть 5 е Л0. Будем говорить, что понятие ¿¡-редукции замкнуто относительно частичной подстановки, если из того, что </(о, .... в <5,

где/-константа, Г/,..., 1ке Л, 1 <> РУ^р,.....Г*)) с {у,,...,у„}, у,еУа ,

а,еМТ, I = 1,..., п, п £ 0, и/((/,..„¡¡) не является константным термом, следует, что для любого подмножества РО' свободных вхождений переменных в терме ^ существует подмножество РО свободных вхождений

переменных в терме такое, что </(!,,..., 1^)[РО]{т/у!.....т,/у,},

1][РО']{т/у,.....т,/у„)> е 6для любых и.....г,„ где т, е Ла<1 а, еМТ,г = 1,...,п.

Приводится два примера естественного понятия редукции. В первом случае определенное нами понятие ¿-редукции обладает ПН-свойством, но не является замкнутым относительно частичной подстановки, во втором случае - замкнуто относительно частичной подстановки, но не обладает свойством подстановочности.

Естественное, эффективное понятие <5-редукции назовем реальным, если оно обладает ПН-свойством и замкнуто относительно частичной подстановки.

Далее используя выражение «понятие ¿-редукции» мы будем понимать реальное понятие ¿-редукции.

В разделе 3.2 вводится понятие правила вычисления р, основанного на подстановке правых частей уравнений программы вместо некоторых свободных вхождений переменных терма. Приводятся примеры шести правил вычисления. Дается определение последовательности вычисления для программы Р, некоторого понятия ¿-редукции, правила вычисления р и начального значения переменных. Определяется функция, //•'' соответствующая программе Р, понятию ¿-редукции и правилу вычисления р. Доказывается Теорема 3.2.1 утверждающая, что для любой программы Р, правила вычисления р и понятия ¿-редукции функция /р является продолжением функции

Введем понятие правила вычисления р. Пусть программа Р имеет вид (1) и 1еЛ такой, что РУ(0 с {р1,...,р„}. Перенумеруем все свободные вхождения переменных р1,...,р„ в терме t слева на право. Правило вычисления р по каждому терму / определяет некоторое непустое подмножество номеров свободных вхождений переменных Р,,.. ,,Р„ терма которые следует

одновременно заменить термами г/.....гп соответственно. Назовем это

подмножество множеством вхождений переменных р1,...,р„ терма /

определяемых правилом вычисления р.' Естественно, что подстановка предполагается допустимой. Результат такой замены обозначим р(1).

Перед тем как определить конкретные правила вычисления введем несколько понятий.

Свободное вхождение переменной Р в терм г назовем внутренним, если оно не входит в аппликатор г, область действия которого содержит свободное вхождение (в терм /) некоторой переменной.

Свободное вхождение переменной ^ в терм ? назовем внешним, если оно не входит в область действия аппликатора, содержащего свободное вхождение (в терм г) некоторой переменной.

Свободное вхождение переменной ^ в терм ( назовем свободным для подстановки, если либо оно не является аппликатором, либо имеет, по меньшей мере, один аргумент, который не содержит свободное вхождение (в терм 0 некоторой переменной.

Определим шесть правил вычисления. . 1) Правило самой левой внутренней замены: заменяется самое левое внутреннее свободное вхождение переменной;

2) Правило параллельной внутренней замены: заменяются одновременно все внутренние свободные вхождения переменных;

3) Правило самой левой (внешней) замены заменяется самое левое (внешнее) свободное вхождение переменной;

4) Правило параллельной внешней замены: заменяются одновременно все внешние свободные вхождения переменных;

5) Правило замены вхождений свободных для подстановки: заменяются одновременно все свободные вхождения переменных, свободные для подстановки;

6) Правило полной замены: заменяются одновременно все свободные вхождения переменных.

Правила 1, 2, 3, 4 и 6 являются обобщениями аналогичных правил вычисления определенных в работе1. Правилу 5 в той же работе соответствует правило свободного аргумента.

Пусть 5 - некоторое понятие 5-редукции, Р - программа вида (1), где е У(0, , к>1, р - правило вычисления и с/ е Е?. Рассмотрим

последовательность термов ... определяемую следующим образом:

• ¡о есть терм

• е ИК и р(г) —, ¡>1. Определенную таким образом последовательность термов 10, I,, ... назовем последовательностью вычисления для <1 соответствующую 8, р и Р.

Корректность данного определения следует из Теоремы 2.4.1 (о единственности нормальной формы).

1 МапнаЗ. Теория неподвижной точгалдорамм//Кибернетический сборник (новая серияХ выл. 15,1978, стр. 38-100.

Определим функцию f£'p, соответствующую некоторому понятию ¿-редукции, правилу вычисления р и программе Р вида (1), где F,eVlD, k¿¡.

Пусть d е Г? и t0, t¡, ... - последовательность вычисления для d: J>p Г tti, если для некоторого i0 ¿I t,t eD

r l__¿, если для всех i ¿11, eD

Заметим, что не всегда //'р = fP и что функции //•" могут быть различными при различных 8 (приводится соответствующий пример понятия ¿-редукции, правила вычисления р и программы Р).

Теорема 3.2.1. (о функции, соответствующей правилу вычисления). Для всякого понятия ¿-редукции, правила вычисления р и программы Р имеем://'е^.

В разделе 3.3 дается определение полноты правила вычисления р для фиксированного понятия ¿-редукции. Доказывается Теорема 3.3.1 утверждающая, что так называемая существенность подстановки на каждом шаге построения последовательности вычисления является необходимым и достаточным условием полноты правила вычисления р при фиксированном понятии ¿-редукции.

Пусть р - правило вычисления. Правило р назовем полным для некоторого фиксированного понятия редукции, если для всякой программы р /;•' =//>.

Пусть программа Р имеет вид (1), где F, е V[D,^D]¡ к ¿ 1, F, е Va , a¡ е МТ, i=],...,n, п>0, /-наименьшее решение программы Р, р — некоторое правило вычисления и d eD*. Пусть также l0, t¡, ... - последовательность вычисления для d. Будем говорить, что на некотором шаге » ¿ 0 построения последовательности вычисления для d правило р для неконстантного терма t¡[p] определяет существенную подстановку, если Valf (t¡) * J. и Val} (ti[p]{£2¡/F),..., Í2,/F,J) = _Z, где t,[p] - терм í„ в котором зафиксировано множество свободных вхождений, определяемое правилом вычисления р, Í2¡

- наименьший элемент множества a¡,i=l.....п. В противном случае будем

говорить, что правило р для терма t¡[p] определяет несущественную подстановку.

Теорема 3.3.1. Правило вычисления р для фиксированного понятия & редукции является полным правилом вычисления в том и только в том случае, если для всяких программы Р вида (1), где F, е K[D>_(0], k¿!, и de

Lf имеем следующее: если fp(d) = d0 * J., где fr - семантика программы Р, то на каждом шаге построения последовательности вычисления для d правило р определяет существенную подстановку.

В разделе 3.4 дается определение полноты правила вычисления р, как совпадение функций fp и для любых Р и д. Доказывается Теорема 3.4.1.

Теорема 3.4.1. Правило вычисления р является полным правилом вычисления в том и только в том случае, если оно является полным для некоторого фиксированного понятия «5-редукции.

Раздел 3.5 посвящен установлению полноты следующих правил вычисления: полной замены (Теорема 3.5.1), параллельной внешней замены (Теорема 3.5.2), самой левой замены для программ, использующих естественно расширенные функции и функцию 1/_Леп_еЬе (Теорема 3.5.3).

Теорема 3.5.1. Правило полной замены является полным правилом вычисления.

Теорема 3.5.2. Правило параллельной внешней замены является полным правилом вычисления.

Будем говорить, что функция / е [йк—Ю] 1) естественно расширена, если/(...Д,...} = ±.

Теорема 3.5.3. Для программ, в которых используемые константы порядка 1 являются естественно расширенными функциями (кроме ¡/_Леп_еЬе), правило самой левой замены является полным правилом вычисления.

В разделе 3.6 доказывается Теорема 3.6.1 устанавливающая неполноту следующих правил: самой левой внутренней замены, параллельной внутренней замены, самой левой замены, замены вхождений свободных для подстановки.

Теорема 3.6.1. Правила 1, 2, 3 и 5 не являются полными правилами вычисления.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

1. Формализовано понятие 5-редукции в монотонных моделях типового Х-исчисления, использующих константы порядка <7. Доказана теорема утверждающая, что любая /^редукция терма приводит к терму эквивалентному данному. Получены результаты о сильной & нормализуемое™ и о сильной уЗ£нормализуемости терма.

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

3. Дано определение реального понятия 5-редукции, которое является эффективным, естественным понятием «5-редукции, обладающим ПН-

свойством и замкнутым относительно частичной подстановки. Это именно то понятие ô-редукции, которое встречается на практике.

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

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

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

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

2. Nigiyan S.A., Budaghyan L.E. On execution of functional programs. // Proceedings of the Conference of Computer Science and Information Technologies (CSIT-99). Publishing House of NAS of RA, Yerevan, 1999, p. 33-35.

3. Budaghyan L.E. Formalizing the notion of 6-reduction in monotonic models of typed X,-calculus. //Algebra, Geometry & Their Applications, Vol. 1, YSU Press, Yerevan, 2002, p. 48-57.

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

5. Budaghyan L. Е, On 6-reduction in monotonic models of typed Л-calculus. // Proceedings of the Conference of Computer Science and Information Technologies (CSIT-2003), Publishing House of NAS of RA, Yerevan, 2003, p.65-67.

6. Budaghyan L. E. A Necessary and sufficient condition of completeness of computation rule for strong typed functional programs. // Proceedings of the Conference of Computer Science and Information Technologies (CSIT-2005), Publishing House of NAS of RA, Yerevan, 2005, p. 16-19.

Тираж 100.

Подразделение оперативной полиграфии ЕГУ Ереван, Ал. Манукяна 1

СОДЕРЖАНИЕ.

ВВЕДЕНИЕ.

ГЛАВА 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

ЗАКЛЮЧЕНИЕ

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.