2025-11-17T09:43:13.266953

Constructive validity of a generalized Kreisel-Putnam rule

Pezlar
In this paper, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry-Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for the intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding computational content of the typed Split rule. In other words, we want to find an appropriate selector function for the Split rule by considering its typed variant. Our investigation can also be reframed as an effort to answer the following questions: is the Split rule constructively valid in the sense of BHK semantics? Our answer is positive for the Split rule as well as for its newly proposed generalized version called the S rule.
academic

একটি সাধারণীকৃত Kreisel-Putnam নিয়মের গঠনমূলক বৈধতা

মৌলিক তথ্য

  • পেপার আইডি: 2311.15376
  • শিরোনাম: একটি সাধারণীকৃত Kreisel-Putnam নিয়মের গঠনমূলক বৈধতা
  • লেখক: Ivo Pezlar (চেক একাডেমি অফ সায়েন্সেস, ফিলোসফি ইনস্টিটিউট)
  • শ্রেণীবিভাগ: cs.LO (কম্পিউটার বিজ্ঞান - কম্পিউটার বিজ্ঞানে যুক্তি), math.LO (গণিত - যুক্তি)
  • প্রকাশনার সময়: ২০২৩ সালের ২৮ নভেম্বর (arXiv v2)
  • পেপার লিঙ্ক: https://arxiv.org/abs/2311.15376

সারসংক্ষেপ

এই পেপারটি সাধারণীকৃত Kreisel-Putnam নিয়ম (যা সাধারণীকৃত Harrop নিয়ম বা Split নিয়ম নামেও পরিচিত) এর গণনামূলক ব্যাখ্যা প্রস্তাব করে, BHK শব্দার্থবিজ্ঞান শৈলী অনুসরণ করে। সূত্র এবং প্রকারের মধ্যে Curry-Howard সামঞ্জস্য ব্যবহার করে এটি অর্জন করা হয়। প্রথমে সরাসরি প্রস্তাবনামূলক যুক্তির স্বাভাবিক অনুমান ব্যবস্থায় Split নিয়মের অনুমান আচরণ পরীক্ষা করা হয়, যা টাইপ করা Split নিয়মের সংশ্লিষ্ট গণনামূলক বিষয়বস্তু ক্যাপচার করার জন্য উপযুক্ত প্রোগ্রাম প্রণয়নে আমাদের গাইড করবে। অন্য কথায়, আমরা এর টাইপ করা রূপান্তর বিবেচনা করে Split নিয়মের উপযুক্ত নির্বাচক ফাংশন খুঁজে পেতে চাই। আমাদের গবেষণা নিম্নলিখিত প্রশ্নের উত্তর দেওয়ার জন্য পুনর্বিবৃত করা যেতে পারে: Split নিয়ম কি BHK শব্দার্থবিজ্ঞানের অর্থে গঠনমূলকভাবে বৈধ? আমরা Split নিয়ম এবং এর নতুন প্রস্তাবিত সাধারণীকরণ (S নিয়ম নামে পরিচিত) উভয়ের জন্য একটি ইতিবাচক উত্তর প্রদান করি।

গবেষণা পটভূমি এবং প্রেরণা

মূল সমস্যা

এই পেপারটি যে মূল সমস্যাটি সমাধান করতে চায় তা হল: Split নিয়ম কি BHK শব্দার্থবিজ্ঞানের অর্থে গঠনমূলকভাবে বৈধ? বিশেষভাবে, এটি একটি গঠনমূলক ফাংশন খুঁজে পাওয়া যা Split নিয়মের পূর্বশর্তের যেকোনো প্রমাণকে এর সিদ্ধান্তের প্রমাণে রূপান্তরিত করতে পারে।

সমস্যার গুরুত্ব

