Ukubhala kabusha

Kumathematika, isayensi yekhompiyutha, kanye nokunengqondo, ukubhala kabusha kuhlanganisa izindlela eziningi (okungenzeka zinganqumeli ) zokushintsha amagama angezansi efomula namanye amagama.Izinto okugxilwe kuzo zalesi sihloko zihlanganisa amasistimu okubhala kabusha (owaziwa nangokuthi amasistimu okubhala kabusha, bhala kabusha izinjini, noma amasistimu okunciphisa ).Ngokwesimo sawo esiyisisekelo, aqukethe iqoqo lezinto, kanye nobudlelwano bokuthi zingaguqulwa kanjani lezo zinto.

Ukubhala kabusha kungase kunganqumi .Umthetho owodwa wokubhala kabusha igama ungasetshenziswa ngezindlela eziningi ezahlukene kulelo gama, noma kungasebenza umthetho ongaphezu kowodwa.Amasistimu okubhala kabusha awanikezi i- algorithm yokushintsha ithemu elilodwa ukuya kwelinye, kodwa isethi yemithetho engase isetshenziswe.Nokho, uma kuhlanganiswe ne-algorithm efanelekile, amasistimu okubhala kabusha angabhekwa njengezinhlelo zekhompyutha , futhi izaga ezimbalwa ze- nezilimi zokuhlela ezimemezelayo zisekelwe ekubhalweni kabusha kwethemu.

Isibonelo samacala

Okunengqondo

Ngo logic, inqubo yokuthola ifomu evamile conjunctive (CNF) yefomula ezingase zithathwe njengoba uhlelo ubhalwe kabusha.Imithetho yesibonelo sesistimu enjalo ingaba:

$\mathrm{\neg }\mathrm{\neg }A\to A$ ( ukuchithwa okuphindwe kabili )

$\mathrm{\neg }(A\wedge B)\to \mathrm{\neg }A\vee \mathrm{\neg }B$ (Imithetho kaDe Morgan )

$\mathrm{\neg }(A\vee B)\to \mathrm{\neg }A\wedge \mathrm{\neg }B$

$(A\wedge B)\vee C\to (A\vee C)\wedge (B\vee C)$ ( ukusabalalisa )

$A\vee (B\wedge C)\to (A\vee B)\wedge (A\vee C),$

lapho inombolo ( $\to$ ) kubonisa ukuthi isisho esihambisana nesandla sobunxele somthetho singabhalwa kabusha sibe sisohlangothini lwesandla sokudla, futhi izimpawu ngayinye isho umusho ongaphansi.Esimisweni esinjalo, umthetho ngamunye ukhethwa ukuze uhlangothi lwesobunxele lulingane nohlangothi lwesokudla, futhi ngenxa yalokho lapho uhlangothi lwesobunxele lufana ne-subexpression, ukubhala kabusha kwaleyo nkulumo engaphansi ukusuka kwesobunxele kuya kwesokudla igcina ukuvumelana okunengqondo kanye nenani layo yonke inkulumo. .

I-Arithmetic

Amasistimu okubhala kabusha ethemu angasetshenziswa ukubala ukusebenza kwezibalo ezinombolweni zemvelo .Ukuze wenze lokhu, inombolo ngayinye enjalo kufanele ifakwe ikhodi njengetemu .Umbhalo wekhodi olula yilowo osetshenziswa ku- axiom ye -Peano, esekelwe ku-0 (zero) ongashintshi kanye nomsebenzi womlandeli u- S . isibonelo, izinombolo 0, 1, 2, kanye no-3 zimelelwe imigomo 0, S(0), S(S(0)), kanye S(S(S(0))), ngokulandelana.Uhlelo olulandelayo lokubhala kabusha lungasetshenziswa ukubala isamba nomkhiqizo wezinombolo zemvelo ezinikeziwe.

$\begin{array}{ccc}A+0& \to A& \text{(1)},\\ A+S(B)& \to S(A+B)& \text{(2)},\\ A\cdot 0& \to 0& \text{(3)},\\ A\cdot S(B)& \to A+(A\cdot B)& \text{(4)}.\end{array}$

Isibonelo, ukubalwa kuka-2+2 ukuze kuphumele ku-4 kungaphindwa ngokuphinda kubhalwe igama ngale ndlela elandelayo:

$S(S(0))+S(S(0))$ $\stackrel{(2)}{\to }$ $S(S(S(0))+S(0))$ $\stackrel{(2)}{\to }$ $S(S(S(S(0))+0))$ $\stackrel{(1)}{\to }$ $S(S(S(S(0)))),$

lapho izinombolo zomthetho zinikezwa ngenhla komcibisholo obhala kabusha.

Njengesinye isibonelo, ukubalwa kwe-2⋅2 kubukeka kanje:

