Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная




НазваРабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная
старонка3/3
А П Бельтюков
Дата канвертавання31.01.2013
Памер438.04 Kb.
ТыпРабочая программа
1   2   3

Лекция 13.


3.3. Формальное описание синтаксиса ядра языка


Для того, чтобы задавать алгоритмы над описанным множеством

данных, будем использовать описываемый далее язык

программирования.


Прежде всего, зададим бесконтекстный синтаксис языка

программирования. Далее "выр" обозначает "выражение", "стр"

обозначает "выражение, строящее объект", "исп" - "выражение,

использующее объект", "объ" - "выражение, задающее объект"

(справа написаны комментарии):


выр ::= стр | исп


объ ::= стр | исп


исп ::= цифры -- натуральное число

| имя -- переменная (буквы)

| объ . l -- выборка левой компоненты пары

| объ . r -- выборка правой компоненты пары

| Case ( объ = исп ) first ( исп ) second ( выр )

| Case ( объ = исп ) first ( стр ) second ( исп )

-- разбор случаев

| объ ( выр ) -- применение функции


стр ::= ( выр , выр ) -- создание пары

| First ( выр ) -- генерация первого варианта

| Second ( выр ) -- генерация второго варианта

| Case ( имя = выр ) first ( стр ) second ( стр )

-- разбор случаев

| Row ( имя : выр ) val ( выр )

-- генерация таблицы

| For ( имя , имя : выр := выр ; выр ) to ( выр )

-- цикл

| Nx ( выр ) -- следующее число

| Sd -- множество кодов диагностики

| Sr ( выр ) -- генерация диапазона

| Sa ( выр , выр ) -- сложение множеств

| Sm ( выр , выр ) -- умножение множеств

| Cd -- сложность кодов диагностики

| Cr ( выр ) -- сложность диапазона

| Cm ( выр , выр ) -- умножени на сложность

| Ca ( выр , выр ) -- сложение сложностей

| Cu ( выр , выр ) -- объединение сложностей


3.4. Семантика ядра языка


Выражение, содержащее перемнные x[1],...,x[n] может считаться

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

переменных (которые считаются "исходными данными").


Лекция 14.


3.5. Полиномиальная временная сложность ядра языка


Нетрудно показать что время выполнения программы ограничено

многочленом от первичной сложности входных данных (каждой

программе соответствует свой многочлен). Доказательство этого

факта можно проводить индукцией по построению выражений.


Лекция 15.


3.6. Расширение полиномиального языка программирования.

Подпрограммы, типы значений


Добавим в синтаксис языка (в качестве средств для работы с

подпрограммами) понятия алгоритма функции, применения функции и

типа значения ("тип") следующим образом.


Прежде всего, вводится понятие процедуры-функции

(подпрограммы-функции или алгоритма (вычисления) функции).

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

следующими правилами:


стр ::= Proc ( имя ) val ( выр )

-- порождение алгоритма функции

исп ::= объ ( выр ) -- применение функции


Выражение Proc(X)val(F[X]) является собственно алгоритмом, если

оно не содержит свободных (т.е. не связанных) переменных.

Применение функции Proc(X)val(F[X]) к выражению E заключается в

вычислении выражения F[E]:


Proc(X)val(F[X])(E) = F[E].


Это определение обладает существенным недостатком: иногда оно

приводит к порочному кругу, например, в соответствии с этим

определением, попытка вычисления


Proc(x)val(x(x))(Proc(x)val(x(x)))


никогда не завершится, а будет продолжаться в бесконечном цикле:


Proc(x)val(x(x))(Proc(x)val(x(x))) =

Proc(x)val(x(x))(Proc(x)val(x(x))) =

Proc(x)val(x(x))(Proc(x)val(x(x))) =

...,


Чтобы избавиться от этого недостатка можно ограничить

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


Один из способов сделать это - ввести понятие "типа значения".

Тип значения - специальное выражение, предназначенное для

контроля возможных значений другого выражения. Далее типы

значений будут обозначаться буквами A, B, C, D. Введем следующие

типы значений:


Nat - любое натуральное число;


Range(a) - натуральное число, не превосходящее a;


Congr(a,b) - "конгруэнция" a и b: если значения a и b равны,

равны, то возможно значение 0, в любом случае значением может

быть код сообщения об ошибке; это можно понимать как возможный

результат проверки равенства: если не обнаружено никакой ошибки,

то значения a и b должны совпадать;


Uni(A,B) - значение одного из двух видов (0,a), где a имеет

тип А, или (1,b), где b имеет тип B;


Str(X:A)B[X] - пара (a,b), где а имеет тип A, а b имеет тип

B(a);


Arr(X:A)B(X) - таблично заданная функция f: f(a) имеет тип B[a];


Fun(X:A)B(X) - алгоритмически заданная функция f: f(a) имеет тип

B(a);


Bs(A) - конечное множество, включающее все элементы типа A;


Bc(A) - верхняя граница первичной сложности данных типа A;


3.7. Формальное определение синтаксиса расширения языка с типами


Для того, чтобы использовать язык с типами, вносятся следующие

изменения в синтаксис.


Исключается правило


объ ::= стр


Остается правило


объ ::= исп


Добавляются следующие правила:


исп ::= ( выр : тип ) -- типизированное выражение


тип ::= Nat -- натуральное число

| Error -- код сообщения об ошибке

| Range ( выр ) -- элемент диапазон

| Congr ( выр , выр ) -- конгруэнция (если значения

выражений равны, то 0, в

любом случае значением можнет

быть код сообщения об ошибке)

| Uni ( тип , тип ) -- значение одного из двух типов

| Str ( имя : тип ) тип

-- структура, состоящая из двух

полей, тип второго из которых

может зависеть от значения первого

| Arr ( имя : вид ) тип

-- таблично заданная функция

| Fun ( имя : тип ) тип

-- алгоритмически заданная

функция

| Bs ( тип ) -- список, включающий все

элементы заданного типа

| Bc ( тип ) -- граница сложности для данных

