3.

Докажем эту равносильность.

В этой выкладке мы опирались на следующее утверждение:

Определение ППФ и семантика логики предикатов

Комбинируя два типа символов, можно рекурсивно определить составную формулу логики предикатов, называемую правильно построенной формулой (ППФ) или логической формулой.

1. Атомарный предикат является ППФ.

2. Если F и G являются ППФ, то также ППФ.

3. Если F(x) - ППФ, то (x)F(x) и (x)F(x) - ППФ.

4. Все результаты, полученные применением конечного числа раз (1) - (3) являются ППФ. Ничто другое не является ППФ.

Формулы логики предикатов строятся безотносительно к понятиям задаваемой предметной области. Если решено, что этими формулами будет описываться конкретная предметная область, то должно быть установлено соответствие между понятиями предметной области и этими формулами. Это предполагает следующие действия:

1. Устанавливаются соответствия между константами логики предикатов и сущностями этой области. Константы Имена объектов.

2. Устанавливаются соответствия между формулами и функциональными отношениями предметной области.

3. Устанавливаются соответствия между атомарными предикатами и концептуальными отношениями предметной области.

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

1. Задается непустое множество D, определяющее сущности рассматриваемой предметной области, и элементы из D определяются как константы или переменные.

2. Для функций (функциональные отношения), определенных на множестве аргументов от до D назначаются функциональные символы.

3. Каждому предикату n переменных назначается отношение, определенное на Dⁿ, и его значение - True или False.

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

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

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

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

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

Предложения

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

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

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

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

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

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

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

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

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

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

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

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

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

Задание 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. Функциональное программирование

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

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, сходится к некоторому представлению , а именно: все выходные данные, начиная с некоторого момента времени, совпадают с , при этом называют правильным представлением 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), индукционным шагом - (na)(U(n)U(n+1)), предположением индукции - утверждение U(k), где k - произвольное натуральное число большее или равное a.

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

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

Для доказательства утверждений 1-3 часто бывает удобной индукция с двойным базисом, то есть для случая 1 индукция с базисом U(1)U(2) и индукционным шагом (n) ((U(n)U(n+1))U(n+2)). Иногда удобно применять индукцию с тройным, четырехкратным и т.д. базисом.

Для доказательства утверждений вида

(8)

применяется индукция по двум переменным. Однако, утверждение (8) часто удается свести к индукции по одной переменной. Для этого формируем в качестве значения переменной m произвольное число и обозначаем его а. Докажем утверждение (n)U(a,n). Из этого утверждения очевидно следует (8). Но последнее утверждение имеет вид 1 и его можно доказать индукцией. При такой схеме n называется индукционной переменной. Говорят также, что (8) доказывается по n при фиксированном m.

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

1.Требуется найти ошибку в доказательстве того, что натуральные числа равны между собой.

Пусть A переменная с областью определения R(N) (множества натуральных чисел), n - переменная с областью определения N (натуральные числа). Обозначим через U(A, n) высказывание: «Если множество A содержит n элементов, то в A нет двух неравных натуральных чисел». Очевидно, утверждение



равносильно утверждению задачи.

Докажем утверждение (1) индукцией по n, причем индукцию будем применять в ее простейшей форме. Базисом индукции является:

(A)U(A,1). (2)

Докажем (2). Возьмем произвольное MN и докажем

U(M,1). (3)

Тем самым будет доказано утверждение (2). Но на основе определения U, (3) утверждает: «Если множество M содержит один элемент, то в M нет двух неравных натуральных чисел», что очевидно. Предположим теперь в качестве предположения индукции, что (A)U(A,n) верно для некоторого натурального k, то есть, что верно

(A)U(A,k) (4)

и докажем, что верно

(A)U(A,k+1) (5)

Тем самым утверждение (1) будет доказано. Для доказательства (5) возьмем произвольное MN и докажем

U(M,k+1) (6)

Тем самым (5) будет доказано. На основе определения U, (6) есть утверждение: «Если множество M содержит k+1 элементов, то в M нет двух неравных натуральных чисел». Чтобы доказать эту импликацию, предположим, что ее посылка верна. Пронумеруем как-нибудь элементы множества M. Пусть, например:

Докажем, что в множестве M нет двух неравных натуральных чисел. Тем самым доказательство будет закончено. Рассмотрим два вспомогательных множества:

Каждое из них получено выбрасыванием из M одного элемента и, следовательно, содержит k элементов. В силу предположения индукции (4) U(K,k) - «Если множество K содержит k элементов, то в K нет двух неравных натуральных чисел». Но множество K как раз содержит k элементов, следовательно, в нем нет двух неравных натуральных чисел. Отсюда:

(7)

Используем еще раз предположение индукции (4). Возьмем теперь в качестве значения A множество L. Теперь из (4) получим утверждение U(L,k), что означает: «Если множество L содержит k элементов, то в нем нет двух неравных натуральных чисел». Но множество L содержит как раз k элементов, следовательно, в нем нет двух неравных натуральных чисел. В частности:

(8)

Из (7) и (8) следует, что в M нет двух неравных натуральных чисел. Доказательство закончено.

3.2 Рекурсия

Особое место для систем функционального программирования приобретает рекурсия, поскольку она позволяет учитывать значения функции на предыдущих шагах.

С теоретической точки зрения рекурсивные определения являются теоретической основой всей современной теории вычислимых функций. Рассмотрим два способа вычисления f(1)+f(2)+…+f(n). При итерации сделаем следующим образом. Определим подпрограмму:

Sub Add(S,k,f)

S=S+f

k=k-1

End Sub

Тогда процедуру без использования цикла можно определить следующим образом:

S=0

k=n

I: Add(S,k,f(k))

J: If k0 Then Goto I

Здесь подпрограмма Add выполняется n раз последовательно и независимо, причем каждый раз используется только одна команда возврата. Это итерация.

Для рекурсии построим функцию:

If k=0 Then

Sum(f,k)=0

Else

Sum(f,k)=f(k)+Sum(f,k-1)

End If

Теперь достаточно просто узнать значение Sum(f,n). Рассмотрим частный случай при n=2. Из определения следует, что необходимо вычислить f(2), а затем обратиться к вычислению Sum(f,1), результат вычисления которого должен быть прибавлен к f(2). Следовательно, сохранить в памяти f(2), установить еще один возврат и обратиться еще один раз к нашему определению. Теперь вычисляем f(1), снова запоминаем результат в памяти, устанавливаем третий возврат и в третий раз обращаемся к определению для вычисления Sum(f,0). Последняя функция равна 0, и мы выходим из определения, используя возврат, установленный перед обращением к определению. Далее прибавляем 0 к f(1), снова выходим из определения, используя второй возврат, прибавляем 0+f(1) к f(2) и производим окончательный выход. Это рекурсия. Определение Sum использовалось не последовательно и независимо, а с вложением последующего использования в предыдущее (что характерно для индуктивного вывода), три команды возврата одновременно хранились в памяти и использовались по принципу «последний пришел - выполнился первый» (LIFO).

Здесь мы рассмотрели пример простой рекурсии. Другим более сложным примером рекурсии является вычисление чисел Фибоначчи. Их можно определить с помощью следующих формул:

Формально число Фибоначчи можно вычислить по следующей явной формуле:

F(n) = [(1 + 5)ⁿ - (1 - 5)ⁿ] / (2ⁿ 5).

Эта формула относительно сложна. На самом деле в этом виде задача даже полностью не решена, поскольку алгоритм использования формулы требуется уточнить. Например, осуществлять ли раскрытие внутренних скобок по формуле бинома? Какое значение брать для числа 5, то есть сколько брать десятичных знаков? Очевидно, что хотя результат должен быть целым, он не будет таковым. Следовательно, встает вопрос, до какого соседнего целого нужно округлять? Как быть при этом уверенным в результате?

Для этой задачи можно использовать решение с непосредственной подстановкой:

Sub F(n)

If n > 2 Then

F(n) = F(n - 1) + F(n - 2)

Else

F(n) = 1

End If

End Sub

