حساب بريسبرغر

حساب بريسبرغر هو نظرية من الدرجة الأولى للأعداد الطبيعية مع الجمع ، سُميت تكريمًا لموجيز بريسبرغر الذي قدمها عام ١٩٢٩. يحتوي توقيع حساب بريسبرغر على عمليتي الجمع والمساواة فقط ، مع إهمال عملية الضرب تمامًا. يمكن وضع بديهيات حسابية لهذه النظرية ؛ وتشمل هذه البديهيات مخططًا للاستقراء .

تُعدّ حسابات بريسبرغر أضعف بكثير من حسابات بيانو ، التي تشمل عمليات الجمع والضرب. وعلى عكس حسابات بيانو، تُعتبر حسابات بريسبرغر نظرية قابلة للتقرير . وهذا يعني أنه من الممكن تحديد ما إذا كانت أي جملة في لغة حسابات بريسبرغر قابلة للإثبات من بديهيات هذه الحسابات، وذلك باستخدام خوارزمية محددة. مع ذلك، فإن التعقيد الحسابي التقاربي لوقت تشغيل هذه الخوارزمية هو على الأقل ضعف التعقيد الأسي ، كما أوضح فيشر ورابين (1974) .

ملخص

تحتوي لغة حساب بريسبورغر على ثوابت.0{\displaystyle 0}و1{\displaystyle 1}ودالة ثنائية+{\displaystyle +}، تُفسَّر على أنها إضافة.

في هذه اللغة، فإن بديهيات حساب بريسبورغر هي الإغلاقات الشاملة لما يلي: [ 1 ]

  1. ¬(0=x+1){\displaystyle \neg (0=x+1)}[ ن 1 ]
  2. x+1=y+1x=y{\displaystyle x+1=y+1\to x=y}
  3. x+0=x{\displaystyle x+0=x}
  4. x+(y+1)=(x+y)+1{\displaystyle x+(y+1)=(x+y)+1}
  5. يتركP(x){\displaystyle P(x)}لتكن صيغة من الدرجة الأولى في لغة حساب بريسبرغر مع متغير حرx{\displaystyle x}(وربما متغيرات حرة أخرى). عندئذٍ، تُعتبر الصيغة التالية بديهية:
(P(0)x(P(x)P(x+1)))yP(y).{\displaystyle (P(0)\land \forall x(P(x)\to P(x+1)))\to \forall y\,P(y).}

(5) هو مخطط بديهي للاستقراء ، يمثل عددًا لا نهائيًا من البديهيات. لا يمكن استبدال هذه البديهيات بأي عدد محدود من البديهيات، أي أن حساب بريسبرغر غير قابل للتأصيل البديهي المحدود في منطق الرتبة الأولى. [ 2 ]

يمكن النظر إلى حساب بريسبرغر على أنه نظرية من الدرجة الأولى تتضمن المساواة، وتحتوي تحديدًا على جميع نتائج البديهيات المذكورة أعلاه. أو يمكن تعريفه، بدلاً من ذلك، بأنه مجموعة الجمل الصحيحة في التفسير المقصود : بنية الأعداد الصحيحة غير السالبة ذات الثوابت.0{\displaystyle 0}،1{\displaystyle 1}وجمع الأعداد الصحيحة غير السالبة.

صُممت حسابات بريسبرغر لتكون كاملة وقابلة للتقرير. لذلك، لا يمكنها صياغة مفاهيم مثل قابلية القسمة أو أولية الأعداد ، أو بشكل أعم، أي مفهوم عددي يؤدي إلى ضرب المتغيرات. ومع ذلك، يمكنها صياغة حالات فردية من قابلية القسمة؛ على سبيل المثال، تثبتxy((y+y=x)(y+y+1=x)).\forall x\,\exists y\;((y+y=x)\lor (y+y+1=x)).هذا يعني أن كل عدد إما زوجي أو فردي.

ملكيات

