Fun with Formal Program Semantics (О формальной семантике программ – просто) Шилов Николай Вячеславович Computer Science клуб - Екатеринбург Март 2012. - презентация

1 Fun with Formal Program Semantics (О формальной семантике программ – просто) Шилов Николай Вячеславович Computer Science клуб - Екатеринбург Март 2012

2 Тема 1: Понятие об операционной, денотационной, аксиоматической и семантике второго порядка (на примере игрушечного эзотерического языка TEL)

3 Синтаксис, семантика, прагматика Язык программирования – это любой искусственный язык для организации автоматической обработки данных на вычислительной машине. Всякий (искусственный или естественный) язык обычно характеризуются своим синтаксисом, семантикой и прагматикой Шилов Николай Вячеславович Всего слайдов 66 3

4 Синтаксис, семантика, прагматика Синтаксис – это правописание языка. Семантика – это правила придания смысла синтаксически правильным выражениям этого языка. Прагматика – это практика, методы, способы, пути использования грамматически правильных осмысленных (т.е. имеющих семантику) выражений языка Шилов Николай Вячеславович Всего слайдов 66 4

5 «Пляшущие человечки» Артура Конана Дойля Очередное дело Шерлока Холмса закручивается вокруг пляшущих человечков – с первого взгляда, невинного детского рисунка. Но в итоге пляшущие человечки оказались шифром простой замены с флагами – разделителями слов Шилов Николай Вячеславович Всего слайдов 66 5

6 «Пляшущие человечки» Артура Конана Дойля Синтаксис – как в естественном языке с заменой букв на «пляшущих человечков». Семантика – в соответствии с семантикой естественного языка (после обратной замены). Прагматика – шифр одной из чикагских преступных группировок. Упражнение #1: расшифруйте следующую запись Шилов Николай Вячеславович Всего слайдов 66 6

7 Семантика естественного языка Глокая куздра штеко будланула бокра и курдячит бокрёнка искусственная фраза на основе русского языка, в которой все корневые морфемы заменены на бессмысленные сочетания звуков. Фраза создана академиком А. А. Потебня для иллюстрации того, что многие семантические признаки слова можно понять из его морфологии. Пример использовался на вводных лекциях к курсу «Основы языкознания» Шилов Николай Вячеславович Всего слайдов 66 7

8 Семантика естественного языка Общий смысл фразы понятен: – некоторое, определенным образом характеризуемое, существо женского пола – что-то сделало определённым образом с другим существом мужского пола, – а затем начала (и продолжает до настоящего момента) делать что-то другое с его детёнышем (или более мелким представителем того же вида) Шилов Николай Вячеславович Всего слайдов 66 8

9 Семантические парадоксы Фразы русского языка, записанные с использованием только 33 символом клавиатуры, состоящие из не более чем 73 символов, могут закодировать (натуральные) числа от 1 до Спрашивается, какое число кодирует следующая фраза: Эта фраза кодирует число на единицу большее, чем 33 в 73-ей степени Шилов Николай Вячеславович Всего слайдов 66 9

10 Игрушечный Эзотерический Язык TEL (Toy Exoteric Language) TEL не является языком программирования, т.к. не предназначен для обработки данных на компьютере. Он предназначен (это его прагматика) для первоначального знакомства с понятиями операционная, денотационная и аксиоматическая семантика Шилов Николай Вячеславович Всего слайдов 66 10

11 Игрушечный Эзотерический Язык TEL (Toy Exoteric Language) Синтаксис языка TEL чрезвычайно похож на синтаксис языка программирования, его проще объяснить на следующем простом примере правильного выражения (которое мы обозначим sample для удобства дальнейшего использования): if z

12 Игрушечный Эзотерический Язык TEL: неформальный синтаксис Правильные выражения языка TEL – это как бы «программы», построенные из переменных, арифметических выражений, логических выражений, операторов присваивания при помощи разделителя «;», условий «if-then-else» и циклов «while-do» Шилов Николай Вячеславович Всего слайдов 66 12

13 Игрушечный Эзотерический Язык TEL: формальный синтаксис Шилов Николай Вячеславович Всего слайдов BNF-определение синтаксиса TEL

14 Игрушечный Эзотерический Язык TEL: неформальная семантика Так как правильные выражения языка выглядят как программы, то их можно изображать графически в виде блок-схем. Всякая блок-схема – это граф, вершины которого – операторы присваивания и логические выражения Шилов Николай Вячеславович Всего слайдов 66 14

15 Игрушечный Эзотерический Язык TEL: блок-схема для sample Шилов Николай Вячеславович Всего слайдов начало z