Для приведенных выше функций существуют алгебраические выражения, по которым их можно вычислить. Поэтому, используемые для них рекурсии, будем называть простыми. Однако, существуют функции, которые не являются простыми рекурсиями. Эти функции можно определить рекурсивно, но нельзя записать в терминах алгебраических выражений. Характерным примером является функция Аккермана. Пытаясь определить эту функцию алгебраически, получим только последовательность экспонент, записанных через многоточие. С другой стороны существует простая запись этой функции через рекурсию:

A(m,n)=iif(m=0,n+1,iif(n=0,A(m-1,1),A(m-1,A(m,n-1)))).

Вообще говоря, вычисление таких функций может быть бесконечным (характерная особенность индуктивного вывода). В качестве примера приведем функцию f(m,n), результатом которой является 1 в случае, если в десятичной записи числа встречается фрагмент из последовательности повторяющихся цифр m длиной n.

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

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

f(…g(…,f,…,f,…)).

Рекурсия является взаимной между двумя или более функциями, если они вызывают друг друга, то есть когда в определении функции f вызывается функция g, которая в свою очередь содержит вызов функции g:

f((…)(…g…));

g((…)(…f…)).

Рекурсия более высокого порядка является рекурсией, в которой аргументом рекурсивного вызова является рекурсивный вызов:

f(…f(…f…)…).

3.2.1 Компьютерное задание

Дана последовательность символов a1, a2, …, an. С применением рекурсии реализовать процедуру инверсии данной последовательности, то есть процедуру получения последовательности b1, b2, …, bn такой, что b1 = an, b2 = an-1, …, bn-1 = a2, bn = a1.

3.3 -исчисление

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

В выражении

буква x может быть заменена любой другой буквой (за исключением t или f) и смысл выражения от этого не изменится в любом контексте, где это выражение может быть использовано.

В определении функции вида:

… где g(x) = a sin(px + q)

буква x также пуста.

С точки зрения вычислительной математики возникает проблема, является ли x именем объекта (областью рабочей памяти) или нет; или x - это объект, значением которого является другое имя. Этот вариант может иметь дальнейшее развитие, когда фактический параметр в g(x) является выражением отличным от простой переменной, например, как в записи g(t² + 2).

Очевидно, что в основе лежит вопрос определения функций. Для этих целей в 1941 году Черчем было введено -исчисление. Задать функцию - это означает указать закон соответствия, приписывающий значение функции каждому допустимому значению аргумента. Пусть M - некоторая формула, содержащая x в качестве свободной переменной. Тогда x.[M] есть функция, значение которой для любого аргумента получается подстановкой этого аргумента в M вместо x. Операцию образования выражения x.[M] из M и x называют - операцией или функциональной абстракцией.

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

Основным понятием является понятие функции f, которая сопоставляет по крайней мере один объект f(x₁, …, x_n) (ее значение) с каждой n - кой объектов x₁, …, x_n (ее аргументов, которые сами могут рассматриваться как функции). - исчисление позволяет учитывать специфику вычисления функции в зависимости от используемых аргументов, то есть от того какой из аргументов рассматривается как связанная переменная.

Например, в дифференциальном исчислении выражение x-y может рассматриваться как функция f от x, либо как функция g от y. Для того, чтобы их различать будем записывать:

f = x.[x-y], g = y.[x-y].

Говорят, что префикс x абстрагирует функцию x.[x-y] от выражения x-y.

Аналогичные обозначения применяются для функций от многих переменных. Например, x-y отвечает функциям от двух переменных h и k: h(x, y) = x-y, k(y, x) = -y+x. Это можно записать:

h = xy.[x-y], k = yx.[x-y].

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

Например, определим функцию:

s = x.[y.[x-y]],

которая для каждого числа a превращается в

s(a) = x.[y.[x-y]](a) = y.[a-y],

а для каждой пары a, b в

s(a (b)) = s(a, b) = x.[y.[x-y]](a, b) = a-b.

Предположим, что имеется бесконечная последовательность переменных и конечная или бесконечная последовательность констант. Атом определяется как переменная или константа. Множество - термов определяется индуктивно:

1. Каждый атом есть - терм.

2. Если X и Y - - термы, то (XY) - - терм.

