Quantifier Unification Link to heading

For now our little theorem prover can unify only atomic formulas (predicates). When we encounter quantifiers everything gets more interesting. Let’s look at a specific example that Paulson discusses in his paper.

Why can’t we unify \(\exists x.P(x)\) with \(\exists x.P(?a)\) by simply setting \(?a\) to \(x\)?
It seems intuitive at first glance, but it’s a trap.

Think about what these two formulas actually mean:

  • \(\exists x.P(x)\) – means “there exists some \(x\) for which \(P(x)\) is true”
  • \(\exists x.P(?a)\) – means “there exists some \(x\), and \(P\) holds for some specific value \(?a\)”

These are fundamentally different logical statements:

  1. \(\exists x.P(x)\) – “exists an \(x\) such that \(P(x)\)”
  2. \(\forall x.P(?a)\) – “exists an \(x\), and P holds for \(?a\)”

What if we simply map \(?a\) to \(x\):
\(?a := x\)
Well, then we get \(\exists x.P(x)\) but we’ve just created a scope violation.
We’re trying to make \(?a\) reference a variable that only exists inside the quantifier.
It’s like trying to reference a variable outside its scope in programming:

let x = 1 in
let f = fun y -> x + y in  (* x refers to x = 1 *)
let x = 2 in
f 0                        (* still returns 1, not 2 *)

Paulson made an interesting choice in Folderol – it only unifies atomic formulas. No quantifiers involved. At first, this might seem limiting, but if you’re building an educational system like folderol, sticking to atomic formulas might be the wise choice.

Occurs check Link to heading

Do we really need an occurs check?
Some systems (like Prolog) skip the occurs check to go faster, but that can lead to problems – like circular data structures or getting stuck in an endless loop.

I don’t know (and I don’t really care) if modern Prolog skips the occurs check in 2025,
but that’s what Paulson wrote in 1990.

Folderol uses a naive unification algorithm. While it might require exponential time in some edge cases, it usually performs well enough. Paulson mentions that there is a more sophisticated approach by Martelli and Montanari (1982) which avoids the occurs check through equation sorting, but it’s mainly of theoretical interest (I haven’t read it and probably never will lol).

Instantiation of Terms Link to heading

In Paulson’s Folderol, substitutions during unification aren’t applied immediately. Instead, they are delayed because it is simply more efficient. Delaying substitutions avoids repeatedly rewriting large terms. Instead, we just pass around the environment from one unification to another, accumulating substitutions as we go.

For simplicity and efficiency reasons, in folderol we use environments only during unification. After unification is complete, we should “instantiate” the entire proof. This means we should goe through the proof and apply all the substitutions recorded in the environment.

Paulson introduces a recursive function, inst_term, that performs the meta-variable substitution:

let rec inst_term env = function
  | Term.Function (name, args) ->
      let args' = List.map ~f:(inst_term env) args in
      Term.Function (name, args')
  | Term.Param (name, var_names) ->
      let vars =
        var_names
        |> List.map ~f:(fun v -> inst_term env (Term.Var v))
        |> List.fold ~init:[] ~f:Term.variable_names
      in
      Term.Param (name, vars)
  | Term.Var name -> (
      match find env name with
      | Some term -> inst_term env term
      | None -> Term.Var name)
  | term -> term

Same with formulas:

let rec inst_formula env = function
  | Formula.Pred (name, terms) ->
      let terms' = List.map ~f:(inst_term env) terms in
      Formula.Pred (name, terms')
  | Formula.Conn (conn, subformulas) ->
      let subformulas' = List.map ~f:(inst_formula env) subformulas in
      Formula.Conn (conn, subformulas')
  | Formula.Quant (quant, var_name, body) ->
      let body' = inst_formula env body in
      Formula.Quant (quant, var_name, body')