Лекция "Основные подходы к синтезу программ" Содержание лекции Реализационная семантика формул



страница1/4
Дата03.12.2012
Размер0.58 Mb.
ТипЛекция
  1   2   3   4
А.П.Бельтюков
Синтез программ. Сентябрь-декабрь 2007.

Дедуктивное программирование.

Факультативный курс для студентов

4курса специальности

”Прикладная математика И информатика”
file://belt/_/edu/wp/sp/sp_7.txt

version:79f.g.m.a2з.3.6.c.k.s.bh.n.o.c1

http://csds.udsu.ru/~belt/sp_7.txt
Общие характеристики курса
Лекций- 54 часа,

занятий- 36 часов.

Материалы лекций и занятий
Примечания:

- названия тем лекций уточняются.

Лекция 1. "Основные подходы к синтезу программ"
Содержание лекции
Реализационная семантика формул.

Приложение 1 к лекции 1. "Синтаксис традиционных предикатных логических

формул без отрицаний (простейший язык без функций)"
Далее "::=", "|", "..." - метасимволы с "традиционным" смыслом.
Определяется понятие формулы некоторого логико-предметного языка

без отрицаний (и эквивалентностей - они избыточны, отрицания

моделируются импликациями вида (Ф => Error), где Error - некоторая

формула, реализациями которой могут быть только разве лишь

так называемые "сообщения об ошибках в интерпретации", которые

иногда могут заменять собой реальное решение задачи, если

мы пытаемся решить эту задачу в неподходящих условиях).
Считается, что зафиксированы непересекающиеся класс

<имя> и конечный список <предикат>.

Цепочки этих классов не содержат

символов: "(", ",", ")", "&", "v", "=>", "A", "E".
Бесконтекстный синтаксис формул:
<формула> ::= <предикат>(<имя>,...,<имя>)|

(<формула> <связка> <формула>)|<квантор> <имя> <формула>
<связка> ::= & | v | =>
<квантор> ::= A | E

Приложение 2 к лекции 1. "Правила построения реализаций"
Для построения реализаций формул следует зафиксировать:
1) предметную область U - класс конструктивных объектов,

то есть класс "исходных" предметов, задаваемых конечными цепочками символов

класса <имя> - <имя предмета>; "x:U" будет означать, что x - имя предмета.
2) для каждой формулы вида

<предикат>(<имя предмета>,...,<имя предмета>)

- класс так называемых "первичных реализаций" - объектов, задаваемых

цепочками символов, не содержащих (неуравновешенных) круглых скобок

и запятых (вне скобок); этот класс будем обозначать через

R(<предикат>(<имя предмета>,...,<имя предмета>));

он может быть и пустым для некоторых формул такого вида;
3) некоторый вид алгоритмов L (например, Машины Тьюринга),

программы которых также кодируются цепочками символов, не

содержащих (неуравновешенных) круглых скобок

и запятых (вне скобок); p:L будет означать, что p - код такая

программа для данного вида алгоритмов.

Определим в этих условиях классы реализаций для других формул

по следующим правилам:
R((C & B)) = {(c,b) | c:C, b:B},

"a:A" означает, что a - элемент R(A)...,

R((C v B)) = {(0,c) | c:C} U {(1,b)|b:B},

здесь "U" - объединение,

R((C => B)) = {p:L | Ax (с:C => !p(с) & p(с):B)},

"!p(x)" означает, что программа p применима к цепочке x,

справа логические связки и кванторы понимаются в традиционном

"классическом" смысле;

R(Ex B(x)) = {(c,b) | c:U, b:B(c)},

R(Ax B(x)) = {p:L | Ax (с:U => !p(с) & p(с):B(c))}.

Лекция 2. "Основы дедуктивного синтеза алгоритмов"
Контрольные вопросы к лекции 1
Пусть U={a,b}

A(a)={1} A(b)=0 B(a)={2,3}, B(b)={4,5}

1. R(Ex(A(x)&B(x)))=?

2. R(Ey(A(y)\/B(y)))=?

Содержание лекции 2
Конструктивные доказательства и их реализационная семантика.

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

Удобный вариант ламбда-языка для записи программ,

выраженных традиционными конструктивными доказательствами.

