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, Joseph Goguen "Proving and Rewriting" International Conference on Algebraic and Logic Programming, 1990 Nancy, France pp 1-24  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:

  ( ukuchithwa okuphindwe kabili )
  (Imithetho kaDe Morgan )

  ( ukusabalalisa )
  This variant of the previous rule is needed since the commutative law A∨B = B∨A cannot be turned into a rewrite rule. A rule like A∨B → B∨A would cause the rewrite system to be nonterminating.

lapho inombolo (  ) 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. 



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



lapho izinombolo zomthetho zinikezwa ngenhla komcibisholo obhala kabusha.

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



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 Book and Otto, p. 10 noma isistimu yokubhala kabusha engabonakali (isifinyezo se- ARS ). Bezem et al., p. 7,I-ARS imane iyisethi engu- A yezinto, kanye nokuhlobana okumbambambili → ku- A okubizwa ngokuthi ubuhlobo bokunciphisa, bhala kabusha ubuhlobo Bezem et al., p. 7 noma nje ukunciphisa . 

Imibono eminingi kanye nokuphawula kungachazwa kulungiselelo elivamile le-ARS.  ukuvalwa kwe- reflexive transitive kwe  .  ukuvalwa kwe-symmetric ye  .  ukuvalwa kwe- reflexive transitive symmetric of  . Igama elithi inkinga le-ARS liyanquma, kunikezwe u- x kanye no- y, ukuthi ngabe  . Into engu- x ku- A ibizwa ngokuthi i- reducible uma kukhona omunye u- y ku- A onjalo  ; kungenjalo ibizwa ngokuthi i- irreducible noma ifomu elivamile . Into ethi y ibizwa ngokuthi "uhlobo olujwayelekile luka- x " uma , futhi y akanakuncishiswa. Uma uhlobo olujwayelekile luka- x luhlukile, lokhu kuvame ukuchazwa ngokuthi  . Uma yonke into inefomu okungenani elilodwa elivamile, i-ARS ibizwa ngokuthi normalizing .  noma u- x kanye no- y kuthiwa angahlanganiswa uma kukhona okuthi z nempahla leyo  . Kuthiwa i-ARS inempahla ye- Church–Rosser uma  kusho  . I-ARS ihlangana uma kukho konke u- w, x, kanye no- y kokuthi A,  kusho  . I-ARS ihlangana endaweni uma futhi kuphela uma kubo bonke u- w, x, kanye no- y kokuthi A,  kusho  . Kuvele ARS kuthiwa oqeda noma noetherian uma kukhona akukho ketanga elingapheli  . 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.