Confluence (การเขียนบทคัดย่อใหม่)

Q: การบรรจบกันของพื้นดิน

ระบบการเขียนเทอมใหม่จะ มีความสอดคล้องกัน หาก เทอม พื้นฐานทุกเทอม มีความสอดคล้องกัน นั่นคือเทอมทุกเทอมไม่มีตัวแปร [ 3 ]

ในวิทยาการคอมพิวเตอร์และคณิตศาสตร์การบรรจบกัน (confluence)เป็นคุณสมบัติของ ระบบ การเขียนใหม่ (rewriting system) ซึ่งอธิบายว่าเทอมใดในระบบดังกล่าวสามารถเขียนใหม่ได้มากกว่าหนึ่งวิธีเพื่อให้ได้ผลลัพธ์เดียวกัน บทความนี้อธิบายคุณสมบัติดังกล่าวในบริบทที่เป็นนามธรรมที่สุดของระบบการเขียนใหม่แบบนามธรรม (abstract rewriting system )

ตัวอย่างที่สร้างแรงบันดาลใจ

กฎทั่วไปของเลขคณิตพื้นฐานก่อให้เกิดระบบการเขียนใหม่แบบนามธรรม ตัวอย่างเช่น นิพจน์ (11 + 9) × (2 + 4) สามารถประเมินได้โดยเริ่มจากวงเล็บซ้ายหรือวงเล็บขวา อย่างไรก็ตาม ในทั้งสองกรณีจะได้ผลลัพธ์เดียวกันในที่สุด หากนิพจน์ทางคณิตศาสตร์ทุกนิพจน์ประเมินได้ผลลัพธ์เดียวกันโดยไม่คำนึงถึงกลยุทธ์การลดรูป ระบบการเขียนใหม่ทางคณิตศาสตร์นั้นเรียกว่าระบบที่สอดคล้องกับพื้นฐาน ระบบการเขียนใหม่ทางคณิตศาสตร์อาจสอดคล้องกับพื้นฐานหรือเป็นเพียงระบบที่สอดคล้องกับพื้นฐานเท่านั้น ขึ้นอยู่กับรายละเอียดของระบบการเขียนใหม่^{[ 1 ]}

ตัวอย่างที่สองซึ่งเป็นนามธรรมมากขึ้นได้มาจากการพิสูจน์ต่อไปนี้ขององค์ประกอบกลุ่ม แต่ละตัวที่เท่ากับ ส่วนกลับของส่วนกลับของมัน: ^{[ 2 ]}

สัจพจน์ของกลุ่ม
เอ1	1 ⋅ a	= a
เอ2	a ⁻¹ ⋅ a	= 1
เอ3	( a ⋅ b ) ⋅ c	= a ⋅ ( b ⋅ c )

พิสูจน์R4 : a ⁻¹ ⋅( a ⋅ b ) = b
	a ⁻¹ ⋅ ( a ⋅ b )
=	( a ⁻¹ ⋅ a ) ⋅ b	โดย A3(r)
=	1 ⋅ b	โดย A2
=	ข	โดย A1

พิสูจน์R6 : ( a ⁻¹ ) ⁻¹ ⋅ 1 = a
	( a ⁻¹ ) ⁻¹ ⋅ 1
=	( a ⁻¹ ) ⁻¹ ⋅ ( a ⁻¹ ⋅ a )	โดย A2(r)
=	เอ	โดย R4

พิสูจน์**R10** : ( a ⁻¹ ) ⁻¹ ⋅ b = a ⋅ b
	( a ⁻¹ ) ⁻¹ ⋅ b
=	( a ⁻¹ ) ⁻¹ ⋅ ( a ⁻¹ ⋅ ( a ⋅ b ))	โดย R4(r)
=	a ⋅ b	โดย R4

บทพิสูจน์ของ**R11** : a ⋅ 1 = a
	a ⋅ 1
=	( a ⁻¹ ) ⁻¹ ⋅ 1	โดย R10(r)
=	เอ	โดย R6

พิสูจน์**R12** : ( a ⁻¹ ) ⁻¹ = a
	( a ⁻¹ ) ⁻¹
