الحساب المحدود

الموسوعة الحرة

الحساب المحدود هو مصطلح جامع لمجموعة من النظريات الفرعية الضعيفة لحساب بيانو . تُستنتج هذه النظريات عادةً باشتراط أن تكون المُكمِّمات محدودة في بديهية الاستقراء أو المسلمات المكافئة ( المُكمِّم المحدود يكون على الصورة ∀ x  ≤ t أو ∃ x ≤ t ، حيث t حد لا يحتوي على x ). الهدف الرئيسي هو توصيف فئة أو أخرى من فئات التعقيد الحسابي ، بمعنى أن الدالة تكون كلية قابلة للإثبات إذا وفقط إذا كانت تنتمي إلى فئة تعقيد معينة. علاوة على ذلك، تُقدم نظريات الحساب المحدود نظائر موحدة لأنظمة إثبات القضايا القياسية ، مثل نظام فريجه ، وهي مفيدة بشكل خاص في بناء براهين ذات حجم متعدد الحدود في هذه الأنظمة. يسمح توصيف فئات التعقيد القياسية ومطابقتها لأنظمة إثبات القضايا بتفسير نظريات الحساب المحدود كنظم رسمية تُجسد مستويات مختلفة من الاستدلال الممكن (انظر أدناه).    

بدأ هذا النهج من قبل روهيت جيفانلال باريك [ 1 ] في عام 1971، وتم تطويره لاحقًا بواسطة صموئيل ر . بوس [ 2 ] وعدد من علماء المنطق الآخرين.

النظريات

نظرية كوك للمعادلات

قدم ستيفن كوك نظرية المعادلاتPV{\displaystyle PV}(بالنسبة إلى التحقق متعدد الحدود) صياغة البراهين البنائية الممكنة (أو الاستدلال متعدد الحدود). [ 3 ] لغةPV{\displaystyle PV}يتألف من رموز دوال لجميع الخوارزميات ذات الزمن متعدد الحدود، والتي تُقدم استقرائيًا باستخدام توصيف كوبام لدوال الزمن متعدد الحدود. تُقدم بديهيات واشتقاقات النظرية بالتزامن مع الرموز من اللغة. النظرية معادلاتية، أي أن عباراتها تؤكد فقط على تساوي حدين. وهو امتداد شائع لـPV{\displaystyle PV}هي نظريةPV1{\displaystyle PV_{1}}، نظرية عادية من الدرجة الأولى. [ 4 ] بديهياتPV1{\displaystyle PV_{1}}هي جمل عالمية وتحتوي على جميع المعادلات القابلة للإثبات فيPV{\displaystyle PV}. فضلاً عن ذلك،PV1{\displaystyle PV_{1}}يحتوي على بديهيات تحل محل بديهيات الاستقراء للصيغ المفتوحة.

نظريات بوس من الدرجة الأولى

