Лекции по семантика на езиците за програмиране
Изтегляне 3.6 Mb.
|
| глава на програмата,
1, …, k са термове от тип Nat или условни термове. Примерна програма R1: F (X), where F (X) = if X = 0 then 1 else F (X – 1) * X
F (X), where F (X) = F (X)
Навсякъде по-долу си мислим, че R е фиксирана и има вида от по-горе. Нека е функционален терм. Израз от вида c, където c е константа от типа на наричаме опростяване на в програмата R. Ще дефинираме правила, по които ще се извършва опростяването.
f (1, 2, …, n) c. Тук 1, …, n имат типове, които съответстват на типа на операцията f.
термове от тип Nat.
3V. (предаване по стойност) Нека 1, 2, …, са функционални термове, които са условни или от тип Nat, 1 i k. Нека 1 c1, 2 c2, …, , 1 i k. Нека i (X1/c1, X2/c2, …, / , , , …, ) c. Тогава (1, 2, …, ) c. 3N. (предаване по име) Нека 1, 2, …, са функционални термове, които са условни или от тип Nat, 1 i k. Нека i (X1/1, X2/2, …, / , , , …, ) c. Тогава (1, 2, …, ) c. Оттук нататък, ако типът на терма не е изрично отбелязан, ще считаме, че той е подбран така, че съответните дефиниции и твърдения да имат смисъл. Казваме, че опростяването c е изводимо по стойност в програмата R и отбелязваме R c, ако съществува крайна редица S0, S1, …, Sn от множества от опростявания, такава че:
Казваме, че опростяването c е изводимо по име в програмата R и отбелязваме R c, ако съществува крайна редица S0, S1, …, Sn от множества от опростявания, такава че:
И в двата случая числото n наричаме дължина на извода за опростяването c. Като пример ще покажем, че опростяването F (0) 1 е изводимо по стойност в примерната програма R1 от по-горе. S0 = S1 = { 0 0 } S2 = S1 { 0 = 0 tt } S3 = S2 { 1 1 } S4 = S3 { if 0 = 0 then 1 else F (0 - 1) * 0 1 } S5 = S4 { F (0) 1 } Редицата от опростявания S0, S1, S2, S3, S4, S5 има необходимите свойства R1 F (0) 1. Естествено, същото опростяване F (0) 1 е изводимо в R1 и по име, при това със същия извод, т.е. R1 F (0) 1. По-долу ще покажем, че всяко опростяване, което е изводимо по стойност е изводимо и по име и с пример ще покажем, че обратното не е вярно. Ще формулираме една лема, която по същество е преформулиране на дефинициите, така че няма да я доказваме. Лемата формулираме в два варианта - с предаване по стойност и с предаване по име. Лема (за извода по стойност): Нека R c с дължина на извода k.
Лема (за извода по име): Нека R c с дължина на извода k.
Лемата за извода означава, че изводът по стойност и по име на едно опростяване е детерминиран – към всеки терм е приложимо единствено правило за опростяване. С помощта на лемата за извода, ще покажем, че ако един терм има опростяване, то то е единствено. Твърдение (еднозначност на опростяването по стойност): Нека е функционален терм, c1 и c2 са константи и R c1 и R c2. Тогава c1 = c2. Доказателство: провеждаме пълна индукция по дължината на извода R c1. Нека R c1 с дължина на извода k и твърдението е изпълнено за изводи R c1 с дължини по-малки от k. Разглеждаме случаи в зависимост от вида на . Нека е константа, = d. Имаме R c1 и R c2. От лемата за извода получаваме, че c1 = d = c2. Нека = f (1, 2, …, n), където f е n-местна основна операция. Имаме R c1 с дължина на извода k. От лемата за извода съществуват константи а1, а2, …, аn, такива че R j aj, j = 1, 2, …, n с дължина на извода по-малка от k и f (a1, a2, …, an) = c1. Имаме R c2 с дължина на извода по-малка от k. От лемата за извода съществуват константи b1, b2, …, bn, такива че R j bj, j = 1, 2, …, n и f (b1, b2, …, bn) = c2. По индукционното предположение получаваме, че aj = bj за всяко j = 1, 2, …, n и тъй като f е функция, то c1 = c2. Нека = if then 1 else 2. Имаме R c1 с дължина на извода k. От лемата за извода R tt и R 1 c1 или R ff и R 2 c1, при това тези изводи са с дължина по-малка от k. Нека R tt и R 1 c1 с дължини на изводите по-малки от k. Имаме R c2. От лемата за извода R tt и R 1 c2 или R ff и R 2 c2. Ако допуснем, че R ff, то от индукционното предположение ще получим tt = ff, което е противоречие. Така R tt и R 1 c2. Сега отново от индукционното предположение получаваме c1 = c2. Случаят R ff и R 2 c1 се разглежда абсолютно аналогично. Нека = (1, 2, …, ). Имаме R c1 с дължина на извода k. От лемата за извода съществуват константи a1, a2, …, , такива че R j aj, j = 1, 2, …, ni с дължини на изводите по-малка от k и R i (X1/a1, X2/a2, …, / , F) c1 с дължина на извода по-малка от k. Имаме R c2. От лемата за извода съществуват константи b1, b2, …, , такива че R j bj, j = 1, 2, …, ni и R i (X1/b1, X2/b2, …, / , F) c2. От индукционното предположение, приложено за изводите R j aj, j = 1, 2, …, ni получаваме aj = bj за всяко j = 1, 2, …, n. При това положение, i (X1/a1, X2/a2, …, / , F) = i (X1/b1, X2/b2, …, / , F). Прилагаме индукционното предположение за извода
Твърдението е доказано. Твърдение (еднозначност на опростяването по име): Нека е функционален терм, c1 и c2 са константи и R c1 и R c2. Тогава c1 = c2. Доказателство: провеждаме пълна индукция по дължината на извода R c1. Нека R c1 с дължина на извода k и твърдението е изпълнено за изводи R c1 с дължини по-малки от k. Разглеждаме случаи в зависимост от вида на . Нека е константа, = d. Имаме R c1 и R c2. От лемата за извода получаваме, че c1 = d = c2. Нека = f (1, 2, …, n), където f е n-местна основна операция. Имаме R c1 с дължина на извода k. От лемата за извода съществуват константи а1, а2, …, аn, такива че R j aj, j = 1, 2, …, n с дължина на извода по-малка от k и f (a1, a2, …, an) = c1. Имаме R c2. От лемата за извода съществуват константи b1, b2, …, bn, такива че R j bj, j = 1, 2, …, n и f (b1, b2, …, bn) = c2. По индукционното предположение получаваме, че aj = bj за всяко j = 1, 2, …, n и тъй като f е функция, то c1 = c2. Нека = if then 1 else 2. Имаме R c1 с дължина на извода k. От лемата за извода R tt и R 1 c1 или R ff и
Нека R tt и R 1 c1 с дължини на изводите по-малки от k. Имаме R c2. От лемата за извода R tt и R 1 c2 или R ff и R 2 c2. Ако допуснем, че R ff, то от индукционното предположение ще получим tt = ff, което е противоречие. Така R tt и R 1 c2. Сега отново от индукционното предположение получаваме c1 = c2. Случаят R ff и R 2 c1 се разглежда абсолютно аналогично. Нека = (1, 2, …, ). Имаме R c1 с дължина на извода k. От лемата за извода R i (X1/1, X2/2, …, / , F) c1 с дължина на извода по-малка от k. Имаме R c2. От лемата за извода R i (X1/1, X2/2, …, / , F) c2. Прилагаме индукционното предположение за извода R i (X1/1, X2/2, …, / , F) c1 и получаваме c1 = c2. Твърдението е доказано. Да напомним, че R е програма от вида 0 (X1, …, Xn, , , …, ), where (X1, …, ) = i (X1, …, , , , …, ), i = 1, 2, …, k. Дефинираме функция OV (R) : Nn N, OV (R) (a1, a2, …, an) b R 0 (X1/a1, X2/a2, …, Xn/an, F) b. Функцията OV (R) наричаме операционна семантика на програмата R с предаване по стойност. Определението е коректно, т.е. OV (R) действително е функция, тъй като е в сила еднозначност на опростяването по стойност.
Функцията ON (R) наричаме операционна семантика на програмата R с предаване по име. Определението е коректно, т.е. ON (R) действително е функция, тъй като е в сила еднозначност на опростяването по име.
F (G (X), X), where F (X, Y) = if Y = 0 then 0 else X G (X) = G (X) Имаме !OV (R)(0), тъй като опростяването на терма F (G (0), 0) се свежда до опростяване на G (0), който очевидно няма опростяване. От друга страна ON (R)(0) 0. Действително, S0 = S1 = { 0 0 } S2 = S1 { 0 = 0 tt } S3 = S2 { if 0 = 0 then 0 else G (0) } S4 = S3 { F (G (0), 0) 0 } Така R F (G (0), 0) 0.
1, 2, …, n са функционални термове. Нека R 1 c1, R 2 c2, …, R n cn и R (Y1/c1, Y2/c2, …, Yn/cn, , , …, ) c. Тогава R (Y1/1, Y2/2, …, Yn/n, , , …, ) c. Доказателство: провеждаме индукция по дължината на извода R (Y/c, F) c. Нека R (Y/c, F) c с дължина на извода s и твърдението е изпълнено за изводи R (Y/c, F) c с дължина на извода по-малко от s. Разглеждаме случаи в зависимост от вида на . Нека е константа, = d. Имаме R (Y/c, F) c и от лемата за извода получаваме c = d. Имаме (Y/, F) = d = c R (Y/, F) c. Нека е променлива, = Yj, j { 1, 2, …, n}. Тогава (Y/c, F) = cj. Имаме R (Y/c, F) c и от лемата за извода cj = c. От друга страна, (Y/, F) = j и по условие R j cj. Така R (Y/, F) c. Нека е основна операция, = f (1, 2, …, l). Тогава (Y/c, F) = = f (1 (Y/c, F), 2 (Y/c, F), …, l (Y/c, F)). Имаме R (Y/c, F) c с дължина на извода s. От лемата за извода съществуват константи d1, d2, …, dl, такива че R j (Y/c, F) dj, j = 1, 2, …, l с дължина на извода по-малка от s и f (d1, d2, …, dl) = c. От индукционното предположение имаме R j (Y/, F) dj за всяко j = 1, 2, …, l. Освен това, (Y/, F) = f (1 (Y/, F), 2 (Y/, F), …, l (Y/, F)) и f (d1, d2, …, dl) = c. При това положение, R (Y/, F) c. Нека е условен терм, = if then 1 else 2. Тогава (Y/c, F) = = if (Y/c, F) then 1 (Y/c, F) else 2 (Y/c, F). Имаме R (Y/c, F) c с дължина на извода s. От лемата за извода R (Y/c, F) tt и
Нека R (Y/c, F) tt и R 1 (Y/c, F) c. От индукционното предположение получаваме R (Y/, F) tt и R 1 (Y/, F) c. Oт друга страна, (Y/, F) = if (Y/, F) then 1 (Y/, F) else 2 (Y/, F). Така R (Y/, F) c. Случаят R (Y/c, F) ff и R 2 (Y/c, F) c се разглежда абсолютно аналогично. Нека е обръщение към функция, = (1, 2, …, ), 1 i k. Тогава (Y/c, F) = (1 (Y/c), 2 (Y/c), …, (Y/c), F). Имаме R (Y/c, F) c с дължина на извода s. От лемата за извода R i (X1/1 (Y/c), X2/2 (Y/c), …, / (Y/c), F) c с дължина на извода по-малка от s. Имаме i (X1/1 (Y/c), X2/2 (Y/c), …, , / (Y/c), F) = i (X1/1, X2/2, …, / ) (Y/c, F). От индукционното предположение получаваме, че
Каталог: uni uni -> Отчет за ибсф ра, ибсф ksf и ибсф 33 за средствата по набирателните сметки uni -> Условия и ред за приемане, отчитане и унищожаване на документи с фабрична номерация нормативна уредба uni -> "Икономиката е история на човешката трудова дейност." Маршал uni -> Програма за развитието на силите на мозъка. През 1978 г въз основа на разработените принципи той започва да обучава хора, а към 1980 г неговите лекции вече се ползват с колосален успех в цял свят Изтегляне 3.6 Mb. Сподели с приятели:
|