modification

n 1: the act of making something different (as e.g. the size of a

garment) [syn: {alteration}, {adjustment}]

2: a slightly modified copy; not an exact copy: "a modification

of last year's model"

3: the grammatical relation that exists when a word qualifies

the meaning of the phrase [syn: {qualifying}, {limiting}]

4: an event that occurs when something passes from one state or

phase to another: "the change was intended to increase

sales"; "this storm is certainly a change for the worse"

[syn: {change}, {alteration}]

unification

The generalisation of {pattern matching} that is

the {logic programming} equivalent of {instantiation} in

{logic}. When two {term}s are to be unified, they are

compared. If they are both constants then the result of

unification is success if they are equal else failure. If one

is a variable then it is bound to the other, which may be any

term (which satisfies an "{occurs check}"), and the

unification succeeds. If both terms are structures then each

pair of sub-terms is unified {recursive}ly and the unification

succeeds if all the sub-terms unify.

The result of unification is either failure or success with a

set of variable bindings, known as a "{unifier}". There may

be many such unifiers for any pair of terms but there will be

at most one "{most general unifier}", other unifiers simply

add extra bindings for sub-terms which are variables in the

original terms.

(1995-12-14)