قدّم صموئيل بوس نظريات الرتبة الأولى للحساب المحدودS2أنا{\displaystyle S_{2}^{i}}[ 2 ]​S2أنا{\displaystyle S_{2}^{i}}هي نظريات من الدرجة الأولى مع المساواة في اللغةل={0،S،+،⋅،♯،|x|،⌊x2⌋}{\displaystyle L=\{0,S,+,\cdot ,\sharp ,|x|,\lfloor {\frac {x}{2}}\rfloor \}}، حيث الدالة|x|{\displaystyle |x|}يهدف إلى تحديد⌈سجل⁡(x+1)⌉{\displaystyle \lceil \log(x+1)\rceil }(عدد الأرقام في التمثيل الثنائي لـx{\displaystyle x}) وx♯y{\displaystyle x\sharp y}يكون2|x|⋅|y|{\displaystyle 2^{|x|\cdot |y|}}. (لاحظ أن|x♯x|∼|x|2{\displaystyle |x\sharp x|\sim |x|^{2}}، أي♯{\displaystyle \sharp }يُتيح ذلك التعبير عن حدود متعددة الحدود بطول بتات المدخلات. المُكمِّمات المحدودة هي تعبيرات من الشكل التالي:∃x≤ت⋯:=∃x(x≤ت∧...){\displaystyle \exists x\leq t\dots :=\exists x(x\leq t\wedge \dots )} ,∀x≤ت⋯:=∀x(x≤ت→...){\displaystyle \forall x\leq t\dots :=\forall x(x\leq t\rightarrow \dots )} , حيثت{\displaystyle t}هو مصطلح لا يحتوي على أي من عناصرx{\displaystyle x}يكون المُكمِّم المحدود محدودًا بدقة إذات{\displaystyle t}له شكل|s|{\displaystyle |s|}لفترةs{\displaystyle s}صيغةϕ{\displaystyle \phi }تكون محدودة بدقة إذا كانت جميع المحددات الكمية في الصيغة محدودة بدقة. التسلسل الهرمي لـΣأناب{\displaystyle \Sigma _{i}^{b}}وΠأناب{\displaystyle \Pi _{i}^{b}}يتم تعريف الصيغ استقرائياً:Σ0ب=Π0ب{\displaystyle \Sigma _{0}^{b}=\Pi _{0}^{b}}هي مجموعة الصيغ ذات الحدود الدقيقة.Σأنا+1ب{\displaystyle \Sigma _{i+1}^{b}}هل إغلاقΠأناب{\displaystyle \Pi _{i}^{b}}في ظل الكميات الوجودية المحدودة والكميات العالمية المحدودة بدقة، وΠأنا+1ب{\displaystyle \Pi _{i+1}^{b}}هل إغلاقΣأناب{\displaystyle \Sigma _{i}^{b}}تحت تأثير المحددات الكمية الشاملة المحدودة والمحددات الكمية الوجودية المحدودة بدقة. تُجسد الصيغ المحدودة التسلسل الهرمي ذي الوقت متعدد الحدود : لأيأنا≥1{\displaystyle i\geq 1}، الصفΣأناP{\displaystyle \Sigma _{i}^{P}}يتطابق مع مجموعة الأعداد الطبيعية التي يمكن تعريفها بواسطةΣأناب{\displaystyle \Sigma _{i}^{b}}فيشمال{\displaystyle \mathbb {N} }(النموذج القياسي للحساب) وثنائيًاΠأناب=ΠأناP(شمال){\displaystyle \Pi _{i}^{b}=\Pi _{i}^{P}(\mathbb {N} )}. بخاصة،شمالP=Σ1ب(شمال){\displaystyle NP=\Sigma _{1}^{b}(\mathbb {N} )}.

النظريةS2أنا{\displaystyle S_{2}^{i}}يتألف من قائمة محدودة من البديهيات المفتوحة المشار إليها بـ BASIC ومخطط الاستقراء متعدد الحدود

ϕ(0)∧∀x≤أ(ϕ(⌊x2⌋)→ϕ(x))→ϕ(أ){\displaystyle \phi (0)\wedge \forall x\leq a(\phi (\lfloor {\frac {x}{2}}\rfloor )\rightarrow \phi (x))\rightarrow \phi (a)}

أينϕ∈Σأناب{\displaystyle \phi \in \Sigma _{i}^{b}}.

نظرية بوس للشهادة

أثبت بوس (1986) أنΣ1ب{\displaystyle \Sigma _{1}^{b}}نظرياتS21{\displaystyle S_{2}^{1}}يتم رصدها بواسطة دوال ذات زمن متعدد الحدود. [ 2 ]

نظرية (بوس 1986)

افترض أنS21⊢∀x∃yϕ(x،y){\displaystyle S_{2}^{1}\vdash \forall x\exists y\phi (x,y)}، معϕ∈Σ1ب{\displaystyle \phi \in \Sigma _{1}^{b}}ثم، يوجدPV{\displaystyle PV}- رمز الدالةو{\displaystyle f}بحيثPV⊢∀xϕ(x،و(x)){\displaystyle PV\vdash \forall x\phi (x,f(x))}.

علاوة على ذلك،S21{\displaystyle S_{2}^{1}}يستطيعΣ1ب{\displaystyle \Sigma _{1}^{b}}- تعريف جميع الدوال ذات الزمن متعدد الحدود. أي،Σ1ب{\displaystyle \Sigma _{1}^{b}}الدوال القابلة للتعريف فيS21{\displaystyle S_{2}^{1}}هي تحديداً الدوال القابلة للحساب في زمن متعدد الحدود. ويمكن تعميم هذا التوصيف ليشمل مستويات أعلى من التسلسل الهرمي متعدد الحدود.

المراسلات لأنظمة إثبات القضايا

تُدرس نظريات الحساب المحدود غالبًا في سياق أنظمة البرهان الافتراضي. وكما أن آلات تورينج تُعدّ مكافئات موحدة لنماذج حسابية غير موحدة، مثل الدوائر المنطقية ، يُمكن اعتبار نظريات الحساب المحدود مكافئات موحدة لأنظمة البرهان الافتراضي. يُعدّ هذا الربط مفيدًا بشكل خاص في بناء البراهين الافتراضية المختصرة. فغالبًا ما يكون من الأسهل إثبات نظرية ما في نظرية الحساب المحدود، ثم ترجمة البرهان من الدرجة الأولى إلى سلسلة من البراهين المختصرة في نظام البرهان الافتراضي، بدلًا من تصميم البراهين الافتراضية المختصرة مباشرةً في نظام البرهان الافتراضي.

تم تقديم المراسلات بواسطة إس. كوك. [ 3 ]

بشكل غير رسمي، أΠ1ب{\displaystyle \Pi _{1}^{b}}إفادة∀xΦ(x){\displaystyle \forall x\Phi (x)}ويمكن التعبير عنها بشكل مكافئ كسلسلة من الصيغΦن(x):=∀x(|x|=ن→Φ(x)){\displaystyle \Phi _{n}(x):=\forall x(|x|=n\rightarrow \Phi (x))}. منذΦن(x){\displaystyle \Phi _{n}(x)}هو مسند coNP، كلΦن(x){\displaystyle \Phi _{n}(x)}ويمكن صياغتها بدورها على أنها تحصيل حاصل.||ϕ||ن{\displaystyle ||\phi ||^{n}}(ربما تحتوي على متغيرات جديدة لازمة لترميز حساب المسند)Φن{\displaystyle \Phi _{n}}).