16 Игрушечный Эзотерический Язык TEL: неформальная семантика Договоримся измерять «длину» пути по блок- схеме количеством операторов присваивания на этом пути (т.е. логические выражения не идут в счёт). Тогда «смыслом» каждого правильного выражения является целое число, равное «длине» кратчайшего пути по графу блок-схемы «программы» от начала до конца Шилов Николай Вячеславович Всего слайдов 66 16

17 Игрушечный Эзотерический Язык TEL: неформальная семантика В частности, семантика выражения sample есть число 1. if z

18 Операционная семантика: механический арифмометр Операционная семантика – это подход к определению семантики через работу «механического устройства», умеющего выполнять определённый набор действий (операций), переходя из состояния в состояние Шилов Николай Вячеславович Всего слайдов 66 18

19 Операционная семантика: механический арифмометр Обычно операционная семантика языка задаётся описанием метода трансляции правильных выражений языка в соответствующую последовательность действий такого устройства, а семантика каждого правильного выражения определяется путём выполнения соответствующей последовательности действий Шилов Николай Вячеславович Всего слайдов 66 19

20 Игрушечный Эзотерический Язык TEL: операционная семантика Для TEL в качестве механического устройства примем «арифмометр», способный складывать натуральные числа и выбирать минимум из двух натуральных чисел Шилов Николай Вячеславович Всего слайдов 66 20

21 Игрушечный Эзотерический Язык TEL: операционная семантика Определим алгоритм трансляции F рекурсивно следующим образом: – F(x:=t) = 1 для любо присваивания; – F(β;γ) = F(β) + F(γ); – F(if ζ then β else γ) = min{F(β), F(γ)}; – F(while ζ do β) = 0. Такой метод трансляции языка сопоставляет каждому правильному выражению TEL арифметическое выражение, состоящее из 0, 1 и операций «+» и «min» Шилов Николай Вячеславович Всего слайдов 66 21