заданного типа


Циклы используются только в конструкции вида:


Proc(X)val(For(Z,Y:F[Z]:=G;H[Z,Y])to(X)),


которая сокращенно записывается как


For(X,Y:F[X]:=G;H[X,Y]).


Лекция 16.


3.7. Библиотечные функции


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

Обозначения библиотечных функций считаются выражениями,

задающими объекты. С каждым таким обозначением связывается тип.


Примеры библиотечных функций и их типов:


- описанная уже операция увеличения числа на 1:


Nx : Fun(n:Nat)Nat,


- переход от элемента диапазона к соответствующему числу

(двуместная функция считается одноместной функцией, выдающей

функцию):


Ext : Fun(n:Nat)Fun(x:Range(n))Nat,


- остаток от деления как элемент диапазона (с обработкой

ситуации попытки деления на 0):


Mod : Fun(n:Nat)Fun(n:Nat)Uni(Range(m),Congr(m,0)).


3.8. Контекстные условия типы выражений и допустимые типы


Далее буквами X и Y обозначаются переменные, буквами A, B, C -

типы, буквами E, F, G - выражения. Запись


A : Type


будет обозначать, что A - допустимый тип ("A принадлежит классу

Type"), другие записи вида


E : A


будут обозначать что выражение E имеет тип A ("E принадлежит

классу A"). Записи


Г |- E : A


и


Г

---

E:A


будут означать, что E принадлежит классу A в предположениях Г.

Запись B[X] означает, что B может содержать свободно переменную

X. В этом случае B[E] - результат подстановки выражения E в B

вместо всех свободных вхождений переменной x.


Контекстные условия языка записываются в виде следующих правил:


- правила допустимоcти типов:


Nat : Type


Error : Type


E : Nat

---------------

Range(E) : Type


E, F : Nat

-----------------

Congr(E,F) : Type


A : Type

B : Type

---------------

Uni(A,B) : Type


A : Type

X : A |- B[X] : Type

--------------------

Str(X:A)B[X] : Type


A : Type

X : A |- B[X] : Type

--------------------

Arr(X:A)B[X] : Type


A : Type

X : A |- B[X] : Type

--------------------

Fun(X:A)B[X] : Type


- правила для натуральных чисел:


0 : Nat


E : Nat

-----------

Nx(E) : Nat


- правила для основных операций:

-- объединение:


E : A

-------------------

First(E) : Uni(A,B)


E : A

--------------------

Second(E) : Uni(B,A)


E : (A,В)

X : A |- F[X] : C

X : A |- G[X] : C

------------------------------------

Case(X=E)first(F[X])second(G[X]) : C


-- пара:


E : A

F : B[E]

--------------------

(E,F) : Str(X:A)B[X]


E : Str(X:A)B[X]

----------------

E.l : A

E.r : B[E.l]


-- таблица функции:


E : Bs(A)

X : A |- F[X] : B[X]

--------------------------------

Row(X:E)val(F[X]) : Arr(X:A)B[X]


F : Arr(X:A)B[X]

E : A

----------------

F(E) : B[E]


-- алгоритм функции:


X : A |- E[X] : B[X]

---------------------------------

Proc(X:A)Val(E[X]) : Fun(X:A)B[X]


F : Fun(X:A)B[X]

E : A

----------------

F(E) : B[E]


- правила для циклов:


X : Nat |- F : Bc(A[X])

G : A[0]

X : Nat, Y : A |- H[X,Y] : A[Nx(X)]

---------------------------------------------

For(X,Y:F[X]:=G;H[X,Y]) : Fun(X:Nat)A[X]


E, F : Nat

-------------------

Cd : Bc(Congr(E,F))


E, F : Nat

-------------------

Sd : Bs(Congr(E,F))


Cd : Bs(Error)


Sd : Bs(Error)


E : Nat

--------------------

Cr(E) : Bc(Range(E))


E : Nat

--------------------

Sr(E) : Bs(Range(E))


E : Bc(A)

F : Bc(B)

----------------------

Cu(E,F) : Bc(Uni(A,B))


E : Bs(A)

F : Bs(B)

----------------------

Sa(E,F) : Bs(Uni(A,B))


E : Bc(A)

X : A -> F : Bc(B[X])

--------------------------

Ca(E,F) : Bc(Str(X:A)B[X])


E : Bs(A)

X : A -> F : Bs(B[X])

--------------------------

Sm(E,F) : Bs(Str(X:A)B[X])


E : Bs(A)

X : A -> F : Bc(B[X])

--------------------------

Cm(E,F) : Bc(Arr(X:A)B[X])


Лекция 17. Индуктивный синтез алгоритмов и программ


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


Лекция 18. Трансформационный синтез алгоритмов и программ


Основы трансформационного синтеза программ. Частичные и смешанные вычисления.



  1. Программа лабораторных занятий


Занятие 1. Основные подходы к синтезу программ


Занятие 2. Основы дедуктивного синтеза алгоритмов


Занятие 3. Логические основы дедуктивного синтеза программ

Занятие 4. Формулы как постановки задач программирования


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


Занятие 6. Специализированные языки программирования

Занятие 7. Постановки ациклических задач


Занятие 8. Постановки задач с циклами


Занятие 9. Постановки задач с рекурсиями


Занятие 10. Синтез полиномиальных программ


Занятие 11. Язык данных для полиномиального программирования


Занятие 12. Переменные и выражения в полиномиальном программировании


Занятие 13. Формальное описание синтаксиса ядра языка. Семантика


Занятие 14. Полиномиальная временная сложность синтезируемых программ


Занятие 15. Расширение языка полиномиального программирования


Занятие 16. Библиотечные функции, контекстные условия, типы выражений и допустимые типы


Занятие 17. Индуктивный синтез алгоритмов и программ


Занятие 18. Трансформационный синтез алгоритмов и программ


  1. Программа самостоятельной работы студента


Самостоятельная работа выполняется в виде заданий к соответствующим лабораторным работам. Задания сдаются раз неделю по следующим неделям:


Неделя 1. Основные подходы к синтезу программ


Неделя 2. Основы дедуктивного синтеза алгоритмов


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

Неделя 4. Формулы как постановки задач программирования


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


Неделя 6. Специализированные языки программирования

Неделя 7. Постановки ациклических задач


Неделя 8. Постановки задач с циклами


Неделя 9. Постановки задач с рекурсиями


Неделя 10. Синтез полиномиальных программ


Неделя 11. Язык данных для полиномиального программирования


Неделя 12. Переменные и выражения в полиномиальном программировании


Неделя 13. Формальное описание синтаксиса ядра языка. Семантика


Неделя 14. Полиномиальная временная сложность синтезируемых программ


Неделя 15. Расширение языка полиномиального программирования


Неделя 16. Библиотечные функции, контекстные условия, типы выражений и допустимые типы


Неделя 17. Индуктивный синтез алгоритмов и программ


Неделя 18. Трансформационный синтез алгоритмов и программ


  1. Контролирующие материалы


Задания для самостоятельной работы


*** Раздел 1 ***


Тестовое задание 1


Условие 1


Пусть S - множество (тип данных) студентов, Q - множество задаваемых

вопросов, R(s,q) - множество правильных ответов, данных студентом s

на вопрос q [тип R задается формой R(S,Q)].


Вопрос 1


Как сформулировать на определенном таким образом логико-предметном

языке утверждение:

"Каждый студент правильно ответил хотя бы на один вопрос"?


Пример верного ответа на вопрос 1:


As:S Eq:Q R(s,q).


Тестовое задание 2


Условие 2


Пусть теперь вдобавок к условию 1 выполнено следующее:


S={a,b}, Q={c,d}, R(a,c)={e,f}, R(a,d)={g}, R(b,c)=0, R(b,d)={h}.


Вопрос 2


Как записать множество всех реализаций утверждения, сформулированного

в вопросе 1 с использованием таблично заданных функций?


Пример правильного ответа на вопрос 2:


{{(a,(c,e)),(b,(d,h))},

{(a,(c,f)),(b,(d,h))},

{(a,(d,g)),(b,(d,h))}}.


Тест


При условиях 1 и 2 сформулировать и выписать все табличные реализации

следующих предложений:


Задачи 1-2. Хотя бы один из студентов правильно ответил на все вопросы.

Задачи 3-4. На каждый вопрос правильно ответил хотя бы один студент.

Задачи 5-6. Хотя бы на один из вопросов правильно ответили все студенты.


*** Раздел 2 ***


Пример задачи из области мобильной связи


Типы данных и предикаты:

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

T(n) - "n - телефон",

B(n) - "n - база",

С(m,n) - "n можно соединить с m"


Пример задачи, сформулированной на традиционном логико-предметном

языке:

An:N (T(n) => Em:N (B(m) & C(n,m))&

An:N Am:N (B(n) & B(m) => C(n,m))&

An:N Am:N Ak:N (C(n,m) & C(m,k) => C(n,k))&

An:N Am:N (C(n,m) => C(m,n)) =>

An:N Am:N C(n,m)


Пример той же задачи (с решением) на специальном языке:

((n:N, T(n) => m:N, B(m), C(n,m)),

(n:N, m:N, B(n), B(m) => C(n,m)),

(n:N, m:N, k:N, C(n,m), C(m,k) => C(n,k)),

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

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

)

{bs,bc,tc,rc; return

({n,m;

bs(n)=nb,bnb,cnnb;

bs(m)=mb,bmb,cmmb;

bc(nb,mb,bnb,bmb)=cnbmb;

tc(n,nb,mb,cnnb,cnbmb)=cnmb;

rc(m,mb,cmmb)=cmbm;

tc(n,mb,m,cnmb,cmbm)=cnm;

return(cnm);

})}


Синтаксис языка постановок


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

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

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

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


Синтаксис языка решений


программа ::= '{' тело '}'

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

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

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

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

выражение ::= имя | программа


Запросы с циклами


Пример производственной задачи


Предопределенные типы данных и предикаты:

i:I - "i - продукт",

R(i,j) - "продукт i вырабатывается из продукта j",

A:Type - "A - описание данных"


Комментарии к задаче:

S(i) - стоимость продукта i,

for_i_r(A,body)=r; - оператор цикла по продуктам с шагом R с типом

обрабатываемых данных A, результатом работы r и телом body вида {i,prev;a},

где i - параметр цикла, prev(j,rij) - значение, выработанное на шаге

j, связанном c шагом i значением rij типа R(i,j), а - оператор тела цикла.


Задача нахождения стоимостей продуктов (с решением):

(for_i_r:(A:Type,(i:I,prev:(j:I,R(i,j)=>A(j))=>A(i))=>(i:I=>A(i))),

S:Type,

sp:(i:I=>S(i)|j:I,R(i,j)),

cn:(i,j:I,R(i,j),S(j)=>S(i))

=>(i:I=>S(i))

)

{for_i_r,S,sp,cn;

for_i_r

(S,

{i,prev;

sp(i){si;return(si)}=j,rij;

prev(j,rij)=sj;

cn(i,j,rij,sj)=si;

return(si)

}

)=solution;

return(solution)

}


Это же можно сокращенно записать так:

(for_i_r:(A:Type,(i:I,(j:I,R(i,j)=>A(j))=>A(i))=>(i:I=>A(i))),

S:Type,

(i:I=>S(i)|j:I,R(i,j)),

(i,j:I,R(i,j),S(j)=>S(i))

=>(i:I=>S(i))

)

{for_i_r,S,sp,cn;

for_i_r

(S,

{i,prev;

sp(i){;}j;

prev(j,rij);

cn(i,j,rij,sj);

}

)=solution;

(solution)

}


Развернутая запись с типами при определяющих вхождениях имен выглядит так:


(for_i_r:(A:Type,(i:I,prev:(j:I,R(i,j)=>A(j))=>A(i))=>(i:I=>A(i))),

S:Type,

sp:(i:I=>S(i)|j:I,R(i,j)),

cn:(i,j:I,R(i,j),S(j)=>S(i))

=>solution:(i:I=>S(i))

)


{for_i_r:(A:Type,(i:I,prev:(j:I,R(i,j)=>A(j))=>A(i))=>(i:I=>A(i))),

S:Type,

sp:(i:I=>S(i)|j:I,R(i,j)),

cn:(i,j:I,R(i,j),S(j)=>S(i)),

return:(solution:(i:I=>S(i)));

for_i_r

(S,

{i:I,prev:(j:I,R(i,j)=>A(j));

sp(i){si:S(i);return(si)}=j:I,rij:R(i,j);

prev(j,rij)=sj:S(j);

cn(i,j,rij,sj)=si:S(i);

return(si)

}

)=solution:(i:I=>S(i));

return(solution)

}


Полная запись со всеми типами и именами выглядит так

(порядок записи: "решение:описание"):


{for_i_r:(A:Type,(i:I,prev:(j:I,r:R(i,j)=>a:A(j))=>a:A(i))=>(i:I=>a:A(i))),

S:Type,

sp:(i:I=>s:S(i)|j:I,r:R(i,j)),

cn:(i,j:I,r:R(i,j),sj:S(j)=>si:S(i)),

return:(solution:(i:I=>s:S(i)));

for_i_r

(S:Type,

{i:I,prev:(j:I,R(i,j)=>S(j)),return:(si:S(i));

sp(i:I){si:S(i);return(si:S(i))}=j:I,rij:R(i,j);

prev(j:I,rij:R(i,j))=sj:S(j);

cn(i:I,j:I,rij:R(i,j),sj:S(j))=si:S(i);

return(si:S(i))

}:(i:I,prev:(j:I,r:R(i,j)=>s:S(j))=>si:S(i))

)=solution:(i:I=>s:S(i));

return(solution:(i:I=>s:S(i)))

}

:

(for_i_r:(A:Type,(i:I,prev:(j:I,r:R(i,j)=>a:A(j))=>a:A(i))=>(i:I=>a:A(i))),

S:Type,

sp:(i:I=>s:S(i)|j:I,r:R(i,j)),

cn:(i,j:I,r:R(i,j),sj:S(j)=>si:S(i))

=>solution:(i:I=>s:S(i))

)


Тест


Контекст i,j:I,r:R(i,j),

f:(x:I=>A(x)),g:(x,y:I,R(x,y)=>A(x)),h:(x:I,R(i,x)=>A(x))


|F:

(Z): |f|g|h

-------+-+-+-

(i) |X|0|0

(j) |X|0|0

(i,j,r)|0|X|0

(i,r) |0|0|0

(j,r) |0|0|X


*** Раздел 3 ***


Здесь


Ent - описания сущностей

Rel - описания простых предикатов (атрибутов, связей...)

City - города

Road(c,d) - "город c соединен с городом d дорогой"

High(c,d) - "город c расположен выше города d"

Port(c) - "в городе c есть морской порт"

Error - ошибки в базе данных


Пример работы базы данных с ограничениями

City:Ent,

High,Port,Road:Rel,

ir:(i:City,High(i,i)=>Error),

tr:(i,j,k:City,High(i,j),High(j,k)=>High(i,j)),

go:(i:City=>Port(i)|j:City,High(i,j),Road(i,j)):


? Ijevsk:City

Port(Ijevsk)? No

j:City,High(Ijevsk,j),Road(Ijevsk,j)? Moscow

Port(Moscow)? No

j:City,High(Moscow,j),Road(Moscow,j)? Izhevsk

Ijevsk:City,High(Ijevsk,Ijevsk)=>Error!

j:City,High(Moscow,j),Road(Moscow,j)? SPb

Port(SPb)? Yes

? Cesis:City

Port(Cesis)? No

j:City,High(Cesis,j),Road(Cesis,j)? Riga

Port(Riga)? Yes

...


Далее - "слабая задача транспортной логистики":


Пусть Way(x,y) - пути из x в y.


Постановка задачи:


(forgen:

(I:Ent,R:Type,(i:I,R(i,i)=>Error),(i,j,k:I,R(i,j),R(j,k)=>R(i,j))

=>for:(A:Type,(i:I,prev:(j:I,R(i,j)=>A(j))=>A(i))=>(i:I=>A(i)))

),

packer:

(I:Ent,W:Type,j:I=>B:Type,pack:(i:I,W(i,j)=>B(i)),unpack:(i:I,B(i)=>W(i,j)))

City:Ent,Higher:Rel,Way:Type,

ir:(i:City,Higher(i,i)=>Error),

tr:(i,j,k:City,Higher(i,j),Higher(j,k)=>Higher(i,j)),

go:(i:City=>Port(i)|j:City,Higher(i,j),Road(i,j)),

rw:(i,j:City,Road(i,j)=>Way(i,j)),

tw:(i,j,k:City,Way(i,j),Way(j,k)=>Way(i,k)),

sw:(i,j:City,Port(i),Port(j)=>Way(i,j))

=>task:(i,j:City,Port(j)=>Way(i,j)))

)


Решение задачи (короткая запись):


{forgen,packer,City,Higher,Way,ir,tr,go,rw,tw,sw;

forgen(City,Higher,ir,tr)=for;

return

({i,j,pj;

packer(City,Way,j)=B,pack,unpack;

for

(B,

{i,prev;

go(i){pi;sw(i,j,pi,pj)=wij;pack(i,wij)=bi;return(bi)}

=k,hik,rik;

prev(k,rik)=bk;

unpack(k,bk)=wkj;

rw(i,k,rik)=wik;

tw(i,k,j,wik,wkj)=wij;

pack(i,wij)=bi;

return(bi)

}

)=subtask;

subtask(i)=bi;

unpack(i,bi)=wij;

return(wij)

})}


Это же решение в сокращенной записи:


{forgen,packer,City,Higher,Way,ir,tr,go,rw,tw,sw;

forgen(City,Higher,ir,tr)for;

return

({i,j;

packer(City,Way,j)B,pack,unpack;

for

(B,

{i,prev;

go(i){;sw(i,j);pack(i);}k;

prev(k);

unpack(k);

rw(i,k);

tw(i,k,j);

pack(i);

}

)subtask;

subtask(i);

unpack(i);

})}


Это же решение с полными комментариями по типам определяющих вхождений имен

{forgen:

(I:Ent,R:Type,(i:I,R(i,i)=>Error),(i,j,k:I,R(i,j),R(j,k)=>R(i,j))

=>for:(A:Type,(i:I,prev:(j:I,R(i,j)=>A(j))=>A(i))=>(i:I=>A(i)))

),

packer:

(I:Ent,W:Type,j:I=>B:Type,pack:(i:I,W(i,j)=>B(i)),unpack:(i:I,B(i)=>W(i,j))),

City:Ent,Higher:Rel,Way:Type,

ir:(i:City,Higher(i,i)=>Error),

tr:(i,j,k:City,Higher(i,j),Higher(j,k)=>Higher(i,j)),

go:(i:City=>Port(i)|j:City,Higher(i,j),Road(i,j)),

rw:(i,j:City,Road(i,j)=>Way(i,j)),

tw:(i,j,k:City,Way(i,j),Way(j,k)=>Way(i,k)),

sw:(i,j:City,Port(i),Port(j)=>Way(i,j)),

return:((i,j:City,Port(j)=>Way(i,j))));


forgen(City,High,ir,tr)

=for:(A:Type,(i:City,prev:(j:City,Higher(i,j)=>A(j))=>A(i))=>(i:City=>A(i)));

return

({i,j:City,pj:Port(j),return:(Way(i,j));

packer(City,Way,j)=B:Type,pack:(i:I,Way(i,j)=>B(i)),unpack:(i:I,B(i)=>W(i,j));

for

(B,

{i:City,prev:(j:City,Higher(i,j)=>A(j));

go(i){pi:Port(i);sw(i,j,pi,pj)=wij:Way(i,j);pack(i,wij)=bi:B(i);return(bi)}

=k:City,hik:Higher(i,k),rik:Road(i,j);

prev(k,rik)=bk:B(k);

unpack(k,bk)=wkj:Way(k,j);

rw(i,k,rik)=wik:Way:(i,k);

tw(i,k,j,wik,wkj)=wij:Way(i,j);

pack(i,wij)=bi:B(i);

return(bi)

}

)=subtask:(i:City=>B(i));

subtask(i)=bi:B(i);

unpack(i,bi)=wij:Way(i,j);

return(wij)

})}


*** Раздел 4 ***


Информационные задачи с ресурсами


Задача нахождения стоимостей продуктов (с решением):

d:$(i) - d - сумма, соответствующая сложности i

$:Res - $ - описание ресурса


(for:(A:Type,(i:I,prev:(j:I,R(i,j)=>A(j))=>A(i))=>(i:I=>A(i))),

S:Type,

pack:(i:I,($(i)=>S(i))=>A(i)),

unpack:(i:I,A(i),$(i)=>S(i)),

sp:(i:I=>($(i)=>S(i))|($(i)=>j:I,R(i,j),$(j))),

cn:(i,j:I,R(i,j),S(j)=>S(i))

=>(i:I,$(i)=>S(i)))

)

