# Tag Info

13

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 with specific properties) to a problem (a pair of terms). Term rewriting uses a notion called "pattern matching". What you probably meant is: what is the ...

9

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-variables or unification variables. As I explain a bit in this answer, the problem reduces to higher order unification, on which several people have written ...

8

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 follows: A type checking system can be turned into a type inference system by making the rules linear and adding constraints. I'll use the application rule as an ...

8

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 syntactically identical. However, you can consider other base equivalence relations that are coarser than syntactic equality. For example, there's associative, ...

7

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 $\sigma$ of the terms such that any other unifier can be written as $\sigma\circ\tau$ for some substitution $\tau$: in other words any other unifier can be ...

5

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 $\approx$-suspension at which point you'll not be able to satisfy the premise as $\nabla$ is empty but the disagreement set is $\{a,b\}$. There are no other ...

5

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 repository for your textbook. The code in Lisp, for example, is here. A helpful note to remember when looking at first-order unification algorithms is that function ...

4

I found out that such a thing is called anti-unification. This problem was addressed by Plotkin and Reynolds. Here is a brief overview.

4

If you model the lambda terms via deBruijn indexes and the meta variables via Prolog variables, you could build a Prolog constraint solver. Here is an example that works already quite well, the basic constraints that were used are as follows: % shift(+Indexed, +Nat, +Nat, -Indexed) % subst(+Indexed, +Nat, +Indexed, -Indexed) % reduce(+Indexed, +Indexed, -...

4

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: this program is far from being pedagogically written. I am thinking in particular of the presentation of the function UNIFY-VAR which is analyzed below. ...

4

First, let's desugar the withs. First definition: wa''-aux : ∀ m n -> n + m ≡ m + n -> wa (m + n) ≡ wa (n + m) wa''-aux m n refl = ? -- cannot unify n + m with m + n wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m) wa'' m n = wa''-aux m n (comm n m) Second definition: wa''-aux : ∀ m n w -> w ≡ m + n -> wa (m + n) ≡ wa w wa''-aux m n .(m + n) refl ...

3

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 equations to unify them separately. That is, you can turn $\mathtt{p}(X,X) = \mathtt{q}(\mathtt{a},\mathtt{b})$ into $\mathtt{p}(X,Y) = \mathtt{q}(\mathtt{a},\... 3 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 details of the algorithm. In particular the transitions will be$\approx?$-abstraction-2 and$\approx?$-variable followed by$\#?$-abstraction-2 and$\#?$-... 3 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 are standard algorithms for solving this. However, this doesn't handle equivalence relations like commutativity or associativity. E-unification might be what ... 3 The variables called x in the two sentences are not related. We can rename them to make it clear: ~Loves(x1,F(x1)) v Loves(G(x1),x1) ~Animal(x2) v Loves(Jack,x2) Now when matching ~Loves(x1,F(x1)) and Loves(Jack,x2), you can see you'll get Jack/x1, F(Jack)/x2 and the final result as in the book. 3 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 infinite set of inputs to an infinite set of outputs. You've only given a finite set of inputs, so there's an infinite number of problems which could be described by ... 3 In rewrite theory, you often want confluence of your system: if $$u_1\leftarrow t\rightarrow u_2$$ Then there is some term$v$such that $$u_1\rightarrow v\leftarrow u_2$$ It is possible to tell whether a set of rewrite rules is confluent by examining the critical pairs: pairs of rules$t_1\rightarrow u_1,t_2\rightarrow u_2$and an instance$\theta$such ... 2 "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) from that. Now "Everybody who has a house pays utilities" is just$\forall x. \text{Houseower}(x) \Rightarrow \text{PaysUtilities}(x)$because there is no ... 2 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 general. However, if you are willing to save some extra information on the side while you are solving$D$, then yes there are methods to do what you want -- ... 2 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 (typically) handled by introducing a unification variable. To perform existential introduction, you need to have a term$t$. The rule looks like: $$\dfrac{\Gamma\vdash ... 2 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 symbolic expression -- it is a syntactic object that is not intended to be interpreted in the way you are interpreting it. If you like, you can think of it as ... 2 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 ability to substitute "each variable once, all at once" like this is important for the correctness of the definition. So substitution is defined so that there is ... 1 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 \sigma \iff \exists_{i, j}: s_i \sigma = t_j \sigma, $$i.e,$$\mathcal{U}_{C}(\{ s \approx_{C}^{?} t \}) = \bigcup\limits_{1 \leq i \leq m \\ 1 \leq j \leq n} \... 1 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. 1 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 arrays as terms and multidimensional arrays as arrays of arrays. You'll also introduce a new term symbol that doesn't occur in$\mathscr{L}$. So for example, if you ... 1 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 has 0 or 1 children. These can handle union, concatenation, and recursion (star), and you can solve for variables like you describe. They're decidable, even ... 1 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 introduces "syntactic shorthand": when they write something like$a \to b \to c$, it should be understand that they actually mean$(a \to (b \to c))$. The ... 1 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 saying is exactly occur check. 1 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 second step, you inferred that$X=p(Z)$. In the third step, you inferred that$X=Z$. It follows that you can infer$Z=p(Z)$. So we know$X=Z=p(Z)$and$w=Y$. ... 1 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 depending on whatever universally quantified variables are in scope. Then your initial formula would be the skolemization of$\forall x\exists y:(has(x,y)\...

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