Переменные. Структуры данных. Исходные данные. Пары.

Ламбда-конструкция. Вызов. Встроенные операции (left,right,con).

Выражение. Присваивание перед выражением.

Равенство. Константы 0 и 1. Условное выражение if E1=E2 then S1 else S2.

Запись традиционных правил вывода в виде программных конструкций.

Приложение 1 к лекции 2. "Синтаксис доказательств"
[планируется добавить]
Пример
Доказательство (сокращённо):

A1 ]Ax(T(x)=>Ez(B(z)&C(x,z))

A2 ]AxAy(B(x)&B(y)=>C(x,y))

A3 ]AxAy(C(x,y)=>C(y,x))

A4 ]AxAyAz(C(x,y)&C(y,z)=>C(x,z))

*x

*y

0 ]T(x)&T(y)

1 |T(x)

2 |T(y)

3 |Ez(B(z)&C(x,z) A1(x,1)

|c 3

4 |B(c) "

5 |C(x,c) "

6 |Ez(B(z)&C(y,z) A1(y,2)

|d 6

7 |B(d) "

8 |C(y,d) "

9 |C(c,d) A2(c,d,4,7)

10 |C(d,y) A3(y,d,8)

11 |C(x,d) A4(x,c,d,5,9)

12 |C(x,y) A4(x,d,y,11,10)

13 (Ax(T(x)=>Ez(B(z)&C(x,z))

&AxAy(B(x)&B(y)=>C(x,y))

&AxAy(C(x,y)=>C(y,x))

&AxAyAz(C(x,y)&C(y,z)=>C(x,z))

=>AxAy(T(x)&T(y)=>C(x,y))
Приложение 2 к лекции 2. "Правила вывода"
[планируется добавить]

Приложение 3 к лекции 2. "Синтаксис языка для записи программ,

извлекаемых из доказательств"
[планируется добавить]
Пример
алгоритм:
lambda(A1)

lambda(A2)

lambda(A3)

lambda(A4)

lambda(x)

lambda(y)

lambda(f0)

(f1:=left(f0);

f2:=right(f0)

f3a:=A1(x);f3:=f3a(f1);

c:=left(f3);

f4a:=right(f3);f4:=left(f4a);

f5:=right(f4a);

f6a:=A1(y);f6:=f6a(f2);

d:=left(f6);

f7a:=right(f6);f7:=left(f7a);

f8:=right(f7a); f9a:=A2(c);

f9b:=f9a(d);f9:=f9b(con(f4,f7));

f10a:=A3(y);f10b:=f10a(d);f10:=f10b(f8);

f11:=A4(x)(c)(d)(con(f5,f9)); сокращённо

A4(x)(d)(y)(con(f11,f10))) ""

Лекция 3. Логические основы дедуктивного синтеза программ
Соответствие между конструкциями доказательств и конструкциями программ.

Основы языка постановок задач - языка спецификаций,

специализированного логического языка.

Простейший язык программирования, предназначенный для дедуктивного

построения программ по спецификациям.

Приложение 1 к лекции 3. "Синтаксис языка доказательств с

выполняемыми конструкциями"
[планируется добавить]
Пример
Доказательство (сокращённо): алгоритм:

A1 ]Ax(T(x)=>Ez(B(z)&C(x,z)) lambda(A1)

A2 ]AxAy(B(x)&B(y)=>C(x,y)) lambda(A2)

A3 ]AxAy(C(x,y)=>C(y,x)) lambda(A3)

A4 ]AxAyAz(C(x,y)&C(y,z)=>C(x,z)) lambda(A4)

*x lambda(x)

*y lambda(y)

0 ]T(x)&T(y) lambda(f0)

