From 469ed26e90ef96e44764938c7cdddfb271f272c4 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Fri, 3 Apr 2026 14:21:40 +0800 Subject: feat: implement substitution logic and unify/applySubstitution functions for term resolution --- CMakeLists.txt | 1 + include/atp/infer/substitution.h | 42 +++-- include/atp/infer/unification.h | 4 + src/infer/substitution.cc | 119 ++++++++++++++ src/infer/unification.cc | 68 ++++++++ tests/test_unification.cc | 337 +++++++++++++++++++++++++++++++++++++++ 6 files changed, 561 insertions(+), 10 deletions(-) create mode 100644 src/infer/substitution.cc diff --git a/CMakeLists.txt b/CMakeLists.txt index 2cf69db..edeb6b7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -72,6 +72,7 @@ set(ATP_SOURCES src/core/term_bank.cc src/core/clause_store.cc src/normalize/clausifier.cc + src/infer/substitution.cc src/infer/unification.cc src/infer/resolution.cc src/index/discrim_tree.cc diff --git a/include/atp/infer/substitution.h b/include/atp/infer/substitution.h index f9f562a..671f6d7 100644 --- a/include/atp/infer/substitution.h +++ b/include/atp/infer/substitution.h @@ -16,39 +16,61 @@ * along with this program. If not, see . */ - #pragma once /// @file substitution.h /// @brief Variable binding map: Var -> Term. +/// +/// Short-lived object created during unification, applied to build resolvents, +/// then discarded. Never stored long-term. +#include "atp/core/term_bank.h" #include "atp/core/types.h" -#include +#include namespace atp { -/// A substitution is a mapping from variable TermIds to their bound TermIds. -/// Designed as a short-lived, stack-allocated object during unification. +/// A substitution σ maps variable TermIds to their bound TermIds. +/// +/// Example: σ = { X → f(a), Y → Z } +/// lookup(X) = f(a) (direct binding) +/// resolve(X) = f(a) (same — f(a) is not a variable) +/// resolve(Y) = Z (if Z is unbound, stops at Z) +/// resolve(Y) = f(b) (if Z → f(b) also in σ, walks the chain) class Substitution { public: Substitution() = default; - /// Bind a variable to a term. Returns false if already bound to something different. + /// Bind a variable to a term. Returns false if already bound to a different term. bool bind(TermId var, TermId term); - /// Look up what a variable is bound to. Returns kInvalidId if unbound. + /// Look up what a variable is directly bound to. Returns kInvalidId if unbound. [[nodiscard]] TermId lookup(TermId var) const; - /// Walk the binding chain to the final bound value. - [[nodiscard]] TermId resolve(TermId id) const; + /// Walk the binding chain to the final value. + /// If var → Y → f(a), returns f(a). + /// Requires TermBank to check whether intermediate values are variables. + [[nodiscard]] TermId resolve(TermId id, const TermBank& bank) const; + + /// Apply this substitution to a term recursively, creating new terms in the bank. + /// Free (unbound) variables are left as-is. + [[nodiscard]] TermId apply(TermId term, TermBank& bank) const; + + /// Check if a variable occurs anywhere inside a term (for occurs check). + [[nodiscard]] bool occursIn(TermId var, TermId term, const TermBank& bank) const; /// Clear all bindings. void clear(); + /// Number of bindings. + [[nodiscard]] size_t size() const { return bindings_.size(); } + + /// Check if empty. + [[nodiscard]] bool empty() const { return bindings_.empty(); } + private: - // TODO: Phase 2 implementation - std::vector> bindings_; + std::unordered_map bindings_; }; } // namespace atp diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h index 7d91aaf..f2ea180 100644 --- a/include/atp/infer/unification.h +++ b/include/atp/infer/unification.h @@ -37,4 +37,8 @@ struct UnificationConfig { bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, const UnificationConfig& config = {}); +/// Apply a substitution to a term recursively, creating new terms in the bank. +/// Free (unbound) variables are left unchanged. +TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank); + } // namespace atp diff --git a/src/infer/substitution.cc b/src/infer/substitution.cc new file mode 100644 index 0000000..c570676 --- /dev/null +++ b/src/infer/substitution.cc @@ -0,0 +1,119 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + */ + +#include "atp/infer/substitution.h" +#include "atp/core/term.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +namespace atp { + +bool Substitution::bind(TermId var, TermId term) { + auto [it, inserted] = bindings_.emplace(var, term); + if (!inserted) { + // Already bound — succeed only if bound to the same term + return it->second == term; + } + return true; +} + +TermId Substitution::lookup(TermId var) const { + auto it = bindings_.find(var); + if (it != bindings_.end()) { + return it->second; + } + return kInvalidId; +} + +TermId Substitution::resolve(TermId id, const TermBank& bank) const { + // Walk the chain: X → Y → Z → f(a) + // Stop when we hit a non-variable or an unbound variable. + while (bank.isVariable(id)) { + auto it = bindings_.find(id); + if (it == bindings_.end()) { + break; // Unbound variable — stop here + } + id = it->second; + } + return id; +} + +TermId Substitution::apply(TermId term, TermBank& bank) const { + // First, resolve through variable chain + term = resolve(term, bank); + + if (bank.isVariable(term)) { + // Free variable (unbound) — leave as-is + return term; + } + + // IMPORTANT: Copy symbol_id and args BEFORE recursing. + // Recursive apply() calls may trigger bank.makeTerm() → realloc → dangling ref. + const Term& t = bank.getTerm(term); + SymbolId sym = t.symbol_id; + std::vector old_args(t.args); // copy! + + if (old_args.empty()) { + // Constant or 0-arity — no substitution needed + return term; + } + + // Recursively apply to all arguments + std::vector new_args; + new_args.reserve(old_args.size()); + bool changed = false; + for (TermId arg : old_args) { + TermId new_arg = apply(arg, bank); + new_args.push_back(new_arg); + if (new_arg != arg) { + changed = true; + } + } + + if (!changed) { + return term; + } + + return bank.makeTerm(sym, new_args); +} + +bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const { + term = resolve(term, bank); + + if (var == term) { + return true; + } + + if (bank.isVariable(term)) { + return false; // Different unbound variable + } + + const Term& t = bank.getTerm(term); + for (TermId arg : t.args) { + if (occursIn(var, arg, bank)) { + return true; + } + } + return false; +} + +void Substitution::clear() { + bindings_.clear(); +} + +} // namespace atp \ No newline at end of file diff --git a/src/infer/unification.cc b/src/infer/unification.cc index b62ffd0..be8a025 100644 --- a/src/infer/unification.cc +++ b/src/infer/unification.cc @@ -17,3 +17,71 @@ */ +#include "atp/infer/unification.h" +#include "atp/core/types.h" +#include "atp/infer/substitution.h" + +namespace atp { + + bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, + const UnificationConfig& config) { + t1 = subst.resolve(t1, bank); + t2 = subst.resolve(t2, bank); + + if (t1 == t2) { + return true; + } + + if (bank.isVariable(t1)) { + if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) { + return false; + } + subst.bind(t1, t2); + return true; + } + + if (bank.isVariable(t2)) { + if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) { + return false; + } + subst.bind(t2, t1); + return true; + } + + const Term& term1 = bank.getTerm(t1); + const Term& term2 = bank.getTerm(t2); + + if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) { + return false; + } + + for (size_t i = 0; i < term1.arity(); ++i) { + if (!unify(bank, term1.args[i], term2.args[i], subst, config)) { + return false; + } + } + + return true; + } + + TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) { + term = subst.resolve(term, bank); + if (bank.isVariable(term)) { + return term; + } + + // IMPORTANT: Copy args and symbol_id BEFORE recursing. + // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs. + const Term& t = bank.getTerm(term); + SymbolId sym = t.symbol_id; + std::vector old_args(t.args); // copy! + + std::vector new_args; + new_args.reserve(old_args.size()); + for (TermId arg : old_args) { + new_args.push_back(applySubstitution(subst, arg, bank)); + } + return bank.makeTerm(sym, new_args); + } + +} // namespace atp \ No newline at end of file diff --git a/tests/test_unification.cc b/tests/test_unification.cc index b62ffd0..3ee6f00 100644 --- a/tests/test_unification.cc +++ b/tests/test_unification.cc @@ -16,4 +16,341 @@ * along with this program. If not, see . */ +#include +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/infer/substitution.h" +#include "atp/infer/unification.h" + +namespace atp { +namespace { + +// ═══════════════════════════════════════════════════════════════════════════ +// Test Fixture +// ═══════════════════════════════════════════════════════════════════════════ + +class UnificationTest : public ::testing::Test { + protected: + SymbolTable symbols; + TermBank bank{symbols}; + + // Symbols + SymbolId sym_a{}, sym_b{}, sym_c{}; + SymbolId sym_f{}, sym_g{}, sym_h{}; + SymbolId sym_P{}; + SymbolId sym_X{}, sym_Y{}, sym_Z{}; + + // Terms (created in SetUp) + TermId a{}, b{}, c{}; + TermId X{}, Y{}, Z{}; + + void SetUp() override { + sym_a = symbols.intern("a", SymbolKind::kConstant); + sym_b = symbols.intern("b", SymbolKind::kConstant); + sym_c = symbols.intern("c", SymbolKind::kConstant); + sym_f = symbols.intern("f", SymbolKind::kFunction, 1); + sym_g = symbols.intern("g", SymbolKind::kFunction, 2); + sym_h = symbols.intern("h", SymbolKind::kFunction, 1); + sym_P = symbols.intern("P", SymbolKind::kPredicate, 2); + sym_X = symbols.intern("X", SymbolKind::kVariable); + sym_Y = symbols.intern("Y", SymbolKind::kVariable); + sym_Z = symbols.intern("Z", SymbolKind::kVariable); + + a = bank.makeTerm(sym_a, {}); + b = bank.makeTerm(sym_b, {}); + c = bank.makeTerm(sym_c, {}); + X = bank.makeVar(sym_X); + Y = bank.makeVar(sym_Y); + Z = bank.makeVar(sym_Z); + } + + // Helper: make f(arg) + TermId f(TermId arg) { return bank.makeTerm(sym_f, {{arg}}); } + // Helper: make g(arg1, arg2) + TermId g(TermId a1, TermId a2) { return bank.makeTerm(sym_g, {{a1, a2}}); } + // Helper: make h(arg) + TermId h(TermId arg) { return bank.makeTerm(sym_h, {{arg}}); } + // Helper: make P(arg1, arg2) + TermId P(TermId a1, TermId a2) { return bank.makeTerm(sym_P, {{a1, a2}}); } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// Substitution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, SubstBindAndLookup) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_EQ(subst.lookup(X), a); + EXPECT_EQ(subst.lookup(Y), kInvalidId); // unbound +} + +TEST_F(UnificationTest, SubstBindSameTermSucceeds) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_TRUE(subst.bind(X, a)); // same binding → OK +} + +TEST_F(UnificationTest, SubstBindDifferentTermFails) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_FALSE(subst.bind(X, b)); // different binding → fail +} + +TEST_F(UnificationTest, SubstResolveChain) { + // X → Y → a + Substitution subst; + subst.bind(X, Y); + subst.bind(Y, a); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, SubstResolveUnbound) { + Substitution subst; + EXPECT_EQ(subst.resolve(X, bank), X); // unbound → returns itself +} + +TEST_F(UnificationTest, SubstResolveNonVariable) { + Substitution subst; + EXPECT_EQ(subst.resolve(a, bank), a); // constant → returns itself +} + +TEST_F(UnificationTest, SubstApplySimple) { + // σ = {X → a} apply to f(X) → f(a) + Substitution subst; + subst.bind(X, a); + TermId fx = f(X); + TermId result = subst.apply(fx, bank); + TermId expected = f(a); + EXPECT_EQ(result, expected); +} + +TEST_F(UnificationTest, SubstApplyLeavesUnbound) { + // σ = {X → a} apply to g(X, Y) → g(a, Y) + Substitution subst; + subst.bind(X, a); + TermId gxy = g(X, Y); + TermId result = subst.apply(gxy, bank); + TermId expected = g(a, Y); + EXPECT_EQ(result, expected); +} + +TEST_F(UnificationTest, SubstApplyNested) { + // σ = {X → f(a)} apply to g(X, b) → g(f(a), b) + Substitution subst; + subst.bind(X, f(a)); + TermId result = subst.apply(g(X, b), bank); + EXPECT_EQ(result, g(f(a), b)); +} + +TEST_F(UnificationTest, SubstOccursIn) { + Substitution subst; + // X occurs in f(X) + EXPECT_TRUE(subst.occursIn(X, f(X), bank)); + // X occurs in g(a, f(X)) + EXPECT_TRUE(subst.occursIn(X, g(a, f(X)), bank)); + // X does NOT occur in f(a) + EXPECT_FALSE(subst.occursIn(X, f(a), bank)); + // X does NOT occur in Y (different variable) + EXPECT_FALSE(subst.occursIn(X, Y, bank)); +} + +TEST_F(UnificationTest, SubstClearAndSize) { + Substitution subst; + EXPECT_TRUE(subst.empty()); + subst.bind(X, a); + subst.bind(Y, b); + EXPECT_EQ(subst.size(), 2); + subst.clear(); + EXPECT_TRUE(subst.empty()); + EXPECT_EQ(subst.lookup(X), kInvalidId); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Unification Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, UnifyIdenticalConstants) { + Substitution subst; + EXPECT_TRUE(unify(bank, a, a, subst)); + EXPECT_TRUE(subst.empty()); +} + +TEST_F(UnificationTest, UnifyDifferentConstants) { + Substitution subst; + EXPECT_FALSE(unify(bank, a, b, subst)); +} + +TEST_F(UnificationTest, UnifyVarWithConstant) { + Substitution subst; + EXPECT_TRUE(unify(bank, X, a, subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyConstantWithVar) { + // Symmetric: unify(a, X) should also work + Substitution subst; + EXPECT_TRUE(unify(bank, a, X, subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyTwoVariables) { + Substitution subst; + EXPECT_TRUE(unify(bank, X, Y, subst)); + // One should be bound to the other + TermId rx = subst.resolve(X, bank); + TermId ry = subst.resolve(Y, bank); + EXPECT_EQ(rx, ry); +} + +TEST_F(UnificationTest, UnifyCompoundTerms) { + // f(X) =? f(a) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, f(X), f(a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyMultipleArgs) { + // g(X, Y) =? g(a, b) → {X → a, Y → b} + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, Y), g(a, b), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); + EXPECT_EQ(subst.resolve(Y, bank), b); +} + +TEST_F(UnificationTest, UnifyConflictingBindings) { + // g(X, X) =? g(a, b) → fails (X can't be both a and b) + Substitution subst; + EXPECT_FALSE(unify(bank, g(X, X), g(a, b), subst)); +} + +TEST_F(UnificationTest, UnifyConsistentRepeatedVar) { + // g(X, X) =? g(a, a) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, X), g(a, a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyDifferentHeadSymbols) { + // f(X) =? h(X) → fails + Substitution subst; + EXPECT_FALSE(unify(bank, f(X), h(X), subst)); +} + +TEST_F(UnificationTest, UnifyDifferentArity) { + // f(X) =? g(X, Y) → fails (arity 1 vs 2) + Substitution subst; + EXPECT_FALSE(unify(bank, f(X), g(X, Y), subst)); +} + +TEST_F(UnificationTest, UnifyNestedTerms) { + // f(g(X, a)) =? f(Y) → {Y → g(X, a)} + Substitution subst; + EXPECT_TRUE(unify(bank, f(g(X, a)), f(Y), subst)); + EXPECT_EQ(subst.resolve(Y, bank), g(X, a)); +} + +TEST_F(UnificationTest, UnifyVarWithCompound) { + // X =? f(a) → {X → f(a)} + Substitution subst; + EXPECT_TRUE(unify(bank, X, f(a), subst)); + EXPECT_EQ(subst.resolve(X, bank), f(a)); +} + +TEST_F(UnificationTest, UnifyDeepNesting) { + // f(f(f(X))) =? f(f(f(a))) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, f(f(f(X))), f(f(f(a))), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyChainedVariables) { + // g(X, Y) =? g(Y, a) → {X → Y, Y → a} effectively X → a + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, Y), g(Y, a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); + EXPECT_EQ(subst.resolve(Y, bank), a); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Occurs Check Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, OccursCheckBlocks) { + // X =? f(X) with occurs check → fails + Substitution subst; + UnificationConfig config{.enable_occurs_check = true}; + EXPECT_FALSE(unify(bank, X, f(X), subst, config)); +} + +TEST_F(UnificationTest, OccursCheckDisabledAllows) { + // X =? f(X) without occurs check → succeeds (unsound but fast) + Substitution subst; + UnificationConfig config{.enable_occurs_check = false}; + EXPECT_TRUE(unify(bank, X, f(X), subst, config)); +} + +TEST_F(UnificationTest, OccursCheckDeep) { + // X =? f(g(X, a)) with occurs check → fails + Substitution subst; + UnificationConfig config{.enable_occurs_check = true}; + EXPECT_FALSE(unify(bank, X, f(g(X, a)), subst, config)); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// applySubstitution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, ApplySubstitutionSimple) { + Substitution subst; + subst.bind(X, a); + EXPECT_EQ(applySubstitution(subst, f(X), bank), f(a)); +} + +TEST_F(UnificationTest, ApplySubstitutionNested) { + Substitution subst; + subst.bind(X, a); + subst.bind(Y, b); + EXPECT_EQ(applySubstitution(subst, g(f(X), Y), bank), g(f(a), b)); +} + +TEST_F(UnificationTest, ApplySubstitutionPreservesUnbound) { + Substitution subst; + subst.bind(X, a); + // Y is unbound → stays as Y + EXPECT_EQ(applySubstitution(subst, g(X, Y), bank), g(a, Y)); +} + +TEST_F(UnificationTest, ApplySubstitutionToConstant) { + Substitution subst; + subst.bind(X, a); + // Constant is unchanged + EXPECT_EQ(applySubstitution(subst, b, bank), b); +} + +TEST_F(UnificationTest, ApplySubstitutionChain) { + // σ = {X → Y, Y → a} apply to f(X) → f(a) + Substitution subst; + subst.bind(X, Y); + subst.bind(Y, a); + EXPECT_EQ(applySubstitution(subst, f(X), bank), f(a)); +} + +TEST_F(UnificationTest, UnifyThenApply) { + // Full round-trip: unify P(X, f(Y)) with P(a, f(b)), then apply + Substitution subst; + TermId lhs = P(X, f(Y)); + TermId rhs = P(a, f(b)); + ASSERT_TRUE(unify(bank, lhs, rhs, subst)); + + EXPECT_EQ(applySubstitution(subst, lhs, bank), P(a, f(b))); + EXPECT_EQ(applySubstitution(subst, rhs, bank), P(a, f(b))); + // Both sides should produce the same term after applying the MGU + EXPECT_EQ(applySubstitution(subst, lhs, bank), + applySubstitution(subst, rhs, bank)); +} + +} // namespace +} // namespace atp -- cgit v1.2.3