১. তাত্ত্বিক তাৎপর্য: Kreisel-Putnam নিয়ম হল সরাসরি যুক্তিতে একটি অনুমোদিত কিন্তু অনুমানযোগ্য নিয়ম, যদিও Dummett-Prawitz শৈলীর শব্দার্থবিজ্ঞানের রূপান্তরে এটি প্রমাণ-তাত্ত্বিকভাবে বৈধ। ২. যুক্তি ব্যবস্থার বৈশিষ্ট্য: যখন Split নিয়ম সরাসরি যুক্তিতে যোগ করা হয়, ফলস্বরূপ ব্যবস্থা (যেমন প্রশ্নমূলক সরাসরি যুক্তি) বিচ্ছেদ সম্পত্তি বজায় রাখে এবং কাঠামোগত সম্পূর্ণতা রয়েছে, যা চিরন্তন যুক্তির বৈশিষ্ট্য। ३. ব্যাপক প্রয়োগ: Split নিয়ম ডোমেইন যুক্তি সহ একাধিক ক্ষেত্রে প্রদর্শিত হয়, এর মৌলিক গুরুত্ব প্রদর্শন করে।

বিদ্যমান পদ্ধতির সীমাবদ্ধতা

१. গণনামূলক ব্যাখ্যার অভাব: Split নিয়মের গুরুত্ব সত্ত্বেও, এর প্রমাণ-তাত্ত্বিক অর্থ এবং গণনামূলক বিষয়বস্তু বেশিরভাগই অন্বেষণ করা হয়নি। २. গঠনমূলক বৈধতা অস্পষ্ট: Split নিয়মের গণনামূলক বিষয়বস্তু ব্যাখ্যা করার জন্য কোনো স্পষ্ট গঠনমূলক ফাংশন নেই।

গবেষণার প্রেরণা

Curry-Howard সামঞ্জস্যের মাধ্যমে, সূত্রগুলিকে প্রকার হিসাবে বিবেচনা করে, Split নিয়মের গণনামূলক বিষয়বস্তু ক্যাপচার করার জন্য উপযুক্ত নির্বাচক ফাংশন খুঁজে পাওয়া, এর গঠনমূলক বৈধতা প্রতিষ্ঠা করা।

মূল অবদান

१. S নিয়ম প্রস্তাব: Split নিয়মকে বিচ্ছেদ নির্মূলন নিয়মের সাধারণীকৃত রূপ হিসাবে পুনর্বিবৃত করা, S নিয়ম নামে পরিচিত। २. গঠনমূলক বৈধতা প্রতিষ্ঠা: S নিয়মের জন্য কার্যকর নির্বাচক ফাংশন S খুঁজে পাওয়া, এর গঠনমূলক বৈধতা প্রমাণ করা। ३. গণনামূলক ব্যাখ্যা প্রদান: টাইপ করা রূপান্তর এবং গণনামূলক নিয়মের মাধ্যমে, Split নিয়মের সম্পূর্ণ গণনামূলক ব্যাখ্যা প্রদান করা। ४. নিয়মিতকরণ সম্পত্তি প্রমাণ: Martin-Löf গঠনমূলক প্রকার তত্ত্বে টাইপ করা S নিয়ম যোগ করার পরেও নিয়মিতকরণ বজায় থাকে তা প্রমাণ করা। ५. নিয়ম সমতুল্যতা প্রতিষ্ঠা: Split নিয়ম এবং S নিয়মের সমতুল্যতা প্রমাণ করা এবং সংশ্লিষ্ট হ্রাস প্রক্রিয়া প্রদান করা।

পদ্ধতির বিস্তারিত ব্যাখ্যা

কাজের সংজ্ঞা

ইনপুট: Split নিয়মের পূর্বশর্ত C → (A ∨ B), যেখানে C একটি Harrop সূত্র আউটপুট: Split নিয়মের সিদ্ধান্ত (C → A) ∨ (C → B)সীমাবদ্ধতা: পূর্বশর্ত থেকে সিদ্ধান্তে রূপান্তরের জন্য গঠনমূলক ফাংশন খুঁজে পাওয়া

মূল পদ্ধতির স্থাপত্য

