Откройте актуальную версию документа прямо сейчас
Если вы являетесь пользователем интернет-версии системы ГАРАНТ, вы можете открыть этот документ прямо сейчас или запросить по Горячей линии в системе.
Приложение Е
(справочное)
Подходы на основе интерпретируемой логики предикатов
Использование интерпретируемой логики предикатов для описания концептуальных схем основывается на представлении о концептуальной схеме и информационной базе как совокупности абстрактных элементов, называемых предложениями. На практике предложения представляются строками символов. Символы кодируются соответствующими наборами состояний физических элементов носителей памяти информационной системы.
Руководящий принцип реализации рассматриваемых подходов, связанных с применением интерпретируемой дедуктивной формальной логической системы, состоит в том, чтобы к информационному процессору, внешнему по отношению к концептуальной схеме и информационной базе, предъявлялись минимальные требования. На практике многие конструкции могут быть встроены в реальный информационный процессор в целях обеспечения эффективности и сокращения затрат.
Сформулированный принцип можно осуществлять по-разному. Для того чтобы обеспечить основной выбор из этих различных возможностей, необходим второй руководящий принцип. Он выводится из требования простоты концептуальной схемы для понимания и применения различными пользователями.
Необходим механизм добавления конструкций произвольной сложности к формальной системе, позволяющей пользователям взаимодействовать с ней на любом требуемом уровне общности понятий. Для соблюдения этого принципа без нарушения первого формальная система должна включать механизм, обеспечивающий возможность определения новых конструкций через уже существующие.
Е.1 Фундаментальные понятия
При моделировании проблемной области существующие в ней предметы - только сущности. Относящиеся к сущности ситуации, которые могут иметь или не иметь место в проблемной области - только высказывания.
Системы и правила дедукции выбираются таким образом, чтобы каждая аксиома интерпретировалась как истинное утверждение о проблемной области, а каждое предложение, непосредственно выводимое из набора предложений, интерпретируемых как истинное утверждение о проблемной области, само интерпретировалось как истинное утверждение о проблемной области.
Правило дедукции - единственное, что требуется в подходах на основе интерпретируемой логики предикатов, сохраняет истинность. Однако аксиомы, выбираемые разработчиком концептуальной схемы, в значительной степени зависят от проблемной области; гарантия корректности возлагается на разработчика.
Используемый формальный язык описывается лишь в той степени, которая необходима для определения основных категорий грамматических конструкций и обеспечения интерпретируемости универсальной машиной Тьюринга.
Конкретный синтаксис не представлен (за исключением случаев, когда необходимо детализировать пример), чтобы любой формальный язык, наследующий рассматриваемый абстрактный синтаксис, мог использоваться для выполнения описываемой программы.
Е.2 Грамматика и семантика
Для придания значения (семантики) различным выражениям в языке необходимо начать с (желательно малого) набора неопределенных понятий, известных как примитивы. Тогда другие понятия формально определяются через неформально понимаемые примитивы и получают значения. Суть каждого примитивного понятия формально вводится путем установления аксиом, предполагаемых истинными. То же самое имеет место в элементарной геометрии, где понятия точки, линии и плоскости берутся как основные (неопределенные), а более сложные конструкции, такие как треугольники и окружности, определяются в терминах этих примитивов и аксиом (постулаты Эвклида), формально устанавливающих свойства точек, линий и плоскостей.
Е.2.1 Абстрактный синтаксис
Определенные общие концепции - это основные понятия (примитивы), характеризующие абстрактный синтаксис (грамматику) любого языка. К ним относятся:
ТЕРМ - лингвистический объект, обозначающий сущность;
ПРЕДЛОЖЕНИЕ - лингвистический объект, представляющий определенное высказывание;
ФУНКТОР - лингвистический объект, который обозначает функцию от других лингвистических объектов, имеющую в качестве аргументов (вход) список лингвистических объектов и выдающую в качестве значения (выход) единственный уникально определенный лингвистический объект.
Функтор есть средство, позволяющее конструировать лингвистические объекты произвольной сложности. Все, что представляется необходимым для концептуальной схемы и информационной базы - это функторы первого уровня, т.е. функторы, аргументами которых являются только термы и предложения (никогда - функторы) и значениями которых являются термы или предложения (никогда - функторы). Тем не менее, ничто из поясняемого ниже не препятствует введению функторов высшего уровня в тех случаях, когда это требуется для концептуальной схемы и информационной базы.
Функторы называются чистыми, если их списки аргументов всегда представляют собой или только предложения, или только термы. Функторы называются функторами подстановки, если существует шаблон, в который могут быть подставлены элементы списка аргументов. Функторы могут быть фиксированными или независящими от того, фиксирован список аргументов по длине или нет.
Элементарными функторами называются фиксированные функторы подстановки первого уровня. Существуют четыре вида чистых элементарных функторов подстановки. Это:
|
Аргументы |
|
Значение |
|
Термы |
|
Терм |
|
Термы |
|
Предложение |
|
Предложения |
|
Предложение |
|
Предложения |
|
Терм |
Очевидно, что каждый из характеризуемых выше чистых элементарных функторов применим к концептуальным схемам. Два других вида функторов, являющихся элементарными, но не чистыми, также важны для концептуальных схем: кванторы и абстракторы. Переменные являются видом терма
|
Аргументы |
|
|
Значение |
|
|
Переменная |
+ |
предложение |
Предложение |
|
|
Переменная |
+ |
предложение |
Терм |
|
Переменные - это аналоги местоимений естественного языка, они относятся к неопределенным сущностям проблемной области, точно так же как местоимения в естественном языке относятся к неопределенным предметам в предложениях с анафорой.
Сконструированные (составные) предложения и термы могут быть открытыми или замкнутыми в зависимости от того, имеют они свободные переменные или нет. Только замкнутые предложения могут быть однозначно интерпретированы, и по этой причине они будут единственным видом предложений, встречающихся в концептуальной схеме и информационной базе.
Данный раздел не дает подробного описания открытых и замкнутых предложений и способа связывания переменных. Достаточно отметить, что путем добавления нужных кванторов из любого предложения можно связать его свободные переменные.
Собственные имена всегда можно исключить и заменить предикатами, использующими абстрактор, называемый "дескриптором" и определяющий собственное имя в контексте.
Е.2.2 Конкретный синтаксис
В противоположность другим примерам, приведенным в стандарте, конкретный синтаксис любой версии подхода интерпретируемой логики предикатов не может быть полностью описан в системе обозначений, представленной в приложении В, т.к. язык в существенной мере не контекстно свободен. Здесь приводится краткое описание конкретного синтаксиса. Часть этого описания зависит от контекста ввиду контекстной чувствительности языка, но следует понимать, что полный синтаксис может быть описан совершенно формально и исчерпывающе на любом языке, приемлемом для описания концептуальных схем и основанном на подходе интерпретируемой логики предикатов. Рассматриваемый ниже язык именуется "L". Выбор синтаксических деталей здесь производится для ограничения набора символов, чтобы уделить основное внимание разъяснению сути вопроса.
Итак:
прописная буква |
= "А" | "В" | "С" | ... | "Z" |
строчная буква |
= "а" | "b" | "с" |... | "z" |
цифра |
= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9". |
прим |
= " ' ' ". |
Примечание - Это означает единичный начальный символ.
| |
точка |
= " . " |
другой знак |
= "&" | "(" | ")" | "*" | "+" | "-" | "/" | ":" | |
|
";" | "," | "<" | "=" | ">" | "[" | "\" | "]" | |
|
"{" | "}" | " ". |
прописная-курсив |
= " A" | "B" | "C" | ... | "Z". |
строчная-курсив |
= "a" | "b" | "с" |... | "z". |
знак |
= прописная-буква | строчная-буква | цифра | |
|
прим | точка | прописная-курсив | |
|
строчная-курсив | другой знак. |
строка |
= знак {знак}. |
переменная |
= (прописная-курсив {прим}) | (строчная-курсив {прим}). |
составной-символ |
= прописная-буква {строчная-буква} {прим}. |
числовой-символ |
= {цифра} [точка] {цифра}. |
Примечание - Строка не должна начинаться и/или заканчиваться ни цифрой, ни точкой.
| |
символ |
= переменная | составной-символ | числовой-символ | другой знак. |
выражение |
= символ {символ}. |
Нетрудно убедиться, что любую строку, являющуюся выражением, можно разложить на символы единственным способом. | |
предикат-примитив |
= "Pr" {строчная-буква} {прим}, |
прим-переменная-список |
= (прим переменная) | |
|
(прим прим-переменная-список переменная). |
атомарное-предложение |
= "Pr" {строчная-буква} прим-переменная список. |
предложение-примитив |
= атомарное-предложение |
|
("Для всех" переменная предложение-примитив) | |
|
("Не" предложение-примитив) | |
|
("Если" предложение-примитив "То" предложение-примитив). |
Вхождение переменной в предложение-примитив следует понимать буквально. Вхождение - основной текстно-чувствительный аспект L. "х" не считается входящим в "х"'. Вхождение переменной называется связанным в предложении-примитиве, если существует предложение-примитив, содержащее это вхождение переменной, являющееся частью или всем рассматриваемым предложением-примитивом и начинающееся с выражения "Для всех", за которым следует эта переменная. Вхождение переменной свободно в предложении-примитиве, если оно не связано в этом предложении-примитиве. Переменная называется свободной переменной предложения-примитива, если она имеет свободное вхождение в предложение-примитив.
Предложение-примитив называется открытым, если оно имеет по крайней мере одну свободную переменную, в противном случае оно называется замкнутым.
Все, что может быть сформулировано как утверждение, в L может выражаться только замкнутыми предложениями-примитивами. Однако даже простейшие утверждения становятся пространственными, громоздкими и неудобными при чтении, если их выразить как предложения-примитивы. Поэтому вводится следующая дополнительная конструкция:
ОПРЕДЕЛЕНИЕ
Любое выражение является определением, если оно утверждается как таковое уполномоченным источником.
За исключением небольшого числа специальных случаев, необходимых для начального развертывания, которые здесь не рассматриваются, все определения будут замкнутыми предложениями в одной из двух следующих форм:
выражение "| ff" выражение;
выражение "=" выражение.
Как будет показано далее, символ "| ff" интерпретируется как связка, которая, будучи вставлена между двумя предложениями, означает их логическую эквивалентность. Последовательность определений в этой форме строится так, что правостороннее выражение (определяющее выражение) каждого определения в последовательности является или предложением-примитивом, или левосторонним выражением (определяемое выражение) какого-либо предыдущего определения в последовательности. Благодаря взаимозаменяемости логически эквивалентных выражений очень сложные утверждения можно представить в сжатой форме, логически эквивалентной предложению-примитиву.
Аналогичный процесс в определениях второй формы, т.е. символ "=", интерпретируется как предикат идентичности, и также обеспечивает взаимозаменяемость выражений. Конечно, в этой ситуации выражения по обе стороны знака идентичности являются термами, а не предложениями. Используя способ концептуального определения, можно определить термы везде, где может появиться переменная (также терм) в атомарном предложении. Все, что может утверждаться о сущности, обозначенной термом, может быть интерпретировано.
Введя концепцию последовательности определений, можно еще кое-что сказать о конкретном синтаксисе L. Следующие концепции вводятся здесь для иллюстрации того, что они являются фактически синтаксическими понятиями.
АКСИОМА
Любое замкнутое предложение, утверждаемое в качестве такового авторитетным источником.
ДОКАЗАТЕЛЬСТВО
Любая последовательность замкнутых предложений является доказательством, если для любого предложения Q: либо Q есть аксиома, либо до Q в последовательности есть предложения Р и "Если Р то Q".
ТЕОРЕМА
Любое предложение, для которого существует доказательство, содержащее это предложение.
Хотя не существует общего алгоритма нахождения доказательства, которое содержит данное предложение и, следовательно, разрешающей процедуры для определения того, является ли предложение-кандидат теоремой или нет (определение "теоремы" - синтаксическое), однако существует механизм определения, является ли данная последовательность доказательством и содержит ли она предложение-кандидат.
Е.2.3 Семантика
Семантика формального языка L устанавливается путем присваивания значений его примитивным конструкциям.
Интерпретация двух примитивных связок и примитивного квантора очевидна; она заимствуется из традиционной логики первого порядка.
Е.3 Моделирование
Е.3.1 Классификация аксиом
Из предложений L в качестве аксиом выбираются определенные замкнутые предложения. Один набор аксиом А1 составляет аксиомы логики и математики. Применение правил вывода позволяет получить дополнительный набор предложений, которые являются теоремами, выводимыми исключительно на основе аксиом А1. Хотя существует большое разнообразие различных наборов предложений, любой из которых может быть выбран в качестве А, общая совокупность теорем будет, как правило, одним и тем же во всех случаях. Разумно предположить, что все концептуальные схемы и информационные базы будут включать в себя один и тот же набор А1.
Следует отметить, что большинство аксиом А1 являются схемами аксиом - утверждениями метаязыка о том, что каждое предложение заданной формы - аксиома. Хотя существует ограниченное число таких схем, множество аксиом в А1 фактически не ограничено.
Концептуальная схема не исчерпывает всех предложений. Если бы все возможные предложения были бы выводимыми в концептуальной схеме, это противоречило бы определению. Кроме того, ничто не осталось бы для самой информационной базы. В общем, должно существовать много различных допустимых совокупностей предложений, наборов предложений, несовместимых между собой или с концептуальной схемой. Различные допустимые совокупности предложений, конечно, могут не согласовываться друг с другом. Информационная база будет представлять собой одну из этих допустимых совокупностей предложений вместе с теоремами, выводимыми в данный момент из предложений информационной базы и концептуальной схемы.
Часто для определенных концептуальной схемы и информационной базы требуется, чтобы в информационной базе присутствовал некоторый набор предложений. Эти требования отличаются от аксиом или теорем, из них выводимых. Концептуальная схема может потребовать, чтобы, например, было доступно какое-либо параметрическое значение. Здесь концептуальная схема не определяет точное значение, а утверждает, что оно существует. Предложение, указывающее это значение, должно быть в информационной базе, а не в концептуальной схеме. Может быть указано любое из допустимых значений, но должно присутствовать одно из них.
При наличии концептуальной схемы и требуемых предложений остальная часть концептуальной схемы и информационной базы - вспомогательная. Необходимо лишь, чтобы все предложения вместе образовывали допустимую совокупность. Конечно, в любой данный момент состояние концептуальной базы - это точно определенный набор предложений.
Должны существовать и другие наборы предложений, совместимые с состоянием концептуальной схемы и информационной базы и, следовательно, допустимые для дополнения.
Е.3.2 Конструкции
Цель данного подраздела - выработать более удобные формы для примитивных понятий. Сначала рассматриваются конструкции, существенные для базовой логики. В этом начальном изложении буквы "Р" и "Q" будут означать произвольные предложения, а буквы "X" и "Y" - произвольные термы.
Связки, используемые обычно в элементарной логике, можно легко определить через связки-примитивы:
"(P Или Q" эквивалентно "(Если Не Р То Q";
"(Р & Q)" эквивалентно "Не (Не Р Или Не Q";
"(Р | ff Q)" эквивалентно "((Если Р То Q) & (Если Q То Р))";
Целесообразно использовать дополнительный квантор:
"Для некоторого ХР" эквивалентно "Не Для всех X Не Р"
Приведенные четыре определения (фактически, определяющие схемы) вместе с шестью схемами аксиом, устанавливающими свойства предложений "Не Р", "(Если Р Тогда Q", "Для всех ХР" достаточны для всей необходимой логики, не зависимой от специфических предикатов.
Для представления математических формулировок требуется пять предикатов-примитивов: три одноместные и два двухместных. Предикаты-примитивы вводились синтаксически в такой форме:
"Pr" (строчная буква} {прим}
Pr устанавливает, что символ - это предикат, строка строчных букв служит просто для отличия одного предиката от другого, а число символов прим определяет, сколько переменных должно следовать за предикатом, чтобы получилось правильно построенное атомарное предложение. Используя определения, можно ввести более удобные обозначения:
|
(Нуль X | ff Pra' X) |
|
|
(Индивид X | ff Prb' X) |
|
|
(Класс X | ff Prc' X) |
|
Интерпретация этих трех предикатов проста. "Нуль X" утверждает, что сущность, обозначенная символом X, - нулевая сущность, "Индивид X" утверждает, что сущность индивидная, а "Класс X" утверждает, что сущность, обозначенная символом X, - класс. В каждой проблемной области, в подходах интерпретируемой логики предикатов, все множество сущностей распадается на эти взаимоисключающие категории. Нулевая сущность - грубый эквивалент отсутствия чего-либо. Нулевая сущность существует, т.е. должна существовать теорема "Для некоторого х Нуль х". Это вид сущности, к которой приводятся невозможные предметы, например "Нуль квадратная-окружность".
Следующие бинарные предикаты фундаментальны:
((X = Y) | ff Pra ' ' X Y)
((X Принадлежит Y) | ff Prb ' ' X Y).
"X = Y" утверждает, что сущность, обозначенная символом X, идентична сущности, обозначенной Y, и "X принадлежит Y" утверждает, что сущность, обозначенная X, - это член класса, обозначенного символом Y. Для того чтобы высказывание "X принадлежит Y" было истинным, Y должен обозначать класс, но это высказывание значимо независимо от того, что обозначает Y. Такая ситуация характерна для подходов интерпретируемой логики предикатов и вынуждает использовать явные ограничения. Должна быть введена аксиома, подобная следующей:
"Для любого X Для любого Y (Если (X Принадлежит Y) То Класс Y)".
Достаточность этих предикатов-примитивов для логики и математики давно продемонстрирована. В обычных формулировках достаточно пяти схем аксиом и семнадцати явных аксиом.
Количество необходимых определений зависит от объема математики, необходимой для описания определенной рассматриваемой проблемной области. В последующем будут излагаться только понятия, относящиеся к примеру приложения Б, и то неформально, главным образом, чтобы ввести обозначения. Во-первых, вводится понятие определенных описаний:
"The X Р" обозначает такую единственную сущность X, что высказывание, утверждаемое Р, - истинно, если такая единственная сущность существует.
Описания - это термы или термы специфической формы, которые определяются в контексте всех возможных позиций в атомарных предложениях. Все другие сложные термы, в конечном счете, редуцируются к определенным описаниям. Таким образом, точное определение понятий "класс всех х таких, что Р", обозначаемого "{Х\Р}" определяется следующим образом: ({Х\Р} = The Y (Класс Y & Для всех X (Если Для некоторого Z (X Принадлежит Z) То (X Принадлежит Y) | ff Р))).
Это определение вместе с соответствующими аксиомами (не приведенными здесь) гарантирует, что L - экстенциональный, т.е. что два класса идентичны тогда и только тогда, когда они имеют одни и те же члены, и что известные парадоксы класса исключаются.
Классы могут задаваться посредством перечисления членов:
({а, b, с, ..., z} = {X \ X = а Или Х = b Или Х = с Или ...
Или X = z}).
Упорядоченные пары могут быть определены следующим образом:
([х, у] = ({х}, {х, у}}).
Тогда отношения являются классами упорядоченных пар:
({ху \ Р} = {z\ Для некоторого х Для некоторого у
(z = [х, у] & Р)}).
То есть отношение х с у такое, что Р является классом упорядоченных пар [х, у], таких, что Р - истинно. Утверждать, что А находится в связи типа "члена" с В значит утверждать, что ([А, В] Принадлежит {ху \ х принадлежит y}).
Функции, используемые в строго математическом смысле в подходе интерпретируемой логики предикатов, задаются следующим образом:
(Fx Y = {ух \ у = Y}).
Функция от х, значение которой (для аргумента х) есть Y, является отношением у с х таким, что у = Y. Функции - это просто специальные отношения, где для каждого аргумента имеется единственное значение.
По разным причинам удобно использовать специфическое обозначение для результата применения функции. Вместо F(x), L использует:
(F:х = The у ([y, х] Принадлежит F)).
Если Удвоить = Fx, 2х, то Удвоить : 3=6.
Подобная конструкция допускает идентификацию класса всех сущностей, вступающих в отношение R с каким-либо членом определенного класса. Так:
(R; х = {у \ Для некоторого z
(z Принадлежит х & [у, z] Принадлежит R)}).
Удобно использовать также некоторые элементарные понятия теории множеств. Это такие обычные понятия:
Объединение:
(х U у = {z / z Принадлежит х или z Принадлежит y}).
Пересечение:
(х N у = {z / z Принадлежит х & z Принадлежит у}).
Дополнение:
(С х = {у \ Не (у Принадлежит x)}).
Подмножество:
(х В у | ff Для всех z (Если z Принадлежит х То z Принадлежит у)).
Оконечное объединение:
(Un х = {у \ Для некоторого z (z Принадлежит х & у Принадлежит z)}).
Обратное утверждение:
(Cnv R = {ху \ [у, х] Принадлежит R}).
Декартово произведение:
(х X у = {zw\z Принадлежит х & w Принадлежит у}).
Некоторые конкретные сущности определяются и обозначаются особо:
Нулевая сущность:
(W = The х Нуль х).
Пустое множество:
(O = {х \ Не х = х).
Класс индивидов:
(I = {х \ Индивид х}).
Класс элементов (Универсальный класс):
(E = {х \ Для некоторого у (х Принадлежит у)})
Класс всех функций:
(Fcn = {F \ Для некоторого х Для некоторого у.
(F В х Х у
& для всех х' Для всех у' Для всех у' '
(Если [у', х'] Принадлежит F
& [у", х'] Принадлежит F
То у' = y ' '))}).
Левый домен произвольного отношения:
(Dl R - {х \ Для некоторого у ([х, у] Принадлежит R)}).
Правый домен произвольного отношения:
(Dr R = {у \ Для некоторого х ([x, у] Принадлежит R)}).
Известно, что все математические конструкции могут быть определены в терминах множеств. Здесь это не делается. Однако предполагается, что это проделано таким образом, что все промежуточные определения являются аксиомами. Явно необходимы для примера лишь такие конструкции:
0, 1, 2, ... |
Последовательность натуральных чисел (нуль есть пустое множество); |
Nn |
Класс всех натуральных чисел; |
Nrp |
Класс всех положительных действительных чисел; |
< , > |
Предикаты арифметического порядка; |
+, -, *, / |
Традиционные арифметические операторы; |
К |
Функция мощности, т.е. К : х - это кардинальное число - число элементов в классе, обозначенное х; |
Среднее |
Арифметическое среднее функции, то есть Среднее: F - арифметическое среднее значение функции, обозначенной F, при условии, что эти значения являются действительными числами. |
Для того чтобы говорить об именах сущностей, необходимо ввести в качестве индивидов надписи - экземпляры типографских строк (а также их отображения в памяти компьютера) и классы надписей, рассматриваемых как эквивалентные (представляющие одни и те же абстрактные символы).
Для этого используется тот же метод, что и рассматриваемый здесь для концептуальной схемы и информационной базы. Начинаем, как обычно, с примитивных предикатов. Существуют три таких необходимых примитива: надписи, соединение и лексикографическая последовательность.
Надписи - это конечные линейные последовательные образы, составленные из более или менее связанных графических элементов (глифов), выбранных из алфавита знаков. Важно отметить, что каждый экземпляр физической реализации надписи отличается от каждой другой такой физической реализации. Четвертый и шестой глифы в слове "надписи" - различные надписи, хотя они являются членами одного и того же знака. С учетом этих различий приводятся следующие пояснения соответствующих примитивных предикатов.
Надпись
Prd'x утверждает, что сущность, обозначенная х, является надписью.
Соединение
Pra' ' 'xyz утверждает, что сущность, обозначенная z, является надписью, полученной путем приписывания к сущности, обозначенной х, сущности, обозначенной у.
Лексикографическая последовательность
Prc' 'ху утверждает, что сущность, обозначенная у, является глифом и элементом знака, который непосредственно лексикографически следует за знаком, элементом которого является глиф, обозначенный х.
Необходимо пояснить последний предикат. Он предполагает, что в алфавите имеется порядок. Поскольку единственный рассматриваемый здесь алфавит описан в Г.2.2 данного приложения, естественно предположить, что лексикографический порядок - это порядок, в котором представлены его знаки. Таким образом, если х обозначает "а", тогда Prc' 'ху истинно тогда и только тогда, когда у означает "b".
Теперь глифы можно характеризовать как надписи, которые не могут быть результатом соединения: первый знак - как набор всех глифов, которым лексикографически не предшествует ни один глиф; второй знак - как набор всех глифов, лексикографически следующих за глифами в первом знаке, и т.д. Теперь может быть определена алфавитная функция, например А на подмножестве натуральных чисел от 0 до 127. Значение функции для каждого такого числа - это знак, кодируемый бинарным представлением числа, которое является аргументом. То есть, А:9 = "А".
Определим; | |||
({х (Conc у) = The z Для всех х' Для всех y' Для всех z' | |||
|
{Если х' Принадлежит х |
||
|
& у' Принадлежит у |
||
|
& Pra' ' 'x'y'z' |
||
|
То z' Принадлежит z)). |
||
Теперь имеется механизм орфографического анализа в L. Так, слово "Cat" в L - это А | |||
|
((4:25 Conс А:11) Conc A:39). |
Хотя это не очень легко запоминающееся обозначение, оно совершенно точно. Таким же образом могут быть введены любые другие имена. Очевидно также, как можно описать формальный синтаксис L на L.
Можно определить новый примитивный предикат обозначение:
Prd' 'ху утверждает, что сущность, обозначенная х, обозначает сущность, обозначенную у (является именем для нее).
Это приводит к функции
(Обозначение = Fx {у \ Prd' 'ух}).
Обозначение: х тогда является набором всех сущностей, взятых как имена для х в проблемной области. Естественно, необходимо обеспечить приемлемый набор аксиом, чтобы определить, какие понятия являются именами в определенной проблемной области и какие правила применяются для их назначения, но в любой момент, когда встречается выражение "(N Принадлежит Обозначение: х)", он обозначает, что то, что обозначено N, т.е. именем того, что обозначено х.
Понятие реализации чего-либо, что имеет место в воспринимаемом мире, - основная конструкция, допускающая рассуждение о физическом мире в концептуальных схемах. Реализации, рассматриваемые как индивиды, связываются с определенными точками времени и пространства. Реализации считаются мгновенными и точечными, отличимыми одна от другой и от всех других индивидов. Чтобы описать основные свойства реализаций, вводятся примитивные предикаты, а для того, чтобы установить семантику этих свойств, вводятся аксиомы, налагающие ограничения на эти примитивные предикаты. Первоначальные высказывания о реализациях относятся к их местоположению во времени и пространстве.
Но размещение во времени существенно. Единственный примитивный предикат, достаточный для введения времени, - это
((X Раньше чем Y) | ff Pre' ' XУ).
Основное отношение можно теперь определить следующим образом:
(Раньше = {ху \ х Раньше чем у}).
Удобно также явно определить обратное отношение:
(Позже = Cnv Раньше).
Класс всех реализаций (в смысле физического универсума) определяется как класс всего, что участвует в отношении Раньше:
(Реализации = DI Раньше U Dr Раньше).
Теперь можно ввести аксиомы, относящиеся к предикату "Раньше чем".
(Реализации В l).
Для всех х Для всех у
(Если х Раньше чем у Тогда Не у Раньше чем х).
Для всех х Для всех у Для всех z
(Если х Раньше чем у & у Раньше чем z То х Раньше чем z).
Для всех х Для всех у
(Если х Раньше чем у То для некоторого z
(х Раньше чем z & z Раньше чем y)).
Для всех х
(Если х Принадлежит Реализация То Для некоторого у (у Раньше чем х)).
Для всех х
(Если х Принадлежит Реализациям То Для некоторого у (х Раньше чем у)).
Значение этих аксиом вполне очевидно. Первая утверждает, что реализации - это индивиды, вторая - что отношение Раньше асимметрично, третья - что оно транзитивно, а четвертая - что оно плотно. Последние две устанавливают, что для любой реализации всегда есть, по крайней мере, одна - раньше и одна - позже.
Для моделей интерпретируемой логики предикатов характерно отсутствие фундаментального индивида, представляющего принципиальный интерес; интерес представляют различные множества индивидов. Следовательно:
(События = {х \ Не х = 0 & х В Реализациях}).
Таким образом, события - это непустые подмножества множества реализации.
Раньше и Позже - это соответствующие отношения на реализациях. Перед и После - это соответствующие отношения на событиях,
(Перед = {ху \ х Принадлежит События
& у Принадлежит События
& Для всех х' Для всех y'
(Если x' Принадлежит х
& у' Принадлежит у
То х' Раньше чем y')}).
(После = Cnv Перед).
Таким образом, одно событие происходит перед другим, если каждая реализация в первом осуществляется раньше, чем каждая реализация в другом.
Каждое множество реализаций, не содержащее членов более ранних, чем другие, есть момент. Оно может быть получено из функции, определенной на реализациях и ставящей в соответствие каждой реализации момент, которому она принадлежит:
(Момент = Fx Между Реализациями {у \ у
Принадлежит Реализациям & Не
([х, у] Принадлежит Перед U После)}).
(Моменты = Dl Момент).
При определении понятия "Момент" был введен новый технический прием. Выражение
(Fx Между Y Z = {ух \ х Принадлежит Y & у = Z)} является примером определения, введенного не для того, чтобы описать новые понятия, а лишь для более компактной записи выражения.
Два события одновременны, если моменты, порождаемые их реализациями, совпадают.
Таким образом:
(Одновременно = {ху Между События \ Момент: х = Момент: у}).
С помощью нескольких примитивных предикатов, не описанных здесь, которые устанавливают определенный момент как исходный, другой момент как отстоящий от первого на единицу времени (например, секунду) и момент, определяющий полпути между любыми двумя другими моментами, можно ввести метрику для времени. Тогда каждому моменту времени можно поставить в соответствие определенное число - число секунд, на которое момент отстоит от исходного. Каждому числу в таком случае можно поставить в соответствие событие, являющееся объединением всех моментов, которым соответствует это число. Класс секунды становится таким образом классом событий. Аналогично можно ввести Дни, Месяцы, Годы и в необходимых случаях, такие классы, как Первый день месяца. Январь и т.д.
Если вы являетесь пользователем интернет-версии системы ГАРАНТ, вы можете открыть этот документ прямо сейчас или запросить по Горячей линии в системе.