24.4. ???

А сейчас будут рассмотрены две оставшиеся компоненты - воплощение в "реальных" системах, а также их образ в ментальной сфере, взятой в её абстрактной форме, позляющей с ней работать именно в рамках семантики.

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

23.2.4. Поведение И-ЛИБО систем и его Характерные Черты (ХЧ)

Поэтому, чтобы от характерных черт перейти к собственно поведению, надо, по сути, статическую структуру ХЧ развернуть:

• во времени
• в пространстве всего универсума переменных и их допустимых значений

Итак:

1. Надо чисто формально расширить состав (всех возможных) переменных потока данных именами (всех возможных) вершин, находящихся в состоянии активен / бездействующий.

   Это и будет новый полный универсум, образованным из состояний универсума.

   Тогда (полным) состоянием системы называется произведение произвольного состояния её корневой ВС на состояние активности, которое вычисляется рекурсивно в зависимости от типа очередного узла при условии активности головной вершины.

   В более общем случае, как видно, тип узла зависит от типа системы - рассматриваемой здесь И-ЛИБО, ЛИБО-СЛЕДУЕТ и др.

2. Моменты глобального времени имеют обычный для нашего макро-мира линейный порядок, от рассмотрения которого для конкретного типа системы, возможно, приходится абстрагироваться.
3. Экспериментом над согласованной системой ВС здесь будет называться множество пар, <s,t> образованных состоянием универсума, привязанного ко второй компоненте - моменту глобального времени так, что:
   • s является прообразом некоторого состояния её корневой ВС
   • головной узел находится в состоянии активен, а состояния прочих узлов, если такие имеются, определяются типом системы
   • все(!) состояния потока данных такой системы, то есть все состояния её корневой ВС, участвуют указанным образом в формировании её поведения во время эксперимента
   • как правило, моменты времени эксперимента не исчерпывают всего множества моментов времени, когда наблюдается указанное состояние универсума, являясь его собственным подмножеством

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

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

Для рассматриваемых здесь И-ЛИБО систем отсутствует какая-либо связь между моментами глобального времени, которые между собой даже никак не упорядочены.

Для простоты можно ограничиться лишь их конечными множествами.

И в каждый такой момент каждая переменная потока управления принимает некоторое своё допустимое значение согласно типу узла:

• тип И: активными являются все подсистемы
• тип ЛИБО: активной является лишь та подсистема, к которой из данного узла ведёт дуга с ключом селектора, являющимся проекцией текущего состояния (он существует и единственен согласно теореме ...)

Аналогичным образом далее будет рассмотрена семантика языка ЛИБО-СЛЕДУЕТ систем.

Общая тема монотонности языка имеет практическое воплощение в следующем вопросе:
как соотносится поведение некоторой системы в двух следующих случаях:

• это единственная система (в эксперименте)
• она является частью надсистемы (с которой и производится экспериментм)

Так, если система отлажена автономно, почему при объединении с другими подсистемами её поведение может измениться, привести к ошибке; и можно ли этого избежать?

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

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

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

Это достигается за счёт того, что самая существенная, но минимальная по объёму часть информации в виде И- и ЛИБО-ключей переносится в коммутаторы и селекторы надсистемы, то есть, в её конструкцию, которую разработчик контролирует гораздо полнее, чем поведение.

Этим обеспечивается консервативность всяческих дополнений и развитий.

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

А именно, было выдвинуто предположение, что знание организовано в виде небольших, связанных между собой фрагментов, каждому из которых сопоставляется некоторый "срез" полной реальности.

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

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

Итак, под фрагментом понимается проекция на базис фрагмента некоторого множества состояний универсума, входящих в эксперимент (они, естественно, оказываются связаны отношением ЛИБО).

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

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

Существенным является то, что состояния активности здесь принято считать контролируемыми человеком, чего не всегда можно сказать про поведение.

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

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

А с другой стороны, если такой фрагмент записать в виде формулы и попробовать автоматически интегрировать со всей остальной системой, то собственно тестирование становится излишним - всё, что должно быть проверено таким образом может быть просто предварительно записано в виде формально проверяемой спецификации.

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

Если теперь рассмотреть эксперимент с двумя системами, одна из которых получена консервативным шагом изменения другой, то Главная Теорема говорит, что поведение одной является прообразом для поведение исходной.

Это значит, что если нам требуется (монотонное!) усложнение поведения системы, то это можно сделать консервативным шагом её изменения, что поддаётся формальной проверке.

Надо только помнить, что здесь это допустимо лишь для согласованных систем.

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

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

Пример

Вопрос о том, являются ли "Утренняя звезда" и "Вечерняя звезда" одним и тем-же объектом - Венерой, можно трактовать как вопрос

Назад Вперёд