१. নিয়ম পুনর্বিবৃতি

মূল Split নিয়ম:

C → (A ∨ B)
─────────────── Split
(C → A) ∨ (C → B)

S নিয়মে পুনর্বিবৃত করা (বিচ্ছেদ নির্মূলন):

[C]
 ⋮
A ∨ B    [C → A]    [C → B]
          ⋮           ⋮
          D           D
─────────────────────────── S
            D

२. টাইপ করা S নিয়ম

Martin-Löf গঠনমূলক প্রকার তত্ত্বের কাঠামোতে, S নিয়মের টাইপ করা রূপ:

[z : C]
  ⋮
c(z) : A ∨ B    [x : C → A]    [y : C → B]
                   ⋮              ⋮
                d(x) : D        e(y) : D
────────────────────────────────────────── S
            S(c, d, e) : D

३. নির্বাচক S এর গণনামূলক নিয়ম

নির্বাচক S এর গণনা প্যাটার্ন ম্যাচিং এবং কেস বিশ্লেষণের উপর ভিত্তি করে:

বাম শাখা গণনামূলক নিয়ম:

S(inl(a(z)), d, e) = d(λz.a(z)) : D

ডান শাখা গণনামূলক নিয়ম:

S(inr(b(z)), d, e) = e(λz.b(z)) : D

প্রযুক্তিগত উদ্ভাবনী পয়েন্ট

१. Harrop সূত্রের বিশেষ চিকিত্সা

  • মূল অন্তর্দৃষ্টি: Harrop সূত্র গণনামূলকভাবে অপ্রাসঙ্গিক, কারণ তাদের কোনো গণনামূলক বিষয়বস্তু নেই
  • প্রযুক্তিগত বাস্তবায়ন: Smith (1993) এর ফলাফল ব্যবহার করে, মুক্ত ভেরিয়েবল সহ খোলা প্রমাণ বস্তু গণনা করার অনুমতি দেয়, যতক্ষণ এই ভেরিয়েবলগুলির পরিসীমা Harrop সূত্রের মধ্যে সীমাবদ্ধ থাকে

२. অনুমান বিচারের বিশেষীকরণ

বিশেষায়িত অনুমান বিচারের ফর্ম প্রবর্তন:

z : C ⊢ b(z) : B(z)

যেখানে C Harrop সূত্রে সীমাবদ্ধ, যার অর্থ ব্যাখ্যা: b(z) একটি প্রোগ্রাম যা গণনার পরে B(z) প্রকারের একটি নিয়মিত প্রমাণ বস্তু তৈরি করে।

३. হ্রাস প্রক্রিয়ার ডিজাইন

S নিয়মের জন্য সংশ্লিষ্ট হ্রাস নিয়ম প্রদান করা:

  • S-redL: বাম বিচ্ছেদের হ্রাস পরিচালনা করে
  • S-redR: ডান বিচ্ছেদের হ্রাস পরিচালনা করে

এই হ্রাস নিয়মগুলি নিয়মের সামঞ্জস্য এবং স্থানীয় সম্পূর্ণতা নিশ্চিত করে।

পরীক্ষামূলক সেটআপ

তাত্ত্বিক যাচাইকরণ কাঠামো

এই পেপারটি প্রধানত পরীক্ষামূলক যাচাইকরণের পরিবর্তে তাত্ত্বিক বিশ্লেষণ পরিচালনা করে, নিম্নলিখিত কাঠামো গ্রহণ করে: १. ভিত্তি ব্যবস্থা: সরাসরি প্রস্তাবনামূলক যুক্তি (IPC) এর স্বাভাবিক অনুমান ব্যবস্থা २. প্রকার তত্ত্ব: Martin-Löf গঠনমূলক প্রকার তত্ত্ব ३. শব্দার্থবিজ্ঞান কাঠামো: BHK ব্যাখ্যা এবং Curry-Howard সামঞ্জস্য

যাচাইকরণ পদ্ধতি