3. Если Y - - терм, а x - переменная, то x.[Y] - - терм.

Приведенное выше определение функции g(x) в этом исчислении записывается следующим образом:

g = (x).[a* sin(p * x + q)],

а вместо g(t² + 2) можно записать:

(x).[a* sin(p * x + q)] (t² + 2).

За символом следует еще несколько синтаксических конструкций: вначале идет список связанных переменных, затем выражение, в которое входят эти переменные (тело - выражения). Если остановиться здесь, то будем иметь функцию без операндов, такую как sin (заголовок функции). Но далее может следовать список фактических операндов. В этом случае имеем результат: взятие функции от этих операндов.

Важное значение приобретает сочетание - исчисления и рекурсии. Предположим, что существует функция «следующий» - назовем ее next(x) - для каждого целого положительного числа и нуля. На самом деле - это функция x + 1, но будем считать, что + пока не определен.

Используя next, можем задать функцию «предыдущий» - prior(x) (после определения - эта функция будет иметь вид x -1). Определим эту функцию следующим образом:

prior(x) = previous(x, 0) Where previous(y, z) = iif(next(z) = y, z, previous(y, next(z))).

Процесс вычисления prior(x) начинается при z = 0, далее последовательно вычисляются последовательно функции next до тех пор, пока следующий для z не будет равен x. Это значение z и является ответом. Теперь можем определить сумму и разность двух чисел.

Sum(x, y) = iif(y = 0, x, Sum(next(x), prior(y))),

Diff(x, y) = iif(y = 0, x, Diff(prior(x), prior(y))).

Обратим внимание, что если y>x, то при вычислении Diff настанет такой момент, когда потребуется вычисление prior(0), а среди положительных чисел нет предшественника нуля. Поэтому говорят, что Diff вычислимо только частично для положительных чисел.

Теперь представим Sum в - исчислении:

Sum = (x, y).[iif(y = 0, x, Sum(next(x), prior(y)))]

Можно выполнить дальнейшее преобразование этой функции с помощью - исчисления. Введя еще одно - обозначение, убираются все рекурсивные ссылки из тела - определения:

Sum =f.(x, y).[iif(y = 0, x, Sum(next(x), prior(y)))](Sum),

а затем можно совсем убрать объект определения из правой части за счет введения оператора Y такого, что если F - функция, то YF - решение уравнения y = F(x).

Sum = Yf.(x, y).[iif(y = 0, x, f(next(x), prior(y)))].

В этом определении f - связанная переменная, которая при разрешении уравнения может быть заменена на что-либо другое. Следовательно, при замене на Sum получим:

Sum = YSum.(x, y).[iif(y = 0, x,.Sum(next(x), prior(y)))].

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

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

Учитывая, что выражение x.[Px](a) может быть редуцировано к Pa, выражение:

f.y.x.[f(x, y)],

сформулированное:

f.y.x.[f(x, y)](подсистема)

сводится к

y.x.[подсистема(x, y)],

y.x.[подсистема(x, y)](ЭВМ)x.[подсистема(x, ЭВМ)], а

x.[подсистема(x, ЭВМ)](процессор)подсистема(процессор, ЭВМ).

Таким образом, - редукция осуществляется слева направо, и поэтому f.y.x.[f(x, y)], сформулированное в виде f.y.x.[f(x, y)](любит, Мария, Иван), дает любит(Иван, Мария).

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

1.Определить функцию f(x, y) = iif(x>y, sin(x), cos(x)) в - исчислении. Дать ее запись для x=t и y=/2. Осуществить редукцию.

2.Осуществить редукцию следующих - выражений:

