Математическая Логика, 06 семинар (от 05 декабря)

Материал из eSyr's wiki.

(Различия между версиями)

Перейти к: навигация, поиск

Текущая версия

Предыдущий семинар | Следующий семинар

Содержание

1 Задача 4.5
- 1.1 Решение
2 Задача 4.6
- 2.1 Решение
3 Расширение возможностей логического программирования
4 Домашнее задание
- 4.1 Задача 4.9
  - 4.1.1 Решение
5 Предикаты, расширяющие вычислительные возможности логических программ

[править] Задача 4.5

Проверить вхождение одного списка в другой в качестве подсписка.

? check_sublist(x,y)

[править] Решение

check_sublist(nil, x) ← ;
check_sublist(x, x) ← ;
check_sublist(x₁ . x, x₁ . y) ← check_sublist(x, y);
check_sublist(x₁ . x, y₁ . y) ← x₁ ≠ y₁, check_sublist(x₁ . x, y);

[править] Задача 4.6

Обратить список.

? reverse(x,y)

[править] Решение

reverse(nil, nil) ← ;
reverse(x . y, z) ← reverse(y, z₁), concat(z₁, x . nil, z);

[править] Расширение возможностей логического программирования

Повышение удобства работы.

[править] Встроенные предикаты

Некоторые выражения удобно вычислять без использования SLR-резолюции.

[править] Отношение равенства

Отношение равенства: =⁽²⁾ — двуместный предикат.

Пример записи: t₁ = t₂

Что подразумевает равенство? Если интерпретатор видит, что очередной подцелью является равенство, то он пытается найти наиболее общий унификатор (НОУ), и, если он есть, то это успех. Другими словами, решается уравнение t₁ = t₂.

Например, x + 2 = 3 + y, НОУ — {^x/₃, ^y/₂} — успех
Другой пример — 2 + 3 = 5, НОУ(2 + 3, 5) = ∅, синтаксического совпадения не будет (требуется решение в свободной алгебре термов, без интерпретации)

[править] Тождество

Тождество: ==⁽²⁾

Он круче. Будет успех, если t₁ совпадает с t₂.

[править] Неравенство

Неравенство: ≠⁽²⁾

Разрешаетя успешно, если нет НОУ.

[править] Нетождество

Нетождество: =/=⁽²⁾

Разрешается успешно с пустой подстановкой, если t₁ и t₂ синтаксически различны.

[править] Задача 4.8 (использование предиката нетождество)

Построить пересечение множеств, представленных бесповторными списками.

? common(x,y,z)

[править] Решение

common(nil, L, nil) ← ;
common(L, nil, nil) ← ;
common(x . L₁, L₂, x . L₃) ← elem(x, L₂), common(L₁, L₂, L₃);
common(x . L₁, L₂, L₃) ← nonelem(x, L₂), common(L₁, L₂, L₃);

nonelem(x, y . z) ← x =/= y, nonelem(x, z);
nonelem(x, nil) ← ;

[править] Задача 4.10 (введение дооплнительных функций для хранения вспомогательной информации)

Построитьсписок L2,состоящий из тех и только тех элементов списка L1, которые содержатся в нем однократно.

? single(L1,L2)

[править] Решение

Казалось бы, решение должно быть таким:

single(x . L1, x . L2) ← nonelem(x, L1), single(L1, L2);
single(x . L1, L2) ← elem(x, L1), single(L1, L2);
single(nil, nil) ← ;

Но эта программа решает дргую задачу — построение списка, в котором каждый из элементов списка L1 входит ровно один раз. На самом деле, правильное решение следующее:

single(L₁, L₂) ← R(L₁, nil, L₂);
R(nil, L₂, nil) ← ;
R(x . L₂, L₂, x . L₃) ← nonelem(x, L₁), nonelem(x, L₂), R(L₁, L₂, L₃);
R(x . L₁, L₂, L₃) ← elem(x, L₁), R(L₁, x . L₂, L₃)
R(x . L₁, L₂, L₃) ← elem(x, L₂), R(L₁, L₂, L₃);