1 |T(x) (f1:=left(f0);

2 |T(y) f2:=right(f0)

3 |Ez(B(z)&C(x,z) A1(x,1) f3a:=A1(x);f3:=f3a(f1);

|c 3 c:=left(f3);

4 |B(c) " f4a:=right(f3);f4:=left(f4a);

5 |C(x,c) " f5:=right(f4a);

6 |Ez(B(z)&C(y,z) A1(y,2) f6a:=A1(y);f6:=f6a(f2);

|d 6 d:=left(f6);

7 |B(d) " f7a:=right(f6);f7:=left(f7a);

8 |C(y,d) " f8:=right(f7a); f9a:=A2(c);

9 |C(c,d) A2(c,d,4,7) f9b:=f9a(d);f9:=f9b(con(f4,f7));

10 |C(d,y) A3(y,d,8) f10a:=A3(y);f10b:=f10a(d);f10:=f10b(f8);

11 |C(x,d) A4(x,c,d,5,9) f11:=A4(x)(c)(d)(con(f5,f9)); сокращённо

12 |C(x,y) A4(x,d,y,11,10) A4(x)(d)(y)(con(f11,f10))) ""

13 (Ax(T(x)=>Ez(B(z)&C(x,z))

&AxAy(B(x)&B(y)=>C(x,y))

&AxAy(C(x,y)=>C(y,x))

&AxAyAz(C(x,y)&C(y,z)=>C(x,z))

=>AxAy(T(x)&T(y)=>C(x,y))

Приложение 2 к лекции 3. "Синтаксис специализированного

языка постановок задач"
формула ::= имя | имя '(' имя ',' ... ',' имя ')'

| '(' имя ':' формула ',' ... ',' имя ':' формула '=>'

имя ':' формула ',' ... ',' имя ':' формула '|' ... '|'

имя ':' формула ',' ... ',' имя ':' формула ')'
Другой вариант записи:
<тип> ::= <имя> | <имя> ( <имена> ) | ( <формы> => <варианты> )

<варианты> ::= <формы> | <варианты> \/ <формы>

<формы> ::= <форма> | <формы> , <форма>

<форма> ::= <имя> : <тип>

<имена> ::= <имя> | <имена> , <имя>
Приложение 3 к лекции 3. "Синтаксис языка решений задач

дедуктивного программирования"
программа ::= '{' тело '}'

тело ::= имя ',' ... ',' имя ';' оператор

оператор ::= 'return' цифры аргумент

| имя аргумент [программа ... программа] тело

аргумент ::= '(' выражение ',' ... ',' выражение ')'

выражение ::= имя | программа
Другой вариант записи:
<программа> ::= { <действие> }

<действие> ::= <имена> ; <оператор>

<оператор> ::= return <цифры> <аргумент>

| <имя> <аргумент> <программы> = <действие>

<программы> ::= | <программа> <программы>

<аргумент> ::= ( <значения> )

<значения> ::= <значение> | <значения> , <значение>

<значение> ::= <имя> | <программа>

<цифры> ::= | <цифра> <цифры>

<цифра> ::= 0|1|2|3|4|5|6|7|8|9

<имя> ::= <буква> | <буква> <буквы>

<буква>::=q|w|e|r|t|y|u|i|o|p|a|s|d|f|g|h|j|k|l|z|x|c|v|b|n|m

|Q|W|E|R|T|Y|U|I|O|P|A|S|D|F|G|H|J|K|L|Z|X|C|V|B|N|M
Пример
Формализация на языке постановок задач:
Типы, свойства и отношения:

N:Type - "узел связи"

T:Type(x:N) - "x - телефон"

B:Type(x:N) - "x - база"

C:Type(x:N,y:N) - "соединение от x до y"
Формула постановки задачи:

(a1:(x:N,T(x)=>y:N,B(y),C(x,y)),

a2:(x,y:N,B(x),B(y)=>C(x,y)),

a3:(x,y:N,C(x,y)=>C(y,x)),

a4:(x,y,z:N,C(x,y),C(y,z)=>C(x,z))=>

th:(x,y:N,T(x),T(y)=>C(x,y))

)
Синтезированная программа (обозначения доказательства сохранены):

{a1,a2,a3,a4;

return0({x,y,f1,f2;

a1(x,f1)=c,f4,f5;

a1(y,f2)=d,f7,f8;

a2(c,d,f4,f7)=f9;

a3(y,d,f8)=f10;

a4(x,d,y,f11,f10)=f12;

return0(f12)

} )}

Лекция 4. Формулы как постановки задач программирования
Контрольные вопросы к лекциям 2 и 3
Написать на ламбда-языке реализации формул
1. (A=>(B=>(A&B)))

2. ((AvB)=>((A=>C)=>((B=>C)=>C)))

Примеры постановок задач дедуктивного программироания и их решений
1. Простейший пример для ЯДП:
Легенда: T - телефон, B - база, C - связь:

((x:T=>z:B,C(x,z)), -- 1) каждый телефон может найти базу для связи

(z:B,y:T=>C(z,y)), -- 2) каждая база может соединиться с любым телефоном

(x,y:T,z:B,C(x,z),C(z,y)=>C(x,y)), -- 3) транзитивность соединения

x,y:T -- 4) имеются два телефона

=>C(x,y))) -- тогда их можно связать