१. গঠনমূলকতা: স্পষ্ট নির্বাচক ফাংশন নির্মাণের মাধ্যমে গঠনমূলক বৈধতা প্রমাণ করা २. নিয়মিতকরণ: Smith (1993) এর নিয়মিতকরণ প্রমাণ প্রসারিত করে সিস্টেমের সামঞ্জস্য যাচাই করা ३. সমতুল্যতা: পারস্পরিক অনুমানের মাধ্যমে Split নিয়ম এবং S নিয়মের সমতুল্যতা প্রমাণ করা

পরীক্ষামূলক ফলাফল

প্রধান তাত্ত্বিক ফলাফল

१. গঠনমূলক বৈধতা প্রমাণ

উপপাদ্য: S নিয়ম গঠনমূলকভাবে বৈধ। প্রমাণ: স্পষ্ট নির্বাচক S নির্মাণের মাধ্যমে, যা S নিয়মের পূর্বশর্ত থেকে সিদ্ধান্তে রূপান্তর করতে পারে।

२. নিয়মিতকরণ উপপাদ্য

উপপাদ্য: Martin-Löf গঠনমূলক প্রকার তত্ত্বে টাইপ করা S নিয়ম যোগ করার পরেও, সিস্টেম নিয়মিতকরণ বজায় রাখে। প্রমাণ: Smith (1993) এর Kleene-Aczel স্ল্যাশ সাকার্যকারিতার প্রকার তত্ত্ব অনুবাদ প্রসারিত করে, S নিয়ম সহ সিস্টেম নিয়মিতকরণ সম্পত্তি সন্তুষ্ট করে তা প্রমাণ করা।

३. সমতুল্যতা ফলাফল

উপপাদ্য: Split নিয়ম এবং S নিয়ম যুক্তিগতভাবে সমতুল্য। প্রমাণ:

  • S নিয়ম থেকে Split নিয়ম অনুমান করা যায়
  • Split নিয়ম থেকে S নিয়ম অনুমান করা যায়

নির্দিষ্ট কেস বিশ্লেষণ

কেস १: পরমাণু সূত্রের ক্ষেত্রে

সূত্র (p → (q ∨ r)) → ((p → q) ∨ (p → r)) এর জন্য, যেখানে p একটি পরমাণু সূত্র (তাই একটি Harrop সূত্র), S নিয়ম ব্যবহার করে সফলভাবে প্রমাণ করা যায়।

কেস २: অ-Harrop সূত্রের ক্ষেত্রে

সূত্র ((s ∨ t) → (q ∨ r)) → (((s ∨ t) → q) ∨ ((s ∨ t) → r)) এর জন্য, যেহেতু (s ∨ t) একটি Harrop সূত্র নয়, S নিয়ম প্রয়োগ করা যায় না, নিয়মের সীমাবদ্ধতা প্রদর্শন করে।

সম্পর্কিত কাজ

প্রধান সম্পর্কিত গবেষণা

१. Kreisel-Putnam যুক্তি: প্রাথমিকভাবে Kreisel এবং Putnam (1957) দ্বারা প্রস্তাবিত, সরাসরি যুক্তির চেয়ে শক্তিশালী কিন্তু বিচ্ছেদ সম্পত্তি বজায় রাখে এমন একটি যুক্তি ব্যবস্থা। २. প্রশ্নমূলক সরাসরি যুক্তি: Punčochář (2016) এবং Ciardelli ইত্যাদি (2020) এর কাজ, সরাসরি যুক্তিতে Split নিয়ম যোগ করে প্রাপ্ত ব্যবস্থা। ३. প্রমাণ-তাত্ত্বিক শব্দার্থবিজ্ঞান: Prawitz (1971, 1973) এর Dummett-Prawitz শৈলী শব্দার্থবিজ্ঞান এবং এর রূপান্তর।

এই পেপারের সম্পর্কিত কাজের সাথে সম্পর্ক