{for,S,pack,unpack,sp,cn;

for

(A,

{i,prev;

sp(i){disi;return(disi)}=dijrdj;

pack

(i,

{di;

dijrdj(si)=j,rij,dj;

prev(j,rij)=aj;

unpack(j,aj,dj)=sj;

cn(i,j,rij,sj)=si;

return(si)

}

)=ai;

return(ai);

}

)=subtask;

return({i,di;subtask(i)=ai;unpack(i,ai,di)=si;return(si)})

}


*** Раздел 5 ***


Первоначальная запись задачи о стоимости продуктов

в другом синтаксисе:


(for:(A:Type,

body:(i:I,

prev:(j:I,rij:R(i,j),returnaj:(aj:A(j))),

returnai:(ai:A(i))

),

return:((i:I,returnai:(ai:A(i))))

),

S:Type,

sp:(i:I,return0:(S(i)),return1:(j:I,R(i,j))),

cn:(i,j:I,R(i,j),S(j),returnsi:(S(i))),

return:((i:I,returnsi:(S(i))))

)

{for,S,sp,cn,return;

for(S,{i,prev,returnsi;

sp(i,{si;returnsi(si)},

{j,rij;prev(j,rij,{sj;cn(i,j,rij,sj,{si;returnsi(si)})})}

)

},

{solution;return(solution)}

)

}


