De Bruijn index
গাণিতিক যুক্তিতে, ডি ব্রুইন সূচক হল ডাচ গণিতবিদ নিকোলাস গোভার্ট ডি ব্রুইন দ্বারা উদ্ভাবিত একটি সরঞ্জাম যা আবদ্ধ চলকগুলির নামকরণ না করে ল্যাম্বডা ক্যালকুলাসের পদগুলির প্রতিনিধিত্ব করে। এই সূচকগুলি ব্যবহার করে লেখা পদগুলি α-রূপান্তরের ক্ষেত্রে অপরিবর্তনীয়, তাই α-সমতুল্যতার জন্য চেক বাক্যবিন্যাসগত সমতার জন্য একই। প্রতিটি ডি ব্রুইন সূচক একটি প্রাকৃতিক সংখ্যা যা একটি λ-মেয়াদে একটি পরিবর্তনশীলের ঘটনার প্রতিনিধিত্ব করে এবং সেই ঘটনা এবং তার সংশ্লিষ্ট বাঁধাইয়ের মধ্যে সুযোগ থাকা বাঁধাইয়ের সংখ্যাকে নির্দেশ করে। নিম্নলিখিত কয়েকটি উদাহরণ রয়েছেঃ λx শব্দটি। λy x, যাকে কখনও কখনও কে কম্বিনেটর বলা হয়, ডি ব্রুইন সূচকগুলির সাথে λλ2 হিসাবে লেখা হয়। ঘটনা x-এর বাইন্ডার হল দ্বিতীয় λ। λx শব্দটি। λy λz। ডি ব্রুইজন সূচকের সঙ্গে xz (yz) (এস সমন্বয়কারী) হল λλλ31 (211)। λz শব্দটি। (λy। y (λx। x)) (λx। z x) হল λ (λ1 (λ1)) (λ21)। নিচের চিত্রটি দেখুন, যেখানে বাঁধাগুলি রঙিন এবং উল্লেখগুলি তীর দিয়ে দেখানো হয়েছে। ডি ব্রুইন সূচকগুলি সাধারণত স্বয়ংক্রিয় উপপাদ্য প্রোভার এবং লজিক প্রোগ্রামিং সিস্টেমের মতো উচ্চ-ক্রমের যুক্তি ব্যবস্থায় ব্যবহৃত হয়। আনুষ্ঠানিক সংজ্ঞা আনুষ্ঠানিকভাবে, ডি ব্রুইন সূচক ব্যবহার করে লেখা λ-শব্দের (এম, এন,.) নিম্নলিখিত বাক্যবিন্যাস রয়েছে (বন্ধনীগুলি অবাধে অনুমোদিত): এম, এন,: = এন। এম এন। λ এম যেখানে এন-0 এর চেয়ে বড় প্রাকৃতিক সংখ্যা-হল চলক। একটি পরিবর্তনশীল n আবদ্ধ হয় যদি এটি কমপক্ষে n বাইন্ডার (λ) এর আওতায় থাকে; অন্যথায় এটি মুক্ত। একটি পরিবর্তনশীল n-এর জন্য বাঁধাই সাইট হল nতম বাঁধাই যা এর আওতায় রয়েছে, সবচেয়ে ভিতরের বাঁধাই থেকে শুরু করে। λ-শব্দের সবচেয়ে আদিম ক্রিয়া হল প্রতিস্থাপনঃ একটি শব্দের মুক্ত চলককে অন্যান্য শব্দের সাথে প্রতিস্থাপন করা। উদাহরণস্বরূপ, β-হ্রাস (λM) N-এ, আমাদের অবশ্যই চলক n1, n2,., m-এ nk-এর উদাহরণগুলি খুঁজে বের করতে হবে যা λM-এ λ দ্বারা আবদ্ধ, বাইরের λ-বাইন্ডার অপসারণের সাথে মেলে M-এর মুক্ত চলকগুলি হ্রাস করুন, এবং n1, n2,., nk-কে N-এর সাথে প্রতিস্থাপন করুন, প্রতিবার N-এ ঘটে যাওয়া মুক্ত চলকগুলি যথাযথভাবে বৃদ্ধি করুন, λ-বাইন্ডারের সংখ্যার সাথে মেলে, যার অধীনে সংশ্লিষ্ট চলকটি ঘটে যখন N একটির জন্য প্রতিস্থাপন করে। উদাহরণস্বরূপ, প্রয়োগ (λλ42 (λ13)) (λ51) বিবেচনা করুন যা সাধারণ স্বরলিপিতে (λx) লেখা নিম্নলিখিত শব্দের সাথে সামঞ্জস্যপূর্ণ হতে পারে। λy z x (λu। u x)) (λx। ডাব্লু এক্স)। প্রথম ধাপের পরে, আমরা λ4· (λ1·) শব্দটি পাই, যেখানে প্রতিস্থাপনের জন্য নির্ধারিত চলকগুলি বাক্স দ্বারা প্রতিস্থাপিত হয়। দ্বিতীয় ধাপটি মুক্ত চলকগুলিকে হ্রাস করে λ3⁄2 (λ1⁄2) দেয়। অবশেষে, ধাপ 3-এ, আমরা বাক্সগুলিকে আর্গুমেন্ট দিয়ে প্রতিস্থাপন করি, যথা λ51; প্রথম বাক্সটি একটি বাইন্ডারের অধীনে, তাই আমরা এটিকে λ61 দিয়ে প্রতিস্থাপন করি (যা λ51 এবং মুক্ত চলকগুলি 1 দ্বারা বৃদ্ধি করা হয়); দ্বিতীয়টি দুটি বাইন্ডারের অধীনে, তাই আমরা এটিকে λ71 দিয়ে প্রতিস্থাপন করি। চূড়ান্ত ফলাফল হল λ3 (λ61) (λ1 (λ71))। আনুষ্ঠানিকভাবে, একটি প্রতিস্থাপন হ 'ল M1.M2 লেখা পদগুলির একটি সীমাহীন তালিকা, যেখানে এমআই হ' ল মুক্ত চলকের প্রতিস্থাপন। ধাপ 3-এ ক্রমবর্ধমান ক্রিয়াকলাপকে কখনও কখনও শিফট বলা হয় এবং কে লেখা হয় যেখানে কে একটি প্রাকৃতিক সংখ্যা যা চলক বাড়ানোর পরিমাণ নির্দেশ করে এবং দ্বারা সংজ্ঞায়িত করা হয়। উদাহরণস্বরূপ, 0 হল পরিচয় প্রতিস্থাপন, একটি শব্দ অপরিবর্তিত রেখে। M1.M2.Mn শব্দের একটি সীমাবদ্ধ তালিকা বিকল্প M1.M2.Mn. (n + 1). (n + 2) কে সংক্ষিপ্ত করে। n-এর চেয়ে বড় সমস্ত চলক অপরিবর্তিত রেখে। একটি 'এম' শব্দের পরিবর্তে 'এস'-এর প্রয়োগ 'এম' [এস] লেখা হয়। দুটি প্রতিস্থাপন s1 এবং s2-এর গঠন s1s2 লেখা হয় এবং (M1.M2) s = M1 [s]. M2 [s] দ্বারা সংজ্ঞায়িত করা হয়. বৈশিষ্ট্য M [s1s2] = (M [s1]) [s2] সন্তুষ্ট করে, এবং প্রতিস্থাপন নিম্নরূপ পদগুলিতে সংজ্ঞায়িত করা হয়ঃ উপরের β-হ্রাসের জন্য বর্ণিত পদক্ষেপগুলি এইভাবে আরও সংক্ষিপ্তভাবে প্রকাশ করা হয়ঃ (λM) N → βM [N]। ডি ব্রুইন সূচকের বিকল্পগুলি λ-শব্দের মানক "নামযুক্ত" উপস্থাপনা ব্যবহার করার সময়, যেখানে চলকগুলিকে লেবেল বা স্ট্রিং হিসাবে বিবেচনা করা হয়, শর্তাবলীতে কোনও ক্রিয়াকলাপ সংজ্ঞায়িত করার সময় একজনকে অবশ্যই স্পষ্টভাবে α-রূপান্তর পরিচালনা করতে হবে। বাস্তবে এটি জটিল, অদক্ষ এবং প্রায়শই ত্রুটি-প্রবণ। তাই এটি এই ধরনের শব্দের বিভিন্ন উপস্থাপনা অনুসন্ধানের দিকে পরিচালিত করেছে। অন্যদিকে, λ-শব্দের নামযুক্ত উপস্থাপনা আরও বিস্তৃত এবং অন্যরা আরও অবিলম্বে বুঝতে পারে কারণ চলকগুলিকে বর্ণনামূলক নাম দেওয়া যেতে পারে। সুতরাং, এমনকি যদি কোনও সিস্টেম অভ্যন্তরীণভাবে ডি ব্রুইন সূচক ব্যবহার করে, তবে এটি নাম সহ একটি ব্যবহারকারী ইন্টারফেস উপস্থাপন করবে। ডি ব্রুইন সূচকগুলি দেখার একটি বিকল্প উপায় হল ডি ব্রুইন স্তর, যা উপরের পরিবর্তে স্ট্যাকের নীচে থেকে ভেরিয়েবলগুলিকে সূচীভুক্ত করে। এটি রিইনডেক্স মুক্ত চলকগুলির প্রয়োজনীয়তা দূর করে, উদাহরণস্বরূপ প্রসঙ্গকে দুর্বল করার সময়, যেখানে ডি ব্রুইন সূচকগুলি রিইনডেক্স আবদ্ধ চলকগুলির প্রয়োজনীয়তা দূর করে, উদাহরণস্বরূপ অন্য প্রসঙ্গে একটি বদ্ধ অভিব্যক্তি প্রতিস্থাপনের সময়। ডি ব্রুইন সূচকগুলি λ-শব্দের একমাত্র উপস্থাপনা নয় যা α-রূপান্তরের সমস্যাকে দূর করে। নামযুক্ত উপস্থাপনাগুলির মধ্যে, পিটস এবং গ্যাবের নামমাত্র কৌশলগুলি একটি পদ্ধতি, যেখানে একটি λ-শব্দের উপস্থাপনাকে পরিবর্তনশীল বিন্যাস ব্যবহার করে এটির সাথে পুনর্লিখনযোগ্য সমস্ত শব্দের সমতুল্য শ্রেণী হিসাবে বিবেচনা করা হয়। এই পদ্ধতিটি ইসাবেল/এইচওএল-এর নোমিনাল ডেটাটাইপ প্যাকেজ দ্বারা নেওয়া হয়। আরেকটি সাধারণ বিকল্প হল উচ্চ-ক্রমের উপস্থাপনার আবেদন যেখানে λ-বাইন্ডারকে একটি সত্যিকারের ফাংশন হিসাবে বিবেচনা করা হয়। এই ধরনের উপস্থাপনায়, α-সমতুল্যতা, প্রতিস্থাপন ইত্যাদির বিষয়গুলি। একটি মেটা-লজিক-এ একই ক্রিয়াকলাপের সাথে চিহ্নিত করা হয়। প্রুফ অ্যাসিস্ট্যান্ট-এ কোনও ডিডাকটিভ সিস্টেমের মেটা-থিওরেটিক বৈশিষ্ট্য সম্পর্কে যুক্তি করার সময়, কখনও কখনও নিজেকে প্রথম-ক্রমের উপস্থাপনায় সীমাবদ্ধ রাখা এবং অনুমানের নাম বা নাম পরিবর্তনের ক্ষমতা থাকা বাঞ্ছনীয়। স্থানীয়ভাবে নামহীন পদ্ধতিটি চলকগুলির একটি মিশ্র উপস্থাপনা ব্যবহার করে-আবদ্ধ চলকগুলির জন্য ডি ব্রুইন সূচক এবং মুক্ত চলকগুলির জন্য নাম-যা উপযুক্ত হলে ডি ব্রুইন সূচকযুক্ত পদগুলির α-ক্যানোনিকাল ফর্ম থেকে উপকৃত হতে সক্ষম। ব্যারেন্ড্রেগের পরিবর্তনশীল কনভেনশন হল একটি কনভেনশন যা সাধারণত প্রমাণ এবং সংজ্ঞাগুলিতে ব্যবহৃত হয় যেখানে এটি ধরে নেওয়া হয় যেঃ আবদ্ধ ভেরিয়েবলগুলি মুক্ত ভেরিয়েবল থেকে আলাদা, এবং সমস্ত বাইন্ডার ভেরিয়েবলগুলিকে আবদ্ধ করে যা ইতিমধ্যে সুযোগে নেই। একটি ইন্ডাক্টিভ সংজ্ঞার সাধারণ প্রসঙ্গে, কনভেনশন ব্যবহার করে একটি ইন্ডাক্টিভ সংজ্ঞাকে যেখানে কনভেনশন ব্যবহার করা হয় না সেখানে রূপান্তর করার জন্য প্রয়োজনীয় α-রূপান্তর প্রয়োগ করা সম্ভব নয়, কারণ একটি পরিবর্তনশীল একটি বাঁধাই অবস্থানে এবং নিয়মে একটি অ-বাঁধাই অবস্থানে উভয়ই উপস্থিত হতে পারে। যদি প্রতিটি নিয়ম নিম্নলিখিত দুটি শর্ত পূরণ করেঃ নিয়মটি নামমাত্র যুক্তির অর্থে সমতুল্য, অর্থাৎ নিয়মের প্রাঙ্গণ ধরে নিয়ে ভেরিয়েবলগুলির নাম পরিবর্তন করে এর বৈধতা অপরিবর্তিত থাকে, নিয়মে বাঁধাই অবস্থানের ভেরিয়েবলগুলি স্বতন্ত্র এবং উপসংহারে মুক্ত λ-পদগুলির জন্য ডি ব্রুইন নোটেশন দেখুন। সমন্বিত যুক্তি, পরিবর্তনশীল নামগুলি বাদ দেওয়ার একটি আরও প্রয়োজনীয় উপায়। তথ্যসূত্র ল্যাম্বডা ক্যালকুলাস