Предикат түрлендірушісінің қасиеттері

  1. R соңғы шартының функциясы бетінде қарастырылатын предикаттар түрлендірушісімен бірнеше анықталған қасиеттерге ие.

Қасиет 1. Кез келген S конструкциясы үшін

WP (S,F)=F

Айталық, бұл теңдік орындалмасын. Мұндай WP (S,F) шартын қанағаттандыратын ең болмаса бір жағдай табылар еді. Бұл жағдайда S  конструкциясының бастапқы жағдайы ретінде аламыз. Анықтамаға сәйкес  S-і іске қосу F предикатын қанағаттандырады соңғы жағдайға әкеледі. Бірақ бұл жерде қарама-қайшылық туады, F предикатының анықтамасы бойынша F-і қанағаттандыратын жағдай  жоқ, осылайша (4) қатынасты дәлелдейді.

Қасиет 2.  Кез-келген S конструкциясы және барлық жағдайлар үшін (5)  Q=>R қатынасы орындалатын Q, R соңғы шарттары үшін мына қатынас орындалады.

WP(S,Q)=> WP(S,R)    (6)

Шындығында, WP(S,Q) –і үшін қанағаттандыратын кез келген бастапқы жағдайда жүйе жұмысының ақырғы жағдайы үшін анықтама бойынша Q орындалады. (5) қатынасын ескерсек  R-ң де орындалатындығы келіп шығады. Демек, берілген бастапқы жағдай бір мезгілде WP(S,R) шартын да қанағаттандыратын болады, (6)-да көрсетілгендей қасиет-2 бұл монотондық қасиет.

  1. Қасиет 3. Кез келген S конструкциясы және Q және R соңғы шарттар үшін WP(S,Q) and  WP(S,R) = WP(S,Q and R)  (7) ќатынасы орындалады. [and =  ]

Жағдайлар кеңестігінің кез келген нүктесінде  (7) –ң сол жағынан оң жағы келіп шығады, өйткені WP(S,Q) және WP(S,R) –ді қанағаттандыратын кез келген бастапқы жағдайлар үшін Q және R-ді қанағаттандыратын жағдайдың болатындығын білеміз. Одан әрі анықтамаға сәйкес барлық жағдайлар үшін

(Q and R)=>Q

ќасиет 2-ні ескеріп барлық жағдайлар үшін  WP(S,Q and R )=> WP(S,Q)

дәл осылай барлық жағдайлар үшін  WP(S,Q and R )=> WP(S,R) бола алады. Бірақ A=>B және A=>C болса, онда  A=>(B and C) деуімізге болады. Сондықтан жағдайлар кеңіәстігінің кез келген нүктесінде (7) –ң оң жағынан сол жағы келіп шығады. Екі жақта барлық жерде бірінен – бірі келіп шығатындықтан олар тең болу керек. Осылай 3-қасиет  дәлелденеді.

  1. Қасиет 4. Кез келген Sконструкциясы үшін және кез келген Q және R соңғы шарттар үшін  (WP(S,Q or R )=> WP(S,R))=> WP(S,Q or R ) (8) қатынасы барлық жағдайлар үшін ақиқат болады.

Анықтамаға сәйкес барлық жағдайлар үшін WP(S,Q )=> WP(S,Q or R) дәл осылай WP(S,R )=> WP(S,Q or R) барлық жағдайда A=>C және B=>C үшін (A or B)=>C деуге болады. Осылай (8) қатынастың ақиқат екендігі дәлелденеді.

Қасиет 4. Кез келген детерминерленген S конструкциясы кез келген Q және R  соңғы шарттар үшін

(WP(S,Q ) or WP (S,R))=WP(S,Q or R) (8)

Бұл қатынастың енді оң жағынан сол жағы келіп шығатынын көрсету қажет. WP(S,Q or R ) алғы шартын қанағаттандыратын қайсы бір бастапқы жағдайда қарастырайық, бұл бастапқы жағдайға жалғыз ғана ақырғы жағдай сәйкес келеді. Ол Q- ді R-ді не екеуінде қанағаттандыруы мүмкін, бұдан шығатыны бастапқы жағдай WP(S,Q) –ді не WP(S,R)-ді не екеуінде, яғни ол WP(S,Q) or WP(S,R)-ді қанағаттандыруы керек. Сонымен 4-қасиет дәлелденді. [детерминерленген машина үшін конструкцияны іске қосқанда кейінгі оқиғалар толығымен оның бастапқы жағдайымен анықталады. Бірдей бастапқы жағдайда екі мәрте қайталап іске түсірсек, бірдей оқиғалар жүреді деп айта алмаймыз. Мүмкін болған оқиғалар класының қайсы бір оқиғасы жүреді]. F арқылы жағдайлар кеңестігінің барлық нүктесінде жалған болатын предикатын белгілейміз; ол бос жиынға сәйкес келеді.

«Baribar.kz-тің» Telegram-каналына жазыламыз!