2025-11-11T14:52:08.882681

Non-commutative linear logic fragments with sub-context-free complexity

Nishimiya, Taniguchi

We present new descriptive complexity characterisations of classes REG (regular languages), LCFL (linear context-free languages) and CFL (context-free languages) as restrictions on inference rules, size of formulae and permitted connectives in the Lambek calculus; fragments of the intuitionistic non-commutative linear logic with direction-sensitive implication connectives. Our identification of the Lambek calculus fragments with proof complexity REG and LCFL is the first result of its kind. We further show the CFL complexity of one of the strictly `weakest' possible variants of the logic, admitting only a single inference rule. The proof thereof, moreover, is based on a direct translation between type-logical and formal grammar and structural induction on provable sequents; a simpler and more intuitive method than those employed in prior works. We thereby establish a clear conceptual utility of the Cut-elimination theorem for comparing formal grammar and sequent calculus, and identify the exact analogue of the Greibach Normal Form in Lambek grammar. We believe the result presented herein constitutes a first step toward a more extensive and richer characterisation of the interaction between computation and logic, as well as a finer-grained complexity separation of various sequent calculi.

academic

অ-বিনিময়যোগ্য রৈখিক যুক্তির খণ্ডাংশ যার উপ-প্রসঙ্গ-মুক্ত জটিলতা রয়েছে

মৌলিক তথ্য

পত্র ID: 2511.02348
শিরোনাম: অ-বিনিময়যোগ্য রৈখিক যুক্তির খণ্ডাংশ যার উপ-প্রসঙ্গ-মুক্ত জটিলতা রয়েছে
লেখক: ইউসাকু নিশিমিয়া (ইলিনয় বিশ্ববিদ্যালয় স্প্রিংফিল্ড ও RIKEN AIP), মাসায়া তানিগুচি (RIKEN AIP)
শ্রেণীবিভাগ: cs.LO (কম্পিউটার বিজ্ঞানে যুক্তি), cs.CC (গণনামূলক জটিলতা), cs.FL (আনুষ্ঠানিক ভাষা), math.LO (গাণিতিক যুক্তি)
প্রকাশনার সময়: ২০২৫ সালের ৪ নভেম্বর (arXiv প্রাক-মুদ্রণ)
পত্রের লিঙ্ক: https://arxiv.org/abs/2511.02348

সারসংক্ষেপ

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

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

সমস্যার পটভূমি

উপ-কাঠামোগত যুক্তি গবেষণা: প্রমাণ তত্ত্ববিদরা উপ-কাঠামোগত যুক্তি অধ্যয়ন করেন যাতে কাঠামোগত নিয়মগুলি অনুমতি বা নির্মূল করা প্রমাণ সিস্টেমের বৈশিষ্ট্যগুলিকে কীভাবে প্রভাবিত করে তা বুঝতে পারেন, সাধারণত ক্রম ক্যালকুলাসের আকারে উপস্থাপিত হয়।
রৈখিক যুক্তির গণনামূলক তাৎপর্য: রৈখিক যুক্তি (LL) সংকোচন এবং দুর্বলতা নিয়মগুলি সীমাবদ্ধ করে, যা প্রমাণগুলিকে শাস্ত্রীয় যুক্তির চেয়ে আরও সম্পদ-সচেতন করে তোলে, এবং তাই গণনার সাথে আরও প্রাসঙ্গিক। MALL হল PSPACE-সম্পূর্ণ এবং MLL হল NP-সম্পূর্ণ বলে পরিচিত।
ল্যাম্বেক ক্যালকুলাসের প্রকাশনা শক্তি: ল্যাম্বেক ক্যালকুলাস L হল LL এর স্বজ্ঞাত, অ-বিনিময়যোগ্য, গুণক খণ্ডাংশ, যার দিক-সংবেদনশীল অন্তর্ভুক্তি রয়েছে। পেন্টাস প্রমাণ করেছেন যে ল্যাম্বেক ব্যাকরণ এবং প্রসঙ্গ-মুক্ত ব্যাকরণের সমতুল্যতা, কিন্তু চমস্কি শ্রেণীবিন্যাসে নিম্ন ভাষা শ্রেণীর সাথে সামঞ্জস্যপূর্ণ L খণ্ডাংশগুলি এখনও চিহ্নিত করা হয়নি।

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

বিদ্যমান গবেষণা LL এর "দুর্বলতর" খণ্ডাংশের গণনামূলক জটিলতা সম্পর্কে অনেক কিছু জানে না, বিশেষত নিয়মিত ভাষা এবং রৈখিক প্রসঙ্গ-মুক্ত ভাষার সাথে সামঞ্জস্যপূর্ণ ল্যাম্বেক ক্যালকুলাস খণ্ডাংশের বর্ণনার অভাব রয়েছে। এই পত্রটি এই ফাঁক পূরণ করার লক্ষ্য রাখে, যুক্তি সূত্রের আকার এবং দিকনির্দেশনা সীমাবদ্ধতা এবং ব্যাকরণ প্রকাশনা শক্তির পরিবর্তনের মধ্যে সঠিক সামঞ্জস্য প্রতিষ্ঠা করে।

মূল অবদান

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

পদ্ধতির বিস্তারিত বর্ণনা

কাজের সংজ্ঞা

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

তাত্ত্বিক কাঠামো

ল্যাম্বেক ক্যালকুলাসের সংজ্ঞা

ল্যাম্বেক ক্যালকুলাস L অন্তর্ভুক্ত করে:

স্বতঃসিদ্ধ: α → α
কাট নিয়ম: Γ,α,Θ → β এবং Δ → α থেকে Γ,Δ,Θ → β অনুমান করা
ছয়টি অনুমান নিয়ম: তিনটি দ্বিপদী সংযোজক /, \ এবং · জড়িত বাম-ডান নিয়ম

মূল ধারণা

প্রকার ডিগ্রি d(α): প্রকার α-তে সংযোজকের বিভিন্ন উপস্থিতির সংখ্যা
প্রকার সেট: Tp(/) শুধুমাত্র / সংযোজক ধারণকারী প্রকার সেট নির্দেশ করে, Tpn ডিগ্রি ≤ n সহ প্রকার নির্দেশ করে
ল্যাম্বেক ব্যাকরণ: চতুর্গুণ (Pr, V, SG, f), যেখানে f হল প্রকার নিয়োগ ফাংশন

মূল উপপাদ্য

উপপাদ্য 2 (প্রধান ফলাফল): নিম্নলিখিত তিন জোড়া ল্যাম্বেক খণ্ডাংশ ব্যাকরণ এবং আনুষ্ঠানিক ব্যাকরণের সমতুল্য প্রকাশনা শক্তি রয়েছে:

L(/ →)-ব্যাকরণ Tp(/) সহ ⇔ CFG
L(/ →, \ →)-ব্যাকরণ Tp1(/, ) সহ ⇔ LCFG
L(/ →)-ব্যাকরণ Tp1(/) সহ ⇔ REG

প্রমাণ কৌশল

হ্রাসযোগ্যতা শর্ত (লেম্মা 3)

Tp(/) এ অ-খালি প্রকার ক্রম Γ এর জন্য, L(/ →) ⊢ Γ → SG যদি এবং শুধুমাত্র যদি:

Γ = α,Δ1,...,Δn, যেখানে α ফর্ম (···((S/βn)/βn-1)/···)/β1
সমস্ত 1≤k≤n এর জন্য, L(/ →) ⊢ Δk → βk

নির্মাণ পদ্ধতি

CFG থেকে ল্যাম্বেক ব্যাকরণ: গ্রেইবাখ স্বাভাবিক ফর্ম অনুমান করে, উৎপাদন নিয়ম A → aB1···Bn কে প্রকার নিয়োগে রূপান্তরিত করা (···((A/Bn)/Bn-1)/···)/B1 ∈ f(a)
ল্যাম্বেক ব্যাকরণ থেকে CFG: প্রকার নিয়োগ (···((α/βn)/βn-1)/···)/β1 ∈ f(a) কে উৎপাদন নিয়ম α → aβ1β2···βn এ রূপান্তরিত করা

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

এই পত্রটি বিশুদ্ধ তাত্ত্বিক গবেষণা, যা পরীক্ষামূলক যাচাইকরণ জড়িত নয়, বরং কঠোর গাণিতিক প্রমাণের মাধ্যমে সমতুল্যতা সম্পর্ক প্রতিষ্ঠা করে।

প্রমাণ পদ্ধতি

কাঠামোগত আবেগ: প্রমাণযোগ্য ক্রমের উপর কাঠামোগত আবেগ
কাট নির্মূলকরণ: জেন্টজেন উপপাদ্য ব্যবহার করে কাট-মুক্ত প্রমাণের অস্তিত্ব নিশ্চিত করা
দ্বিমুখী নির্মাণ: ভাষা সমতুল্যতার উভয় দিক আলাদাভাবে প্রমাণ করা

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

প্রধান ফলাফল

প্রস্তাব 4 (প্রসঙ্গ-মুক্ত ভাষা)

L(/ →) এবং Tp(/) এর উপর ভিত্তি করে ল্যাম্বেক ব্যাকরণ ঠিক খালি স্ট্রিং ছাড়া প্রসঙ্গ-মুক্ত ভাষা চিনতে পারে।

প্রমাণের মূল বিষয়:

CFG → L(/ →) ব্যাকরণ: গ্রেইবাখ স্বাভাবিক ফর্ম ব্যবহার করে, সংশ্লিষ্ট প্রকার নিয়োগ নির্মাণ করা
L(/ →) ব্যাকরণ → CFG: প্রকার নিয়োগকে উৎপাদন নিয়মে রূপান্তরিত করা, আবেগের মাধ্যমে ভাষা সমতুল্যতা প্রমাণ করা

প্রস্তাব 6 (রৈখিক প্রসঙ্গ-মুক্ত ভাষা)

Tp1(/, ) এ সীমাবদ্ধ L(/ →, \ →)-ব্যাকরণ ঠিক রৈখিক ভাষা চিনতে পারে।

নির্মাণ পদ্ধতি:

A/B ∈ f(a) ⟺ A → aB ∈ P (ডান-রৈখিক)
B\A ∈ f(a) ⟺ A → Ba ∈ P (বাম-রৈখিক)
A ∈ f(a) ⟺ A → a ∈ P (টার্মিনাল)

অনুসিদ্ধান্ত 7 (নিয়মিত ভাষা)

Tp1(/) এ সীমাবদ্ধ L(/ →)-ব্যাকরণ ঠিক নিয়মিত ভাষা চিনতে পারে।

মূল আবিষ্কার

দিকনির্দেশনার গুরুত্ব: একক-দিক L(/ →)-ব্যাকরণ ডান-নিয়মিত ব্যাকরণের সাথে সামঞ্জস্যপূর্ণ, দ্বি-দিক L(/ →, \ →)-ব্যাকরণ রৈখিক ব্যাকরণের সাথে সামঞ্জস্যপূর্ণ
ডিগ্রি সীমাবদ্ধতার প্রভাব: প্রকার ডিগ্রি সীমাবদ্ধতা 1 এ স্বাভাবিকভাবে উৎপাদন নিয়মের (দ্বি)রৈখিকতার সাথে সামঞ্জস্যপূর্ণ
গ্রেইবাখ স্বাভাবিক ফর্মের সাদৃশ্য: একক-দিক L(/ →)-ব্যাকরণ গ্রেইবাখ স্বাভাবিক ফর্মের প্রমাণ-তাত্ত্বিক সাদৃশ্য হিসাবে দেখা যায়

সিদ্ধান্ত এবং আলোচনা

প্রধান সিদ্ধান্ত

সঠিক বৈশিষ্ট্য: ল্যাম্বেক ক্যালকুলাস খণ্ডাংশ এবং চমস্কি শ্রেণীবিন্যাসে তিনটি গুরুত্বপূর্ণ ভাষা শ্রেণীর মধ্যে সঠিক সামঞ্জস্য প্রতিষ্ঠা করা
সরলীকৃত পদ্ধতি: পূর্ববর্তী কাজের চেয়ে আরও সরাসরি এবং স্বজ্ঞাত প্রমাণ পদ্ধতি প্রদান করা
তাত্ত্বিক অন্তর্দৃষ্টি: যুক্তি অনুমান নিয়ম এবং আনুষ্ঠানিক ব্যাকরণ উৎপাদন নিয়মের মধ্যে গভীর সংযোগ প্রকাশ করা

সীমাবদ্ধতা

পরিসীমা সীমাবদ্ধতা: চমস্কি শ্রেণীবিন্যাসে শুধুমাত্র অংশ ভাষা শ্রেণী বিবেচনা করা
খালি স্ট্রিং পরিচালনা: নির্মিত ব্যাকরণ খালি স্ট্রিং অন্তর্ভুক্ত করে না
ব্যবহারিক প্রয়োগ: প্রধানত তাত্ত্বিক ফলাফল, ব্যবহারিক প্রয়োগ মূল্য আরও অন্বেষণের জন্য অপেক্ষা করছে

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

লেখকরা তিনটি প্রতিশ্রুতিশীল গবেষণা দিক প্রস্তাব করেছেন:

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

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

সুবিধা

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

অপূর্ণতা

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

প্রভাব

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

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

তাত্ত্বিক কম্পিউটার বিজ্ঞান: যুক্তি সিস্টেমের গণনামূলক জটিলতা গবেষণার জন্য নতুন পদ্ধতি প্রদান করা
আনুষ্ঠানিক ভাষা তত্ত্ব: ভাষা শ্রেণীর যুক্তি বৈশিষ্ট্যের জন্য নতুন দৃষ্টিভঙ্গি প্রদান করা
প্রাকৃতিক ভাষা প্রক্রিয়াকরণ: প্রকার যুক্তি-ভিত্তিক ব্যাকরণ বিশ্লেষণের জন্য তাত্ত্বিক ভিত্তি প্রদান করতে পারে
প্রমাণ তত্ত্ব গবেষণা: উপ-কাঠামোগত যুক্তির আরও গবেষণার জন্য প্রযুক্তিগত সরঞ্জাম প্রদান করা

তথ্যসূত্র

পত্রটি এই ক্ষেত্রের মূল সাহিত্য উদ্ধৃত করে, যার মধ্যে রয়েছে:

গিরার্ডের রৈখিক যুক্তি প্রতিষ্ঠাপক কাজ Gir87
ল্যাম্বেকের মূল কাজ Lam58
ল্যাম্বেক ব্যাকরণ প্রকাশনা শক্তির উপর পেন্টাসের গুরুত্বপূর্ণ ফলাফল Pen93, Pen97
রৈখিক যুক্তি জটিলতার শাস্ত্রীয় ফলাফল LMSS92, Kan91

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