Chapter 10: Unification and anti-unification

Introduction

This chapter introduces unification as filling holes to make structures equal and anti-unification as replacing differences with holes to find shared generalizations.

• Unification direction and purpose: Explain unification as finding substitutions for holes that make two things equal, and describe it as moving from general terms with holes toward a specific satisfactory result.
  Why it matters: This is the central problem that the chapter’s binary-term algorithms solve.
• Anti-unification generalization: Describe anti-unification as starting with two unequal specific things, retaining their common parts, and turning the differing parts into holes to form a generalization.
  Why it matters: Anti-unification makes similarities explicit, enabling later code-analysis applications such as inferring bug-fixing patterns.
• Chapter application roadmap: State that the chapter applies unification to binary trees and connects it to arbitrary logic problems, type inference, and logic programming, then applies anti-unification to similarity-oriented code analysis including bug-fixing-pattern deduction.
  Why it matters: The applications show why these apparently abstract operations are useful beyond the tree algorithms themselves.

Key terms: unification, holes, substitution, anti-unification, generalizations, binary trees, logic problems, type inference, logic programming, code analysis

10.1 Unifying binary terms

This section introduces binary terms, substitutions, and the first-order unification problem by translating an immutable-stack matching puzzle into terms.

• Binary term representation: Describe the three kinds of binary terms—holes, constants, and symbols—and how each is written and compared for equality.
  Why it matters: Binary terms provide the common structure that lets unification work on problems without reasoning about a domain such as stacks directly.
• Substitutions and bound holes: Explain that a substitution maps holes to terms, distinguishes bound from free holes, and recursively replaces bound holes until none remain in the substituted result.
  Why it matters: A substitution is the result that makes two terms equal, and recursive replacement ensures that chained bindings are fully resolved.
• Stack puzzle as unification: Trace how the stack puzzle becomes a binary-term unification problem, including the deductions X→two and Y→stackOne that make the two terms equal.
  Why it matters: The example shows why representing a domain problem as terms allows the same unification reasoning to be automated and reused.

Key terms: binary term, term, hole, constant, symbol, first-order binary term, substitution, bound hole, free hole, Substitute

10.1.1 Unifying binary terms, first attempt

This section presents a plausible recursive unification algorithm for binary terms, then exposes how rebinding a hole can create contradictory or cyclic substitutions that require an occurs check.

• First-attempt unification rules: Describe how the first-attempt algorithm compares two binary terms and builds a substitution. State that equal terms succeed, a hole is bound to the other term, matching symbols recurse on their left and right children, and a mismatch or failed recursive call fails.
  Why it matters: These rules establish the basic recursive structure that the corrected unification algorithm will retain.
• Recursive substitution chains: Explain why Substitute must recurse through a substituted term rather than making only one replacement. In the successful example, replacing Y with stackOne must also replace the X contained inside stackOne with its binding to two.
  Why it matters: Following substitution chains is necessary to produce terms with all bound holes eliminated.
• Cyclic rebinding failure: Explain why the first-attempt algorithm fails when the same hole receives incompatible bindings or is rebound to a term containing itself. Describe the X→two followed by X→stackOne case, and connect it to either a duplicate-key/replaced-binding problem or unbounded recursive Substitute calls that end in stack overflow.
  Why it matters: This failure demonstrates why unification needs an occurs check before accepting a hole binding.

Key terms: unification, binary terms, substitution, hole, symbol, Substitute, bound holes, occurs check, unbounded recursion, stack-overflow exception

10.1.2 Unifying binary terms, this time with an occurs check

This subsection corrects binary-term unification by following hole aliases during the occurs check and by dereferencing already bound holes before continuing unification.

• Alias-aware occurs check: Explain why an occurs check must follow bound-hole substitutions, not merely inspect the holes visibly present in a term. Describe how checking through aliases prevents cyclic substitutions that make substitution recurse forever.
  Why it matters: Following aliases is what prevents a seemingly valid substitution from creating an infinite self-reference.
• Bound-hole dereferencing: Describe why unification must look up a hole that is already bound and restart unification on its bound term. Explain that this compares a hole's existing meaning with its proposed new meaning instead of silently assigning it twice.
  Why it matters: Dereferencing bound holes ensures that every occurrence of a hole remains consistent with its one established binding.