=	( a ⁻¹ ) ⁻¹ ⋅ 1	โดย R11(r)
=	เอ	โดย R6

การพิสูจน์นี้เริ่มต้นจากสัจพจน์กลุ่ม A1–A3 ที่กำหนดให้ และสร้างข้อเสนอห้าข้อ ได้แก่ R4, R6, R10, R11 และ R12 โดยแต่ละข้อใช้ข้อเสนอก่อนหน้าบางส่วน และ R12 เป็นทฤษฎีบทหลัก การพิสูจน์บางส่วนต้องใช้ขั้นตอนที่ไม่ชัดเจน หรือแม้แต่ขั้นตอนที่สร้างสรรค์ เช่น การใช้สัจพจน์ A2 ในทางกลับกัน ทำให้สามารถเขียน "1" ใหม่เป็น " a ⁻¹ ⋅ a" ในขั้นตอนแรกของการพิสูจน์ R6 แรงจูงใจทางประวัติศาสตร์ประการหนึ่งในการพัฒนาทฤษฎีการเขียนเทอมใหม่ก็คือการหลีกเลี่ยงความจำเป็นในการใช้ขั้นตอนดังกล่าว ซึ่งยากที่จะค้นหาโดยมนุษย์ที่ไม่มีประสบการณ์ นับประสาอะไรกับโปรแกรมคอมพิวเตอร์

หากระบบการเขียนใหม่ของเทอมเป็นแบบต่อเนื่องและสิ้นสุดจะมีวิธีการที่ตรงไปตรงมาในการพิสูจน์ความเท่าเทียมกันระหว่างนิพจน์สองตัว (หรือที่เรียกว่าเทอม ) sและt : เริ่มต้นด้วยsใช้ความเท่าเทียมกัน^{[หมายเหตุ 1 ]}จากซ้ายไปขวาให้นานที่สุดเท่าที่จะทำได้ จนกระทั่งได้เทอม s′ ในที่สุดหาเทอมt′จากtในทำนองเดียวกัน หากเทอมs′และt′ตรงกันอย่างแท้จริง แสดงว่า sและtเท่ากัน ที่สำคัญกว่านั้น หากไม่ตรงกัน แสดงว่าsและtไม่สามารถเท่ากันได้ กล่าวคือ เทอมsและt ใดๆ ที่สามารถพิสูจน์ว่าเท่ากันได้ สามารถทำได้โดยวิธีนั้น

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

กรณีทั่วไปและทฤษฎี

ในแผนภาพนี้ $a$ สามารถลดรูปเป็น $b$ หรือ $c$ ได้โดยใช้ขั้นตอนการเขียนใหม่ศูนย์ขั้นตอนหรือมากกว่า (แสดงด้วยเครื่องหมายดอกจัน) เพื่อให้ความสัมพันธ์การเขียนใหม่เป็นแบบบรรจบกัน ตัวลดรูปทั้งสองจะต้องลด รูป เป็น $d$ ร่วมกันในที่สุด

ระบบการเขียนใหม่สามารถแสดงได้ในรูปกราฟแบบมีทิศทางโดยที่โหนดแทนนิพจน์ และขอบแทนการเขียนใหม่ ตัวอย่างเช่น ถ้านิพจน์aสามารถเขียนใหม่เป็นb ได้ เราจะกล่าวว่าbเป็นตัวลดรูปของa (หรืออีกนัยหนึ่งa ลดรูปเป็นbหรือaเป็นการขยายของb ) สิ่งนี้แสดงโดยใช้สัญลักษณ์ลูกศร; a → bแสดงว่าaลดรูปเป็นbโดยสัญชาตญาณแล้ว หมายความว่ากราฟที่เกี่ยวข้องมีขอบแบบมีทิศทางจากaไปยัง b

ถ้ามีเส้นทางเชื่อมระหว่างโหนดกราฟสองโหนดcและdเส้นทางนั้นจะก่อให้เกิดลำดับการลดรูปตัวอย่างเช่น ถ้าc → c′ → c′′ → ... → d′ → dเราสามารถเขียนได้ว่าc → c′′ → c′′*→dบ่งชี้ว่ามีลำดับการลดรูปจากcไปยังd อยู่ ในทางทฤษฎีแล้ว*→คือการปิดแบบสะท้อนและถ่ายทอดของ → โดยใช้ตัวอย่างจากย่อหน้าก่อนหน้า เรามี (11+9)×(2+4) → 20×(2+4) และ 20×(2+4) → 20×6 ดังนั้น (11+9)×(2+4)*→20×6.

