5
votes
Accepted
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.♦
- 169k
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 (...
- 12.2k
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.♦
- 169k
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 ...
- 3,583
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 ...
- 937
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 ...
- 24.9k
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 \...
- 320
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 ...
- 111
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 ...
- 30.4k
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 ...
- 320
Only top scored, non community-wiki answers of a minimum length are eligible