Tag Info

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-...
• 8,204
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 ...
• 12.1k

• 12.1k
Accepted

Why this pattern matching fails in Agda?

First, let's desugar the withs. First definition: ...
• 156
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,182
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 ...
• 12.1k
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 ...
• 12.1k

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

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,523
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 ...
• 925
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 ...
• 22.1k
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 (...
• 12.1k
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 ...
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,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 ...
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.8k
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 ...
• 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 ...
• 159k

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