ในตรรกศาสตร์และวิทยาศาสตร์คอมพิวเตอร์โดยเฉพาะอย่างยิ่งในการให้เหตุผลอัตโนมัติ การ รวมกัน ( unification)เป็นกระบวนการเชิงอัลกอริทึมในการแก้สมการระหว่างนิพจน์ เชิงสัญลักษณ์ ซึ่งแต่ละนิพจน์มีรูปแบบด้านซ้าย = ด้านขวาตัวอย่างเช่น เมื่อใช้x , y , zเป็นตัวแปร และให้fเป็นฟังก์ชันที่ไม่มีการ ตีความ ชุด สมการ เดี่ยว { f (1, y ) = f ( x ,2) } เป็นปัญหาการรวมกันลำดับที่หนึ่งเชิงไวยากรณ์ ซึ่งมีการแทนที่ { x ↦ 1, y ↦ 2 } เป็นคำตอบเดียว

ข้อตกลงต่างๆ แตกต่างกันไปในเรื่องค่าที่ตัวแปรอาจมีได้และนิพจน์ใดที่ถือว่าเทียบเท่ากัน ในการรวมเชิงไวยากรณ์ลำดับที่หนึ่ง ตัวแปรจะครอบคลุมเทอมลำดับที่หนึ่งและความเทียบเท่าเป็นไปตามไวยากรณ์ การรวมแบบนี้มีคำตอบ "ที่ดีที่สุด" เพียงหนึ่งเดียว และใช้ในการเขียนโปรแกรมเชิงตรรกะและ การใช้งาน ระบบประเภท ของภาษาโปรแกรม โดยเฉพาะอย่างยิ่งใน อัลกอริธึม การอนุมานประเภทตามHindley–Milnerในการรวมลำดับที่สูงกว่า ซึ่งอาจจำกัดเฉพาะการรวมรูปแบบลำดับที่สูงกว่า เทอมอาจรวมถึงนิพจน์แลมบ์ดา และความเทียบเท่าขึ้นอยู่กับการลดเบต้า การรวมแบบนี้ใช้ในตัวช่วยพิสูจน์และการเขียนโปรแกรมเชิงตรรกะลำดับที่สูงกว่า เช่นIsabelle , TwelfและlambdaPrologสุดท้าย ในการรวมเชิงความหมายหรือ E-unification ความเท่าเทียมกันขึ้นอยู่กับความรู้พื้นฐานและตัวแปรจะครอบคลุมโดเมนที่หลากหลาย การรวมแบบนี้ใช้ในตัวแก้ปัญหา SMT อัลกอริ ธึ มการเขียนเทอมใหม่และการวิเคราะห์ โปรโตคอลการเข้ารหัสลับ

ปัญหาการรวมสมการคือเซตจำกัดE ={ l ₁ ≐ r ₁ , ..., l _n ≐ r _n }ของสมการที่ต้องแก้ โดยที่l _i , r _iอยู่ในเซตของพจน์หรือนิพจน์ขึ้นอยู่กับว่านิพจน์หรือพจน์ใดที่อนุญาตให้ปรากฏในเซตสมการหรือปัญหาการรวมสมการ และนิพจน์ใดที่ถือว่าเท่ากัน จึงมีการแบ่งกรอบการรวมสมการออกเป็นหลายแบบ หากอนุญาตให้ใช้ตัวแปรลำดับสูงกว่า นั่นคือตัวแปรที่แทนฟังก์ชันในนิพจน์ กระบวนการนี้เรียกว่าการรวมสมการลำดับสูงกว่ามิฉะนั้น เรียกว่า การรวมสมการลำดับแรกหากต้องการคำตอบที่ทำให้ทั้งสองข้างของแต่ละสมการเท่ากันอย่างแท้จริง กระบวนการนี้เรียกว่าการรวมสมการเชิงไวยากรณ์หรือแบบอิสระมิฉะนั้นเรียกว่าการรวม สมการ เชิงความหมายหรือ แบบสมการ หรือ การรวมสมการ Eหรือการรวมสมการโมดูลัสทฤษฎี ${\displaystyle T}$

ถ้าด้านขวาของแต่ละสมการปิด (ไม่มีตัวแปรอิสระ) ปัญหาจะเรียกว่าการจับคู่ (รูปแบบ) ด้านซ้าย (ที่มีตัวแปร) ของแต่ละสมการเรียกว่ารูปแบบ^{[ 1 ]}

ในทางทฤษฎีแล้ว แนวทางการรวมเป็นหนึ่งเดียวตั้งอยู่บนพื้นฐานของสิ่งต่อไปนี้

• เซตของตัวแปรอนันต์สำหรับการรวมลำดับที่สูงขึ้น เป็นเรื่องสะดวกที่จะเลือกตัวแปรที่ไม่ซ้ำกันจากเซตของตัวแปรที่ถูกผูกไว้กับเทอมแลมบ์ดา${\displaystyle V}$${\displaystyle V}$
• เซตของเทอมต่างๆที่มีคุณสมบัติว่าสำหรับการรวมแบบอันดับแรกมักจะเป็นเซตของเทอมอันดับแรก (เทอมที่สร้างขึ้นจากสัญลักษณ์ตัวแปรและฟังก์ชัน) สำหรับการรวมแบบอันดับสูงกว่าจะประกอบด้วยเทอมอันดับแรกและเทอมแลมบ์ดา (เทอมที่มีตัวแปรอันดับสูงกว่าบางตัว)${\displaystyle T}$${\displaystyle V\subseteq T}$${\displaystyle T}$${\displaystyle T}$
• การจับคู่โดยกำหนดเซตของตัวแปรอิสระที่ปรากฏใน เทอม นั้น ให้กับแต่ละเทอม${\displaystyle {\text{vars}}\colon T\rightarrow }$${\displaystyle \mathbb {P} }$${\displaystyle (V)}$${\displaystyle t}$${\displaystyle {\text{vars}}(t)\subsetneq V}$${\displaystyle t}$
• ทฤษฎีหรือความสัมพันธ์สมมูล บน ซึ่งระบุว่าเทอมใดถือว่าเท่ากัน สำหรับการรวม E อันดับแรกสะท้อนถึงความรู้พื้นฐานเกี่ยวกับสัญลักษณ์ฟังก์ชันบางอย่าง ตัวอย่างเช่น ถ้าถือว่าสลับที่ได้ถ้าเป็นผลมาจากโดยการสลับอาร์กิวเมนต์ของในบาง (อาจจะทุก) ครั้ง^{[หมายเหตุ 1 ]}ในกรณีทั่วไปที่ไม่มีความรู้พื้นฐานเลย จะมีเพียงเทอมที่เหมือนกันตามตัวอักษรหรือตามไวยากรณ์เท่านั้นที่ถือว่าเท่ากัน ในกรณีนี้ ≡ เรียกว่าทฤษฎีอิสระ (เพราะเป็นวัตถุอิสระ ) ทฤษฎีว่างเปล่า (เพราะเซตของประโยค สมการ หรือความรู้พื้นฐานนั้นว่างเปล่า) ทฤษฎีของฟังก์ชันที่ไม่ได้ ตีความ (เพราะการรวมทำบนเทอม ที่ไม่ได้ตีความ ) หรือทฤษฎีของตัวสร้าง (เพราะสัญลักษณ์ฟังก์ชันทั้งหมดสร้างเทอมข้อมูลขึ้นมาแทนที่จะดำเนินการกับเทอมเหล่านั้น) สำหรับการรวมอันดับสูงกว่า โดยปกติแล้วถ้าและสมมูลกันแบบอัลฟา${\displaystyle \equiv }$${\displaystyle T}$${\displaystyle \equiv }$${\displaystyle \oplus }$${\displaystyle t\equiv u}$${\displaystyle u}$${\displaystyle t}$${\displaystyle \oplus }$${\displaystyle t\equiv u}$${\displaystyle t}$${\displaystyle u}$

