# Tag Info

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
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
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 ...
• 11.8k

• 11.8k
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

### 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
Accepted

### Why this pattern matching fails in Agda?

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

### 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
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,107

### 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
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 ...
• 11.8k
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 ...
• 11.8k

### 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
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
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

### 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 ...
• 3,413
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
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 (...
• 11.8k
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 ...
• 2,148
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