গুচ্ছবদ্ধ যুক্তি

গুচ্ছবদ্ধ যুক্তি একটি উপ-গঠনমূলক যুক্তির বৈচিত্র্য যা পিটার ও'হার্ন এবং ডেভিড পিম প্রস্তাব করেছিলেন। গুচ্ছবদ্ধ যুক্তি সম্পদ সংমিশ্রণ সম্পর্কে যুক্তি তৈরির জন্য মৌলিক ধারণা প্রদান করে, যা কম্পিউটার এবং অন্যান্য সিস্টেমের উপাদানমূলক বিশ্লেষণে সহায়তা করে। এটি বিভাগ তত্ত্বগত এবং সত্য-ক্রিয়াশীল অর্থবহতা ধারণ করে, যা সম্পদের বিমূর্ত ধারণা দিয়ে ব্যাখ্যা করা যায় এবং এর প্রমাণ তত্ত্বে অনুমেয়তা রায়ের মধ্যে গুচ্ছবদ্ধ কাঠামো (গুচ্ছ) থাকে, যা তালিকা বা (মাল্টি)সেট নয়, যা অধিকাংশ প্রমাণ ক্যালকুলিতে ব্যবহৃত হয়। গুচ্ছবদ্ধ যুক্তি টাইপ তত্ত্ব সম্পর্কিত, এবং এর প্রথম ব্যবহার ছিল আদেশমূলক প্রোগ্রাম এ অ্যালিয়াসিং এবং অন্যান্য প্রকারের হস্তক্ষেপ নিয়ন্ত্রণে।

এই যুক্তি প্রোগ্রাম যাচাইকরণ-এ ব্যবহৃত হয়েছে, যেখানে এটি বিচ্ছিন্ন যুক্তির ঘোষণার ভাষার ভিত্তি, এবং সিস্টেম মডেলিং-এ ব্যবহৃত হয়েছে, যেখানে এটি একটি সিস্টেমের উপাদান দ্বারা ব্যবহৃত সম্পদ বিভাজন করার একটি পদ্ধতি প্রদান করে।

ভিত্তি

ধ্রুপদী যুক্তির উপসংহার তত্ত্ব সংযোজন এবং প্রস্তাবনাকে সম্পর্কিত করে:

$A\wedge B⊢C\text{iff}A⊢B\Rightarrow C$

গুচ্ছবদ্ধ যুক্তিতে উপসংহার তত্ত্বের দুটি সংস্করণ রয়েছে:

$A*B⊢C\text{iff}A⊢B-*C\text{এবং এছাড়াও}A\wedge B⊢C\text{iff}A⊢B\Rightarrow C$

$A*B$ এবং $B-*C$ হল সংযোজন এবং প্রস্তাবনার এমন রূপ যা সম্পদকে বিবেচনায় নেয় (নিচে ব্যাখ্যা করা হয়েছে)। এই যুক্তিতে $\wedge$ এবং $\Rightarrow$ আবর্তনমূলক যুক্তি থেকে গৃহীত, তবে একটি বুলিয়ান বৈকল্পিক বুলিয়ান যুক্তির মতো $\mathrm{\neg }$ অন্তর্ভুক্ত করে। সুতরাং, গুচ্ছবদ্ধ যুক্তি গঠনমূলক নীতিগুলির সাথে সামঞ্জস্যপূর্ণ, তবে এর উপর নির্ভরশীল নয়।

সত্য-ক্রিয়াশীল অর্থবহতা (সম্পদ অর্থবহতা)

এই সূত্রগুলিকে বোঝার সবচেয়ে সহজ উপায় হল এর সত্য-ক্রিয়াশীল অর্থবহতার ক্ষেত্রে। এই অর্থবহতায় একটি সূত্র প্রদত্ত সম্পদের পরিপ্রেক্ষিতে সত্য বা মিথ্যা।