نظرية (كوك 1975)

افترض أنS21⊢∀xΦ(x){\displaystyle S_{2}^{1}\vdash \forall x\Phi (x)}، أينΦ∈Π1ب{\displaystyle \Phi \in \Pi _{1}^{b}}ثم التكرارات||ϕ||ن{\displaystyle ||\phi ||^{n}}تتميز هذه البراهين بنطاق زمني متعدد الحدود . علاوة على ذلك، يمكن بناء هذه البراهين باستخدام دالة زمنية متعددة الحدود.PV{\displaystyle PV}يثبت هذا الواقع.

إضافي،S21{\displaystyle S_{2}^{1}}يثبت ما يسمى بمبدأ الانعكاس لنظام فريج الموسع، مما يعني أن نظام فريج الموسع هو أضعف نظام إثبات يتمتع بالخاصية من النظرية أعلاه: كل نظام إثبات يحقق الاستلزام يحاكي فريج الموسع.

لقد كانت الترجمة البديلة بين عبارات الرتبة الثانية والصيغ الافتراضية التي قدمها جيف باريس وأليكس ويلكي (1985) أكثر عمليةً في تمثيل الأنظمة الفرعية لـ Extended Frege مثل Frege أو Frege ذي العمق الثابت. [ 5 ] [ 6 ]

انظر أيضاً

مراجع

  1. ↑ روهيت ج. باريك. الوجود والجدوى في الحساب، مجلة المنطق الرمزي 36 (1971) 494-508.
  2. 1 2 3 بوس، صموئيل . "الحساب المحدود". بيبليوبوليس، نابولي، إيطاليا، 1986 .
  3. 1 2 كوك، ستيفن (1975). "البراهين البنائية الممكنة وحساب القضايا". وقائع الندوة السنوية السابعة لجمعية آلات الحوسبة حول نظرية الحوسبة . الصفحات 83-97 . 
  4. ↑ كرايتشيك، يان؛ بودلاك، بافيل؛ تاكيوتي، ج. (1991). "الحساب المحدود والتسلسل الهرمي متعدد الحدود". حوليات المنطق البحت والتطبيقي . ص 143-153 . 
  5. ↑ باريس، جيف ؛ ويلكي، أليكس (1985). "مسائل العد في الحساب المحدود". مناهج في المنطق الرياضي . المجلد 1130. الصفحات 317-340 .  
  6. ↑ كوك، ستيفن ؛ نغوين، فونغ (2010). "الأسس المنطقية لتعقيد البرهان". وجهات نظر في المنطق. كامبريدج: مطبعة جامعة كامبريدج. doi : 10.1017/CBO9780511676277 . ISBN 978-0-521-51729-4MR 2589550​​ ( مسودة من عام 2008 )

للمزيد من القراءة

  • بوس، صموئيل ، "الحساب المحدود"، بيبليوبوليس، نابولي، إيطاليا، 1986.
  • كوك، ستيفن ؛ نغوين، فونغ (2010)، الأسس المنطقية لتعقيد البرهان ، وجهات نظر في المنطق، كامبريدج: مطبعة جامعة كامبريدج، doi : 10.1017/CBO9780511676277 ، ISBN 978-0-521-51729-4، MR 2589550 ( مسودة من عام 2008 )
  • كرايتشيك، يان (1995)، الحساب المحدود، والمنطق الافتراضي، ونظرية التعقيد ، مطبعة جامعة كامبريدج
  • كرايتشيك، جان، إثبات التعقيد ، مطبعة جامعة كامبريدج، 2019.
  • بودلاك، بافيل (2013)، الأسس المنطقية للرياضيات والتعقيد الحسابي، مقدمة مبسطة ، سبرينغر
  • هاجيك، بيتر ؛ بودلاك، بافيل (2016). ما وراء الرياضيات في الحساب من الدرجة الأولى . منظورات في المنطق. مطبعة جامعة كامبريدج. ISBN 978-1-107-16841-1. OCLC 982287942 .