أثبت بريسبرغر (1929) أن حساب بريسبرغر هو:

  • متسق : لا توجد عبارة في حساب بريسبرغر يمكن استنتاجها من البديهيات بحيث يمكن استنتاج نفيها أيضًا.
  • كامل : بالنسبة لكل عبارة في لغة حساب بريسبورغر، إما أن يكون من الممكن استنتاجها من البديهيات أو من الممكن استنتاج نفيها.
  • قابل للتقرير : توجد خوارزمية تقرر ما إذا كانت أي عبارة معينة في حساب بريسبرجر نظرية أم لا نظرية - لاحظ أن "اللا نظرية" هي صيغة لا يمكن إثباتها، وليس بالضرورة بشكل عام صيغة يمكن إثبات نفيها، ولكن في حالة نظرية كاملة كما هو الحال هنا يكون التعريفان متكافئين.

يمكن إثبات قابلية حسم حساب بريسبرغر باستخدام حذف الكميات ، مدعومًا بالاستدلال حول التطابق الحسابي . [ 3 ] [ 4 ] [ 5 ] [ 6 ] [ 7 ] [ 8 ] يمكن استخدام الخطوات المستخدمة لتبرير خوارزمية حذف الكميات لتعريف بديهيات قابلة للحساب لا تحتوي بالضرورة على مخطط بديهيات الاستقراء. [ 3 ] [ 9 ]

في المقابل، فإن حساب بيانو ، وهو حساب بريسبورغر معزز بالضرب، غير قابل للتقرير، كما أثبت تشيرش إلى جانب الإجابة السلبية لمسألة القرار . وبحسب نظرية عدم الاكتمال لغودل ، فإن حساب بيانو غير مكتمل، ولا يمكن إثبات اتساقه داخليًا (لكن انظر برهان الاتساق لجينتزن ).

التعقيد الحسابي

تُعدّ مسألة القرار في حساب بريسبرغر مثالًا مثيرًا للاهتمام في نظرية التعقيد الحسابي والحوسبة . لنفترض أن n هو طول عبارة في حساب بريسبرغر. عندئذٍ، أثبت فيشر ورابين (1974) أنه في أسوأ الحالات، يكون طول برهان العبارة في منطق الرتبة الأولى على الأقل n.22جن{\displaystyle 2^{2^{cn}}}، لبعض الثوابت c > 0. وبالتالي، فإن خوارزمية القرار الخاصة بهم لحساب بريسبرغر لها زمن تشغيل أسي على الأقل. كما أثبت فيشر ورابين أنه لأي بديهية معقولة (محددة بدقة في بحثهما)، توجد نظريات بطول n لها براهين بطول أسي مضاعف . ويشير عمل فيشر ورابين أيضًا إلى أنه يمكن استخدام حساب بريسبرغر لتعريف صيغ تحسب أي خوارزمية بشكل صحيح طالما أن المدخلات أقل من حدود كبيرة نسبيًا. ويمكن زيادة هذه الحدود، ولكن فقط باستخدام صيغ جديدة.

وقد تناولت الدراسات الحديثة أيضاً مشاكل التركيب الوظيفي المتعلقة بحساب بريسبرغر، بما في ذلك تحديد الأجزاء المقيدة باستخدام إجراءات حل أكثر كفاءة. [ 10 ]

من ناحية أخرى، أثبت أوبن وجود حد أعلى أسي ثلاثي لإجراء اتخاذ القرار في حساب بريسبرغر. [ 11 ] [ n2 ]

أظهر بيرمان (1980) حدًا أكثر دقة للتعقيد باستخدام فئات التعقيد المتناوبة . وقد ثبت أن مجموعة العبارات الصحيحة في حساب بريسبرغر (PA) كاملة بالنسبة لـ TimeAlternations (2 2 n O(1) , n). وبالتالي، يقع تعقيدها بين زمن أسي مزدوج غير حتمي (2-NEXP) ومساحة أسية مزدوجة (2-EXPSPACE). ويتحقق الاكتمال في ظل اختزالات كارب . (تجدر الإشارة أيضًا إلى أنه على الرغم من أن حساب بريسبرغر يُختصر عادةً إلى PA، إلا أن PA في الرياضيات عمومًا تعني عادةً حساب بيانو ).