$A*B$ নির্দেশ করে যে প্রদত্ত সম্পদটি $A$ এবং $B$ কে সন্তুষ্টকারী সম্পদে বিভাজিত করা যায়। $B-*C$ নির্দেশ করে যে আমরা যদি প্রদত্ত সম্পদে $B$ কে সন্তুষ্টকারী অতিরিক্ত সম্পদ যোগ করি, তবে মিলিত সম্পদ $C$ কে সন্তুষ্ট করে। $\wedge$ এবং $\Rightarrow$ এর পরিচিত অর্থ রয়েছে।

এই সূত্রগুলির অর্থবোধকতা ডেভিড পিম প্রস্তাবিত একটি forcing semantics $r\models A$ দ্বারা ভিত্তিপ্রাপ্ত, যেখানে $A^{\prime }$ সম্পদ $r^{\prime }$ কে নির্দেশ করে। এই অর্থবোধকতা আবর্তনমূলক যুক্তি বা প্রচলিত যুক্তির ক্রিপকে অর্থবোধকতার সাথে তুলনীয়, তবে মডেলের উপাদানগুলি সম্পদ হিসাবে বিবেচিত হয় যা সংমিশ্রণ এবং বিভাজনের যোগ্য। উদাহরণস্বরূপ, সংযোজনের জন্য forcing semantics হল:

$r\models A*B\text{iff}\mathrm{\exists }{r}_A,r_B.r_A\models A,r_B\models B,\text{এবং}{r}_A\bullet r_B\le r$

যেখানে $r_A\bullet r_B$ সম্পদ সংমিশ্রণের একটি পদ্ধতি এবং $\le$ একটি প্রাক্কলনের সম্পর্ক নির্দেশ করে। এই গুচ্ছবদ্ধ যুক্তির অর্থবোধকতা প্রাসঙ্গিক যুক্তি (বিশেষ করে রাউটলি-মেয়ারের ক্রিয়াত্বক অর্থবোধকতা)র পূর্ববর্তী কাজের উপর ভিত্তি করে তৈরি হয়েছে, তবে এটি থেকে পৃথক কারণ এটি $r\bullet r\le r$ প্রয়োজনীয়তা আরোপ করে না এবং $\wedge$ এবং $\Rightarrow$-এর প্রচলিত আবর্তনমূলক বা ধ্রুপদী যুক্তির অর্থবোধকতা গ্রহণ করে। $r\bullet r\le r$ সম্পত্তি প্রাসঙ্গিকতার ক্ষেত্রে সঙ্গতিপূর্ণ, কিন্তু সম্পদ ব্যবস্থাপনার ক্ষেত্রে এটি অস্বীকার করা হয়; একটি সম্পদের দুটি কপি থাকা একটির সমান নয়, এবং কিছু মডেলে (যেমন হিপ মডেল) $r\bullet r$ সংজ্ঞায়িত নাও হতে পারে। $\Rightarrow$ (বা $\mathrm{\neg }$)-এর প্রচলিত অর্থবোধকতা প্রাসঙ্গিকতাবাদীরা প্রায়ই প্রত্যাখ্যান করেন যাতে 'উপাদানীয় প্রস্তাবনার প্যারাডক্স' থেকে মুক্তি পাওয়া যায়, যা সম্পদ মডেলিংয়ের দৃষ্টিকোণ থেকে কোনো সমস্যা নয় এবং তাই গুচ্ছবদ্ধ যুক্তি এটি প্রত্যাখ্যান করে না। এই অর্থবোধকতা রৈখিক যুক্তির 'পর্বের অর্থবোধকতা'-এর সাথে সম্পর্কিত, তবে $\wedge$ এবং $\Rightarrow$-এর প্রচলিত (এমনকি বুলিয়ান) অর্থবোধকতা গ্রহণ করার মাধ্যমে পৃথক হয়, যা রৈখিক যুক্তিতে প্রত্যাখ্যাত হয় গঠনমূলক থাকার প্রচেষ্টায়। এই বিষয়গুলো পিম, ও'হার্ন এবং ইয়াং এর একটি প্রবন্ধে বিস্তারিত আলোচনা করা হয়েছে।