В этом решении вводится дополнительный список, в котором хранятся те элементы, котрые входят в L₁ более одного раза. Для хранения этого списка вводится дополнительная функция R, где он передаётся в качестве параметра.

[править] Домашнее задание

Задача 4.9

[править] Задача 4.9

Построить список L3, состоящий из всех тех и только тех элементов списка L1, которые не содержатся в списке L2

? sieve(L1 ,L2, L3)

[править] Решение

sieve(L1, nil, L1) ← ;
sieve(x . L1, L2, x . L3) ← nonelem(x, L2), nonelem(x, L3), sieve(L1, L2, L3);
sieve(x . L1, L2, L3) ← sieve(L1, L2, L3);

[править] Предикаты, расширяющие вычислительные возможности логических программ

[править] Предикаты сравнения

Для данных типа INTEGER разумно ввести операции сравнения: <, ≤, ≥, >. Тогда мы должны описать операционную семантику. Если текущая подцель — сравнение, то тогда он спрашивает, а правда ли, что t₁, t₂ — числа, и если числа, то правда, что выполняется отношение сравнения для этих чисел? Если да, то успех с пустой подстановкой.

Пример:

? 2 ≤ 3 → success
? x ≤ x + 1 → failure — сравнивать можно только чилса
1 ≤ 2 + 3 → failure; — в правой части — выражение

[править] Задача 1.1 (применение функций сравнения)

Проверить, является ли заданный целочисленный список L упорядоченным.

? ordered(L)

[править] Решение

ordered(nil) ← ;
ordered(x . nil) ← ;
ordered(x . y . L) ← x ≤ y, ordered(y . L);

[править] Задача 1.2

Для заданного целочисленного списка L отыскать его наибольший элемент.

? max(L,x)

[править] Решение

max(x . nil, x) ← ;
max(x . L, x) ← max(L, y), y ≤ x;
max(x . L, y) ← max(L, y), x < y;

Подсчитаем количество операций. В худшем случае их будет 2^len(L). Если мы модифицируем решение (сделав рекурсию хвостовой), то получим линейную сложность:

max(x . nil, x) ← ;
max(x . L, y) ← max3(L, x, y);
max3(nil, x, x) ←
max3(x . L, y, z) ← x ≤ y, max3(L, y, z);
max3(x . L, y, z) ← max3(L, x, z);

Если нужны дополнительные переменные, которые хранят накапливаемые данные, то введите дополнительные предикаты.

[править] Вычислительные функции

Есть функции +, −, ×, div, mod, … Но их надо заставить вычислиться.

Предикат, который занимается вычислениями: is⁽²⁾

? t₁ is t₂
   ↓ {^t₁/_val(t₂)}
success

Спецификация операционной семантики:

t₁ ∈ Var
t₂ — арифметическое выражение, имеющеезначение, которое можно вычислить (val(t₂))
Выполнить подстановку ^t₁/_val(t₂)

Пример:

? x is 3 × (2 + 1)
   ↓ {^x/₉}
success

? x is y + 1
failure

y — переменная, у неё неопределённое значение

? x is x + 1
failure

? y = 3 + 2, z + 1 = 4 + u, x is z + y
   ↓ {^y/_{3 + 2}}
? z + 1 = 4 + u, x is z + (3 + 2)
   ↓ {^z/₄, ^u/₁}
? x is 4 + (3 + 2)
   ↓ {^x/₉}
success

[править] Задача 2.2 (Применение арифметических предикатов)

Вычисления суммы элементов целочисленного списка L.

? sum(L,x)

[править] Решение

sum(nil, 0) ← ;
sum(x . l, y) ← sum(L, z), y is x + z;

Математическая Логика

Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16

Календарь

Сентябрь	24	25	26
Октябрь	02	03	10	17	24	31
Ноябрь	07	14	21	28
Декабрь	05	12	19

Семинары

01 02 03 04 05 06 07

Календарь

