Лекции В.А. Захарова, страница 29

Однако для удобства пользования логическимипрограммами к ним можно добавлять специальные встроенныефункции и предикаты, операционная семантика которыхопределяется вне рамок SLD- резолютивного вывода.Рассмотрим некоторые наиболее широко используемыевстроенные средства логического программирования.ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикат равенства =Предикат равенства t1 = t2 — это 2-х местный предикат,предназначенный для унификации термов. Его операционнаясемантика задается следующими правилами:? tt1 = t2θt?⇔НОУ(t1 , t2 ) 6= ∅θ ∈ НОУ(t1 , t2 )ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикат равенства =Предикат равенства t1 = t2 — это 2-х местный предикат,предназначенный для унификации термов. Его операционнаясемантика задается следующими правилами:? tt1 = t2θt?⇔НОУ(t1 , t2 ) 6= ∅θ ∈ НОУ(t1 , t2 )? t1 t= t2failure⇔НОУ(t1 , t2 ) = ∅ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикат равенства =Пример? X + 2t= 3 + Y{X /3, Y /2}t?ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикат равенства =Пример? X + 2t= 3 + Y{X /3, Y /2}t?? 3 + 2 t= 2 + 3failureВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикат тождества ==Предикат тождества t1 == t2 — это 2-х местный предикат,предназначенный для проверки тождественности(синтаксической идентичности) термов.

Его операционнаясемантика задается следующими правилами:? tt == tεt?ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикат тождества ==Предикат тождества t1 == t2 — это 2-х местный предикат,предназначенный для проверки тождественности(синтаксической идентичности) термов. Его операционнаясемантика задается следующими правилами:? tt == tεt?? t1 ==t t2failure⇔t1 , t2 — разныетермыВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикат тождества ==Пример? X + 2t== X + 2εt?ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикат тождества ==Пример? X + 2t== X + 2εt?? X + 2t== 2 + YfailureВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикаты неравенства \ =, = \ =Предикаты неравенства t1 \ = t2 , t1 = \ = t2 определяютсяпри помощи оператора отрицания выражениями not(t1 = t2 ) иnot(t1 == t2 ).Пример? 3 + 2 t\ = 2 + 3εt?ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫПредикаты неравенства \ =, = \ =Предикаты неравенства t1 \ = t2 , t1 = \ = t2 определяютсяпри помощи оператора отрицания выражениями not(t1 = t2 ) иnot(t1 == t2 ).Пример? 3 + 2 t\ = 2 + 3εt?? 3 + X t= \ = 3 + XfailureВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫТипы данныхДля определения более сложных встроенных предикатоввводятся типы данныхinteger, real, boolean, char, и т.

д.Каждый тип данных определяется множеством констант,обозначающих элементы этого типа данных. Например,boolean = {true, false}.Тогда в каждом типе данных вводятся необходимыеотношения, присущие элементам этого типа. Например, в типеданных integer можно ввести отношения сравнения<, <=, >=, >, и др.ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫТипы данныхПример? 2 t< 3εt?ВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫТипы данныхПример? 2 t< 3εt?? 1 + 1t < 5 − 2failureВСТРОЕННЫЕ ФУНКЦИИ И ПРЕДИКАТЫТипы данныхДля введенных типов данных можно ввести встроенныефункции (операции), присущие элементам этих типовНапример, в типе данных integer можно ввести двухместныефункции (операции) +, −, ×, div, и др.Однако чтобы вычисленные значения можно было передаватьпеременным, необходимо специальное средство.

Предикатравенства = для этой цели не годится, поскольку онзанимается лишь унификацией термов.? X =t 2 + 3θ = {X /2 + 3}t?ПРЕДИКАТ ВЫЧИСЛЕНИЯ ЗНАЧЕНИЙПредикат вычисления значений is — это встроенный предикат,предназначенный для вычисления значений встроенныхфункций. Операционная семантика этого предиката задаетсяследующими правилами.Условимся использовать запись val(t) для обозначениязначение терма t, составленного из встроенных функций иконстант.

