خوارزمية الشكل الناظمي وتطبيقاتها

قدّم الدرس عن الأشكال الناظمية برهانين على وجودها. يمرّ الأول بجدول الصدق، الذي له $2^n$ سطرًا لـ$n$ من المتغيرات؛ ويجتاز الثاني الصيغة بدءًا من المتغيرات متّبعًا قاعدة تكوينها الوحيدة. ولا يقول أيٌّ منهما كيف نتصرف أمام صيغة مكتوبة باستلزامات واستلزامات مزدوجة ونفي متداخل، وهي الهيئة التي تُقدَّم بها الصيغ عادةً. وإذا كان الأمر كذلك، فإنه ينقصنا إجراء يعمل على الكتابة نفسها، ويمكن تنفيذه دون تفكير، ويُعلم عنه أنه يتوقف وأنه يعطي صيغة مكافئة. وذلك هو الخوارزمية، ودراستها هي الموضوع الأول لهذا الدرس؛ والثاني هو ما يُصنع بها: وصف سلوك جهاز بصيغ، وبناء دارة تعيد إنتاجه.

الكتابات والإبدال

لنتذكر أن صيغ الدورة سلاسل من الدوائر والأقراص، وأن $\neg$ و$\vee$ و$\wedge$ و$\rightarrow$ و$\leftrightarrow$ و$\veebar$ اختصارات معرَّفة انطلاقًا من النفي المشترك (الدرس عن لغة منطق القضايا). فحين نكتب $((p \vee q) \rightarrow (\neg q \wedge p))$ لا نكتب السلسلة، بل كتابة لها: شجرة أوراقها متغيرات وعُقدها الروابط $\neg$ و$\wedge$ و$\vee$ و$\rightarrow$ و$\leftrightarrow$ و$\veebar$ و$\downarrow$، لكلٍّ منها مكوّناته. وكل كتابة تدلّ على صيغة واحدة، هي التي تنتج عن بسط اختصاراتها؛ وقد يكون للصيغة الواحدة عدة كتابات: فقد لاحظ الدرس عن الأشكال الناظمية أن $\neg\neg\varphi$ و$(\varphi \vee \varphi)$ هما السلسلة نفسها. والخوارزمية تقرأ الكتابة لا السلسلة؛ ولذلك يحسن التمييز بينهما. ولأن التمييز لا يهمّ إلا لمعرفة أين تعمل كل خطوة، سنستعمل الحروف $\varphi$ و$\psi$ و$\chi$ للكتابات وللصيغ التي تدلّ عليها، وسنكتب $\varphi \eqsem \psi$ حين تكون الصيغ المدلول عليها متكافئة دلاليًا. والكتابة الجزئية من كتابةٍ هي الشجرة الجزئية التي جذرها إحدى عُقدها.

تُبدل خطوةٌ من الخوارزمية كتابةً جزئية بأخرى. والأداة التي تضمن أن هذا التغيير لا يغيّر المعنى هي مبرهنة الإبدال الدلالي من الدرس عن النتيجة الدلالية والتكافؤ الدلالي؛ لكن تلك المبرهنة تُبدل ورودًا واحدًا في السلسلة، وقد تقابل الكتابةَ الجزئية عدةُ ورودات في السلسلة، لأن كل اختصار ينسخ مكوّناته: ففي $(\varphi \vee \psi) = ((\varphi \downarrow \psi) \downarrow (\varphi \downarrow \psi))$ يرد المكوّن $\varphi$ مرتين. والتوطئة الآتية تكيّف الإبدال مع الكتابات.

هنا $F_c$ دالة الصدق للرابط: $F_\neg(a) = 1 - a$، و$F_\wedge(a, b) = ab$، وهكذا مع البقية. وتُنال النتيجة نفسها من مبرهنة الإبدال الدلالي بتطبيقها مرة لكل نسخة من $\theta$ في السلسلة وربط التكافؤات بالتعدي؛ والبرهان بالكتابة أقصر لأنه يعدّ الروابط المكتوبة لا النسخ.