বিভাগীয় অর্থবোধকতা (দ্বিগুণ বন্ধ বিভাগ)

গুচ্ছবদ্ধ যুক্তির উপসংহার তত্ত্বের দ্বিগুণ সংস্করণটির একটি বিভাগ তত্ত্বগত গঠন রয়েছে। আবর্তনমূলক যুক্তির প্রমাণ কার্টেসিয়ান বন্ধ বিভাগে ব্যাখ্যা করা যায়, যেখানে শেষপ্রান্তে প্রাকৃতিক সংযুক্তি সম্পর্ক বজায় থাকে:

$Hom(A\wedge B,C)\text{is isomorphic to}Hom(A,B\Rightarrow C)$

গুচ্ছবদ্ধ যুক্তি সেই বিভাগে ব্যাখ্যা করা যায় যা দুটি বন্ধ গঠন ধারণ করে:

গুচ্ছবদ্ধ যুক্তির একটি বিভাগীয় মডেল এমন একটি বিভাগ যেখানে একটি সমমিত মনয়ডাল বন্ধ গঠন এবং একটি কার্টেসিয়ান বন্ধ গঠন রয়েছে।

ডে-এর টেনসর গুণফল নির্মাণ ব্যবহার করে বিভিন্ন ধরণের বিভাগীয় মডেল তৈরি করা যেতে পারে।

এছাড়াও, গুচ্ছবদ্ধ যুক্তির প্রস্তাবনা অংশের একটি গেম অর্থবোধকতা রয়েছে।

বীজগাণিতিক অর্থবোধকতা

গুচ্ছবদ্ধ যুক্তির বীজগাণিতিক অর্থবোধকতা তার বিভাগীয় অর্থবোধকতার একটি বিশেষ ক্ষেত্র, তবে এটি সহজভাবে উপস্থাপন করা যায় এবং আরও প্রবেশযোগ্য হতে পারে।

গুচ্ছবদ্ধ যুক্তির একটি বীজগাণিতিক মডেল একটি হেইটিং বীজগাণিতিক অবস্থানতন্ত্র যেখানে একটি সমমিত অবশিষ্টিত জালিকা গঠন (একই জালিকার জন্য) বিদ্যমান। অর্থাৎ, একটি সংযুক্ত ক্রমিক মনয়ড যার সাথে $A*B\le C\text{iff}A\le B-*C$ সম্পর্কিত একটি প্রস্তাবনা রয়েছে।

গুচ্ছবদ্ধ যুক্তির বুলিয়ান সংস্করণের মডেল:

গুচ্ছবদ্ধ যুক্তির একটি বুলিয়ান বীজগাণিতিক মডেল একটি বুলিয়ান বীজগাণিতিক অবস্থানতন্ত্র যা একটি অবশিষ্টিত সমমিত মনয়ডাল গঠন ধারণ করে।

প্রমাণ তত্ত্ব এবং টাইপ তত্ত্ব (গুচ্ছ)

গুচ্ছবদ্ধ যুক্তির প্রমাণ ক্যালকুলাস প্রচলিত সিকুয়েন্স ক্যালকুলাস থেকে আলাদা কারণ এটি উপপত্তির জন্য তালিকা সদৃশ কাঠামোর পরিবর্তে গাছ সদৃশ প্রসঙ্গ ধারণ করে। গণিতীয় প্রস্তাবনার উপর ভিত্তি করে $\mathrm{\Delta }$ এর মধ্যে একটি গুচ্ছ গঠন ব্যবহার করা হয় যা প্রসঙ্গের গভীর অভেদ অনুমোদন করে এবং শুধুমাত্র পৃষ্ঠস্তরে সীমাবদ্ধ নয়। গুচ্ছবদ্ধ যুক্তির সাথে সম্পর্কিত একটি টাইপ তত্ত্ব রয়েছে যা দুই ধরনের ফাংশন টাইপ ধারণ করে। কারি–হাওয়ার্ড মিলনায়তন অনুসারে, প্রস্তাবনার নিয়মগুলো ফাংশন টাইপগুলোর নিয়মের সাথে সঙ্গতিপূর্ণ।

