WWW.PROGRAMMA.X-PDF.RU
БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА - Учебные и рабочие программы
 


«УНИВЕРСИТЕТ Грачян Гурген Гагикович ОБ ОСНОВНОЙ СЕМАНТИКЕ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ ...»

.01.09 «

»

-2009

ЕРЕВАНСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

Грачян Гурген Гагикович

ОБ ОСНОВНОЙ СЕМАНТИКЕ

ФУНКЦИОНАЛЬНЫХ ПРОГРАММ

АВТОРЕФЕРАТ

диссертации на соискание ученой степени

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

по специальности 01.01.09 “Математическая кибернетика и



математическая логика” Ереван-2009 `.....

`.....

.....

` 2009. 5- 1400- - Тема диссертации утверждена в Ереванском государственном университете Научный руководитель: доктор физ.-мат. наук С.А. Нигиян Официальные оппоненты: доктор физ.-мат. наук Г.Б. Маранджян кандидат физ.-мат. наук С.А. Аветисян Ведущая организация: Институт проблем информатики и автоматизации НАН РА Защита диссертации состоится 5-го июня 2009 г. в 1400 часов на заседании специализированного совета ВАК 044 “Математическая кибернетика и математическая логика” при ЕГУ по адресу: 0025 г. Ереван, ул. Алека Манукяна, 1.

С диссертацией можно ознакомится в бибилиотеке Ереванского государственного университета.

Автореферат разослан 4-го мая 2009 г.

Ученый секретарь специализированного совета, кандидат физ.-мат. наук В.Ж. Думанян

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

Актуальность темы. В диссертационной работе рассматриваются бестиповые и строго типизированные функциональные программы. Бестиповые функциональные программы представляют собой системы уравнений с отделяющимися переменными в бестиповом -исчислении. Основная (детонационная) семантика таких программ определяется как терм в бестиповом -исчислении, использующий некоторый комбинатор неподвижной точки. Обычно используется комбинатор неподвижной точки Y (парадоксальный комбинатор Карри). Существует множество технологий интерпретации бестиповых функциональных языков программирования. Например, Eval/Apply-интерпретатор, SECD машина, метод, основанный на редукции графов, метод CPS преобразований. Исследование соотношения процедурных семантик используемых методов и основной семантики является одной из актуальных и важных проблем теории функционального программирования. Перечисленные методы, а также многие другие, эквивалентны, так называемым, алгоритмам интерпретации. В работе1 процедурные семантики алгоритмов интерпретации сравниваются с основной семантикой, определяемой с помощью комбинатора неподвижной точки Y. Возникает естественный вопрос:

верны ли эти результаты для произвольного комбинатора неподвижной точки?

Таким образом, важным является рассматриваемый в диссертационной работе вопрос об инвариантности основной семантики относительно комбинатора неподвижной точки, а также вопрос о том, как ведут себя основные семантики, определяемые разными комбинаторами неподвижной точки, при конкретных редукционных стратегиях.

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

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

• Исследовать вопрос об инвариантности основной семантики бестиповой функциональной программы относительно комбинатора неподвижной точки.

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

• Дать оценки ординалов, при которых достигаются компоненты порядков 3 наименьшего решения строго типизированной функциональной программы.

–  –  –

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

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

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





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

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

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

Теоретическая и практическая ценность. Результаты, полученные в диссертационной работе, носят как теоретический, так и практический характер.

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

Апробация работы и публикации. Основные результаты диссертации докладывались на семинаре кафедры программирования и информационных технологий ЕГУ, на общем семинаре факультета информатики и прикладной математики ЕГУ, на международных конференциях CSIT-05, Ереван, 2005 и CSITЕреван, 2007.

Основные результаты работы отражены в 5-ти публикациях.

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

– 93 страницы.

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

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

Глава 1 посвящена доказательству теоремы об инвариантности основной семантики бестиповых функциональных программ.

В разделе 1.1 приводятся определения и результаты, используемые в главах 1 и

2. Определяются понятие терма, -редукции и приводятся используемые нами основные теоремы -исчисления. Все приводимые определения и результаты можно найти в монографии1.

Пусть V – счетное множество переменных. Множество термов определяется традиционным образом:

Б а ре н дре г т Х. Ламбда-исчисление, его синтаксис и семантика, М.: Мир, 1985, 606 с..

1. если x V, то x ;

2. если M 1, M 2, то ( M 1M 2 ) ;

3. если x V и M, то ( xM ).

Принято использовать следующую сокращенную запись термов: терм (...( M 1M 2 )...M k ), где M i, i = 1,..., k, k 1, принято обозначать M 1M 2...M k ; терм ( x1 ( x2...( xm M )...)), где M, x j V, j = 1,..., m, m 0, принято обозначать x1...xm.M.

Традиционным образом вводятся понятия свободного и связанного вхождения переменной в терм и понятие свободной переменной терма. Множество всех свободных переменных терма M условимся обозначать FV ( M ). Терм, не содержащий свободных переменных, назовем замкнутым. Множество всех замкнутых термов обозначим 0.

Через M [ x1,..., xm ] условимся обозначать терм M с указанием интересующих нас попарно различных переменных x1,..., xm, m 1. Через M [ N1,..., N m ] или через M [ x1 := N1,..., xm := N m ] обозначим терм, полученный в результате одновременной подстановки термов N1,..., N m в терм M вместо всех свободных вхождений переменных x1,..., xm, соответственно. Подстановку назовем допустимой, если ни одна свободная переменная подставляемого терма не связывается в результате подстановки. Далее, мы будем рассматривать только допустимые подстановки.

Термы M и N назовем конгруэнтными (обозначим M N ), если один терм можно получить из другого переименованием связанных переменных. Далее, мы не будем различать конгруэнтные термы.

Понятие -редукции определяется как следующее множество пар:

= {(( x.R )Q, R[ x := Q]) | R, Q, x V }.

Tерм вида ( x.R)Q называется -редексом (далее просто редексом), а терм R[ x := Q ] – его сверткой. Традиционным образом определяются отношение одношаговой -редукции ( ), отношение -редукции ( ) и отношение равенства ( = ). Далее, условимся отношение одношаговой -редукции называть просто одношаговой редукцией, а отношение -редукции – просто редукцией.

Будем также опускать символ в соответствующих обозначениях, т.е. отношение обозначать, отношение –, а отношение = – =.

Терм, не содержащий редексов, называется -нормальной формой (далее, просто нормальной формой). Множество всех нормальных форм условимся обозначать NF, а множество всех замкнутых нормальных форм – NF 0. Будем говорить, что терм M имеет нормальную форму, если существует терм N NF такой, что M = N.

Теорема Черча-Россера.

a) Если M M 1 и M M 2, то существует такой терм N, что M 1 N и M 2 N.

b) Если M 1 = M 2, то существует такой терм N, что M 1 N и M 2 N.

Следствие теоремы Черча-Россера.

a) Если M = N, где N – нормальная форма, то M N.

b) Если M = N1 и M = N 2, где N1 и N 2 – нормальные формы, то N1 N 2.

Теорема о неподвижной точке. Существует такой терм Z, что если его применить к произвольному терму M, то получим неподвижную точку терма M, т.е. M ( ZM ) = ZM.

–  –  –

неподвижной точки (основной семантикой) программы P, соответствующей комбинатору неподвижной точки Z. Определим множество Fix( P, Z ), соответствующее семантике L1, следующим образом:

Z

–  –  –

В разделе 1.3 формулируется теорема 1.1 (об инвариантности основной семантики относительно комбинатора неподвижной точки), которая является главным результатом данной главы. А также формулируется основная лемма 1.1 и приводится доказательство теоремы 1.1 с использованием леммы 1.1.

Теорема 1.1 (об инвариантности основной семантики).

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

Fix( P, Z ) = Fix ( P, Z ), т.е., множество Fix( P, Z ), соответствующее семантике неподвижной точки, инвариантно относительно комбинатора неподвижной точки.

Справедливость теоремы 1.1 вытекает из следующей основной леммы 1.1.

Лемма 1.1 (основная).

Пусть Z, Z – произвольные комбинаторы неподвижной точки и M – терм, в котором зафиксировано некоторое вхождение подтерма ZL, L. Обозначим через M терм, который получается из M заменой указанного вхождения подтерма ZL термом Z L. Предположим также, что свободные вхождения переменных в соответствующих вхождениях подтермов ZL и Z L не связываются в термах M и M, соответственно. Тогда M 0 является нормальной формой терма M в том и только в том случае, если M 0 является нормальной формой терма M.

Разделы 1.4 и 1.

5 посвящены доказательству основной леммы 1.1.

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

В разделе 2.1 доказывается следующая теорема 2.1.

Теорема 2.1.

Существует бестиповая функциональная программа P0 и такие комбинаторы неподвижной точки Z и Z, что, если L – основная семантика программы P0, определяемая с помощью комбинатора неподвижной точки Z, а L

– основная семантика программы P0, определяемая с помощью комбинатора неподвижной точки Z, то L L.

Причем, теорема 2.1 доказывается для классических комбинаторов неподвижной точки Y и.

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

Редукционной стратегией называется произвольное отображение S :

такое, что для любого терма M, M S ( M ). Из этого определения, согласно следствию теоремы Черча-Россера, вытекает, что если M NF, то S ( M ) M.

Редукционная стратегия S называется одношаговой, если при M \ NF, M S ( M ). Редукцию M N назовем S редукцией, если N S n ( M ), где n 0 и S n ( M ) определяется следующим образом: S 0 ( M ) M, S k +1 ( M ) S ( S k ( M )), k 0.

S Для S редукции M N, мы будем использовать запись M N. Редукционная стратегия S называется нормализующей, если для любого терма M, имеющего S нормальную форму M 0, имеет место M M 0.

Пусть S – редукционная стратегия, Z1, Z 2 – комбинаторы неподвижной точки, P – бестиповая функциональная программа и L1, L2 – основные семантики программы P, определяемые с помощью Z1, Z 2, соответственно. Тогда, согласно теореме 1.1 об инвариантности основной семантики, для любых Q1,..., Qk, M 0 NF 0 ( k 0 ) имеем L1Q1...Qk M 0 L2Q1...Qk M 0.

Возникает вопрос: имеет ли место то же самое для редукционной стратегии S, т.е. имеет ли место следующее?

S S (2) L1Q1...Qk M 0 L2Q1...Qk M 0 Редукционная стратегия определяется как произвольное отображение с ограничением, что это отображение, как отношение, является подмножеством отношения -редукции. Следовательно, нетрудно построить “искусственную” стратегию, для которой (2) не имеет место. Ввиду этого, мы рассматриваем данный вопрос для “естественных” классов стратегий, которые мы сейчас определим.

Определим класс активных редукционных стратегий и класс улучшенных активных стратегий. Все редукционные стратегии этих классов являются одношаговыми. Пусть – произвольное множество термов, содержащее все нормальные формы, т.е. NF. Определим активную редукционную стратегию AS. Пусть M \ NF и ( x.R)Q – самый левый редекс терма M. Тогда:

1. если Q, то AS ( M ) определяется как результат одношаговой редукции терма M, во время которой свертывается самый левый редекс ( x.R)Q ;

2. в противном случае, если Q, то AS ( M ) определяется как терм, полученный путем замены рассмотренного вхождения терма Q термом AS (Q).

Определим улучшенную активную редукционную стратегию ASR. Пусть

M \ NF и ( x.R)Q – самый левый редекс терма M. Тогда:

1. если Q или x FV ( R ), то ASR ( M ) определяется как результат одношаговой редукции терма M, во время которой свертывается самый левый редекс ( x.R)Q ;

2. в противном случае, если Q, то ASR ( M ) определяется как терм, полученный путем замены рассмотренного вхождения терма Q термом ASR (Q ).

“Улучшение” во втором определении состоит в том, что если терм R самого левого редекса ( x.R)Q рассматриваемого терма не содержит свободных вхождений переменной x, то нет смысла редуцировать терм Q, и в этом случае также свертывается редекс ( x.R)Q.

Теорема 2.2.

Пусть редукционная стратегия AS ( NF ) не нормализующая и пусть множество не содержит термов вида y.( x.R)Q ( R, Q, x, y V ). Тогда существует программа P, комбинаторы неподвижной точки Z1, Z 2 и термы N1,..., N k NF 0 ( k 0 ) такие, что если L1, L2 – основные семантики программы P, определяемые с помощью Z1, Z 2, соответственно, то AS L1 N1...N k M 0 NF 0, а AS редукция терма L2 N1...N k продолжается бесконечно.

Теорема 2.3.

Пусть редукционная стратегия ASR ( NF ) не нормализующая. Тогда существует программа P, комбинаторы неподвижной точки Z1, Z 2 и термы N1,..., N k NF 0 ( k 0 ) такие, что если L1, L2 – основные семантики программы P, определяемые с помощью Z1, Z 2, соответственно, то ASR L1 N1...N k M 0 NF 0, а ASR редукция терма L2 N1...N k продолжается бесконечно.

–  –  –

Теорема 2.5.

Существует бестиповая функциональная программа P, состоящая из одного уравнения, комбинатор неподвижной точки Z и термы N1,..., N k ( k 0 ) такие, что если L – основная семантика программы P, определяемая с помощью Z обычным образом, а K – основная семантика программы P, определяемая с ANFR помощью Z согласно (4), то KN1...N k M 0 NF, где ANFR = ASRNF, но ANFR редукция терма LN1...N k продолжается бесконечно.

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

В разделе 3.1 приводятся используемые определения и результаты, взятые из работ1,2. Пусть A1,, An – частично упорядоченные множества с частичными Moschovakis Y.N. On Basic Notions of Theory of Induction. Logic, Foundations of Mathematics and Computability, Butts, Hintikka, eds. Reidel, 1977, p. 207-236.

Ни ги ян С.А. Об интерпретации функциональных языков программирования. Программирование, N2, 1993, стр. 58-68 порядками 1,, n, соответственно. Определим частичный порядок на множестве

A1 An следующим образом:

(a1, an ) (b1,, bn ) если ai bi, 1 i n, для любых (a1, an ), (b1,, bn ) A1 An.

Если A и B – частично упорядоченные множества с частичными порядками A, B, соответственно, то частичный порядок на множестве отображений = { f | f : A B} определим следующим образом: для любых f, g, f g, если f (a) B g (a), для каждого a A. Отображение f называется монотонным, если для любых a1, a2 A, из a1 A a 2 следует f (a1 ) B f (a 2 ). Множество всех монотонных отображений из A в B обозначим [ A B].

Частично упорядоченное множество A называется полным, если всякое линейно упорядоченное подмножество A имеет наименьшую верхнюю грань. Очевидно, что всякое полное множество имеет наименьший элемент – sup. Известно, что если A и B – полные множества, то таковым будут и множества A B и [ A B].

Пусть A – полное множество, f [ A A] и – наименьший элемент множества A. Для всякого ординала l, определим f l () следующим образом:

f 0 () =, если существует l такой, что l = l + 1, то f l () = f ( f l ()), в противном случае f l () = sup { f l () | l l}. Известно1, что существует ординал l0 l такой, что f 0 () есть наименьшая неподвижная точка отображения f.

Зафиксируем счетное предметное множество M такое, что M, и определим частичный порядок на нем следующим образом: для каждого m M, m, m m.

Определим множество типов TYPES и одновременно каждому типу сопоставим натуральное число ord ( ), называемое его порядком.

1. M TYPES и ord( M ) = 0 ;

2. если 1,, k, TYPES (k 1), то [1 k ] TYPES и ord ([ 1 k ]) = max(ord( 1 ),, ord( k ), ord( )) + Известно, что всякий тип является полным множеством. Пусть TYPES и c. Тогда c будем называть константой типа и положим ord(c) = ord( ).

Каждому типу сопоставим счетное множество переменных типа – V, которые могут принимать значения из множества. Если x V, то положим ord ( x) = ord ( ). Приведем определение типизированного терма. Так как далее мы будем рассматривать только типизированные термы, то условимся, далее говоря терм, понимать типизированный терм. Множество всех термов типа обозначим через. Параллельно с определением терма, для каждого терма t определим множество свободных переменных терма t, которое обозначим FV (t ).

Предположим также, что FV (t ) { y1,, y n } ( n 0 ), где y i Vi, i TYPES, 1 Moschovakis Y.N. On Basic Notions of Theory of Induction. Logic, Foundations of Mathematics and Computability, Butts, Hintikka, eds. Reidel, 1977, p. 207-236.

–  –  –

программы P и – наименьший элемент множества 1 n, то для любой Fi 1 Ни ги ян С.А. Об интерпретации функциональных языков программирования. Программирование, N2, 1993, стр. 58-68

–  –  –

соответствующий натуральному ряду.

В разделе 3.2 приводятся оценки ординала, при котором достигается наименьшая неподвижная точка произвольного монотонного отображения.

Пусть A – полное множество. Через D( A) мы будем обозначать множество всех линейно упорядоченных подмножеств множества A, а через DL( A) – множество всех вполне упорядоченных подмножеств множества A. Для каждого вполне упорядоченного множества D DL( A), через o(D) мы будем обозначать соответствующий ему ординал. Определим множество ординалов L( A) следующим образом:

L( A) = {l | D DL( A), o( D ) = l }.

–  –  –

Теорема 3.2.

Пусть A – полное множество и – наименьший элемент множества A, l A – ординал, соответствующий множеству L( A). Тогда для любого ординала l0 такого, что l0 + 2 l A, существует такое отображение f [ A A], что f l0 () f l0 +1 ().

В разделе 3.3 приводятся оценки ординалов, при которых получаются компоненты порядка 3 наименьшего решения строго типизированных программ.

Следующая теорема 3.3 непосредственно следует из теоремы 3.1.

Теорема 3.3.

Пусть P – программа (5), – отображение, соответствующее системе P, – наименьший элемент множества 1 x … x n, l p – ординал, соответствующий множеству L( 1 x … x n ) и f = ( f1, … f n ) – наименьшее решение l системы P. Тогда f i = p () i, 1 i n.

–  –  –

всех переменных от которых зависит Fi, т.е. DV ( Fi ) = {Fj Fi Fj }.

Заметим, что FV (t i ) DV ( Fi ). Очевидно, что только что введенное нами отношение "зависимости" между переменными транзитивно. Следовательно, если переменная Fi зависит от переменной F j, то DV ( F j ) DV ( Fi ). Через DV3 ( Fi ) мы будем обозначать множество всех переменных порядка три и выше, от которых зависит переменная Fi, т.е. DV3 ( Fi ) = {F j DV ( Fi ) | ord ( F j ) 3}. Очевидно, что если переменная Fi зависит от переменной F j, то DV3 ( F j ) DV3 ( Fi ). Скажем, что переменная Fi рекурсивна, если Fi зависит от самой себя., т.е. Fi DV ( Fi ).

Теорема 3.4.

Пусть P – программа (5), – отображение, соответствующее системе P, – наименьший элемент множества 1 x … x n, f = ( f 1, … f n ) – наименьшее решение системы P и ord ( Fi ) 3 ( 1 i0 n ). Тогда, если все

–  –  –

Теорема 3.5.

Для любых типов и, существует такая программа P вида (5) и такая переменная Fi (1 i n ) порядка ord([ ]) + 2, что если – отображение, соответствующее системе уравнений P, – наименьший элемент множества 1 x … x n, f = ( f1, … f n ) – наименьшее решение системы P и l0 – ординал, соответствующий множеству L([ ]), то для любого ординала l такого, что l + 2 l0, имеем l ()i l + 1()i.

Если в теореме 3.5 возьмем = = M, то получится, что компонента порядка 3 наименьшего решения не достигается при ординалах счетной мощности.

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

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

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

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

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

1. Hrachyan G. G. On Least Fixpoint of Monotone Mappings and Equation Systems in Monotone Models of Typed Lambda Calculus. Algebra, Geometry & Their Applications, Vol. 3-4, YSU, Yerevan, 2004, p. 86-96.

2. Hrachyan G. G. On Least Solution of Equation Systems in Monotone Models of Typed Lambda Calculus. Proceedings of the Conference CSIT-2005, Yerevan, 2005, p. 70-73.

3. Hrachyan G. G. The Invariance of the Main Semantics of Type-Free Functional Programs Relatively to the Fixpoint Combinator. Proceedings of the Conference CSIT-2007, Yerevan, 2007, p. 48-49.

4. Грачян Г. Г. Комбинаторы неподвижной точки и основная семантика бестиповых функциональных программ. ДНАН Армении, том 109, N1, 2009, стр.7-14.

5. Hrachyan G. G. The Basic Semantics of Untyped Functional Programs and Reduction Strategies. Transactions of IIAP of NAS RA: Mathematical Problems of Computer Science, Vol. 32, 2009, p. 5-13.

« »

.

1.

,,

–  –  –

:, :

, 3. (2 ), :

, 3 :

Gurgen G. Hrachyan “On Basic Semantics of Functional Programs”



Похожие работы:

«24–26 марта, Научная программа 20-й зал №6 №5 №7 №4 Большой зал №3 №1 №2 Регистрация Вход с парковки Лифт 4-го этажа ПРОГРАММА КОНФЕРЕНЦИИ XX Всероссийская юбилейная научно-практическая конференция Достижения и перспективы развития лабораторной службы России Программа 24 марта, вторник 09:00–10:15 РЕГИСТРАЦИЯ УЧАСТНИКОВ БОЛЬШОЙ ЗАЛ 10:15 ОТКРЫТИЕ КОНФЕРЕНЦИИ Приветствие участников: Куликов А.Г. – Проректор по научной работе РМАПО 10:30 Пленарная сессия Председатели: профессор Долгов В.В.,...»

«ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ НАУКИ ИНСТИТУТ МОРСКОЙ ГЕОЛОГИИ И ГЕОФИЗИКИ ДАЛЬНЕВОСТОЧНОГО ОТДЕЛЕНИЯ РОССИЙСКОЙ АКАДЕМИИ НАУК МАЛОЕ ИННОВАЦИОННОЕ ПРЕДПРИЯТИЕ ООО «ГЕОФИЗИЧЕСКИЕ ТЕХНОЛОГИИ» ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ НАУКИ САХАЛИНСКИЙ ФИЛИАЛ ГЕОФИЗИЧЕСКОЙ СЛУЖБЫ РОССИЙСКОЙ АКАДЕМИИ НАУК При финансовой поддержке: ПРАВИТЕЛЬСТВО РОССИЙСКИЙ ФОНД САХАЛИНСКОЙ ФУНДАМЕНТАЛЬНЫХ ОБЛАСТИ ИССЛЕДОВАНИЙ GEODYNAMIC PROCESSES AND NATURAL HAZARDS. LESSONS OF NEFTEGORSK...»

«1. Цели освоения дисциплины Цели освоения дисциплины: формирование у обучающихся прочного мировоззрения на основе изучения классических методов и последних достижений в области синтеза новых материалов не только с позиций эволюции представлений о структуре Периодической системы Д.И. Менделеева на химическом уровне, но и на атомном, микро-, мезо-, и макро уровне. В результате освоения данного модуля бакалавр приобретает знания, умения и навыки, необходимые для реализации в дальнейшем в полном...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИИЙСКОЙ ФЕДЕРАЦИИ Снежинский физико-технический институт – Филиал федерального государственного автономного образовательного учреждения высшего профессионального образования «Национальный исследовательский ядерный университет «МИФИ» (СФТИ НИЯУ МИФИ) УТВЕРЖДАЮ зам. руководителя по учебной и научно-методической работе _ П.О. Румянцев «» 201_ г. ОПИСАНИЕ ОБРАЗОВАТЕЛЬНОЙ ПРОГРАММЫ 14.03.02 – Ядерные физика и технологии Квалификация (степень): академический...»

«Министерство образования Российской Федерации СОГЛАСОВАНО УТВЕРЖДАЮ Заместитель Министра Заместитель Министра здравоохранения Российской образования Российской Федерации Федерации Т.И.Стуколова В.Д.Шадриков 09.03.2000 г. 10.03.2000 г. Номер государственной регистрации 136 МЕД / СП Государственный образовательный стандарт высшего профессионального образования Специальность 040900 – Медицинская биофизика Квалификация – Врач-биофизик Вводится с момента утверждения Москва 2000 1. ОБЩАЯ...»

«№ 6 (6) Национальный исследовательский центр «Курчатовский институт» июнь 2014 Петербургский институт ядерной физики им. Б. П. Константинова Информационный бюллетень События В Кремле состоялось заседание Совета при Президенте РФ по науке и образованию 23 июня под председательством президента В. В. Путина состояалистов требованиям предприятий, что свидетельствует о необхолось заседание Совета при Президенте РФ по науке и образованию. димости пересмотра структуры образовательного процесса. В ходе...»

«С. Д. ВАРЛАМОВ, Л. ] II III.I.Е Р М Л I I. 1'. В. И. 3ИНКОВ СКИЙ Экспериментальные задачи на уроках физики и физических олимпиадах С.Д.Варламов А. Р. 3ильберман В. И. Зинковокий ЭКСПЕРИМЕНТАЛЬНЫЕ ЗАДАЧИ НА УРОКАХ ФИЗИКИ И ФИЗИЧЕСКИХ ОЛИМПИАДАХ Москва Издательство МЦНМО УДК 53 (023) + 74.262.2 ББК 22.3я72 В1 ПоддержаноДепартаментом образования г. Москвы в рамках программы «Одаренные дети» Варламов С. Д., 3ильберман А. Р., Зинковский В. И. В18 Экспериментальныезадачи на уроках физики и...»

«XLIII Международная Звенигородская конференция по физике плазмы и УТС, 8-12 февраля 2016 Программный комитет XLIII Международной (Звенигородской) конференции по физике плазмы и УТС Коврижных Л.М. доктор физико-математических наук, ИОФ РАН, сопредседатель Фортов В.Е. академик РАН, ИТЭС ОИВТ РАН, сопредседатель Александров А.Ф. доктор физико-математических наук, МГУ Воробьев В.С. доктор физико-математических наук, ОИВТ РАН Готт Ю.В. доктор физико-математических наук, НИЦ «Курчатовский институт»...»

«Программа лекционного курса АСТРОФИЗИКА для студентов 4-ого курса (дневная форма обучения) физического факультета Самарского государственного университета (2013-2014 учебный год, 8 семестр, 54 часа) ВВЕДЕНИЕ Предмет и задачи астрономии. Основные разделы астрономии. Возникновение и основные этапы развития астрономии 1. Практическое значение астрономии. РАЗДЕЛ 1. Основы астрометрии 1.1. Небесная сфера (НС). Основные свойства НС. Основные точки, линии, круги и плоскости НС. Системы небесных...»

«Программа мастер класса «ОСНОВЫ НАНОИНЖЕНЕРИИ» Для учащихся и преподавателей СОШ, СПО, физико-математических лицеев и гимназий   Кафедра ИУ-4 К.Ю.Богданов, к.ф.-м.н., зав. кафедрой физики лицея №1586 А.И.Власов, к.т.н., доцент, тел. (499)263-65-52 Основная цель мастер-класса: ознакомить учащихся СОШ, СПО, ССПО, ориентированных на дальнейшее обучение по программам подготовки бакалавра/магистра по направлению подготовки 654300 – Проектирование и технология электронных средств, инженера по...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Федеральное государственное автономное образовательное учреждение «Московский физико-технический институт (государственный университет)» МФТИ «УТВЕРЖДАЮ» Проректор по учебной и методической работе Д.А. Зубцов « »_20 г. Рабочая программа дисциплины (модуля) по дисциплине: Физика элементарных частиц по направлению: 010900 «Прикладные математика и физика» профиль подготовки магистерская программа: 010915 «Физика высоких энергий» факультет: ФОПФ...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ АВТОНОМНОЕ ОБРАЗОВАТЕЛЬНОЕ УЧРЕЖДЕНИЕ ВЫСШЕГО ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ «Национальный исследовательский ядерный университет «МИФИ» «УТВЕРЖДАЮ» Проректор НИЯУ МИФИ _ _ «_» _ 2012 г. Образовательная программа по развитию одаренности у детей и подростков, составленная с учетом уровня подготовленности, направлений интересов, в области физических наук с использованием модели Дополнительное образование детей вуз...»

«Software Integrated Solutions Расписание открытых курсов по программному обеспечению в 2015 году (Тюменский Научный Центр, Schlumberger) Геофизика и геология Кол-во Дата Название курса Уровень курса ПО дней 06.07-10.07 5 Основы и Геология в Petrel Базовый Petrel 10.08-14.08 5 Основы и Геофизика в Petrel Базовый Petrel 27.08-28.08 2 Продвинутая геофизика в Petrel Углубленный Petrel 07.09-09.09 3 Моделирование свойств в Petrel Углубленный Petrel 02.11-05.11 4 Структурное моделирование в Petrel...»

«Авторская программа: Е.М.Гутник, А.В.Перышкин. Физика. 7-9 классы. – М.: Дрофа, 2008 год Учебник Автор А.В. Перышкин Название Физика. 8 класс; Издательство, год издания М.: Дрофа, 2010 Пояснительная записка Рабочая программа по элективному курсу Я решаю лучше всех (методы решения физических задач) составлена на основе авторской учебной программы элективного курса автора Добельник Е.А., утвержденной и допущенной к использованию (протокол РЭС № 4 от 23.11.2005) и переутверждённой в 2011 г. ()...»

«центр образования «Технологии обучения»ПРИНЯТО УТВЕРЖДАЮ учебно-методическим Директор советом _ // Протокол № _ от «»_ 2014 г. «» _ 2014 г. Рабочая программа среднего общего образования «Естествознание» для учеников 11 класса на 2014/2015 учебный год Составитель программы: Филиппова Татьяна Георгиевна учитель физики г. Москва 2014 год ПАСПОРТ РАБОЧЕЙ ПРОГРАММЫ 1. Тип программы: программа среднего (полного) общего образования. 2. Статус программы: рабочая программа учебного курса. 3. Название,...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «ЛИПЕЦКИЙ ГОСУДАРСТВЕННЫЙ ПЕДАГОГИЧЕСКИЙ УНИВЕРСИТЕТ» Факультет физико-математических и компьютерных наук Кафедра русского языка и общего языкознания РАБОЧАЯ ПРОГРАММА ДИСЦИПЛИНЫ Язык и человек Направление подготовки 44.03.05 Педагогическое образование (с двумя профилями подготовки) Профиль подготовки Физика и математика Квалификация...»

«Аннотация к рабочей программе по географии курса «География. Начальный курс. 5 класс». Цели и задачи курса Основными целями курса являются: -знакомство с особенностями природы окружающего нас мира, с древнейшим изобретением человечества – географической картой, с взаимодействием природы и человека;-пробуждение интереса к естественным наукам и к географии в частности;-формирование умений безопасного и экологически целесообразного поведения в окружающей среде. При изучении курса решаются...»

«Е. Д. Карих, И. С. М анак СПЕЦИАЛИЗАЦИЯ “КВАНТОВАЯ ЭЛЕКТРОНИКА” В СИСТЕМ Е М НОГОУРОВНЕВОГО УНИВЕРСИТЕТСКОГО ОБРАЗОВАНИЯ В настоящее время в Белорусском государственном университете происходит системная реорганизация образовательного процесса в связи с переходом на многоуровневую систему подготовки специалистов: ба­ калавр, дипломированный специалист, магистр. В связи с этим пере­ страиваются учебные планы и программы, на качественно новый уро­ вень переводится методическое обеспечение учебного...»

««УТВЕРЖДАЮ» Проректор по УР СГТУ имени Гагарина Ю.А. д.и.н., профессор Лобачева Г.В. «_» 2014 г. ПРОГРАММА междисциплинарного экзамена для поступления в магистратуру по направлению 12.04.04 «Биотехнические системы и технологии» по кафедре «Биотехнические и медицинские аппараты и системы» физико-технического факультета ФГБОУ ВО «Саратовский государственный технический университет имени Гагарина Ю.А.» Саратов 2015 ВОПРОСЫ К МЕЖДИСЦИПЛИНАРНОМУ ВСТУПИТЕЛЬНОМУ ЭКЗАМЕНУ В МАГИСТРАТУРУ ПО НАПРАВЛЕНИЮ...»

«Министерство образования и науки Российской Федерации Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «Уральский государственный педагогический университет» Институт физики и технологии Кафедра теории и методики обучения физике, технологии и мультимедийной дидактики РАБОЧАЯ УЧЕБНАЯ ПРОГРАММА по дисциплине «Деловой иностранный язык» для ООП «050100.68 – Педагогическое образование магистерская программа: Инновационные образовательные...»



 
2016 www.programma.x-pdf.ru - «Бесплатная электронная библиотека - Учебные, рабочие программы»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.