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-...
cody's user avatar
  • 8,204
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 ...
Derek Elkins left SE's user avatar
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 $...
David Richerby's user avatar
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 ...
cody's user avatar
  • 8,204
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 $\...
Derek Elkins left SE's user avatar
4 votes
Accepted

Why this pattern matching fails in Agda?

First, let's desugar the withs. First definition: ...
mudri's user avatar
  • 156
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: ...
Alexey Romanov's user avatar
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 ...
Derek Elkins left SE's user avatar
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 ...
Derek Elkins left SE's user avatar
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 ...
D.W.'s user avatar
  • 159k
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 ...
D.W.'s user avatar
  • 159k
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 ...
Aaron Rotenberg's user avatar
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 ...
ShyPerson's user avatar
  • 925
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 ...
Pseudonym's user avatar
  • 22.1k
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 (...
Derek Elkins left SE's user avatar
1 vote
Accepted

How can I compute the most general unifier for these two expressions?

There seems to be a small confusion with the notation. Notice that $\sigma = \{z = a, \ y = h(b), \ x = h(b) \}$ and $\sigma' = \{z = a, \ y = h(b), \ x = y \}$ are the same unifier, written in a ...
Gabriel F. Silva's user avatar
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 \...
Gabriel F. Silva's user avatar
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.
Jake's user avatar
  • 3,810
1 vote

Inference and Unification algorithm provided to a Unification graph of two expressions

Yes, your solution and process are correct, assuming that alpha and beta are variables. It might help to rewrite your terms in a ...
William Lewis's user avatar
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 ...
Joey Eremondi's user avatar
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 ...
alim's user avatar
  • 994
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 ...
D.W.'s user avatar
  • 159k

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