เมื่อกำหนดเช่นนี้แล้ว การบรรจบกันสามารถนิยามได้ดังนี้a ∈ Sถือว่าบรรจบกันหากสำหรับทุกคู่b , c ∈ Sที่a*→บีและเอ*→cมีอยู่d ∈ Sที่มีb*→งและค*→d (แทนด้วย) ถ้าทุกa ∈ Sเป็นแบบบรรจบกัน เราจะกล่าวว่า → เป็นแบบบรรจบกัน คุณสมบัตินี้บางครั้งเรียกว่าคุณสมบัติเพชรตามรูปร่างของแผนภาพที่แสดงทางด้านขวา ผู้เขียนบางคนสงวนคำว่าคุณสมบัติเพชรไว้สำหรับรูปแบบหนึ่งของแผนภาพที่มีการลดรูปเพียงครั้งเดียวทุกที่ กล่าวคือ เมื่อใดก็ตามที่a → bและa → cจะต้องมีdที่ทำให้b → dและc → dรูปแบบที่มีการลดรูปเพียงครั้งเดียวมีความเข้มแข็งกว่ารูปแบบที่มีการลดรูปหลายครั้งอย่างเคร่งครัด $b\mathbin {\downarrow } c$

การบรรจบกันของพื้นดิน

ระบบการเขียนเทอมใหม่จะมีความสอดคล้องกันหาก เทอม พื้นฐานทุกเทอมมีความสอดคล้องกัน นั่นคือเทอมทุกเทอมไม่มีตัวแปร^{[ 3 ]}

จุดบรรจบในท้องถิ่น

กล่าวได้ว่าองค์ประกอบa ∈ S เป็น แบบรวมตัวกันในระดับท้องถิ่น (หรือรวมตัวกันอย่างอ่อน^{[ 5 ]} ) ถ้าสำหรับทุกb , c ∈ Sที่a → bและa → cจะมีd ∈ Sที่b*→งและค*→d . ถ้าทุกa ∈ Sเป็นจุดบรรจบกันเฉพาะที่ (locally confluence) แล้ว → จะเรียกว่าจุดบรรจบกันเฉพาะที่ หรือมีคุณสมบัติ Church–Rosser แบบอ่อน (weak Church–Rosser property ) ซึ่งแตกต่างจากจุดบรรจบ (confluence) ตรงที่bและcต้องถูกลดรูปมาจากaในขั้นตอนเดียว ในทำนองเดียวกัน บางครั้งจุดบรรจบก็ถูกเรียกว่าจุดบรรจบทั่วโลก (global confluence )

ความสัมพันธ์*→ซึ่งถูกนำมาใช้เป็นสัญลักษณ์สำหรับลำดับการลดรูป อาจมองได้ว่าเป็นระบบการเขียนใหม่ในตัวของมันเอง โดยมีความสัมพันธ์คือการปิดแบบสะท้อนและถ่ายทอดของ→เนื่องจากลำดับของลำดับการลดรูปก็คือลำดับการลดรูปอีกเช่นกัน (หรือเทียบเท่ากัน เนื่องจากการสร้างการปิดแบบสะท้อนและถ่ายทอดนั้นเป็นคุณสมบัติเอกลักษณ์ )**→=*→ดังนั้น → จะบรรจบกันก็ต่อเมื่อ*→เป็นจุดบรรจบกันในท้องถิ่น

ระบบการเขียนใหม่สามารถบรรจบกันได้ในระดับท้องถิ่นโดยไม่จำเป็นต้องบรรจบกันในระดับสากล ตัวอย่างแสดงในรูปที่ 1 และ 2 อย่างไรก็ตามทฤษฎีบทของนิวแมนกล่าวว่า หากระบบการเขียนใหม่ที่บรรจบกันในระดับท้องถิ่นไม่มีลำดับการลดขนาดอนันต์ (ซึ่งในกรณีนี้จะเรียกว่าเป็นระบบสิ้นสุดหรือเป็นระบบปกติอย่างเข้มแข็ง ) แล้วระบบนั้นจะบรรจบกันในระดับสากล

