Лекция 2. Общие принципы дедуктивной верификации программ. Логика Хоара (1185524), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

I 6|= 4 > 6.hπ0 , {x/4, y /6}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x ; π0 , {x/4, y /6}i↓Ihy ⇐ y − x; π0 , {x/4, y /6}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè: ASS, θ1 = {y /y − x}θ0 = {x/4, y /6 − 4} .hπ0 , {x/4, y /6}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x ; π0 , {x/4, y /6}i↓Ihy ⇐ y − x; π0 , {x/4, y /6}i↓Ihπ0 , {x/4, y /6 − 4}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè:hπ0 , {x/4, y /6−4}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè: WHILE1 , ò.

ê. I |= ¬(4 = 6 − 4).hπ0 , {x/4, y /6−4}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x ; π0 , {x/4, y /6−4}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè: IF1 , ò. ê. I |= 4 > 6 − 4.hπ0 , {x/4, y /6−4}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x ; π0 , {x/4, y /6−4}i↓Ihx ⇐ x − y ; π0 , {x/4, y /6−4}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè: ASS, θ2 = {x/x −y }θ1 = {x/4−(6−4), y /6−4} .hπ0 , {x/4, y /6−4}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x ; π0 , {x/4, y /6−4}i↓Ihx ⇐ x − y ; π0 , {x/4, y /6−4}i↓Ihπ0 , {x/4−(6−4), y /6−4}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè: WHILE0 , ò.