१. Condoluci এবং Manighetti (2018) এর সাথে তুলনা: তারা সম্পর্কিত Harrop নিয়মের গণনামূলক দৃষ্টিভঙ্গি অধ্যয়ন করেছেন, কিন্তু শীর্ষ-নিচের পদ্ধতি গ্রহণ করেছেন, যখন এই পেপার নিচ-উপরের পদ্ধতি গ্রহণ করে। २. Smith (1993) এর সাথে সম্পর্ক: এই পেপারটি Kleene-Aczel স্ল্যাশ সাকার্যকারিতার প্রকার তত্ত্ব সম্পর্কে Smith এর কাজ প্রসারিত করে, বিশেষত খোলা প্রমাণ বস্তুর গণনা সম্পর্কে।

উপসংহার এবং আলোচনা

প্রধান উপসংহার

१. Split নিয়ম গঠনমূলকভাবে বৈধ: S নিয়মের মধ্যস্থতার মাধ্যমে, Split নিয়ম BHK শব্দার্থবিজ্ঞানের অর্থে গঠনমূলকভাবে বৈধ। २. S নিয়ম প্রাকৃতিক সাধারণীকরণ প্রদান করে: বিচ্ছেদ নির্মূলন নিয়ম হিসাবে, S নিয়ম Split নিয়মের আরও প্রাকৃতিক প্রকাশ প্রদান করে। ३. সিস্টেম ভাল সম্পত্তি বজায় রাখে: S নিয়ম যোগ করার পরে প্রকার ব্যবস্থা নিয়মিতকরণ ইত্যাদি গুরুত্বপূর্ণ সম্পত্তি বজায় রাখে।

সীমাবদ্ধতা

१. Harrop সূত্রে সীমাবদ্ধ: S নিয়ম শুধুমাত্র পূর্বশর্তে C যখন Harrop সূত্র হয় তখনই প্রয়োগ করা যায়, সিস্টেম সামঞ্জস্যপূর্ণ প্রতিস্থাপনের অধীন নয়। २. জটিলতা: নির্বাচক S এর গণনা খোলা প্রমাণ বস্তুর প্রক্রিয়াকরণ জড়িত, তাত্ত্বিক জটিলতা বৃদ্ধি করে। ३. ব্যবহারিকতা: তাত্ত্বিক ফলাফলের প্রকৃত প্রয়োগ মূল্য আরও অন্বেষণের প্রয়োজন।

ভবিষ্যত দিকনির্দেশনা

१. অন্যান্য সাধারণীকরণ: Split নিয়মকে অন্তর্ভুক্তি নির্মূলন নিয়মের অন্য সাধারণীকরণ হিসাবে বিবেচনা করা অন্বেষণ করা। २. সম্প্রসারিত প্রয়োগ: অন্যান্য যুক্তি ব্যবস্থা এবং গণনামূলক কাঠামোতে S নিয়মের প্রয়োগ গবেষণা করা। ३. বাস্তবায়ন যাচাইকরণ: নির্দিষ্ট প্রমাণ সহায়কে এই তাত্ত্বিক ফলাফল বাস্তবায়ন এবং যাচাই করা।

গভীর মূল্যায়ন

সুবিধা

१. তাত্ত্বিক গভীরতা: Split নিয়মের গভীর প্রমাণ-তাত্ত্বিক বিশ্লেষণ এবং গঠনমূলক ব্যাখ্যা প্রদান করে। २. পদ্ধতি উদ্ভাবন: Split নিয়মকে S নিয়মে পুনর্বিবৃত করে, নতুন তাত্ত্বিক দৃষ্টিভঙ্গি প্রদান করে। ३. প্রযুক্তিগত কঠোরতা: Martin-Löf প্রকার তত্ত্বের কাঠামোতে কঠোর আনুষ্ঠানিক চিকিত্সা পরিচালনা করে। ४. সম্পূর্ণতা: শুধুমাত্র গঠনমূলক বৈধতা প্রমাণ করে না, বরং নিয়মিতকরণ ইত্যাদি গুরুত্বপূর্ণ সম্পত্তি যাচাই করে।