ทรัพย์สินของ Church–Rosser

กล่าวกันว่าระบบการเขียนใหม่มีคุณสมบัติ Church–Rosserก็ต่อเมื่อหมายความว่าสำหรับวัตถุx , yทั้งหมดAlonzo ChurchและJ. Barkley Rosserพิสูจน์ในปี 1936 ว่าแคลคูลัสแลมบ์ดามีคุณสมบัตินี้^[⁶^]ดังนั้นจึงเป็นที่มาของชื่อคุณสมบัตินี้^[⁷^] (ข้อเท็จจริงที่ว่าแคลคูลัสแลมบ์ดามีคุณสมบัตินี้ยังเป็นที่รู้จักกันในชื่อทฤษฎีบท Church–Rosser ) ในระบบการเขียนใหม่ที่มีคุณสมบัติ Church–Rosser ปัญหาคำพูดอาจลดลงเหลือเพียงการค้นหาผู้สืบทอดร่วม ในระบบ Church–Rosser วัตถุจะมีรูปแบบปกติอย่างมากที่สุดหนึ่งรูปแบบ นั่นคือรูปแบบปกติของวัตถุจะมีเอกลักษณ์เฉพาะหากมีอยู่ แต่ก็อาจไม่มีอยู่ก็ได้ ในแคลคูลัสแลมบ์ดา ตัวอย่างเช่น นิพจน์ (λx.xx)(λx.xx) ไม่มีรูปแบบปกติ เนื่องจากมีลำดับการลดรูปเบตาอนันต์ (λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ... ^[⁸^] $x{\stackrel {*}{\leftrightarrow }}y$ $x{\mathbin {\downarrow }}y$

ระบบการเขียนใหม่จะมีคุณสมบัติ Church–Rosser ก็ต่อเมื่อมีความสอดคล้อง กันเท่านั้น ^{[ 9 ]}เนื่องจากการเทียบเท่ากันนี้ จึงพบความแตกต่างในคำจำกัดความมากมายในวรรณกรรม ตัวอย่างเช่น ใน "Terese" คุณสมบัติ Church–Rosser และความสอดคล้องกันถูกกำหนดให้มีความหมายเหมือนกันและเหมือนกับคำจำกัดความของความสอดคล้องกันที่นำเสนอไว้ที่นี่ Church–Rosser ตามที่กำหนดไว้ที่นี่ไม่ได้ระบุชื่อ แต่ถูกกำหนดให้เป็นคุณสมบัติที่เทียบเท่ากัน การเบี่ยงเบนจากข้อความอื่นนี้เป็นไปโดยเจตนา^{[ 10 ]}

จุดบรรจบกึ่งสมบูรณ์

นิยามของการบรรจบกันในระดับท้องถิ่นแตกต่างจากนิยามของการบรรจบกันในระดับโลกตรงที่พิจารณาเฉพาะองค์ประกอบที่ได้มาจากองค์ประกอบที่กำหนดในขั้นตอนการเขียนใหม่เพียงครั้งเดียวเท่านั้น โดยการพิจารณาองค์ประกอบหนึ่งที่ได้มาจากขั้นตอนเดียวและอีกองค์ประกอบหนึ่งที่ได้มาจากลำดับใดๆ เราจะได้แนวคิดระดับกลางของการบรรจบกันแบบกึ่งสมบูรณ์: a ∈ Sกล่าวได้ว่ามีการบรรจบกันแบบกึ่งสมบูรณ์หากสำหรับทุกb , c ∈ Sโดยที่a → bและa*→cมีd ∈ Sที่มีb อยู่*→งและค*→d ; ถ้าทุกa ∈ Sเป็นแบบกึ่งบรรจบกัน เราจะกล่าวว่า → เป็นแบบกึ่งบรรจบกัน

องค์ประกอบกึ่งต่อเนื่องไม่จำเป็นต้องต่อเนื่อง แต่ระบบการเขียนใหม่กึ่งต่อเนื่องนั้นจำเป็นต้องต่อเนื่อง และระบบต่อเนื่องนั้นโดยปริยายแล้วเป็นกึ่งต่อเนื่อง

การบรรจบกันที่แข็งแกร่ง

การบรรจบกันอย่างเข้มแข็ง (Strong confluence) เป็นอีกรูปแบบหนึ่งของการบรรจบกันในระดับท้องถิ่น (Local confluence) ซึ่งช่วยให้เราสรุปได้ว่าระบบการเขียนใหม่นั้นมีการบรรจบกันในระดับสากล (Globally confluence) กล่าวได้ว่าองค์ประกอบa ∈ S มี การบรรจบกันอย่างเข้มแข็งถ้าสำหรับทุกb , c ∈ Sที่a → bและa → cจะมีd ∈ Sที่b*→dและc → dหรือc = d ; ถ้าทุกa ∈ Sมีความสอดคล้องกันอย่างแข็งแกร่ง เราจะกล่าวว่า → มีความสอดคล้องกันอย่างแข็งแกร่ง

องค์ประกอบที่ไหลมาบรรจบกันไม่จำเป็นต้องไหลมาบรรจบกันอย่างเข้มข้น แต่ระบบการเขียนใหม่ที่ไหลมาบรรจบกันอย่างเข้มข้นนั้นย่อมต้องไหลมาบรรจบกันอย่างแน่นอน

ตัวอย่างของระบบที่บรรจบกัน

การลดรูปพหุนามมอดูโลไอเดีย ลเป็นระบบการเขียนใหม่ที่ต่อเนื่องกัน โดยมีเงื่อนไขว่าต้องใช้ฐานGröbner
ทฤษฎีบทของมัตสึโมโตะได้มาจากการบรรจบกันของความสัมพันธ์แบบถักเปีย
การลดรูป β ของเทอม λ นั้นสอดคล้องกับทฤษฎีบท Church– Rosser

ดูเพิ่มเติม

หมายเหตุ

^จากนั้นจึงเรียกกฎเหล่านั้นว่ากฎการเขียนใหม่เพื่อเน้นย้ำการวางแนวจากซ้ายไปขวา
^อัลกอริทึมการเติมเต็มของ Knuth–Bendixสามารถใช้คำนวณระบบดังกล่าวจากชุดสมการที่กำหนดได้ ระบบดังกล่าว เช่น สำหรับกลุ่มต่างๆ แสดงไว้ที่นี่โดยมีการกำหนดหมายเลขข้อเสนออย่างสม่ำเสมอ การใช้ระบบนี้ การพิสูจน์ เช่น R6 ประกอบด้วยการประยุกต์ใช้ R11 และ R12 ในลำดับใดก็ได้กับเทอม ( a ⁻¹ )⁻¹ ⋅1 เพื่อให้ได้เทอม aโดยไม่มีกฎอื่นใดที่สามารถนำมาใช้ได้

ลิงก์ภายนอก

ไวส์สไตน์, เอริก ดับเบิลยู. "บรรจบกัน" . แมทเวิลด์ .

[3] จากนั้นจึงเรียกกฎเหล่านั้นว่ากฎการเขียนใหม่เพื่อเน้นย้ำการวางแนวจากซ้ายไปขวา

[4] อัลกอริทึมการเติมเต็มของ Knuth–Bendixสามารถใช้คำนวณระบบดังกล่าวจากชุดสมการที่กำหนดได้ ระบบดังกล่าว เช่น สำหรับกลุ่มต่างๆ แสดงไว้ที่นี่โดยมีการกำหนดหมายเลขข้อเสนออย่างสม่ำเสมอ การใช้ระบบนี้ การพิสูจน์ เช่น R6 ประกอบด้วยการประยุกต์ใช้ R11 และ R12 ในลำดับใดก็ได้กับเทอม ( a ⁻¹ )⁻¹ ⋅1 เพื่อให้ได้เทอม aโดยไม่มีกฎอื่นใดที่สามารถนำมาใช้ได้

[ 1 ]

[ 2 ]

[หมายเหตุ 1 ]

[หมายเหตุ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[

[

[

[ 9 ]

[ 10 ]