De Bruijn notation
গাণিতিক যুক্তিতে, ডি ব্রুইন স্বরলিপি হল ডাচ গণিতবিদ নিকোলাস গোভার্ট ডি ব্রুইন দ্বারা উদ্ভাবিত λ ক্যালকুলাসের পদগুলির একটি বাক্যবিন্যাস। এটি λ ক্যালকুলাসের জন্য স্বাভাবিক বাক্যবিন্যাসের বিপরীত হিসাবে দেখা যেতে পারে যেখানে একটি অ্যাপ্লিকেশনের আর্গুমেন্টটি পরবর্তীটির মূল অংশের পরিবর্তে ফাংশনে তার সংশ্লিষ্ট বাইন্ডারের পাশে স্থাপন করা হয়। আনুষ্ঠানিক সংজ্ঞা ডি ব্রুইন স্বরলিপিতে শর্তাবলী () হয় চলক (), অথবা দুটি ওয়াগনের উপসর্গের মধ্যে একটি থাকে। বিমূর্ত ওয়াগন, লিখিত, λ ক্যালকুলাসের স্বাভাবিক λ-বাইন্ডারের সাথে মিলে যায় এবং আবেদনকারী ওয়াগন, লিখিত, λ ক্যালকুলাসের একটি অ্যাপ্লিকেশনের যুক্তির সাথে মিলে যায়। ঐতিহ্যবাহী বাক্যবিন্যাসের পদগুলি একটি ইন্ডাক্টিভ ফাংশন সংজ্ঞায়িত করে ডি ব্রুইন নোটেশনে রূপান্তরিত করা যেতে পারে যার জন্যঃ অনুবাদের ক্ষেত্রে λ-শব্দের সমস্ত ক্রিয়াকলাপ যাতায়াত করে। উদাহরণস্বরূপ, ডি ব্রুইন স্বরলিপিতে স্বাভাবিক β-হ্রাস হল, অনুমানযোগ্যভাবে, এই স্বরলিপির একটি বৈশিষ্ট্য হল যে β-রিডেক্সের বিমূর্ত এবং প্রয়োগকারী ওয়াগনগুলি বন্ধনীর মতো জোড়া দেওয়া হয়। উদাহরণস্বরূপ, শব্দের β-হ্রাসের পর্যায়গুলি বিবেচনা করুন, যেখানে রিডেক্সগুলি আন্ডারলাইন করা হয়েছেঃ সুতরাং, যদি কেউ আবেদনকারীকে একটি খোলা প্যারেন্ট ('(') এবং বিমূর্তটিকে একটি ঘনিষ্ঠ বন্ধনী (']') হিসাবে দেখেন, তবে উপরের শব্দের প্যাটার্নটি হল '((] (])'। ডি ব্রুইন এই ব্যাখ্যায় একজন আবেদনকারী এবং তার সংশ্লিষ্ট বিমূর্তকারীকে অংশীদার এবং অংশীদারবিহীন ওয়াগনকে ব্যাচেলর বলে অভিহিত করেন। ওয়াগনগুলির একটি ক্রম, যাকে তিনি একটি বিভাগ বলে অভিহিত করেছিলেন, যদি এর সমস্ত ওয়াগনগুলি অংশীদার হয় তবে তা ভাল ভারসাম্যপূর্ণ। ডি ব্রুইন স্বরলিপির সুবিধাগুলি একটি সুষম বিভাগে, অংশীদার ওয়াগনগুলি নির্বিচারে ঘুরিয়ে দেওয়া যেতে পারে এবং যতক্ষণ সমতা ধ্বংস না হয়, শব্দটির অর্থ একই থাকে। উদাহরণস্বরূপ, উপরের উদাহরণে, আবেদনকারীকে তার বিমূর্তকারী বা বিমূর্তকারীকে আবেদনকারীর কাছে আনা যেতে পারে। প্রকৃতপক্ষে, ল্যাম্বডার শর্তাবলীতে সমস্ত বিনিময় এবং ক্রমবর্ধমান রূপান্তরগুলি কেবল অংশীদার ওয়াগনগুলির সমতা-সংরক্ষণ পুনর্বিন্যাসের পরিপ্রেক্ষিতে বর্ণনা করা যেতে পারে। এইভাবে ডি ব্রুইন স্বরলিপিতে λ-শব্দের জন্য একটি সাধারণ রূপান্তর আদিম পাওয়া যায়। λ-শব্দের বেশ কয়েকটি বৈশিষ্ট্য যা ঐতিহ্যবাহী স্বরলিপি ব্যবহার করে বর্ণনা করা এবং প্রমাণ করা কঠিন, ডি ব্রুইন স্বরলিপিতে সহজেই প্রকাশ করা হয়। উদাহরণস্বরূপ, একটি টাইপ-তাত্ত্বিক পরিবেশে, কেউ সহজেই টাইপিং প্রসঙ্গে একটি শব্দের জন্য ক্যানোনিকাল শ্রেণীর প্রকারগুলি গণনা করতে পারে এবং টাইপ চেকিং সমস্যাটি যাচাই করে যে চেক করা প্রকারটি এই শ্রেণীর সদস্য কিনা তা পুনরায় উল্লেখ করতে পারে। ডি ব্রুইন স্বরলিপি বিশুদ্ধ ধরনের ব্যবস্থায় সুস্পষ্ট প্রতিস্থাপনের জন্য ক্যালকুলিতেও কার্যকর বলে প্রমাণিত হয়েছে। আরও দেখুন গাণিতিক স্বরলিপি রেফারেন্স ল্যাম্বডা ক্যালকুলাস