ตัวอย่างเช่น ปัญหาการรวมลำดับที่หนึ่งทางไวยากรณ์ { y = cons (2, y ) } ไม่มีคำตอบบนเซตของ เทอม จำกัดอย่างไรก็ตาม มันมีคำตอบเดียว { y ↦ cons (2, cons (2, cons (2,...))) } บนเซตของ เทอม ต้นไม้อนันต์ ในทำนองเดียวกัน ปัญหาการรวมลำดับที่หนึ่งทางความหมาย { a ⋅ x = x ⋅ a } มีการแทนที่แต่ละแบบในรูปแบบ { x ↦ a ⋅...⋅ a } เป็นคำตอบในเซมิกรุป กล่าว คือ ถ้า (⋅) ถือว่า มีคุณสมบัติ การสลับที่ แต่ปัญหาเดียวกันนี้ เมื่อมองในกลุ่มอาเบเลียนซึ่ง (⋅) ถือว่า มีคุณสมบัติ การสลับที่ เช่นกัน การแทนที่ใดๆ ก็ตามจะเป็นคำตอบได้

ตัวอย่างหนึ่งของการรวมลำดับที่สูงกว่าคือ เซตที่มีสมาชิกเดียว { a = y ( x ) } ซึ่งเป็นปัญหาการรวมลำดับที่สองเชิงไวยากรณ์ เนื่องจากyเป็นตัวแปรฟังก์ชัน วิธีแก้ปัญหาหนึ่งคือ { x ↦ a , y ↦ ( ฟังก์ชันเอกลักษณ์ ) }; อีกวิธีหนึ่งคือ { y ↦ ( ฟังก์ชันคงที่ที่แมปแต่ละค่าไปยังa ), x ↦ (ค่าใดๆ) }

