markh@csd4.milw.wisc.edu (Mark William Hopkins) (12/28/88)
This is a followup to the previous article posted on this topic.
Underlying both unification algorithms discussed in that article is a
theory of syntatic patterns, which I will try to outline here.
Consider a specific grammar G:
S --> NP VP
NP --> D N
VP --> V NP
D --> 'the' | 'a'
N --> 'boy' | 'girl' | 'child'
V --> 'saw' | 'kissed' | 'loves' | 'hit'
A syntatic pattern is an expression formed with this grammar by adding pattern
variables. Pattern variables are denoted here by identifiers preceded by
question marks, e.g. ?x. A pattern variable denotes an arbitrary entity of one
of the classes, S, NP, ..., V -- this class is referred to as the variable's
type. A variable's type is assumed to be given a priori.
In addition, lambda abstractions are allowed. For example:
F = lambda ?x: NP ( ?x kissed the girl)
denotes the function which takes a NP argument and produces the result as
indicated in the brackets. For example:
F[the boy] = [the boy kissed the girl]
The type of this function is denoted as (NP --> S).
Underlying these considerations is a type system for syntatic patterns.
This system is defined a set of type matching rules for each non-terminal in
the grammar; the rules are generated from the grammar itself. For example,
the type matching rules for the class S are:
(I) ?x: S if and only if ?x denotes an arbitrary member of S.
(II) if np: NP and vp: VP then np vp: S
In addition for these type matching rules, there are type matching rules for
lambda abstractions:
(I) if ?x: N1 and f(?x): N2 then (lambda ?x. f(?x)): N1 --> N2
(II) if f: N1 --> N2 and n: N1 then (f n): N2
For each type, the pattern space has a partial ordering defined on it.
For example, if A and B are patterns of type S, then
A Less1 B if and only if A = (lambda ?x.B) n
for some pattern variable ?x and compatible pattern n. This states that
A is a less general pattern than B and can be derived from B by substituting
for one pattern variable. The partial ordering, Less, is defined as the
reflexive/transitive closure of this relation.
Since we have a partial ordering, we can define least upper bounds and
greatest lower bounds. This is where the previous article figures in. The
greatest lower bound of two patterns is the result obtained by the Unification
Algorithm. The least upper bound is obtained by the Other Unification
Algorithm discussed in that article.
For reference, I will denote this least upper bound as the Abstraction of
the two patterns and will call the algorithm Abstraction Unification. Given
two pattern A, B if their abstraction is a pattern C then the following is
true:
A = lambda ?x1. ... (lambda ?xm. C) n1 ... nm
B = lambda ?y1. ... (lambda ?yn. C) p1 ... pm
For example, for the two patterns:
?np kissed the girl, the boy ?vp
the abstraction is:
?np ?vp
and
?np kissed the girl = ( lambda ?vp. (?np ?vp) ) [kissed the girl]
the boy ?vp = ( lambda ?np. (?np ?vp) ) [the boy]
Another example:
?np kissed the girl, ?np hit the boy
gives:
?np ?v the ?n
where:
?np kissed the girl = lambda ?v. lambda ?n.(?np ?v the ?n) [kissed] [girl]
?np hit the boy = lambda ?v. lambda ?n.(?np ?v the ?n) [hit] [boy]
It is here that we see the significance of Abstraction Unification: It is a
*syntatic pattern recognition* algorithm, capable of inducting parametrized
patterns from a set of instances.