12

SAT solvers solve the Boolean Satisfiability Problem. This is "the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE." An example is find an assignment of truth values to variables $a,b,c$ such that $(a \lor b \lor c)\land (\lnot a \lor \lnot b \lor c)\land (a \lor \lnot ...


11

Unification is such a fundamental concept in computer science that perhaps at time we even take it for granted. Any time we have a rule or equation or pattern and want to apply it to some data, unification is used to specialize the rule to the data. Or if we want to combine two general but overlapping rules, unification provides us with the most general ...


11

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

Proof assistants such as Isabelle/HOL work on a syntactical level on a logical calculus. Imagine you have the modus ponens rule (MP) $\qquad \displaystyle P\to Q, P\ \Longrightarrow\ Q$ and the proof goal $\qquad \displaystyle (a \lor b) \to (c \land d), a \lor b \ \overset{!}{\Longrightarrow} c\land d$ We humans see immediately that this follows with ...


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

I don't think it is important to inference engines. The unification algorithm is however very helpful for type inference. These are two very different kinds of inference. Type inference is important to computer science because types are important in the theory of programming languages, which is a significant part of computer science. Types are also close to ...


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


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)\...


1

You can use things like pair, proj ... as constants only. That works very well conceptually. Nevertheless, there are reasons why programming languages tend to use special syntactic forms for the like of products: Readability, e.g. ( M, N ) reads more natural than pair M N to some. For efficient reductions. It is possible to code the reductions for pairs up ...


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