$\frac{\mathrm{\Gamma },x:A⊢M:B}{\mathrm{\Gamma }⊢\lambda x.M:A-*B}\frac{\mathrm{\Gamma };x:A⊢M:B}{\mathrm{\Gamma }⊢\alpha x.M:A\Rightarrow B}$

এখানে দুটি ভিন্ন বাইন্ডার, $\lambda$ এবং $\alpha$, রয়েছে, যা প্রতিটি ফাংশন টাইপের জন্য আলাদা।

গুচ্ছবদ্ধ যুক্তির প্রমাণ তত্ত্ব প্রাসঙ্গিক যুক্তিতে গুচ্ছ ব্যবহারের একটি ঐতিহাসিক ঋণ বহন করে। তবে গুচ্ছ কাঠামোকে বিভাগীয় এবং বীজগাণিতিক অর্থবোধকতা থেকে নিরূপণ করা যেতে পারে: $-*$ এর নিয়ম তৈরি করার জন্য আমাদের উচিত সিকুয়েন্সের বামদিকে $*$ অনুকরণ করা, এবং $\Rightarrow$ প্রবর্তনের জন্য $\wedge$ অনুকরণ করা। এই বিবেচনা দুটি সংযোজনকারী অপারেটরের ব্যবহারের দিকে পরিচালিত করে।

জেমস ব্রাদারস্টন গুচ্ছবদ্ধ যুক্তি এবং এর প্রকরণগুলোর জন্য একটি ঐক্যবদ্ধ প্রমাণ তত্ত্ব নিয়ে কাজ করেছেন, যেখানে বেলন্যাপ এর ডিসপ্লে লজিক ধারণা ব্যবহার করেছেন।

গালমিচ, মেরি, এবং পিম লেবেলড টেবলো ভিত্তিক পূর্ণতা এবং অন্যান্য মেটা-তত্ত্বসহ গুচ্ছবদ্ধ যুক্তির একটি ব্যাপক আলোচনা করেছেন।

প্রয়োগসমূহ

হস্তক্ষেপ নিয়ন্ত্রণ

উপ-গঠনমূলক টাইপ তত্ত্ব ব্যবহার করে সম্পদের নিয়ন্ত্রণের প্রথম উদাহরণে, জন সি. রেনল্ডস দেখিয়েছিলেন কিভাবে আফিন যুক্তির টাইপ তত্ত্ব ব্যবহার করে অ্যালগল-সদৃশ প্রোগ্রামিং ভাষাগুলোতে অ্যালিয়াসিং এবং অন্যান্য ধরনের হস্তক্ষেপ নিয়ন্ত্রণ করা যায়। ও'হার্ন গুচ্ছ টাইপ তত্ত্ব ব্যবহার করে রেনল্ডসের সিস্টেমটি প্রসারিত করেন, যা হস্তক্ষেপ এবং অ-হস্তক্ষেপ আরও নমনীয়ভাবে মেশানো সম্ভব করে তোলে। এটি রেনল্ডসের সিস্টেমে পুনরাবৃত্তি এবং লাফ সংক্রান্ত সমস্যাগুলি সমাধান করেছিল।

বিভাজন যুক্তি

বিভাজন যুক্তি হোর লজিক এর একটি সম্প্রসারণ, যা পরিবর্তনশীল পয়েন্টার ব্যবহারকারী ডেটা কাঠামো সম্পর্কে যুক্তি প্রদান সহজতর করে। হোর লজিকের মতো, বিভাজন যুক্তির সূত্রগুলো আকারে হয় $\{Pre\}program\{Post\}$, তবে প্রাক-শর্ত এবং পর-শর্তগুলো গুচ্ছবদ্ধ যুক্তির একটি মডেলে ব্যাখ্যা করা হয়।