То же - с развернутыми комментариями (постановка задачи вложена, скобки):


(for:(A:Type,

(i:I,

prev:(j:I,rij:R(i,j),returnaj:(aj:A(j))),

returnai:(ai:A(i))

),

return:(solution:(i:I,returnai:(ai:A(i))))

),

S:Type,

sp:(i:I,returnsi:(S(i)),returnjrij:(j:I,R(i,j))),

cn:(i,j:I,R(i,j),S(j),returnsi:(S(i))),

return:((i:I,returnsi:(S(i))));

for(S,(i:I,

prev:(j:I,R(i,j),returnsj:(sj:S(j))),

returnsi:(si:S(i));


sp(i,(si:S(i);returnsi(si)),

(j:I,rij:R(i,j);

prev(j,rij,(sj:S(j);cn(i,j,rij,sj,(si:S(i);returnsi(si)))))

)

)

),

(solution:(i:I,returnsi:(si:A(i)));return(solution))

)

)


С отделением возвратов:


(for:(A:Type,

(i:I,

prev:(j:I,rij:R(i,j)=>(aj:A(j)))=>

returnai:(ai:A(i))

)=>

(solution:(i:I=>(ai:A(i))))

),

S:Type,

sp:(i:I=>(S(i)),(j:I,R(i,j))),

cn:(i,j:I,R(i,j),S(j)=>(S(i)))=>

return:(solution:(i:I=>(si:S(i))))

)