การแทนที่ (Substitution)คือการจับคู่จากตัวแปรไปยังเทอม สัญลักษณ์ { x ↦ h ( a , y ), z ↦ b } หมายถึงการจับคู่ที่แมปตัวแปรแต่ละตัวไปยังเทอมสำหรับ x > y และตัวแปรอื่นๆ ไปยังตัวมันเอง ตัวแปรทั้งสองต้องแตกต่างกันเป็นคู่ๆการนำการแทนที่ไปใช้กับเทอมจะเขียนใน รูป แบบ postfixเป็น { x ↦ h ( a , y ), z ↦ b } ซึ่งหมายถึงการแทนที่ตัวแปรทุกตัว ในเทอมด้วย ตัวแปรนั้น พร้อมกันผลลัพธ์ของการนำการแทนที่ไปใช้กับเทอมเรียกว่าอินสแตนซ์ของเทอมนั้นตัวอย่างลำดับแรกคือ การนำการแทนที่{ x ↦ h ( a , y ), z ↦ b } ไปใช้ กับเทอม z = z( a, y)${\displaystyle \sigma :V\rightarrow T}$${\displaystyle \{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$${\displaystyle x_{i}}$${\displaystyle t_{i}}$${\displaystyle i=1,...,k}$${\displaystyle x_{i}}$${\displaystyle t}$${\displaystyle t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$${\displaystyle x_{i}}$${\displaystyle t}$${\displaystyle t_{i}}$${\displaystyle t\tau }$${\displaystyle \tau }$${\displaystyle t}$${\displaystyle t}$

	${\displaystyle f(}$	${\displaystyle {\textbf {x}}}$	${\displaystyle ,a,g(}$	${\displaystyle {\textbf {z}}}$	${\displaystyle ),y)}$
ผลผลิต
	${\displaystyle f(}$	${\displaystyle {\textbf {h}}({\textbf {a}},{\textbf {y}})}$	${\displaystyle ,a,g(}$	${\displaystyle {\textbf {b}}}$	${\displaystyle ),y).}$

ถ้าเทอมหนึ่งมีตัวอย่างที่เทียบเท่ากับเทอมอีกเทอมหนึ่งนั่นคือ ถ้าสำหรับการแทนที่บางอย่าง เทอมหนึ่งเรียกว่าทั่วไปกว่า เทอมอีก เทอมหนึ่ง และ เทอมอีก เทอมหนึ่งเรียกว่าเฉพาะเจาะจงกว่าเทอมอีกเทอมหนึ่ง หรือถูกรวมไว้ในเทอมอีกเทอมหนึ่งตัวอย่างเช่น เทอม หนึ่งทั่วไปกว่า เทอมอีกเทอมหนึ่ง ถ้า ⊕ เป็นเทอมสลับที่ได้เนื่องจากเทอมอีกเทอม หนึ่งคือ ทั่วไปกว่าเทอมอีกเทอมหนึ่ง${\displaystyle t}$${\displaystyle u}$${\displaystyle t\sigma \equiv u}$${\displaystyle \sigma }$${\displaystyle t}$${\displaystyle u}$${\displaystyle u}$${\displaystyle t}$${\displaystyle x\oplus a}$${\displaystyle a\oplus b}$${\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b}$

ถ้า ≡ คือความเหมือนกันทางไวยากรณ์ของคำศัพท์ คำศัพท์หนึ่งอาจมีความทั่วไปและเฉพาะเจาะจงกว่าอีกคำหนึ่งได้ก็ต่อเมื่อคำศัพท์ทั้งสองแตกต่างกันเพียงแค่ชื่อตัวแปรเท่านั้น ไม่ใช่โครงสร้างทางไวยากรณ์ คำศัพท์ดังกล่าวเรียกว่าตัวแปรหรือการเปลี่ยนชื่อของกันและกัน ตัวอย่างเช่น เป็นตัวแปรของ เนื่องจาก และ อย่างไรก็ตามไม่ใช่ตัวแปรของ เนื่องจากไม่มีการแทนที่ใดที่จะเปลี่ยนคำศัพท์หลังให้เป็นคำศัพท์แรก ได้ดังนั้นคำศัพท์หลังจึงมีความเฉพาะเจาะจงกว่าคำศัพท์แรกอย่างถูกต้อง ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$$${\displaystyle f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})}$$$${\displaystyle f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1}).}$$${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$

สำหรับค่าใดๆ ก็ตามเทอมหนึ่งอาจมีความทั่วไปมากกว่าและมีความเฉพาะเจาะจงมากกว่าเทอมที่มีโครงสร้างแตกต่างกัน ตัวอย่างเช่น ถ้า ⊕ เป็นเทอมเอกลักษณ์ (idempotent ) นั่นคือ ถ้า ⊕ เป็นจริงเสมอเทอมนั้นจะมีความทั่วไปมากกว่า⊕ ^{[หมายเหตุ 2 ]}และในทางกลับกัน^{[หมายเหตุ 3 ]}แม้ว่า⊕ และ ⊕ จะมีโครงสร้างที่แตกต่างกันก็ตาม ${\displaystyle \equiv }$${\displaystyle x\oplus x\equiv x}$${\displaystyle x\oplus y}$${\displaystyle z}$${\displaystyle x\oplus y}$${\displaystyle z}$

การแทนที่พิเศษกว่าหรือถูกรวมโดยการแทนที่ถ้าถูกรวมโดยสำหรับแต่ละเทอมเรายังกล่าวอีกว่ามีความทั่วไปมากกว่าในทางที่เป็นทางการมากขึ้น ให้ใช้เซตอนันต์ที่ไม่ว่างเปล่าของตัวแปรเสริม โดยที่ไม่มีสมการใดในปัญหาการรวมประกอบด้วยตัวแปรจาก จากนั้น^การแทนที่จะถูกรวมโดยการแทนที่อื่นถ้ามีการแทนที่เช่นนั้น สำหรับทุกเทอม[ 2 ^{] ตัวอย่าง} เช่นถูกรวมโดย โดยใช้แต่ ไม่ถูกรวมโดยเนื่องจากไม่ใช่ตัวอย่าง ของ^{[ 3 ]}${\displaystyle \sigma }$${\displaystyle \tau }$${\displaystyle t\sigma }$${\displaystyle t\tau }$${\displaystyle t}$${\displaystyle \tau }$${\displaystyle \sigma }$${\displaystyle V}$${\displaystyle l_{i}\doteq r_{i}}$${\displaystyle V}$${\displaystyle \sigma }$${\displaystyle \tau }$${\displaystyle \theta }$${\displaystyle X\notin V}$${\displaystyle X\sigma \equiv X\tau \theta }$${\displaystyle \{x\mapsto a,y\mapsto a\}}$${\displaystyle \tau =\{x\mapsto y\}}$${\displaystyle \theta =\{y\mapsto a\}}$${\displaystyle \sigma =\{x\mapsto a\}}$${\displaystyle \tau =\{x\mapsto y\}}$${\displaystyle f(x,y)\sigma =f(a,y)}$${\displaystyle f(x,y)\tau =f(y,y)}$

การแทนที่ σ คือคำตอบของปัญหาการรวมEถ้าl _i σ ≡ r _i σสำหรับการแทนที่ดังกล่าวเรียกว่าตัวรวมของEตัวอย่างเช่น ถ้า ⊕ มีคุณสมบัติการสลับที่ ปัญหาการรวม { x ⊕ a ≐ a ⊕ x } จะมีคำตอบ { x ↦ a }, { x ↦ a ⊕ a }, { x ↦ a ⊕ a ⊕ a } เป็นต้น ในขณะที่ปัญหา { x ⊕ a ≐ a } ไม่มีคำตอบ ${\displaystyle i=1,...,n}$

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

เซตSเรียกว่าเซตขั้นต่ำหากไม่มีสมาชิกใดในเซตนั้นที่รวมสมาชิกอื่นเข้าไป ขึ้นอยู่กับกรอบงาน เซตการแทนที่ที่สมบูรณ์และขั้นต่ำอาจมีสมาชิกเป็นศูนย์ หนึ่ง จำนวนจำกัด หรือจำนวนอนันต์ หรืออาจไม่มีอยู่เลยเนื่องจากสายโซ่สมาชิกที่ซ้ำซ้อนเป็นอนันต์^{[ 4 ]}ดังนั้น โดยทั่วไปแล้ว อัลกอริทึมการรวมจะคำนวณค่าประมาณที่จำกัดของเซตที่สมบูรณ์ ซึ่งอาจเป็นหรือไม่เป็นเซตขั้นต่ำก็ได้ แม้ว่าอัลกอริทึมส่วนใหญ่จะหลีกเลี่ยงตัวรวมที่ซ้ำซ้อนเมื่อเป็นไปได้^{[ 2 ]}สำหรับการรวมไวยากรณ์ลำดับแรก Martelli และ Montanari ^{[ 5 ]}ได้นำเสนออัลกอริทึมที่รายงานความไม่สามารถแก้ไขได้หรือคำนวณตัวรวมตัวเดียวที่สร้างเซตการแทนที่ที่สมบูรณ์และขั้นต่ำด้วยตัวมันเอง เรียกว่าตัว รวมทั่วไปที่สุด

การรวมเชิงไวยากรณ์ของพจน์ลำดับที่หนึ่งเป็นกรอบการรวมที่ใช้กันอย่างแพร่หลายที่สุด โดยอิงจากTที่เป็นเซตของพจน์ลำดับที่หนึ่ง (เหนือเซตVของตัวแปรที่กำหนด, Cของค่าคงที่ และF _nของ สัญลักษณ์ฟังก์ชัน n -ary) และ ≡ ที่เป็นความเท่าเทียมกันเชิงไวยากรณ์ในกรอบนี้ ปัญหาการรวมที่แก้ได้แต่ละปัญหา{ l ₁ ≐ r ₁ , ..., l _n ≐ r _n } มี เซตคำตอบเดี่ยวที่สมบูรณ์และเห็นได้ชัดว่าน้อยที่สุด{ σ }สมาชิกσ ของเซตนี้ เรียกว่าตัวรวมทั่วไปที่สุด ( mgu ) ของปัญหา พจน์ทางด้านซ้ายและด้านขวามือของสมการที่เป็นไปได้แต่ละสมการจะเท่ากันเชิงไวยากรณ์เมื่อใช้ mgu กล่าวคือl ₁ σ = r ₁ σ ∧ ... ∧ l _n σ = r _n σตัวรวมใดๆ ของปัญหาจะถูกรวมไว้^{[หมายเหตุ 4 ]}โดยmgu σ mgu มีเอกลักษณ์เฉพาะตัวจนถึงรูปแบบต่างๆ: ถ้าS ₁และS ₂เป็นเซตคำตอบที่สมบูรณ์และน้อยที่สุดของปัญหาการรวมไวยากรณ์เดียวกันแล้วS ₁ = { σ ₁ } และS ₂ = { σ _{2 } สำหรับการแทนที่} σ ₁และσ ₂บางอย่างและxσ ₁เป็นรูปแบบหนึ่งของxσ ₂สำหรับตัวแปรx แต่ละตัว ที่ปรากฏในปัญหา

ตัวอย่างเช่น ปัญหาการรวม { x ≐ z , y ≐ f ( x ) } มีตัวรวม { x ↦ z , y ↦ f ( z ) } เพราะว่า

x	{ x ↦ z , y ↦ f ( z ) }	=	z	=	z	{ x ↦ z , y ↦ f ( z ) }	, และ
y	{ x ↦ z , y ↦ f ( z ) }	=	เอฟ ( z )	=	เอฟ ( x )	{ x ↦ z , y ↦ f ( z ) }	.

นี่คือตัวรวมที่ครอบคลุมที่สุด ตัวรวมอื่นๆ สำหรับปัญหาเดียวกัน ได้แก่ เช่น { x ↦ f ( x ₁ ), y ↦ f ( f ( x ₁ )), z ↦ f ( x ₁ ) }, { x ↦ f ( f ( x ₁ )), y ↦ f ( f ( f ( x ₁ ))), z ↦ f ( f ( x ₁ )) } และอื่นๆ อีกมากมาย มีตัวรวมที่คล้ายกันอยู่นับไม่ถ้วน

ตัวอย่างเช่น ปัญหาg ( x , x ) ≐ f ( y ) ไม่มีคำตอบในส่วนที่ ≡ เป็นเอกลักษณ์ตามตัวอักษร เนื่องจากหากมีการแทนที่ใดๆ ทางด้านซ้ายและด้านขวา จะยังคงรักษาgและf ที่อยู่ด้านนอกสุด ไว้ และเทอมที่มีสัญลักษณ์ฟังก์ชันที่อยู่ด้านนอกสุดต่างกันจะมีความแตกต่างกันทางไวยากรณ์

Jacques Herbrandได้อภิปรายแนวคิดพื้นฐานของการรวมและร่างอัลกอริทึมในปี 1930 ^{[ 9 ] [ 10 ] [ 11 ]} แต่ผู้เขียนส่วนใหญ่ยกให้ John Alan Robinsonเป็นผู้คิดค้นอัลกอริทึมการรวมตัวแรก(ดูในกรอบ) ^{[ 12 ] [ 13 ] [หมายเหตุ 5 ]}อัลกอริทึมของ Robinson มีพฤติกรรมแบบเลขชี้กำลังในกรณีที่เลวร้ายที่สุดทั้งในด้านเวลาและพื้นที่^{[ 11 ] [ 15 ]}ผู้เขียนจำนวนมากได้เสนออัลกอริทึมการรวมที่มีประสิทธิภาพมากขึ้น^{[ 16 ]}อัลกอริทึมที่มีพฤติกรรมเชิงเส้นในกรณีที่เลวร้ายที่สุดถูกค้นพบโดยอิสระโดยMartelli & Montanari (1976)และPaterson & Wegman (1976) ^{[หมายเหตุ 6 ]} Baader & Snyder (2001)ใช้เทคนิคที่คล้ายกับ Paterson-Wegman ดังนั้นจึงเป็นเชิงเส้น^{[ 17 ]}แต่เช่นเดียวกับอัลกอริทึมการรวมเชิงเส้นส่วนใหญ่ จะช้ากว่าเวอร์ชัน Robinson สำหรับอินพุตขนาดเล็กเนื่องจากค่าใช้จ่ายในการประมวลผลล่วงหน้าของอินพุตและการประมวลผลภายหลังของเอาต์พุต เช่น การสร้างการแสดงDAG de Champeaux (2022)ก็มีความซับซ้อนเชิงเส้นในขนาดของอินพุตเช่นกัน แต่สามารถแข่งขันกับอัลกอริทึม Robinson ได้สำหรับอินพุตขนาดเล็ก ความเร็วที่เพิ่มขึ้นได้มาจากการใช้ การแสดงแคลคูลัส เชิงวัตถุที่หลีกเลี่ยงความจำเป็นในการประมวลผลล่วงหน้าและภายหลัง แต่ทำให้วัตถุตัวแปรรับผิดชอบในการสร้างการแทนที่และการจัดการกับนามแฝง เดอ ชองโปซ์ อ้างว่าความสามารถในการเพิ่มฟังก์ชันการทำงานให้กับแคลคูลัสเชิงเงื่อนไขที่แสดงเป็นวัตถุ โปรแกรมมิ่งนั้น เปิดโอกาสให้สามารถปรับปรุงการดำเนินการตรรกะอื่นๆ ได้เช่นกัน^{[ 15 ]}

อัลกอริทึมต่อไปนี้มักถูกนำเสนอและมีที่มาจากMartelli & Montanari (1982) [ ^{หมายเหตุ 7 ]}เมื่อกำหนดชุดสมการศักยภาพที่จำกัด อัลกอริทึมจะใช้กฎเพื่อแปลงชุดสมการนั้นให้เป็นชุดสมการที่เทียบเท่ากันในรูปแบบ { x ₁ ≐ u ₁ , ..., x _m ≐ u _m } โดยที่x ₁ , ..., x _mเป็นตัวแปรที่แตกต่างกัน และu ₁ , ..., u _mเป็นพจน์ที่ไม่มีx _iชุดในรูปแบบนี้สามารถอ่านได้ว่าเป็นการแทนที่ หากไม่มีคำตอบ อัลกอริทึมจะสิ้นสุดด้วย ⊥; ผู้เขียนคนอื่นใช้ "Ω" หรือ " fail " ในกรณีนั้น การดำเนินการแทนที่ตัวแปรx ทั้งหมด ในปัญหาGด้วยพจน์tจะถูกเขียนแทนด้วยG { x ↦ t } เพื่อความง่าย สัญลักษณ์คงที่ถือเป็นสัญลักษณ์ฟังก์ชันที่มีอาร์กิวเมนต์เป็นศูนย์ ${\displaystyle G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}}$