প্রাথমিক সংস্করণটি নিম্নলিখিত মডেলের উপর ভিত্তি করে ছিল:

• $Heaps=L{\rightharpoonup }_{f}V$ (স্থানগুলোর মানগুলিতে সীমিত আংশিক ফাংশন)
• $h_0\bullet h_1=$ অ-অভারল্যাপিং ডোমেনযুক্ত হিপের ইউনিয়ন, যা ডোমেন ওভারল্যাপ করলে সংজ্ঞায়িত নয়।

ডোমেনগুলোর ওভারল্যাপিংয়ের ক্ষেত্রে সংযোজনটি সংজ্ঞায়িত না হওয়ার কারণে বিভাজন ধারণাটি মডেল করা হয়। এটি গুচ্ছবদ্ধ যুক্তির বুলিয়ান প্রকরণের একটি মডেল। বিভাজন যুক্তি মূলত ধারাবাহিক প্রোগ্রামগুলোর বৈশিষ্ট্য প্রমাণের জন্য ব্যবহৃত হয়েছিল, তবে পরে এটি একাধিক কার্যপ্রবাহে (Concurrency) প্রসারিত হয়, একটি প্রমাণ নিয়ম ব্যবহার করে:

$\frac{\{P_1\}{C}_1\{Q_1\}\{P_2\}{C}_2\{Q_2\}}{\{P_1*P_2\}{C}_1\parallel C_2\{Q_1*Q_2\}}$

যা সমান্তরাল থ্রেডগুলোর দ্বারা অ্যাক্সেস করা স্টোরেজ ভাগ করে।

পরবর্তীতে, সম্পদের অর্থবোধকতার বৃহত্তর সাধারণতাকে কাজে লাগানো হয়: বিভাজন যুক্তির বিমূর্ত সংস্করণ হোর ত্রয়ীর জন্য কাজ করে, যেখানে প্রাক-শর্ত এবং পর-শর্তগুলো নির্দিষ্ট হিপ মডেলের পরিবর্তে একটি নির্বিচার আংশিক কমিউটেটিভ মনোইডের উপর ব্যাখ্যা করা হয়। উপযুক্ত কমিউটেটিভ মনোইড নির্বাচন করে, অবাক করা বিষয় হলো, সমান্তরাল বিভাজন যুক্তির বিমূর্ত সংস্করণের প্রমাণ নিয়মগুলোকে হস্তক্ষেপকারী সমান্তরাল প্রক্রিয়াগুলোর ওপর যুক্তি প্রদানের জন্য ব্যবহার করা যায়, যেমন রিলাই-গ্যারান্টি এবং ট্রেস-ভিত্তিক যুক্তি প্রদান।

বিভাজন যুক্তি বিভিন্ন প্রোগ্রামের স্বয়ংক্রিয় এবং অর্ধ-স্বয়ংক্রিয় যুক্তি প্রদানের জন্য অনেক সরঞ্জামের ভিত্তি, এবং এটি ফেসবুকে বর্তমানে ব্যবহৃত *Infer* প্রোগ্রাম বিশ্লেষকের মধ্যে ব্যবহৃত হচ্ছে।

সম্পদ ও প্রক্রিয়া

গুচ্ছবদ্ধ যুক্তি (সিঙ্ক্রোনাস) সম্পদ-প্রক্রিয়া ক্যালকুলাস SCRP এর সাথে যুক্ত হয়ে ব্যবহার করা হয়েছে, যা একটি (মডাল) যুক্তি প্রদান করে যা হেনেসি–মিলনার অর্থে সমান্তরাল সিস্টেমের যৌগিক কাঠামোকে চিহ্নিত করে।