for(S,(i:I,

prev:(j:I,rij:R(i,j)=>(sj:S(j)))=>

returnsi:(si:S(i))

)

sp(i,

(si:S(i))returnsi(si)),

(j:I,rij:R(i,j))

prev(j,rij,(sj:S(j))cn(i,j,rij,sj,(si:S(i))returnsi(si)))

),

(solution:(i:I=>(si:S(i))))return(solution)

)


Короче:


(for:(A:Type,

(i:I,

prev:(j:I,rij:R(i,j)=>(aj:A(j)))=>

returnai:(ai:A(i))

)=>

(solution:(i:I=>(ai:A(i))))

),

S:Type,

sp:(i:I=>(S(i)),(j:I,R(i,j))),

cn:(i,j:I,R(i,j),S(j)=>(S(i)))=>

return:(solution:(i:I=>(si:S(i))))

)

for(S,(i,

prev=>

returnsi

)

sp(i,(si) returnsi(si),

(j,rij)

prev(j,rij,(sj; cn(i,j,rij,sj,(si:S(i); returnsi(si)))))

),

(solution) return(solution))

)


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


программа ::= формула имя(<выр>,...,<выр>))

формула ::= (форма,...,форма[=>форма,...,форма])

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

тип ::= имя | имя (имя,...,имя) | формула

