Логическое и функциональное программирование (стр. 8 из 16)

Множество D, рассматриваемое с позиций логики предикатов, называется областью переменных.

Значения ППФ оцениваются следующим образом:

1. Если известны значения логических формул F и G, то значения

оцениваются по таблице истинности.

2. Если для всех xÎMF оценивается как истина, то истиной является ("x)F(x).

3. Если хотя бы для одного xÎMF оценивается как истина, то ($x)F(x) тоже истина.

Предложения

Когда все переменные предиката являются связанными, то такой предикат называется предложением. Различие между ППФ, являющимися и не являющимися предложениями, состоит в том, что предложениям можно однозначно поставить в соответствие значение True или False, в то время как во втором случае нельзя непосредственно по виду формулы вынести суждение об ее истинности или ложности. Например, предикатная формула подсистема (x, y) не является предложением. Если в нее подставлены определенные значения, например, x = процессор, y = ЭВМ, то выражение подсистема (процессор, ЭВМ) принимает значение True, а при подстановке x = человек, выражение подсистема(человек, ЭВМ) является False. То есть истинность или ложность предикатной формулы можно оценить тогда и только тогда, когда в переменные подставлены некоторые конкретные сущности (в этом случае формула называется высказыванием). Отметим, что значение предикатных формул со связанными переменными можно определить, и не производя такого рода подстановки.

Например,

- у каждого человека имеется отец – является истиной, а - любой является чьим-то отцом – является ложью.

Предположим, что имеется некоторое множество логических формул S. Если существует такая интерпретация, что все эти формулы принимают значение истина, то подобная интерпретация называется моделью. Например, рассмотрим множество:

Тогда интерпретация вида (человек (Сократ) = True) и (смертен (Сократ) = True) – является моделью так как все логические формулы S есть истина. Не обязательно, что такая модель единственна.

Пусть имеется некоторая группа S логических формул. Если для всех моделей S некоторая логическая формула s есть истина, то принято говорить, что s является логическим заключением (консеквентом) в S. Факт реализации логического консеквента записывается в виде S½=s.

Правила вывода логики предикатов

Вывод представляет собой процедуру, которая из заданной группы выражений выводит, отличное от заданного выражение. Когда группа выражений, образующих посылку, является истиной, то должно гарантироваться, что выражение, выведенное из них в соответствии с правилом вывода, также является истиной.

В логике предикатов в качестве такого правила вывода используется правило, которое из двух выражений A и A®Bвыводит новое выражение B. Это правило называется правилом дедуктивного вывода.

Для описаний правил вывода во многих случаях используется нотация (как это указывалось выше), при которой над чертой записывается группа выражений, принимаемых за посылку, а под чертой – выражение, которое выводится:

Такой тип правила вывода носит название modusponens.

Можно многократно использовать одно и тоже правило вывода. Например, если помимо выражений A, A®B существует выражение B®C, то можно вывести C, дважды использовав приведенное правило. Получение выражения s применением конечного числа раз правила вывода к заданной группе выражений S будем записывать в виде:

При этом говорят, что s дедуктивно выводится из S. Очевидно, что из вышеуказанного, легко выводится еще одно правило:

Практические задания

Задание 1. Задан предикат выполнение(x, y) , который задает отношение «y является результатом выполнения программы x». Дать интерпретацию утверждений:

("x)($y)выполнение(x,y);

($x)("y) выполнение(x,y);

("x)("y) выполнение(x,y);

($x)("y) выполнение(x,y);

("y)($x) выполнение(x,y);

($x)($y) выполнение(x,y).

Задан предикат реализация(x, y), который означает «программа x реализована на языке y». Записать утверждения:

А) Существует программа, реализованная на Паскале, имеющая в качестве результата 1000.

Б) Любая программа, написанная на C, дает результат.

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

Функциональное программирование представляет собой модель индуктивного вывода, реализуемую с помощью рекурсивных процедур, l-исчисления и списковых структур.

3.1Индуктивный вывод

Индуктивный вывод – это вывод из имеющихся данных, объясняющего их общего правила. Например, пусть известно, что есть некоторая функция от одной переменной. Рассмотрим как выводится f(x), если последовательно задаются в качестве данных пары значений (1, f(0)), (1, f(1)). Вначале задается (0, 1) и имеет смысл ввести постоянную функцию f(x) = 1. Затем задается пара (1, 1), которая удовлетворяет f(x)=1. Следовательно, нет необходимости менять вывод. Пусть теперь задается (2, 3). Это не согласуется с нашим выводом. Предположим, что методом проб и ошибок удается найти

. Она удовлетворяет заданным до сих пор фактам. Далее, если будут следовать факты (3, 7), (4, 13), (5, 21), …, убедимся в справедливости предшествующего вывода. Таким образом в индуктивном выводе в каждый момент времени объясняются все данные, полученные до этого момента. Если данные, позже, перестанут удовлетворять полученному выводу, то его придется менять. Следовательно, индуктивный вывод – это неограниченно долгий процесс.

Для определения индуктивного вывода необходимо уточнить:

1. Множество правил объектов вывода.

2. Метод представления правил.

3. Способ показа примеров.

4. Метод вывода.

5. Критерий правильности вывода.

В качестве правил – объектов вывода можно рассматривать:

- функции;

- грамматики языков;

- программы.

Метод представления удобно организовывать в виде пар (x, f(x)), последовательности действий, вычисляющих f(x) и т.д.

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

Запрос входных данных ® предположение ® выходные данные.

Критерием правильности вывода считается идентификация в пределе. Говорят, что машина вывода M идентифицирует в пределе правило R, если при показе примеров правилу R последовательность выходных данных, генерируемых M, сходится к некоторому представлению t, а именно: все выходные данные, начиная с некоторого момента времени, совпадают с t, при этом t называют правильным представлением R. Кроме того, говорят, что множество правил G позволяет сделать индуктивный вывод, если существует некоторая машина вывода M, которая идентифицирует в пределе любое правило R из множества G.

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

3.1.1Математическая индукция

Методом математической индукции называются утверждения вида:

Пусть переменная n имеет область N (натуральные числа). Чтобы доказать первое утверждение, достаточно доказать два утверждения:

(4)

(5)

Первое из этих утверждений называется базисом индукции, второе - индукционным шагом. Для доказательства второго утверждения берут произвольное натуральное число, обозначают его какой-либо буквой, скажем k, и доказывают импликацию:

U(k) ®U(k+1) (6)

Как следует из определения квантора общности, доказав это получим (5). Для доказательства (6) предполагают, что истинна посылка:

U(k) (7)

и выводят из этого предположения, что истинно ее заключение U(k+1). Утверждение (7) называется предположением индукции.

При доказательстве утверждения (2) базисом индукции является утверждение U(a), индукционным шагом – ("n³a)(U(n)®U(n+1)), предположением индукции – утверждение U(k), где k – произвольное натуральное число большее или равное a.

При доказательстве утверждения (3) базисом индукции является утверждение U(a), индукционным шагом – утверждение ("n:a£n<b)(U(n)®U(n+1)), предположением индукции U(k), где k – произвольное натуральное число такое, что a£n<b. Такая индукция называется индукцией по интервалу. От индукции по интервалу можно перейти к индукции спуска. Индукцией спуска называется индукция, базисом которой является утверждение U(b), индукционным шагом – утверждение ("n:a£n<b)(U(n+1)®U(n)). Предположением индукции в этой форме является утверждение U(k+1), где k – произвольное натуральное число такое, что a£n<b.

Иногда утверждение 1 удобно доказывать возвратной индукцией. Возвратная индукция - это индукция с базисом U(1), но с индукционным шагом ("n)("m£n)(U(m) ®U(n)). Предположением индукции является ("m<k)U(m), где k – произвольное натуральное число. Возвратная индукция с измененным базисом и индукционным шагом применяется и при доказательстве утверждений 2 и 3.