Лекции по семантика на езиците за програмиране
Изтегляне 3.6 Mb.
|
R i (X1/1 (Y/), X2/2 (Y/), …, / (Y/), F) c. Oт друга страна, (Y/) = (1 (Y/), 2 (Y/), …, (Y/)). Окончателно, R (Y/, F) c. Лемата е доказана.
Доказателство: провеждаме индукция по дължината на извода по стойност R c. Нека R c с дължина на извода s и твърдението е изпълнено за изводи R c с дължина на извода по-малка от s. Разглеждаме различни случаи в зависимост от вида на . Нека е константа, = d. Имаме R c, така че от лемата за извода c = d и R c. Нека е основна операция, = f (1, 2, …, n). Имаме R c с дължина на извода s, така че от лемата за извода съществуват константи c1, c2, …, cn, такива че R j cj, j = 1, 2, …, n с дължина на изводите по-малка от s и f (c1, c2, …, cn) = c. От индукционното предположение получаваме R j cj, j = 1, 2, …, n. Освен това f (c1, c2, …, cn) = c, така че R c. Нека е условен терм, = if then 1 else 2. Имаме R c с дължина на извода s, така че от лемата за извода R tt и R 1 c или R ff и R 2 c, при това изводите са с дължина по-малка от s. Нека R tt и R 1 c. От индукционното предположение R tt и R 1 c. Така R c. Случаят R ff и R 2 c се разглежда абсолютно аналогично. Нека е обръщение към функция, = (1, 2, …, ). Имаме R c с дължина на извода s, така че от лемата за извода съществуват константи c1, c2, …, , такива че R j cj, j = 1, 2, …, ni с дължини на изводите по-малки от s и R i (X1/c1, X2/c2, …, / , F) c с дължина на извода по-малка от s. От индукционното предположение получаваме R j cj, j = 1, 2, …, ni и R i (X1/c1, X2/c2, …, / , F) c. Прилагаме лемата за симулацията и получаваме R i (X1/1, X2/2, …, / , F) c. Оттук получаваме R c. Теорема: OV (R) ON (R). Доказателство: нека OV (R)(а) b. Тогава R 0 (X/a, F) b. От предната лема получаваме R 0 (X/a, F) b. Taка ON (R)(а) b.
Нека a1, a2, …, an N, 1 , 2 , …, k . Дефинираме индуктивно понятието стойност на терма в a1, …, an, 1, …, k, която записваме (a1, …, an, 1, …, k) или съкратено (a, ):
Тогава (а, ) f (1 (a, ), 2 (a, ), …, l (a, )).
(a, ) 1 (a, ), ако (a, ) tt, (a, ) 2 (a, ), ако (a, ) ff, ! (a, ), ако ! (a, ).
Тогава (a, ) i (1 (a, ), 2 (a, ), …, (a, )). Тъй като функциите i са частични, стойността (a, ) може да не е навсякъде определена. Освен това, стойността на терма, ако е определена, зависи от неговия тип – ако термът е от тип Bool, то той приема булеви стойности, ако термът е условен или е от тип Nat, то неговите стойности са естествени числа. По-нататък за краткост ще означаваме F = . Лема (съгласуване на заместване и стойност): Нека (X1, …, Xn, , , …, ) e терм. Нека 1 ( , , …, ), 2 ( , , …, ), …, n ( , , …, ) са функционални термове, F и 1 () c1, 2 () c2, …, n () cn. Тогава (c, ) (X/, F)(). Доказателство: индукция по построението на . Нека е константа, = c. Тогава (c, ) c, (X/, F) = c и (X/, F)() c (c, ) (X/, F)(). Нека е обектова променлива, = Xi, i { 1, 2, …, n }. Тогава (c, ) ci и (X/, F) = i (F), така че (X/, F)() ci (c, ) (X/, F)(). Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Тогава (c, ) f (1 (c, ), 2 (c, ), …, l (c, )) f (1 (X/, F)(), 2 (X/, F)(), …, l (X/, F)()) f (1 (X/, F), 2 (X/, F), …, l (X/, F))() f (1, 2, …, l)(X/, F)() (X/, F)(). Използвали сме индукционното предположение и дефиницията за стойност на терм. Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Нека (c, ) tt. Тогава (c, ) 1 (c, ). От друга страна (X/, F) = if (X/, F) then 1 (X/, F) else 2 (X/, F). По индукционното предположение (X/, F)() tt и 1 (X/, F)() 1 (c, ). При това положение, (X/, F)() 1 (X/, F)() 1 (c, ) (c, ). Случаят (c, ) ff се разглежда абсолютно аналогично. Нека ! (c, ). Тогава ! (c, ). От индукционното предположение имаме ! (X/, F)() ! (X/, F)() (c, ) (X/, F)(). Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Имаме (c, ) i (1 (c, ), 2 (c, ), …, (c, )) i (1 (X/, F)(), 2 (X/, F)(), …, (X/, F)()) (1 (X/, F), 2 (X/, F), …, (X/, F))() (1, 2, …, )(X/, F)() (X/, F)(). Използвали сме индукционното предположение и дефиницията за стойност на терм. Твърдение (за монотонност): Нека (X, F) е терм, , F, и a Nn. Тогава за всяка константа b от типа на имаме, че (a, ) b (a, ) b. Доказателство: индукция по построението на . Нека е константа, = c. Нека (a, ) b. Тогава b = c и (a, ) c = b. Нека е обектова променлива, = Xi, i { 1, 2, …, n }. Нека (a, ) b. Тогава b = ai и (a, ) ai = b. Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Нека (a, ) b. Тогава съществуват константи c1, c2, …, cl, такива че 1 (a, ) c1, 2 (a, ) c2, …, l (a, ) cl и f (c1, c2, …, cl) = b. От индукционното предположение 1 (a, ) c1, 2 (a, ) c2, …, l (a, ) cl, също f (c1, c2, …, cl) = b (а, ) f (1 (a, ), 2 (a, ), …, l (a, )) f (c1, c2, …, cl) = b. Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Нека (a, ) b. Тогава (а, ) tt и 1 (a, ) b или (а, ) ff и 2 (a, ) b. Нека (a, ) tt и 1 (a, ) b. От индукционното предположение имаме (a, ) tt и 1 (a, ) b. Така (a, ) b. Случаят (а, ) ff и 2 (a, ) b се разглежда аналогично. Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Нека (a, ) b. Тогава съществуват константи c1, c2, …, , такива че 1 (a, ) c1, 2 (a, ) c2, …, (а, ) и i (c1, c2, …, ) b. От индукционното предположение имаме, че 1 (a, ) c1, 2 (a, ) c2, …, (а, ) . Тъй като , то i (c1, c2, …, ) b. Така (a, ) b. Твърдение (за компактност): Нека (X, F) е терм. За всеки а Nn, F и константа b от типа на е изпълнено: (a, ) b съществуват крайни подфункции , такива че (a, ) b. Доказателство: индукция по построението на . Нека е константа, = c. Нека (a, ) b. Тогава b = c. Да изберем = (!1, !2, …, ! ). Тук индексът показва броя на аргументите. Тогава са крайни подфункции на и (a, ) c = b. Нека е обектова променлива, = Xi, i { 1, 2, …, n }. Нека (a, ) b. Тогава b = ai. Да изберем = (!1, !2, …, ! ). Тогава са крайни подфункции на и (a, ) ai = b. Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Нека (a, ) b. Тогава съществуват константи c1, c2, …, cl, такива че 1 (a, ) c1, 2 (a, ) c2, …, l (a, ) cl и f (c1, c2, …, cl) = b. От индукционното предположение съществуват крайни подфункции 1 , 2 , …, l , такива че 1 (a, 1) c1, 2 (a, 2) c2, …, l (a, l) cl. Нека 1 = (11, 12, …, 1k), 1j j, j = 1, 2, …, k. Нека 2 = (21, 22, …, 2k), 2j j, j = 1, 2, …, k. … Нека l = (l1, l2, …, lk), lj j, j = 1, 2, …, k. Нека 1 = 11 21 … l1. Тъй като 11, 21, …, l1 са крайни подфункции на една и съща функция 1, то 1 e добре дефинирана крайна подфункция на 1. Аналогично, нека 2 = 12 22 … l2, 2 2, …, k = 1k 2k … lk, k k. Нека = (1, 2, …, k). Тогава и са крайни функции. Ясно е, че i , i = 1, 2, …, l. От монотонността получаваме 1 (a, ) c1, 2 (a, ) c2, …, l (a, ) cl, също f (c1, c2, …, cl) = b (a, ) b. Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Нека (a, ) b. Тогава (а, ) tt и 1 (a, ) b или (а, ) ff и 2 (a, ) b. Нека (a, ) tt и 1 (a, ) b. От индукционното предположение съществуват крайни подфункции 1 , 2 , такива че (a, 1) tt и 1 (a, 2) b. Нека 1 = (11, 12, …, 1k), 1j j, j = 1, 2, …, k. Нека 2 = (21, 22, …, 2k), 2j j, j = 1, 2, …, k. Тогава 1 = 11 21 e добре дефинирана крайна подфункция на 1, 2 = 12 22 e добре дефинирана крайна подфункция на 2, …, k = 1k 2k e добре дефинирана крайна подфункция на k. Нека = (1, 2). Тогава и са крайни функции. Естествено, 1 , 2 и от монотонността получаваме (a, ) tt и 1 (a, ) b. При това положение, (a, ) b. Случаят (а, ) ff и 2 (a, ) b се разглежда абсолютно аналогично. Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Нека (a, ) b. Тогава съществуват константи c1, c2, …, , такива че 1 (a, ) c1, 2 (a, ) c2, …, (а, ) и i (c1, c2, …, ) b. От индукционното предположение съществуват крайни подфункции 1 , 2 , …, , такива че 1 (a, 1) c1, 2 (a, 2) c2, …, (а, ) . Нека 1 = (11, 12, …, 1k), 1j j, j = 1, 2, …, k. Нека 2 = (21, 22, …, 2k), 2j j, j = 1, 2, …, k. … Нека = ( , , …, ), j, j = 1, 2, …, k. Нека 1 = 11 21 … , 2 = 12 22 … , …, k = 1k 2k … . Oтново 1, 2, …, k са крайни функции и 1 1, 2 2, …, k 1. Нека i* = i { (c1, c2, …, , b }. Тогава i* е крайна подфункция на i, тъй като i (c1, c2, …, ) b и i е крайна подфункция на i. Нека = (1, …, i-1, i*, i+1, …, k). Тогава и са крайни функции. Естествено, 1 , 2 , …, и от монотонността получаваме, че 1 (a, ) c1, 2 (a, ) c2, …, (а, ) . Освен това, i* (c1, c2, …, ) b (a, ) b. Твърдението е доказано.
Нека 0 1 … n …е монотонно растяща редица от елементи на F. За всеки a Nn и константа b от типа на имаме (a, ) b съществува n N, такова че (a, n) b. Доказателство: нека съществува n N, такова че (a, n) b. Имаме n и от монотонността получаваме (a, ) b. Нека (a, ) b. От твърдението за компактност съществуват крайни подфункции , такива че (a, ) b. Нека = (1, 2, …, k). Имаме = . Тъй като , то 1 , 2 , …, k . Имаме, че 1, 2, …, k са крайни функции и от едно твърдение за частични функции получаваме, че съществуват n1, n2, …, nk, такива че 1 , 2 , …, k . Нека n = max (n1, n2, …, nk). Тъй като редиците { }, { }, …, { } са монотонни, то 1 , 2 , …, k n. Накрая от твърдението за монотонност получаваме (a, n) b. Нека (X1, …, Xn, , , …, ) е терм от тип Nat или условен терм. Дефинираме изображение Г : F по следния начин: Г (1, 2, …, k)(a1, a2, …, an) (a1, …, an, 1, …, k) за всяко (a1, a2, …, an) Nn, (1, 2, …, k) F. Каталог: uni uni -> Отчет за ибсф ра, ибсф ksf и ибсф 33 за средствата по набирателните сметки uni -> Условия и ред за приемане, отчитане и унищожаване на документи с фабрична номерация нормативна уредба uni -> "Икономиката е история на човешката трудова дейност." Маршал uni -> Програма за развитието на силите на мозъка. През 1978 г въз основа на разработените принципи той започва да обучава хора, а към 1980 г неговите лекции вече се ползват с колосален успех в цял свят Изтегляне 3.6 Mb. Сподели с приятели:
|