f.[g.[t.[f(g(x)+t(y)]]](sin, cos, tg),

g.[t.[f.[f(g(x)+t(y)]]](sin, cos, tg),

f.[t.[g.[f(g(x)+t(y)]]](sin, cos, tg),

3.4 Использование списков

Введем некоторые определения. Символ - это набор букв, цифр и специальных знаков. Кроме символов будем использовать: числа, Т - истина, Nil - ложь или пустой список. Будем понимать под константами - числа, Т, Nil. Будем понимать под атомами символы и числа. Назовем списком упорядоченную последовательность, элементами которой являются атомы или другие списки (подсписки). Будем заключать списки в круглые скобки, а элементы списка разделять пробелами.

Формально список можно определить следующим образом:

Список :- Nil / (голова хвост)

[Список либо пуст, либо это пара голова и хвост]

голова :- атом / список

[рекурсия в глубину]

хвост :- список

[рекурсия в ширину]

Другой вариант определения:

Список :- Nil / (элемент элемент … )

Элемент :- атом / список

[рекурсия]

Обратим внимание, что атом это не список, хотя символ может идентифицировать список. Каждый символ имеет значение. Им может быть список, в том числе и пустой, константа, функция, которую рассматривают как специальный символ. Для записи функций будем использовать префиксную нотацию, т.е. x + y будем записывать, как (+ x y).

Атомы и списки будем называть S - выражениями.

Для представления списков будем использовать совокупность ячеек памяти, каждая из которых содержит два указателя. Первый указатель играет роль указателя на сына, второй - на брата. Например, список (А В) будет иметь вид.

Отсутствие указателя будем обозначать символом .

Список (* (+ 2 3) с) будет иметь представление:

Чтобы определить выражение по его машинному представлению, нужно просматривать представление, следуя указателям, расположенным слева, на наибольшую глубину и затем по правым указателям (внешний просмотр).

При записи выражения каждой стрелке, не заканчивающейся на атоме, соответствует открывающаяся скобка, каждому символу - закрывающаяся скобка, каждому атому - сам атом.

Этой схеме соответствует список ((А)(В)).

Вернемся к определению атома. Фактически атомы являются функциями, аргументы которых представляют собой следующие за ними S - выражения. В свою очередь аргумент сам может быть функцией, которую надо вычислить. Поэтому возникает необходимость определять, что представляет собой данный элемент: значение выражения L или символьное имя L какого-то S - выражения. В первом случае перед выражением ставится` или указатель QUOTE. Апостроф запрещает вычисление следующего за ним S - выражения, которое воспроизводится без изменений.

Для задания выражений введем функцию Setq:

(Setq <атом> <S - выражение>)

(Setq <атом> `<S - выражение>)

В первом случае выражение должно быть вычислено, во втором - на вычисляется. Кроме того, Setq связывает полученный результат с атомом.

(Setq L1 (+ 4 5))

(Setq L1 `(+ 4 5))

В первом случае L1 связано с (9), во втором - с (+ 4 5).

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

(CAR ` (A B C)) A

(CAR ` A) ошибка, А не список.

Функция CDR возвращает хвост списка. Если список состоит из одного элемента, то результатом является Nil.

(CDR ` (A B C)) (B C)

Комбинация вызовов CAR и CDR выделяет произвольный элемент списка. Для простоты эту комбинацию записывают в виде:

(C…R список)

Вместо многоточия записывается комбинация из букв А (для CAR) и D (для CDR).

(CADDAR L) = (CAR (CDR (CDR (CAR L))))

Функция CONS строит новый список из переданных ему головы и хвоста.

(CONS голова хвост)

(CONS `a `(b c)) (a b c)

(CONS `(a b) `(c d)) ((a b) c d)

(CONS (+ 1 2) `(+ 4)) (3 + 4)

Здесь первый аргумент без апострофа, поэтому берется как значение.

(CONS `(+ 1 2) `(+ 4)) ((+ 1 2) + 4)

(CONS `(a b c) Nil) ((a b c))

(CONS Nil `(a b c)) (Nil a b c)

Предикат ATOM используется для анализа списков, а именно, для идентификации является ли объект атомом или нет.

(ATOM `x) T

(ATOM (CDR `(A B C))) Nil. Атом от списка (B C) естественно False.

(ATOM (ATOM (+ 2 3))) T.

Результат сложения чисел атом. Т также является атомом.

(EQUAL <S-выр1> <S-выр2>) T, если и только если значения обоих выражений равны.

(EQ <S-выр1> <S-выр2>) T, если и только если значения обоих выражений равны и представляют один физический список.

(AND <S-выр1> <S-выр2> … <S-вырn>) - если встречается Nil,, возвращается Nil, иначе значение последнего выражения.

(OR <S-выр1> … <S-вырn>) - если при просмотре встречается выражение отличное от Nil, то оно возвращается, иначе Nil.

(NOT <S-выр>) T, если и только если значение выражения есть Nil.

Определять функции будем согласно - исчислению.

( (x₁, x₂, …, x_n) f)

x_i - формальный параметр.

f - тело функции.

Например, функция вычисляющая сумму квадратов будет определяться следующим образом:

( (x y) (+ (* x x) (* y y))).

Чтобы произвести вычисления будем осуществлять - вызов.

( - выражение a₁, …, a_n),

Здесь a_i - форма , задающая фактические параметры.

(( (x y) (+ (* x x) (* y y))) 2 3) - дает 13.

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

(DEFUN <имя> < - выражение>).

Для удобства исключим значок и внешние скобки.

(DEFUN проценты (часть целое) (* (/ часть целое) 100)).

Вызов:

(проценты 4 20)

Результат: 20.

Условное выражение COND имеет следующий вид:

(COND (p1 a1)

(p2 a2)

. . .

(pn an))

Значение COND определяется следующим образом:

1. Выражения pi вычисляются последовательно слева направо (сверху вниз) до тех пор, пока не встретится выражение, значение которого отлично от Nil.

2. Вычисляется результирующее выражение ai соответствующее этому pi и полученное значение возвращается в качестве результата.

3. Если нет ни одного pi, значение которого отлично от Nil, то значение COND равно Nil/

В более общем виде:

(COND (p1 a1)

…

(pj)

…

(pk ak₁ … ak_n)

…)

В этом случае:

- если условию не ставится в соответствие результирующее выражение, то в качестве результата при истинности предиката выдается само значение предиката;

- если условию соответствует несколько S - выражений, то при его истинности они вычисляются слева направо и результатом будет значение последнего S - выражения.

Реализуем логические связки И, ИЛИ, .

(defun И(x y) (COND (x y) (T Nil)))

(defun ИЛИ (x y) (COND (x T) (T y)))

(defun (x y) (COND (x y) (T T)))

С помощью COND можно реализовать различные варианты условных выражений.

(if <условие> <то-выр> <иначе-выр>) (COND (<условие> <то-выр>) (T <иначе-выр>))

Чтобы говорить о некотором свойстве, связанным с некоторым объектом и его значением, будем использовать функцию:

(PUTPROP <атом1> <список> <атом2>).

Эта функция связывает свойства, выраженные списком <атом2>, с конкретным объектом с именем <атом1>. Конкретные значения свойства задаются в объекте <список>.

(PUTPROP `Петр `(Иван Ирина) `Дети).

Чтобы узнать обладает ли объект данным свойством, будем использовать функцию GET:

(GET <атом1> <атом2>) значение свойства.

(GET `Петр `Дети) (Иван Ирина)

Теперь сформулируем алгоритм для вычисления списков. Алгоритм должен вычислять значение списка в последовательности, задаваемой указателями - «сыновьями», а затем учитывается последний из встреченных указателей «братьев». После этого учитываются указатели «сыновья», связанные с этим последним, и так далее, пока не получается окончательное значение для данной ветви. Затем вычисления повторяются снова, охватывая выражения более высокого уровня, и так до тех пор пока не будет определено значе ние всего списка. Те части всего выражения, которые ожидают вычисления значений их аргументов, называются квазарами.

Этот алгоритм представим в вида процедуры Eval(S), где S - выражение.

Sub Eval(S)

If S есть атом then

Возврат значение S

Else

If S1 = QUOTE then

Возврат S2

Else

S1 есть функция

If S1 указывает на специальную обработку, выполнить эту обработку

Else

Применить Eval ко всем элементам S2 последовательно и затем рекуррентно использовать их найденные значения.

Окончательный возврат S1 (Eval (S2))

End If

End If

End If

S1 - первый сын для S. S2 - элементы выражения S, представляющие собой множество братьев выражения S1.

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

1.Создать машинное представление для списков:

(a (b c) ( (d) e (f)))

( + a (* b (/ (+ c (/ d e)) f)))

(/ (+ ( a (- (b c)))) (* (/ (d b)) a))

(flat (hd (a) flat (tl (a) b)))

(cons (copy (hd (l) )) copy (tl (l)))))

2.Определить значения списков:

(car `(a (b c) ((d) e (f))))

(cdr `(a (b c) ((d) e (f))))

(cdadr `(a (b c) ((d) e (f))))

(cons nil `(суть пустой список))

(cons (car `(a b))(cdr `(a b)))

(car `(car (a b c)))

(cdr (car (cdr `(a b c))))