{bs, -- посылка 1

ts, -- посылка 2

tc, -- посылка 3

x,y; -- посылка 4

bs(x)=z,c; -- первый телефон ищет базу

ts(z,y)=d; -- база связывается со вторым телефоном

tc(x,y,z,c,d)=e; -- соединение проключается

0(e)

}

2. Пример для ЯДП с разветвлением:
Легенда: + N - узел связи:

((x:N,T(x)=>v:N,B(v),C(x,v)),

(v:N,B(v),y:N,T(y)=>C(v,y)\/w:N,B(w),C(w,y)),

(v,w:N,B(v),B(w)=>C(v,w)),

(x,y,z:N,C(x,y),C(y,z)=>C(x,z)),

x,y:N,T(x),T(y)=>C(x,y))

{bs,ts,bc,tc,x,y,tx,ty;bs(x,tx)=v,bv,cxv;

ts(v,bv,y,ty){cvy,tc(x,v,y,cxv,cvy)=cxy;0(cxy)}

=w,bw,cwy;bc(v,w,bv,bw)=cvw;tc(x,v,w,cxv,cvw)=cxw;

tc(x,w,y,cxw,cwy)=cxy;0(cxy)}

Лекция 5. Математические основы программирования и функциональный подход
Контрольный вопрос
Написать программу по спецификации:

p:(f:(x:A=>y:B),g:(x:B=>y:C)=>h:(x:A=>y:C))

p=?
Программирование как логико-математическая деятельность,

функциональные программы как доказательства.

Проверка контекстных условий в синтезированных программах как

проверка правильности доказательства. Способы развёрнутой записи

программ-доказательств. Сокращённая запись программ-локазательств.

Лекция 6. Специализированные языки программирования
Язык спецификаций программ. Язык программирования, ориентированный

на дедуктивный синтез алгоритмов.
Уровни спецификаций (спецификации обычных языков

программирования с точки зрения дедуктивного программирования).
Перегрузка спецификаций. Спецификации готовых

алгоритмов. Спецификации пустых действий. Спецификации формальных

действий. Спецификации виртуальных данных. Спецификации типов.

Конструкции второго и высших порядков. Типы как аргументы,

порождение типов. Спецификации подтипов,

типы со специфицируемыми параметрами.

Дескриптивно-предикатные типы с параметрами.

Соглашения о связях.
Пример интуиционистской арифметики Пеано в качестве системы

программирования (конструктивные теории как системы программирования).

Лекция 7. Задачи с типами значений высших порядков,

параметризованными типами
Контрольный вопрос:
Пусть N - элементы некоторой алгебры с операцией умножения,

M(x,y,z) - x*y=z (M - предикат умножения, здесь x и y - делители z

или "z делится на x и y").

Записать спецификацию задачи нахождения наиболее общего делителя

произвольных двух элементов алгебры

(делителя, делящегося на все общие делители этих двух элементов).
Ответ:
(x,y:N

=>

d,u,v:N,M(d,u,x),M(d,v,y),

(z,u,v:N,M(z,u,x),M(z,v,y)=>w:N,M(z,w,d))

)

Задачи построения объектов первого и следующих функциональных порядков.

"Уплощение" спецификации.