выр ::= имя | программа


*** Раздел 6 ***


Пример посложнее (полная задача транспортной логистики):


(City:Ent,

High:Rel,

(I:List,R:Type,(i:I,R(i,i)=>Error),(i,j,k:I,R(i,j),R(j,k)=>R(i,j))

=>(A:Type,(i:I,prev:(j:I,R(i,j)=>A(j))=>A(i))=>(i:I=>A(i)))

),

(i:City,High(i,i)=>Error),

(i,j,k:City,High(i,j),High(j,k)=>High(i,j)),

(i:City=>Port(i)|j:City,High(i,j),Road(i,j)),

Way:Type,

(i,j:City,Road(i,j)=>Way(i,j)),

(i,j:City,w:Way(i,j)=>Way(j,i)),

(i,j,k:City,Way(i,j),Way(j,k)=>Way(i,k)),

(i,j:City,Port(i),Port(j)=>Way(i,j))

(I:Ent,P:Rel,W:Type

=>C:Type,(i,j:I,P(j),W(i,j)=>C(i)),(i:I,C(i)=>j:I,P(j),W(i,j))),

(I:Ent,W:Type,j:I=>B:Type,(i:I,W(i,j)=>B(i)),(i:I,B(i)=>W(i,j)))

=>(j:City=>(i:City=>Way(i,j)))

)


Подсказкa: сначала следует запрограммировать

task1:(j:City=>k:City,Port(k),Way(j,k))


Решение задачи

{City,High,forgen,ir,tr,go,Way,rw,iw,tw,sw,pack3,pack1;

pack3(City,Port,Way)=CPW,CPWpack,CPWunpack;

forgen(City,High,ir,tr)=for_c_h;

for_c_h

(CPW,

{...

}

)=task1a:(i:City=>CPW(i));

return

({j;

pack1(City,Way,j)=Wj,WjPack,WjUnpack;

for_c_h

(CW,

{...

}

)=taska:(i:City=>Wj(x));

return({i;taska(i)=wi_j;WjUnpack(i,wi_j)=wij;return(wij)})

}

)

}


Пример задачи с ограничением сложности без индукции

(сложность ограничивается при выводе без сечений)

(E - равенство, A и B - противоположные свойства)


Постановка задачи:


( -- Пусть:

z,i:X, -- есть два предмета - z и i,

(x:X=>A(x)|B(x)), -- каждый предмет - обладает свойством A или B,

(x:X=>E(x,z)|E(x,i)), -- каждый предмет равнозначен z или i,

(x,y:X,E(x,y),B(y)=>B(x)) -- если два предмета равнозначны

-- и второй из них обладает свойством B,

-- то первый предмет также обладает свойством B.

=> -- Тогда:

x:X, A(x) -- или есть хотя бы один предмет типа A

| (x:B => B(x)) -- или все предметы обладают свойством B.

)


Решение:

{z,i:X, -- Пусть есть два предмета - z и i,

f:(x:X=>A(x)|B(x)), -- каждый предмет обладает свойством A или B,

g:(x:X=>E(x,z)|E(x,i)), -- каждый предмет равнозначен z или i,

h:(x,y:X,E(x,y),B(y)=>B(x)),-- если два предмета равнозначны

-- и второй из них обладает свойством B,

-- то первый предмет также обладает свойством B.

0:(x:X, A(x)), -- Результат 0: получить предмет со свойством A

1:((x:B => B(x))); -- Результат 1: для всех предметов установить B.

f(z)

{az:A(z); -- Cлучай 1: z обладает свойством A.

0(z,az) -- Тогда результат 0: есть предмет со свойством A.

}=bz:B(z); -- Случай 2: z обладает свойством B.

f(i){ai:A(i); -- Подслучай 2.1: i обладает свойством A.

0(i,ai)} -- Тогда результат 0: есть предмет со свойством A.

=bi:B(i); -- Подслучай 2.2: i тоже обладает свойством B.

1({ -- Тогда результат 1:

x:X, -- Возьмем произвольное x.

0:(B(x)); -- и получим для него свойство B.

g(x)

{exz:E(x,z); -- Подслучай 2.2.1: x равнозначно z.

h(x,z,exz)=bx:B(x); -- Тогда x обладает свойством В.

0(bx) -- Требуемое доказано.

}=exi:E(x,i); -- Подслучай 2.2.2: x равнозначно i.

h(x,i,exi)=bx:B(x); -- Тогда x обладает свойством В.

0(bx) -- Требуемое доказано.

} )}


Альтернативная запись этой задачи:


