อัลกอริทึมการเติมเต็ม Knuth–Bendix (ตั้งชื่อตามDonald Knuthและ Peter Bendix ^{[ 1 ]} ) เป็นอัลกอริทึมกึ่งตัดสินใจ^{[ 2 ] [ 3 ]} สำหรับการแปลงชุดสมการ (เหนือเทอม ) ให้เป็นระบบการเขียนเทอมใหม่แบบต่อเนื่อง เมื่ออัลกอริทึมประสบความสำเร็จ จะสามารถแก้ ปัญหาคำศัพท์สำหรับพีชคณิต ที่กำหนด ได้ อย่างมีประสิทธิภาพ

อัลกอริทึมของ Buchbergerสำหรับการคำนวณฐาน Gröbnerเป็นอัลกอริทึมที่คล้ายคลึงกันมาก แม้ว่าจะพัฒนาขึ้นโดยอิสระ แต่ก็อาจมองได้ว่าเป็นตัวอย่างของการนำอัลกอริทึม Knuth–Bendix มาใช้ในทฤษฎีวงแหวนพหุนาม

สำหรับเซตEของสมการการปิดเชิงอนุมาน ของเซตนั้น (⁎⟷อี) คือเซตของสมการทั้งหมดที่สามารถได้มาโดยการใช้สมการจากEในลำดับใดก็ได้ ในทางรูปธรรมEถือเป็นความสัมพันธ์ทวิภาค , (⟶อี) คือการปิดการเขียนใหม่และ (⁎⟷อี) คือการปิดสมมูลของ (⟶อีสำหรับชุดRของกฎการเขียนใหม่การปิดเชิงอนุมาน ของชุดนั้น (⁎⟶อาร์∘⁎⟵อาร์) คือเซตของสมการทั้งหมดที่สามารถยืนยันได้โดยการใช้กฎจากRจากซ้ายไปขวากับทั้งสองข้างจนกว่าจะเท่ากันอย่างแท้จริง ในทางรูปธรรมRถูกมองว่าเป็นความสัมพันธ์แบบไบนารีอีกครั้ง (⟶อาร์) คือการปิดการเขียนใหม่ของมัน (⟵อาร์) คือสิ่งที่ตรงกันข้ามและ (⁎⟶อาร์∘⁎⟵อาร์) คือความสัมพันธ์ของการประกอบกันของการปิดแบบสะท้อนและถ่ายทอด (⁎⟶อาร์และ⁎⟵อาร์)

ตัวอย่างเช่น ถ้าE = {1⋅ x = x , x ⁻¹ ⋅ x = 1, ( x ⋅ y )⋅ z = x ⋅( y ⋅ z )}เป็นสัจพจน์ ของ กลุ่ม ลำดับการอนุมานจะเป็นดังนี้

a ⁻¹ ⋅( a ⋅ b )   ⁎⟷อี   ( a ⁻¹ ⋅ a )⋅ b   ⁎⟷อี   1⋅ b   ⁎⟷อี   ข

แสดงให้เห็นว่าa ⁻¹ ⋅( a ⋅ b ) ⁎⟷อีbเป็นสมาชิกของ การปิดเชิงนิรนัย ของ Eถ้าR = { 1⋅ x → x , x ⁻¹ ⋅ x → 1, ( x ⋅ y )⋅ z → x ⋅( y ⋅ z ) }เป็นเวอร์ชัน "กฎการเขียนใหม่" ของEลำดับการอนุมาน

( a ⁻¹ ⋅ a )⋅ b   ⁎⟶อาร์   1⋅ b   ⁎⟶อาร์   บี       และ       บี   ⁎⟵อาร์   ข

แสดงให้เห็นว่า ( a ⁻¹ ⋅ a )⋅ b⁎⟶อาร์∘⁎⟵อาร์bเป็นสมาชิกของ การปิดเชิงนิรนัย ของ Rอย่างไรก็ตาม ไม่มีวิธีใดที่จะได้a ⁻¹ ⋅( a ⋅ b )⁎⟶อาร์∘⁎⟵อาร์b คล้ายกับข้างต้น เนื่องจาก ไม่สามารถ ใช้กฎ( x ⋅ y )⋅ z → x ⋅( y ⋅ z ) จากขวาไปซ้ายได้

อัลกอริทึม Knuth–Bendix รับชุดสมการE ระหว่าง เทอมต่างๆและลำดับการลดรูป (>) บนชุดของเทอมทั้งหมด และพยายามสร้างระบบการเขียนเทอมใหม่R ที่บรรจบกันและสิ้นสุด ซึ่งมีการปิดเชิงอนุมานเช่นเดียวกับEในขณะที่การพิสูจน์ผลลัพธ์จากEมักต้องอาศัยสัญชาตญาณของมนุษย์ การพิสูจน์ผลลัพธ์จากRไม่จำเป็นต้องอาศัยสัญชาตญาณ สำหรับรายละเอียดเพิ่มเติม โปรดดูConfluence (abstract rewriting)#Motivating examplesซึ่งมีตัวอย่างการพิสูจน์จากทฤษฎีกลุ่มที่ดำเนินการทั้งโดยใช้EและR

เมื่อกำหนดเซตEของสมการระหว่างเทอมแล้ว กฎการอนุมานต่อไปนี้สามารถใช้เพื่อแปลงให้เป็นระบบการเขียนใหม่ของเทอมที่บรรจบกันที่ เทียบเท่ากัน (ถ้าเป็นไปได้): ^{[ 4 ] [ 5 ]} กฎเหล่านี้ขึ้นอยู่กับ ลำดับการลด ที่ผู้ใช้กำหนด(>) บนเซตของเทอมทั้งหมด โดยจะยกขึ้นเป็นลำดับที่มีพื้นฐานที่ดี (▻) บนเซตของกฎการเขียนใหม่โดยกำหนด( s → t ) ▻ ( l → r )ถ้า

• ส>อีlในลำดับการครอบคลุมหรือ
• sและlมี ความ คล้ายคลึงกันอย่างแท้จริงและt > r

ตัวอย่างการทำงานต่อไปนี้ ซึ่งได้มาจากโปรแกรมพิสูจน์ทฤษฎีบท Eคำนวณการเติมเต็มสัจพจน์กลุ่ม (แบบบวก) ตามที่ Knuth, Bendix (1970) กล่าวไว้ เริ่มต้นด้วยสมการเริ่มต้นสามสมการสำหรับกลุ่ม (องค์ประกอบกลาง 0, องค์ประกอบผกผัน, การเชื่อมโยง) โดยใช้f(X,Y)สำหรับX + Yและi(X)สำหรับ − Xสมการที่มีเครื่องหมายดอกจัน 10 สมการนั้นประกอบกันเป็นระบบการเขียนใหม่ที่ลู่เข้า "pm" ย่อมาจาก " paramodulation " ซึ่งใช้การดำเนินการdeduceการคำนวณคู่วิกฤตเป็นตัวอย่างหนึ่งของ paramodulation สำหรับข้อความหน่วยสมการ "rw" คือการเขียนใหม่ ซึ่งใช้การดำเนินการcompose , collapseและsimplifyการกำหนดทิศทางของสมการทำโดยปริยายและไม่ได้บันทึกไว้

ดูเพิ่มเติมที่โจทย์ปัญหา (คณิตศาสตร์)สำหรับตัวอย่างอื่น ๆ ของเรื่องนี้

กรณีสำคัญในทฤษฎีกลุ่มเชิงคำนวณคือระบบการเขียนสตริงใหม่ ซึ่งสามารถใช้กำหนดป้ายกำกับมาตรฐานให้กับสมาชิกหรือโคเซตของกลุ่มที่นำเสนอแบบจำกัดโดยเป็นผลคูณของตัวสร้างกรณีพิเศษนี้เป็นจุดสนใจของส่วนนี้

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

พิจารณาโมโนอิดที่นำเสนออย่างจำกัด โดยที่ X คือเซตจำกัดของตัวสร้าง และ R คือเซตของความสัมพันธ์ที่กำหนดบน X ให้ X ^*เป็นเซตของคำทั้งหมดใน X (นั่นคือ โมโนอิดอิสระที่สร้างโดย X) เนื่องจากความสัมพันธ์ R สร้างความสัมพันธ์สมมูลบน X* เราจึงสามารถพิจารณาสมาชิกของ M ว่าเป็นชั้นสมมูลของ X _*^ภายใต้ R สำหรับแต่ละชั้น{w1 _, w2 _, ...}เป็นที่พึงปรารถนาที่จะเลือกตัวแทนมาตรฐานwkตัวแทนนี้เรียกว่า รูป แบบมาตรฐานหรือรูปแบบปกติสำหรับแต่ละคำwkในชั้นนั้น หากมีวิธีการคำนวณเพื่อกำหนดรูปแบบปกติwᵢ สำหรับแต่ละ wk ปัญหาคำ _{ก็ จะได้รับการแก้ไขได้ง่าย ระบบการเขียนใหม่ที่บรรจบกันช่วยให้สามารถ ทำ เช่นนั้น ได้}อย่างแม่นยำ ${\displaystyle M=\langle X\mid R\rangle }$

แม้ว่าในทางทฤษฎีแล้ว การเลือกรูปแบบมาตรฐานสามารถทำได้อย่างตามอำเภอใจ แต่โดยทั่วไปแล้ววิธีการนี้ไม่สามารถคำนวณได้ (ลองพิจารณาว่าความสัมพันธ์สมมูลในภาษาหนึ่งสามารถสร้างคลาสอนันต์จำนวนมหาศาลได้) หากภาษานั้นมีการจัดลำดับที่ดีลำดับ < จะให้วิธีการที่สอดคล้องกันในการกำหนดตัวแทนขั้นต่ำ อย่างไรก็ตาม การคำนวณตัวแทนเหล่านี้อาจยังคงเป็นไปไม่ได้ โดยเฉพาะอย่างยิ่ง หากใช้ระบบการเขียนใหม่เพื่อคำนวณตัวแทนขั้นต่ำ ลำดับ < ควรมีคุณสมบัติดังต่อไปนี้ด้วย:

A < B → XAY < XBY สำหรับคำทุกคำ A, B, X, Y

คุณสมบัตินี้เรียกว่าความไม่แปรเปลี่ยนภายใต้การเลื่อน (translation invariance ) ลำดับที่ทั้งไม่แปรเปลี่ยนภายใต้การเลื่อนและเป็นลำดับที่ดี (well-order) เรียกว่าลำดับลดรูป (reduction order )

จากการนำเสนอโมโนอิด เราสามารถกำหนดระบบการเขียนใหม่ได้โดยความสัมพันธ์ R ถ้า A x B อยู่ใน R แล้ว A < B ซึ่งในกรณีนี้ B → A เป็นกฎในระบบการเขียนใหม่ มิฉะนั้น A > B และ A → B เนื่องจาก < เป็นลำดับการลดรูป คำ W ที่กำหนดสามารถลดรูปได้เป็น W > W_1 > ... > W_n โดยที่ W_n เป็นคำที่ไม่สามารถลดรูปได้ภายใต้ระบบการเขียนใหม่ อย่างไรก็ตาม ขึ้นอยู่กับกฎที่ใช้ในแต่ละ W _i  → W _i+1อาจทำให้ได้การลดรูปที่ไม่สามารถลดรูปได้สองแบบที่แตกต่างกัน W _n  ≠ W' _mของ W แต่ถ้าหากระบบการเขียนใหม่ที่กำหนดโดยความสัมพันธ์ถูกแปลงเป็นระบบการเขียนใหม่แบบต่อเนื่องโดยใช้อัลกอริทึม Knuth–Bendix การลดรูปทั้งหมดจะรับประกันได้ว่าจะสร้างคำที่ไม่สามารถลดรูปได้คำเดียวกัน นั่นคือรูปแบบปกติสำหรับคำนั้น

สมมติว่าเราได้รับงานนำเสนอ โดยที่คือเซตของตัวสร้างและคือเซตของความสัมพันธ์ที่ให้ระบบการเขียนใหม่ สมมติเพิ่มเติมว่าเรามีลำดับการลดรูประหว่างคำที่สร้างโดย(เช่นลำดับ shortlex ) สำหรับแต่ละความสัมพันธ์ในสมมติว่าดังนั้นเราจึงเริ่มต้นด้วยเซตของการลดรูป ${\displaystyle \langle X\mid R\rangle }$${\displaystyle X}$${\displaystyle R}$${\displaystyle <}$${\displaystyle X}$${\displaystyle P_{i}=Q_{i}}$${\displaystyle R}$${\displaystyle Q_{i}<P_{i}}$${\displaystyle P_{i}\rightarrow Q_{i}}$

ขั้นแรก หากความสัมพันธ์ใดสามารถลดรูปได้ ให้แทนที่ " และ" ด้วยรูปแบบที่ลดรูปแล้ว ${\displaystyle P_{i}=Q_{i}}$${\displaystyle P_{i}}$${\displaystyle Q_{i}}$

ถัดไป เราจะเพิ่มการลดทอนเพิ่มเติม (นั่นคือ การเขียนกฎใหม่) เพื่อกำจัดข้อยกเว้นที่อาจเกิดขึ้นจากการบรรจบกัน สมมติว่าและทับซ้อนกัน ${\displaystyle P_{i}}$${\displaystyle P_{j}}$

1. กรณีที่ 1: คำนำหน้าของเท่ากับคำต่อท้ายของหรือในทางกลับกัน ในกรณีแรก เราสามารถเขียนและได้ ในกรณีหลัง เราสามารถเขียน และได้${\displaystyle P_{i}}$${\displaystyle P_{j}}$${\displaystyle P_{i}=BC}$${\displaystyle P_{j}=AB}$${\displaystyle P_{i}=AB}$${\displaystyle P_{j}=BC}$
2. กรณีที่ 2: อาจถูกบรรจุอยู่ภายใน (ล้อมรอบด้วย) อย่างสมบูรณ์ หรือในทางกลับกัน ในกรณีแรก เราสามารถเขียนและได้ ในกรณีหลัง เราสามารถเขียน และได้${\displaystyle P_{i}}$${\displaystyle P_{j}}$${\displaystyle P_{i}=B}$${\displaystyle P_{j}=ABC}$${\displaystyle P_{i}=ABC}$${\displaystyle P_{j}=B}$

ลดคำโดยใช้ครั้งแรก จากนั้นใช้ครั้งแรกอีกครั้ง เรียกผลลัพธ์ว่า ตามลำดับ ถ้าแสดงว่าเรามีกรณีที่ Confluence อาจล้มเหลว ดังนั้น ให้เพิ่มการลดลง ใน${\displaystyle ABC}$${\displaystyle P_{i}}$${\displaystyle P_{j}}$${\displaystyle r_{1},r_{2}}$${\displaystyle r_{1}\neq r_{2}}$${\displaystyle \max r_{1},r_{2}\rightarrow \min r_{1},r_{2}}$${\displaystyle R}$

หลังจากเพิ่มกฎลงใน แล้วให้ลบกฎใดๆ ในที่อาจมีด้านซ้ายที่สามารถลดรูปได้ (หลังจากตรวจสอบแล้วว่ากฎเหล่านั้นมีคู่ที่สำคัญกับกฎอื่นๆ หรือไม่) ${\displaystyle R}$${\displaystyle R}$

ทำซ้ำขั้นตอนนี้จนกว่าจะตรวจสอบด้านซ้ายที่ซ้อนทับกันทั้งหมดแล้ว

พิจารณาโมโนอิดนี้:

${\displaystyle \langle x,y\mid x^{3}=y^{3}=(xy)^{3}=1\rangle }$.

เราใช้ลำดับ shortlexซึ่งเป็นโมโนอิดอนันต์ แต่ถึงกระนั้น อัลกอริทึม Knuth–Bendix ก็สามารถแก้ปัญหาโจทย์คำถามได้

ดังนั้น การลดสามขั้นแรกของเราจึงมีดังนี้

${\displaystyle x^{3}\rightarrow 1}$

1

${\displaystyle y^{3}\rightarrow 1}$

2

${\displaystyle (xy)^{3}\rightarrow 1}$.

3

คำต่อท้ายของ(กล่าวคือ) เป็นคำนำหน้าของดังนั้นพิจารณาคำว่าเมื่อลดรูปโดยใช้ ( 1 ) เราจะได้เมื่อลดรูปโดยใช้ ( 3 ) เราจะได้ดังนั้น เราจะได้ซึ่งให้กฎการลดรูป ${\displaystyle x^{3}}$${\displaystyle x}$${\displaystyle (xy)^{3}=xyxyxy}$${\displaystyle x^{3}yxyxy}$${\displaystyle yxyxy}$${\displaystyle x^{2}}$${\displaystyle yxyxy=x^{2}}$

${\displaystyle yxyxy\rightarrow x^{2}}$.

4

ในทำนองเดียวกัน การใช้และการลดโดยใช้ ( 2 ) และ ( 3 ) เราจะได้ดังนั้นการลด ${\displaystyle xyxyxy^{3}}$${\displaystyle xyxyx=y^{2}}$

${\displaystyle xyxyx\rightarrow y^{2}}$.

5

กฎทั้งสองข้อนี้ล้าสมัยแล้ว ( 3 ) ดังนั้นเราจึงลบออก

ถัดไป พิจารณาโดยการทับซ้อน ( 1 ) และ ( 5 ) เมื่อลดทอนแล้วจะได้ดังนั้นเราจึงเพิ่มกฎ ${\displaystyle x^{3}yxyx}$${\displaystyle yxyx=x^{2}y^{2}}$

${\displaystyle yxyx\rightarrow x^{2}y^{2}}$.

6

เมื่อพิจารณาโดยการทับซ้อนกันของ ( 1 ) และ ( 5 ) เราจะได้ดังนั้นเราจึงเพิ่มกฎ ${\displaystyle xyxyx^{3}}$${\displaystyle xyxy=y^{2}x^{2}}$

${\displaystyle y^{2}x^{2}\rightarrow xyxy}$.

7

กฎที่ล้าสมัยเหล่านี้ ( 4 ) และ ( 5 ) ดังนั้นเราจึงลบออก

ตอนนี้เราเหลือเพียงระบบการเขียนใหม่แล้ว

${\displaystyle x^{3}\rightarrow 1}$

( 1 )

${\displaystyle y^{3}\rightarrow 1}$

( 2 )

${\displaystyle yxyx\rightarrow x^{2}y^{2}}$

( 6 )

${\displaystyle y^{2}x^{2}\rightarrow xyxy}$.

( 7 )

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

ลำดับของตัวสร้างอาจส่งผลอย่างมากต่อการสิ้นสุดของกระบวนการเติมเต็มแบบ Knuth–Bendix ตัวอย่างเช่น พิจารณากลุ่มอาเบเลียนอิสระโดยการนำเสนอแบบโมโนอิด:

${\displaystyle \langle x,y,x^{-1},y^{-1}\,|\,xy=yx,xx^{-1}=x^{-1}x=yy^{-1}=y^{-1}y=1\rangle .}$

การเติมเต็ม Knuth–Bendix ที่เกี่ยวข้องกับลำดับพจนานุกรมจะจบลงด้วยระบบบรรจบกัน อย่างไรก็ตาม เมื่อพิจารณาลำดับพจนานุกรมตามความยาวแล้วจะไม่จบลง เนื่องจากไม่มีระบบบรรจบกันแบบจำกัดที่เข้ากันได้กับลำดับหลังนี้^{[ 6 ]}${\displaystyle x<x^{-1}<y<y^{-1}}$${\displaystyle x<y<x^{-1}<y^{-1}}$

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

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

• ไวส์สไตน์, เอริค ดับเบิลยู. "อัลกอริธึมการสำเร็จ Knuth–Bendix " แมทเวิลด์ .
• โปรแกรม Knuth-Bendix Completion Visualizer (เลิกใช้งานแล้ว)
• เครื่องมือออนไลน์ที่ใช้ขั้นตอนวิธีเติมเต็ม Knuth-Bendix