Lambda-mu calculus
গাণিতিক যুক্তি এবং কম্পিউটার বিজ্ঞানে, ল্যাম্বডা-মু ক্যালকুলাস হল মিশেল প্যারিগট দ্বারা প্রবর্তিত ল্যাম্বডা ক্যালকুলাসের একটি সম্প্রসারণ। এটি দুটি নতুন অপারেটর প্রবর্তন করেঃ এমইউ অপারেটর (যা গণনাযোগ্যতা তত্ত্বে পাওয়া এমইউ অপারেটর এবং মডেল এমইউ-ক্যালকুলাসের এমইউ অপারেটর থেকে সম্পূর্ণ আলাদা) এবং বন্ধনী অপারেটর। প্রমাণ-তাত্ত্বিকভাবে, এটি শাস্ত্রীয় প্রাকৃতিক অনুমানের একটি ভাল আচরণের সূত্র প্রদান করে। এই বর্ধিত গণনার অন্যতম প্রধান লক্ষ্য হল শাস্ত্রীয় যুক্তিতে উপপাদ্যের সাথে সম্পর্কিত অভিব্যক্তিগুলি বর্ণনা করতে সক্ষম হওয়া। কারি-হাওয়ার্ড সমরূপতা অনুসারে, ল্যাম্বডা ক্যালকুলাস নিজেই কেবল স্বজ্ঞাত যুক্তিতে উপপাদ্য প্রকাশ করতে পারে এবং বেশ কয়েকটি শাস্ত্রীয় যৌক্তিক উপপাদ্য মোটেও লেখা যায় না। তবে এই নতুন অপারেটরদের সাথে কেউ এমন পদ লিখতে সক্ষম হয় যার ধরণ রয়েছে, উদাহরণস্বরূপ, পিয়ার্সের সূত্র। শব্দার্থগতভাবে এই অপারেটরগুলি ধারাবাহিকতার সাথে সামঞ্জস্যপূর্ণ, যা কিছু কার্যকরী প্রোগ্রামিং ভাষায় পাওয়া যায়। আনুষ্ঠানিক সংজ্ঞা আমরা ল্যাম্বডা-মু ক্যালকুলাসের প্রসঙ্গে একটি লাভ করার জন্য একটি ল্যাম্বডা অভিব্যক্তিটির সংজ্ঞা বৃদ্ধি করতে পারি। ল্যাম্বডা ক্যালকুলাসে পাওয়া তিনটি প্রধান অভিব্যক্তি নিম্নরূপঃ, একটি পরিবর্তনশীল, যেখানে V হল যে কোনও শনাক্তকারী। একটি বিমূর্ততা, যেখানে V হল যে কোনও শনাক্তকারী এবং E হল যে কোনও ল্যাম্বডা অভিব্যক্তি। , একটি অ্যাপ্লিকেশন, যেখানে ই এবং ই '; যে কোনও ল্যাম্বডা এক্সপ্রেশন। বিস্তারিত জানার জন্য, সংশ্লিষ্ট নিবন্ধটি দেখুন। ঐতিহ্যবাহী λ-ভেরিয়েবল ছাড়াও, ল্যাম্বডা-মু ক্যালকুলাসে মাইক্রো-ভেরিয়েবলের একটি স্বতন্ত্র সেট রয়েছে। এই মাইক্রো-ভেরিয়েবলগুলি নির্বিচারে সাবটার্মগুলির নাম বা হিমায়িত করতে ব্যবহার করা যেতে পারে, যা আমাদের পরে সেই নামগুলি বিমূর্ত করার অনুমতি দেয়। শব্দের সেটটিতে নামহীন (সমস্ত ঐতিহ্যবাহী ল্যাম্বডা অভিব্যক্তি এই ধরনের) এবং নামযুক্ত পদ রয়েছে। ল্যাম্বডা-মু ক্যালকুলাস দ্বারা যে পদগুলি যুক্ত করা হয় সেগুলি এই ফর্মেরঃ এটি একটি নামযুক্ত শব্দ, যেখানে α একটি μ-পরিবর্তনশীল এবং t একটি নামহীন শব্দ। একটি নামহীন শব্দ, যেখানে α একটি μ-পরিবর্তনশীল এবং E "একটি নামযুক্ত শব্দ। হ্রাস ল্যাম্বডা-মু ক্যালকুলাসে ব্যবহৃত মৌলিক হ্রাসের নিয়মগুলি নিম্নরূপঃ যৌক্তিক হ্রাস কাঠামোগত হ্রাস η-হ্রাসের সমতুল্য নামকরণ করে, কারণ α মুক্তভাবে u-তে ঘটে না এই নিয়মগুলি ক্যালকুলাসকে সংহত করে। আরও হ্রাসের নিয়মগুলি যোগ করা যেতে পারে যাতে আমাদের স্বাভাবিক রূপের একটি শক্তিশালী ধারণা প্রদান করা যায়, যদিও এটি সঙ্গমের ব্যয়ে হবে। এছাড়াও দেখুন নিয়ন্ত্রণ রেফারেন্স সহ ল্যাম্বডা ক্যালকুলির টাইপ করা সাধারণীকরণের জন্য ধ্রুপদী বিশুদ্ধ টাইপ সিস্টেম বাহ্যিক লিঙ্ক ল্যাম্বডা-মু ল্যাম্বডা দ্য আলটিমেট সম্পর্কিত প্রাসঙ্গিক আলোচনা। ল্যাম্বডা ক্যালকুলাস প্রমাণ তত্ত্ব