{z, i:X,

f:{x:X,{A(x)},{B(x)}},

g:{x:X,{E(x,z)},{E(x,i)}},

h:{x,y:X,E(x,y),B(y),{B(x)}},

0:{x:X,A(x)}, 1:{{x:B,{B(x)}}};

f(z,{az:A(z);0(z,az)},

{bz:B(z);

f(i,{ai:A(i);0(i,ai)}

{bi:B(i);

1({x:X,0:{B(x)};

g(x,{exz:E(x,z);h(x,z,exz,{bx:B(x);0(bx)})},

{exi:E(x,i);h(x,i,exi,{bx:B(x);0(bx)})}

)

}

)

}

)

}

)

}


********** Итоговые задачи **********


Задача 1. Пусть U={a,b}


Даны следующие списки реализаций предикатов C и D:


1. C(a)=0, C(b)={1}, D(a)={2,3}, D(b)={4}

2. C(a)={1}, C(b)=0, D(a)={2}, D(b)={3,4}

3. C(a)={1,2}, C(b)={3}, D(a)=0, D(b)={4,5}

4. C(a)={1}, C(b)={2,3}, D(a)={4}, D(b)=0

5. C(a)=0, C(b)={1}, D(a)={2}, D(b)={3,4}

6. C(a)={1,2}, C(b)=0, D(a)={3}, D(b)={4}


Найти все реализации:


1. Ex (C(x) & D(x))

2. Ex (C(x) \/ D(x))

3. Ex C(x) & Ey D(y)

4. Ex C(x) \/ Ey D(y)

5. Ex Ey (C(x) & D(y))


Задача 2. Расставить типы:


1. ((A=>B,C), (B=>D), A=> C,D)

{a:...,

b:...,

c:...,

return:(...);

a(c)=d:...,e:...;

b(d)=f:...;

return(e,f)}


2. ((A=>B,C), (B=>D)=> (A=>C,D))

