Композиция отношений и функций.
Частное значение заголовка программы - преобразование внешнего списка строк в строковое представление значения INPUT в таблице выполнения; частное значение точки –преобразование строкового представления OUTPUT в таблице выполнения во внешний список строк. Оставшаяся часть программы между заголовком и финальной точкой последовательно преобразует начальное состояние выполнения в финальное. Таким образом, функция, соответствующая частному значению заголовка программы, предоставляет входные данные для основной части программы, а основная часть программы предоставляет входные данные для функции, соответствующей частному значению финальной точки.
Результат последовательного выполнения функций, выполняющихся одна после другой, где выходные данные предыдущей функции используются как входные данные для следующей, называется композицией.
Композицией отношений r и s, обозначаемая как r ◦ s, является новое отношение всех возможных пар <x, z>, таких, что для некоторого промежуточного значения у, <x, y> Î r и <y, z> Î s. Записанное в set-нотации данное определение будет выглядеть как:
r ◦ s = {<x, z>, :для некоторого у, <x, y> Î r, <y, z> Î s}
Новое понятие, «некоторое y», может быть определено через известные нам понятие области определения отношения. Рассмотрим отношение между парами и промежуточными значениями.
t = {<<x, z>, y>: <x, y> Î r, <y, z> Î s }
Аргумент <x, z> находится в паре с y в t, только тогда когда промежуточное значение y существует, таким образом, значением r ◦ s будут все возможные аргументы t.
r ◦ s = domain(t)
Программное исчисление формализует интуитивно определяемые значения в таблице выполнения, но существует глубокое различие между box-функциями программного исчисления и таблицами выполнения. Box-функция определяет значение программы во всей его полноте, тогда как таблица выполнения описывает только один элемент значения программы, соответствующий заданным входным данным.
Информация в таблице выполнения получается вычислением box-функции к определенному значению аргумента. Начиная с этого аргумента, значение программы значение программы производит набор промежуточных значений в таблице выполнения.
Таким образом, таблица выполнения является представлением композиции частных значений, но вычисленных для одного аргумента.
Композиция box-функций является также функцией (а не просто значением), и может быть использована для вычисления функции значения больших частей программы, тогда как значение, которое предоставляется таблицей выполнения, не может быть использовано в таких вычислениях.
Определение композиции использует понятие промежуточного значения, которое может быть опущено для функций. Если r однозначно определено на x, определение может быть переписано с использованием функциональной формы записи (value-нотации):
r ◦ s = {<x, z>, :для некоторого у, y=r(x), <y, z> Î s}
если дополнительно s однозначно определено на y
r ◦ s = {<x, z>, :для некоторого у, y=r(x), z=s(y)}
Производя замену для y
r ◦ s = {<x, s(r(x))>: r однозначно определено на x. s однозначно определено на r(x) }
в этой форме промежуточное значение, y, не встречается. Когда r и s однозначно определены, композиция также будет однозначно определена на x.
Поскольку все функции определены однозначно, композиция двух функций также является функцией.
Value-нотация предоставляет способ найти значение композиции двух функций. Для вычисления (f ◦ g)(x) сначала находим y=f(x), затем g(y)
Например, функция, заданная композицией
PROGRAM Any (INPUT, OUTPUT) ◦ .
Может быть прямо вычислена для списка строк L. Сначала найдем
y = PROGRAM Any (INPUT, OUTPUT) (L)
и затем .(y)
Таким образом, PROGRAM Any (INPUT, OUTPUT) ◦ .(L)= .(y),
где y = PROGRAM Any (INPUT, OUTPUT) (L)
Результат ,eltn:
y= {INPUT ·<††, u, R>, OUTPUT ·<††, ††, W>},
.(y)= <††>
вне зависимости от строки u, полученной из списка L. Значение строки прошлого в OUTPUT пусто, и этого достаточно для вычисления результата композиции, который оказался постоянной функцией для любого входного списка строк L.
Композиция является ассоциативной, т.е. для любых отношений r, s, t
(r ◦ s) ◦ t = r ◦ (s ◦ t)
потому что
(r ◦ s) ◦ t = {<x,u>: для некоторого z, <x, z> Î (r ◦ s), <x, u> Î t}
= {<x, u>: для некоторого z, некоторого y <x, y> Î r, <y, z> Î s, <z, u> Î t }
= {<x, u>: некоторого y <x, y> Î r, <y, u> Î (s◦ t}
= r◦ (s ◦ t)
Композиция более чем двух отношений не нуждается в скобках, порядок вычисления может быть любым и может определяться удобством вычисления.
Композиция не является коммутативной. Однако, функция эквивалентности (identity function I) и пустая функция коммутативны с любым отношением, т.н. для любого отношения s:
если domain(s) Í domain(I), тогда s ◦ I = I ◦ s = s
s ◦ {} = {} ◦ s = s
Функции и отношения, применение которых в отношении отменяет друг друга называются инверсными, т.е. r является инверсным отношением для s если и только если,
r ◦ s = I
где I – функция эквивалентности для domain(r)
Транспозицией функции или отношения r, обозначаемой rT является отношение, где поменяли местами элементы всех пар в r, т.е:
rT= {<x, y>: <y, x> Î r}
Транспонирование может быть инверсным, и именно в таком качестве оно будет использоваться в программном исчислении. Полезна следующая проверка:
Если транспозицией отношения r является функция, тогда такая транспозиция является прямой инверсией для r.
Чтобы проиллюстрировать это, предположим, что транспозицией r является функция, тогда, по определению композиции,
r ◦ rT = {<x, z>: для некоторого y, <x, y> Î r, <y, z> Î rT}
= {<x, z>: для некоторого y, <y, x> Î rT, <y, z> Î rT}
Поскольку rT – функция, любые два значения, находящиеся в паре с одним аргументом, идентичны, как x и z для y в примере выше. Тогда
r ◦ rT = {<x, x>: для некоторого y, <x, y> Î r, <y, x> Î rT}
= {<x, x>: для некоторого y, <x, y> Î r }
= I, функция эквивалентности над domain(r)
Поэтому rT является прямой инверсией для r.
Значение объявлений.
Синтаксическим объектом, располагающимся между заголовком программы и финальной точкой является блок CFPascal. Частное значение блока преобразует начальное состояние выполнения для блока в конечное. Это преобразование может иметь несколько отдельных частей: декларация переменных и процедур, и корневое выражение BEGIN блока.
Декларация изменяет состояние выполнения, добавляя к нему один или несколько идентификаторов. До выполнения декларации идентификаторы не существуют, после декларации они могут иметь значения. Частное значение декларации изменяет область определения состояния выполнения, добавляя идентификатор. Будет удобно отдельно разделять декларации для типов CHAR, TEXT и PROCEDURE.
Значение деклараций будет описываться с помощью отношений, которые не являются функциями. Отношение будет состоять из пар всех возможных значений и имени объявленного идентификатора, фиксируя идею, что значение неизвестно.
Для переменной N типа CHAR определим:
VAR N: CHAR = {<s, t>: t = s È {<N, x>} для любого символьного значения x}
Строка N соответствует синтаксису <идентификатора> и строка VAR N: CHAR формально должна быть представлена как:
V = †VAR† & N & †CHAR†
При использовании символа ? для обозначения значения N:
VAR N: CHAR = {<s, t>: t = s È {<N, ?>} }
не так очевидно, что любые символьные значения образуют пары с N. Например, пусть s будет аргументом VAR N: CHAR, тогда s будет:
s È {Ch·A},
s È {Ch·B},
…
для всех возможных символьных значений.
Хотя VAR N: CHAR не является функцией, VAR N: CHART является функцией, потому что ее пары имеют вид:
<s È {N·A}, s>
<s È {N·B}, s>
…
и каждому аргументу соответствует уникальное значение.
Значение декларации файловых переменных аналогично. Пусть N – идентификатор, определим:
VAR N: TEXT = {<s, t>: t = s È {N·<x, y, z>} для некоторых строк x, y и некоторого z Î {R,W}}
Сокращенная форма записи присоединяет 3-список <?,?,?> к вновь созданному идентификатору.
Объявления более, чем одной переменной являются прямым обобщением рассмотренног. К состоянию выполнения добавлается несколько идентификаторов, каждый в паре с неопределенным символьным значением или 3-списком.
Это может быть выражено композицией:
VAR Сh1, Ch2: CHAR = VAR Сh1: CHAR ◦ VAR Ch2: CHAR
= {<s, t>: t = s È {Ch1·?} È {Ch2·?}}
которая включает пары, такие как
<s, s È {Ch1·C} È {Ch2·F}>
и все остальные комбинации двух символьных значений.
Предположим, что
x = {INPUT ·<††, †† , R>, OUTPUT ·<††, ††, W>}
является аргументом отношения VAR Сh: CHAR, тогда x образует пары в отношении для
{INPUT ·<††, †† , R>, OUTPUT ·<††, ††, W>} È {Ch·с}
для всех символьных значений c. Представим это в виде формулы:
VAR Сh: CHAR ({INPUT ·<††, †† , R>, OUTPUT ·<††, ††, W>})
= { INPUT ·<††, †† , R>, OUTPUT ·<††, ††, W>, Ch·?}
Объявление процедур, насколько нам в данный момент известно, не изменяет количество в столбцов в таблице выполнения. Когда позднее идентификатор процедуры используется в в процедурном выражении, вызывается <тело> процедуры. Задача объявления процедуры - записать информацию, которая сделает возможными действия описанные в процедуре. Этот текст присоединяется к идентификатору процедуры подобно значению из таблицы выполнения для переменной.
Для идентификатора процедуры N и тела T, определим:
PROCEDURE N; T = {<s, t>: t = s È {<N, T>}}
При определении значения декларативной части и значений других частей программы мы принимаем, что программа и ее части синтаксически корректны. Строки, не соответствующие синтаксическим и контекстным правилам, не могут иметь значений.
Вычисляя значения только синтаксически корректных программ, мы исключаем из рассмотрения все затруднения связанные с неправильным синтаксисом. Например, если бы было возможным повторное объявление идентификатора, необходимо было бы описать и рассматривать такую ситуацию. Но поскольку это синтаксическая ошибка, семантическое определение не рассматривает такую возможность.
Значение блоков.
Блок может содержать ноль или больше объявлений переменных и процедур, но он должен завершаться оператором BEGIN. Простейший блок не содержит объявлений или операторов внутри BEGIN
BEGIN
END
Поскольку в таблице выполнения такой блок не меняет значений переменных, то его преобразование одно состояния программы в другое состояние программы является функцией эквивалентности I.
BEGIN END = I
Когда блок содержит объявления, пары идентификатор-значение добавляются к исходному состоянию выполнения до того как выполнится оператор BEGIN, а после его выполнения удаляются из состояния выполнения. Например, если частным значением VAR … добавлены переменные, тогда нам необходимо VAR …T чтобы удалить эти значения из состояния выполнения.
Простой блок
VAR
Ch: CHAR;
BEGIN
END
с частным значением:
VAR Ch: CHAR; BEGIN END = VAR Ch: CHAR ◦ BEGIN END ◦ VAR Ch: CHAR T
а именно, композицией, которая сначала добавляет Ch·? к состоянию выполнения, потом выполняет эквивалентные преобразования, потом удаляет Ch и значение из состояния выполнения. Начинаясь с состояния выполнения:
{INPUT ·<††, Ñ / , R>, OUTPUT ·<††, ††, W>}
композиция имеет следующее значение:
(VAR Ch: CHAR ◦ BEGIN END ◦ VAR Ch: CHAR T )
({INPUT ·<††, Ñ / , R>, OUTPUT ·<††, ††, W>})
= (BEGIN END ◦ VAR Ch: CHAR T )
({INPUT ·<††, Ñ / , R>, OUTPUT ·<††, ††, W>, Ch·?})
= (VAR Ch: CHAR T ) ({INPUT ·<††, Ñ / , R>, OUTPUT ·<††, ††, W>, Ch·?})
= {INPUT ·<††, Ñ / , R>, OUTPUT ·<††, ††, W>}
То есть как и ожидалось, VAR Ch: CHAR содержит все пары из
<s, s È {Ch·c}>, для любого символьного значения c
которое мы сокращенно записали добавив Ch·? К состоянию выполнения.
BEGIN END не изменяет состояние выполнения, а VAR Ch: CHAR T удаляет пару сокращенно обозначенную как Ch·?
Общий случай для частного значения блока следует аналогичен вышеописанному. Когда объявления отсутствуют, значение блока – это просто значение выражения BEGIN. Когда присутствуют объявления процедур или переменных F, за которыми следует оператор BEGIN B, значение блока будет
F; B = F ◦ B ◦ F T
Блок с объявлением одной переменно и одной процедуры может быть проанализирован примерно следующим образом:
VAR … ; PROCEDURE … ; BEGIN … END
= VAR … ; ◦ PROCEDURE … ; BEGIN … END ◦ VAR … ; T
= VAR … ; ◦ PROCEDURE … ; ◦ BEGIN … END ◦ VAR … ; T
Мы типично для программного исчисления описали частное значение блока. Подстрока программы, соответствующая определенной синтаксической части, в дальнейшем разбивается на подстроки и значение исходной подстроки определяется через значения элементов на которые она была разбита.
В дальнейшем мы рассмотрим частные значения операторов CF Pascal, но рассматривая результаты выполнения операторов в таблице выполнения, мы уже сейчас можем получить формальное представление программы.
PROGRAM CopyChar (INPUT, OUTPUT);
VAR
Ch: CHAR;
BEGIN
READ(Ch);
WRITELN(Ch)
END.
Значение программы Q может быть вычислено для 1-списка <†ABC†>
Q (<†ABC†>) = PROGRAM … END. (<†ABC†>)
= PROGRAM … ◦ VAR … END ◦. (<†ABC†>) (1)
= VAR … END ◦ . ({INPUT ·<††, ABC/ , R>, OUTPUT ·<††, ††, W>}) (2)
= VAR … ◦ BEGIN … END ◦ VAR … T ◦ .
({INPUT ·<††, ABC/ , R>, OUTPUT ·<††, ††, W>}) (3)
= BEGIN … END ◦ VAR … T ◦ .
({INPUT ·<††, ABC/ , R>, OUTPUT ·<††, ††, W>, Ch·?}) (4)
= VAR … T ◦ .({INPUT ·<†A†, BC/ , R>, OUTPUT ·<†A/†, ††, W>, Ch·A}) (5)
= .({INPUT ·<†A†, BC/ , R>, OUTPUT ·<†A/†, ††, W> }) (6)
= <†A†>
Шаг (1) детализирует значение программы Q через композицию заголовка блока и точки. Шаг (2) применяет композицию оставшихся компонентов к значению заголовка. Шаг (3) расширяет значение блока до композиции объявлений, оператора BEGIN и транспозиции объявления. Шаг (4) применяет композицию оставшихся компонентов к значению программы после выполнения деклараций. Шаг (5) применяет композицию оставшихся компонентов к значению программы после выполнения оператора BEGIN. Шаг (6) показывает значение программы после применения к предыдущему значению транспозиции объявлений. Шаг (7) фиксирует значение программы после выполнения финальной точки.
Объединим наши знания об области определения и значений для частей программы в следующей таблице.
| Часть программы | Область определения | Область значений |
| программа | список строк | список строк |
| заголовок программы | список строк | состояния выполнения |
| точка | состояния выполнения | список строк |
| блок | состояния выполнения | состояния выполнения |
| объявление | состояния выполнения | состояния выполнения |
| оператор BEGIN | состояния выполнения | состояния выполнения |