অপূর্ণতা

१. সীমিত প্রয়োগ পরিসীমা: Harrop সূত্রের সীমাবদ্ধতা প্রকৃত প্রয়োগকে প্রভাবিত করতে পারে। २. উচ্চ জটিলতা: খোলা প্রমাণ বস্তুর গণনা জড়িত, বোঝা এবং বাস্তবায়নের অসুবিধা বৃদ্ধি করে। ३. পরীক্ষামূলক যাচাইকরণের অভাব: নির্দিষ্ট সিস্টেমে বাস্তবায়ন এবং যাচাইকরণের অভাব।

প্রভাব

१. তাত্ত্বিক অবদান: প্রমাণ-তাত্ত্বিক শব্দার্থবিজ্ঞান এবং গঠনমূলক প্রকার তত্ত্বের ছেদ ক্ষেত্রে গুরুত্বপূর্ণ অবদান। २. পদ্ধতিগত মূল্য: অন্যান্য যুক্তি নিয়মের গঠনমূলক বৈধতা অধ্যয়নের জন্য পদ্ধতি টেমপ্লেট প্রদান করে। ३. মৌলিক গবেষণা: সরাসরি যুক্তির গণনামূলক বিষয়বস্তু বোঝার জন্য নতুন অন্তর্দৃষ্টি প্রদান করে।

প্রযোজ্য পরিস্থিতি

१. প্রমাণ-তাত্ত্বিক গবেষণা: যুক্তি নিয়মের প্রমাণ-তাত্ত্বিক সম্পত্তি এবং গণনামূলক ব্যাখ্যা অধ্যয়নের জন্য প্রযোজ্য। २. প্রকার তত্ত্ব উন্নয়ন: গঠনমূলক প্রকার তত্ত্বের তাত্ত্বিক ভিত্তি প্রসারিত এবং সমৃদ্ধ করতে ব্যবহার করা যায়। ३. যুক্তি প্রোগ্রামিং: যুক্তি প্রোগ্রামিং ভাষাগুলিকে নতুন তাত্ত্বিক সমর্থন প্রদান করতে পারে।

সংদর্ভ

এই পেপারটি সমৃদ্ধ সম্পর্কিত সাহিত্য উদ্ধৃত করে, প্রধানত অন্তর্ভুক্ত:

  • Kreisel এবং Putnam (1957) Kreisel-Putnam যুক্তির যুগান্তকারী কাজ
  • Smith (1993) Kleene-Aczel স্ল্যাশ সাকার্যকারিতার প্রকার তত্ত্ব ব্যাখ্যা সম্পর্কে
  • Martin-Löf (1984) গঠনমূলক প্রকার তত্ত্বের ভিত্তি
  • Prawitz (1965, 1971, 1973) প্রমাণ তত্ত্ব এবং শব্দার্থবিজ্ঞান কাজ
  • প্রশ্নমূলক যুক্তি সম্পর্কে সাম্প্রতিক গবেষণা (Punčochář 2016, Ciardelli ইত্যাদি 2020)

এটি যুক্তি এবং প্রকার তত্ত্বের ছেদ ক্ষেত্রে একটি উচ্চমানের তাত্ত্বিক গবেষণা পেপার, Split নিয়মের গঠনমূলক বিষয়বস্তু বোঝার জন্য গুরুত্বপূর্ণ তাত্ত্বিক অবদান প্রদান করে। যদিও এটি নির্দিষ্ট প্রযুক্তিগত জটিলতা এবং প্রয়োগ সীমাবদ্ধতা রয়েছে, তবে এর কঠোর তাত্ত্বিক বিশ্লেষণ এবং উদ্ভাবনী পদ্ধতিবিজ্ঞান সম্পর্কিত ক্ষেত্রের উন্নয়নের জন্য গুরুত্বপূর্ণ মূল্য রাখে।