هل تعني الشريعة تطبيعًا ضعيفًا؟

Question

سياق:نظرية النوع.

فهمي ل:

• ون:يمكن إعادة كتابة كل مصطلح إلى NF.
• القانونيّة:تتم إعادة كتابة كل مصطلح في شكل قانوني.

ثم يؤدي ذلك إلى حدس حيث إذا كانت القانونيّة صحيحة، فسنحصل على NF = النموذج الكنسي وبالتالي يحمل WN.ومع ذلك، لا أرى الناس يذكرون هذا كثيرًا، مثل هذا السؤال يتحدث عن القانون القانوني ولكنه لا يذكر أبدًا NF أو التطبيع.على nLab, ، يُقال إن الشكل المتعارف عليه هو الشكل العادي، وهو ما يبرر تخميني "NF = النموذج المتعارف عليه" ولكنه لا يشير إلى أن WN يحمل ذلك.لذلك أنا أشك في حدسي.

لذا، أتساءل عما إذا كان هذا صحيحًا (هل هناك دليل؟)، أو إذا كان خطأ (هل هناك مثال مضاد؟).

Answer 1

Canonicity لا يعني التطبيع الضعيف.أولاً، اسمحوا لي أن أصيغ التعريفات المعنية بشكل أكثر دقة:

• ون:كل مصطلح مفتوح يمكن اختزاله إلى مصطلح عادي
• القانونيّة:كل حد مغلق يمكن اختزاله إلى حد قانوني

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

المصطلحات العادية والكنسي ليست هي نفسها.على سبيل المثال، x متغير في x : Bool السياق طبيعي ولكنه ليس قانونيًا.وكذلك الأجل المغلق λ(b : Bool). if true then b else b هو الكنسي ولكن ليس طبيعيا.

تتمتع نظرية النوع الممتد بخاصية القانونية ولكن ليس WN أو SN أو الوجود الفريد للأشكال العادية.وذلك لأنه في ETT من الممكن إضافة مساواة تعريفية غير متناسقة إلى السياق، أو إضافة نظرية معادلة لنظام تورينج الكامل.على سبيل المثال، في سياق ETT n : Nat, p : n = suc n ال n المتغير ليس له شكل عادي فريد، منذ ذلك الحين n يمكن توسيعها بشكل تعسفي باستخدام p.

ومع ذلك، إذا كان لدينا مصطلح ETT مغلق، فلا يمكن أن يكون لدينا أي شيء مراوغ في السياق، لذلك لا يزال من الممكن تقييم المصطلح المغلق إلى نموذج أساسي.