Тогда...? tt1 is t2θ⇔t1 ∈ Var ,определено val(t2 )t?θ = {t1 /val(t2 )}ПРЕДИКАТ ВЫЧИСЛЕНИЯ ЗНАЧЕНИЙПредикат вычисления значений is — это встроенный предикат,предназначенный для вычисления значений встроенныхфункций. Операционная семантика этого предиката задаетсяследующими правилами.Условимся использовать запись val(t) для обозначениязначение терма t, составленного из встроенных функций иконстант. Тогда...? tt1 is t2θ⇔t1 ∈ Var ,определено val(t2 )t?θ = {t1 /val(t2 )}ПРЕДИКАТ ВЫЧИСЛЕНИЯ ЗНАЧЕНИЙПредикат вычисления значений is — это встроенный предикат,предназначенный для вычисления значений встроенныхфункций. Операционная семантика этого предиката задаетсяследующими правилами.Условимся использовать запись val(t) для обозначениязначение терма t, составленного из встроенных функций иконстант.

Тогда...? tt1 is t2θt?⇔? t1 tis t2t1 ∈ Var ,определено val(t2 ) failureθ = {t1 /val(t2 )}⇔в остальныхслучаяхПРЕДИКАТ ВЫЧИСЛЕНИЯ ЗНАЧЕНИЙПример? X is 3t+ 2{X /5}t?ПРЕДИКАТ ВЫЧИСЛЕНИЯ ЗНАЧЕНИЙПример? X is 3t+ 2{X /5}t?? X is Yt + 1failureПРЕДИКАТ ВЫЧИСЛЕНИЯ ЗНАЧЕНИЙПример? X is 3t+ 2{X /5}t?3 + 1 ist 4failureМОДИФИКАЦИЯ БАЗ ДАННЫХОбычно логическая программа P разделяется на две части —систему правил Pclauses и базу данных Pdatabase . База данныхсостоит из всех основных фактов программы.Система правил Pclauses представляет, по сути дела, алгоритмрешения задачи, и его неразумно изменять по ходу решениязадачи.А вот базу данных Pdatabase по ходу вычисления можномодиифцировать.

И для этой цели в системах логическогопрограммирования есть специальные встроенные операторыпополнения и сокращения базы данных.МОДИФИКАЦИЯ БАЗ ДАННЫХОператор пополнения базы данных assert(A), где A — атом,добавляет к базе данных факт A ←;? X is 2 + 2, tassert(Oценка(X ))PX /4?? assert(A)tP? assert(Oценка(4))tεεt??tP ∪ {A ←; }PP ∪ {Oценка(4) ←; }МОДИФИКАЦИЯ БАЗ ДАННЫХОператор пополнения базы данных assert(A), где A — атом,добавляет к базе данных факт A ←;? X is 2 + 2, tassert(Oценка(X ))PX /4?? assert(A)tP? assert(Oценка(4))tεεt??tP ∪ {A ←; }PP ∪ {Oценка(4) ←; }Поскольку в логических программах правила и фактыупорядочены, нужны два варианта оператора пополнения базданных: asserta(A) и assertz(A).МОДИФИКАЦИЯ БАЗ ДАННЫХОператор сокращения базы данных retract(A), где A — атом,удаляет из базы данных факт A ←;? Есть(X ), retract(Xt ), not(Есть())X /ЯP = {Есть(Я) ←; }?? retract(Я),tnot(Есть(Я))εP = {Есть(Я) ←; }?? retract(A)tP? not(Есть(Я))tεεt??tP \ {A ←; }P=∅P=∅МОДИФИКАЦИЯ БАЗ ДАННЫХТворческая задачаА что если разрешить в теле правила использовать наряду сатомами также и программные утверждения? Как то,например,A0 ← A1 , .

. . , Ai , (B0 ← B1 , . . . , Bm ), Ai+1 , . . . , An ;илиA0 ← A1 , . . . , Ai , (B0 ←), Ai+1 , . . . , An ;1. Как определить разумную декларативную семантику таких«составных» правил?2. Как определить адекватную операционную семантикутаких правил?3. Можно ли определить адекватную операционнуюсемантику «составных» правил на основе резолютивноговывода?КОНЕЦ ЛЕКЦИИ 17.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 18-19.Интуиционистская логика.Модальные логики.модальныелогикиy6интуиционистскаялогикаyI@yдругиелогическиеоперации@@другаятеориядоказательствсемантика@логических@связок@другиеформылогическоговывода@@yдругие кванторылогикивысших порядков@iспециальные интерпретации-КЛАССИЧЕСКАЯЛОГИКАyаксиоматическиетеорииИНТУИЦИОНИСТСКАЯ ЛОГИКАИнтуиционизм — это философское течение в математике,возникшее в начале 20 века как критический отклик нанеограниченное применение формальных логических методов вматематике, приводящее к парадоксам (антиномиям).По мнению интуиционистов (Брауэр, Вейль, Пуанкаре),парадоксы возникают в связи с тем, что законы логики,справедливые для конечных множеств, безосновательнопереносятся на бесконечные множества.Не все математические утверждения, верные для конечныхмножеств, остаются справедливыми и для бесконечныхмножеств.

