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

• เซตอนันต์${\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}$.
• ทฤษฎีหรือความสัมพันธ์สมมูล${\displaystyle \equiv }$บน${\displaystyle T}$ซึ่งบ่งชี้ว่าเงื่อนไขใดบ้างที่ถือว่าเท่าเทียมกัน สำหรับการรวม E ลำดับที่หนึ่ง${\displaystyle \equiv }$สะท้อนให้เห็นถึงความรู้พื้นฐานเกี่ยวกับสัญลักษณ์ฟังก์ชันบางอย่าง ตัวอย่างเช่น ถ้า${\displaystyle \oplus }$ถือว่าเป็นสมบัติสลับที่ได้${\displaystyle t\equiv u}$ถ้า${\displaystyle u}$ผลลัพธ์จาก${\displaystyle t}$โดยการสลับอาร์กิวเมนต์ของ${\displaystyle \oplus }$ในบางกรณี (อาจจะทุกกรณี) ^{[หมายเหตุ 1 ]}ในกรณีทั่วไปที่ไม่มีความรู้พื้นฐานเลย เฉพาะคำที่เหมือนกันตามตัวอักษรหรือตามไวยากรณ์เท่านั้นที่จะถือว่าเท่ากัน ในกรณีนี้ ≡ เรียกว่าทฤษฎีอิสระ (เพราะเป็นวัตถุอิสระ ) ทฤษฎีว่างเปล่า (เพราะเซตของประโยค สมการ หรือความรู้พื้นฐานว่างเปล่า) ทฤษฎีของฟังก์ชันที่ไม่ได้ตีความ (เพราะการรวมทำบนคำ ที่ไม่ได้ตีความ ) หรือทฤษฎีของตัวสร้าง (เพราะสัญลักษณ์ฟังก์ชันทั้งหมดสร้างคำข้อมูลขึ้นมาแทนที่จะดำเนินการกับคำเหล่านั้น) สำหรับการรวมลำดับที่สูงกว่า โดยปกติแล้ว${\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 ↦ (ค่าใดๆ) }

การแทนที่คือการจับคู่${\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}$ตัวอย่างลำดับแรกคือ การใช้การแทนที่{ x ↦ h ( a , y ), z ↦ b }กับเทอม

	${\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}$.

ถ้า ≡ คือความเหมือนกันทางไวยากรณ์ (literal identity) ของคำศัพท์ คำศัพท์หนึ่งอาจมีความทั่วไปและเฉพาะเจาะจงกว่าอีกคำศัพท์หนึ่งได้ก็ต่อเมื่อคำศัพท์ทั้งสองแตกต่างกันเพียงแค่ชื่อตัวแปรเท่านั้น ไม่ใช่โครงสร้างทางไวยากรณ์ คำศัพท์ดังกล่าวเรียกว่าตัวแปรหรือการเปลี่ยนชื่อของกันและกัน ตัวอย่างเช่น ${\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})}$เนื่องจากไม่มีการแทนที่ใดที่จะเปลี่ยนพจน์หลังให้เป็นพจน์แรกได้ ดังนั้นพจน์หลังจึงมีความพิเศษกว่าพจน์แรกอย่างแท้จริง

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

การทดแทน${\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 }$[ ^{2 ] ตัวอย่าง} เช่น${\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)}$[ ^{3 ]​}

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

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

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

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 ]}กำหนดให้เซตจำกัด${\displaystyle G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}}$สำหรับสมการที่เป็นไปได้หลายสมการ อัลกอริทึมจะใช้กฎในการแปลงให้เป็นชุดสมการที่เทียบเท่ากันในรูปแบบ { x ≐ u , ..., x ≐ u } โดยที่x , ..., x เป็นตัวแปรที่แตกต่างกัน และu , ..., u เป็นพจน์ที่ไม่มีx อยู่เลย ชุดสมการในรูปแบบนี้สามารถอ่านได้ว่าเป็นการแทนที่ หากไม่มีคำตอบ อัลกอริทึมจะสิ้นสุดด้วย ⊥; ผู้เขียนคนอื่นใช้ "Ω" หรือ " fail " ในกรณีนั้น การดำเนินการแทนที่ตัวแปรx ทั้งหมด ในปัญหาGด้วยพจน์tจะถูกเขียนแทนด้วยG { x ↦ t } เพื่อความง่าย สัญลักษณ์คงที่ถือเป็นสัญลักษณ์ฟังก์ชันที่มีอาร์กิวเมนต์เป็นศูนย์

${\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}))}$		ตรวจสอบ

ตามหลักไวยากรณ์ของ 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 โดยการรวมxx=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))\}}$⁠ , cf. picture. เพื่อหลีกเลี่ยงความซับซ้อนของเวลาแบบเลขชี้กำลังที่เกิดจากการระเบิดดังกล่าว อัลกอริทึมการรวมขั้นสูงจึงทำงานบนกราฟแบบไม่มีวงจรทิศทาง (DAGS) แทนที่จะเป็นต้นไม้ ^{[ 19 ]}

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

ในบทนำ:

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

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

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

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

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

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

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

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

• A , D , D ^{[ 35 ]}
• A , C , D ^{[หมายเหตุ 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 | ไม่ใช่ตัวแปรและสามารถรวมเป็นหนึ่งเดียวกับl ได้ ผ่านทางmgu σแล้วsสามารถลดทอนให้แคบลงเหลือเทอมt = sσ [ rσ ] นั่นคือเหลือเทอมsσโดยที่เทอมย่อยที่p ถูกแทนที่ด้วยrσสถานการณ์ที่sสามารถลดทอนให้แคบลงเหลือtมักจะใช้สัญลักษณ์s ↝ tโดยสัญชาตญาณแล้ว ลำดับขั้นตอนการลดทอนt ↝ t ↝ ... ↝ t สามารถคิดได้ว่าเป็นลำดับขั้นตอนการเขียนใหม่t → t → ... → t แต่เทอมเริ่มต้น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 ′สำหรับการแทนที่ τ บางอย่าง