请输入您要查询的字词:

 

单词 unification
释义
unification

Computer
  • An operation on well-formed formulas, namely that of finding a most general common instance. The formulas can be terms or atomic formulas (see predicate calculus). A common instance of two formulas A and B is a formula that is an instance of both of them, i.e. that can be obtained from either by some consistent substitution of terms for variables. As an example let A and B be the following:

    A=p(f(u),v)B=p(w,g(x))
    Let u, v, w, x, y, z be variables, and c, d constants. Consider the substitution that replaces u, v, w, x respectively by the terms y, g(z), f(y), z. This substitution, when applied to A and B, transforms them both into the same formula I1, where
    I1=P(f(y),g(z))
    Hence the above is a common instance of A and B. It is however only one of infinitely many: other common instances of A and B include
    I2=P(f(z),g(y))I3=P(f(y),g(y))I4=P(f(f(y)),g(g(z)))I5=P(f(c),g(d))
    Note that I2, I3, I4, I5 are themselves instances of I1. In fact any common instance of A and B is an instance of I1 and therefore I1 is called a most general common instance of A and B. Of the formulas above, the only other one that is a most general common instance is I2. I5 would also be one if c and d were variables rather than constants; indeed the y and z of I1 could be any two distinct variables. In some cases A and B have no common instance; two examples of this are
    A=P(f(u),ν)B=P(g(w),x)
    and
    A=P(f(u),u)B=P(w,f(w))
    If A and B do have a common instance however, they must have a most general one. There are algorithms (the original one being Robinson’s, 1965) for deciding whether a given A and B have a common instance, and if so finding a most general one. Robinson’s motivation for describing unification was its role in resolution theorem proving. Resolution was at one time associated with ‘general problem-solving’ techniques in artificial intelligence. More recently it has provided the conceptual basis for the logic programming language Prolog. Another use of unification is in compile-time type-inference, especially for polymorphic types.


随便看

 

科学参考收录了60776条科技类词条,基本涵盖了常见科技类参考文献及英语词汇的翻译,是科学学习和研究的有利工具。

 

Copyright © 2000-2023 Sciref.net All Rights Reserved
京ICP备2021023879号 更新时间:2024/12/26 0:58:38