Например, для конечных множеств верен принципАрхимеда «Часть всегда меньше целого», а длябесконечных множеств — нет.Вполне возможно, что не все законы классической(аристотелевой) логики допускают неограниченное ибезоговорочное использование в математике.ИНТУИЦИОНИСТСКАЯ ЛОГИКАНапример, рассмотрим одну широко распространенную схемудоказательства.Доказать: Если выполнены условия A, то ∃x P(x).Схема доказательства: Предположим противное, т. е.

∀x ¬P(x).Тогда ...(фа-фа, ля-ля)..., что противоречит условиям A.Значит, предположение ∀x ¬P(x) неверно, и поэтому ∃x P(x).QEDВсе хорошо, но где же та x, для которой верно P(x)?Из такого доказательства это значение извлечь невозможно.Но тогда, по мнению интуиционистов, это не доказательство, асловоблудие.Чтобы исключить доказательства такого рода, нужнопересмотреть семантику логических связок и кванторов.ИНТУИЦИОНИСТСКАЯ ЛОГИКАСемантика Колмогорова–Брауэра–ГейтингаПопробуем взглянуть на логические формулы как наутверждения о разрешимости математических задач.Каждая атомарная формула A будет обозначать некоторуюзадачу.

Истинность A будет означает, что задача имеетрешение, и это решение можно предъявить. Ложность A будетозначать, что задача решения не имеет.Логические связки позволяют конструировать из простыхзадач составные задачи.Оценим, как (не)разрешимость составных задач зависит от(не)разрешимости простых задач.ИНТУИЦИОНИСТСКАЯ ЛОГИКАСемантика Колмогорова–Брауэра–Гейтингаϕ & ψ:Решить обе задачи ϕ и ψ и предъявить решение;ϕ ∨ ψ:Выбрать одну из двух задач ϕ и ψ, решить выбранную задачу и предъявить решение;ϕ → ψ:Показать, что решение задачи ψ сводится к решению задачи ϕ, т.

е. предъявить способ, который позволяет, располагая решением задачи ϕ,построить решение задачи ψ;¬ ϕ:Доказать, что задача ϕ не имеет решения.Законами интуиционистской логики считаются только теформулы, которые соответствуют описаниям составных задач,имеющих решение при любых условиях.ИНТУИЦИОНИСТСКАЯ ЛОГИКАЗаконы интуиционистской логикиIP → P — каждую задачу можно свести к ней самой;I(P → Q)&(Q → R) → (P → R) — чтобы свести задача Rк задаче P достаточно найти задачу Q, к которой можносвести задачу R, и которую, в свою очередь, можно свестик задаче P;IP → ¬¬P — чтобы убедиться в том, что не существуетдоказательства неразрешимости задачи P, достаточнонайти решение задачи P;I(¬P ∨ ¬Q) → ¬(P&Q) — чтобы показать, что обе задачиP и Q нельзя решить одновременно, достаточно выбратьодну из этих задач и показать, что она неразрешима.ИНТУИЦИОНИСТСКАЯ ЛОГИКАФормулы, не являющиеся законамиинтуиционистской логикиI¬¬P → P — если вы можете обосновать, что нельзяпостроить доказательства неразрешимости задачи P, тоэтого еще недостаточно, чтобы получить решение самойзадачи P;IP ∨ ¬P — неправда, что для любой задачи можно либополучить решение, либо доказать, что никакого решенияне существует;I¬(P&Q) → (¬P ∨ ¬Q) — если можно доказать, что обезадачи P и Q нельзя решить одновременно, то это не даетоснования считать, что хотя бы одна из них являетсянеразрешимой.Да как же это так?Уж не скрывается ли здесь простая игра слов?ИНТУИЦИОНИСТСКАЯ ЛОГИКАПопробуем строго определить семантику утверждений,касающихся разрешимости задач.Истинность формул оценивается в интерпретациях.