3.Запишите последовательность вызовов CAR и CDR, выделяющих из приведенных списков символ «цель». Упростите эти последовательности с помощью функций C…R.

(1 2 цель 3 4)

((1) (2 цель ) (3 4 цель)))

((1 (2 (3 4 цель))))

4.Определить вид списка, имеющего следующее машинное представление:

4. Реализовать с помощью COND логические операции: эквивалентность, штрих Шеффера, стрелка Пирса.

5. Реализовать функцию reverse, переставляющую местами элементы списка.

3.4.2 Компьютерное задание

Создать БД для индуктивного вывода и реализовать программу заполнения этой базы для оператора Setq. Возможная структура таблицы для хранения списков:

Имя поля	Тип	Комментарий
List	Text	Наименование списка
BeginList	Boolean	Является ли началом списка, если да -TRUE
SonPointer	Long	Указатель на сына
BrotherPointer	Long	Указатель на брата
ValueEl	Text	Значение. Для указателей Nil
ValueType	Text	Тип значения: ячейка, список, пустой список, атом, функция

Пример заполнения:

Пусть последовательно создаются 2 списка:

Setq a (* (+ 2 3) c)

Setq Second ((a) (b))

Структура списков: Список а

Список Second

Таблица для этих списков будет иметь вид:

List	BeginList	SonPointer	Brother Pointer	ValueEl	ValueType
a	true	2	4	Nil	ячейка
a	false	3	0	Nil	ячейка
a	false	0	0	*	функция
a	false	5	11	Nil	ячейка
a	false	6	7	Nil	ячейка
a	false	0	0	+	функция
a	false	8	9	Nil	ячейка
a	false	0	0	2	атом
а	false	10	0	Nil	ячейка
а	false	0	0	3	атом
а	false	12	0	Nil	ячейка
a	false	0	0	c	Пустой список
Second	true	14	16	Nil	ячейка
Second	false	15	0	Nil	ячейка
Second	false	0	0	a	список
Second	false	17	0	Nil	ячейка
Second	false	18	0	Nil	ячейка
Second	false	0	0	b	Пустой список

