Программирование
<<  Функциональное программирование Функциональное программирование  >>
Функциональное программирование
Функциональное программирование
Лекция 23
Лекция 23
Доказательство программ
Доказательство программ
Формальное доказательство
Формальное доказательство
Еще пример
Еще пример
Более сложный пример
Более сложный пример
Продолжение
Продолжение
Продолжение
Продолжение
Почему в ФП просто доказывать свойства программ
Почему в ФП просто доказывать свойства программ
Пределы верификации
Пределы верификации
Неразрешимость проблемы самоприменимости
Неразрешимость проблемы самоприменимости
Доказательство
Доказательство
Следствия
Следствия
Вопросы
Вопросы

Презентация: «Функциональное программирование». Автор: Митя;Лена. Файл: «Функциональное программирование.ppt». Размер zip-архива: 2531 КБ.

Функциональное программирование

содержание презентации «Функциональное программирование.ppt»
СлайдТекст
1 Функциональное программирование

Функциональное программирование

Факультет инноваций и высоких технологий Московский физико-технический институт

2 Лекция 23

Лекция 23

Доказательство свойств программ

2

3 Доказательство программ

Доказательство программ

Полуформальное доказательство По индукции Для n=1: ||fact n||= ||if 1=1 then 1 else 1*fact(0)|| = 1 = n! Для n>1: ||fact n||= ||if n=1 then 1 else n*fact(n-1)|| = ||n*fact(n-1)|| = n*||fact(n-1)|| = n*(n-1)!=n! Формальное доказательство || letrec fact = fun x -> if x=1 then 1 else x*fact(x-1) || = ?n.n!

let rec fact n = if n = 1 then 1 else n*fact(n-1)

Индуктивное предположение

3

4 Формальное доказательство

Формальное доказательство

Семантика fact: f0=? fn=?x.if x=1 then 1 else x*fn-1(x-1) fact = ?ifi Доказательство: fn(x) = x!, x?n; f(x) = ?, x>n fact(n)= (?ifi)(n)= ?i(fi(n))=?i=0..n(fi(n))=fn(n)=n!

4

5 Еще пример

Еще пример

Покажем app x (app y z) = app (app x y) z Индукция по длине x x=[]: app [] (app y z) = app y z app (app [] y) z = app y z Для x = h::t app (h::t) (app y z) = h::app t (app y z) = h::(app(t y) z) app (app h::t y) z = app(h::app t y) z =h::(app(t y) z)

let rec app a b = match a with [] -> b | h::t -> h::(app t b);;

5

6 Более сложный пример

Более сложный пример

Докажем, что rev(rev l) = l

Лемма 1: app l [] = l l = [] app [] [] = [] l = h::t app h::t [] = h::(app t []) = h::t = l

let rec rev = function [] -> [] | h::t -> app (rev t) [h];;

6

7 Продолжение

Продолжение

Лемма 2: rev(app a b) = app (rev b) (rev a) a=[] rev(app [] b) = rev b app (rev b) (rev []) = app (rev b) [] = rev b a=h::t rev(app h::t b)=rev(h::(app t b))=app(rev (app t b))[h]= app(app (rev b)(rev t))[h]=app(rev b)(app (rev t)[h])= app(rev b)(rev h::t)=app(rev b)(rev a)

7

8 Продолжение

Продолжение

rev(rev l) = l l=[]: rev(rev []) = rev [] = [] l=h::t rev(rev h::t) = rev(app (rev t) [h]) = app(rev [h])(rev (rev t)) = app (rev h::[]) t = app(app (rev []) [h]) t = app (app [] [h]) t = app [h] t = app h::[] t = h::app([] t) = h::t = l

8

9 Почему в ФП просто доказывать свойства программ

Почему в ФП просто доказывать свойства программ

Отсутствие побочных эффектов в функциях Денотат функций – математическая функция

9

10 Пределы верификации

Пределы верификации

Ограниченность верификации показывается теоремой Гёделя о неполноте: Любая формальная система, содержащая формальную арифметику, будет неполна, т.е. будут существовать истинные утверждения, невыводимые в этой теории Применительно к верификации: Проблема остановки Проблема самоприменимости

10

11 Неразрешимость проблемы самоприменимости

Неразрешимость проблемы самоприменимости

ФП P применима к входным данным D, если выражение PD редуцируется к НФ за конечное число шагов ФП P называется самоприменимой, если она применима к самой себе как входным данным Задача: построить программу T : TP ? t, если Р – самоприменима TP ? f, если Р – не самоприменима

11

12 Доказательство

Доказательство

Построим функцию F = ?x.cond (T x) ((?x.x x) (?x.x x)) (t) Тогда F применима к несамоприменимым функциям и наоборот Пусть F – самоприменима, тогда FF должно не редуцироваться, что противоречит определению самоприменимости Пусть F – не самоприменима, тогда FF – не редуцируется, что противоречит построению

12

13 Следствия

Следствия

Невозможно решить проблему остановки: По произвольной функции и входным данным определить, произойдет ли зацикливание или нет Однако возможно решать проблему в некотором приближении: Анализ типовых случаев зацикливания Зацикливание за первые n шагов

13

14 Вопросы

Вопросы

14

«Функциональное программирование»
http://900igr.net/prezentacija/informatika/funktsionalnoe-programmirovanie-246428.html
cсылка на страницу

Программирование

31 презентация о программировании
Урок

Информатика

130 тем
Слайды
900igr.net > Презентации по информатике > Программирование > Функциональное программирование