${\displaystyle G\cup \{t\doteq t\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G}$			ลบ
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}}$			สลายตัว
${\displaystyle G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle \bot }$	ถ้าหรือ${\displaystyle f\neq g}$${\displaystyle k\neq m}$		ขัดแย้ง
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq x\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$			แลกเปลี่ยน
${\displaystyle G\cup \{x\doteq t\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\{x\mapsto t\}\cup \{x\doteq t\}}$	ถ้าและ${\displaystyle x\not \in {\text{vars}}(t)}$${\displaystyle x\in {\text{vars}}(G)}$		กำจัด[หมายเหตุ 8 ]
${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle \bot }$	ถ้า${\displaystyle x\in {\text{vars}}(f(s_{0},...,s_{k}))}$		ตรวจสอบ

ความพยายามที่จะรวมตัวแปรxกับเทอมที่มีxเป็นเทอมย่อยที่เข้มงวดx ≐ f (..., x , ...) จะนำไปสู่เทอมอนันต์เป็นคำตอบสำหรับxเนื่องจากxจะปรากฏเป็นเทอมย่อยของตัวมันเอง ในเซตของเทอมอันดับแรก (จำกัด) ตามที่กำหนดไว้ข้างต้น สมการx ≐ f (..., x , ...) ไม่มีคำตอบ ดังนั้น กฎ การกำจัดจึงสามารถใช้ได้เฉพาะเมื่อx ∉ vars ( t ) เท่านั้น เนื่องจากการตรวจสอบเพิ่มเติมนี้ ซึ่งเรียกว่าการตรวจสอบการเกิดขึ้นทำให้ขั้นตอนวิธีช้าลง จึงถูกละเว้น เช่น ในระบบ Prolog ส่วนใหญ่ จากมุมมองทางทฤษฎี การละเว้นการตรวจสอบนี้เทียบเท่ากับการแก้สมการบนต้นไม้อนันต์ ดู#การรวมเทอมอนันต์ด้านล่าง

สำหรับการพิสูจน์การสิ้นสุดของอัลกอริทึม ให้พิจารณาสามสิ่งต่อไปนี้ โดยที่n _varคือจำนวนตัวแปรที่ปรากฏมากกว่าหนึ่งครั้งในชุดสมการn _lhsคือจำนวนสัญลักษณ์ฟังก์ชันและค่าคงที่ทางด้านซ้ายของสมการที่เป็นไปได้ และn _eqnคือจำนวนสมการ เมื่อใช้ กฎ eliminate n _varจะลดลง เนื่องจากxถูกกำจัดออกจากGและเก็บไว้เฉพาะใน { x ≐ t } การใช้กฎอื่นใดจะไม่สามารถเพิ่มn _varได้อีก เมื่อใช้ กฎ decompose , conflictหรือswap n _lhs จะลดลง เนื่องจากอย่างน้อย fที่อยู่นอกสุดทางด้านซ้ายจะหายไป การใช้กฎdeleteหรือcheck ที่เหลือ จะไม่สามารถเพิ่มn _lhs ได้ แต่จะลดn _eqnดังนั้น การใช้กฎใดๆ จะลดสามสิ่งต่อไปนี้เมื่อเทียบกับลำดับพจนานุกรมซึ่งเป็นไปได้เพียงจำนวนครั้งที่จำกัดเท่านั้น ${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangle }$${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangle }$

Conor McBrideสังเกต^{[ 18 ]}ว่า "โดยการแสดงโครงสร้างที่การรวมใช้ประโยชน์" ใน ภาษา ที่มีประเภทขึ้นอยู่กับเช่นEpigramอัลกอริทึมการรวมของ Robinsonสามารถทำให้เป็นแบบเรียกซ้ำตามจำนวนตัวแปรได้ ซึ่งในกรณีนี้การพิสูจน์การสิ้นสุดแยกต่างหากจึงไม่จำเป็น

ตามหลักไวยากรณ์ของ Prolog สัญลักษณ์ที่ขึ้นต้นด้วยตัวอักษรพิมพ์ใหญ่คือชื่อตัวแปร สัญลักษณ์ที่ขึ้นต้นด้วยตัวอักษรพิมพ์เล็กคือสัญลักษณ์ฟังก์ชัน และเครื่องหมายจุลภาคใช้เป็นตัวดำเนินการตรรกะ "และ" สำหรับสัญลักษณ์ทางคณิตศาสตร์ x , y, zใช้เป็นตัวแปรf, gใช้เป็นสัญลักษณ์ฟังก์ชัน และa, bใช้เป็นค่าคงที่

สัญกรณ์โปรล็อก	สัญกรณ์ทางคณิตศาสตร์	การทดแทนแบบรวม	คำอธิบาย
a = a	{ a = a }	{}	สำเร็จ ( ตรรกบท )
a = b	{ a = b }	⊥	aและbไม่ตรงกัน
X = X	{ x = x }	{}	สำเร็จ ( ตรรกบท )
a = X	{ a = x }	{ x ↦ a }	xถูกรวมเข้ากับค่าคงที่a
X = Y	{ x = y }	{ x ↦ y }	xและyเป็นค่าที่ซ้ำกัน
f(a,X) = f(a,b)	{ f ( a , x ) = f ( a , b ) }	{ x ↦ b }	สัญลักษณ์ฟังก์ชันและค่าคงที่ตรงกันxถูกรวมเข้ากับค่าคงที่b
f(a) = g(a)	{ f ( a ) = g ( a ) }	⊥	fและgไม่ตรงกัน
f(X) = f(Y)	{ f ( x ) = f ( y ) }	{ x ↦ y }	xและyเป็นค่าที่ซ้ำกัน
f(X) = g(Y)	{ f ( x ) = g ( y ) }	⊥	fและgไม่ตรงกัน
f(X) = f(Y,Z)	{ f ( x ) = f ( y , z ) }	⊥	ล้มเหลว สัญลักษณ์ของฟังก์ชัน fมีจำนวนอาร์กิวเมนต์ต่างกัน
f(g(X)) = f(Y)	{ f ( g ( x )) = f ( y ) }	{ y ↦ g ( x ) }	รวมyเข้ากับเทอม⁠ ⁠${\displaystyle g(x)}$
f(g(X),X) = f(Y,a)	{ f ( g ( x ), x ) = f ( y , a ) }	{ x ↦ a , y ↦ g ( a ) }	รวมxกับค่าคงที่aและyกับเทอม⁠ ⁠${\displaystyle g(a)}$
X = f(X)	{ x = f ( x ) }	ควรจะเป็น ⊥	ส่งคืนค่า ⊥ ในตรรกะลำดับที่หนึ่งและภาษา Prolog สมัยใหม่หลายภาษา (บังคับใช้โดยการตรวจสอบ occurs ) ใช้งานได้สำเร็จทั้งในภาษา Prolog แบบดั้งเดิมและ Prolog II โดยสามารถรวมxเข้ากับเทอมอนันต์x=f(f(f(f(...))))ได้
X = Y, Y = a	{ x = y , y = a }	{ x ↦ a , y ↦ a }	ทั้งxและyมีค่าคงที่เท่ากับa
a = Y, X = Y	{ a = y , x = y }	{ x ↦ a , y ↦ a }	ตามตัวอย่างข้างต้น (ลำดับของสมการในชุดไม่สำคัญ)
X = a, b = X	{ x = a , b = x }	⊥	ล้มเหลวaและbไม่ตรงกัน ดังนั้นxจึงไม่สามารถรวมกับทั้งสองได้

ตัวรวมทั่วไปที่สุดของปัญหาการรวมลำดับแรกทางไวยากรณ์ที่มีขนาดnอาจมีขนาด2nตัวอย่างเช่น ปัญหา⁠ ⁠${\displaystyle (((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))}$มีตัวรวมทั่วไปที่สุด⁠ ⁠${\displaystyle \{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*((a*a)*(a*a))\}}$ดังแสดงในภาพ เพื่อหลีกเลี่ยงความซับซ้อนของเวลาแบบเลขชี้กำลังที่เกิดจากการระเบิดดังกล่าว อัลกอริทึมการรวมขั้นสูงจึงทำงานบน^กราฟแบบไม่มีวงจรทิศทาง (DAG) แทนที่จะเป็นต้นไม้^{[ 19 ]}

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

ในบทนำ:

1. ตัวแปรสามารถรวมเข้ากับค่าคงที่ เทอม หรือตัวแปรอื่นได้ ซึ่งจะทำให้ตัวแปรนั้นกลายเป็นชื่อเรียกแทนของตัวแปรคงที่นั้นโดยปริยาย ในภาษาโปรล็อกสมัยใหม่หลายภาษาและในตรรกศาสตร์ลำดับที่หนึ่งตัวแปรไม่สามารถรวมเข้ากับเทอมที่มีตัวแปรนั้นอยู่ได้ นี่คือสิ่งที่เรียกว่าการตรวจสอบการเกิดขึ้น (occes check )
2. ค่าคงที่สองค่าจะสามารถรวมกันได้ก็ต่อเมื่อค่าคงที่ทั้งสองนั้นเหมือนกันทุกประการ
3. ในทำนองเดียวกัน เทอมหนึ่งสามารถรวมเข้ากับเทอมอื่นได้ หากสัญลักษณ์ฟังก์ชันสูงสุดและจำนวนพารามิเตอร์ของเทอมนั้นเหมือนกัน และหากพารามิเตอร์สามารถรวมเข้าด้วยกันได้พร้อมกัน โปรดทราบว่านี่เป็นพฤติกรรมแบบเรียกซ้ำ
4. การดำเนินการส่วนใหญ่ รวมถึง+, -, *, /, ไม่ได้รับการประเมินโดย=ดังนั้น ตัวอย่างเช่น1+2 = 3จึงไม่สามารถหาคำตอบได้เนื่องจากมีความแตกต่างกันทางไวยากรณ์ การใช้ข้อจำกัดทางเลขคณิตจำนวนเต็ม#=ทำให้เกิดรูปแบบหนึ่งของการรวม E ซึ่งการดำเนินการเหล่านี้ได้รับการตีความและประเมิน^{[ 20 ]}

โดยทั่วไปแล้วอัลกอริธึม การอนุมานประเภทจะใช้หลักการรวมประเภท โดยเฉพาะอย่างยิ่ง การอนุมานประเภทแบบ Hindley-Milnerซึ่งใช้ในภาษาโปรแกรมเชิงฟังก์ชันอย่าง HaskellและMLตัวอย่างเช่น เมื่อพยายามอนุมานประเภทของนิพจน์ Haskell True : ['x']คอมไพเลอร์จะใช้ประเภทa -> [a] -> [a]ของฟังก์ชันการสร้างลิสต์(:)ประเภทBoolของอาร์กิวเมนต์ตัวแรกTrueและประเภท[Char]ของอาร์กิวเมนต์ตัวที่สอง['x']ตัวแปรประเภทโพลีมอร์ฟิกaจะถูกรวมเข้ากับBoolและอาร์กิวเมนต์ตัวที่สอง[a]จะถูกรวมเข้ากับ[Char]ไม่aสามารถเป็นทั้งBoolและCharในเวลาเดียวกันได้ ดังนั้นนิพจน์นี้จึงไม่มีประเภทที่ถูกต้อง

เช่นเดียวกับ Prolog สามารถกำหนดอัลกอริธึมสำหรับการอนุมานประเภทได้ดังนี้:

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

การรวมเป็นหนึ่งเดียวถูกนำมาใช้ในสาขาวิจัยต่างๆ ของภาษาศาสตร์เชิงคำนวณ^{[ 21 ] [ 22 ]}

ตรรกะที่เรียงลำดับตามค่าช่วยให้สามารถกำหนดประเภทหรือชนิดให้กับแต่ละเทอม และประกาศประเภท s1เป็นประเภทย่อยของประเภท _{s2 ซึ่ง}โดยทั่วไปเขียนว่า _s1 ⊆ _s2 ตัวอย่าง เช่น เมื่อให้เหตุผลเกี่ยวกับสิ่งมีชีวิตทางชีววิทยา การประกาศให้ประเภท dogเป็นประเภทย่อยของประเภท animal นั้นมีประโยชน์ต้องการเทอมที่มีประเภท s ใดๆ ก็สามารถใช้เทอมที่มีประเภทย่อยใดๆ ของ sแทนได้ ตัวอย่างเช่น สมมติว่ามีการประกาศฟังก์ชัน mother : animal → animalและการประกาศค่าคงที่ lassie : dogเทอม mother ( lassie ) นั้นถูกต้องและมีประเภท animalเพื่อให้ได้ข้อมูลว่าแม่ของ dog เป็น dog อีกที ก็อาจมีการประกาศ mother : dog → dog อีกครั้ง ซึ่งเรียกว่าการโอเวอร์โหลดฟังก์ชันคล้ายกับการโอเวอร์โหลดในภาษาโปรแกรม

Waltherได้เสนออัลกอริทึมการรวมสำหรับเงื่อนไขในตรรกะเรียงลำดับ โดยกำหนดให้สำหรับประเภทที่ประกาศไว้สองประเภทใดๆs ₁ , s ₂จะต้องประกาศส่วนร่วมของพวกมันs ₁ ∩ s _{2 ด้วยเช่นกัน: ถ้า} x ₁และx ₂เป็นตัวแปรประเภทs ₁และs ₂ตามลำดับ สมการx ₁ ≐ x ₂จะมีคำตอบ { x ₁ = x , x ₂ = x } โดยที่x : s ₁ ∩ s ₂ ^{[ 23} ] หลังจากรวมอัลกอริทึมนี้เข้ากับตัวพิสูจน์ทฤษฎีบทอัตโนมัติแบบอิงตามข้อความ เขาสามารถแก้ปัญหามาตรฐานได้โดยการแปลเป็นตรรกะเรียงลำดับ ซึ่ง ^{ทำให้} ลดขนาดลงไปหนึ่งลำดับ เนื่องจากตัวบ่งชี้เอกภาคจำนวนมากกลายเป็นประเภท

Smolka ได้วางแนวทางทั่วไปของตรรกะเรียงลำดับเพื่อให้สามารถใช้โพลีมอร์ฟิซึมแบบพารามิเตอร์ได้ [ ^{24 ] ใน} กรอบงานของเขา การประกาศการเรียงลำดับย่อยจะถูกส่งต่อไปยังนิพจน์ประเภทที่ซับซ้อน ตัวอย่างเช่น รายการเรียงลำดับแบบพารามิเตอร์( X )อาจถูกประกาศ (โดยที่Xเป็นพารามิเตอร์ประเภทเช่นเดียวกับในเทมเพลต C++ ) และจากการประกาศการเรียงลำดับย่อยint ⊆ floatความสัมพันธ์list ( int ) ⊆ list ( float ) จะถูกอนุมานโดยอัตโนมัติ ซึ่งหมายความว่าแต่ละรายการของจำนวนเต็มก็เป็นรายการของจำนวนทศนิยมด้วย

Schmidt-Schauß ได้ขยายตรรกะเรียงลำดับทั่วไปเพื่อให้สามารถประกาศเทอมได้ ^{[ 25 ]} ตัวอย่างเช่น สมมติว่ามีการประกาศซับซอร์ตeven ⊆ intและodd ⊆ intการประกาศเทอมเช่น ∀ i  : int . ( i + i ) : evenอนุญาตให้ประกาศคุณสมบัติของการบวกจำนวนเต็มที่ไม่สามารถแสดงได้ด้วยการโอเวอร์โหลดแบบปกติ

ข้อมูลเบื้องต้นเกี่ยวกับต้นไม้อนันต์:

• B. Courcelle (1983). "คุณสมบัติพื้นฐานของต้นไม้อนันต์" . Theoret. Comput. Sci . 25 (2): 95– 169. doi : 10.1016/0304-3975(83)90059-2 .
• Michael J. Maher (กรกฎาคม 1988). "การกำหนดสัจพจน์ที่สมบูรณ์ของพีชคณิตของต้นไม้จำกัด ต้นไม้ตรรกยะ และต้นไม้อนันต์". รายงานการประชุมสัมมนาประจำปีครั้งที่ 3 ของ IEEE ว่าด้วยตรรกศาสตร์ในวิทยาการคอมพิวเตอร์ เอดินบะระหน้า  348–357 .
• Joxan Jaffar; Peter J. Stuckey (1986). "ความหมายของการเขียนโปรแกรมตรรกะต้นไม้อนันต์" . วิทยาศาสตร์คอมพิวเตอร์เชิงทฤษฎี . 46 : 141– 158. doi : 10.1016/0304-3975(86)90027-7 .

อัลกอริทึมการรวม, Prolog II:

• A. Colmerauer (1982). KL Clark; S.-A. Tarnlund (บรรณาธิการ). Prolog และ Infinite Trees . Academic Press.
• Alain Colmerauer (1984). "สมการและอสมการบนต้นไม้จำกัดและอนันต์" ใน ICOT (บรรณาธิการ). รายงานการประชุมนานาชาติว่าด้วยระบบคอมพิวเตอร์ยุคที่ห้าหน้า  85–99

การใช้งาน:

• Francis Giannesini; Jacques Cohen (1984). "การสร้างตัวแยกวิเคราะห์และการจัดการไวยากรณ์โดยใช้ต้นไม้อนันต์ของ Prolog"วารสารการเขียนโปรแกรมเชิงตรรกะ 1 ( 3): 253– 265. doi : 10.1016/0743-1066(84)90013-X .

การรวมสมการ ( E-unification)คือปัญหาของการหาคำตอบสำหรับชุดสมการ ที่กำหนด โดยคำนึงถึงความรู้พื้นฐานเกี่ยวกับสมการEซึ่งกำหนดไว้ในรูปของชุดความเท่าเทียม กันสากล สำหรับชุด E บางชุด ได้มีการคิดค้น อัลกอริทึมแก้สมการ(หรือที่เรียกว่าอัลกอริทึมการรวมสมการ E ) ขึ้นมาแล้ว แต่สำหรับ ชุดอื่นๆ นั้น ได้มีการพิสูจน์แล้วว่าไม่มีอัลกอริทึมดังกล่าวอยู่จริง

ตัวอย่างเช่น ถ้าaและbเป็นค่าคงที่ที่ต่างกันสมการจะไม่มี${\displaystyle x*a\doteq y*b}$คำตอบในแง่ของการรวมเชิงไวยากรณ์ ล้วนๆ โดยที่ไม่ทราบอะไรเกี่ยวกับตัวดำเนินการเลยอย่างไรก็ตาม${\displaystyle *}$ถ้าทราบว่าตัวดำเนินการนั้น มีคุณสมบัติ ${\displaystyle *}$การสลับที่ได้ การแทนที่{ x ↦ b , y ↦ a }จะแก้สมการข้างต้นได้ เนื่องจาก

	⁠ ⁠${\displaystyle x*a}$	{ x ↦ b , y ↦ a }
=	⁠ ⁠${\displaystyle b*a}$		โดยการยื่นคำร้องขอเปลี่ยนตัว
=	⁠ ⁠${\displaystyle a*b}$		โดยสมบัติการสลับที่ของ⁠ ⁠${\displaystyle *}$
=	⁠ ⁠${\displaystyle y*b}$	{ x ↦ b , y ↦ a }	โดยการประยุกต์ใช้การแทนที่ (แบบผกผัน)

ความรู้พื้นฐานEสามารถระบุคุณสมบัติการสลับที่ของ⁠ ⁠ ได้${\displaystyle *}$โดยใช้ความเท่าเทียมกันสากล " ⁠ ⁠${\displaystyle u*v=v*u}$สำหรับทุกu , v "

หลักเกณฑ์การตั้งชื่อที่ใช้

∀ u , v , w :	⁠ ⁠${\displaystyle u*(v*w)}$	=	⁠ ⁠${\displaystyle (u*v)*w}$	เอ	ความสัมพันธ์เชิงสมาคมของ⁠ ⁠${\displaystyle *}$
∀ u , v :	⁠ ⁠${\displaystyle u*v}$	=	⁠ ⁠${\displaystyle v*u}$	ซี	คุณสมบัติการสลับที่ของ⁠ ⁠${\displaystyle *}$
∀ u , v , w :	⁠ ⁠${\displaystyle u*(v+w)}$	=	⁠ ⁠${\displaystyle u*v+u*w}$	ดีแอล	การกระจายตัวทางซ้ายของ⁠ ⁠${\displaystyle *}$เหนือ⁠ ⁠${\displaystyle +}$
∀ u , v , w :	⁠ ⁠${\displaystyle (v+w)*u}$	=	⁠ ⁠${\displaystyle v*u+w*u}$	ดร.	การกระจายตัวทางขวาของ⁠ ⁠${\displaystyle *}$เหนือ⁠ ⁠${\displaystyle +}$
∀ u :	⁠ ⁠${\displaystyle u*u}$	=	คุณ	ฉัน	ความไร้สมรรถภาพทางเพศของ⁠ ⁠${\displaystyle *}$
∀ u :	⁠ ⁠${\displaystyle n*u}$	=	คุณ	เอ็นแอล	องค์ประกอบกลางด้านซ้ายnเมื่อเทียบกับ⁠ ⁠${\displaystyle *}$
∀ u :	⁠ ⁠${\displaystyle u*n}$	=	คุณ	น.ร.​	องค์ประกอบกลางด้านขวาnเมื่อเทียบกับ⁠ ⁠${\displaystyle *}$

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

สามารถสรุปผลการรวมทฤษฎีได้สำหรับทฤษฎีต่อไปนี้:

• A ^{[ 26 ]}
• A , C ^{[ 27 ]}
• A , C , I ^{[ 28 ]}
• A , C , N _l ^{[หมายเหตุ 9 ] [ 28 ]}
• A ,ฉัน^{[ 29 ]}
• A , N _l , N _r (โมโนอิด) ^{[ 30 ]}
• C ^{[ 28 ]}
• วงแหวนบูลีน^{[ 31 ] [ 32 ]}
• กลุ่มอาเบเลียนแม้ว่าลายเซ็นจะถูกขยายด้วยสัญลักษณ์เพิ่มเติมตามอำเภอใจ (แต่ไม่ใช่สัจพจน์) ^{[ 33 ]}
• พีชคณิตโมดอลK4 ^{[ 34 ]}

การรวมเป็นหนึ่งเดียวสามารถตัดสินได้บางส่วนสำหรับทฤษฎีต่อไปนี้:

• A , D _l , D _r ^{[ 35 ]}
• A , C , D _l ^{[หมายเหตุ 9 ] [ 36 ]}
• วงแหวนสลับตำแหน่ง^{[ 33 ]}

หากมีระบบการเขียนใหม่เทอมบรรจบRสำหรับEอัลกอริทึมพาราโมดูเลชันด้านเดียว^{[ 37 ]} สามารถใช้เพื่อแจงนับโซลูชันทั้งหมดของสมการที่กำหนด

เริ่มต้นด้วยGซึ่งเป็นปัญหาการรวมที่ต้องแก้ไข และSเป็นการแทนที่เอกลักษณ์ กฎต่างๆ จะถูกนำมาใช้แบบไม่แน่นอนจนกว่าเซตว่างจะปรากฏเป็นG ที่แท้จริง ในกรณีนี้S ที่แท้จริง จะเป็นการแทนที่แบบรวม ขึ้นอยู่กับลำดับที่กฎการปรับพารามิเตอร์ถูกนำมาใช้ การเลือกสมการที่แท้จริงจากGและการเลือก กฎ ของRในmutateเส้นทางการคำนวณที่แตกต่างกันจึงเป็นไปได้ บางเส้นทางเท่านั้นที่นำไปสู่คำตอบ ในขณะที่บางเส้นทางสิ้นสุดที่G ≠ {} ซึ่งไม่มีกฎใดใช้ได้อีกต่อไป (เช่นG = { f (...) ≐ g (...) })

ตัวอย่างเช่น ระบบการเขียนใหม่ของเทอมRถูกใช้เพื่อกำหนด ตัวดำเนินการ ต่อท้ายของรายการที่สร้างจากconsและnilโดยที่cons ( x , y ) ถูกเขียนในรูปแบบอินฟิกซ์เป็นx . yเพื่อความกระชับ เช่นapp ( a . b . nil , c . d . nil ) → a . app ( b . nil , c . d . nil ) → a . b . app ( nil , c . d . nil ) → a . b . c . d . nilแสดงให้เห็นถึงการต่อกันของรายการa . b . nilและc . d . nilโดยใช้กฎการเขียนใหม่ 2, 2 และ 1 ทฤษฎีสมการEที่สอดคล้องกับRคือการปิดความสอดคล้องของRซึ่งทั้งสองอย่างถูกมองว่าเป็นความสัมพันธ์ทวิภาคบนเทอม ตัวอย่างเช่นapp ( a . b . nil , c . d . nil ) ≡ a . b . c . d . nil ≡ app ( a . b . c . d . nil , nil ) อัลกอริทึมพาราโมดูเลชันจะแจงนับคำตอบของสมการโดยสัมพันธ์กับEเมื่อป้อนตัวอย่างRเข้าไป

ตัวอย่างเส้นทางการคำนวณที่ประสบความสำเร็จสำหรับปัญหาการรวม { app ( x , app ( y , x )) ≐ a . a . nil } แสดงอยู่ด้านล่าง เพื่อหลีกเลี่ยงการชนกันของชื่อตัวแปร กฎการเขียนใหม่จะถูกเปลี่ยนชื่ออย่างสม่ำเสมอทุกครั้งก่อนใช้งานโดยกฎmutate ; v ₂ , v ₃ , ... เป็นชื่อตัวแปรที่สร้างโดยคอมพิวเตอร์เพื่อจุดประสงค์นี้ ในแต่ละบรรทัด สมการที่เลือกจากGจะถูกไฮไลต์ด้วยสีแดง ทุกครั้ง ที่ใช้กฎ mutateกฎการเขียนใหม่ที่เลือก ( 1หรือ2 ) จะถูกระบุไว้ในวงเล็บ จากบรรทัดสุดท้ายสามารถหา การแทนที่แบบรวม S = { y ↦ nil , x ↦ a . nil } ได้ ในความเป็นจริง app ( x , app ( y , x )) { y ↦ nil , x ↦ a . nil } = app ( a . nil , app ( nil , a . nil )) ≡ app ( a . nil , a . nil ) ≡ a . app ( nil , a . nil ) ≡ a . a . nilแก้ปัญหาที่กำหนดได้ เส้นทางการคำนวณที่ประสบความสำเร็จอีกเส้นทางหนึ่ง ซึ่งได้มาจากการเลือก "mutate(1), mutate(2), mutate(2), mutate(1)" นำไปสู่การแทนที่S = { y ↦ a . a . nil , x ↦ nil }; ซึ่งไม่ได้แสดงไว้ในที่นี้ ไม่มีเส้นทางอื่นใดที่นำไปสู่ความสำเร็จ

ถ้าRเป็นระบบการเขียนใหม่ของพจน์ลู่เข้าสำหรับEแนวทางอื่นนอกเหนือจากส่วนก่อนหน้าคือการประยุกต์ใช้ " ขั้นตอน การจำกัดขอบเขต " อย่างต่อเนื่อง ซึ่งในที่สุดจะสามารถแจงนับคำตอบทั้งหมดของสมการที่กำหนดได้ ขั้นตอนการจำกัดขอบเขต (ดูภาพประกอบ) ประกอบด้วย

• การเลือกพจน์ย่อยที่ไม่เปลี่ยนแปลงของพจน์ปัจจุบัน
• โดยการรวมไวยากรณ์เข้ากับด้านซ้ายของกฎจากRและ
• แทนที่ด้านขวามือของกฎที่สร้างขึ้นลงในเทอมที่สร้างขึ้น

ตามหลักการแล้ว ถ้าl → rเป็นสำเนาที่เปลี่ยนชื่อของกฎการเขียนใหม่จากRโดยไม่มีตัวแปรใดที่เหมือนกันกับเทอมsและเทอมย่อยs | _pไม่ใช่ตัวแปรและสามารถรวมเป็นหนึ่งเดียวกับl ได้ ผ่านทางmgu σแล้วsสามารถลดทอนให้แคบลงเหลือเทอมt = sσ [ rσ ] _{p ได้}นั่นคือเหลือเทอมsσโดยที่เทอมย่อยที่p ถูกแทนที่ด้วยrσสถานการณ์ที่sสามารถลดทอนให้แคบลงเหลือtมักจะใช้สัญลักษณ์s ↝ tโดยสัญชาตญาณแล้ว ลำดับขั้นตอนการลดทอนt ₁ ↝ t ₂ ↝ ... ↝ t _nสามารถคิดได้ว่าเป็นลำดับขั้นตอนการเขียนใหม่t ₁ → t ₂ → ... → t _nแต่เทอมเริ่มต้นt ₁จะถูกสร้างขึ้นเรื่อยๆ ตามความจำเป็นเพื่อให้กฎแต่ละข้อที่ใช้สามารถนำไปใช้ได้

การคำนวณพาราโมดูเลชัน ตัวอย่างข้างต้นสอดคล้องกับลำดับการแคบลงต่อไปนี้ ("↓" แสดงถึงการสร้างอินสแตนซ์ในที่นี้):

เทอมสุดท้ายv ₂ . v ₂ . nilสามารถรวมเข้ากับเทอมด้านขวาเดิมa . a . nilได้ ทางไวยากรณ์

บทพิสูจน์การจำกัดขอบเขต^{[ 38 ]}รับประกันว่าเมื่อใดก็ตามที่อินสแตนซ์ของเทอมsสามารถเขียนใหม่เป็นเทอมtโดยระบบการเขียนเทอมใหม่แบบลู่เข้าsและtก็ สามารถจำกัดขอบเขตและเขียนใหม่เป็นเทอมs ′และt ′ตามลำดับ โดยที่t ′เป็นอินสแตนซ์ของs ′

ในเชิงรูปธรรม: เมื่อใดก็ตามที่sσ→*ถ้า tเป็นจริงสำหรับการแทนที่ σ บางอย่าง ก็จะมีเทอม s ′ , t ′ อยู่ ซึ่ง s↝*s ′และ t→*t ′และ s ′ τ = t ′สำหรับการแทนที่ τ บางค่า

แอปพลิเคชันจำนวนมากต้องการให้พิจารณาการรวมเทอมแลมบ์ดาแบบมีประเภทแทนที่จะเป็นเทอมลำดับแรก การรวมดังกล่าวมักเรียกว่า^การรวมลำดับสูงการรวมลำดับสูงไม่สามารถตัดสินได้ [ ^{39 ] [ 40 ] [ 41 ]}และปัญหาการรวมดังกล่าวไม่มีตัวรวมทั่วไปส่วนใหญ่ ตัวอย่างเช่น ปัญหาการรวม { f ( a , b , a ) ≐ d ( b , a , c ) } โดยที่ตัวแปรเดียวคือfมีคำตอบ { f ↦ λ x .λ y .λ z . d ( y , x , c ) }, { f ↦ λ x .λ y .λ z . d ( y , z , c ) }, { f ↦ λ x .λ y .λ z . d ( y , a , c ) }, { f ↦ λ x .λ y .λ z . d ( b , x , c ) }, { f ↦ λ x .λ y .λ z . d ( b , z , c ) } และ { f ↦ λ x .λ y .λ z . d ( b , a , c ) } สาขาหนึ่งของการรวมลำดับสูงที่ได้รับการศึกษาอย่างดีคือปัญหาของการรวมเทอมแลมบ์ดาที่มีประเภทง่ายๆ โมดูลัสความเท่าเทียมกันที่กำหนดโดยการแปลง αβη Gérard Huetได้นำเสนออัลกอริทึมการรวม (ก่อน) ที่สามารถตัดสินได้บางส่วน^{[ 42 ]}ซึ่งอนุญาตให้ค้นหาพื้นที่ของตัวรวมอย่างเป็นระบบ (โดยขยายอัลกอริทึมการรวมของ Martelli-Montanari ^{[ 5 ]}ด้วยกฎสำหรับเทอมที่มีตัวแปรลำดับสูงกว่า) ซึ่งดูเหมือนว่าจะใช้งานได้ดีพอสมควรในทางปฏิบัติ Huet ^{[ 43 ]}และ Gilles Dowek ^{[ 44 ]}ได้เขียนบทความสำรวจหัวข้อนี้ไว้แล้ว

เซตย่อยหลายเซตของการรวมลำดับสูงมีพฤติกรรมที่ดี กล่าวคือ เซตย่อยเหล่านี้สามารถตัดสินได้และมีตัวรวมทั่วไปที่สุดสำหรับปัญหาที่แก้ไขได้ เซตย่อยหนึ่งดังกล่าวคือเทอมลำดับแรกที่อธิบายไว้ก่อนหน้านี้การรวมรูปแบบลำดับสูงซึ่งพัฒนาโดย Dale Miller ^{[ 45 ]}เป็นเซตย่อยอีกเซตหนึ่งเช่นกัน ภาษาการเขียนโปรแกรมตรรกะลำดับสูงλPrologและTwelfได้เปลี่ยนจากการรวมลำดับสูงแบบเต็มรูปแบบไปเป็นการใช้งานเฉพาะส่วนของรูปแบบเท่านั้น น่าประหลาดใจที่การรวมรูปแบบนั้นเพียงพอสำหรับโปรแกรมเกือบทั้งหมด หากปัญหาการรวมรูปแบบที่ไม่ใช่ปัญหาหนึ่งๆ ถูกระงับไว้จนกว่าการแทนที่ในภายหลังจะทำให้การรวมเข้าไปอยู่ในส่วนของรูปแบบ เซตย่อยของการรวมรูปแบบที่เรียกว่าการรวมฟังก์ชันในฐานะตัวสร้างก็มีพฤติกรรมที่ดีเช่นกัน^{[ 46 ]}ตัวพิสูจน์ทฤษฎีบท Zipperposition มีอัลกอริทึมที่รวมเซตย่อยที่มีพฤติกรรมที่ดีเหล่านี้เข้ากับอัลกอริทึมการรวมลำดับสูงแบบเต็มรูปแบบ^{[ 2 ]}

ในภาษาศาสตร์เชิงคำนวณ หนึ่งในทฤษฎีที่มีอิทธิพลมากที่สุดของการสร้างแบบวงรีคือ วงรีจะถูกแทนด้วยตัวแปรอิสระซึ่งค่าของตัวแปรเหล่านั้นจะถูกกำหนดโดยใช้การรวมลำดับที่สูงกว่า ตัวอย่างเช่น การแสดงความหมายของ "จอนชอบแมรี่และปีเตอร์ก็ชอบด้วย" คือ like( j , m ) ∧ R( p )และค่าของ R (การแสดงความหมายของวงรี) จะถูกกำหนดโดยสมการlike( j , m ) = R( j ) กระบวนการแก้สมการดังกล่าวเรียกว่าการรวมลำดับที่สูงกว่า^{[ 47 ]}

Wayne Snyderได้ให้การวางนัยทั่วไปของการรวมลำดับที่สูงกว่าและการรวม E กล่าวคือ อัลกอริทึมในการรวมเทอมแลมบ์ดาโมดูลทฤษฎีสมการ^{[ 48 ]}

• การเขียนใหม่
• กฎที่ยอมรับได้
• การแทนที่แบบชัดเจนในแคลคูลัสแลมบ์ดา
• การแก้สมการทางคณิตศาสตร์
• การแยกส่วน : การแก้ความไม่สมดุลระหว่างการแสดงออกเชิงสัญลักษณ์
• การต่อต้านการรวม : การคำนวณการสรุปทั่วไปน้อยที่สุด (lgg) ของสองเทอม ซึ่งเป็นสิ่งที่ตรงกันข้ามกับการคำนวณอินสแตนซ์ทั่วไปมากที่สุด (mgu)
• แลตทิซการครอบคลุม (Subsumption lattice)คือแลตทิซที่มีการรวมเป็นหนึ่ง (meet) และการต่อต้านการรวมเป็นหนึ่ง (join)
• การจัดเรียงออนโทโลยี (ใช้การรวมเข้าด้วยกันโดยมีความเท่าเทียมกันทางความหมาย )

ลองค้นหาคำว่า "การรวมชาติ"ในวิกิพีเดีย ซึ่งเป็นพจนานุกรมเสรี

• Franz BaaderและWayne Snyder (2001). "ทฤษฎีการรวมเป็นหนึ่งเดียว"ในJohn Alan RobinsonและAndrei Voronkovบรรณาธิการ, Handbook of Automated Reasoningเล่มที่ 1 หน้า 447–533. สำนักพิมพ์ Elsevier Science Publishers.
• Gilles Dowek (2001). "Higher-order Unification and Matching" เก็บถาวรเมื่อ 2019-05-15 ที่Wayback MachineในHandbook of Automated Reasoning
• Franz Baader และTobias Nipkow (1998). การเขียนคำศัพท์ใหม่และเรื่องอื่นๆ . สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์
• Franz Baader และJörg H. Siekmann (1993). "ทฤษฎีการรวมเป็นหนึ่งเดียว" ในคู่มือตรรกศาสตร์ในปัญญาประดิษฐ์และการเขียนโปรแกรมเชิงตรรกะ
• Jean-Pierre Jouannaud และClaude Kirchner (1991). "การแก้สมการในพีชคณิตนามธรรม: การสำรวจการรวมเป็นหนึ่งเดียวโดยใช้กฎเกณฑ์" ในตรรกศาสตร์เชิงคำนวณ: บทความเพื่อเป็นเกียรติแก่ Alan Robinson
• Nachum DershowitzและJean-Pierre Jouannaud , Rewrite Systems , ใน: Jan van Leeuwen (บรรณาธิการ), Handbook of Theoretical Computer Science , เล่ม B Formal Models and Semantics , Elsevier, 1990, หน้า 243–320
• Jörg H. Siekmann (1990). "ทฤษฎีการรวมเป็นหนึ่ง". ในClaude Kirchner (บรรณาธิการ) การรวมเป็นหนึ่ง . สำนักพิมพ์ Academic Press.
• เควิน ไนท์ (มีนาคม 1989). "การรวมเป็นหนึ่งเดียว: การสำรวจแบบสหวิทยาการ" (PDF) . ACM Computing Surveys . 21 (1): 93– 124. CiteSeerX  10.1.1.64.8967 . doi : 10.1145/62029.62030 . S2CID  14619034 .
• เจราร์ด ฮิวเอตและดีเร็ก ซี. ออปเพน (1980) "สมการและกฎการเขียนใหม่: แบบสำรวจ" . รายงานทางเทคนิค มหาวิทยาลัยสแตนฟอร์ด.
• Raulefs, Peter; Siekmann, Jörg; Szabó, P.; Unvericht, E. (1979). "การสำรวจสั้นๆ เกี่ยวกับสถานะของศิลปะในปัญหาการจับคู่และการรวม" ACM SIGSAM Bulletin . 13 (2): 14– 20. doi : 10.1145/1089208.1089210 . S2CID  17033087 .
• Claude Kirchner และ Hélène Kirchner. การเขียนใหม่ การแก้ปัญหา การพิสูจน์ . อยู่ระหว่างการจัดทำ