ê. I 6|= ¬(4−(6−4) = 6−4).hπ0 , {x/4, y /6−4}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x ; π0 , {x/4, y /6−4}i↓Ihx ⇐ x − y ; π0 , {x/4, y /6−4}i↓Ihπ0 , {x/4−(6−4), y /6−4}i↓Ih∅, {x/4−(6−4), y /6−4}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè: Êîíåö âû÷èñëåíèÿ.hπ0 , {x/4, y /6−4}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x ; π0 , {x/4, y /6−4}i↓Ihx ⇐ x − y ; π0 , {x/4, y /6−4}i↓Ihπ0 , {x/4−(6−4), y /6−4}i↓Ih∅, {x/4−(6−4), y /6−4}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÊàê ñëåäóåò èç îïðåäåëåíèÿ, ëþáîå âû÷èñëåíèå ëèáî ÿâëÿåòñÿáåñêîíå÷íîé ïîñëåäîâàòåëüíîñòüþ, ëèáî çàâåðøàåòñÿñîñòîÿíèåì h∅, ηi .

 ïîñëåäíåì ñëó÷àå îöåíêà η íàçûâàåòñÿðåçóëüòàòîì âû÷èñëåíèÿ.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÊàê ñëåäóåò èç îïðåäåëåíèÿ, ëþáîå âû÷èñëåíèå ëèáî ÿâëÿåòñÿáåñêîíå÷íîé ïîñëåäîâàòåëüíîñòüþ, ëèáî çàâåðøàåòñÿñîñòîÿíèåì h∅, ηi .  ïîñëåäíåì ñëó÷àå îöåíêà η íàçûâàåòñÿðåçóëüòàòîì âû÷èñëåíèÿ.Áóäåì èñïîëüçîâàòü çàïèñü −→∗I äëÿ îáîçíà÷åíèÿðåôëåêñèâíîãî è òðàíçèòèâíîãî çàìûêàíèÿ îòíîøåíèÿïåðåõîäîâ −→I .Òîãäà îöåíêà ïåðåìåííûõ η ÿâëÿåòñÿ ðåçóëüòàòîì âû÷èñëåíèÿïðîãðàììû π íà îöåíêå ïåðåìåííûõ θ â èíòåðïðåòàöèè I â òîìè òîëüêî òîì ñëó÷àå, êîãäà âûïîëíÿåòñÿ îòíîøåíèåhπ, θi −→∗I h∅, ηi.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÏÐÎÃÐÀÌÌÍåôîðìàëüíàÿ ïîñòàíîâêà.Ïðîãðàììà π ñ÷èòàåòñÿ (÷àñòè÷íî ) êîððåêòíîé , åñëè äëÿëþáûõ íà÷àëüíûõ äàííûõ, óäîâëåòâîðÿþùèõ îïðåäåëåííîìóóñëîâèþ ϕ , ðåçóëüòàò âû÷èñëåíèÿ (åñëè âû÷èñëåíèåçàâåðøàåòñÿ) óäîâëåòâîðÿåò îïðåäåëåííîìó óñëîâèþ ψ .×àñòè÷íî êîððåêòíàÿ ïðîãðàììà, âñå âû÷èñëåíèÿ êîòîðîéçàâåðøàþòñÿ, íàçûâàåòñÿ òîòàëüíî êîððåêòíîé .Îãðàíè÷åíèå ϕ , êîòîðîå íàëàãàåòñÿ íà íà÷àëüíûå äàííûå,íàçûâàåòñÿ ïðåäóñëîâèåì , à òðåáîâàíèå ψ , êîòîðîìó äîëæíûóäîâëåòâîðÿòü ðåçóëüòàòû âû÷èñëåíèÿ, íàçûâàåòñÿïîñòóñëîâèåì ïðîãðàììû.Çàäà÷à âåðèôèêàöèè ïðîãðàììû π çàêëþ÷àåòñÿ â ïðîâåðêå÷àñòè÷íîé êîððåêòíîñòè ïðîãðàììû π îòíîñèòåëüíî çàäàííîãîïðåäóñëîâèÿ ϕ è çàäàííîãî ïîñòóñëîâèÿ ψ .ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÏÐÎÃÐÀÌÌÔîðìàëüíàÿ ïîñòàíîâêà.Ðàñøèðèì ìíîæåñòâî ôîðìóë ëîãèêè ïðåäèêàòîâ, ââåäÿ âðàññìîòðåíèå â êà÷åñòâå ôîðìóë âûðàæåíèÿ íîâîãîñïåöèàëüíîãî âèäà.ÎïðåäåëåíèåÒðèïëåòîì Õîàðà (òðîéêîé Õîàðà) íàçûâàåòñÿ âñÿêîåâûðàæåíèå âèäàϕ{π}ψ,ãäå ϕ, ψ ôîðìóëû ëîãèêè ïðåäèêàòîâ,à π èìïåðàòèâíàÿ ïðîãðàììà.Îáîçíà÷èì HTσ ìíîæåñòâî òðèïëåòîâ Õîàðà ñèãíàòóðû σ .ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÏÐÎÃÐÀÌÌÂûïîëíèìîñòü òðèïëåòîâ Õîàðà â èíòåðïðåòàöèÿõîïðåäåëÿåòñÿ òàê:I |= ϕ{π}ψ⇐⇒äëÿ ëþáûõ îöåíîê ïåðåìåííûõ θ, η,åñëè I |= ϕθ è hπ, θi −→ ∗I h∅, ηi,òî I |= ψη.Îïðåäåëåíèå (÷àñòè÷íîé êîððåêòíîñòè ïðîãðàììû)Ïóñòü ϕ, ψ ôîðìóëû ëîãèêè ïðåäèêàòîâ, à π èìïåðàòèâíàÿïðîãðàììà.Ïðîãðàììà π íàçûâàåòñÿ ÷àñòè÷íî êîððåêòíîé âèíòåðïðåòàöèè I îòíîñèòåëüíî ïðåäóñëîâèÿ ϕ è ïîñòóñëîâèÿ ψ ,åñëè òðèïëåò ϕ{π}ψ âûïîëíèì â èíòåðïðåòàöèè I , ò.

