mod Ex10 logic: 'cl' rem \para \bf 10. CVIČENIE Z PREDMETU LOGIKA PRE INFORMATIKOV 2 \end \para* http://ii.fmph.uniba.sk/cl/courses/lpi2/ex/ex10.cl rem \para* \it Dátum: \end štvrtok 9. 12. 2004 \para* \it Odporúčaná verzia CL: \end 5.81.16 \para* \it WWW stránka predmetu: \end http://ii.fmph.uniba.sk/cl/courses/lpi2?lang=sk \para* \it Kontakt na cvičiaceho: \end mailto:kluka@fmph.uniba.sk rem \para Preskočte nasledujúce komponenty až po nadpis "Cvičenia". appldisp/0 Tau Id(0,Ent('tau'),0) appldisp/0 Sigma Id(0,Ent('sigma'),0) appldisp/2 Ind Subsup(Arg(0),40,Arg(1),None) appldisp/1 Sgn_d Std('sgn',0) appldisp/2 Max_d Prefix(90,2,Id(0,'max',0), Fenced(Op('(',0),Infix(Arg(0),30,2,Op(',',0),Arg(1)),Op(')',0))) appldisp/0 Cdots Op(Ent('ctdot'),0) pred/0 Fill_in 'Cdots' Fill_in <-> \f rem \para \bf C V I Č E N I A \end rem \para \bf Explicitné klauzálne definície \end rem \para Vašou úlohou v tomto cvičení je pre každú z daných explicitných (t. j. nerekurzívnych) klauzálnych definícií skonštruovať klauzálnu formulu, dokázať pre ňu existenčnú podmienku, zaviesť funkciu minimalizáciou tejto formuly a dokázať klauzuly definície. rem \para \it \bf Diskriminácia na nulu. \end \end \para \ft Tau = 0 \end | \ft Tau != 0 \end \para* Pripomeňme, že pre diskrimináciou je taká \ft n \end-tica formúl, že pre ľubovoľné termy dosadené za \ft Tau \end platí \it práve jedna \end formúl z \ft n \end-tice (v tomto prípade \ft Tau = 0 \end, \ft Tau != 0 \end). rem \para* \bf Príklad 1. \end Klauzulami s diskrimináciou na nulu môžeme zadefinovať znamienkovú funkciu \ft Sgn_d(x) \end: \def fun Sgn 'Sgn_d' Sgn(x) = 0 <- x = 0 Sgn(x) = 1 <- x != 0 \end \para Aby sme ľahšie skonštruovali klauzálnu formulu pre túto funkciu, klauzuly upravíme do tvaru, v ktorom je hodnota funkcie označená (novou) premennou, ktorej budeme hovoriť \it výstupná \end premenná: \def* Sgn_d(x) = v <- x = 0 & 0 = v Sgn_d(x) = v <- x != 0 & 1 = v \end \para Zodpovedajúca klauzálna formula má tvar: \eq* x = 0 & 0 = v \/ x != 0 & 1 = v \end \para Dokážeme existenčnú podmienku (existenciu hodnoty výstupnej premennej v nájdenej klauzálnej formule): thm Sgn_exists \e v(x = 0 & 0 = v \/ x != 0 & 1 = v) proof cut x = 0 inst* \e v v = 0; 0 proved. inst* \e v v = 1; 1 proved... rem \para Funkciu zadefinujeme minimalizáciou klauzálnej formuly: fun Sgn 'Sgn_d' Sgn(x) = \m v [ x = 0 & 0 = v \/ x != 0 & 1 = v ] rem \para A klauzuly dokážeme ako vety: thm Sgn_clause1 x = 0 -> Sgn(x) = 0 proof use Sgn.0:0; 0 proved.. thm Sgn_clause2 x != 0 -> Sgn(x) = 1 proof use Sgn.0:0; x proved.. rem \para \it \bf Dichotomická diskriminácia. \end \end \para \ft Tau < Sigma \end | \ft Tau >= Sigma \end rem \para \bf Cvičenie 1. \end Jednoduchou funkciou definovateľnou pomocou dichotomickej diskriminácie je maximum: \def fun/2 Max 'Max_d' Max(x,y) = y <- x < y Max(x,y) = x <- x >= y \end \para Podobne ako v príklade 1 \points \item \para upravte definíciu zavedením vystupnej premennej, \item \para skonštruujte klauzálnu formulu, \item \para dokážte existenčnú podmienku (existenciu hodnoty výstupnej premennej v klauzálnej formule), \item \para definujte funkciu minimalizáciou a \item \para dokážte klauzuly pre maximum ako teorémy. \end \para Aby sme vám ušetrili vytváranie komponentov, vyrobili sme šablónu, v ktorej stačí, definovať predikát \ft Max_clf \end tak, aby bol ekvivalentný klauzálnej formule a doplniť dôkazy. pred/3 Max_clf Max_clf(x,y,v) <-> v = x & x >= y \/ v = y & x < y thm Max_exists \e vMax_clf(x,y,v) proof cut x >= y inst* \e vMax_clf(x,y,v); x exp Max_clf; x,y,x proved.. inst* \e vMax_clf(x,y,v); y exp Max_clf; x,y,y proved.... fun/2 Max 'Max_d' Max(x,y) = \m v [ Max_clf(x,y,v) ] thm Max_clause1 x < y -> Max(x,y) = y proof use Max.4,0,0; x; y use Max_clf.2,0,0; x; y; Max(x,y) proved... thm Max_clause2 x >= y -> Max(x,y) = x proof use Max.4,0,0; x; y use Max_clf.2,0,0; x; y; Max(x,y) proved... rem \para \it \bf Trichotomická diskriminácia. \end \end \para \ft Tau < Sigma \end | \ft Tau = Sigma \end | \ft Tau > Sigma \end rem \para \bf Cvičenie 2. \end Zadefinujte funkciu \def fun/2 Cmp Cmp(x,y) = 0 <- x < y Cmp(x,y) = 1 <- x = y Cmp(x,y) = 2 <- x > y \end \para podobne ako v cvičení 1. pred/3 Cmp_clf Cmp_clf(x,y,v) <-> v = 0 & x < y \/ v = 1 & x = y \/ v = 2 & x > y thm Cmp_exists \e vCmp_clf(x,y,v) proof case Trich; x,y @ x1,y1; x1,y1; x1,y1 inst* \e vCmp_clf(x,y,v); 0 exp Cmp_clf; x,y,0 proved.. inst* \e vCmp_clf(y,y,v); 1 exp Cmp_clf; y,y,1 proved.. inst* \e vCmp_clf(x,y,v); 2 exp Cmp_clf; x,y,2 proved.... fun/2 Cmp Cmp(x,y) = \m v [ Cmp_clf(x,y,v) ] thm Cmp_clause1 x < y -> Cmp(x,y) = 0 proof use Cmp.4,0,0; x; y use Cmp_clf.2,0,0; x; y; Cmp(x,y) proved... thm Cmp_clause2 x = y -> Cmp(x,y) = 1 proof use Cmp.4,0,0; x; y use Cmp_clf.2,0,0; x; y; Cmp(x,y) proved... thm Cmp_clause3 x > y -> Cmp(x,y) = 2 proof use Cmp.4,0,0; x; y use Cmp_clf.2,0,0; x; y; Cmp(x,y) proved... rem \para \it \bf Monadická diskriminácia. \end \end \para \ft Tau = 0 \end | \ft Tau = x+1 \end \para* Premenná \ft x \end musí byť nová v mieste použitia. Táto diskriminácia je prvá, v ktorej sa vyskytuje \it pattern matching \end ( \it porovnávanie so vzorom \end). Vzormi sú \ft 0 \end a \ft x+1 \end a porovnávame s nimi výraz \ft Tau \end. Do CL je zabudovaná všeobecnejšia forma tejto diskriminácie: \para \ft Tau = 0 \end | \ft Tau = 1 \end | \ft Cdots \end | \ft Tau = d-1 \end | \ft Tau = x+d \end \para* kde \ft d \end je \it numerál \end (číselná konštanta). Napr. pre numerál \ft 3 \end máme \ft Tau = 0 \end | \ft Tau = 1 \end | \ft Tau = 2 \end | \ft Tau = x+3 \end. \para Pripomeňme, že v diskriminácii, ktorá obsahuje premenné je ich hodnota určená jednoznačne. rem \para \bf Príklad 2. \end Zadefinujeme funkciu predchodcu \def fun Pred Pred(0) = 0 Pred(y+1) = y \end \para Okrem zavedenia výstupnej premennej presunieme diskrimináciu z argumentov funkcie do tela klauzuly (argumenty označíme novými premennými): \def* Pred(x) = v <- x = 0 & 0 = v Pred(x) = v <- x = y+1 & y = v \end \para Keď konštruujeme klauzálnu formulu, nové premenné zavedené diskrimináciou (v tomto prípade \ft y \end) \it existenčne kvantifikujeme \end: \eq* x = 0 & 0 = v \/ \e y(x = y+1 & y = v) \end rem \para \bf Cvičenie 3. \end Dokončite príklad 2. pred/2 Pred_clf Pred_clf(x,v) <-> x = 0 & 0 = v \/ \e y(x = y+1 & y = v) thm Pred_exists \e vPred_clf(x,v) proof case N; x @ 0; x1 inst* \e vPred_clf(0,v); 0 exp Pred_clf; 0,0 proved.. inst* \e vPred_clf(x1+1,v); x1 exp Pred_clf; x1+1,x1 inst* \e y y = x1; x1 proved..... fun Pred Pred(x) = \m v [ Pred_clf(x,v) ] thm Pred_clause1 Pred(0) = 0 proof use Pred.4,0,0; 0 exp Pred_clf; 0,Pred(0) proved... thm Pred_clause2 Pred(y+1) = y proof use Pred.4,0,0; y+1 exp Pred_clf; y+1,Pred(y+1) eigen \e y1(y = y1 & y1 = Pred(y+1)).0; y1 proved.... rem \para \it \bf Binárna diskriminácia. \end \end \para \ft Tau = S0(x) \end | \ft Tau = S1(x) \end \para* Premenné \ft x \end musia byť nové v mieste použitia. rem \para \bf Cvičenie 4. \end Zadefinujte funkciu rozlišujúcu párne a nepárne čísla \def fun Even Even S0(y) = 1 Even S1(y) = 0 \end \para podobne ako v príklade 2 a cvičení 3. pred/2 Even_clf Even_clf(x,v) <-> \e y(x = S0(y) & 1 = v \/ x = S1(y) & 0 = v) thm Even_exists \e vEven_clf(x,v) proof case Nb; x @ x1; x1; x1 inst* \e vEven_clf(S0(0),v); 1 exp Even_clf; S0(0),1 inst* \e y y = 0; 0 proved... inst* \e vEven_clf(S0(x1),v); 1 exp Even_clf; S0(x1),1 inst* \e y x1 = y; x1 proved... inst* \e vEven_clf(S1(x1),v); 0 exp Even_clf; S1(x1),0 inst* \e y x1 = y; x1 proved..... fun Even Even(x) = \m v [ Even_clf(x,v) ] thm Even_clause1 Even S0(x) = 1 proof use Even.4,0,0; S0(x) exp Even_clf; S0(x),Even S0(x) proved... thm Even_clause2 Even S1(x) = 0 proof use Even.4,0,0; S1(x) exp Even_clf; S1(x),Even S1(x) proved... rem \para \it \bf Diadická diskriminácia. \end \end \para \ft Tau = 0 \end | \ft Tau = S1(x) \end | \ft Tau = S2(x) \end \para* Premenné \ft x \end musia byť nové v mieste použitia. rem \para \bf Cvičenie 5. \end Zadefinujte funkciu rozlišujúcu párne a nepárne čísla, ale pomocou diadickej diskriminácie \def fun Even2 Even2(0) = 1 Even2 S1(y) = 0 Even2 S2(y) = 1 \end pred/2 Even2_clf Even2_clf(x,v) <-> \e y(x = 0 & 1 = v \/ x = S1(y) & 0 = v \/ x = S2(y) & 1 = v) thm Even2_exists \e vEven2_clf(x,v) proof case N2; x @ 0; x1; x1 inst* \e vEven2_clf(0,v); 1 exp Even2_clf; 0,1 proved.. inst* \e vEven2_clf(S1(x1),v); 0 exp Even2_clf; S1(x1),0 inst* \e y x1 = y; x1 proved... inst* \e vEven2_clf(S2(x1),v); 1 exp Even2_clf; S2(x1),1 inst* \e y x1 = y; x1 proved..... fun Even2 Even2(x) = \m v [ Even2_clf(x,v) ] thm Even2_clause1 Even2(0) = 1 proof use Even2.4,0,0; 0 exp Even2_clf; 0,Even2(0) proved... thm Even2_clause2 Even2 S1(x) = 0 proof use Even2.4,0,0; S1(x) exp Even2_clf; S1(x),Even2 S1(x) proved... thm Even2_clause3 Even2 S2(x) = 1 proof use Even2.4,0,0; S2(x) exp Even2_clf; S2(x),Even2 S2(x) proved... rem \para \it \bf Default. \end \end V klauzálnej definícii môžeme klauzuly pre niektoré nezaujímavé prípady \it vynechať \end. Funkcia však musí mať hodnotu aj v týchto prípadoch a je ňou \it defaultová \end hodnota \ft 0 \end. Vynechaným klauzulám tiež hovoríme defaultové. \para Pri konštrukcii klauzálnej formuly pre klauzálnu definíciu musíme zobrať do úvahy aj defaultové klauzuly. Pri tom nám môže pomôcť kompilátor CL. Pre danú klauzálnu definíciu interne vytvára strom diskriminácií, ktorý obsahuje aj defaultové prípady. Stlačením \it Expand \end nad klauzálnou definíciou sa strom diskriminácií ("if-ov") zobrazí v poli \it Results \end (úplne posledné pole na stránke). rem \para \bf Príklad 3. \end Ak teda máme zadefinovať funkciu \ft F1 \end s klauzulami \def fun F1 F1(x) = 7 <- x < 3 F1(x) = 450 <- x > 3 \end \para môžeme tieto klauzuly napísať do CL: fun F1_aux F1_aux(x) = 7 <- x < 3 F1_aux(x) = 450 <- x > 3 rem \para Po stlačení \it Expand \end uvidíme v \it Results \end, že medzi klauzulami chýba prípad \ft x = 3 \end (defaultová hodnota \ft 0 \end je zobrazená červeno). \para Klauzuly \bf zúplníme \end pridaním práve objaveného defaultového prípadu \def* F1(x) = 7 <- x < 3 F1(x) = 0 <- x = 3 F1(x) = 450 <- x > 3 \end \para Ďalej pokračujeme ako doteraz -- zavedením výstupnej premennej, zostrojením klauzálnej formuly atď. rem \para \bf Cvičenie 6. \end Zostrojte klauzálnu formulu, zadefinujte minimalizáciou a dokážte všetky (aj defaultové) klauzuly funkcie \def fun F2 F2(n+1) = 7*n+3 \end pred/2 F2_clf F2_clf(x,v) <-> \e n(x = 0 & 0 = v \/ x = n+1 & 7*n+3 = v) thm F2_exists \e vF2_clf(x,v) proof case N; x @ 0; n inst* \e vF2_clf(0,v); 0 exp F2_clf; 0,0 proved.. inst* \e vF2_clf(n+1,v); 7*n+3 exp F2_clf; n+1,7*n+3 inst* \e n1 n1 = n; n proved..... fun F2 F2(x) = \m v [ F2_clf(x,v) ] thm F2_clause1 F2(0) = 0 proof use F2.4,0,0; 0 exp F2_clf; 0,F2(0) proved... thm F2_clause2 F2(n+1) = 7*n+3 proof use F2.4,0,0; n+1 exp F2_clf; n+1,F2(n+1) eigen \e n1(n = n1 & 7*n1+3 = F2(n+1)).0; n1 proved.... rem \para \it \bf Vnáranie diskriminácií. \end \end Na definovanie funkcií často potrebujeme rozhodovať medzi viacerými zložitejšími prípadmi, ako umožňuje jedna distriminácia. rem \para \bf Príklad 4. \end Zložitejšou funkciou využívajúcou trojnásobnú dichotomickú diskrimináciu je maximum troch prvkov, definované klauzulami: \def fun/3 Max3 Max3(x,y,z) = z <- x <= y & y <= z Max3(x,y,z) = y <- x <= y & y > z Max3(x,y,z) = z <- x > y & x <= z Max3(x,y,z) = x <- x > y & x >= z \end \para Funkciu najprv obligátne upravíme pridaním výstupnej premennej: \def* Max3(x,y,z) = v <- x <= y & y <= z & z = v Max3(x,y,z) = v <- x <= y & y > z & y = v Max3(x,y,z) = v <- x > y & x <= z & z = v Max3(x,y,z) = v <- x > y & x >= z & x = v \end \para Klauzuly sú najprv diskriminované dichotómiou premenných \ft x \end a \ft y \end. V prípade, že \ft x <= y \end, sú prvé dve klauzuly ďalej diskriminované dichotómiou \ft y \end a \ft z \end. V prípade \ft x > y \end sú posledné dve klauzuly ďalej diskriminované dichotómiou \ft x \end a \ft z \end. Tento rozbor vnorenia diskriminácií si, podobne ako pri defaultových klauzulách, môžeme uľahčiť využitím kompilátora CL (napíšeme klauzálnu definíciu a stlačíme \it Expand \end). \para Klauzálnu formulu zostrojíme postupom zhora nadol takto: \points \item \para \header* pred/4 A1 \end \header* pred/4 A2 \end Aplikujeme "vonkajšiu" dichotomickú diskrimináciu \ft x \end a \ft y \end: \eq* x <= y & A1(x,y,z,v) \/ x > y & A2(x,y,z,v) \end \item \para Časť \ft A1 \end zostrojíme aplikovaním "vnútornej" diskriminácie prvých dvoch klauzúl \eq* A1(x,y,z,v) <-> y <= z & z = v \/ y > z & y = v \end \item \para Časť \ft A2 \end zostrojíme aplikovaním "vnútornej" diskriminácie posledných dvoch klauzúl \eq* A2(x,y,z,v) <-> x <= z & z = v \/ x > z & x = v \end \end rem \para \bf Cvičenie 7. \end Dokončite príklad 4. pred/4 Max3_a1 Max3_a1(x,y,z,v) <-> y <= z & z = v \/ y > z & y = v pred/4 Max3_a2 Max3_a2(x,y,z,v) <-> x <= z & z = v \/ x > z & x = v pred/4 Max3_clf Max3_clf(x,y,z,v) <-> x <= y & Max3_a1(x,y,z,v) \/ x > y & Max3_a2(x,y,z,v) thm Max3_exists \e vMax3_clf(x,y,z,v) proof cut x <= y cut y <= z inst* \e vMax3_clf(x,y,z,v); z exp Max3_clf; x,y,z,z exp Max3_a1; x,y,z,z proved... inst* \e vMax3_clf(x,y,z,v); y exp Max3_clf; x,y,z,y exp Max3_a1; x,y,z,y proved.... cut x <= z inst* \e vMax3_clf(x,y,z,v); z exp Max3_clf; x,y,z,z exp Max3_a2; x,y,z,z proved... inst* \e vMax3_clf(x,y,z,v); x exp Max3_clf; x,y,z,x exp Max3_a2; x,y,z,x proved...... fun/3 Max3 Max3(x,y,z) = \m v [ Max3_clf(x,y,z,v) ] thm Max3_clause1 x <= y & y <= z -> Max3(x,y,z) = z proof use Max3.4,0,0; x; y; z exp Max3_clf; x,y,z,Max3(x,y,z) exp Max3_a1; x,y,z,Max3(x,y,z) proved.... thm Max3_clause2 x <= y & y > z -> Max3(x,y,z) = y proof use Max3.4,0,0; x; y; z exp Max3_clf; x,y,z,Max3(x,y,z) exp Max3_a1; x,y,z,Max3(x,y,z) proved.... thm Max3_clause3 x > y & x <= z -> Max3(x,y,z) = z proof use Max3.4,0,0; x; y; z exp Max3_clf; x,y,z,Max3(x,y,z) exp Max3_a2; x,y,z,Max3(x,y,z) proved.... thm Max3_clause4 x > y & x >= z -> Max3(x,y,z) = x proof use Max3.4,0,0; x; y; z exp Max3_clf; x,y,z,Max3(x,y,z) exp Max3_a2; x,y,z,Max3(x,y,z) split x <= z & z = Max3(x,y,z) \/ x > z & x = Max3(x,y,z).4,0,0,0 proved proved..... rem \para \bf Príklad 5. \end \header* pred/3 A1 \end Situácia s vnorenými distrimináciami je o niečo komplikovanejšia v prípade pattern-matchingových diskriminácií. Funkcia \def fun Nb_n2 Nb_n2 S0(y) = 0 <- y = 0 Nb_n2 S0(y) = S2(z) <- y = z+1 Nb_n2 S1(y) = S1(y) \end \para je komplikovane zadefinovanou identitou ( \ft \a x Nb_n2(x) = x \end). Obsahuje dve diskriminácie -- vonkajšia je binárna, vnútorná (rozdeľujúca prvé dve klauzuly) je monadická. Najprv vykonáme obligátne zavedenie výstupnej premennej a presun diskriminácií z argumentov do tela klauzúl (zúplňovať netreba, nemáme žiadne defaultové prípady): \def* Nb_n2(x) = v <- x = S0(y) & y = 0 & 0 = v Nb_n2(x) = v <- x = S0(y) & y = z+1 & S2(z) = v Nb_n2(x) = v <- x = S1(y) & S1(y) = v \end \para Klauzálnu formulu potom skonštruujeme takto: \eq* \e y(x = S0(y) & A1(x,y,v)) \/ \e y(x = S1(y) & S1(y) = v) \end \para pričom klauzálna formula \ft A1(x,y,v) \end pre vnorenú diskrimináciu je \eq* A1(x,y,v) <-> y = 0 & 0 = v \/ \e z(y = z+1 & S2(z) = v) \end rem \para \bf Cvičenie 8. \end Dokončite príklad 5. pred/3 Nb_n2_a1 Nb_n2_a1(x,y,v) <-> y = 0 & 0 = v \/ \e z(y = z+1 & S2(z) = v) pred/2 Nb_n2_clf Nb_n2_clf(x,v) <-> \e y(x = S0(y) & Nb_n2_a1(x,y,v)) \/ \e y(x = S1(y) & S1(y) = v) thm Nb_n2_exists \e vNb_n2_clf(x,v) proof case Nb; x @ y; y; y inst* \e vNb_n2_clf(S0(0),v); 0 exp Nb_n2_clf; S0(0),0 inst* \e y1(y1 = 0 & Nb_n2_a1(S0(0),y1,0)); 0 exp Nb_n2_a1; S0(0),0,0 proved.... case N; y @ 0; z proved inst* \e vNb_n2_clf(S0(z+1),v); S2(z) exp Nb_n2_clf; S0(z+1),S2(z) inst* \e y1(z+1 = y1 & Nb_n2_a1(S0(z+1),y1,S2(z))); y exp Nb_n2_a1; S0(z+1),z+1,S2(z) inst* \e z1 z1 = z; z proved...... inst* \e vNb_n2_clf(S1(y),v); S1(y) exp Nb_n2_clf; S1(y),S1(y) inst* \e y1 y1 = y; y proved..... fun Nb_n2 Nb_n2(x) = \m v [ Nb_n2_clf(x,v) ] thm Nb_n2_clause1 y = 0 -> Nb_n2 S0(y) = 0 proof use Nb_n2.4,0,0; S0(0) exp Nb_n2_clf; S0(0),Nb_n2 S0(0) eigen \e y1(y1 = 0 & Nb_n2_a1(S0(0),y1,Nb_n2 S0(0))).0; y1 exp Nb_n2_a1; S0(0),0,Nb_n2 S0(0) proved..... thm Nb_n2_clause2 y = z+1 -> Nb_n2 S0(y) = S2(z) proof use Nb_n2.4,0,0; S0(y) exp Nb_n2_clf; S0(z+1),Nb_n2 S0(z+1) eigen \e y1(z+1 = y1 & Nb_n2_a1(S0(z+1),y1,Nb_n2 S0(z+1))).0; y1 exp Nb_n2_a1; S0(y1),y1,Nb_n2 S0(y1) conj..... thm Nb_n2_clause3 Nb_n2 S1(y) = S1(y) proof use Nb_n2.4,0,0; S1(y) exp Nb_n2_clf; S1(y),Nb_n2 S1(y) eigen \e y1(y = y1 & S1(y1) = Nb_n2 S1(y)).0; y1 proved.... rem \para \bf Cvičenie 8a. \end Dokážte, že \ft Nb_n2 \end je identita. thm Nb_n2_id Nb_n2(x) = x proof use Nb_n2.4,0,0; x exp Nb_n2_clf; x,Nb_n2(x) eigen \e y(x = S0(y) & Nb_n2_a1(x,y,Nb_n2(x))) \/ \e y(x = S1(y) & S1(y) = Nb_n2(x)).0:3,0,0,0; y,y1 split x = S0(y) & Nb_n2_a1(x,y,Nb_n2(x)) \/ x = S1(y1) & S1(y1) = Nb_n2(x).4, 0, 0, 0 exp Nb_n2_a1; S0(y),y,Nb_n2 S0(y) split y = 0 & Nb_n2 S0(y) = 0 \/ \e z(y = z+1 & S2(z) = Nb_n2 S0(y)).4,0, 0,0 proved conj.. proved..... rem \para \bf Cvičenie 9. \end Zadefinujete funkciu \def fun Pred2 Pred2(0) = 0 Pred2 S1(y) = S0(y) Pred2 S2(y) = S1(y) \end \para A dokážte, že počíta predchodcu svojho argumentu. pred/2 Pred2_clf Pred2_clf(x,v) <-> x = 0 & 0 = v \/ \e y(x = S1(y) & S0(y) = v) \/ \e y(x = S2(y) & S1(y) = v) thm Pred2_exists \e vPred2_clf(x,v) proof case N2; x @ 0; x1; x1 inst* \e vPred2_clf(0,v); 0 exp Pred2_clf; 0,0 proved.. inst* \e vPred2_clf(S1(x1),v); S0(x1) exp Pred2_clf; S1(x1),S0(x1) inst* \e y y = x1; x1 proved... inst* \e vPred2_clf(S2(x1),v); S1(x1) exp Pred2_clf; S2(x1),S1(x1) inst* \e y y = x1; x1 proved..... fun Pred2 Pred2(x) = \m v [ Pred2_clf(x,v) ] thm Pred2_clause1 Pred2(0) = 0 proof use Pred2.4,0,0; 0 exp Pred2_clf; 0,Pred2(0) proved... thm Pred2_clause2 Pred2 S1(y) = S0(y) proof use Pred2.4,0,0; S1(y) exp Pred2_clf; S1(y),Pred2 S1(y) eigen \e y1(y = y1 & S0(y1) = Pred2 S1(y)).0; y1 proved.... thm Pred2_clause3 Pred2 S2(y) = S1(y) proof use Pred2.4,0,0; S2(y) exp Pred2_clf; S2(y),Pred2 S2(y) eigen \e y1(y = y1 & S1(y1) = Pred2 S2(y)).0; y1 proved.... thm Pred2_pred Pred2(x) = Pred(x) proof use Pred2.4,0,0; x exp Pred2_clf; x,Pred2(x) use Pred.4,0,0; x exp Pred_clf; x,Pred(x) split x = 0 & Pred(x) = 0 \/ \e y(x = y+1 & y = Pred(x)).4,0,0,0 proved eigen \e y(x = y+1 & y = Pred(x)).0; y split \e y1(Pred(y+1) = 2*y1 & S0(y1) = Pred2(Pred(y+1)+1)) \/ \e y1(Pred(y+1) = 2*y1+1 & S1(y1) = Pred2(Pred(y+1)+1)).4,0,0,0 conj conj........ rem \para \it \bf Diskriminácia na podiel a zvyšok. \end \end Pre každý \it numerál \end (číselnú konštantu) \ft d > 0 \end je diskrimináciou \para \ft Tau = d*q+r & 0 <= r & r <= d-1 \end \para* pre nové premenné \ft q \end a \ft r \end. Napr. pre numerál \ft 5 \end máme \ft Tau = 5*q+r & 0 <= r & r <= 4 \end. rem \para \bf Cvičenie 10. \end Zadefinujete funkciu \def fun Swap_rem4 Swap_rem4(4*x+r) = 4*x+3 <- 0 <= r & r <= 3 & r = 0 Swap_rem4(4*x+r) = 4*x+2 <- 0 <= r & r <= 3 & r = 1 Swap_rem4(4*x+r) = 4*x+1 <- 0 <= r & r <= 3 & r = 2 Swap_rem4(4*x+r) = 4*x <- 0 <= r & r <= 3 & r = 3 \end pred/2 Swap_rem4_clf Swap_rem4_clf(x,v) <-> \e y(x = 4*y & 4*y+3 = v) \/ \e y(x = 4*y+1 & 4*y+2 = v) \/ \e y(x = 4*y+2 & 4*y+1 = v) \/ \e y(x = 4*y+3 & 4*y = v) thm Swap_rem4_exists \e vSwap_rem4_clf(x,v) proof use Swap_rem4_clf.2,1,0:0; x; v split \e y(x = 4*y & 4*y+3 = v) \/ \e y(x = 4*y+1 & 4*y+2 = v) \/ \e y(x = 4*y+2 & 4*y+1 = v) \/ \e y(x = 4*y+3 & 4*y = v) -> Swap_rem4_clf(x,v).2,1,0 case Nb; x @ x1; x1; x1 inst* \e y(y = 0 & 4*y+3 = v); 0 inst* \e vSwap_rem4_clf(S0(0),v); 3 exp Swap_rem4_clf; S0(0),3 inst* \e y y = 0; 0 proved.... case Nb; x1 @ x2; x2; x2 proved inst* \e y(x2 = y & 4*y+3 = v); x2 inst* \e vSwap_rem4_clf(S0 S0(x2),v); 4*x2+3 exp Swap_rem4_clf; S0 S0(x2),4*x2+3 inst* \e y y = x2; x2 proved.... inst* \e y(x2 = y & 4*y+1 = v); x2 inst* \e vSwap_rem4_clf(S0 S1(x2),v); 4*x2+1 exp Swap_rem4_clf; S0 S1(x2),4*x2+1 inst* \e y y = x2; x2 proved..... conj. inst* \e vSwap_rem4_clf(x,v); v proved.... fun Swap_rem4 Swap_rem4(x) = \m v [ Swap_rem4_clf(x,v) ] thm Swap_rem4_clause1 0 <= r & r <= 3 & r = 0 -> Swap_rem4(4*x+r) = 4*x+3 proof use Swap_rem4.4,0,0; 4*x exp Swap_rem4_clf; 4*x,Swap_rem4(4*x) eigen \e y(x = y & 4*y+3 = Swap_rem4(4*x)).0; y proved.... thm Swap_rem4_clause2 0 <= r & r <= 3 & r = 1 -> Swap_rem4(4*x+r) = 4*x+2 proof use Swap_rem4.4,0,0; 4*x+1 exp Swap_rem4_clf; 4*x+1,Swap_rem4(4*x+1) eigen \e y(x = y & 4*y+2 = Swap_rem4(4*x+1)).0; y proved.... thm Swap_rem4_clause3 0 <= r & r <= 3 & r = 2 -> Swap_rem4(4*x+r) = 4*x+1 thm Swap_rem4_clause4 0 <= r & r <= 3 & r = 3 -> Swap_rem4(4*x+r) = 4*x rem \para \it \bf Párová diskriminácia. \end \end Okrem už uvedených diskriminácií je do CL zabudovaná aj párová diskriminácia \para \ft Tau = 0 \end | \ft Tau = v,w \end \para* Striktne vzaté by sme túto diskrimináciu nemali používať, pretože sa týka párovacej funkcie " \bf , \end " zabudovanej do CL. Dokazovač CL však o tejto funkcii nevie viac, ako sme dokázali v cvičení ex08 o párovacej funkcii " \bf ; \end ". rem \para \bf Cvičenie 11. \end Zadefinujete funkciu \def fun F3 F3(0) = 0 F3(u,0) = u F3(u,v,w) = u+v*w \end pred/2 F3_clf F3_clf(x,v) <-> x = 0 & 0 = v \/ \e a(x = a,0 & a = v) \/ \e a\e b\e c(x = a,b,c & a+b*c = v) thm F3_exists \e vF3_clf(x,v) proof case Ln; x @ 0; v,w inst* \e vF3_clf(0,v); 0 exp F3_clf; 0,0 proved.. case Ln; w @ 0; v1,w1 inst* \e v1F3_clf((v,0),v1); v exp F3_clf; (v,0),v inst* \e a a = v; v proved... inst* \e v2F3_clf((v,v1,w1),v2); v+v1*w1 exp F3_clf; (v,v1,w1),v+v1*w1 inst* \e a(\e b(\e c(w1 = c & a+b*c = v+v1*w1) & v1 = b) & v = a):0,3, (0,3,0,1,0), 1,0; v; v1; w1 proved...... fun F3 F3(x) = \m v [ F3_clf(x,v) ] thm F3_clause1 F3(0) = 0 proof use F3.4,0,0; 0 exp F3_clf; 0,F3(0) proved... thm F3_clause2 F3(u,0) = u proof use F3.4,0,0; u,0 exp F3_clf; (u,0),F3(u,0) eigen \e a(u = a & a = F3(u,0)).0; a proved.... thm F3_clause3 F3(u,v,w) = u+v*w proof use F3.4,0,0; u,v,w exp F3_clf; (u,v,w),F3(u,v,w) eigen \e a(\e b(\e c(w = c & a+b*c = F3(u,v,w)) & v = b) & u = a).0:0,3, (0,3,0, 1,0),1, 0; a,b, c proved.... rem \para \bf Cvičenie 12. \end Zadefinujte doleuvedené funkcie pomocou minimalizácie príslušných klauzálnych formúl a dokážte klauzuly ako teorémy. \it Nezabúdajte na defaultové klauzuly. \end \def fun/2 F4 F4(0,0) = 1 F4(2,a,b) = 2 <- a > b \end rem \para Nezabúdajte, že sa to robí presne tak isto ako všetky ostatné cvičenia z tohto cvičenia a ja sa idem radšej vyspať, než by som mal toto stále dokola robiť. rem \def fun/2 F5 F5(0,0) = 1 F5(3,x,y,z) = 2 <- x > y \end rem \def fun/3 G_fib G_fib(x,0,u,z,b) = S0(u+z) G_fib(x,1,a) = S1(x-1) G_fib(x,m+2,a) = S0(1) <- x < 2 G_fib(x,m+2,a) = S1(x-2) <- x >= 2 \end rem \def fun/3 G_fib2 G_fib2(0,n,a) = S0(1) G_fib2(1,n,a) = S0(1) G_fib2(x+2,m+2,a) = S1(x) G_fib2(x+2,1,a) = S1(x+1) G_fib2(x+2,0,u,v,b) = S0(u+v) \end