Logic of Generality

From GM-RKB
(Redirected from Specialization)
Jump to navigation Jump to search


References

2018a

  • (Wikipedia, 2018) ⇒ https://en.wikipedia.org/wiki/Anti-unification_(computer_science)#Generalization,_specialization Retrieved:2018-4-8.
    • If a term [math]\displaystyle{ t }[/math] has an instance equivalent to a term [math]\displaystyle{ u }[/math], that is, if [math]\displaystyle{ t \sigma \equiv u }[/math] for some substitution [math]\displaystyle{ \sigma }[/math], then [math]\displaystyle{ t }[/math] is called more general than [math]\displaystyle{ u }[/math] , and [math]\displaystyle{ u }[/math] is called more special than, or subsumed by, [math]\displaystyle{ t }[/math] . For example, [math]\displaystyle{ x \oplus a }[/math] is more general than [math]\displaystyle{ a \oplus b }[/math] if [math]\displaystyle{ \oplus }[/math] is commutative, since then [math]\displaystyle{ (x \oplus a)\{x \mapsto b\} = b \oplus a \equiv a \oplus b }[/math] .

      If [math]\displaystyle{ \equiv }[/math] is literal (syntactic) identity of terms, a term may be both more general and more special than another one only if both terms differ just in their variable names, not in their syntactic structure; such terms are called variants, or renamings of each other.

      For example, [math]\displaystyle{ f(x_1,a,g(z_1),y_1) }[/math] is a variant of [math]\displaystyle{ f(x_2,a,g(z_2),y_2) }[/math] , since [math]\displaystyle{ f(x_1,a,g(z_1),y_1) \{ x_1 \mapsto x_2, y_1 \mapsto y_2, z_1 \mapsto z_2\} = f(x_2,a,g(z_2),y_2) }[/math] and [math]\displaystyle{ f(x_2,a,g(z_2),y_2) \{x_2 \mapsto x_1, y_2 \mapsto y_1, z_2 \mapsto z_1\} = f(x_1,a,g(z_1),y_1) }[/math] .

      However, [math]\displaystyle{ f(x_1,a,g(z_1),y_1) }[/math] is not a variant of [math]\displaystyle{ f(x_2,a,g(x_2),x_2) }[/math] , since no substitution can transform the latter term into the former one, although [math]\displaystyle{ \{x_1 \mapsto x_2, z_1 \mapsto x_2, y_1 \mapsto x_2 \} }[/math] achieves the reverse direction.

      The latter term is hence properly more special than the former one.

      A substitution [math]\displaystyle{ \sigma }[/math] is more special than, or subsumed by, a substitution [math]\displaystyle{ \tau }[/math] if [math]\displaystyle{ x \sigma }[/math] is more special than [math]\displaystyle{ x \tau }[/math] for each variable [math]\displaystyle{ x }[/math] .

      For example, [math]\displaystyle{ \{ x \mapsto f(u), y \mapsto f(f(u)) \} }[/math] is more special than [math]\displaystyle{ \{ x \mapsto z, y \mapsto f(z) \} }[/math] , since [math]\displaystyle{ f(u) }[/math] and [math]\displaystyle{ f(f(u)) }[/math] is more special than [math]\displaystyle{ z }[/math] and [math]\displaystyle{ f(z) }[/math] , respectively.

2017a

2017b