• Correct binary-term unification rules: Trace the corrected first-order binary-term unification algorithm: dereference bound holes, accept equal terms, bind free holes only after the alias-aware occurs check, and recursively unify matching symbols' children using one substitution. State when it fails, including incompatible symbols or a failed recursive child unification.
  Why it matters: These rules turn unification into a reliable way to find consistent bindings for holes in binary terms.

Key terms: occurs check, bound hole, substitution, alias, Substitute, free hole, unification, first-order binary-term unification, symbol

10.2 The performance of binary term unification

This section analyzes why binary-term unification can have exponential worst-case cost, outlines optimizations, and explains why Robinson’s algorithm remains practically useful.

• Exponential substitution blowup: Explain how a tower-like binary-term unification problem causes substitution to build a full binary tree whose size doubles for each additional hole. State that with n holes, Substitute can allocate O(2^n) objects, requiring exponential space and therefore exponential time.
  Why it matters: A unifier can appear fast on small examples while a substitution expands into an unexpectedly enormous term.
• Unification performance costs: Describe the other expensive operations in the binary-term unifier: structural equality may inspect every subterm, occurs checks and hole searches traverse terms, and repeated occurs checks can search immutable terms for the same hole more than once. Explain that recursion may also process many bound-hole terms with large subterms.
  Why it matters: Recognizing all of the costs prevents attributing unification slowdowns only to the final substitution.
• Practical optimization choices: Explain the proposed performance improvements: memoized factory functions can deduplicate immutable symbols, constants, and terms so equality can use reference equality and repeated structures share storage; immutable dictionaries can make substitution-taking functions eligible for memoization. State that optimizations can reduce the worst case to O(n^3), while more complex preprocessed algorithms can be linear, yet Robinson’s algorithm is commonly preferred because typical real-world problems are fast enough and the simplest acceptable algorithm is favored.
  Why it matters: Algorithm selection should balance worst-case complexity against implementation complexity and the workloads that actually occur.

Key terms: Substitute, substitution, bound hole, binary term, O(2^n), exponential space, structural equality, occurs check, immutable terms, memoized factory functions

10.3 Type inference and logic programming

This section shows how unification solves type-inference constraints and, combined with backtracking, answers logic-programming queries.

• Type inference as unification: Explain how a type-inference problem can be encoded as a unification problem, with generic parameters and omitted types represented as holes and type constructors represented as terms. Describe that unification finds substitutions for those holes that make the method declaration, call arguments, and result type agree.
  Why it matters: This lets one unification algorithm infer related types rather than requiring a separate solver for each typing situation.
• Logic queries through backtracking: Describe how a database of facts, a rule with a condition and consequence, and a query containing a hole can be solved by unification plus backtracking. Trace how matching a query against a rule creates subproblems, and how alternative fact matches are tried to find possible bindings.
  Why it matters: Combining unification with backtracking turns symbolic facts and rules into a way to automatically search for logical conclusions.
• First-order logic applicability: State that first-order unification can solve problems expressed in first-order logic, using symbols, holes, constants, and logical relationships such as and, or, not, universal quantification, and if-then. Explain why this makes unification useful beyond type systems, including logic programming.
  Why it matters: Recognizing a problem as a first-order logic problem can reveal that unification is an appropriate solver.

Key terms: unification, type inference, generic type parameters, holes, substitution, List, backtracking search, facts, rules, query

10.4 Anti-unifying binary terms

This section introduces anti-unification as finding the most specific binary term pattern shared by two unequal terms, using holes for their differences.

• Anti-unification direction: Explain how anti-unification differs from unification: rather than filling holes to make unequal terms equal, it finds what unequal terms have in common and replaces differences with holes.
  Why it matters: This reversal of perspective is the foundation for understanding anti-unification algorithms.
• Shared structural constraints: Describe the common structure preserved when anti-unifying the example terms: a top-level multiplication, a right-hand division by 5, and equal left operands for the multiplication and division. Trace how substituting X with Add(1,2) or 6 recreates the respective original term.
  Why it matters: A useful generalization must preserve relationships in the inputs, not merely permit each input to be reconstructed.
