15 votes
Accepted

Term Rewriting vs Unification

Term rewriting is a rewriting formalism. Starting with a term we rewrite the term according to the term rewriting rules until a normal form is found. Unification is finding a solution (substitution ...
  • 1,100
9 votes
Accepted

Is there a general algorithm to fill holes in terms of the Calculus of Constructions?

There is certainly a lot of research into this problem! It often goes by the name of elaboration. It is an undecidable problem in general, as you may have guessed. The "holes" are often called meta-...
  • 7,754
8 votes
Accepted

why nominal unification is a first-order unification?

Most experience people have with unification (if any) is usually unification modulo syntactic equality: two terms unify if there is a substitution for unification variables that makes the terms ...
7 votes

What is a unifier?

A unifier of a set of terms is just any substitution that, when applied to each of the terms, makes them all equal. There's also the concept of a "most general unifier" (MGU), which is a unifier $...
7 votes
Accepted

Generating constraints to solve dependently-typed metavariables?

There's a nice idiom, which is explained more in chapter 22 of Types and Programming Languages (it's used for polymorphism rather than dependent types, but the idea is the same). The idiom is as ...
  • 7,754
5 votes
Accepted

"not provable", what does this to do with unification?

They mean you can't use the rules in Figure 2 defining $\approx$ (and $\#$) to derive $\emptyset\vdash a.\!X\approx b.\!X$. If you attempt to do it you'll use $\approx$-abstraction-2 followed by $\...
5 votes
Accepted

Can someone clarify this unification algorithm?

First, unification algorithms are tricky. Studying other textbooks will help. Second, things will probably get clearer if you look at actual code implementations. Have a look at the online code ...
  • 816
4 votes

Can someone clarify this unification algorithm?

This algorithm presentation is indeed pedagogically unclear. I will not repeat here the previous contributions. However, I believe some points need clarification. Sorry if some of it is a bit subtle: ...
  • 19.2k
4 votes
Accepted

Why this pattern matching fails in Agda?

First, let's desugar the withs. First definition: ...
  • 156
3 votes

E-Unification: “Goal seeking” pattern matching between directed trees

This is called unification. There is a one-to-one correspondence between terms and trees; the tree is the parse tree of a corresponding term. It sounds like you want the most general unifier. There ...
  • 144k
3 votes
Accepted

How can unifying 2 sentences in first-order logic result in a variable becoming 2 different things?

The variables called x in the two sentences are not related. We can rename them to make it clear: ...
3 votes

Can high-order unification be applied to programming by example?

It's incredibly unlikely that a complete sorting algorithm that works for ANY input would be deduced from just 3 inputs. In particular, there's a problem: sorting is a problem that matches an ...
  • 29.2k
3 votes
Accepted

Are these examples of unification problems?

Yes, the variables can occur more than once in a term. Either way you end up with a system of equations. For plain unification, you can always have the unification variables be distinct and then add ...
3 votes
Accepted

is this an example of nominal unification?

Sure, these unify under nominal unification. You get a unifier like $X = (b\ a)\bullet\lambda c.c$ which simplifies to $X = \lambda c.c$. Figures 1 and 3 of Nominal Unification describe the relevant ...
2 votes

Skolemization with multiple arguments -- how to unify

"Everyone has a heart" gets first encoded first as $\forall x. \text{Person}(x) \Rightarrow \exists y. \text{Hart}(y) \wedge \text{Has}(x,y)$. Then you get the Skolemization (that you found in RN) ...
  • 1,230
2 votes
Accepted

Unification --- removing equations and updating the solution

If all you have is the solution to these equations (the most general unifier for $D$), I don't know of any good algorithm for your problem that will be better than "compute the answer from scratch" in ...
  • 144k
2 votes
Accepted

Injectivity not required for unification algorithms?

Here $f$ is not a mathematical function. Rather, it is a function symbol. Don't think of $f(a,b)$ as the result of evaluating the function at parameters $a,b$. Rather, think of it as a term in a ...
  • 144k
2 votes

Why does the substitution {x/f(y), y/z} work this way?

Because that's not how substitution is defined. Seriously, there isn't much more to it than that. In some situations (such as applying a single step of a collection of rewriting rules), having the ...
2 votes
Accepted

What algorithms for unification over (multidimensional) array terms?

By way of context, I'll assume the goal is to do unification in classical first-order logic in a fixed language $\mathscr{L}$. (Formatting and other corrections welcome.) Briefly, you can treat ...
  • 816
2 votes
Accepted

Is Unification "an Implementation of Existential Quantification"?

It's possible you're paraphrasing me. I've certainly said things similar to that e.g. here. A more precise statement would be that existential quantification in logic programming languages is (...
2 votes
Accepted

Unification with a list of terms

Prolog compilers already do this. Imagine if you had the program: p(t1) :- body_1. p(t2) :- body_2. % ... p(tn) :- body_n. and you issued the query ...
  • 19.3k
1 vote
Accepted

Unifiers modulo commutativity in terms of syntactic unifiers and $\approx_{C}$-class

Note that for all $s, t \in T(\Sigma, V)$ we have: $$s \approx_{C} t \iff \exists_{i, j}: s_i = t_j \tag{*}$$ Using (*) for the terms $s \sigma$ and $t \sigma$ we obtain: $$s \sigma \approx_{C} t \...
1 vote
Accepted

Unification Algorithm without Occur Check

Say you tried to solve $f(A, g(A)) = f(B, B)$ after applying $A \to B$ you'd then have $f(A, g(A)) = f(A, A)$ and you'd have to unify $A = g(A)$ as a sub problem.
  • 3,738
1 vote

Is unification over regular expression equations doable?

I'm fairly sure this is possible. This seems to me as a special case of set constraints over tree languages: we can view regular expressions as a restriction of regular tree languages where each node ...
  • 29.2k
1 vote
Accepted

occur-check, does nominal unification has it?

Yes, it has the occur check. The ~variable transformation rule of nominal unification has a condition which states provided X does not occur in t what it is ...
  • 1,052
1 vote
Accepted

Comparison Procedure in Robinson's Unification Algorithm

It looks like the answer is that, to be syntactically valid, composite types must be fully parenthesized. In particular, $a \to b \to c$ is not a syntactically valid type (per definition 2A1). 2A1.1 ...
  • 144k
1 vote

Skolemization with multiple arguments -- how to unify

One issue with your example is that it doesn't say what you seem to think it says. Recall that skolemization is used to eliminate an existentially quantified variable by replacing it with a function ...
1 vote
Accepted

Unification Functions

Rather than thinking about this in terms of substitutions, you might find it useful to think about this in terms of equalities that you can infer. In the first step, you inferred that $w=Y$. In the ...
  • 144k

Only top scored, non community-wiki answers of a minimum length are eligible