Сентябрь	26
Октябрь	10	24
Ноябрь	07	21
Декабрь	05	19

Ссылки
Официальная страница курса | Задачи
Проведение экзамена | Решение задач: Решение задач методички | Решение задач варианта экзамена 2004 года | Алгоритмы решения задач

Эта статья является конспектом лекции.

Получено с http://esyr.org/wiki/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D0%9B%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%2C_06_%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%28%D0%BE%D1%82_05_%D0%B4%D0%B5%D0%BA%D0%B0%D0%B1%D1%80%D1%8F%29

Категории: Математическая Логика | Лекции

@@ Строка 1: / Строка 1: @@
-== From Ebaums Inc to MurkLoar. ==
+[[Математическая Логика, 05 семинар (от 21 ноября)|Предыдущий семинар]] | [[Математическая Логика, 07 семинар (от 19 декабря)|Следующий семинар]]
-We at EbaumsWorld consider you as disgrace of human race.
-Your faggotry level exceeded any imaginable levels, and therefore we have to inform you that your pitiful resourse should be annihilated.
+=== Задача 4.5 ===
-Dig yourself a grave - you will need it.
+Проверить вхождение одного списка в другой в качестве подсписка.
+ ? check_sublist(x,y)
+==== Решение ====
+ check_sublist(nil, x)&nbsp;&larr;&nbsp;;
+ check_sublist(x, x)&nbsp;&larr;&nbsp;;
+ check_sublist(x<sub>1</sub> . x, x<sub>1</sub> . y)&nbsp;&larr;&nbsp;check_sublist(x, y);
+ check_sublist(x<sub>1</sub> . x, y<sub>1</sub> . y)&nbsp;&larr;&nbsp;x<sub>1</sub> &ne; y<sub>1</sub>, check_sublist(x<sub>1</sub> . x, y);
+=== Задача 4.6 ===
+Обратить список.
+ ? reverse(x,y)
+==== Решение ====
+ reverse(nil, nil)&nbsp;&larr;&nbsp;;
+ reverse(x . y, z)&nbsp;&larr;&nbsp;reverse(y, z<sub>1</sub>), concat(z<sub>1</sub>, x . nil, z);
+== Расширение возможностей логического программирования ==
+Повышение удобства работы.
+=== Встроенные предикаты ===
+Некоторые выражения удобно вычислять без использования SLR-резолюции.
+==== Отношение равенства ====
+Отношение равенства: =<sup>(2)</sup> — двуместный предикат.
+Пример записи: t<sub>1</sub> = t<sub>2</sub>
+Что подразумевает равенство? Если интерпретатор видит, что очередной подцелью является равенство, то он пытается найти наиболее общий унификатор (НОУ), и, если он есть, то это успех. Другими словами, решается уравнение t<sub>1</sub> = t<sub>2</sub>.
+* Например, x + 2 = 3 + y, НОУ — {<sup>x</sup>/<sub>3</sub>, <sup>y</sup>/<sub>2</sub>} — успех
+* Другой пример — 2 + 3 = 5, НОУ(2 + 3, 5) = &empty;, синтаксического совпадения не будет (требуется решение в свободной алгебре термов, без интерпретации)
+==== Тождество ====
+Тождество: ==<sup>(2)</sup>
+Он круче. Будет успех, если t<sub>1</sub> совпадает с t<sub>2</sub>.
+==== Неравенство ====
+Неравенство: &ne;<sup>(2)</sup>
+Разрешаетя успешно, если нет НОУ.
+==== Нетождество ====
+Нетождество: =/=<sup>(2)</sup>
+Разрешается успешно с пустой подстановкой, если t<sub>1</sub> и t<sub>2</sub> синтаксически различны.
+=== Задача 4.8 (использование предиката нетождество) ===
+Построить пересечение множеств, представленных бесповторными списками.
+ ? common(x,y,z)
+==== Решение ====
+ common(nil, L, nil)&nbsp;&larr;&nbsp;;
+ common(L, nil, nil)&nbsp;&larr;&nbsp;;
+ common(x . L<sub>1</sub>, L<sub>2</sub>, x . L<sub>3</sub>)&nbsp;&larr;&nbsp;elem(x, L<sub>2</sub>), common(L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>);
+ common(x . L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>)&nbsp;&larr;&nbsp;nonelem(x, L<sub>2</sub>), common(L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>);
+ nonelem(x, y . z)&nbsp;&larr;&nbsp;x =/= y, nonelem(x, z);
+ nonelem(x, nil)&nbsp;&larr;&nbsp;;
+=== Задача 4.10 (введение дооплнительных функций для хранения вспомогательной информации) ===
+Построитьсписок L2,состоящий из тех и только тех элементов списка L1, которые содержатся в нем однократно.
+ ? single(L1,L2)
+==== Решение ====
+Казалось бы, решение должно быть таким:
+ single(x . L1, x . L2)&nbsp;&larr;&nbsp;nonelem(x, L1), single(L1, L2);
+ single(x . L1, L2)&nbsp;&larr;&nbsp;elem(x, L1), single(L1, L2);
+ single(nil, nil)&nbsp;&larr;&nbsp;;
+Но эта программа решает дргую задачу — построение списка, в котором каждый из элементов списка L1 входит ровно один раз.
+На самом деле, правильное решение следующее:
+ single(L<sub>1</sub>, L<sub>2</sub>)&nbsp;&larr;&nbsp;R(L<sub>1</sub>, nil, L<sub>2</sub>);
+ R(nil, L<sub>2</sub>, nil)&nbsp;&larr;&nbsp;;
+ R(x . L<sub>2</sub>, L<sub>2</sub>, x . L<sub>3</sub>)&nbsp;&larr;&nbsp;nonelem(x, L<sub>1</sub>), nonelem(x, L<sub>2</sub>), R(L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>);
+ R(x . L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>)&nbsp;&larr;&nbsp;elem(x, L<sub>1</sub>), R(L<sub>1</sub>, x . L<sub>2</sub>, L<sub>3</sub>)
+ R(x . L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>)&nbsp;&larr;&nbsp;elem(x, L<sub>2</sub>), R(L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>);
+В этом решении вводится дополнительный список, в котором хранятся те элементы, котрые входят в L<sub>1</sub> более одного раза. Для хранения этого списка вводится дополнительная функция R, где он передаётся в качестве параметра.
+== Домашнее задание ==
+Задача 4.9
+=== Задача 4.9 ===
+Построить список L3, состоящий из всех тех и только тех элементов списка L1, которые не содержатся в списке L2
+ ? sieve(L1 ,L2, L3)
+==== Решение ====
+ sieve(L1, nil, L1) &larr; ;
+ sieve(x . L1, L2, x . L3) &larr; nonelem(x, L2), nonelem(x, L3), sieve(L1, L2, L3);
+ sieve(x . L1, L2, L3) &larr; sieve(L1, L2, L3);
+== Предикаты, расширяющие вычислительные возможности логических программ ==
+=== Предикаты сравнения ===
+Для данных типа INTEGER разумно ввести операции сравнения: &lt;, &le;, &ge;, &gt;. Тогда мы должны описать операционную семантику. Если текущая подцель — сравнение, то тогда он спрашивает, а правда ли, что t<sub>1</sub>, t<sub>2</sub> — числа, и если числа, то правда, что выполняется отношение сравнения для этих чисел? Если да, то успех с пустой подстановкой.
+Пример:
+* ? 2 &le; 3 &rarr; success
+* ? x &le; x + 1 &rarr; failure — сравнивать можно только чилса
+* 1 &le; 2 + 3 &rarr; failure; — в правой части — выражение
+=== Задача 1.1 (применение функций сравнения) ===
+Проверить, является ли заданный целочисленный список L упорядоченным.
+ ? ordered(L)
+==== Решение ====
+ ordered(nil)&nbsp;&larr;&nbsp;;
+ ordered(x . nil)&nbsp;&larr;&nbsp;;
+ ordered(x . y . L)&nbsp;&larr;&nbsp;x &le; y, ordered(y . L);
+=== Задача 1.2 ===
+Для заданного целочисленного списка L отыскать его наибольший элемент.
+ ? max(L,x)
+==== Решение ====
+ max(x . nil, x)&nbsp;&larr;&nbsp;;
+ max(x . L, x)&nbsp;&larr;&nbsp;max(L, y), y &le; x;
+ max(x . L, y)&nbsp;&larr;&nbsp;max(L, y), x &lt; y;
+Подсчитаем количество операций. В худшем случае их будет 2<sup>len(L)</sup>. Если мы модифицируем решение (сделав рекурсию хвостовой), то получим линейную сложность:
+ max(x . nil, x) &larr; ;
+ max(x . L, y) &larr; max3(L, x, y);
+ max3(nil, x, x) &larr;
+ max3(x . L, y, z) &larr; x &le; y, max3(L, y, z);
+ max3(x . L, y, z) &larr; max3(L, x, z);
+Если нужны дополнительные переменные, которые хранят накапливаемые данные, то введите дополнительные предикаты.
+=== Вычислительные функции ===
+Есть функции +, &minus;, &times;, div, mod, … Но их надо заставить вычислиться.
+Предикат, который занимается вычислениями: is<sup>(2)</sup>
+ ? t<sub>1</sub> is t<sub>2</sub>
+    &darr; {<sup>t<sub>1</sub></sup>/<sub>val(t<sub>2</sub>)</sub>}
+ success
+Спецификация операционной семантики:
+# t<sub>1</sub> &isin; Var
+# t<sub>2</sub> — арифметическое выражение, имеющеезначение, которое можно вычислить (val(t<sub>2</sub>))
+# Выполнить подстановку <sup>t<sub>1</sub></sup>/<sub>val(t<sub>2</sub>)</sub>
+Пример:
+ ? x is 3 &times; (2 + 1)
+    &darr; {<sup>x</sup>/<sub>9</sub>}
+ success
+ ? x is y + 1
+ failure
+y — переменная, у неё неопределённое значение
+ ? x is x + 1
+ failure
+ ? y = 3 + 2, z + 1 = 4 + u, x is z + y
+    &darr; {<sup>y</sup>/<sub>3 + 2</sub>}
+ ? z + 1 = 4 + u, x is z + (3 + 2)
+    &darr; {<sup>z</sup>/<sub>4</sub>, <sup>u</sup>/<sub>1</sub>}
+ ? x is 4 + (3 + 2)
+    &darr; {<sup>x</sup>/<sub>9</sub>}
+ success
+=== Задача 2.2 (Применение арифметических предикатов) ===
+Вычисления суммы элементов целочисленного списка L.
+ ? sum(L,x)
+==== Решение ====
+ sum(nil, 0) &larr; ;
+ sum(x . l, y) &larr; sum(L, z), y is x + z;
+{{Математическая Логика}}

Математическая Логика, 06 семинар (от 05 декабря)

Материал из eSyr's wiki.

Текущая версия

Содержание

[править] Задача 4.5

[править] Решение

[править] Задача 4.6

[править] Решение

[править] Расширение возможностей логического программирования

[править] Встроенные предикаты

[править] Отношение равенства

[править] Тождество

[править] Неравенство

[править] Нетождество

[править] Задача 4.8 (использование предиката нетождество)

[править] Решение

[править] Задача 4.10 (введение дооплнительных функций для хранения вспомогательной информации)

[править] Решение

[править] Домашнее задание

[править] Задача 4.9

[править] Решение

[править] Предикаты, расширяющие вычислительные возможности логических программ

[править] Предикаты сравнения

[править] Задача 1.1 (применение функций сравнения)

[править] Решение

[править] Задача 1.2

[править] Решение

[править] Вычислительные функции

[править] Задача 2.2 (Применение арифметических предикатов)

[править] Решение

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты