ТЕОРЕТИЧЕСКИЕ ВОПРОСЫ ПРОГРАММИРОВАНИЯ ~
УДК 681.32
ОБ ОСНОВНОЙ СЕМАНТИКЕ БЕСТИПОВЫХ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ
© 2009 г. Г. Г. Грачян
Факультет, информатики и прикладной математики Ереванский государственный университет 0025 Армения, Ереван, ул. Алека Манукяна, 1 E-mail: gurgen.hrachyan@gmail.com Поступила в редакцию 07.12.2007 г.
Данная работа посвящена бестиповым функциональным программам, которые определяются как системы уравнений с отделяющимися переменными в бестиповом А-исчислении [1, 2]. Основная семантика таких программ обычно определяется с помощью комбинатора неподвижной точки У. В данной работе доказывается теорема об инвариантности семантики относительно комбинатора неподвижной точки.
1. ВВЕДЕНИЕ
Бестиповая функциональная программа представляет собой систему уравнений с отделяющимися переменными в бестиповом А-исчисле-нии [1, 2]. Основная семантика таких программ представляет собой терм, который обычно определяется с помощью комбинатора неподвижной точки У. В данной работе доказывается, что семантики, определяемые с помощью разных комбинаторов неподвижной точки, эквивалентны в том смысле, что, если применить их к одним и тем же "данным", то получим один и тот же "результат".
В [2] определяются и исследуются алгоритмы интерпретации бестиповых функциональных программ. Процедурные семантики, основанные на этих алгоритмах, сравниваются с основной семантикой, определеяемой с помощью комбинатора неподвижной точки У. Из данной работы следует, что результаты, полученные в [2], верны для семантик, определяемых с помощью произвольного комбинатора неподвижной точки.
Работа состоит из введения и разделов 2-5. В разделе 2 приводятся используемые определения и результаты, которые можно найти в [1]. В разделе 3 дается определение бестиповой функциональной программы, ее основной семантики
[2] и формулируется теорема 1 (об инвариантности семантики относительно комбинатора неподвижной точки), которая является главным результатом данной работы. В разделе 3 также формулируется основная лемма 1 и приводится доказательство теоремы 1 с использованием леммы 1. Остальные разделы работы посвящены доказательству леммы 1. В разделе 4 приводятся вспомогательные понятия, такие, как понятия вхождения и остатка, а в разделе 5 определяется понятие контекста неподвижной точки и доказывается лемма 1.
2. ИСПОЛЬЗУЕМЫЕ ОПРЕДЕЛЕНИЯ И РЕЗУЛЬТАТЫ
В этом разделе приводятся используемые нами определения и результаты. Все приводимые определения и оставляемые без доказательства утверждения можно найти в [1]. Прежде всего определим понятие терма. Пусть V - счетное множество переменных. Множество термов Л является наименьшим множеством, удовлетворяющим следующим условиям:
1. если х £ У, то х £ Л;
2. если Мъ М2 £ Л, то (М1М2) € Л;
3. если х £ V и М £ Л, то (АхМ) £ Л.
Принято использовать следующую сокращенную запись термов: терм (• • • (М1М2) • • - Ми), где Мг £ А, г = 1, ■ ■ ■, к, к > 1, принято обозначать М1М2 ■■■мк-терм (Аж1(Аж2 • • • (АхтМ) ■ • •)), где М £ А, Xj £ V, ] = 1, • • •, то, то > О, принято обозначать \х\х2 ■ ■ ■ хт.М. Мы также будем использовать следующее обозначение: терм (Ь(Ь---(ЬМ) •••)), где М, Ь £ Л, г > О, мы буг
дем обозначать ЬгМ.
Традиционным образом вводятся понятия свободного и связанного вхождения переменной в терм и понятие свободной переменной терма. Множество всех свободных переменных терма М условимся обозначать РУ(М). Терм, не содержащий свободных переменных, назовем замкнутым. Множество всех замкнутых термов обозначим Л°.
Через М[х\, ■ ■ ■, хт] условимся обозначать терм М с указанием интересующих нас попарно различных переменных х1,---,хт, то > 1. Через М[Л^1, • • •, ТУт] или через М[х1 := 7УЬ ■ ■ ■ ^Хк'■= N,1^ обозначим терм, полученный в результате одновременной подстановки термов N1, • • •, Nm в терм М вместо всех свободных вхождений переменных х\, ■ ■ ■, хт, соответственно. Для краткости обозначений будем также использовать векторную запись, т.е. терм М[х 1,---,жт] будем обозначать также через М[х\, где х - вектор переменных XI, • • •, хт, а терм 1, • • •, _/Ут] будем обозначать также через М[Л7] или М[х := Щ, где N - вектор термов • • •, Подстановку назовем допустимой,
если ни одна свободная переменная подставляемого терма не связывается в результате подстановки. Далее мы будем рассматривать только допустимые подстановки.
Термы М ъ N назовем конгруэнтными (обозначим М = М), если один терм можно получить из другого переименованием связанных переменных. Далее мы не будем различать конгруэнтные термы. Символ = также будем использовать для указания покомпонентной конгруэнтности векторов термов, т.е. если М - вектор термов М\, • • •, Мк, к > 0, и N - вектор термов N1, • • •, Мт1 то > 0, то запись М = N будет означать, что к = т и Мг- = Ni, г = 1, • • •, к.
Понятие /3-редукции определяется как следующее множество пар:
/3 = {((\х.р[х])<2, Р[х := <з]) | р,д е л, ж е V}.
Терм вида (Ах.Р[х])(^) называется /3-редексом (далее просто редексом), а терм Р[х := 0\ - его сверткой. Отношение одношаговой /3-редукции (—>/з) определяется следующим образом:
1. если (М1,М2) £ /3, то М1 —М2;
2. если М\ —М2, то для произвольного терма М и произвольной переменной х имеем:
(a) ММг —ур ММ2,
(b) МгМ —М2М,
(c) \x.Mi —У/з Ах.М2.
Нетрудно заметить, что М\ —Ур М2 означает, что терм М\ получается из терма М2 путем замены в терме М\ некоторого вхождения редек-са его сверткой. Отношение /3-редукции (—>■— определяется как рефлексивное и транзитивное замыкание отношения одношаговой /3-редукции, а отношение /3-равенства (=/?) определяется следующим образом:
1. если М1 ——У/з М2, то М1 =¡3 М2;
2. если М1 =/з М2, то М2 =/3
3. если М1 =/з М2 и М2 =/3 М3, то М1 =Гз М3.
Далее условимся отношение одношаговой /3-редукции называть просто одношаговой редукцией, а отношение /3-редукции - просто редукцией. Будем также опускать символ /3 в соответствующих обозначениях, т.е. отношение —>¡3 обозначать —)>, отношение —>■—>■/?-->■—>■, а отношение
Терм, не содержащий редексов, называется /3-нормальной формой (далее просто нормальной формой). Множество всех нормальных форм условимся обозначать А^Р, а множество всех замкнутых нормальных форм - ТУР0. Будем говорить, что терм М имеет нормальную форму, если существует терм N £ NР такой, что М = N. Поскольку /3-редукция является рефлексивным и транзитивным замыканием
одношаговой /3-редукции, то из М —>~> N следует, что существуют такие термы М\, • • •, Мк {к > 0), что М0 = М, Мк = N и Мг_ 1 —> Мг, г = 1, • • •, к. Учитывая указанный факт, условимся далее употреблять термин "редукция" не только в смысле отношения —>■—>■, но и в смысле конкретной (возможно, пустой) последовательности одношаговых редукций, т.е. если говорим, что имеем редукцию М —>~> N, то это означает, что имеем конкретную (возможно, пустую) последовательность одношаговых редукций из терма М в терм N. В случае пустой последовательности редукцию назовем пустой редукцией.
Приведем некоторые утверждения, которые мы далее будем широко использовать.
Утверждение 2.1. Пусть Р - произвольный терм, Ь = 1,1,---,Ьк и <3 = (З1, • • •, <Зт -произвольные векторы термов, а х = х■ ■ ■ ,хк и у = г/1, • • •, ут - векторы переменных, причем гфг' => хгф жг/, 2 ф / => у} ф у3,, Х{ ф х^ и у2 ^ РУ(Ь^, где г, г' = 1, • • •, к, к > 0, = 1, • • •, то, то > 0. Тогда
Р[у := <Э][аГ := Ь] = Р[х := £][у := $[х := £]],
где <5[ж := Ь] = С^^х := Ь], ■ ■ - ,<9ш[ж := Ь].
Доказательство. Применим индукцию по построению терма Р:
1. Если Р - переменная, то возможны следующие варианты:
(a) Р = Х{ (1 < I < к). Тогда обе части доказываемого утверждения равны
(b) Р = yj (1 < 3 )■ Тогда обе части равны (^¿[х := Ь].
(c) Р = г ъ г {хг, ■ ■■,хк,у1, • • •,ук}. Тогда обе части равны г.
2. Если Р = РХР2 или Р = АхРх, где х е V, Р\, Р2 € Л, то доказываемое утверждение непосредственно следует из предположения индукции.
Утверждение 2.1 доказано.
Теорема о замене. Пусть Мдг - терм, в котором зафиксировано некоторое вхождение подтерма N. Обозначим через М£ терм, который получается из М путем замены рассматриваемого вхождения подтерма N некоторым термом Ь. Тогда имеет место следующее:
a. N —> Ь Мм —> Мь■
b. N ->—> Ь => Мм ->—> Мь;
c. N = Ь => Мдг = Мь.
Утверждение 2.2. Для произвольных термов М, N, Ь и произвольной переменной х:
a. М —> N => М[х := Ь] —> := Ь];
b. М N М[х := Ь] N[1 := Ь];
c. М = N => М[х := Ь] = N[1 := Ь].
Теорема Черча-Россера. Имеет место следующее:
a. Если М -т—т- Мд и М —>~> М2, то существует такой терм N, что М\ —т—> N и М2 N.
b. Если М\ = М2, то существует такой терм N1 что М\ —>—> N и М2 —> N.
Следствие теоремы Черча-Россера. Имеет место следующее:
а. Если М = N, где N то М ->—> N.
нормальная форма,
Ь. Если М = N1 и М = N2, где ^ и N2 - нормальные формы, то N1 = N2-
Известно, что любой терм М имеет один из следующих видов:
М = \xi---Xk.xNi---Nn, (1)
М = \х1---хк.(\хР)С}М1---Мп, (2)
где Х,Х{£У, г = 1 к > 0, Р, <3,Л^бЛ,
j = 1, • • • ,п, п > 0. Терм вида (1) называется головной нормальной формой. Множество всех головных нормальных форм условимся обозначать HNF. Будем говорить, что терм М имеет головную нормальную форму, если существует такой терм N 6 HNF, что М = N. Известно, что NF С HNF, но HNF <£ NF. Если терм М не является головной нормальной формой, т.е. имеет вид (2), то одношаговую редукцию
—у \х\ ■ ■ -хк.Р[х :=
назовем головной одношаговой редукцией, а все остальные одношаговые редукции назовем внутренними. Редукцию назовем головной редукцией, если она состоит из головных одношаго-вых редукций. Головную одношаговую редукцию М —у N обозначим М —у N, а голов-
h
ную редукцию М —у—у N обозначим М —у—у N.
h
Аналогично, редукцию, состоящую из внутренних одношаговых редукций, назовем внутренней редукцией. Внутреннюю одношаговую редукцию М —у N обозначим М —у N, а внутрен-
i
нюю редукцию М —у—у N обозначим М —у—у N.
г
Заметим, что любая редукция, которая начинается головной нормальной формой, является внутренней редукцией.
Утверждение 2.3. Если имеем головную редукцию М —у—у N, то для произвольной пере-h
менн
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.