• Most specific generalization: Explain why Mult(X, Div(Y, Z)) is not the best anti-unification even though substitutions can recreate both inputs: it loses the shared constant 5 and the equality relationship between the two left operands. State that the goal is the most specific generalization, and that holes stand for terms rather than symbol names.
  Why it matters: Reconstructing both inputs is insufficient; the result must retain every structural similarity that the inputs actually share.

Key terms: unification, anti-unification, holes, substitution, binary term, structural similarities, Mult, Div, most specific generalization, terms

10.5 The first-order binary-term anti-unification algorithm

This section derives and implements a recursive first-order anti-unification algorithm for binary terms, including fresh-hole generation and its performance trade-offs.

• Recursive anti-unification construction: Explain how the recursive algorithm constructs a least-general binary term and two substitutions from two input terms. Describe the cases for equal terms, matching symbol names, and incompatible terms, including how the substitutions reconstruct each original term.
  Why it matters: This is the central method for preserving shared structure while replacing differences with variables.
• Repeated-pair hole reuse: Describe why the algorithm checks existing substitutions before creating a hole, and explain that the same pair of differing subterms must reuse its existing hole. Apply this to the example where Add(1,2) and 6 occur twice.
  Why it matters: Reusing a hole captures repeated differences consistently, producing the best possible anti-unification rather than an unnecessarily general one.
• Fresh hole generation: Describe how the hole factory generates unique unused holes and why it first avoids holes already present in either input term. State that it progresses through names such as A through Z and then A1, B1, and so on, skipping names already in use.
  Why it matters: Fresh holes prevent the algorithm from accidentally treating a newly introduced placeholder as an existing hole in an input term.
• Algorithm complexity improvements: State the baseline space and time costs of the algorithm and explain the two proposed memoization improvements. Explain that structural equality and scanning prior substitutions can each cost O(n) per recursive call, giving O(n²) time, whereas memoized BinTerm factories and memoizing AU can reduce the total cost to O(n).
  Why it matters: The performance analysis identifies why a compact recursive algorithm can become slow on large terms and how sharing and memoization remove that cost.

Key terms: anti-unification, binary terms, result, sub1, sub2, substitutions, reuse, hole, substitution dictionary, previous recursive step

10.6 Clone detection and fix deduction

This section shows how anti-unification can detect code clones and learn recurring bug-fix patterns that can be instantiated to suggest fixes for new code.

• Anti-unification clone detection: Explain how method bodies can be parsed into trees, treated as terms, and anti-unified in pairs to detect code clones. State that the non-hole portions of the anti-unification are the shared structure, and that extensive shared structure suggests the methods are clones.
  Why it matters: This turns a term algorithm into a way to find duplicated code and repeated programming patterns in a real codebase.
• Clone detection value: Describe why detecting clones and common code patterns is useful: duplicated methods can spread bugs and maintenance work, while recurring structures can reveal refactoring opportunities. State that structural clone detection can still find copied work when formatting or identifier names have changed.
  Why it matters: Finding related code helps teams apply needed changes consistently and identify abstractions worth making explicit.
• Bug-fix pattern deduction: Describe how historical bug fixes can be represented as Change terms whose children are the before-code and after-code parses, then anti-unified to derive a generalized fix pattern. Explain that repeatedly anti-unifying many changes exposes common patterns, which can be ranked by frequency.
  Why it matters: A repository of past changes can become evidence for common, reusable ways to repair particular defect types.
• Pattern-based fix suggestion: Explain how a deduced fix pattern can suggest a repair for new buggy code: unify the pattern's before term with the buggy code, use the resulting substitution to instantiate the after pattern, and offer that instantiated code as a potential fix. Illustrate that matching B.A() to frog.ribbit() binds B to frog and A to ribbit, producing the corresponding null-checking fix.
  Why it matters: This rigorously transfers a learned repair pattern to novel code without requiring the tool to have seen that exact call before.

Key terms: anti-unification, parse trees, terms, holes, clone detection, code smell, clones, refactoring, plagiarism, Change term

10.7 Summary

This summary contrasts unification and anti-unification of binary terms, their algorithms and performance, and their uses in logic, type inference, and program analysis.