Включение спецификаций типов в постановку задачи (аргументы

второго и высших типовых порядков - настроечные параметры).
Пример (полная развёрнутая запись):
{N:Type,

B:(n:N=>t:Type),

T:(n:N=>t:Type),

C:(n:N,m:N=>t:Type)

sb:(x:N,t:T(x)=>y:N,b:B(y),c:C(x,y)),

st:(y:N,z:N,b:B(y),u:T(z)=>d:C(x,y)),

tr:(x:N,y:N,z:N,c:C(x,y),d:C(y,z)=e:C(x,z)),

x:N,

z:N,

t:T(x),

u:T(z),

return0:(c:C(x,z));

sb(x:N,t:T(x))=y:N,b:B(y),c:C(x,y);

st:(y:N,z:N,b:B(y),u:T(z))=d:C(x,y));

tr:(x:N,y:N,z:N,c:C(x,y),d:C(y,z))=e:C(x,z));

return0(c:C(x,z))

}:

(N:Type,

B:(n:N=>t:Type),

T:(n:N=>t:Type),

C:(n:N,m:N=>t:Type)

sb:(x:N,u:T(x)=>y:N,b:B(y),c:C(x,y)),

st:(y:N,z:N,b:B(y),t:T(y)=>c:C(x,y)),

tr:(x:N,y:N,z:N,c:C(x,y),d:C(y,z)=>e:C(x,z))

x:N,

z:N,

t:T(x),

u:T(z)

=>

c:C(x,z))

)
Обычная сокращённая запись:
{,

,

,

,

sb,

st,

tr,

x,

z,

t,

u,

return0;

sb(x,t)=y,b,c;

st:(y,z,b,u)=d;

tr:(x,y,z,c,d)=e;

return0(c)

}:

(N:Type,

B,T:(N=>Type),

C:(N,N=>Type)

(x:N,T(x)=>y:N,B(y),C(x,y)),

(y,z:N,B(y),T(y)=>C(x,y)),

(x,y,z:N,C(x,y),C(y,z)=>C(x,z))

x,z:N,

T(x),

T(z)

=>

C(x,z))

)
Сжатая конструктивная запись программы:

{,,,,sb,st,tr,x,z;

sb(x)=y;

st:(y,z);

tr:(x,y,z);

0

}:
Пример: запись аксиомы полной математической индукции

для множества натуральных чисел N
  1   2   3   4

Похожие:

Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconЛекция В. Б. Борщев и B. H. Partee. Казань, кгу, Апрель 2003 стр
Лекция Формальная семантика (продолжение). Интенсиональная логика. Типы. Лямбда и конструкции с лямбдой. Семантика Монтегю для именных...
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconРешением Межгоссовета ЕврАзэс от 27 апреля 2003 г. N 119 основные принципы
Настоящие Основные принципы определяют общие подходы к разработке и реализации межгосударственных целевых программ Евразийского экономического...
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconКраткое содержание лекции 2 Структура и деление атомного ядра 2 Утечка нейтронов из реактора 5 Критический радиус 6
Несколько лекций могут быть только введением в круг этих вопросов. В рамках настоящей лекции мы обсудим самые основные физические...
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconКраткое содержание лекций № Темы лекций. Краткое содержание. Количество часов
Вводная лекция. Цель и задача курса. Организация изучения дисциплин. Основные понятия и определения. Аксиомы статики
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconЛекция №13 Тема: "Магнетизм"
Цель лекции: Дать студентам основные понятия и определения, используемые в разделе электромагнетизм: магнитное поле, напряженность,...
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул icon«Основы менеджмента» и «Менеджмент» Подходы к определению понятия «менеджмент»
Основные понятия бюрократической теории М. Вебера. (по лекции или самостоятельно)
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconЛекция Модульная структура пк. Сазанов В. М
На первой лекции рассмотривались основные понятия Информатики как фундаментальной естественной науки
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconТаппасханова Марина Байдулаховна лекция № тема: «Теоретические основы педагогического проектирования» Основные вопросы, рассматриваемые на лекции
Управление образования
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconЛекция Семантика генитивной конструкции, типы и сорта Тема 1 Генитивная конструкция в русском языке и ее семантика 1
Реалии (вещи, сущности), называемые элементами конструкции – опорным словом и генитивной группой – как-то сортируются нашим языковым...
Лекция \"Основные подходы к синтезу программ\" Содержание лекции Реализационная семантика формул iconЛекция 10. Авторское право и Основы защиты информации Сазанов В. М
На первой лекции рассмотривались основные понятия Информатики как фундаментальной естественной науки
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org