Содержание к диссертации
Введение
ГЛАВА 1. Используемые определения и результаты. теорема о замене 9
1.1. Используемые определения и результаты 10
1.2. Теорема о замене 18
ГЛАВА 2. Формализация понятия 8-редукции. нормальные формы 20
2.1. Понятие 8-редукции. Теорема о редукции 21
2.2. Сильная нормализуемость 25
2.3. Естественное понятие 8-редукции 33
2.4. Единственность нормальной формы 42
ГЛАВА 3. Реальные понятия 5-редукции. правила вычисления 59
3.1. Реальное понятие 8-редукции 61
3.2. Правила вычисления. Функция соответствующая правилу вычисления и реальному понятию 8-редукции 64
3.3. Полнота правила вычисления для фиксированного понятия ^-редукции 72
3.4. Полнота правила вычисления 89
3.5. Полные правила вычисления 91
3.6. Неполные правила вычисления 97
Заключение 100
Литература
- Теорема о замене
- Сильная нормализуемость
- Правила вычисления. Функция соответствующая правилу вычисления и реальному понятию 8-редукции
- Полные правила вычисления
Введение к работе
В предлагаемой диссертационной работе исследуются вопросы, относящиеся к интерпретации строго типизированных функциональных программ, использующих переменные и константы любых порядков. Строго типизированная функциональная программа представляет собой систему уравнений с отделяющимися переменными в монотонной модели типового Л-исчисления. Рассматриваемая нами интерпретация основана на правилах вычисления, использующих подстановку правых частей уравнений программы вместо некоторых свободных вхождений переменных, и последующей ^редукции терма.
Началом исследований такого рода является работа 3. Манны (Z. Manna) [16], глава 5 (русс. пер. [27]), где рассматривались функциональные программы, использующие переменные и константы, порядок которых <1 и которые не использовали Я-абстракцию. Для таких программ была доказана теорема о существовании наименьшего решения, главная компонента которого /р являлась семантикой программы Р. Далее рассматривались шесть правил вычисления, и проводилось сравнение функций, соответствующих этим правилам, с функцией, являющейся семантикой программы. В том случае, когда эти функции совпадали, правило вычисления называлось правилом неподвижной точки (мы такое правило будем называть
4 полным). В том же случае, когда правило вычисления не
являлось правилом неподвижной точки, функция, являющаяся
семантикой программы, являлась продолжением функции,
соответствующей этому правилу.
В работах [28], [29] рассматривались строго типизированные функциональные программы общего вида. Такие программы представляют собой системы уравнений с отделяющимися переменными в монотонной модели типового А,-исчисления, которые используют переменные и константы любых порядков, причем константы порядка 1 являются вычислимыми функциями, а константы, порядок которых 2, -эффективно представимыми. Для таких программ была доказана теорема о существовании наименьшего решения, главная компонента которого, функция/?, является семантикой программы Р, которая достигается на ординале со. Было показано, что для каждой программы Р можно построить программу Р' такую, что Р' не использует констант, порядок которых >2, и/р =/р'.
Перед нами была поставлена задача исследовать вопросы, относящиеся к интерпретации строго типизированных функциональных программ общего вида, использующих переменные любого порядка и константы, порядок которых <1, причем интерпретация должна быть основана на правилах вычисления и р5-редукции. Такое исследование должно включать:
формализацию понятия ^-редукции, исследование этой
формализации;
формализацию понятия правила вычисления, исследование этого понятия;
рассмотрению конкретных правил вычисления (аналогичных рассмотренным в [16]) и исследование этих правил на вопрос полноты.
Исследованию этих вопросов посвящена данная работа. Диссертация состоит из введения, трех глав, заключения и списка используемой литературы.
В главе 1 приводятся используемые определения и результаты, которые берутся нами, как правило, из работ [28], [29] и [30]. Это определения монотонного типа, терма (в монотонной модели типового Л.-исчисления), значения терма, эквивалентности термов, понятия R-нормальной формы, R-нормализуемости и сильной R-нормализуемости для произвольного понятия редукции R. Приводится понятие Р~ редукции и формулируются теоремы о сильной /3-нормализуемости терма и о единственности его Д-нормальной формы. Определяется монотонная система уравнений как система уравнений с отделяющимися переменными в монотонной модели типового ^.-исчисления и формулируется теорема о существовании наименьшего решения для такой системы уравнений. Вводится понятие программы как монотонной системы уравнений, использующей переменные и константы любых порядков, причем константы порядка 1
являются вычислимыми функциями, а константы порядков 2 -эффективно представимы. Семантика программы представляет собой функцию /р, которая является главной компонентой ее наименьшего решения. Формулируется теорема, которая утверждает, что по всякой программе Р можно построить программу Р' такую, что Р' не использует констант, порядок которых >1 и fp = fp'. Далее доказывается теорема о замене, позволяющая замену некоторого подтерма на ему эквивалентный; при этом полученный терм будет эквивалентен данному. Эта теорема носит технический характер и служит для получения основных результатов диссертации.
Теорема о замене
Пусть ї є Ас а є МТ, FV(t) Q {yi,...,yn}, у і є Va, at є MT, і = 1,...,п, п 0. Терм t назовем константным термом со значением d є а, если для любого у0 = у1,...,уп ,у01 є oclf і = 1,...,п имеем: Val- (t)=d.
Введем понятие -редукции: Пусть Л = { f(h,...,tk), т /- константа, г, h, ..., h (к 0) - термы и либо г- константа wf(h,...,tk) является константным термом со значением т, либо т- собственный подтерм терма f(h,...,tk) и j{h,...,h) T\ Любое подмножество 8 множества Л назовем понятием 3-редукции.
Мы будем исследовать понятие редукции /3 и 8, которую обозначим (38. Далее рассматриваемые нами термы не будут использовать константы, порядок которых 2, и условимся /38-редукцию называть просто редукцией, /Анормальную форму -просто нормальной формой, J38-NF обозначать просто NF, одношаговую редукцию обозначать — , редукцию - Теорема 2.1.1 (о редукции). Пусть i,V є А, тогда: t— i = l t .
Перед тем, как перейти к непосредственному доказательству Теоремы 2.1.1, введем одно понятие и докажем Утверждение 2.1.1 и Лемму 2.1.1.
Пусть ї є А, т є Ла, у є Va, а є МТ. Терм т назовем свободным для переменной у в терме Ї, если ни одно из свободных вхождений переменной у в терм Ї не находится в области действия абстрактора, использующего некоторую свободную переменную терма т.
Утверждение 2.1.1. Пусть t є А и FV(t) а {хг,...,Хк,уь---гут}, где х, є Vai, У) є Vp , сії, ft = МТ, і = 1, ..., к, j = 1, ..., т, к,т 0.
Пусть її, ..., tk - термы такие, что tt є Ла , FV(U) с- {yi,...,ym}, tt свободен для xt в терме t и ValPo (tt) = дгД где х є ах, у0 = Уі - Ут У} єД,і = 1, ...,k,j = l, ..., т.Тогда VaLx- (t) = VaLv (t{t/xj). хоУо s Уо l Доказательство ведется индукцией по определению терма. Пусть t = с, с є а, а є МТ, тогда Утверждение 2.1.1 очевидно. Пусть t = х, х є V. Тогда если х =xt (1 i k), то ValSoy0 (xt) = x = Val- (tt), Val- (x,{t/x}) = Valy (tt) и Утверждение 2.1.1 доказано. Если же х = у} (1 j т), то Val- (уг) = у, Valyo (ydt їх}) = Valyo (уі) - у, и Утверждение 2.1.1 доказано. Пусть t = T(TI,...,TS) И ДЛЯ термов Т, Ті, ..., TS (s 0) Утверждение 2.1.1 верно. Тогда: ValSj (т)(УаІ-оУ-о (п),..., Усй-о-о (TS)) (согласно предположению индукции) = Valyg(т{ї/х})(УаІРд(n{їїх}),...,Val- (rs{t/x}))) = Val (z{t Ix Knit Ix },...,Ts{t Ix })) = ValPo(r(Tb...,Ts){I Ix }) = Val -o (t{tlxj). Пусть t = XZI...ZS[T], где zt є AYi, Уг Є MT, І j = Zi Zj, і, j = 1,..., s (s l), T є Ли для терма г Утверждение 2.1.1 верно. Можно считать, что z, 0 {xi,...,Xk,yi,...,ym} для всех і = 1,...,s. Пусть z0 = z1,...,zs , где z, є у, і = 1,...,s. Тогда Val -Xofo (t)(z0) = Val-o-o (А2!...г8[т])(г0) = Val-o oZ (т) (согласно предположению индукции) = Val-o-2o Mtlx}) = Val-o (Xz1...zs[r]{tlx})(z0) = Val-o (t{t/x})(z0). Утверждение 2.1.1 доказано. Лемма 2.1.1. Axi...Xk[r](ti,...,tk) T{tj/xi,...,ti/xk}, где хг є V , at є MT, і pij = Xi Xj, be Л ,т є Л, i,j = 1,...,к (к 1). Доказательство. Пусть FV(Axi...Xk[r](t1,...,tk)) с- {уъ---,ут}, где У] є Vp , р] є MT, j = 1, ..., m (m 0). Учитывая конгруэнтность рассматриваемых нами термов можно, считать, что {xi,...,Xk} п {уь.-,ут} = 0. Пусть у0 = у1,...,ут , у] eft, j = l,...,т, Val% (tt) = х є at/ і = 1,...,к, хо = /..-/л Тогда Val уо (Axi.. .Xk[r](ti,..., h)) VaUJte1...xk[T])(VaUyo(h),...,Val-o(tk)) = УаІ-о(Ях1...хк[т])(х1,...,хк) = Val g-o (т) (по Утверждению 2.1.1) = ValPo (r{tj/xi,...,t]/xk}). Лемма 2.1.1 доказана.
Доказательство Теоремы 2.1.1. Пусть t, V- термы и t — V. Рассмотрим редукционную цепочку Ї — ... — V с минимальной длиной р. Доказательство проведем индукцией пор. Пусть р = 0. Тогда t = t и Теорема 2.1.1 очевидна. Предположим, что Теорема 2.1.1 верна для р 0. Докажем дляр +1. В этом случае t — ... —Н"— , где длина цепочки t — ... — t" равна р (Очевидно, что эта цепочка является самой короткой). Тогда, по предположению индукции ї t". Если покажем, что Ї" t , то в силу транзитивности отношения эквивалентности получим t t .
Докажем, что t" I . Так как Ї"— t , то по определению одношаговой редукции существуют термы г и г такие, что t" = t"r, t = t"r W г,г є /35. Если r,r є Д то r = JX\...xk[T](h,...,h), г = r{t Ixj и по Лемме 2.1.1 г г . Если же г,г є 8, r=f(ti,...,h), г = т, где f(ti,...,tk), т є 8, и по определению 5-редукции г г
Сильная нормализуемость
Пусть to — h —Нг — ... — tn —»... (п 1) некоторая редукционная цепочка для терма to. Подцепочку t, —Нг+і (і 1) этой редукционной цепочки, длина которой равна 1, назовем звеном редукционной цепочки. Каждому звену в редукционной цепочке соответствует одношаговая редукция. Если это -одношаговая Д-редукция ( -редукция), то данное звено назовем /?-звеном (соответственно, -звеном). Если tT — tT некоторое звено редукционной цепочки, где т- редекс, т - его свертка, то редекс т назовем редексом звена, а фиксированное вхождение редекса тв терм tT назовем вхождением редекса звена. Теорема 2.2.1 (о сильной -нормализуемости). Любой терм t сильно -нормализуем. Доказательство ведется индукцией по определению терма.
Пусть t = с, с є а, а є МТ, или t = х, х є V. Тогда очевидно, что терм t сильно -нормализуем. Пусть t = i(ti,...fh) и термы т, h, ..., tk (к 0) сильно & нормализуемы. Докажем, что в этом случае любая 5-редукционная цепочка для терма t конечна. Предположим обратное, т. е. существует бесконечная -редукционная цепочка для терма t. Рассмотрим некоторую такую -редукционную цепочку. Возможны следующие два случая. а) в рассматриваемой -редукционной цепочке для терма t существует -звено U —% U+i (і 0), редексом которого является сам терм if б) в рассматриваемой -редукционной цепочке для терма t такого звена не существует. В случае а) рассмотрим первое такое звено. Пусть t = т(ті,...,Тк) — -%/(т і,...,т к) —% т", где/- константа порядка 1, т — -%/ Ъ — -% т\, і = 1,---,к (к 1), т" - собственный подтерм терма /(тг,...,т\) {т" не может быть константой, так как рассматриваемая нами -редукционная цепочка бесконечна).
Тогда для терма т" также существует бесконечная 5 редукционная цепочка. Очевидно, что т" является подтермом некоторого терма т\ (1 і к), и так как по предположению индукции терм Ті сильно -нормализуем и Ті — ЧБ Т\, ТО легко убедится, что терм т и следовательно, и терм г" также сильно 5 нормализуемы. Это противоречит бесконечности рассматриваемой нами -редукционной цепочки для терма t. Следовательно, в случае а) наше предположение о бесконечности рассматриваемой -редукционной цепочки для терма t ложно.
В случае б) все термы в рассматриваемой -редукционной цепочке имеют вид т {т\,..., Tk), где т — -% т , Ті — -% т\, і = 1,...,к (к 1). Так как по предположению индукции термы т, U, ..., tk сильно -нормализуемы, то рассматриваемая нами & редукционная цепочка для терма т(ті,...,ц) не может быть бесконечной. Полученное противоречие в обоих случаях доказывает, что терм t также сильно -нормализуем. Пусть теперь t = Ахі...Хк[т] и г сильно ( -нормализуем. Тогда очевидно, что t — -% Г в том и только в том случае, если Г = Яхг.-.ХкМ и т— - 5 т . Так как по предположению индукции терм т сильно -нормализуем, терм t также сильно 5-нормализуем. Теорема 2.2.1 доказана. Теорема 2.2.2 (о сильной нормализуемости). Любой терм t сильно нормализуем.
Перед тем как перейти к непосредственному доказательству Теоремы 2.2.2, введем понятие уровня вхождения подтерма в терм, опишем алгоритм разметки неокрашенных и неразмеченных вхождений подтермов в терм, процесс разметки редукционной цепочки и процесс построения / -редукционной цепочки.
Пусть tT - терм с фиксированным вхождением подтерма т. Уровнем фиксированного вхождения подтерма т в терм t назовем число подтермов терма t, собственным подтермом которых является данное вхождение подтерма т.
Далее условимся, что под выражением "вхождение в терм" мы будем понимать вхождение некоторого подтерма в терм.
Правила вычисления. Функция соответствующая правилу вычисления и реальному понятию 8-редукции
Введем понятие правила вычисления р.
Пусть программа Р имеет вид (1) и ї е А такой, что FV(t) с {Vi,...,n}. Перенумеруем все свободные вхождения переменных Fi,...,Fn в терме t слева на право. Правило вычисления р по каждому терму t определяет некоторое непустое подмножество номеров свободных вхождений переменных Fi,...,Fn терма t, которое следует одновременно заменить на термы ті,...,тп/ соответственно. Назовем это подмножество множеством вхождений переменных Fi,...,Fn терма t определяемых правилом вычисления р. Естественно, что подстановка предполагается допустимой. Результат такой замены обозначим P(t).
Перед тем как определить конкретные правила вычисления, введем несколько понятий.
Свободное вхождение переменной F в терм t назовем внутренним, если оно не входит в аппликатор т, область действия которого содержит свободное вхождение (в терм t) некоторой переменной.
Свободное вхождение переменной F в терм t назовем внешним, если оно не входит в область действия аппликатора, содержащего свободное вхождение (в терм t) некоторой переменной в терм Ї.
Свободное вхождение переменной F в терм t назовем свободным для подстановки, если оно либо не является аппликатором, либо имеет по меньшей мере один аргумент, который не содержит свободное вхождение (в терм t) некоторой переменной.
Определим шесть правил вычисления.
1. Правило самой левой внутренней замены: заменяется самое левое внутреннее свободное вхождение переменной.
2. Правило параллельной внутренней замены: заменяются одновременно все внутренние свободные вхождения переменных.
3. Правило самой левой (внешней) замены
заменяется самое левое (внешнее) свободное вхождение переменной.
4. Правило параллельной внешней замены: заменяются одновременно все внешние свободные вхождения переменных.
5. Правило замены вхождений свободных для подстановки: заменяются одновременно все свободные вхождения переменных, свободные для подстановки.
6. Правило полной замены: заменяются одновременно все свободные вхождения переменных.
Правила 1, 2,3,4 и 6 являются обобщениями аналогичных правил вычисления, определенных в [16]. Правилу 5 в [27] соответствует правило свободного аргумента.
Пусть 8 - некоторое понятие -редукции, Р - программа вида (1), где F\ є V к , к 1, р - правило вычисления и d = Dk. Рассмотрим последовательность термов to,h,... определяемую следующим образом: to есть терм Fi(d) , tl+i eNFw. p(tt) — - Un, і 1. Определенную таким образом последовательность термов to, ti, ... назовем последовательностью вычисления для d, соответствующую 8, р и Р. Корректность данного определения следует из Теоремы 2.4.1 (о единственности нормальной формы).
Полные правила вычисления
Докажем, что g(ci,..., 1,...,1) = 1. Предположим обратное g(Cb...,cuL,...,1.) 1. В этом случае в силу монотонности константы g следует, что для любых йг+Ь—Лк є D, g(ci,...,cvl,...,1) с g(ci,—,Ci,dl+i,...,d]() 7і 1. Т.е. для любых значений gi,—,gn свободных переменных Fi,...,Fn Valg (t[p]) l, где g = gh...,gn , что означает, что t терм является константным термом и противоречит условию Леммы 3.5.2. Полученное противоречие доказывает, что наше предположение не верно. Следовательно, g(Ci,...,C„l,...,l) = 1. Лемма 3.5.2 доказана. Доказательство Теоремы 3.5.2. Пусть Р - программа вида (1), где Fi є V t , k l, d є Dk nfp(d) -L- Докажем, что правило параллельной внешней замены на каждом шаге построения последовательности вычисления для d делает существенную подстановку. Пусть to, h, ... - последовательность вычисления для d, соответствующая правилу самой левой замены. В доказательстве Теоремы 3.2.1 было показано, что Valf (tj =fp(d) ± для любого і 0. По Лемме 3.5.2 Va\f{tt[p]{Q/F })=1 для любого
Для программ, в которых используемые константы порядка 1 являются естественно расширенными функциями (кроме if_then_else), правило самой левой замены является полным правилом вычисления.
Перед тем, как перейти к непосредственному доказательству Теоремы 3.5.3, докажем Лемму 3.5.3.
Лемма 3.5.3. Пусть Р - программа вида (1), где используемые константы порядка 1 (кроме if_then_else) являются естественно расширенными функциями, t є Ло, t є NF, FV(t) cz {Fi,...,Fn} и t не является константным термом. Тогда Valj(t[p]{a/F}) = l, где р - правило самой левой замены,/ - наименьшее решение программы Р.
Доказательство проведем индукцией по глубине т самого левого свободного вхождения переменной в терм
Пусть т - 0. Тогда, так как t є NF и t не является константным термом, то либо t = F„ либо t = Ft(...)...(...) для некоторого 1 і п. В обоих случаях очевидно, что Val,(t[p]{n/F}) = ±.
Пусть т - глубина самого левого свободного вхождения переменной в терм t и т 0. Предположим, что для термов, где глубина самого левого свободного вхождения равна т - 1, Лемма 3.5.3 верна. Докажем, что Val/ (t[p]{ Q/F }) = 1. Так как т 0, то либо t = g(h,—,tk), где g - константа порядка 1 и естественно расширенна, либо t =if_then_else(ii,h,h).
Рассмотрим случай, когда Ї = f(th-M, где/- константа порядка 1 и естественно расширена. Пусть самое левое свободное вхождение в терме t находится в подтерме U, 1 i к. Тогда это вхождение будет самым левым и в терме U и его глубина в этом терме равна т - 1. По предположению индукции Valf(t,[p]{f2/F}) = 1. Так как g естественно расширенна, то Val}{t[p]{Q/F}) = g(...,Valf(tt[p]{n/F}),...) = g(...,±,-) = 1. Рассмотрим случай, когда t =ifjhen_else(ti,i2,h), где h,h,h є NF. Самое левое свободное вхождение в терме t находится в подтерме t\. В противном случае, так как ї\ е NF, h будет константой. Следовательно, терм if_then_e\se{ibh,h) будет редексом, что противоречит t є NF. Самое левое свободное вхождение в терме t будет самым левым и в терме h и его глубина в этом терме равна т-1. По предположению индукции Valf(h[p]{n/F})=l.. Тогда Valf(t[p]{Q/F}) if_then_else(Valf {h[p]{Q/F;}),Val; {h),Va\-f (t2)) if_then_else(l,Val / (h),Val/ (h)) = 1. Лемма 3.5.3 доказана.
Доказательство Теоремы 3.5.3. Пусть Р - программа вида (1), где используемые константы порядка 1 являются естественно расширенными функциями (кроме if_then_else), Fj є V k , k l, d є Dk и fp(d) -L- Докажем, что правило самой левой замены на каждом шаге построения последовательности вычисления для d делает существенную подстановку. Пусть to, її, ... - последовательность вычисления для d соответствующая правилу самой левой замены. В доказательстве Теоремы 3.2.1 было показано, что Valf(tt) = fp(d) & -L для любого і 0. По Лемме 3.5.3 Valf {U[p]{Q/F })=1 для любого / 0. Теорема 3.5.3 доказана.