В результате заключаем , что утверждение Y ( s, t ,u ,…) истинно для
всех s Î A * .
Аналогично проводится процесс доказательства для всех остальных переменных t ,u ,…
.
Пример доказательства. Докажем свойство Ax6. ( c-> s ) ¹ <> методом структурной индукции по s .
B(базис индукции) . Согласно Ax4 имеем ( c-> <> ) ¹ <> для всех сÎ A .
I ( индукционная гипотеза ) . ( c-> s ) ¹ <> для всех сÎ A .
S (шаг индукции) . Согласно Ax3 и индукционной гипотезе имеем
( c-> ( c-> s ) ) ¹ ( c-> s ) ; кроме того , для всех d , где d ¹ c , по Ax3
имеем ( d-> ( c-> s ) ) ¹ ( c-> s ) . Таким образом , последнее соотношение
имеет место независимо от того ,c=d или c ¹ d , и свойство Ax6 доказано.
Если s ¹ <> , то будем обозначать через s0 первый символ , а через
s' - результат удаления первого символа из следа s .
Формально это определяется так :
Ax7. ( c-> s )0 =c
Ax8. ( c-> s )' =s .
Отсюда можно вывести свойство :
Ax9. ( c-> s ) = t - ( t ¹ <> ) & ( t0 = c & t' = s)
В LISP - нотации следы можно представлять списками .
Например :
<> - nil (пустой список) ;
( c-> s ) - cons( "c" , s ) ;
s0 - head( s ) ;
s' - tail( s ) .
2.5.1.1. Конкатенация.
Через st обозначается результат конкатенации следов s и t .
Формально это определяется следующим образом :
c1. <> t = t ,
c2. ( c-> s) t = c-> ( st )
Операция конкатенации в LISP - нотации описывается функцией
append( s, t ) , определяемой как
append( s, t )= df ls,t . IF( s=<> , t ,cons ( s0,append(s',t) ) )
Для этой операции справедливы следующие свойства :
c3. s = s<> ;
c4. ( st )u = s( tu ) ;
c5 st = su - t = u ;
c6. st = <> - s = <> & t = <> ;
c7. stÎ A * - s Î A * & t Î A * .
Перечисленные свойства доказываются методом структурной индукции.
В качестве примера докажем свойство c4 :
B(базис индукции) . ( <> t )u = <>( tu ) ( согласно c1 ) .
I ( индукционная гипотеза ) . Пусть ( st )u = s( tu ) для некоторого s .
S (шаг индукции) .
( (c->s)t )u = (c->(st))u (согласно c2)
= c-> ((st)u) u (согласно c2)
= c-> (s(tu)) (по индукционной гипотезе)
= (c -> s )( tu ) (согласно c2)
Для полного завершения доказательства следует провести аналогичное доказательство по переменной t .
Упражнения к разделу . Доказать свойства c3 , c5-c7 .
2.5.1.2. Префикс.
След s является префиксом следа t (обозначается , как s £ t ), если
t начинается с копии s . Формально это определяется так :
p1 . s £ t = df $ u (su=t ) .
Cправедливы следующие свойства префикса :
p2 . <> £ t , для любого следа t ;
p3. ù (( c->s ) £ <> ) ;
p4. ( c->s ) £ ( d-> t ) - c = d & s £ t
Упражнения к разделу . Сформулировать какие-нибудь другие свойства
префикса и доказать их .
2.5.1.3. Операция "после".
Пусть s £ t . Тогда операция t/s ( читается t после s) определяется
следующими аксиомами :
a1. t/<> = t ;
a2. ( c-> t )/ (c->s) =t/s
Пример . < a,b,c,d >/< a,b > = < c,d > .
Cправедливы следующие свойства операции "после" :
a3. (st)/s=t ;
a4. s £ t => s( t/s )= t ;
a5. ((s £ t)& (s£ u)&(t/s=u/s))=> t=u ;
a6. (su) £ t => t/(su)= (t/s)/u .
Данную операцию можно определить с помощью LISP -нотации
следующим образом :
t/s = df after( t, s ) , где after( t, s )= df lt,s . IF( s=<> , t ,after( t' , s' ))
Упражнения к разделу . Доказать свойства a3 - a5 .
2.5.1.4. Проекция .
Пусть B -множество символов , а s -след . Тогда проекция следа s на
множество B ( обозначение s é B) получается удалением из следа s
всех символов , не принадлежащих множеству B . Формально эта
операция определяется следующими аксиомами :
r1. <> é B = <> ;
r2. c Î B => (c-s) é B =c->(s é B) ;
r3. c Ï B => (c-s) é B =c->(s é B) ;
Cправедливы следующие свойства проекции :
r4. s é { } =<> ;
r5. (st) é B = (s é B)(t é B) ;
r6. (s é C) é B=s é (CÇ B) ;
r7. s é B = s - sÎ B* ;
Примеры .
< a,b > é { a,c } = <a>
< a ,c > é { a,c } = <a,c>
< a,b,c,d > é { e } = <>
Упражнения к разделу . Доказать свойства r4 - r7 .
2.5.1.5. Последовательная композиция .
Будем использовать специальный символ Ö для обозначения
успешного завершения следа . Тогда через ( s ; t ) обозначается след ,
получившийся в результате подстановки следа t вместо первого
вхождения символа Ö в s и удаления остатка следа s (то есть той части
следа s , которая следует после символа Ö ) . Если s не содержит Ö ,
то s ; t = s .
Формально эту операцию можно определить так :
s1. <> ; t=<> ;
s2. (<Ö >s ) ;t = t ;
s3. ( c->s );t = c-> (s;t) , c¹Ö .
Поскольку символ Ö является признаком успешного завершения следа ,
то будем исключать из рассмотрения случаи , когда Ö появляется внутри
следа ( например , <a,b,Ö ,c > ) , то есть в любом случае имеет место
соотношение s < Ö > t = s .
Cправедливы следующие свойства последовательной композиции :
s4. (s;t);u = s ;(t;u) ;
s5. (< Ö > ; s) = s ;
s6. (s;t)0 = s0 , s0 ¹Ö ;
Упражнения к разделу . Доказать свойства s4 -s6 .
2.5.1.6. Переименование .
Пусть f - функция , отображающая один алфавит в другой . Если
s - след , построенный из символов , входящих в область определения
функции f , то определим функцию f *(s) как след , получающийся из
следа s путем применения функции f к каждому из его символов .
Формально :
f1. f *(<>) = <> ;
f2. f *(c-> s) = f(c) -> f *(s) .
Аналогично , если B - множество символов из области определения
Функции f , то f *(B) = df { f*(B) | bÎ B } .
Условимся , что :
f3. f*(c) = Ö - c=Ö .
Пример. Пусть f(a)=x , f(b)=y , f(c)=z , f*(Ö ) = Ö , тогда :
f *( < a , b ,c > = < x,y,z > , f *( { a , b ,c } ) = { x,y,z }
Cправедливы следующие свойства операции переименования :
f4. f *(st) = f *( s ) f *( t ) ;
f5. f *(s / t) = f *( s ) / f *( t ) ;
f6. f *(s é B) = f *( s ) é f *( B ) ;
f7. f *(s; t) = f *( s ) ; f *( t )
Упражнения к разделу . Доказать свойства f4 -f7 .
2.5.2. Теория процессов.
Процесс с заданным алфавитом определяется множеством следов ,
символы которых принадлежат этому алфавиту . Каждый след
описывает возможную последовательность событий , в которых процесс может участвовать в определенный момент времени . Формально процесс P - это любое множество следов в алфавите A , для которого выполняются следующие аксиомы :
P0. PÍ A * ;
P1. <> Î P ;
P2. st Î P => s Î P ;
Каждый процесс будет определяться парой (A,P) , где A- алфавит процесса , а P - множество следов в алфавите A . Выделим следующие процессы - примитивы :
FAILA = df ( A , { <> } ) - пустой процесс в алфавите A , который никогда
" ничего не делает " ;
(A , A *)- универсальный процесс в алфавите A , который " все делает".
В дальнейшем для удобства процесс P будем рассматривать просто как множество следов , выделяя его алфавит лишь в тех случаях , когда это необходимо , обозначая через aP алфавит процесса P .
Примеры процессов в алфавите { a, b } : { <> } , { <>,< b > } ,
{ <>,< a >,< a, b > } , { <>,< a >,< a, b > ,< b > , < b, a > } .
Для процессов-примитивов справедливы следующие ниже свойства .
P3. FAILA является процессом в алфавите A .
P4. A * является процессом в алфавите A .
P5. aP= A => FAILA Í P .
Доказательство свойств P3 , P4 . Для доказательства свойств достаточно
показать выполнение аксиом P0 - P2 .
Доказательство (P3) :
P0 . { <> } Í A * ( согласно аксиоме Ax1 ) ;
P1. <> Î { <> } ( согласно теории множеств ) ;
P2. ( st Î { <> } ) = > (st = <>) => (s=<>) => ( s Î { <> } ) ( согласно c6 ) .
Доказательство (P4) :
P0 . A * Í A * ( очевидно ) ;
P1. <> Î A * ( согласно аксиоме Ax1 ) ;
P2. ( st Î A * ) = > ( s Î A * ) ( согласно c7 ) .
2.5.2.1 . Операция присоединения символа .
Если P - процесс , а cÎ aP , то (c->P) определяется как процесс , который начинается с события c , а затем выполняется как процесс P .
Формально это определяется так :
(c->P) = df {<>} È { (c -> s) | cÎ aP & sÎ P } .
Справедливо следующее утверждение.
Pr1. Если P -процесс , а cÎ aP , то (c->P) является процессом в
алфавите aP .
Для доказательства Pr1 достаточно показать выполнение аксиом
P0 - P2 аналогично доказательству свойств P3 , P4 .
2.5.2.2 . Альтернативная операция .
Если P и Q -процессы , то операция P | Q определяется как P или Q .
Формально эта операция определяется следующим образом :
P | Q= df P È Q , где a (P | Q ) = aP È aQ .
Cправедливы следующие свойства :
U1. если P и Q -процессы , то P | Q также является процессом ;
U2. операция P | Q коммутативна и ассоциативна ;
U3. P | (aP) * = (aP) * ;
U4. P | FAIL = P .
Примеры.
А) ( a->(b-> FAIL)) | ( b-> FAIL ) ={ <>,< a > ,< a,b > , < b > } .
Б) Оператор if b then P else Q можно представить в виде
(b->P)| (ù b->Q) , где ù b рассматривается как событие отрицания b .
B) Операцию (a->P | b-> Q) можно интерпретировать как меню-диалог,
где { a,b } - меню из двух элементов a,b ,где выбор элемента a
активизирует процесс P , выбор элемента b активизирует процесс Q .
Упражнения к разделу . Доказать свойства U1 -U4 .
2.5.2.3. Начальное состояние процесса .
Если P - процесс , то определим P0 как множество символов ,опреде-ляющих стартовое состояние процесса :
P0 = df { c | < c > Î P }
Cправедливы следующие свойства :
O1. ( FAIL ) 0 = { } ;
O2. (A *)0 = A ;
O3. ( c-> P ) 0 = { c } ;
O4. ( P |Q ) 0 = P0 È Q0
Пример. (( a-> P) | ( b-> Q )) 0 = ( a-> P) 0 È ( b-> Q ) 0 .
Упражнения к разделу . Доказать свойства O1 -O4 .
2.5.2.4. Операция "после".
Если s - след процесса P , определим P/s (P после s) как множество следов , определяющее поведение процесса P после следа s :
P/s = df { t | st Î P } .
Cправедливы следующие свойства :
A1. если P - процесс и sÎ P , то P/s - процесс ;
A2. P/<> = P ;