Теормин (2006) (мини) (1162021), страница 5
Текст из файла (страница 5)
Ɍɨɝɞɚ ɞɟɪɟɜɨɦ SLD-ɪɟɡɨɥɸɬɢɜɧɵɯ ɜɵɱɢɫɥɟɧɢɣɡɚɩɪɨɫɚ G ɤ Ɋ ɧɚɡɵɜɚɟɬɫɹ ɤɨɪɧɟɜɨɟ ɭɩɨɪɹɞɨɱɟɧɧɨɟ (ɬ.ɟ. ɜɵɯɨɞɹɳɢɟ ɢɡ ɥɸɛɨɝɨ ɭɡɥɚ ɞɭɝɢɩɪɨɧɭɦɟɪɨɜɚɧɵ) ɞɟɪɟɜɨ, ɨɛɥɚɞɚɸɳɟɟ ɫɥɟɞɭɸɳɢɦɢ ɫɜɨɣɫɬɜɚɦɢ:1) ɤɚɠɞɨɣ ɜɟɪɲɢɧɟ ɩɪɢɩɢɫɚɧ ɡɚɩɪɨɫ;2) ɤɨɪɧɸ ɞɟɪɟɜɚ ɩɪɢɩɢɫɚɧ ɡɚɩɪɨɫ G;3) ɢɡ ɤɚɠɞɨɣ ɜɟɪɲɢɧɵ, ɩɨɦɟɱɟɧɧɨɣ ɡɚɩɪɨɫɨɦ G0 , ɢɫɯɨɞɹɬ ɞɭɝɢ, ɩɨɦɟɱɟɧɧɵɟɧɚɬɭɪɚɥɶɧɵɦɢ ɱɢɫɥɚɦɢ 1 d i1 d ... d ik d N , ɝɞɟ N – ɤɨɥɢɱɟɫɬɜɨ ɩɪɨɝɪɚɦɦɧɵɯɭɬɜɟɪɠɞɟɧɢɣ ɜ Ɋ, ɢ ɢɞɭɳɢɟ ɜ ɜɟɪɲɢɧɵ, ɩɨɦɟɱɟɧɧɵɟ G1 , G2 ,..., Gk ɜ ɬɨɦ ɢ ɬɨɥɶɤɨ ɜ ɬɨɦɫɥɭɱɚɟ, ɤɨɝɞɚ l [1, k ] ɡɚɩɪɨɫ Gl ɩɨɥɭɱɟɧ ɢɡ ɡɚɩɪɨɫɚ G ɩɭɬɟɦ ɩɪɢɦɟɧɟɧɢɹɩɪɨɝɪɚɦɦɧɨɝɨ ɭɬɜɟɪɠɞɟɧɢɹ Drl ɢ ɩɪɢ ɷɬɨɦ ɞɪɭɝɢɯ SLD-ɪɟɡɨɥɶɜɟɧɬ, ɢɧɰɢɞɟɧɬɧɵɯ G0 ,ɧɟɬ.Ɍɚɤɢɦ ɨɛɪɚɡɨɦ, ɤɚɠɞɚɹ ɜɟɬɜɶ ɬɚɤɨɝɨ ɞɟɪɟɜɚ ɛɭɞɟɬ ɫɨɨɬɜɟɬɫɬɜɨɜɚɬɶ ɜɵɱɢɫɥɟɧɢɸ ɨɬɜɟɬɚ ɧɚɡɚɩɪɨɫ G ɤ ɥɨɝɢɱɟɫɤɨɣ ɩɪɨɝɪɚɦɦɟ Ɋ.Ɉɩɪɟɞɟɥɟɧɢɟ.
ɋɬɪɚɬɟɝɢɟɣ ɜɵɱɢɫɥɟɧɢɹ ɧɚɡɵɜɚɟɬɫɹ ɫɬɪɚɬɟɝɢɹ ɨɛɯɨɞɚ ɞɟɪɟɜɚ SLDɪɟɡɨɥɸɬɢɜɧɵɯ ɜɵɱɢɫɥɟɧɢɣ:x ɫɬɪɚɬɟɝɢɹ ɨɛɯɨɞɚ ɜ ɲɢɪɢɧɭ: ɩɨɹɪɭɫɧɨɟ ɩɨɫɬɪɨɟɧɢɟ ɞɟɪɟɜɚ. Ʉɚɤ ɬɨɥɶɤɨ ɜ ɨɞɧɨɣɢɡ ɜɟɬɜɟɣ ɨɛɧɚɪɭɠɢɜɚɟɬɫɹ , ɬɨ ɨɬɜɟɬ ɜɵɱɢɫɥɹɟɬɫɹ ɩɭɬɟɦ «ɫɛɨɪɚ» ɜɫɟɯɩɨɞɫɬɚɧɨɜɨɤ ɧɚ ɞɚɧɧɨɣ ɜɟɬɜɢ;x ɫɬɪɚɬɟɝɢɹ ɨɛɯɨɞɚ ɜ ɝɥɭɛɢɧɭ ɫ ɜɨɡɜɪɚɬɨɦ – ɩɨɫɬɪɨɟɧɢɟ ɞɟɪɟɜɚ ɩɨ ɜɟɬɜɹɦ (ɧɚɤɚɠɞɨɦ ɷɬɚɩɟ ɜɵɛɢɪɚɟɬɫɹ ɫɚɦɚɹ ɥɟɜɚɹ ɢɡ ɧɟɩɪɨɣɞɟɧɧɵɯ ɜɟɬɜɟɣ)Ɉɩɪɟɞɟɥɟɧɢɟ. ɋɬɪɚɬɟɝɢɹ ɜɵɱɢɫɥɟɧɢɹ (ɨɛɯɨɞɚ ɞɟɪɟɜɚ SLD-ɪɟɡɨɥɸɬɢɜɧɵɯ ɜɵɱɢɫɥɟɧɢɣ)ɧɚɡɵɜɚɟɬɫɹ ɩɨɥɧɨɣ, ɟɫɥɢ ɞɥɹ ɥɸɛɨɝɨ ɡɚɩɪɨɫɚ G ɤ ɥɨɝɢɱɟɫɤɨɣ ɩɪɨɝɪɚɦɦɟ Ɋ ɜɫɟ ɜɵɱɢɫɥɟɧɧɵɟɨɬɜɟɬɵ ɛɭɞɭɬ ɩɨɫɬɪɨɟɧɵ.19Ɉɩɪɟɞɟɥɟɧɢɟ. Ɉɩɟɪɚɬɨɪ ɨɬɪɢɰɚɧɢɹ (not) – ɷɬɨ ɨɩɟɪɚɬɨɪ ɥɨɝɢɱɟɫɤɨɝɨ ɩɪɨɝɪɚɦɦɢɪɨɜɚɧɢɹ ɫɨɫɥɟɞɭɸɳɟɣ ɨɩɟɪɚɰɢɨɧɧɨɣ ɫɟɦɚɧɬɢɤɨɣ:ɉɭɫɬɶ Ɋ – ɥɨɝɢɱɟɫɤɚɹ ɩɪɨɝɪɚɦɦɚ, ɚ G – ɡɚɩɪɨɫ ɜɢɞɚ not(A).
Ɍɨɝɞɚ ɪɟɚɤɰɢɹ ɢɧɬɟɪɩɪɟɬɚɬɨɪɚ ɧɚɞɚɧɧɵɣ ɡɚɩɪɨɫ ɛɭɞɟɬ ɫɥɟɞɭɸɳɟɣ:1) ɟɫɥɢ ɫɭɳɟɫɬɜɭɟɬ ɭɫɩɟɲɧɨɟ SLD-ɪɟɡɨɥɸɬɢɜɧɨɟ ɜɵɱɢɫɥɟɧɢɟ ɧɚ ɡɚɩɪɨɫ G ' : ? A , ɬɨɪɟɡɭɥɶɬɚɬɨɦ ɜɵɱɢɫɥɟɧɢɹ ɛɭɞɟɬ fail;2) ɟɫɥɢ SLD-ɪɟɡɨɥɸɬɢɜɧɨɟ ɞɟɪɟɜɨ ɜɵɱɢɫɥɟɧɢɣ ɞɥɹ ɡɚɩɪɨɫɚ G ' : ? A ɩɪɟɞɫɬɚɜɥɹɟɬ ɫɨɛɨɣɤɨɧɟɱɧɨɟ ɱɢɫɥɨ ɧɟɭɞɚɱɧɵɯ ɜɟɬɜɟɣ, ɬɨ ɡɚɩɪɨɫ G ɢɦɟɟɬ ɭɫɩɟɲɧɨɟ ɜɵɱɢɫɥɟɧɢɟ;3) ɟɫɥɢ ɢɧɬɟɪɩɪɟɬɚɬɨɪɭ ɧɟ ɭɞɚɥɨɫɶ ɨɛɨɣɬɢ ɜɫɟ ɜɟɬɜɢ ɞɟɪɟɜɚ ɡɚ ɤɨɧɟɱɧɨɟ ɱɢɫɥɨ ɲɚɝɨɜ (ɬ.ɟ.ɟɫɥɢ ɜ SLD-ɪɟɡɨɥɸɬɢɜɧɨɦ ɞɟɪɟɜɟ ɜɵɱɢɫɥɟɧɢɣ ɞɥɹ ɡɚɩɪɨɫɚ G ' : ? A ɩɪɢɫɭɬɫɬɜɭɟɬ ɯɨɬɹɛɵ ɨɞɧɚ ɛɟɫɤɨɧɟɱɧɚɹ ɜɟɬɜɶ, ɚ ɨɫɬɚɥɶɧɵɟ ɧɟɭɞɚɱɧɵ), ɬɨ ɨɬɜɟɬɨɦ ɧɚ ɡɚɩɪɨɫ G ɛɭɞɟɬ f .Ɍɚɤɢɦ ɨɛɪɚɡɨɦ, ɨɩɟɪɚɬɨɪ not ɪɚɛɨɬɚɟɬ ɧɚ ɨɫɧɨɜɟ «ɩɨɱɬɢ ɬɪɟɯɡɧɚɱɧɨɣ» ɥɨɝɢɤɢ, ɱɬɨ ɞɚɟɬɷɮɮɟɤɬ ɧɟɦɨɧɨɬɨɧɧɨɫɬɢ ɜɵɜɨɞɚ.4. Ɉɛɡɨɪ ɪɚɡɞɟɥɨɜ ɦɚɬɟɦɚɬɢɱɟɫɤɨɣ ɥɨɝɢɤɢ4.1. ɂɫɱɢɫɥɟɧɢɟ ɩɪɟɞɢɤɚɬɨɜ ɢ ɷɥɟɦɟɧɬɚɪɧɚɹ ɬɟɨɪɢɹɂɫɱɢɫɥɟɧɢɟ ɩɪɟɞɢɤɚɬɨɜ ɫɨɫɬɨɢɬ ɢɡ ɫɢɫɬɟɦɵ ɚɤɫɢɨɦ ɢ ɩɪɚɜɢɥ ɜɵɜɨɞɚ.
ɋɭɳɟɫɬɜɭɟɬ ɦɧɨɝɨɪɚɡɧɵɯ ɫɢɫɬɟɦ ɚɤɫɢɨɦ.ɋɢɫɬɟɦɚ ɚɤɫɢɨɦ:Ax1: M o \ o M Ax 2 : M o \ o F o M o \ o M o F - ɡɚɤɨɧ ɫɥɨɠɧɨɝɨ ɫɢɥɥɨɝɢɡɦɚ20Ɇɚɬɟɦɚɬɢɱɟɫɤɚɹ ɥɨɝɢɤɚ, ɫɜɨɞɤɚ ɨɩɪɟɞɟɥɟɧɢɣ. (ɫ) 2006 GrGr (grgr@later.ru)Ɇɚɬɟɦɚɬɢɱɟɫɤɚɹ ɥɨɝɢɤɚ, ɫɜɨɞɤɚ ɨɩɪɟɞɟɥɟɧɢɣ. (ɫ) 2006 GrGr (grgr@later.ru)Ax3 : M &\ o MAx 4 : M &\ o \4.2. ɂɧɬɭɢɰɢɨɧɢɫɬɫɤɚɹ ɥɨɝɢɤɚ- ɫɜɨɣɫɬɜɚ ɤɨɧɴɸɧɤɰɢɢAx5 : M o \ o M &\ - ɫɜɨɣɫɬɜɚ ɞɢɡɴɸɧɤɰɢɢAx8 : M o F o \ o F o M \ o F Ax9 : M o M o \ Ax10 : M o \ o M o \ o M - ɡɚɤɨɧɵ ɩɪɨɬɢɜɨɪɟɱɢɹAx11: M M - ɡɚɤɨɧ ɢɫɤɥɸɱɟɧɧɨɝɨ ɬɪɟɬɶɟɝɨ^ t ` , ɝɞɟ ɯ ɫɜɨɛɨɞɧɚ ɞɥɹ t ɜ M .Ax13 : M ( x) ^ x ` o xM ( x)tAx12 : xM ( x) xɉɪɚɜɢɥɚ ɜɵɜɨɞɚ:M M o\1.- ɩɪɚɜɢɥɨ ɨɬɞɟɥɟɧɢɹ (modus ponens); ɫɥɟɞɫɬɜɢɟ ɢɦɩɥɢɤɚɰɢɢ ɨɬɞɟɥɹɟɬɫɹ ɨɬ\MI , S |I int , S | p & q ® int¯ I int , S |ª I int , S |I int , S | p q «¬ I int , S |pqpqI int , S | p S ' S : R ( S , S ') I int , S ' |z p- ɩɪɚɜɢɥɨ ɨɛɨɛɳɟɧɢɹ.- ɥɢɛɨ Mi ɩɨɥɭɱɚɟɬɫɹ ɢɡ ɩɪɟɞɲɟɫɬɜɭɸɳɢɯ ɮɨɪɦɭɥ ɩɨ ɩɪɚɜɢɥɭ ɨɬɞɟɥɟɧɢɹ ɢɥɢ ɨɛɨɛɳɟɧɢɹ.Ʌɨɝɢɱɟɫɤɢɣ ɜɵɜɨɞ – ɮɨɪɦɚɥɢɡɚɰɢɹ ɩɨɧɹɬɢɹ ɦɚɬɟɦɚɬɢɱɟɫɤɨɝɨ ɞɨɤɚɡɚɬɟɥɶɫɬɜɚ.ɉɨɫɥɟɞɧɹɹ ɮɨɪɦɭɥɚ M n ɢɡ ɩɨɫɥɟɞɨɜɚɬɟɥɶɧɨɫɬɢ ɥɨɝɢɱɟɫɤɨɝɨ ɜɵɜɨɞɚ ɧɚɡɵɜɚɟɬɫɹ ɜɵɜɨɞɢɦɨɣ ɢɡȽ ɢ ɨɛɨɡɧɚɱɚɟɬɫɹ ɤɚɤ * | M n .
ȿɫɥɢ Ƚ – ɩɭɫɬɨɟ ɦɧɨɠɟɫɬɜɨ, ɬɨ M n ɧɚɡɵɜɚɟɬɫɹ ɬɟɨɪɟɦɨɣɂɉɋɥɟɞɫɬɜɢɟ ɢɡ ɩɟɪɜɨɣ ɬɟɨɪɟɦɵ Ƚɺɞɟɥɹ: Ɇɚɬɟɦɚɬɢɤɚ – ɧɟɚɤɫɢɨɦɚɬɢɡɢɪɭɟɦɚɹ ɧɚɭɤɚ.Ɉɩɪɟɞɟɥɟɧɢɟ. Ɍɪɨɣɤɨɣ ɏɨɚɪɚ ɧɚɡɵɜɚɟɬɫɹ ɮɨɪɦɭɥɚ ɜɢɞɚ {M } 3 ! {\ } , ɝɞɟ M ,\ - ɮɨɪɦɭɥɵ, ɚɉ – ɩɪɨɝɪɚɦɦɚ, ɩɪɢɱɟɦ ɟɫɥɢ ɧɚ ɜɯɨɞɟ ɩɪɨɝɪɚɦɦɵ ɉ ɜɵɩɨɥɧɹɟɬɫɹ ɭɬɜɟɪɠɞɟɧɢɟ M , ɬɨ ɧɚ ɟɟɜɵɯɨɞɟ ɜɵɩɨɥɧɹɟɬɫɹ ɨɬɧɨɲɟɧɢɟ \ . Ɏɨɪɦɭɥɚ M ɧɚɡɵɜɚɟɬɫɹ ɩɪɟɞɭɫɥɨɜɢɟɦ, ɮɨɪɦɭɥɚ \ ɩɨɫɬɭɫɥɨɜɢɟɦ.Ɉɩɪɟɞɟɥɟɧɢɟ. ɉɪɨɝɪɚɦɦɚ ɉ ɧɚɡɵɜɚɟɬɫɹ ɱɚɫɬɢɱɧɨ ɤɨɪɪɟɤɬɧɨɣ ɨɬɧɨɫɢɬɟɥɶɧɨ ɩɪɟɞɭɫɥɨɜɢɹ Mɢ ɩɨɫɬɭɫɥɨɜɢɹ \ , ɟɫɥɢ ɨɛɳɟɡɧɚɱɢɦɚ ɮɨɪɦɭɥɚ {M } 3 ! {\ } . ɗɬɭ ɨɛɳɟɡɧɚɱɢɦɨɫɬɶ ɫɥɟɞɭɟɬɩɨɧɢɦɚɬɶ ɫɥɟɞɭɸɳɢɦ ɨɛɪɚɡɨɦ: ɞɥɹ ɥɸɛɨɣ ɞɨɩɭɫɬɢɦɨɣ ɢɧɬɟɪɩɪɟɬɚɰɢɢ I ɢ ɥɸɛɨɝɨ ɧɚɛɨɪɚɡɧɚɱɟɧɢɣ ɫɜɨɛɨɞɧɵɯ ɩɟɪɟɦɟɧɧɵɯ {D1 , D 2 ,..., D n } VarM Var\ ɢɡ ɜɵɩɨɥɧɢɦɨɫɬɢ ɮɨɪɦɭɥɵ Mɉ ::=||||Ɉɩɪɟɞɟɥɟɧɢɟ.
Ɏɨɪɦɭɥɚ M ɧɚɡɵɜɚɟɬɫɹ ɨɛɳɟɡɧɚɱɢɦɨɣ ɫ ɬɨɱɤɢ ɡɪɟɧɢɹ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɨɣɥɨɝɢɤɢ (ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɢ ɨɛɳɟɡɧɚɱɢɦɨɣ, ɨɛɨɡɧɚɱɚɟɬɫɹ ɤɚɤ | M ), ɟɫɥɢ ɮɨɪɦɭɥɚ M ɛɭɞɟɬintɜɵɩɨɥɧɢɦɚ ɜ ɥɸɛɨɦ ɫɨɫɬɨɹɧɢɢ S ɥɸɛɨɣ ɢɧɬɟɪɩɪɟɬɚɰɢɢ I int S , R, [ ! .ɍɬɜɟɪɠɞɟɧɢɟ. ȿɫɥɢ ɮɨɪɦɭɥɚ M ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɢ ɨɛɳɟɡɧɚɱɢɦɚ, ɬɨ ɨɧɚ ɨɛɳɟɡɧɚɱɢɦɚ ɢ ɫɬɨɱɤɢ ɡɪɟɧɢɹ ɤɥɚɫɫɢɱɟɫɤɨɣ ɥɨɝɢɤɢ ɩɪɟɞɢɤɚɬɨɜ.ɍɬɜɟɪɠɞɟɧɢɟ. Ɏɨɪɦɭɥɵ p p ɢ p o p ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɢ ɧɟɜɵɩɨɥɧɢɦɵ.ɢɫɱɢɫɥɟɧɢɹ ɩɪɟɞɢɤɚɬɨɜ.Ɍɟɨɪɟɦɚ (Ƚɺɞɟɥɹ; ɤɨɪɪɟɤɬɧɨɫɬɢ ɢ ɩɨɥɧɨɬɵ ɞɥɹ ɢɫɱɢɫɥɟɧɢɹ ɩɪɟɞɢɤɚɬɨɜ): Ɏɨɪɦɭɥɚɹɜɥɹɟɬɫɹ ɬɟɨɪɟɦɨɣ ɢɫɱɢɫɥɟɧɢɹ ɩɪɟɞɢɤɚɬɨɜ ɬɨɝɞɚ ɢ ɬɨɥɶɤɨ ɬɨɝɞɚ, ɤɨɝɞɚ ɨɧɚ ɨɛɳɟɡɧɚɱɢɦɚ.Ɉɩɪɟɞɟɥɟɧɢɟ. ɉɪɨɝɪɚɦɦɚ ɧɚɡɵɜɚɟɬɫɹ ɩɪɚɜɢɥɶɧɨɣ, ɟɫɥɢ ɧɚ ɟɟ ɜɵɯɨɞɟ ɜɫɟɝɞɚ ɩɨɹɜɥɹɟɬɫɹɪɟɡɭɥɶɬɚɬ, ɧɚɯɨɞɹɳɢɣɫɹ ɜ ɨɩɪɟɞɟɥɟɧɧɨɦ ɨɬɧɨɲɟɧɢɢ ɫ ɜɯɨɞɧɵɦɢ ɞɚɧɧɵɦɢ (ɬ.ɟ.| xin (M0 ( xin ) o xout ( R3 ( xin , xout ) & M1 ( xin , xout ))) ).Ɉɩɪɟɞɟɥɢɦ ɦɨɞɟɥɶɧɵɣ ɹɡɵɤ ɩɪɨɝɪɚɦɦɢɪɨɜɚɧɢɹ:ɂɡɦɟɧɹɟɬɫɹ ɢ ɩɨɧɹɬɢɟ ɥɨɝɢɱɟɫɤɨɝɨ ɡɚɤɨɧɚ.Ɉɩɪɟɞɟɥɟɧɢɟ.
Ʌɨɝɢɱɟɫɤɢɦ ɜɵɜɨɞɨɦ ɜ ɢɫɱɢɫɥɟɧɢɢ ɩɪɟɞɢɤɚɬɨɜ ɢɡ ɦɧɨɠɟɫɬɜɚ ɮɨɪɦɭɥ Ƚɧɚɡɵɜɚɟɬɫɹ ɤɨɧɟɱɧɚɹ ɩɨɫɥɟɞɨɜɚɬɟɥɶɧɨɫɬɶ ɮɨɪɦɭɥ M1 , M2 ,..., Mn , ɬɚɤɚɹ, ɱɬɨ ɞɥɹ ɥɸɛɨɝɨ i t 1- ɥɢɛɨ Mi * ;- ɥɢɛɨ Mi - ɨɞɧɚ ɢɡ 15 ɚɤɫɢɨɦ;ɉɭɫɬɶ ɉ – ɩɪɨɝɪɚɦɦɚ, R3 - ɨɬɧɨɲɟɧɢɟ ɦɟɠɞɭ ɟɟ ɜɯɨɞɧɵɦɢ ɢ ɜɵɯɨɞɧɵɦɢ ɞɚɧɧɵɦɢ (ɬ.ɟ. ɟɫɥɢɩɪɢ ɩɨɫɬɭɩɥɟɧɢɢ ɧɚ ɜɯɨɞ ɡɧɚɱɟɧɢɹ ɯ ɩɪɨɝɪɚɦɦɚ ɜɵɞɚɟɬ ɭ, ɬɨ ɜɵɪɚɠɟɧɢɟ R3 ( x, y ) ɹɜɥɹɟɬɫɹɢɫɬɢɧɧɵɦ).( I | M[d1 , d 2 ,..., d n ] ) ɛɭɞɟɬ ɫɥɟɞɨɜɚɬɶ, ɱɬɨ ɩɨɫɥɟ ɡɚɜɟɪɲɟɧɢɹ ɩɪɨɝɪɚɦɦɵ ɉ ɩɟɪɟɦɟɧɧɵɟɩɪɢɦɭɬ ɡɧɚɱɟɧɢɹ d '1 , d '2 ,..., d 'n , ɩɪɢɱɟɦ ɮɨɪɦɭɥɚ \ ɛɭɞɟɬ ɜɵɩɨɥɧɢɦɚ ɧɚ ɞɚɧɧɵɯ ɡɧɚɱɟɧɢɹɯɩɟɪɟɦɟɧɧɵɯ ( I | \ [d1 , d 2 ,..., d n ] ).I int , S | p o q S ' S : R( S , S ') & I int , S ' | p I int , S ' | qɩɨɫɵɥɤɢ.xMɈɩɪɟɞɟɥɟɧɢɟ.
ɂɧɬɭɢɰɢɨɧɢɫɬɫɤɚɹ ɢɧɬɟɪɩɪɟɬɚɰɢɹ – ɷɬɨ ɬɪɨɣɤɚ I int S , R, [ ! , ɝɞɟS – ɧɟɩɭɫɬɨɟ ɦɧɨɠɟɫɬɜɨ ɚɥɶɬɟɪɧɚɬɢɜɧɵɯ ɫɨɫɬɨɹɧɢɣ (ɫɨɫɬɨɹɧɢɣ ɡɧɚɧɢɣ);R S u S - ɨɬɧɨɲɟɧɢɟ ɧɟɫɬɪɨɝɨɝɨ ɱɚɫɬɢɱɧɨɝɨ ɩɨɪɹɞɤɚ, ɭɤɚɡɵɜɚɸɳɟɟ, ɱɬɨ ɧɟɤɨɬɨɪɨɟɫɨɫɬɨɹɧɢɟ ɡɧɚɧɢɣ ɦɨɠɟɬ ɛɵɬɶ ɞɨɫɬɢɝɧɭɬɨ ɢɡ ɞɪɭɝɨɝɨ ɢ ɨɛɥɚɞɚɸɳɟɟ ɫɜɨɣɫɬɜɚɦɢɬɪɚɧɡɢɬɢɜɧɨɫɬɢ, ɚɧɬɢɫɢɦɦɟɬɪɢɱɧɨɫɬɢ ɢ ɪɟɮɥɟɤɫɢɜɧɨɫɬɢ;[ : S u P o ^T , F ` - ɨɰɟɧɤɚ ɢɫɬɢɧɧɨɫɬɢ (ɫɩɨɫɨɛɧɨɫɬɶ ɪɟɲɚɬɶ ɡɚɞɚɱɢ ɜ ɨɩɪɟɞɟɥɟɧɧɨɦɫɨɫɬɨɹɧɢɢ).Ɉɬɧɨɲɟɧɢɟ ɜɵɩɨɥɧɢɦɨɫɬɢ ɞɥɹ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɨɣ ɥɨɝɢɤɢ ɛɭɞɟɬ ɜɵɝɥɹɞɟɬɶ ɫɥɟɞɭɸɳɢɦɨɛɪɚɡɨɦ:I int , S | p [ ( S , p ) TAx14 : x M o \ o M o x\ ; x VarMAx15 : x \ o M o x\ o M 2.4.3.
Ʌɨɝɢɤɚ ɏɨɚɪɚɂɧɬɭɢɰɢɨɧɢɫɬɫɤɚɹ ɥɨɝɢɤɚ (ɥɨɝɢɤɚ Ȼɪɚɭɷɪɚ) – ɷɬɨ ɤɥɚɫɫɢɱɟɫɤɚɹ ɥɨɝɢɤɚ, ɢɡ ɚɤɫɢɨɦ ɤɨɬɨɪɨɣɢɫɤɥɸɱɟɧ ɡɚɤɨɧ «ɢɫɤɥɸɱɟɧɧɨɝɨ ɬɪɟɬɶɟɝɨ».Ax6 : M o M \Ax7 :\ o M \Ɇɚɬɟɦɚɬɢɱɟɫɤɚɹ ɥɨɝɢɤɚ, ɫɜɨɞɤɚ ɨɩɪɟɞɟɥɟɧɢɣ. (ɫ) 2006 GrGr (grgr@later.ru)Ɂɚɦɟɱɚɧɢɟ. ɇɟ ɫɭɳɟɫɬɜɭɟɬ ɧɢ ɨɞɧɨɝɨ ɫɨɞɟɪɠɚɬɟɥɶɧɨɝɨ ɦɚɬɟɦɚɬɢɱɟɫɤɨɝɨ ɭɬɜɟɪɠɞɟɧɢɹ, ɞɥɹɤɨɬɨɪɨɝɨ ɧɟɥɶɡɹ ɛɵɥɨ ɛɵ ɩɨɫɬɪɨɢɬɶ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɨɝɨ ɞɨɤɚɡɚɬɟɥɶɫɬɜɚ, ɨɞɧɚɤɨ ɜɫɟɞɨɤɚɡɚɬɟɥɶɫɬɜɚ ɞɨɥɠɧɵ ɩɨɤɚɡɵɜɚɬɶ ɩɪɚɜɢɥɶɧɨɫɬɶ ɭɬɜɟɪɠɞɟɧɢɹ ɹɜɧɨ (ɤɨɧɫɬɪɭɤɬɢɜɧɨ),ɩɨɷɬɨɦɭ ɜɫɟ ɞɨɤɚɡɚɬɟɥɶɫɬɜɚ ɩɨɥɭɱɚɸɬɫɹ ɛɨɥɟɟ ɫɥɨɠɧɵɦɢ, ɚ ɪɟɡɭɥɶɬɚɬɨɦ ɥɸɛɨɝɨ ɬɚɤɨɝɨɞɨɤɚɡɚɬɟɥɶɫɬɜɚ ɛɭɞɟɬ ɩɨɫɬɪɨɟɧɢɟ ɚɥɝɨɪɢɬɦɚ.ɍɬɜɟɪɠɞɟɧɢɟ (ɞɢɡɴɸɧɤɬɢɜɧɨɟ ɫɜɨɣɫɬɜɨ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɨɣ ɥɨɝɢɤɢ).
ɂɧɬɭɢɰɢɨɧɢɫɬɫɤɚɹɨɛɳɟɡɧɚɱɢɦɨɫɬɶ ɮɨɪɦɭɥɵ M \ ɷɤɜɢɜɚɥɟɧɬɧɚ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɨɣ ɨɛɳɟɡɧɚɱɢɦɨɫɬɢ ɥɢɛɨ M ,ɥɢɛɨ \ .(x = t)ɉ1, ɉ2if A then ɉ1 else ɉ2 fiwhile A do ɉ1 odeps,Ƚɞɟ ɯ – ɩɟɪɟɦɟɧɧɚɹ, t – ɬɟɪɦ ɉi – ɩɪɨɝɪɚɦɦɵ, Ⱥ – ɚɬɨɦ, eps – ɩɭɫɬɨɬɚ.F1 , F2 ,..., Fn, ɩɪɢɱɟɦF0ɜɵɪɚɠɟɧɢɹ ɜ ɜɟɪɯɧɟɣ ɱɚɫɬɢ ɩɪɚɜɢɥɚ ɧɚɡɵɜɚɸɬɫɹ ɩɪɟɞɩɨɫɵɥɤɚɦɢ, ɜɵɪɚɠɟɧɢɟ ɜ ɧɢɠɧɟɣ ɱɚɫɬɢɩɪɚɜɢɥɚ ɧɚɡɵɜɚɟɬɫɹ ɡɚɤɥɸɱɟɧɢɟɦ. ɋɟɦɚɧɬɢɤɚ ɩɪɚɜɢɥɚ ɜɵɜɨɞɚ ɬɚɤɨɜɚ: ɟɫɥɢ ɢɫɬɢɧɧɵɦɩɪɟɞɩɨɫɵɥɤɢ, ɬɨ ɢɫɬɢɧɧɨ ɢ ɡɚɤɥɸɱɟɧɢɹ.Ɉɩɪɟɞɟɥɟɧɢɟ.
ɉɪɚɜɢɥɨɦ ɜɵɜɨɞɚ ɧɚɡɵɜɚɟɬɫɹ ɮɢɝɭɪɚ ɫɥɟɞɭɸɳɟɝɨ ɜɢɞɚ:Ɋɚɫɫɦɨɬɪɢɦ ɫɥɟɞɭɸɳɭɸ ɫɢɫɬɟɦɭ ɩɪɚɜɢɥ:M o M '1 ,{M '1} 3 ! {M '2 }, M 2 o M '2(ɨɫɥɚɛɥɟɧɢɹ)1. 1{M } 3 ! {M }12^ `M o\ x t(ɩɪɢɫɜɚɢɜɚɧɢɹ){M} x:= t ! {\ }{M} 31 ! {F },{F } 3 2 ! {\ }3.(ɩɨɫɥɟɞɨɜɚɬɟɥɶɧɨɝɨ ɫɨɟɞɢɧɟɧɢɹ){M} 3 ; 3 ! {\ }2.1ɍɬɜɟɪɠɞɟɧɢɟ. Ɏɨɪɦɭɥɚ xM ( x) ɨɛɳɟɡɧɚɱɢɦɚ ɬɨɝɞɚ ɢ ɬɨɥɶɤɨ ɬɨɝɞɚ, ɤɨɝɞɚ ɫɭɳɟɫɬɜɭɟɬ ɬɚɤɨɣɬɟɪɦ t, ɱɬɨ ɮɨɪɦɭɥɚ M (t ) ɛɭɞɟɬ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɢ ɨɛɳɟɡɧɚɱɢɦɨɣ.21Ɇɚɬɟɦɚɬɢɱɟɫɤɚɹ ɥɨɝɢɤɚ, ɫɜɨɞɤɚ ɨɩɪɟɞɟɥɟɧɢɣ. (ɫ) 2006 GrGr (grgr@later.ru){F inv & A} 3 !, F inv & A o \ , M o F inv(ɢɬɟɪɚɰɢɢ; F inv ɧɚɡɵɜɚɟɬɫɹ ɢɧɜɚɪɢɚɧɬɨɦ{M} while_A_do_3 ! {\ }ɨɩɟɪɚɬɨɪɚ ɢɬɟɪɚɰɢɢ, ɞɥɹ ɩɪɨɜɟɪɤɢ ɩɪɚɜɢɥɶɧɨɫɬɢ ɪɚɛɨɬɵ ɰɢɤɥɚ ɬɪɟɛɭɟɬɫɹ ɟɝɨ ɧɚɣɬɢ)6.
{M} eps ! {M } (ɚɤɫɢɨɦɚ)5.ɋɢɫɬɟɦɚ ɬɚɤɢɯ ɩɪɚɜɢɥ ɧɚɡɵɜɚɟɬɫɹ PVS (Prototype Verification System) ɢ ɩɨɡɜɨɥɹɟɬ ɭɩɪɨɳɚɬɶɩɪɨɜɟɪɤɭ ɩɪɚɜɢɥɶɧɨɫɬɢ ɩɪɨɝɪɚɦɦ.4.4. Ʌɨɝɢɤɢ ɡɧɚɧɢɣɊɚɫɫɦɨɬɪɢɦ ɦɭɥɶɬɢɚɝɟɧɬɧɭɸ ɫɢɫɬɟɦɭ (ɫɥɨɠɧɭɸ ɫɢɫɬɟɦɭ, ɩɪɢɧɢɦɚɸɳɭɸ ɪɟɲɟɧɢɹ)A1 , A2 ,..., An ɩɪɨɝɪɚɦɦ-ɚɝɟɧɬɨɜ. ɉɪɢ ɷɬɨɦ ɩɪɢɧɹɬɢɟ ɪɟɲɟɧɢɹ ɦɨɠɟɬ ɨɩɢɪɚɬɶɫɹ ɧɚ ɬɨ, ɱɬɨɡɧɚɸɬ ɢɥɢ ɧɟ ɡɧɚɸɬ ɞɪɭɝɢɟ ɭɱɚɫɬɧɢɤɢ ɩɪɨɰɟɫɫɚ ɩɪɢɧɹɬɢɹ ɪɟɲɟɧɢɣ.Ɉɩɪɟɞɟɥɟɧɢɟ. Ɇɨɞɚɥɶɧɵɦ ɨɩɟɪɚɬɨɪɨɦ ɧɚɡɵɜɚɟɬɫɹ ɨɩɟɪɚɬɨɪ , ɤɨɬɨɪɵɣ ɜɵɪɚɠɚɟɬɨɬɧɨɲɟɧɢɟ ɭɜɟɪɟɧɧɨɫɬɢ (ɧɟɨɛɯɨɞɢɦɨɫɬɢ). ȿɝɨ ɫɟɦɚɧɬɢɤɚ ɬɚɤɨɜɚ:ɹM ɨɡɧɚɱɚɟɬ «ɹ ɡɧɚɸ, ɱɬɨ ɮɨɪɦɭɥɚ M ɢɫɬɢɧɧɚ».ȼɨɩɪɨɫ ɨɛɳɟɡɧɚɱɢɦɨɫɬɢ ɮɨɪɦɭɥɵM o M - ɜɨɩɪɨɫ ɧɟɩɪɨɬɢɜɨɪɟɱɢɜɨɫɬɢ ɛɚɡɵ ɡɧɚɧɢɣ.ɹȼɨɩɪɨɫ ɨɛɳɟɡɧɚɱɢɦɨɫɬɢ ɮɨɪɦɭɥɵ M oM - ɜɨɩɪɨɫ ɩɨɥɧɨɬɵ ɛɚɡɵ ɡɧɚɧɢɣ.ɹ4.5. Ⱦɢɧɚɦɢɱɟɫɤɚɹ ɥɨɝɢɤɚ (ɥɨɝɢɤɚ ɩɪɨɝɪɚɦɦ)ɋɢɧɬɚɤɫɢɫ ɞɢɧɚɦɢɱɟɫɤɨɣ ɥɨɝɢɤɢ ɫɨɫɬɨɢɬ ɢɡ ɞɜɭɯ ɱɚɫɬɟɣ:ɉɪɨɝɪɚɦɦɵɎɨɪɦɭɥɵA {a1 , a2 ,..., an } - ɧɚɛɨɪ ɛɚɡɨɜɵɯ ɞɟɣɫɬɜɢɣP {M1 , M2 ,..., Mn } - ɧɚɛɨɪ ɛɚɡɨɜɵɯ ɭɫɥɨɜɢɣ(ɨɩɟɪɚɬɨɪɨɜ)(ɩɪɨɩɨɡɢɰɢɨɧɧɵɯ ɩɟɪɟɦɟɧɧɵɯ)1) a A - ɩɪɨɝɪɚɦɦɚ;1) M P - ɮɨɪɦɭɥɚ;2) 31 , 3 2 - ɩɪɨɝɪɚɦɦɚ;2) M1 & M2 , M1 M2 , M1 o M2 , M - ɮɨɪɦɭɥɵ;3) 31 || 3 2 - ɩɪɨɝɪɚɦɦɚ (|| 3) ɟɫɥɢ ɉ – ɩɪɨɝɪɚɦɦɚ, ɬɨ [3 ]M - ɮɨɪɦɭɥɚ.ɧɟɞɟɬɟɪɦɢɪɨɜɚɧɧɵɣ ɜɵɛɨɪ);4) (3 i ) * - ɩɪɨɝɪɚɦɦɚ;5) M ? - ɩɪɨɝɪɚɦɦɚ (ɬɟɫɬ; M - ɮɨɪɦɭɥɚ).ɉɪɢɦɟɪ: ɜɵɪɚɠɟɧɢɟ {M } <if A then ɉ1 else ɉ2 fi > {\ } , ɡɚɩɢɫɚɧɧɨɟ ɜ ɬɟɪɦɢɧɚɯ ɥɨɝɢɤɢɏɨɚɪɚ, ɜ ɬɟɪɦɢɧɚɯ ɞɢɧɚɦɢɱɟɫɤɨɣ ɥɨɝɢɤɢ ɛɭɞɟɬ ɜɵɝɥɹɞɟɬɶ ɤɚɤ M o [( A ?, 31 ) (A ?, 3 2 )]\ .24224.2{M & A} 31 ! {\ },{M & A} 3 2 ! {\ }(ɜɟɬɜɥɟɧɢɹ){M & A} if_A_then_31_else_3 2 _fi ! {\ }23.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