{f:...,

g:...,

return:(...);

return({a:...,

f(a)=b:...,c:...;

g(b)=d:...;

return(c,d)}


3. ((B=>D), (A=>B,C), A=> C,D)

{a:...,

b:...,

c:...,

return:(...);

b(c)=d:...,e:...;

a(d)=f:...;

return(e,f)}


4. ((B=>D), (A=>B,C) => (A=>C,D))

{f:...,

g:...,

return:(...);

return({a:...,

g(a)=b:...,c:...;

f(b)=d:...;

return(c,d)}


5. ((A=>B,C), (C,B=>D), A=> C,D)

{a:...,

b:...,

c:...,

return:(...);

a(c)=d:...,e:...;

b(e,d)=f:...;

return(e,f)}


6. ((A=>B,C), (C,B=>D)=> (A=>C,D))

{f:...,

g:...,

return:(...);

return({a:...,

f(a)=b:...,c:...;

g(c,b)=d:...;

return(c,d)}


7. ((C,B=>D), (A=>B,C), A=> C,D)

{a:...,

b:...,

c:...,

return:(...);

b(c)=d:...,e:...;

a(e,d)=f:...;

return(e,f)}


8. ((C,B=>D), (A=>B,C) => (A=>C,D))

{f:...,

g:...,

return:(...);

return({a:...,

g(a)=b:...,c:...;

f(c,b)=d:...;

return(c,d)}


9. (x:A, (B(x) => C(x), D(x), E(x)), B(x) => C(x), D(x), E(x))

{a:...,

b:...,

c:...,

return:(...);

b(c)=d:...,e:...,f:...;

return(d,e,f)}


10. (x:A, (B(x) => C(x), D(x) \/ E(x)), B(x) => C(x), D(x) \/ E(x))

{a:...,

b:...,

c:...,

return0:(...),

return1:(...);

b(c)={d:...,e:...;

return0(d,e)}=f:...;

return(f)}


11. (x:A, (B(x) => C(x) \/ D(x) \/ E(x)), B(x) => C(x) \/ D(x) \/ E(x))

{a:...,

b:...,

c:...,

return0:(...),

return1:(...),

return2:(...);

b(c)={d:...;

return0(d)}{e:...;

return1(e)}=f:...;

return(f)}


12. (x:A, B(x), (B(x) => C(x), D(x), E(x)) => C(x), D(x), E(x))

{a:...,

b:...,

c:...,

return:(...);

c(b)=d:...,e:...,f:...;

return(d,e,f)}


13. (x:A, B(x), (B(x) => C(x), D(x) \/ E(x)) => C(x), D(x) \/ E(x))

{a:...,

b:...,

c:...,

return0:(...),

return1:(...);

c(b)={d:...,e:...;

return0(d,e)}=f:...;

return(f)}


14. (x:A, B(x), (B(x) => C(x) \/ D(x) \/ E(x)) => C(x) \/ D(x) \/ E(x))

{a:...,

b:...,

c:...,

return0:(...),

return1:(...),

return2:(...);

b(c)={d:...;

return0(d)}{e:...;

return1(e)}=f:...;

return(f)}


15. ((E=>F,G), (F=>H), E=> G,H)

{a:...,

b:...,

c:...,

return:(...);

a(c)=d:...,e:...;

b(d)=f:...;

return(e,f)}


16. ((E=>F,G), (F=>H)=> (E=>G,H))

{f:...,

g:...,

return:(...);

return({a:...,

f(a)=b:...,c:...;

g(b)=d:...;

return(c,d)}


17. ((F=>H), (E=>F,G), E=> G,H)

{a:...,

b:...,

c:...,

return:(...);

b(c)=d:...,e:...;

a(d)=f:...;

return(e,f)}


18. ((F=>H), (E=>F,G) => (E=>G,H))

{f:...,

g:...,

return:(...);

return({a:...,

g(a)=b:...,c:...;

f(b)=d:...;

return(c,d)}


19. ((E=>F,G), (G,F=>H), E=> G,H)

{a:...,

b:...,

c:...,

return:(...);

a(c)=d:...,e:...;

b(e,d)=f:...;

return(e,f)}


20. ((E=>F,G), (G,F=>H) => (E=>G,H))

{f:...,

g:...,

return:(...);

return({a:...,

f(a)=b:...,c:...;

g(c,b)=d:...;

return(c,d)}


21. ((G,F=>H), (E=>F,G), E => G,H)

{a:...,

b:...,

c:...,

return:(...);

b(c)=d:...,e:...;

a(e,d)=f:...;

return(e,f)}


22. ((G,F=>H), (E=>F,G) => (E=>G,H))

{f:...,

g:...,

return:(...);

return({a:...,

g(a)=b:...,c:...;

f(c,b)=d:...;

return(c,d)}


23. (x:F, (G(x) => H(x), I(x), J(x)), G(x) => H(x), I(x), J(x))

{a:...,

b:...,

c:...,

return:(...);

b(c)=d:...,e:...,f:...;

return(d,e,f)}


24. (x:F, (G(x) => H(x), I(x) \/ J(x)), G(x) => H(x), I(x) \/ J(x))

{a:...,

b:...,

c:...,

return0:(...),

return1:(...);

b(c)={d:...,e:...;

return0(d,e)}=f:...;

return(f)}


25. (x:F, (G(x) => H(x) \/ I(x) \/ J(x)), G(x) => H(x) \/ I(x) \/ J(x))

{a:...,

b:...,

c:...,

return0:(...),

return1:(...),

return2:(...);

b(c)={d:...;

return0(d)}{e:...;

return1(e)}=f:...;

return(f)}


26. (x:F, G(x), (G(x) => H(x), I(x), J(x)) => H(x), I(x), J(x))

{a:...,

b:...,

c:...,

return:(...);

c(b)=d:...,e:...,f:...;

return(d,e,f)}


27. (x:F, G(x), (G(x) => H(x), I(x) \/ J(x)) => H(x), I(x) \/ J(x))

{a:...,

b:...,

c:...,

return0:(...),

return1:(...);

c(b)={d:...,e:...;

return0(d,e)}=f:...;

return(f)}


28. (x:F, G(x), (G(x) => H(x) \/ I(x) \/ J(x)) => H(x) \/ I(x) \/ J(x))

{a:...,

b:...,

c:...,

return0:(...),

return1:(...),

return2:(...);

b(c)={d:...;

return0(d)}{e:...;

return1(e)}=f:...;

return(f)}



  1. Список литературы


Основная литература


1. Э.Х.Тыугу. Концептуальное программирование, М. Наука, 1984, 256.


2. А.П.Бельтюков. Малые сложностные классы и автоматичческий

дедуктивный синтез алгоритмов // Известия института математики и

информамтики, Ижевск, УдГУ, 1995, вып. 2, 3-87.

(http://csds.udsu.ru/~belt/apbsynt8.lat)


Дополнительная литература


1. С.К.Клини. Введение в метаматематику. М "Иностраниздат",

1957, 526 с.


2. К.А.Гоуд. Доказательства как описания вычислений. В кн.

"Математическая логика в программировании". Под ред.

М.В.Захарьящева и Ю.И.Янова. М. 1991. С. 311-330. (407 с.)


3. Дж.Булос,Р.Джефри. Вычислимость и логика, М. Мир. 1994.

396с.


4. Проект COQ // http://www.inria.fr (2005)
1   2   3

Падобныя:

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconПрограмма по дисциплине «Вычислительные задачи геометрии» для специальности: 511200 Математика. Прикладная математика (магистратура) очная форма обучения
Эвм, вычислительной геометрии. Основным содержанием дисциплины является исследования и оценка сложности геометрических построений,...

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconРабочая учебная программа по дисциплине «Литература Швейцарии» для специальности «050303- иностранный язык» по циклу опд. В2 дисциплины по выбору Очная форма обучения
Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconПрограмма курса для студентов специальности 1-31 01 01-02 математика 1-31 03 03-02 прикладная математика
Автор: Касперко М. В., старший преподаватель кафедры алгебры, геометрии и методики преподавания математики ГрГУ

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconРабочая программа по дисциплине "Дерматовенерология" для специальности «Кожные и венерические болезни» 350500 Социальная работа
Рабочая программа составлена с учетом требований Государственного образовательного стандарта высшего профессионального образования...

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconПрограмма дисциплины Русский язык и культура речи для направления 010400. 62 «Прикладная математика и информатика»
Государственное образовательное бюджетное учреждение высшего профессионального образования

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconРабочая учебная программа по дисциплине «Концепции современного естествознания» для студентов факультета клинической психологии для специальности 030302 «Клиническая психология» Кафедра философии, биомедицинской этики и гуманитарных наук
Рабочая программа составлена в соответствии с требованиями Государственного образовательного стандарта профессиональной подготовки...

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconГрафик проведения встреч со студентами университета первого года обучения
Студенты направлений подготовки 140800 «Ядерные физика и технологии», 011200 «Физика», 223200 «Техническая физика», 010400 «Прикладная...

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconРабочая программа дисциплины: " математика и архитектура" для специальности
Государственное образовательное учереждение среднего профессионального оброзования

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconРабочая программа составлена на основе типовой учебной программы для высших учебных заведений по специальности 1-31 03 01 "Математика (по направлениям)", утверждённой 29. 12. 2008 г. Рег.№ Тд g. 161 / тип
Рабочая программа составлена на основе типовой учебной программы для высших учебных заведений по специальности 1-31 03 01 “Математика...

Рабочая программа по дисциплине «синтез программ» для специальности 010200 Прикладная математика и информатика Форма обучения: очная iconРабочая программа составлена на основе типовой учебной программы для высших учебных заведений по специальности 1-31 03 01 "Математика (по направлениям)", утверждённой 29. 12. 2008 г. Рег.№ Тд g. 161 / тип
Рабочая программа составлена на основе типовой учебной программы для высших учебных заведений по специальности 1-31 03 01 “Математика...

Размесціце кнопку на сваім сайце:
be.convdocs.org


База данных защищена авторским правом ©be.convdocs.org 2012
звярнуцца да адміністрацыі
be.convdocs.org
Галоўная старонка