Logic Programming

## Relations, not functions The habit this question breaks is the function habit. A function has a fixed arrow: arguments in, result out, and asking it to run backwards is a different function you would have to write. A logic rule has no arrow. `partOf(Whole, Part)` is a **relation** - a set of pairs that satisfy it - and a query simply asks which members of that set match the shape you supplied. That is why a single definition answers what look like two different questions. They are the same question with different positions left open. ## What unification actually does **Unification** is the matching operation at the heart of the engine. Given two terms, it finds the most general substitution that makes them identical, or fails. Four cases cover it: 1. **A variable against a constant** - the variable is bound to that constant for the rest of the branch. 2. **Two constants** - they match if identical, otherwise the match fails and the engine backtracks. 3. **Two variables** - they are aliased, so binding either one later binds both. 4. **Two compound terms** - the names and argument counts must agree, then the arguments are unified pairwise, recursively. Two properties distinguish this from assignment, and they are what the follow-up usually probes. Unification is **symmetric**: it does not care which side of the match the variable sits on, which is precisely why the relation has no input side. And a binding is **provisional**: it lives only on the current search branch and is undone when the engine backtracks past the point that made it. Assignment is directional and destructive; unification is symmetric and reversible. ## One rule, both directions Take containment facts plus the two-clause transitive definition. Query with the first position bound and the second open, and the engine walks forward from the assembly, collecting what is inside it. Query with the second position bound and the first open, and exactly the same clauses walk the facts the other way, collecting the wholes. The clause text does not know which of its positions was supplied. | goal shape | what is bound | what the engine does | |---|---|---| | both positions constants | everything | a check: succeeds or fails, no search for values | | first bound, second open | the whole | enumerates the parts inside it | | first open, second bound | the part | enumerates the wholes containing it | | both positions open | nothing | enumerates every pair in the relation | That last row is worth naming in an interview, because it is the one that surprises people: a fully open goal is a legitimate query that streams the entire relation, and a definition that is well behaved in the other three shapes can be unusably expensive in this one. ## Where directionality comes back The two-way property is a property of **pure** relational goals, and real rules often contain goals that are not pure in this sense: - An arithmetic evaluation needs its operands known before it can produce a number, so the arguments feeding it must be bound by earlier goals. - A negated goal asks whether something is underivable, which is only a meaningful question once its subject is known. - A goal that reaches outside the knowledge base - reading, printing, calling something - has a direction by nature. Engines describe this as a clause's **modes**: which argument patterns it supports. A clause with a mode restriction is not broken; it is simply a relation you may only query one way, and calling it the other way either fails, errors, or - worst - quietly gives an answer that is not the one you meant. Part of reading someone else's logic program is working out which of its relations are genuinely two-way and which are functions in relational clothing. ## Why the mechanism outlives the paradigm Unification is not confined to programs written in a resolution-based logic language. The same operation - match two structures, bind the open positions on either side, fail on a genuine conflict - is the engine of **Hindley-Milner type inference**, which is why a compiler can work out a type you never wrote from the way a value is used, in either direction. Recognising unification when you meet it elsewhere is most of the practical value of knowing this paradigm at all. Its one-way cousin, pattern matching, binds variables on one side only: the match either fits the given value or does not, and the value is never constrained to fit the pattern.