Critical pair (term rewriting)
[[ફાઇલઃ ક્રિટપેયર svg.svg |thumb |400px |Triangle બે પુનર્લેખન નિયમો s → t (ઉપરની પંક્તિ, ડાબે) અને l → r (જમણે) માંથી મેળવેલ નિર્ણાયક જોડીની આકૃતિ. અવેજી σ ઉપપદ s|p ને l સાથે એકીકૃત કરે છે. પરિણામી આવરણ શબ્દ sσ [lσ] p (નીચલી પંક્તિ, મધ્ય) ને અનુક્રમે tσ અને sσ [rσ] p (નીચલી પંક્તિ, ડાબી અને જમણી) શબ્દમાં ફરીથી લખી શકાય છે. પછીના બે શબ્દો નિર્ણાયક જોડી બનાવે છે. જો પુનર્લેખન નિયમ સમૂહ સંમિશ્રિત હોય તો તેમને આખરે સામાન્ય શબ્દમાં ફરીથી લખી શકાય છે.] એક નિર્ણાયક જોડી શબ્દ પુનર્લેખન પ્રણાલીમાં ઊભી થાય છે જ્યારે બે પુનર્લેખન નિયમો બે અલગ અલગ શબ્દો મેળવવા માટે ઓવરલેપ થાય છે. વધુ વિગતવાર, (t1, t2) એક નિર્ણાયક જોડી છે જો ત્યાં એક શબ્દ t હોય જેના માટે ફરીથી લખવાના નિયમના બે અલગ અલગ ઉપયોગો (ક્યાં તો સમાન નિયમ અલગ રીતે લાગુ થાય છે, અથવા બે અલગ અલગ નિયમો) શબ્દો t1 અને t2 આપે છે. વ્યાખ્યાઓ નિર્ણાયક જોડીની વાસ્તવિક વ્યાખ્યા થોડી વધુ સંકળાયેલી હોય છે કારણ કે તે એવી જોડીને બાકાત રાખે છે જે નિર્ણાયક જોડીઓમાંથી અવેજી દ્વારા મેળવી શકાય છે અને ઓવરલેપ પર આધારિત જોડીને દિશા આપે છે. ખાસ કરીને, ઓવરલેપિંગ નિયમોની જોડી માટે અને, ઓવરલેપ કેટલાક બિન-ખાલી સંદર્ભ માટે છે, અને શબ્દ (જે ચલ નથી) કેટલાક અવેજી હેઠળ મેળ ખાય છે જે સૌથી સામાન્ય છે, નિર્ણાયક જોડી છે. જ્યારે નિર્ણાયક જોડીની બંને બાજુઓ એક જ મુદત સુધી ઘટી શકે છે, ત્યારે નિર્ણાયક જોડીને અભિસારી કહેવામાં આવે છે. જ્યાં નિર્ણાયક જોડીની એક બાજુ બીજી સાથે સમાન હોય છે, ત્યાં નિર્ણાયક જોડીને તુચ્છ કહેવામાં આવે છે. ઉદાહરણો ઉદાહરણ તરીકે, નિયમો સાથે પુનર્લેખન પ્રણાલી શબ્દમાં {|-| f (g (x, y), z) | | → g (x, z) |-| g (x, y) | | → x, |} એકમાત્ર નિર્ણાયક જોડી ±g (x, z), f (x, z) ω છે. આ બંને શબ્દો એક જ પુનર્લેખન નિયમ લાગુ કરીને f (g (x, y), z) શબ્દમાંથી મેળવી શકાય છે. અન્ય એક ઉદાહરણ તરીકે, એક જ નિયમ {|-| f (x, y) | | | | x સાથે પુનર્લેખન પ્રણાલી શબ્દને ધ્યાનમાં લો. |-|} આ નિયમને f (f (x, x), x) શબ્દ પર બે અલગ અલગ રીતે લાગુ કરીને, આપણે જોઈએ છીએ કે (f (x, x), f (x, x)) એક (તુચ્છ) નિર્ણાયક જોડી છે. ક્રિટિકલ જોડી લેમ્મા કોન્ફ્લુઅન્સ સ્પષ્ટપણે કન્વર્જન્ટ ક્રિટિકલ જોડીઓ સૂચવે છેઃ જો કોઈ ક્રિટિકલ જોડી ̃a, b ω ઊભી થાય, તો પછી a અને b નો સામાન્ય ઘટાડો થાય છે અને આમ ક્રિટિકલ જોડી કન્વર્જન્ટ હોય છે. જો પુનર્લેખન પ્રણાલી શબ્દ સંમિશ્રિત ન હોય, તો નિર્ણાયક જોડી એકરૂપ ન થઈ શકે, તેથી નિર્ણાયક જોડીઓ સંભવિત સ્રોતો છે જ્યાં સંગમ નિષ્ફળ જશે. 'ક્રિટિકલ પેઅર લેમ્મા' જણાવે છે કે શબ્દ પુનર્લેખન પદ્ધતિ નબળી છે (ઉર્ફ. સ્થાનિક રીતે) જો અને માત્ર ત્યારે જ સંમિશ્રિત થાય જો તમામ નિર્ણાયક જોડીઓ અભિસારી હોય. આમ, પુનર્લેખન શબ્દ પ્રણાલી નબળી રીતે સંમિશ્રિત છે કે કેમ તે શોધવા માટે, તમામ નિર્ણાયક જોડીઓનું પરીક્ષણ કરવું અને તેઓ અભિસારી છે કે કેમ તે જોવું પૂરતું છે. આ શબ્દ પુનર્લેખન પ્રણાલી નબળી રીતે સંયોજિત છે કે નહીં તે એલ્ગોરિધમિક રીતે શોધવાનું શક્ય બનાવે છે, જો કે બે શબ્દો ભેગા થાય છે કે નહીં તે એલ્ગોરિધમિક રીતે ચકાસી શકાય છે. નુથ-બેન્ડિક્સ કમ્પ્લીશન પણ જુઓ, જે નિર્ણાયક જોડીઓ પર આધારિત એક એલ્ગોરિધમ છે, જે આપેલ એક બાહ્ય કડીની સમકક્ષ મિશ્ર અને સમાપ્તિ શબ્દ પુનર્લેખન પ્રણાલીની ગણતરી કરે છે, સંદર્ભો ફ્રાન્ઝ બાડર અને ટોબિયાસ નિપકોવ, ટર્મ રીરાઈટિંગ એન્ડ ઓલ ધેટ, "કેમ્બ્રિજ યુનિવર્સિટી પ્રેસ, 1998 (બુક વેબલિંક) રીરાઈટિંગ સિસ્ટમ્સ