Lambda-mu calculus
ریاضیاتی منطق اور کمپیوٹر سائنس میں، لیمبڈا-مو کیلکولس مائیکل پیریگوٹ کے متعارف کردہ لیمبڈا کیلکولس کی توسیع ہے۔ یہ دو نئے آپریٹرز متعارف کراتا ہے: ایم یو آپریٹر (جو کمپیوٹیبلٹی تھیوری میں پائے جانے والے ایم یو آپریٹر اور موڈل ایم یو کیلکولس کے ایم یو آپریٹر دونوں سے بالکل مختلف ہے) اور بریکٹ آپریٹر۔ ثبوت-نظریاتی طور پر، یہ کلاسیکی قدرتی کٹوتی کی ایک اچھی طرز عمل کی تشکیل فراہم کرتا ہے۔ اس توسیعی حساب کے اہم مقاصد میں سے ایک کلاسیکی منطق میں نظریات سے مطابقت رکھنے والے تاثرات کو بیان کرنے کے قابل ہونا ہے۔ کری-ہاورڈ آئسومورفزم کے مطابق، لیمبڈا کیلکولس اپنے طور پر تھیوریمز کو صرف بدیہی منطق میں ظاہر کر سکتا ہے، اور کئی کلاسیکی منطقی تھیوریمز بالکل نہیں لکھے جا سکتے۔ تاہم ان نئے آپریٹرز کے ساتھ کوئی بھی ایسی اصطلاحات لکھنے کے قابل ہوتا ہے جن کی قسم ہوتی ہے، مثال کے طور پر، پیئرس کا قانون۔ لفظی طور پر یہ آپریٹرز تسلسل سے مطابقت رکھتے ہیں، جو کچھ فعال پروگرامنگ زبانوں میں پائے جاتے ہیں۔ رسمی تعریف ہم لیمبڈا-مو کیلکولس کے تناظر میں ایک حاصل کرنے کے لیے لیمبڈا اظہار کی تعریف کو بڑھا سکتے ہیں۔ لیمبڈا کیلکولس میں پائے جانے والے تین اہم تاثرات مندرجہ ذیل ہیں:، ایک متغیر، جہاں V کوئی شناخت کنندہ ہے۔ ایک تجریدی، جہاں V کوئی شناخت کنندہ ہے اور E کوئی لیمبڈا اظہار ہے۔ ، ایک ایپلی کیشن، جہاں E اور E "؛ کوئی بھی لیمبڈا تاثرات ہیں۔ تفصیلات کے لیے متعلقہ مضمون دیکھیں۔ روایتی λ-متغیرات کے علاوہ، لیمبڈا-مو کیلکولس میں μ-متغیرات کا ایک الگ مجموعہ شامل ہے۔ یہ μ-متغیرات صوابدیدی ذیلی اصطلاحات کو نام دینے یا منجمد کرنے کے لیے استعمال کیے جا سکتے ہیں، جس سے ہمیں بعد میں ان ناموں پر خلاصہ کرنے کا موقع ملتا ہے۔ اصطلاحات کے سیٹ میں بے نام (تمام روایتی لیمبڈا تاثرات اس قسم کے ہیں) اور نامزد اصطلاحات شامل ہیں۔ لیمبڈا-مو کیلکولس کے ذریعہ جو اصطلاحات شامل کی جاتی ہیں وہ اس شکل کی ہوتی ہیں: یہ ایک نامزد اصطلاح ہے، جہاں α ایک μ-متغیر ہے اور t ایک نامعلوم اصطلاح ہے۔ ایک نامعلوم اصطلاح ہے، جہاں α ایک μ-متغیر ہے اور E "ایک نامزد اصطلاح ہے۔ لیمبڈا-مو کیلکولس میں استعمال ہونے والے بنیادی تخفیف کے اصول درج ذیل ہیں: منطقی تخفیف ساختی تخفیف کا نام بدل کر η-کمی کے مساوی رکھا گیا ہے، کیونکہ α آزادانہ طور پر u میں نہیں ہوتا ہے۔ یہ اصول کیلکولس کو متصل ہونے کا سبب بنتے ہیں۔ ہمیں عام شکل کا مضبوط تصور فراہم کرنے کے لیے مزید تخفیف کے قوانین شامل کیے جا سکتے ہیں، حالانکہ یہ سنگم کی قیمت پر ہوگا۔ کنٹرول حوالہ جات کے ساتھ لیمبڈا کیلکولی کی ٹائپ شدہ عمومی کاری کے لیے کلاسیکی خالص قسم کے نظام بھی دیکھیں بیرونی لنکس لیمبڈا-مو لیمبڈا دی الٹیمیٹ پر متعلقہ بحث۔ لیمبڈا کیلکولس ثبوت نظریہ