Lambda-mu calculus
ગાણિતિક તર્કશાસ્ત્ર અને કોમ્પ્યુટર વિજ્ઞાનમાં, લેમ્બડા-મુ કલનશાસ્ત્ર એ મિશેલ પેરિગોટ દ્વારા રજૂ કરાયેલા લેમ્બડા કલનશાસ્ત્રનું વિસ્તરણ છે. તે બે નવા ઓપરેટરોની રજૂઆત કરે છેઃ એમયુ ઓપરેટર (જે ગણતરી સિદ્ધાંતમાં જોવા મળતા એમયુ ઓપરેટર અને મોડલ એમયુ-કેલ્ક્યુલસના એમયુ ઓપરેટર બંનેથી સંપૂર્ણપણે અલગ છે) અને કૌંસ ઓપરેટર. પુરાવો-સૈદ્ધાંતિક રીતે, તે શાસ્ત્રીય કુદરતી કપાતની સારી વર્તણૂકની રચના પ્રદાન કરે છે. આ વિસ્તૃત કલનનું એક મુખ્ય લક્ષ્ય શાસ્ત્રીય તર્કમાં પ્રમેયોને અનુરૂપ અભિવ્યક્તિઓનું વર્ણન કરવામાં સક્ષમ બનવું છે. કરી-હોવર્ડ આઇસોમોર્ફિઝમ અનુસાર, લેમ્બડા કેલ્ક્યુલસ તેના પોતાના પર માત્ર અંતઃપ્રેરણાત્મક તર્કમાં પ્રમેયોને વ્યક્ત કરી શકે છે, અને કેટલાક શાસ્ત્રીય તાર્કિક પ્રમેયો બિલકુલ લખી શકાતા નથી. જો કે આ નવા ઓપરેટરો સાથે કોઈ એવા શબ્દો લખી શકે છે જેનો પ્રકાર હોય છે, ઉદાહરણ તરીકે, પીયર્સનો નિયમ. અર્થપૂર્ણ રીતે આ ઓપરેટરો કેટલાક કાર્યાત્મક પ્રોગ્રામિંગ ભાષાઓમાં જોવા મળતા સાતત્યને અનુરૂપ છે. ઔપચારિક વ્યાખ્યા આપણે લેમ્બડા-મુ કલનનાં સંદર્ભમાં એક મેળવવા માટે લેમ્બડા અભિવ્યક્તિની વ્યાખ્યામાં વધારો કરી શકીએ છીએ. લેમ્બડા કલનમાં જોવા મળતી ત્રણ મુખ્ય અભિવ્યક્તિઓ નીચે મુજબ છેઃ, એક ચલ, જ્યાં V એ કોઈપણ ઓળખકર્તા છે. એક એબ્સ્ટ્રેક્શન, જ્યાં V એ કોઈપણ ઓળખકર્તા છે અને E એ કોઈપણ લેમ્બડા અભિવ્યક્તિ છે. , એક એપ્લિકેશન, જ્યાં E અને E '; કોઈપણ લેમ્બડા અભિવ્યક્તિઓ છે. વિગતો માટે, સંબંધિત લેખ જુઓ. પરંપરાગત λ-ચલ ઉપરાંત, લેમ્બડા-મુ કલનમાં μ-ચલોનો એક અલગ સમૂહ સામેલ છે. આ μ-ચલોનો ઉપયોગ મનસ્વી પેટા શબ્દોને નામ આપવા અથવા સ્થિર કરવા માટે થઈ શકે છે, જે આપણને પછીથી તે નામો પર અમૂર્ત કરવાની મંજૂરી આપે છે. શબ્દોના સમૂહમાં અનામી (તમામ પરંપરાગત લેમ્બડા અભિવ્યક્તિઓ આ પ્રકારની છે) અને નામવાળી શરતો છે. લેમ્બડા-મુ કલન દ્વારા જે શબ્દો ઉમેરવામાં આવે છે તે આ સ્વરૂપના હોય છેઃ તે એક નામાંકિત શબ્દ છે, જ્યાં α એ μ-ચલ છે અને t એ અનામી શબ્દ છે. આ એક અનામી શબ્દ છે, જ્યાં α એ μ-ચલ છે અને E "એ એક નામાંકિત શબ્દ છે. ઘટાડો લેમ્બડા-મુ કલનમાં ઉપયોગમાં લેવાતા મૂળભૂત ઘટાડાના નિયમો નીચે મુજબ છેઃ તાર્કિક ઘટાડાના માળખાકીય ઘટાડાને η-ઘટાડાની સમકક્ષ નામ આપવામાં આવ્યું છે, કારણ કે α મુક્તપણે u માં થતું નથી. આપણને સામાન્ય સ્વરૂપની મજબૂત કલ્પના પ્રદાન કરવા માટે વધુ ઘટાડાના નિયમો ઉમેરી શકાય છે, જો કે આ સંગમના ભોગે હશે. નિયંત્રણ સંદર્ભો સાથે લામ્બડા કલ્કુલીના ટાઇપ કરેલ સામાન્યીકરણ માટે શાસ્ત્રીય શુદ્ધ પ્રકારની પ્રણાલીઓ પણ જુઓ બાહ્ય લિંક્સ લામ્બડા-મુ લામ્બડા ધ અલ્ટીમેટ પર સંબંધિત ચર્ચા. લેમ્બડા કલન પુરાવો સિદ્ધાંત