ในการเขียนใหม่แบบนามธรรม^{[ 1 ]}วัตถุจะอยู่ในรูปแบบปกติหากไม่สามารถเขียนใหม่ได้อีกต่อไป กล่าวคือไม่สามารถลดทอนได้ ขึ้นอยู่กับระบบการเขียนใหม่ วัตถุอาจเขียนใหม่เป็นรูปแบบปกติได้หลายรูปแบบหรือไม่มีเลย คุณสมบัติหลายอย่างของระบบการเขียนใหม่เกี่ยวข้องกับรูปแบบปกติ

กล่าวอย่างเป็นทางการ ถ้า ( A ,→) เป็นระบบการเขียนใหม่แบบนามธรรม x ∈ Aจะอยู่ในรูปแบบปกติก็ต่อเมื่อไม่มีy ∈ Aใดๆ ที่ทำให้x → y กล่าวคือxเป็นพจน์ที่ไม่สามารถแยกย่อยได้

วัตถุa นั้นเป็นการทำให้เป็นปกติแบบอ่อนหากมีลำดับการเขียนใหม่ที่เฉพาะเจาะจงอย่างน้อยหนึ่งลำดับที่เริ่มต้นจากaซึ่งในที่สุดจะให้รูปแบบปกติ ระบบการเขียนใหม่มีคุณสมบัติการทำให้เป็นปกติแบบอ่อนหรือเป็นการทำให้เป็นปกติแบบอ่อน (WN) หากวัตถุทุกตัวเป็นการทำให้เป็นปกติแบบอ่อน วัตถุa นั้นเป็นการทำให้เป็นปกติแบบเข้มแข็งหากลำดับการเขียนใหม่ทุกลำดับที่เริ่มต้นจากaในที่สุดจะสิ้นสุดด้วยรูปแบบปกติ ระบบการเขียนใหม่เป็นการทำให้เป็นปกติแบบเข้มแข็งสิ้นสุดโนเธอร์เรียนหรือมีคุณสมบัติการทำให้เป็นปกติแบบเข้มแข็ง (SN) หากวัตถุแต่ละตัวเป็นการทำให้เป็นปกติแบบเข้มแข็ง^{[ 2 ]}

ระบบการเขียนใหม่มีคุณสมบัติรูปแบบปกติ (NF) ถ้าสำหรับวัตถุaและรูปแบบปกติbทั้งหมดbสามารถเข้าถึงได้จากaโดยชุดของการเขียนใหม่และการเขียนใหม่แบบผกผันก็ต่อเมื่อaลดลงเหลือb เท่านั้น ระบบการเขียนใหม่มีคุณสมบัติรูปแบบปกติที่ไม่ซ้ำกัน (UN) ถ้าสำหรับรูปแบบปกติa , b ∈ Sทั้งหมดaสามารถเข้าถึงได้จากbโดยชุดของการเขียนใหม่และการเขียนใหม่แบบผกผันก็ต่อเมื่อaเท่ากับb เท่านั้น ระบบการเขียนใหม่มี คุณสมบัติรูป ^แบบปกติที่ไม่ซ้ำกันเมื่อเทียบกับการลดรูป (UN ^{→ ) ถ้าสำหรับทุกเทอม ที่}ลดลงเหลือรูปแบบปกติaและb a เท่ากับb ^[ 3 ]

ส่วนนี้จะนำเสนอผลลัพธ์ที่เป็นที่รู้จักกันดีบางประการ ประการแรก SN หมายถึง WN ^{[ 4 ]}

การบรรจบกัน (ย่อว่า CR) หมายความว่า NF หมายความว่า UN หมายความว่า UN → ^{[ 3 ] โดย}ทั่วไปแล้วการบ่งชี้แบบย้อนกลับจะไม่เกิดขึ้น {a→b,a→c,c→c,d→c,d→e} เป็น UN ^→แต่ไม่ใช่ UN เนื่องจาก b=e และ b,e เป็นรูปแบบปกติ {a→b,a→c,b→b} เป็น UN แต่ไม่ใช่ NF เนื่องจาก b=c, c เป็นรูปแบบปกติ และ b ไม่ลดรูปเป็น c {a→b,a→c,b→b,c→c} เป็น NF เนื่องจากไม่มีรูปแบบปกติ แต่ไม่ใช่ CR เนื่องจาก a ลดรูปเป็น b และ c และ b,c ไม่มีตัวลดรูปร่วมกัน

WN และ UN ^→บ่งชี้ถึงการบรรจบกัน ดังนั้น CR, NF, UN และ UN ^→จะตรงกันหาก WN เป็นจริง^{[ 5 ]}

ตัวอย่างหนึ่งคือ การทำให้การแสดงออกทางคณิตศาสตร์ง่ายขึ้นจะได้ตัวเลข - ในทางคณิตศาสตร์ ตัวเลขทั้งหมดเป็นรูปแบบปกติ ข้อเท็จจริงที่น่าทึ่งคือ การแสดงออกทางคณิตศาสตร์ทั้งหมดมีค่าที่ไม่ซ้ำกัน ดังนั้นระบบการเขียนใหม่จึงเป็นการทำให้เป็นมาตรฐานและมีความสอดคล้องกันอย่างมาก: ^{[ 6 ]}