$S(S(0))\cdot S(S(0))$ $\stackrel{(4)}{\to }$ $S(S(0))+S(S(0))\cdot S(0)$ $\stackrel{(4)}{\to }$ $S(S(0))+S(S(0))+S(S(0))\cdot 0$ $\stackrel{(3)}{\to }$ $S(S(0))+S(S(0))+0)$ $\stackrel{(1)}{\to }$ $S(S(0))+S(S(0))$ $\stackrel{\text{s.a.}}{\to }$ $S(S(S(S(0)))),$

lapho isinyathelo sokugcina sihlanganisa isibonelo sangaphambilini sokubala.

Isayensi yezilimi

Ezifundweni zolimi, imithetho yesakhiwo samagama, ebizwa nangokuthi imithetho yokubhala kabusha, isetshenziswa kwezinye izinhlelo zohlelo lolimi olukhiqizayo,njengendlela yokukhiqiza imisho elungile ngokohlelo lolimi.Umthetho onjalo ngokuvamile uthatha uhlobo A → X, lapho u-A eyilebula yesigaba sokwenziwa , njengebinzana lebizo noma umusho, futhi u-X uwukulandelana kwalawo malebula noma amamofimu, okuveza iqiniso lokuthi u-A angathathelwa indawo ngu-X ekukhiqizeni isakhiwo somusho.Isibonelo, umthetho othi S → NP VP usho ukuthi umusho ungaqukatha ibinzana eliyibizo elilandelwa umusho wesenzo ; eminye imithetho izocacisa ukuthi ibinzana lebizo nebinzana lesenzo lingaqukatha ini, njalo njalo.

Amasistimu okubhala kabusha angabonakali

Kulezi zibonelo ezingenhla, kusobala ukuthi singacabanga ngokubhala kabusha amasistimu ngendlela engabonakali.Kudingeka sicacise isethi yezinto kanye nemithetho engasetshenziswa ukuze siziguqule.Isilungiselelo esivame kakhulu (esingavamile) salo mbono sibizwa ngokuthi isistimu yokunciphisa noma isistimu yokubhala kabusha engabonakali (isifinyezo se- ARS ). I-ARS imane iyisethi engu- A yezinto, kanye nokuhlobana okumbambambili → ku- A okubizwa ngokuthi ubuhlobo bokunciphisa, bhala kabusha ubuhlobo noma nje ukunciphisa .

Imibono eminingi kanye nokuphawula kungachazwa kulungiselelo elivamile le-ARS. $\stackrel{*}{\to }$ ukuvalwa kwe- reflexive transitive kwe $\to$ . $\leftrightarrow$ ukuvalwa kwe-symmetric ye $\to$ . $\stackrel{*}{\leftrightarrow }$ ukuvalwa kwe- reflexive transitive symmetric of $\to$ . Igama elithi inkinga le-ARS liyanquma, kunikezwe u- x kanye no- y, ukuthi ngabe $x\stackrel{*}{\leftrightarrow }y$ . Into engu- x ku- A ibizwa ngokuthi i- reducible uma kukhona omunye u- y ku- A onjalo $x\to y$ ; kungenjalo ibizwa ngokuthi i- irreducible noma ifomu elivamile . Into ethi y ibizwa ngokuthi "uhlobo olujwayelekile luka- x " uma $x\stackrel{*}{\to }y$, futhi y akanakuncishiswa. Uma uhlobo olujwayelekile luka- x luhlukile, lokhu kuvame ukuchazwa ngokuthi $x\downarrow$ . Uma yonke into inefomu okungenani elilodwa elivamile, i-ARS ibizwa ngokuthi normalizing . $x\downarrow y$ noma u- x kanye no- y kuthiwa angahlanganiswa uma kukhona okuthi z nempahla leyo $x\stackrel{*}{\to }z\stackrel{*}{\leftarrow }y$ . Kuthiwa i-ARS inempahla ye- Church–Rosser uma $x\stackrel{*}{\leftrightarrow }y$ kusho $x\downarrow y$ . I-ARS ihlangana uma kukho konke u- w, x, kanye no- y kokuthi A, $x\stackrel{*}{\leftarrow }w\stackrel{*}{\to }y$ kusho $x\downarrow y$ . I-ARS ihlangana endaweni uma futhi kuphela uma kubo bonke u- w, x, kanye no- y kokuthi A, $x\leftarrow w\to y$ kusho $x\downarrow y$ . Kuvele ARS kuthiwa oqeda noma noetherian uma kukhona akukho ketanga elingapheli $x_0\to x_1\to x_2\to \cdots$ . I-confluent ne-ARS eqedayo ibizwa ngokuthi i- convergent noma i- canonical .

Theorems Ezibalulekile Ezingafundwa izinhlelo abstract ubhalwe kabusha kukhona ukuthi ARS kuyinto confluent IFF it has impahla Church-Rosser, lemma Newman sika okuyinto sithi ARS ukuqeda kuyinto confluent kuphela uma kuba endaweni confluent, nokuthi inkinga izwi i ARS kuyinto undecidable ngenjwayelo.