å.I |= ϕ{π}ψ .ËÎÃÈÊÀ ÕÎÀÐÀÎïèðàÿñü íà ïðàâèëà òàáëè÷íîãî âûâîäà äëÿ ëîãèêèïðåäèêàòîâ, ïîñòðîèì ñèñòåìó ïðàâèë âûâîäà, àíàëîãè÷íûõïðàâèëàì âûâîäà äëÿ ñåìàíòè÷åñêèõ òàáëèö.Âïåðâûå òàêóþ ñèñòåìó ëîãè÷åñêîãî âûâîäà ïðåäëîæèë â 1968ã. ×.Ý. Õîàð. Ïðàâèëà âûâîäà Õîàðà èìåþò âèäΦ,ΨΦ,ϕΦ,Ψ1 , Ψ2ãäå Φ, Ψ, Ψ1 , Ψ2 òðèïëåòû Õîàðà,ϕ, ψ ôîðìóëû ëîãèêè ïðåäèêàòîâ.Φ,ϕ, Ψ, ψËÎÃÈÊÀ ÕÎÀÐÀÏðàâèëà âûâîäà ÕîàðàASS:ϕ{x/t} {x ⇐ t} ϕ,trueËÎÃÈÊÀ ÕÎÀÐÀÏðàâèëà âûâîäà ÕîàðàASS:CONS:ϕ{x/t} {x ⇐ t} ϕ,trueϕ{π}ψ,ϕ → ϕ0 , ϕ0 {π}ψ 0 , ψ 0 → ψËÎÃÈÊÀ ÕÎÀÐÀÏðàâèëà âûâîäà ÕîàðàASS:ϕ{x/t} {x ⇐ t} ϕ,trueCONS:ϕ{π}ψ,ϕ → ϕ0 , ϕ0 {π}ψ 0 , ψ 0 → ψCOMP:ϕ{π1 ; π2 }ψ,ϕ{π1 }χ, χ{π2 }ψËÎÃÈÊÀ ÕÎÀÐÀÏðàâèëà âûâîäà ÕîàðàASS:ϕ{x/t} {x ⇐ t} ϕ,trueCONS:ϕ{π}ψ,ϕ → ϕ0 , ϕ0 {π}ψ 0 , ψ 0 → ψCOMP:ϕ{π1 ; π2 }ψ,ϕ{π1 }χ, χ{π2 }ψIF:ϕ {if C then π1 else π2 fi} ψ,(ϕ&C ) {π1 } ψ, (ϕ&¬C ) {π2 } ψËÎÃÈÊÀ ÕÎÀÐÀÏðàâèëà âûâîäà ÕîàðàASS:ϕ{x/t} {x ⇐ t} ϕ,trueCONS:ϕ{π}ψ,ϕ → ϕ0 , ϕ0 {π}ψ 0 , ψ 0 → ψCOMP:ϕ{π1 ; π2 }ψ,ϕ{π1 }χ, χ{π2 }ψIF:ϕ {if C then π1 else π2 fi} ψ,(ϕ&C ) {π1 } ψ, (ϕ&¬C ) {π2 } ψWHILE:ϕ {while C do π od} (ϕ&¬C ).(ϕ&C ) {π} ϕËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå ÕîàðàÂûâîä â ëîãèêå Õîàðà òðèïëåòà Φ0 = ϕ0 {π0 } ψ0 ýòîËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå ÕîàðàÂûâîä â ëîãèêå Õîàðà òðèïëåòà Φ0 = ϕ0 {π0 } ψ0 ýòîêîðíåâîå äåðåâî,y@yy?y@@R y@@@y? @@R yy?yËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå ÕîàðàÂûâîä â ëîãèêå Õîàðà òðèïëåòà Φ0 = ϕ0 {π0 } ψ0 ýòîêîðíåâîå äåðåâî, âåðøèíàìè êîòîðîãî ñëóæàò òðèïëåòû èôîðìóëû ëîãèêè ïðåäèêàòîâ è ïðè ýòîìΦyjyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12?ϕy3?ϕy4ΦyiËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå ÕîàðàÂûâîä â ëîãèêå Õîàðà òðèïëåòà Φ0 = ϕ0 {π0 } ψ0 ýòîêîðíåâîå äåðåâî, âåðøèíàìè êîòîðîãî ñëóæàò òðèïëåòû èôîðìóëû ëîãèêè ïðåäèêàòîâ è ïðè ýòîì1) êîðíåì äåðåâà ÿâëÿåòñÿ òðèïëåò Φ0 ;ΦyjyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12?ϕy3?ϕy4ΦyiËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå Õîàðà2)èç âåðøèíû Φi èñõîäÿò äóãè â âåðøèíó Φj⇐⇒Φi ïðàâèëî òàáëè÷íîãî âûâîäà;ΦjΦyjyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12?yϕ3?yϕ 4ΦyiËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå Õîàðà2)èç âåðøèíû Φi èñõîäÿò äóãè â âåðøèíó Φj⇐⇒Φi ïðàâèëî òàáëè÷íîãî âûâîäà;ΦjΦyjyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12?yϕ3?yϕ 4ΦyiËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå Õîàðà2)èç âåðøèíû Φ1 èñõîäÿò äóãè â âåðøèíû ϕ1 , Φ3 , ϕ2⇐⇒Φ1 ïðàâèëî òàáëè÷íîãî âûâîäà;ϕ1 , Φ3 , ϕ2ΦyiΦyj?yϕ3yΦ0@@@R y@Φ1@@ϕy1? @RyΦ3 @yϕ2?ϕy4ËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå Õîàðà3) ëèñòüÿìè äåðåâà ÿâëÿþòñÿ ôîðìóëû ëîãèêè ïðåäèêàòîâ.ΦyjyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12?yϕ3?yϕ 4ΦyiËÎÃÈÊÀ ÕÎÀÐÀÎïðåäåëåíèå âûâîäà â ëîãèêå ÕîàðàÂûâîä òðèïëåòà Φ0 = ϕ0 {π0 } ψ0 â ëîãèêå Õîàðà íàçûâàåòñÿóñïåøíûì â èíòåðïðåòàöèè I , åñëè äåðåâî âûâîäà ÿâëÿåòñÿêîíå÷íûì, è âñå åãî ëèñòîâûå âåðøèíû ýòî èñòèííûå âèíòåðïðåòàöèè I ôîðìóëû ëîãèêè ïðåäèêàòîâ.ËÎÃÈÊÀ ÕÎÀÐÀÏðèìåðÏîêàæåì, ÷òî ïðîãðàììàπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odïðàâèëüíî âû÷èñëÿåò íàèáîëüøèé îáùèé äåëèòåëü äâóõïîëîæèòåëüíûõ öåëûõ ÷èñåë.ËÎÃÈÊÀ ÕÎÀÐÀÏðèìåðÏîêàæåì, ÷òî ïðîãðàììàπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odïðàâèëüíî âû÷èñëÿåò íàèáîëüøèé îáùèé äåëèòåëü äâóõïîëîæèòåëüíûõ öåëûõ ÷èñåë.Äëÿ ýòîãî íåîáõîäèìî ñôîðìóëèðîâàòü ïðåäóñëîâèå ϕ0 èïîñòóñëîâèå ψ0 , ñîîòâåòñòâóþùåå ýòîìó òðåáîâàíèþ, èïîñòðîèòü óñïåøíûé âûâîä òðèïëåòà ϕ0 {π0 } ψ0 â ëîãèêåÕîàðà.ËÎÃÈÊÀ ÕÎÀÐÀÏðèìåðÄëÿ óäîáñòâà îáîçíà÷åíèé ââåäåì íåêîòîðûå âñïîìîãàòåëüíûåôîðìóëûDIV (x, z) :∃u (u × z = x),GCD(x, y , z) : DIV (x, z) & DIV (y , z) &∀u (DIV (x, u)&DIV (y , u) → (u ≤ z)).Òîãäàϕ0 (x, y , z) : (x > 0) & (y > 0) & GCD(x, y , z),ψ0 (x, z) :z = x.π0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yϕ0 (x,y ,z)π0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yϕ0 (x,y ,z)CONSπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yϕ0 (x,y ,z))yPPPPCONSPPPq yPϕ0 (x, y , z) → ϕ0 (x, y , z)?yπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yϕ0 (x,y ,z))yPPPPCONSPPPq yPϕ0 (x, y , z) → ϕ0 (x, y , z)ϕ0 (x, y , z)&¬¬(x = y ) → (z = x)?yπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yϕ0 (x,y ,z))yPPPPCONSPPPq yPϕ0 (x, y , z) → ϕ0 (x, y , z)ϕ0 (x, y , z)&¬¬(x = y ) → (z = x)?yϕ0 (x, y , z) {π0 } ϕ0 (x, y , z)&¬¬(x = y )π0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yϕ0 (x,y ,z))yPPPPPPϕ0 (x, y , z) → ϕ0 (x, y , z)Pq yPϕ0 (x, y , z)&¬¬(x = y ) → (z = x)?yϕ0 (x, y , z) {π0 } ϕ0 (x, y , z)&¬¬(x = y )WHILE?yϕ0 (x, y , z)&¬(x = y ){if x > y then x ⇐ x −y else y ⇐ y −x }ϕ0 (x, y , z)π0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yϕ0 (x,y ,z))yPPPPPPϕ0 (x, y , z) → ϕ0 (x, y , z)Pq yPϕ0 (x, y , z)&¬¬(x = y ) → (z = x)?yϕ0 (x, y , z) {π0 } ϕ0 (x, y , z)&¬¬(x = y )?yϕ0 (x, y , z)&¬(x = y ){if x > y thenPx ⇐ x −y else y ⇐ y −x }ϕ0 (x, y , z)y PPPPPIFPqPyϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z)π0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yϕ0 (x,y ,z))yPPPPPPϕ0 (x, y , z) → ϕ0 (x, y , z)Pq yPϕ0 (x, y , z)&¬¬(x = y ) → (z = x)?yϕ0 (x, y , z) {π0 } ϕ0 (x, y , z)&¬¬(x = y )?yϕ0 (x, y , z)&¬(x = y ){if x > y thenPx ⇐ x −y else y ⇐ y −x }ϕ0 (x, y , z)y PPPPPIFPqPyϕ0 (x, y , z)&¬(x = y )&¬(x > y ){y ⇐ y −x}ϕ0 (x, y , z)ϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z)Ëåâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z)yËåâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z))yPPy?yPPCONSPPPq yPËåâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z))yϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z)PPy?yPPCONSPPPq yPËåâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z))yϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z)PPyPPCONSPPPq yPϕ0 (x, y , z) → ϕ0 (x, y , z)?yËåâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z))yϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z)PPyPPCONSPPPq yPϕ0 (x, y , z) → ϕ0 (x, y , z)?yϕ0 (x − y , y , z){x ⇐ x −y }ϕ0 (x, y , z)Ëåâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z))yϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z)PPyPPPPPqPyϕ0 (x, y , z) → ϕ0 (x, y , z)?yϕ0 (x − y , y , z){x ⇐ x −y }ϕ0 (x, y , z)ASS?ytrueÏðàâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&¬(x > y ){x ⇐ y −x}ϕ0 (x, y , z)yÏðàâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&¬(x > y ){x ⇐ y −x}ϕ0 (x, y , z))yyPP?yPPCONSPPPq yPÏðàâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&¬(x > y ){x ⇐ y −x}ϕ0 (x, y , z))yϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z)yPP?yPPCONSPPPq yPÏðàâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&¬(x > y ){x ⇐ y −x}ϕ0 (x, y , z))yϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z)yPPPPCONSPPPq yPϕ0 (x, y , z) → ϕ0 (x, y , z)?yÏðàâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&¬(x > y ){x ⇐ y −x}ϕ0 (x, y , z))yϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z)yPPPPCONSPPPq yPϕ0 (x, y , z) → ϕ0 (x, y , z)?yϕ0 (x, y − x, z){y ⇐ y −x}ϕ0 (x, y , z)Ïðàâàÿ âåòâüϕ0 (x, y , z)&¬(x = y )&¬(x > y ){x ⇐ y −x}ϕ0 (x, y , z))yϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z)yPPPPPPPqPyϕ0 (x, y , z) → ϕ0 (x, y , z)?yϕ0 (x, y − x, z){y ⇐ y −x}ϕ0 (x, y , z)ASS?ytrueËÎÃÈÊÀ ÕÎÀÐÀÏðèìåðÏîêàæåì, ÷òî ïîñòðîåííûé âûâîä â ëîãèêå Õîàðà ÿâëÿåòñÿóñïåøíûì äëÿ ñòàíäàðòíîé àðèôìåòè÷åñêîé èíòåðïðåòàöèèI0 = hDI0 = {0, 1, 2, .

Характеристики

Список файлов лекций