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:

: \neg\neg A \to A ( ukuchithwa okuphindwe kabili )
: \neg(A \land B) \to \neg A \lor \neg B (Imithetho kaDe Morgan )
: \neg(A \lor B) \to \neg A \land\neg B
:  (A \land B) \lor C \to (A \lor C) \land (B \lor C) ( ukusabalalisa )
:  A \lor (B \land C) \to (A \lor B) \land (A \lor 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{align}
A + 0    &\to A        & \textrm{(1)}, \\
A + S(B)   &\to S (A + B)    & \textrm{(2)}, \\
A \cdot 0  &\to 0        & \textrm{(3)}, \\
A \cdot S(B) &\to A + (A \cdot B) & \textrm{(4)}.
\end{align}

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{\textrm{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{*}{\rightarrow} ukuvalwa kwe- reflexive transitive kwe \rightarrow . \leftrightarrow ukuvalwa kwe-symmetric ye \rightarrow . \stackrel{*}{\,\leftrightarrow\,} ukuvalwa kwe- reflexive transitive symmetric of \rightarrow . 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 \rightarrow y ; kungenjalo ibizwa ngokuthi i- *irreducible* noma ifomu elivamile . Into ethi *y* ibizwa ngokuthi "uhlobo olujwayelekile luka- *x* " uma x \stackrel{*}{\,\rightarrow\,} 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{*}{\,\rightarrow\,} 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{*}{\,\rightarrow\,} 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 \rightarrow y kusho x\mathbin\downarrow y . Kuvele ARS kuthiwa *oqeda* noma *noetherian* uma kukhona akukho ketanga elingapheli x_0 \rightarrow x_1 \rightarrow x_2 \rightarrow \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.