(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24

(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24

ตัวอย่างของระบบที่ไม่ทำให้เป็นมาตรฐาน (ไม่อ่อนหรือแข็ง) ได้แก่ การนับไปสู่อนันต์ (1 ⇒ 2 ⇒ 3 ⇒ ...) และลูป เช่น ฟังก์ชันการแปลงของสมมติฐานคอลลาทซ์ (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ... ซึ่งเป็นปัญหาที่ยังเปิดอยู่ว่ามีลูปอื่น ๆ ของการแปลงคอลลาทซ์หรือไม่) ^{[ 7 ]}อีกตัวอย่างหนึ่งคือระบบกฎเดียว { r ( x , y ) →  r ( y , x ) } ซึ่งไม่มีคุณสมบัติการทำให้เป็นมาตรฐาน เนื่องจากจากเทอมใด ๆ เช่นr (4,2) ลำดับการเขียนใหม่เพียงลำดับเดียวจะเริ่มต้นขึ้น นั่นคือr (4,2) →  r (2,4) →  r (4,2) →  r (2,4) → ... ซึ่งยาวเป็นอนันต์ สิ่งนี้นำไปสู่แนวคิดของการเขียนใหม่ "โมดูลัสการสลับที่ " โดยที่เทอมอยู่ในรูปแบบมาตรฐานหากไม่มีกฎใด ๆ นอกจากการสลับที่^{[ 8 ]}

ระบบ { b → a , b → c , c → b , c → d } (ดังภาพ) เป็นตัวอย่างของระบบที่ทำให้เกิดการจัดเรียงแบบปกติอย่างอ่อน แต่ไม่ใช่แบบแข็งaและdเป็นรูปแบบปกติ และbและcสามารถลดรูปเป็นaหรือdได้ แต่การลดรูปอนันต์b → c → b → c → ... หมายความว่าทั้งbและcไม่ใช่แบบแข็ง

แคลคูลัสแลมบ์ดาแบบไม่มีประเภทบริสุทธิ์ไม่เป็นไปตามคุณสมบัติการทำให้เป็นมาตรฐานที่เข้มงวด และแม้แต่คุณสมบัติการทำให้เป็นมาตรฐานที่อ่อนแอ พิจารณาเทอม(การประยุกต์ใช้เป็นแบบสมาคมซ้าย ) มันมีกฎการเขียนใหม่ดังต่อไปนี้: สำหรับเทอมใดๆ ${\displaystyle \lambda x.xxx}$${\displaystyle t}$

${\displaystyle (\mathbf {\lambda } x.xxx)t\rightarrow ttt}$

แต่ลองพิจารณาดูว่าจะเกิดอะไรขึ้นเมื่อเรานำไปใช้กับตัวมันเอง: ${\displaystyle \lambda x.xxx}$

${\displaystyle {\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \cdots \,\end{aligned}}}$

ดังนั้น เทอมนี้จึงไม่ทำให้เป็นมาตรฐานอย่างเข้มแข็ง และนี่เป็นลำดับการลดรูปเพียงลำดับเดียว ดังนั้นจึงไม่ใช่การทำให้เป็นมาตรฐานอย่างอ่อนด้วยเช่นกัน ${\displaystyle (\lambda x.xxx)(\lambda x.xxx)}$

ระบบแคลคูลัสแลมบ์ดาแบบมีชนิดข้อมูล ต่างๆ รวมถึง แคลคูลัสแลมบ์ดาแบบมีชนิดข้อมูลอย่างง่ายระบบ FของJean-Yves Girardและแคลคูลัสการสร้างของThierry Coquandล้วนเป็นระบบที่ทำให้เป็นมาตรฐานอย่างเข้มแข็ง

ระบบแคลคูลัสแลมบ์ดาที่มีคุณสมบัติการทำให้เป็นมาตรฐานสามารถมองได้ว่าเป็นภาษาโปรแกรมที่มีคุณสมบัติที่ว่าโปรแกรมทุกโปรแกรมจะสิ้นสุดแม้ว่านี่จะเป็นคุณสมบัติที่มีประโยชน์มาก แต่ก็มีข้อเสียคือ ภาษาโปรแกรมที่มีคุณสมบัติการทำให้เป็นมาตรฐานไม่สามารถสมบูรณ์แบบทัวริงได้ มิฉะนั้นเราจะสามารถแก้ปัญหาการหยุดทำงานได้โดยการดูว่าโปรแกรมตรวจสอบประเภทหรือไม่ ซึ่งหมายความว่ามีฟังก์ชันที่คำนวณได้ซึ่งไม่สามารถกำหนดได้ในแคลคูลัสแลมบ์ดาแบบกำหนดประเภทอย่างง่าย และในทำนองเดียวกันสำหรับแคลคูลัสของการสร้างและระบบ Fตัวอย่างทั่วไปคือตัวแปลตนเองในภาษาโปรแกรมทั้งหมด^{[ 10 ]}

• รูปแบบมาตรฐาน
• แคลคูลัสแลมบ์ดาแบบพิมพ์
• การเขียนใหม่
• การเขียนโปรแกรมเชิงฟังก์ชันโดยรวม
• การคาดเดาของบาเรนเดร็กต์–เกวแวร์–คล็อปป์
• บทพิสูจน์ของนิวแมน
• การทำให้เป็นมาตรฐานโดยการประเมิน