Algebraic semantics (computer science)
કોમ્પ્યુટર વિજ્ઞાનમાં, બીજગણિત શબ્દાર્થશાસ્ત્ર એ ઔપચારિક રીતે કાર્યક્રમની વિશિષ્ટતાઓ વિશે વર્ણન કરવા અને તર્ક કરવા માટે બીજગણિત નિયમો પર આધારિત સ્વયંસિદ્ધ શબ્દાર્થશાસ્ત્રનું એક સ્વરૂપ છે. બીજગણિત સ્પષ્ટીકરણનું વાક્યરચના બે તબક્કામાં ઘડવામાં આવે છેઃ (1) માહિતીના પ્રકારો અને કામગીરી પ્રતીકોની ઔપચારિક સહીને વ્યાખ્યાયિત કરવી, અને (2) સમૂહો અને કાર્યો દ્વારા સહીનું અર્થઘટન કરવું. સહીની વ્યાખ્યા બીજગણિત સ્પષ્ટીકરણની સહી તેના ઔપચારિક વાક્યરચનાને વ્યાખ્યાયિત કરે છે. "સહી" શબ્દનો ઉપયોગ સંગીતના સંકેતલિપીમાં "કી સહી" ના ખ્યાલની જેમ થાય છે. સહીમાં ડેટા પ્રકારોનો સમૂહ હોય છે, જેને સૉર્ટ્સ તરીકે ઓળખવામાં આવે છે, સાથે સેટના પરિવાર સાથે, દરેક સમૂહમાં ઓપરેશન પ્રતીકો (અથવા ફક્ત પ્રતીકો) હોય છે જે પ્રકારોને સંબંધિત કરે છે. આપણે સૉર્ટ સાથે સંબંધિત ઓપરેશન પ્રતીકોના સમૂહને દર્શાવવા માટે ઉપયોગ કરીએ છીએ. ઉદાહરણ તરીકે, પૂર્ણાંક સ્ટેક્સની સહી માટે, આપણે બે પ્રકારો વ્યાખ્યાયિત કરીએ છીએ, એટલે કે, અને, અને ઓપરેશન પ્રતીકોના નીચેના પરિવારઃ જ્યાં ખાલી શબ્દમાળા સૂચવે છે. હસ્તાક્ષરનું સમૂહ-સૈદ્ધાંતિક અર્થઘટન બીજગણિત પ્રકારો અને કામગીરી પ્રતીકોને સમૂહો અને કાર્યો તરીકે અર્થઘટન કરે છે. દરેક સૉર્ટને સમૂહ તરીકે અર્થઘટન કરવામાં આવે છે, જેને સૉર્ટનો વાહક કહેવામાં આવે છે, અને દરેક પ્રતીકને ફંક્શનમાં મેપ કરવામાં આવે છે, જેને ઓપરેશન ઓફ કહેવામાં આવે છે. પૂર્ણાંક સ્ટેક્સની સહીના સંદર્ભમાં, અમે સૉર્ટને પૂર્ણાંકોના સમૂહ તરીકે અર્થઘટન કરીએ છીએ, અને સૉર્ટને પૂર્ણાંક સ્ટેક્સના સમૂહ તરીકે અર્થઘટન કરીએ છીએ. આપણે આગળ ઓપરેશન પ્રતીકોના પરિવારનું નીચેના કાર્યો તરીકે અર્થઘટન કરીએ છીએઃ સિમેન્ટિક્સ શબ્દાર્થ અર્થ અથવા વર્તનનો સંદર્ભ આપે છે. બીજગણિત સ્પષ્ટીકરણ પ્રશ્નમાં ઑબ્જેક્ટનો અર્થ અને વર્તન બંને પ્રદાન કરે છે. સમીકરણ સ્વયંસિદ્ધ બીજગણિત સ્પષ્ટીકરણોના શબ્દાર્થને શરતી સમીકરણોના સ્વરૂપમાં સ્વયંસિદ્ધ દ્વારા વ્યાખ્યાયિત કરવામાં આવે છે. પૂર્ણાંક સ્ટેક્સની સહીના સંદર્ભમાં, આપણી પાસે નીચેના સ્વયંસિદ્ધ સિદ્ધાંતો છેઃ કોઈપણ માટે અને, જ્યાં "" સૂચવે છે "" મળ્યું નથી ". ગાણિતિક સિમેન્ટિક્સ સ્પષ્ટીકરણનું ગાણિતિક સિમેન્ટિક્સ (જેને ડેનોટેશનલ સિમેન્ટિક્સ તરીકે પણ ઓળખવામાં આવે છે) તેના ગાણિતિક અર્થનો સંદર્ભ આપે છે. બીજગણિત સ્પષ્ટીકરણનું ગાણિતિક શબ્દાર્થ એ તમામ બીજગણિતનો વર્ગ છે જે સ્પષ્ટીકરણને સંતોષે છે. ખાસ કરીને, ગોગુએન એટ અલ દ્વારા ક્લાસિક અભિગમ. પ્રારંભિક બીજગણિત (આઇસોમોર્ફિઝમ સુધી અનન્ય) ને બીજગણિત સ્પષ્ટીકરણના "સૌથી પ્રતિનિધિ" મોડેલ તરીકે લે છે. ઓપરેશનલ સિમેન્ટિક્સ સ્પષ્ટીકરણના ઓપરેશનલ સિમેન્ટિક્સનો અર્થ એ છે કે તેને કોમ્પ્યુટેશનલ પગલાઓના ક્રમ તરીકે કેવી રીતે અર્થઘટન કરવું. આપણે મૂળભૂત પદને ચલ વિનાના બીજગણિત અભિવ્યક્તિ તરીકે વ્યાખ્યાયિત કરીએ છીએ. બીજગણિત સ્પષ્ટીકરણના કાર્યકારી શબ્દાર્થનો સંદર્ભ એ છે કે જ્યાં સુધી આવા શબ્દો તેમના સામાન્ય સ્વરૂપો સુધી ન પહોંચે ત્યાં સુધી, જ્યાં સુધી વધુ પુનર્લેખન શક્ય ન હોય ત્યાં સુધી, ડાબેથી જમણે પુનર્લેખન નિયમો તરીકે આપેલા સમતુલ્ય સ્વયંસિદ્ધ શબ્દોનો ઉપયોગ કરીને પાયાના શબ્દોને કેવી રીતે રૂપાંતરિત કરી શકાય છે. પૂર્ણાંક સ્ટેક્સ માટે સ્વયંસિદ્ધોનો વિચાર કરો. ચાલો 'ડીનોટ' ને ફરીથી લખીએ. કેનોનિકલ પ્રોપર્ટી બીજગણિત સ્પષ્ટીકરણને કોન્ફ્લુઅન્ટ (ચર્ચ-રોઝર તરીકે પણ ઓળખાય છે) કહેવામાં આવે છે જો કોઈ પણ ગ્રાઉન્ડ ટર્મનું પુનર્લેખન સમાન સામાન્ય સ્વરૂપ તરફ દોરી જાય છે. જો કોઈ ગ્રાઉન્ડ ટર્મનું પુનર્લેખન મર્યાદિત સંખ્યામાં પગલાં પછી સામાન્ય સ્વરૂપ તરફ દોરી જશે તો તે સમાપ્ત થઈ રહ્યું હોવાનું કહેવાય છે. બીજગણિત સ્પષ્ટીકરણને કેનોનિકલ (કન્વર્જન્ટ તરીકે પણ ઓળખાય છે) કહેવામાં આવે છે જો તે સંમિશ્રિત અને સમાપ્ત થતું હોય. બીજા શબ્દોમાં કહીએ તો, જો કોઈ પણ પાયાના પદનું પુનર્લેખન મર્યાદિત સંખ્યામાં પગલાં પછી અનન્ય સામાન્ય સ્વરૂપ તરફ દોરી જાય તો તે પ્રમાણભૂત છે. કોઈપણ કેનોનિકલ બીજગણિત સ્પષ્ટીકરણને જોતાં, ગાણિતિક સિમેન્ટિક્સ ઓપરેશનલ સિમેન્ટિક્સ સાથે સહમત થાય છે. પરિણામે, કાર્યક્રમની ચોકસાઈના મુદ્દાઓને સંબોધવા માટે કેનોનિકલ બીજગણિત સ્પષ્ટીકરણો વ્યાપકપણે લાગુ કરવામાં આવ્યા છે. ઉદાહરણ તરીકે, અસંખ્ય સંશોધકોએ ઓબ્જેક્ટ-ઓરિએન્ટેડ પ્રોગ્રામિંગમાં ઓબ્જેક્ટ્સની નિરીક્ષણ સમાનતાના પરીક્ષણ માટે આવા સ્પષ્ટીકરણો લાગુ કર્યા છે. ચેન અને ત્સેને ગૌણ સ્રોત તરીકે જુઓ જે 1981 થી 2013 સુધીના અગ્રણી સંશોધનની ઐતિહાસિક સમીક્ષા પ્રદાન કરે છે. બીજગણિત શબ્દાર્થ (ગાણિતિક તર્ક) OBJ (પ્રોગ્રામિંગ ભાષા) જોસેફ ગોગુએન સંદર્ભો ઔપચારિક પદ્ધતિઓ કમ્પ્યુટર વિજ્ઞાનમાં તર્ક ઔપચારિક સ્પષ્ટીકરણ ભાષાઓ પ્રોગ્રામિંગ ભાષા શબ્દાર્થ