SCRP-এর বিশেষত্ব হলো এটি $A*B$-কে সিস্টেমের সমান্তরাল সংযোজন এবং তাদের সংশ্লিষ্ট সম্পদের সংযোজনের ক্ষেত্রে ব্যাখ্যা করে। SCRP-এর প্রক্রিয়া যুক্তির অর্থগত ধারাটি, যা বিভাজন যুক্তির সমান্তরাল নিয়মের সাথে সঙ্গতিপূর্ণ, বলে যে একটি সূত্র $A*B$ একটি সম্পদ-প্রক্রিয়া অবস্থায় $R$, $E$ সত্য যদি এবং কেবল যদি সম্পদ $R=S\bullet T$ এবং প্রক্রিয়া $E$ ~ $F\times G$ এর বিভাজন সম্ভব হয়, যেখানে ~ দ্বারা বাইসিমুলেশন নির্দেশিত হয়, এবং $A$ সম্পদ-প্রক্রিয়া অবস্থায় $S$, $F$ সত্য এবং $B$ সম্পদ-প্রক্রিয়া অবস্থায় $T$, $G$ সত্য হয়; অর্থাৎ, $R,E\models A$ তখনই সত্য যদি $S,F\models A$ এবং $T,G\models B$ সত্য হয়।

SCRP সিস্টেম গুচ্ছবদ্ধ যুক্তির সম্পদগত অর্থবোধকতার উপর সরাসরি ভিত্তিক; অর্থাৎ, সম্পদ উপাদানের ক্রমবদ্ধ মনোইডের উপর। যদিও এটি সরাসরি এবং সহজবোধ্য, তবে এটি একটি নির্দিষ্ট কারিগরি সমস্যার দিকে পরিচালিত করে: হেনেসি–মিলনার পূর্ণতার উপপাদ্য শুধুমাত্র মডাল লজিকের টুকরো জন্য প্রযোজ্য যা বহুলক গুণিতক এবং বহুলক রূপান্তর বাদ দেয়। এই সমস্যা সমাধানের জন্য সম্পদ-প্রক্রিয়া ক্যালকুলাস এমন একটি সম্পদগত অর্থবোধকতার উপর ভিত্তি করে যেখানে সম্পদ উপাদানগুলোকে দুটি কম্বিনেটর ব্যবহার করে যুক্ত করা হয়, যার একটি সমান্তরাল সংযোজন এবং অন্যটি পছন্দ নির্দেশ করে।

স্থানিক যুক্তি

কারডেলি, ক্যায়রেস, গর্ডন এবং অন্যান্যরা প্রক্রিয়া ক্যালকুলাসের একটি ধারাবাহিক যুক্তি নিয়ে গবেষণা করেছেন, যেখানে একটি conjunction (সংযোজন) সমান্তরাল সংযোজনের পরিপ্রেক্ষিতে ব্যাখ্যা করা হয়।টেমপ্লেট:Citation needed SCRP-তে পিম এবং অন্যান্যদের কাজের বিপরীতে, তারা সিস্টেমগুলোর সমান্তরাল সংযোজন এবং সিস্টেমগুলো দ্বারা অ্যাক্সেস করা সম্পদের সংযোজনের মধ্যে পার্থক্য করেন না।

তাদের যুক্তিগুলো সম্পদের অর্থবোধকতার উদাহরণের উপর ভিত্তি করে গড়ে উঠেছে, যা গুচ্ছযুক্ত যুক্তির বুলিয়ান প্রকরণের মডেল প্রদান করে। যদিও এই যুক্তিগুলো বুলিয়ান গুচ্ছযুক্ত যুক্তির উদাহরণ প্রদান করে, এটি মনে হয় যে এগুলো স্বতন্ত্রভাবে উদ্ভাবিত হয়েছে এবং যেকোনো ক্ষেত্রে মডালিটি এবং বাইন্ডারের দিক থেকে উল্লেখযোগ্য অতিরিক্ত কাঠামো রয়েছে। সম্পর্কিত যুক্তিগুলো XML ডেটা মডেলিংয়ের জন্যও প্রস্তাবিত হয়েছে।

আরও দেখুন

• বিভাজন যুক্তি
• প্রাসঙ্গিক যুক্তি
• রৈখিক যুক্তি