Порядок выполнения

1. Создание таблиц и форм для ввода и хранения списков (1 занятие).

2. Реализация алгоритмов преобразования описания списка в машинное представление и обратно (2 занятия).

3. Реализация операций над списками (2 занятия)

4. Реализация алгоритма Eval (2 занятия).

5. Оформление результатов (1 занятие).

4. Логическое программирование

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

4.1 Модели и опровержения

В доказательстве теорем стараются показать, что определенная ППФ B есть логическое следствие множества ППП S = {A₁, …, A_n}, называемых аксиомами рассматриваемой задачи. Правило вывод есть правило, при помощи которого из ранее полученных выражений можно получить новое. Например, если A_i и A_j истинные ППФ, то запись:

указывает, что A_k можно получить из A_i и A_j с помощью правила f_q . Рассмотрим последовательность S(0), …, S(j+1), образованную из некоторого множества аксиом S по правилу:

S(0) = S,

…

S(j+1) = S(j) F(S(j),

где F(S) - множество выражений, которое можно получить из множества S, применяя к каждому его элементу все возможные правила f_q из конечного множества F={f_q}. Говорят, что высказывание B следует из аксиом, принадлежащих S, если B S(j) для некоторого j.

Напомним, что терм - это константа, переменная или функция. В качестве своих аргументов n - местная функция должна иметь п термов. Таким образом, термами будут: a, b, c, f(a), g(f(x), y).

Атомом называется предикат со своими аргументами. Литерал - это атом или его отрицание. Предложение C - это дизъюнкция литералов. Множество предложений S интерпретируется как единое высказывание, представляющее конъюнкцию всех его предложений.

Как уже отмечалось, высказывание T следует из множества предложений S, если T есть логическое следствие предложений из S. Предположим для простоты, что T состоит из единственного предложения. Рассмотрим множество предложений:

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

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

(1)

должно быть ложным для любой модели.

Этот же вывод можно сделать следующим образом:



и от противного:

Предположим, что число атомов конечно. Тогда существует конечное множество моделей, так как k атомам можно присвоить логические значения 2^k различными способами. Очевидно, что присваивать значения этим комбинациям можно последовательно и если для всех моделей (1) окажется ложным, то, безусловно, S влечет T. Такое доказательство называется методом от противного и составляет основу методов доказательства теорем.

Доказать противоречивость (1), если число атомов конечно, достаточно просто. Просто ли это на практике зависит от количества атомов и от возможности порождать и проверять модели.

Возникает задача выявления условий, гарантирующих конечное число атомов. Пусть S - это множество высказываний истинных для тех атомов, которые непосредственно входят в S и тех, которые из них можно вывести. Последнее множество может быть бесконечным. В этом можно убедиться на следующем примере. Пусть S - высказывание, содержащее единственный атом S = {R(a, x)}.

Предположим, что определена функция g(x). Тогда можем построить бесконечную последовательность R(a, x), R(a, g(x)), R(a, g(g(x))), … . Эта последовательность перечислимая, так как можно придумать схему перечисления, по которой упорядочиваются высказывания. Например, по уровню вложенности второго аргумента. Можно показать, что всегда можно построить схему перечисления бесконечного множества атомов, полученного из конечного при помощи некоторой подстановки.

Предположим, что S не содержит переменных. Такая ситуация называется основным случаем, а соответствующий универсум (область определения) Эрбрановой базой. В основном случае можно провести перечисление.

Докажем, например, для конкретной пары чисел (a, b) (но не для произвольной пары чисел вообще x, y) истинность высказывания:

a = b a b.

Аксиомами будут:

A1: a > b,

A2: a < b,

A3: a = b.

Соответствующие предложения будут иметь вид:

- выполняется одно из отношений;

- одновременно не выполняются никакие два отношения.

В этих обозначениях наше утверждение имеет вид:

и его отрицание A3A1. Отсюда получим:

Обозначим

Так как в S может быть только 2³ = 8 атомарных высказываний, легко построить все возможные модели. Если для каждой из них хотя бы одно предложение в S принимает значение ложь, то высказывание вида (1) будет ложным, и поэтому наше утверждение будет истинным.

Модель	Предложения, которым присваивается значение ложь
A1, A2, A3	C2, C3, C4
	C3

Этот метод неэффективен и избыточен. Можно показать, что высказывание S противоречиво, если исследовать меньшее число моделей. Достаточно ограничиться атомами A1 и A3, то есть провести присваивание значений истинности только этим атомам, а значит использовать только четыре модели.

Теорема Эрбрана - Сколема - Геделя. В этой теореме утверждается, что можно найти частичное присваивание, приписывающее значение ложь любому противоречивому множеству предложений.

4.2 Доказательство от противного

4.2.1 Неаксиоматическое описание процедуры

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

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

Отец(x, y) : x является отцом y;

Брат(x, y) : x, y - братья;

Кузен(x, y) : x, y - двоюродные братья;

Дедушка(x, y) : x - дедушка y.

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

(1) (x1)(y1)(z1)((отец(x1, y1) отец(y1, z1)) дедушка(x1, z1)):

если x1 отец y1, а y1 отец z1, то x1 дедушка z1.

(2) (x2, y2, z2, w2)((отец(x2, y2) брат(x2, z2) отец(z2, w2)) кузен(y2, w2)) .

(3) x3, y3, z3)((отец(x3, y3) отец(x3, z3) ) брат(y3, z3)).