للحصول على نتيجة أكثر دقة، لنفترض أن PA(i) هي مجموعة عبارات PA الصحيحة من النوع Σ i ، وPA(i, j) هي مجموعة عبارات PA الصحيحة من النوع Σ i مع تقييد كل كتلة مُكمِّمة بـ j متغير. يُعتبر الرمز '<' خاليًا من المُكمِّمات؛ هنا، تُحسب المُكمِّمات المحدودة كمُكمِّمات. تنتمي PA(1, j) إلى P، بينما PA(1) هي مسألة NP-كاملة. [ 12 ] بالنسبة لـ i > 0 و j > 2، فإن PA(i + 1, j) هي مسألة Σ i P- كاملة . تتطلب نتيجة الصعوبة فقط j>2 (بدلاً من j=1) في كتلة المُكمِّمات الأخيرة. بالنسبة لـ i>0، فإن PA(i+1) هي مسألة Σ i EXP- كاملة . [ 13 ]

قصيرΣن{\displaystyle \Sigma _{n}}حساب بريسبورغر (ن>2{\displaystyle n>2}) يكونΣن-2P{\displaystyle \Sigma _{n-2}^{P}}كامل (وبالتالي NP كامل لـن=3{\displaystyle n=3}هنا، تتطلب كلمة "قصير" أن تكون محدودة (أييا(1){\displaystyle O(1)}حجم الجملة ) باستثناء أن الثوابت العددية غير محدودة (لكن عدد بتاتها في النظام الثنائي يُحتسب ضمن حجم الإدخال). أيضًا،Σ2{\displaystyle \Sigma _{2}}مسألة PA ذات المتغيرين (دون اشتراط كونها "قصيرة") هي مسألة NP-كاملة. [ 14 ] قصيرةΠ2{\displaystyle \Pi _{2}}(وبالتاليΣ2{\displaystyle \Sigma _{2}}) PA موجود في P، وهذا يمتد إلى البرمجة الخطية العددية البارامترية ذات الأبعاد الثابتة. [ 15 ]

التطبيقات

نظرًا لأن حساب بريسبرغر قابل للتقرير، توجد برامج إثبات نظريات آلية خاصة به. على سبيل المثال، يتميز نظاما Rocq و Lean المساعدان للإثبات بتكتيك أوميغا لحساب بريسبرغر، بينما يحتوي برنامج Isabelle المساعد للإثبات على إجراء مُثبت لإزالة المُكمِّمات من قِبل نيبكو (2010) . إن التعقيد الأسي المزدوج للنظرية يجعل استخدام برامج إثبات النظريات على الصيغ المعقدة غير عملي، ولكن هذا السلوك يحدث فقط في وجود مُكمِّمات متداخلة: يصف نيلسون وأوبن (1978) برنامج إثبات نظريات آليًا يستخدم خوارزمية سيمبلكس على حساب بريسبرغر موسع بدون مُكمِّمات متداخلة لإثبات بعض حالات صيغ حساب بريسبرغر الخالية من المُكمِّمات. تستخدم برامج حل مسائل الإرضاء المعياري الحديثة تقنيات البرمجة العددية الكاملة للتعامل مع الجزء الخالي من المُكمِّمات من نظرية حساب بريسبرغر. [ 16 ]

يمكن لحسابات بريسبرغر التعبير عن الضرب بالثوابت، كاختصار للجمع المتكرر:جx=x+x++xج أوقات.{\displaystyle cx=\underbrace {x+x+\cdots +x} _{c{\text{ مرات}}}.}تندرج معظم حسابات فهرسة المصفوفات ضمن نطاق المسائل القابلة للتقرير. [ n 3 ] هذا النهج هو أساس خمسة أنظمة على الأقل لإثبات صحة برامج الحاسوب ، بدءًا من مدقق ستانفورد باسكال في أواخر السبعينيات واستمرارًا حتى نظام Spec# من مايكروسوفت في عام 2005.

علاقة عددية قابلة للتعريف بواسطة بريسبرغر

سنقدم الآن بعض الخصائص المتعلقة بالعلاقات بين الأعداد الصحيحة القابلة للتعريف في حساب بريسبرغر. ولتبسيط الأمر، فإن جميع العلاقات المذكورة في هذا القسم تتعلق بالأعداد الصحيحة غير السالبة.

تكون العلاقة قابلة للتعريف وفقًا لبريسبرغر إذا وفقط إذا كانت مجموعة شبه خطية . [ 17 ]

علاقة عددية أحاديةR{\displaystyle R}أي أن مجموعة من الأعداد الصحيحة غير السالبة قابلة للتعريف وفقًا لبريسبرغر إذا وفقط إذا كانت دورية في نهاية المطاف. أي إذا وُجد حد فاصلتشمال{\displaystyle t\in \mathbb {N} }وفترة إيجابيةصشمال>0{\displaystyle p\in \mathbb {N} ^{>0}}بحيث يكون لكل عدد صحيحن{\displaystyle n}بحيث|ن|ت{\displaystyle |n|\geq t}،نR{\displaystyle n\in R}إذا وفقط إذان+صR{\displaystyle n+p\in R}.

بحسب نظرية كوبام-سيمينوف ، تكون العلاقة قابلة للتعريف وفقًا لبريسبرغر إذا وفقط إذا كانت قابلة للتعريف في حساب بوشي ذي الأساسك{\displaystyle k}للجميعك2{\displaystyle k\geq 2}[ 18 ] [ 19 ] علاقة قابلة للتعريف في حساب بوشي ذي الأساسك{\displaystyle k}وك{\displaystyle k'}لك{\displaystyle k}وك{\displaystyle k'}إن كون الأعداد الصحيحة مستقلة ضربياً هو قابل للتعريف وفقًا لبريسبرغر.

علاقة عددية صحيحةR{\displaystyle R}تكون مجموعة الأعداد الصحيحة قابلة للتعريف وفقًا لمنطق بريسبرغر إذا وفقط إذا كانت جميع مجموعات الأعداد الصحيحة القابلة للتعريف في منطق الرتبة الأولى مع الجمع وR{\displaystyle R}(أي، حساب بريسبرغر بالإضافة إلى مسند لـR{\displaystyle R}يمكن تعريفها وفقًا لبريسبرغر. [ 20 ] وبالمثل، لكل علاقةR{\displaystyle R}لا يمكن تعريف ذلك باستخدام طريقة بريسبرغر، ولكن توجد صيغة من الدرجة الأولى مع الجمع وR{\displaystyle R}التي تحدد مجموعة من الأعداد الصحيحة التي لا يمكن تعريفها باستخدام الجمع فقط.

تكون الدالة الصحيحة قابلة للتعريف وفقًا لـ Presburger إذا وفقط إذا كانت خطية مجزأة على تجزئة شبه خطية لمجالها، مع وجود مكون دوري في كل جزء خطي. [ 21 ]

وصف موشنيك للشخصية

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

يتركRشمالد{\displaystyle R\subseteq \mathbb {N} ^{d}}أن تكون مجموعة، القسمxأنا=ج{\displaystyle x_{i}=j}لR{\displaystyle R}، لأنا<د{\displaystyle i<d}وجشمال{\displaystyle j\in \mathbb {N} }يُعرَّف بأنه

{(x0،...،xأنا-1،xأنا+1،...،xد-1)شمالد-1|(x0،...،xأنا-1،ج،xأنا+1،...،xد-1)R}.{\displaystyle \left\{(x_{0},\ldots ,x_{i-1},x_{i+1},\ldots ,x_{d-1})\in \mathbb {N} ^{d-1}\mid (x_{0},\ldots ,x_{i-1},j,x_{i+1},\ldots ,x_{d-1})\in R\right\}.}

بفرض وجود مجموعتينR،Sشمالد{\displaystyle R,S\subseteq \mathbb {N} ^{d}}و أد{\displaystyle d}مجموعة من الأعداد الصحيحة(ص0،...،صد-1)شمالد{\displaystyle (p_{0},\ldots ,p_{d-1})\in \mathbb {N} ^{d}}المجموعةR{\displaystyle R}يُطلق عليه اسم(ص0،...،صد-1){\displaystyle (p_{0},\dots ,p_{d-1})}- دوري فيS{\displaystyle S}إذا، من أجل الجميع(x0،...،xد-1)S{\displaystyle (x_{0},\dots ,x_{d-1})\in S}بحيث(x0+ص0،...،xد-1+صد-1)S،{\displaystyle (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in S,}ثم(x0،...،xد-1)R{\displaystyle (x_{0},\ldots ,x_{d-1})\in R}إذا وفقط إذا(x0+ص0،...،xد-1+صد-1)R{\displaystyle (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in R}. لsشمال{\displaystyle s\in \mathbb {N} }المجموعة R{\displaystyle R}يقال إنهs{\displaystyle s}- دوري فيS{\displaystyle S}إذا كان(ص0،...،صد-1){\displaystyle (p_{0},\ldots ,p_{d-1})}-دوري بالنسبة للبعض(ص0،...،صد-1)Zد{\displaystyle (p_{0},\dots ,p_{d-1})\in \mathbb {Z} ^{d}}بحيث

أنا=0د-1|صأنا|<s.{\displaystyle \sum _{i=0}^{d-1}|p_{i}|<s.}

وأخيراً، بالنسبة لـك،x0،...،xد-1شمال{\displaystyle k,x_{0},\dots ,x_{d-1}\in \mathbb {N} }يترك

ج(ك،(x0،...،xد-1))={(x0+ج0،...،xد-1+جد-1)|0جأنا<ك}{\displaystyle C(k,(x_{0},\ldots ,x_{d-1}))=\left\{(x_{0}+c_{0},\dots ,x_{d-1}+c_{d-1})\mid 0\leq c_{i}<k\right\}}

يرمز إلى مكعب بحجمك{\displaystyle k}ركنه الأصغر هو(x0،...،xد-1){\displaystyle (x_{0},\dots ,x_{d-1})}.

نظرية موشنيك Rشمالد{\displaystyle R\subseteq \mathbb {N} ^{d}}يمكن تعريفها وفقًا لنموذج بريسبرغر إذا وفقط إذا:

  • لود>1{\displaystyle d>1}ثم جميع أقسامR{\displaystyle R}يمكن تعريفها وفقًا لمنهج بريسبرغر و
  • يوجدsشمال{\displaystyle s\in \mathbb {N} }بحيث يكون لكلكشمال{\displaystyle k\in \mathbb {N} }، يوجدتشمال{\displaystyle t\in \mathbb {N} }بحيث يكون ذلك لجميع(x0،...،xد-1)شمالد{\displaystyle (x_{0},\dots ,x_{d-1})\in \mathbb {N} ^{d}}معأنا=0د-1xأنا>ت،{\displaystyle \sum _{i=0}^{d-1}x_{i}>t,}R{\displaystyle R}يكونs{\displaystyle s}- دوري فيج(ك،(x0،...،xد-1)){\displaystyle C(k,(x_{0},\dots ,x_{d-1}))}.

بشكل بديهي، العدد الصحيحs{\displaystyle s}يمثل طول نوبة العمل، وهو عدد صحيحك{\displaystyle k}حجم المكعبات وت{\displaystyle t}يمثل هذا الحد الأدنى قبل الدورية. وتبقى هذه النتيجة صحيحة عندما يكون الشرط

أنا=0د-1xأنا>ت{\displaystyle \sum _{i=0}^{d-1}x_{i}>t}

يتم استبدالها إما بـمين(x0،...،xد-1)>ت{\displaystyle \min(x_{0},\ldots ,x_{d-1})>t}أو عن طريقالأعلى(x0،...،xد-1)>ت{\displaystyle \max(x_{0},\ldots ,x_{d-1})>t}.

أدى هذا التوصيف إلى ما يسمى "المعيار القابل للتحديد للتعريف في حساب بريسبرغر"، أي: توجد صيغة من الدرجة الأولى مع الجمع ود{\displaystyle d}-ary predicateR{\displaystyle R}هذا صحيح إذا وفقط إذاR{\displaystyle R}يُفسَّر ذلك بواسطة علاقة قابلة للتعريف وفقًا لبريسبرغر. كما تسمح نظرية موشنيك بإثبات أنه من الممكن تحديد ما إذا كان التسلسل التلقائي يقبل مجموعة قابلة للتعريف وفقًا لبريسبرغر.

انظر أيضاً

ملحوظات

  1. لا يوجد عدد إذا جمعه مع1{\displaystyle 1}، مما ينتج عنه0{\displaystyle 0}أي أن النظام لا يحتوي على أرقام سالبة.
  2. قام أوبن (1978) بتوسيع أوبن (1973) من خلال جعل التحليل دقيقًا وإظهار كيفية اعتماد الحد بالضبط على طول الصيغ.
  3. على سبيل المثال، في لغة البرمجة C ، إذافيمكن ترجمةaالتعبير، وهو ما يتناسب مع قيود حساب بريسبورغر.a[i]abaseadr+i+i+i+i

مراجع

فهرس

  • كوبهام، آلان (1969). "حول اعتماد مجموعات الأعداد القابلة للتمييز بواسطة الأوتوماتا المحدودة على الأساس". نظرية الأنظمة الرياضية . 3 (2): 186-192 . doi : 10.1007/BF01746527 . S2CID 19792434 . 
  • هاس، كريستوف (2014). "فئات فرعية من حساب بريسبرغر والتسلسل الهرمي للأس الضعيف". وقائع مؤتمر CSL- LICS . ACM. الصفحات  47:1–47:10. arXiv : 1401.5266 . doi : 10.1145/2603088.2603092 .
  • كينغ، تيم؛ باريت، كلارك دبليو؛ تينيلي، سيزار (2014). "الاستفادة من البرمجة الخطية والبرمجة الخطية المختلطة في تقنية التجميع السطحي". 2014 الأساليب الرسمية في التصميم بمساعدة الحاسوب (FMCAD) . المجلد  2014. الصفحات 139-146 . doi : 10.1109/FMCAD.2014.6987606 . ISBN  978-0-9835-6784-4. S2CID 5542629 . 
  • مونك، ج. دونالد (2012). المنطق الرياضي (نصوص الدراسات العليا في الرياضيات (37)) (طبعة غلاف ورقي معاد طباعتها من الطبعة الأولى الأصلية  لعام 1976). سبرينغر. ISBN 9781468494549.
  • نيلسون، جريج؛ أوبن، ديريك سي. (أبريل 1978). "مُبسِّط قائم على خوارزميات اتخاذ القرار الفعّالة". وقائع الندوة الخامسة لجمعية ACM SIGACT-SIGPLAN حول مبادئ لغات البرمجة - POPL '78 . الصفحات 141-150 . doi : 10.1145/512760.512775 . S2CID 6342372 .  
  • أوبن، ديريك سي. (1973). "حدود أولية لحساب بريسبرغر". وقائع الندوة السنوية الخامسة لجمعية آلات الحوسبة حول نظرية الحوسبة (STOC '73) . الصفحات 34-37 . doi : 10.1145/800125.804033 . 
  • بريسبرجر، موجيسز (1929). "Über die Vollständigkeit eines gwissen Systems der Arithmetik ganzer Zahlen، in welchem ​​die Addition als einzige Operation Hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves، وارسزاوا : 92–101 .انظر ستانسيفير (1984) للاطلاع على الترجمة الإنجليزية
  • بوغ، ويليام (1991). "اختبار أوميغا: خوارزمية برمجة عددية سريعة وعملية لتحليل التبعية". وقائع مؤتمر ACM/IEEE للحوسبة الفائقة لعام 1991 - الحوسبة الفائقة 91. نيويورك، نيويورك، الولايات المتحدة الأمريكية: رابطة آلات الحوسبة. الصفحات 4-13 . CiteSeerX 10.1.1.37.1995 . doi : 10.1145/125826.125848 . ISBN   0897914597. S2CID 3174094 . 
  • ريدي، سي آر؛ لوفلاند، دي دبليو (1978). "حساب بريسبرغر مع تناوب الكميات المحدود". وقائع الندوة السنوية العاشرة لجمعية آلات الحوسبة حول نظرية الحوسبة - STOC '78 . الصفحات 320-325 . doi : 10.1145/800133.804361 . S2CID 13966721 .  
  • يونغ، ب. (1985). "نظريات غودل، والصعوبة الأسية، وعدم قابلية حسم النظريات الحسابية: عرض". في أ. نيرود و ر. شور (محرران). نظرية الاستدعاء الذاتي، الجمعية الرياضية الأمريكية . ص 503-522 .