22 Игрушечный Эзотерический Язык TEL: операционная семантика Например, трансляция sample и соответствующее арифметическое выражение получаются следующим образом: F(if z

23 Игрушечный Эзотерический Язык TEL: операционная семантика = min{1, 1 + F(y:=0) + F(while yz do(y:=y+2 x+1;x:=x+1);x:=x1)} = = min{1, F(while yz do(y:=y+2 x+1;x:=x+1)) + + F(x:=x1)} = = min{1, }. Следовательно, операционная семантика правильного выражения есть 1, что получается, если выполнить все эти действия на нашем «арифмометре» Шилов Николай Вячеславович Всего слайдов 66 23

24 Денотационная семантика: алгебра для вычислений Алгебра – это множество элементов и операций над ними. Например, множество натуральных чисел N с нульместными операциями (константами) 0 и 1, бинарными операциями «+» и «», – это алгебра. Тоже множество N, но с одной константой 0, унарной (одноместной) операцией «+1» и бинарной операцией «min» – это уже другая алгебра, т.к. использует другой набор операций Шилов Николай Вячеславович Всего слайдов 66 24

25 Денотационная семантика: алгебра для вычислений Денотационная семантика – это определение семантики языка в терминах подходящей алгебры путём согласованного сопоставления каждому правильному выражению языка – элемента алгебры, каждому конструктору правильных выражений – алгебраической операции Шилов Николай Вячеславович Всего слайдов 66 25

26 Денотационная семантика: алгебра для вычислений Часто сопоставляющую функцию обозначают посредством двойных квадратных скобок «[[…]]»; Элемент алгебры или операция алгебры, сопоставленные посредством функции [[…]] правильному выражению или конструктору выражений, называют его денотацией Шилов Николай Вячеславович Всего слайдов 66 26

27 Игрушечный Эзотерический Язык TEL: денотационная семантика Выберем в качестве носителя алгебру натуральных чисел N с константами 0, 1 и бинарными операциями «+» и «min». Функцию [[ ]] определим следующим образом: – [[x:=t]] = 1 для любого присваивания; – [[;]] = +, [[ifthen...else...]]=min, [[while–do...]]=0; – [[constr(α, β)]] = [[constr]]([[α]], [[β]]) для любого конструктора из «;», «ifthen...else...», «whiledo...» Шилов Николай Вячеславович Всего слайдов 66 27

28 Игрушечный Эзотерический Язык TEL: денотационная семантика Определение сопоставляет заведомо согласованные денотации правильным выражениям и конструкторам выражений, т.к. определяется композиционно (см. пункт определения для const) Шилов Николай Вячеславович Всего слайдов 66 28

29 Игрушечный Эзотерический Язык TEL: денотационная семантика В частности, для sample имеем: [[if z

30 Игрушечный Эзотерический Язык TEL: денотационная семантика = min{1, 1 + [[;]]([[y:= 0]], [[while yz do (y:= y+2*x+1 ; x:= x+1) ; x:= x-1]])} = = min{ 1, 1 + (1 + [[;]]( [[while yz do (y:= y+2*x+1 ; x:= x+1)]], [[x:= x-1]]))} = = min{ 1, 1 + (1 + (0 + 1))} = Шилов Николай Вячеславович Всего слайдов 66 30

31 Игрушечный Эзотерический Язык TEL: денотационная семантика То, что операционная и денотационная семантики sample совпали, не случайно: Утверждение 1: F(α) = [[α]] для любого правильного выражения α языка TEL. Доказательство (в качестве упражнения #2) – индукция по синтаксической структуре правильного выражения α. Таким образом, операционная и денотационная семантики TEL хорошо согласованы друг с другом Шилов Николай Вячеславович Всего слайдов 66 31

32 Аксиоматическая семантика: синтаксически управляемое доказательство Аксиоматическая семантика – это исчисление для вывода («доказательства») новых утверждений («теорем») по правилам вывода из заранее определённых аксиом («фактов») Шилов Николай Вячеславович Всего слайдов 66 32

33 Игрушечный Эзотерический Язык TEL: аксиоматическая семантика Аксиоматическая семантика языка TEL имеет дело с утверждениями вида m α n где – m – натуральное число, – α – правильное выражение языка TEL, – n – или натуральное число такое, что m n, или символ бесконечности «» Шилов Николай Вячеславович Всего слайдов 66 33

34 Игрушечный Эзотерический Язык TEL: аксиоматическая семантика Шилов Николай Вячеславович Всего слайдов 66 34

35 Игрушечный Эзотерический Язык TEL: аксиоматическая семантика Шилов Николай Вячеславович Всего слайдов if z

36 Аксиоматическая семантика: истинность vs. доказуемость, надёжность vs. полнота Будем говорить, что утверждение mαn верно (истинно), если m[[α]]n. Говорят, что аксиоматическая семантика надёжна, если любое доказуемое утверждение верно; наоборот, говорят что аксиоматическая семантика полна, если всякое верное утверждение доказуемо. Говорят, что аксиоматическая семантика непротиворечива, если … (закончить лпределение – упражнение #3) Шилов Николай Вячеславович Всего слайдов 66 36

37 Игрушечный Эзотерический Язык TEL: надёжность и полнота аксиоматической семантики Пример истинного и доказуемого утверждения: 1 sample Шилов Николай Вячеславович Всего слайдов 66 37

38 Игрушечный Эзотерический Язык TEL: надёжность и полнота аксиоматической семантики Такое совпадение неслучайно. Утверждение 2: Аксиоматическая семантика игрушечного языка TEL надёжна и полна. Доказательство надёжности – индукцией по высоте дерева вывода (в качестве упражнения #4), а доказательство полноты – индукцией по структуре правильного выражения (в качестве упражнения #5) Шилов Николай Вячеславович Всего слайдов 66 38

39 Семантика второго порядка: преобразователь предикатов Предикат (одноместный предикат) – это множество однородных значений. Если эти значения одного «типа» D, то множество всех предикатов – это множество 2 D всех подмножеств D. Преобразователь предикатов – это произвольная функция F:2 D 2 D, т.е. функция, которая преобразует «входной» S D предикат – в «выходной» предикат F(S) D Шилов Николай Вячеславович Всего слайдов 66 39

40 математическое отступление о порядке элементов, множеств, функций и теорий Пусть D – некоторое множество («область»). Элементы D и векторы с компонентами из D (т.е. элементы пространства D1= k1 D k ) называют элементами первого порядка над D. Подмножества D1 (и, в частности, все функции из D p в D q ) называются множествами (предикатами) первого порядка над D (функциями соотвественно) Шилов Николай Вячеславович Всего слайдов 66 40

41 математическое отступление о порядке элементов, множеств, функций и теорий Всякая «теория», изучающая или описывающая свойства элементов первого порядка, называется теорией первого порядка области D Шилов Николай Вячеславович Всего слайдов 66 41

42 математическое отступление о порядке элементов, множеств, функций и теорий Подмножества D1 и векторы, компонентами которых являются подмножества D1 (т.е. элементы пространства D2= k1 (2 D1 ) k ), называют элементами второго порядка над D. В частности, предикаты и функции первого порядка являются элементами второго порядка над D Шилов Николай Вячеславович Всего слайдов 66 42

43 математическое отступление о порядке элементов, множеств, функций и теорий Подмножества D2 и функции из D2в D2 называются множествами (предикатами) второго порядка и функциями второго порядка (функционалами) над D. Всякая «теория», изучающая или описывающая свойства элементов второго порядка, называется теорией второго порядка области D Шилов Николай Вячеславович Всего слайдов 66 43

44 математическое отступление о порядке элементов, множеств, функций и теорий Пусть для некоторого n>0 уже определены множество Dn, элементы, множества и функции n- ого порядка над областью D. Подмножества Dn и векторы, компонентами которых являются подмножества Dn (т.е. элементы пространства D(n+1)= k1 (2 Dn ) k ), называют элементами (n+1)-ого порядка над D. В частности, предикаты и функции n-ого порядка являются элементами (n+1)-ого порядка над D Шилов Николай Вячеславович Всего слайдов 66 44

45 математическое отступление о порядке элементов, множеств, функций и теорий Подмножества D(n+1) и функции из D(n+1) в D(n+1) называются множествами (предикатами) и функциями (n+1)-ого порядка над D. Всякая «теория», изучающая или описывающая свойства элементов (n+1)-ого порядка, называется теорией (n+1)-ого порядка области D Шилов Николай Вячеславович Всего слайдов 66 45

46 математическое отступление о порядке элементов, множеств, функций и теорий Всякая «теория», изучающая или описывающая свойства элементов любого порядка, называется теорией высшего порядка области D. Упражнение #6: Что такое элементы, множества, функции и теория нулевого порядка области D? Шилов Николай Вячеславович Всего слайдов 66 46

47 математическое отступление о школьной алгебре, математическом и функциональном анализе Рассмотрим с точки зрения классификации теорий по порядкам такие учебные предметы, как: – элементарная алгебра, изучаемая в старших классах средней школы; – математический анализ, изучаемый на первых курсах вузов; – функциональный анализ, который изучается на 3 – 4 курсах на факультетах физико- математического профиля Шилов Николай Вячеславович Всего слайдов 66 47

48 математическое отступление о школьной алгебре, математическом и функциональном анализе Элементарная алгебра занимается решением (систем) уравнений и неравенств в вещественных числах. Эти уравнения заданы многочленами с параметрическими коэффициентами, которые обозначают опять же вещественные числа. Например, типичными задачами элементарной алгебры является нахождение всех вещественных корней квадратного уравнения с вещественными коэффициентами a·x 2 + b·x + c = Шилов Николай Вячеславович Всего слайдов 66 48

49 математическое отступление о школьной алгебре, математическом и функциональном анализе Например, в школьном курсе доказывается, что для любых вещественных значений коэффициентов уравнение a·x 2 + b·x + c = 0 имеет решение в вещественных числах тогда и только тогда, когда b 2 - 4·a·c ³ 0, т. е., что следующее предложение принадлежит теории первого порядка поля вещественных чисел: a b c( b 2 -4·a·c0 x(a·x 2 +b·x+c=0) ) Шилов Николай Вячеславович Всего слайдов 66 49

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

51 математическое отступление о школьной алгебре, математическом и функциональном анализе Математический анализ занимается изучением свойств непрерывных и дифференцируемых функций вещественной переменной. Примером может служить теорема о промежуточном значении непрерывной функции на замкнутом отрезке, авторство которой приписывается К.Т.В. Веерштрассу, Б. Больцано и О.Л. Коши Шилов Николай Вячеславович Всего слайдов 66 51

52 математическое отступление о школьной алгебре, математическом и функциональном анализе Для любой функции f непрерывной на отрезке вещественных чисел [a..b], для любого числа y [f(a)..f(b)] найдётся такое число x [a..b], что f(x)=y Шилов Николай Вячеславович Всего слайдов 66 52

53 математическое отступление о школьной алгебре, математическом и функциональном анализе Вспомним, что всякая вещественная функция – это просто множество пар чисел. Поэтому теорема может быть сформулирована в терминах логики второго порядка над полем вещественных чисел следующим образом: f 2 R R a R b R c R d R y R (C(f,a,b) & (a,c) f & (b,d) f & cyd x R( axb & (x,y) f)), где C – трёхместное отношение «быть непрерывной вещественной функцией на отрезке» Шилов Николай Вячеславович Всего слайдов 66 53

54 математическое отступление о школьной алгебре, математическом и функциональном анализе Подобным образом курс математического анализа формализуем как теория второго порядка поля вещественных чисел. Упражнение #7: Определите на языке логики второго порядка над полем вещественных чисел использованное трёхместное отношение «быть непрерывной вещественной функцией на отрезке» Шилов Николай Вячеславович Всего слайдов 66 54

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

56 математическое отступление о школьной алгебре, математическом и функциональном анализе Поэтому часть функционального анализа, изучающая теорию линейных операторов на функциях вещественной переменной, может быть формализована как теория третьего порядка поля вещественных чисел. (Поэтому её и изучают на третьем курсе;-) Шилов Николай Вячеславович Всего слайдов 66 56

57 Почему «семантика второго порядка»? Семантика второго порядка – это сопоставление каждому синтаксически правильному выражению некоторого преобразователя предикатов первого порядка, т.е. функции F:2 D 2 D, которая преобразует «входной» S D предикат – в «выходной» предикат F(S) D Шилов Николай Вячеславович Всего слайдов 66 57

58 Игрушечный Эзотерический Язык TEL: семантика второго порядка Для любого выражения α языка TEL определим преобразователь предикатов PT α на натуральных числах N следующим образом: для любого множества натуральных чисел S, PT α (S) – это множество таких натуральных чисел n N, что для любого выражения β языка TEL, если [[β]]=n, то [[β ; α]] S Шилов Николай Вячеславович Всего слайдов 66 58

59 Игрушечный Эзотерический Язык TEL: семантика второго порядка Утверждение 3: Для любого выражения α языка TEL, для любого множества натуральных чисел S, PT α (S) = S -- [[α]], где операция «--» – это поэлементное вычитание, которое не выводит из множества положительных чисел. Доказательство остаётся в качестве упражнения # Шилов Николай Вячеславович Всего слайдов 66 59

60 Игрушечный Эзотерический Язык TEL: семантика второго порядка Хорошие свойства PT: – PT x:=t (S) = {n > 0 : (n+1) S}, – PT (α) (S) = PT α (S), – PT β;α (S) = PT β (PT α (S)), – Pt while-do (S) = S Упражнение #9: Как выразить Pt if-then β else α (S) через PT β (S) и PT α (S)? Шилов Николай Вячеславович Всего слайдов 66 60

61 О -нотации (ещё одно математическое отступление) Наряду с этой общеизвестной нотацией для функций сложилась и другая нотация, широко используемая в математической логике и теории программирования – т.н. -нотация (читается «лямбда-нотация») Шилов Николай Вячеславович Всего слайдов 66 61

62 О -нотации (ещё одно математическое отступление) Суть -нотации поясним на примере: «2 y + 3, где y R» – это число (но не функция), значение которого зависит от значения числового параметра y по закону 2 y + 3; « y R. (2 y + 3)» - это функция (без имени), где y объявлен переменной посредством спецификатора « » (а не параметром с каким-то значением), которая каждому числу r R сопоставляет число (2 r + 3) R; Шилов Николай Вячеславович Всего слайдов 66 62

63 О -нотации (ещё одно математическое отступление) «f = y R. (2 y + 3)» - это высказывание о том, что функция f совпадает (как множество) с функцией y R. (2 y + 3); «f y R. (2 y + 3)» - это объявление о том, что функция y R. (2 y + 3) получает имя «f» Шилов Николай Вячеславович Всего слайдов 66 63

64 О -нотации (ещё одно математическое отступление) Пусть g m N. ( n N. ( y R. (m y + n))). Функция g - это функция от одной переменной m, которая «пробегает» натуральные числа. Функция g сопоставляет каждому натуральному числу M функцию h M = ( n N. ( y R. (M y + n)), в частности, h 2 = ( n N. ( y R. (2 y + n)) Шилов Николай Вячеславович Всего слайдов 66 64

65 О -нотации (ещё одно математическое отступление) Функция h M – тоже функция одной переменной n, которая тоже «пробегает» натуральные числа и сопоставляет каждому натуральному числу N функцию f M,N = ( y R. (M y + N), в частности f 2,3 – это уже знакомая нам функция f = (2 y + 3) Шилов Николай Вячеславович Всего слайдов 66 65

66 Игрушечный Эзотерический Язык TEL: семантика второго порядка С использованием -нотации Утверждение 3 может быть переформулировано следующим образом: PT = α TEL. S N. (S -- [[α]]), где – PT – семантика второго порядка для игрушечного эзотерического языка TEL, – а «--» – это поэлементное вычитание, которое не выводит из множества положительных чисел. (Проверка остается в качестве упражнения #9.) Шилов Николай Вячеславович Всего слайдов 66 66