1 Glue Semantics

2 Linear logic

>>> from nltk.sem.linearlogic import *
>>> from nltk.sem.glue import *

>>> llp = LinearLogicParser()

>>> from nltk.sem import logic

Parser

>>> print llp.parse(r'f')
f
>>> print llp.parse(r'(g -o f)')
(g -o f)
>>> print llp.parse(r'(g -o (h -o f))')
(g -o (h -o f))
>>> print llp.parse(r'((g -o G) -o G)')
((g -o G) -o G)
>>> print llp.parse(r'(g -o f)(g)')
(g -o f)(g)
>>> print llp.parse(r'((g -o G) -o G)((g -o f))')
((g -o G) -o G)((g -o f))

Simplify

>>> print llp.parse(r'f').simplify()
f
>>> print llp.parse(r'(g -o f)').simplify()
(g -o f)
>>> print llp.parse(r'((g -o G) -o G)').simplify()
((g -o G) -o G)
>>> print llp.parse(r'(g -o f)(g)').simplify()
f
>>> try: llp.parse(r'(g -o f)(f)').simplify()
... except LinearLogicApplicationException, e: print e
...
Cannot apply (g -o f) to f. Cannot unify g with f given {}
>>> print llp.parse(r'(G -o f)(g)').simplify()
f
>>> print llp.parse(r'((g -o G) -o G)((g -o f))').simplify()
f

Test BindingDict

>>> h = ConstantExpression('h')
>>> g = ConstantExpression('g')
>>> f = ConstantExpression('f')

>>> H = VariableExpression('H')
>>> G = VariableExpression('G')
>>> F = VariableExpression('F')

>>> d1 = BindingDict([(H,h)])
>>> d2 = BindingDict([(F,f),(G,F)])
>>> d12 = d1 + d2
>>> all12 = ['%s: %s' % (v, d12[v]) for v in d12.d]
>>> all12.sort()
>>> print all12
['F: f', 'G: f', 'H: h']

>>> d4 = BindingDict([(F,f)])
>>> try: d4[F] = g
... except VariableBindingException, e: print e
Variable F already bound to another value

Test Unify

>>> try: f.unify(g, BindingDict())
... except UnificationException, e: print e
...
Cannot unify f with g given {}

>>> print f.unify(G, BindingDict())
{G: f}
>>> try: f.unify(G, BindingDict([(G,h)]))
... except UnificationException, e: print e
...
Cannot unify f with G given {G: h}
>>> print f.unify(G, BindingDict([(G,f)]))
{G: f}
>>> print f.unify(G, BindingDict([(H,f)]))
{H: f, G: f}

>>> print G.unify(f, BindingDict())
{G: f}
>>> try: G.unify(f, BindingDict([(G,h)]))
... except UnificationException, e: print e
...
Cannot unify G with f given {G: h}
>>> print G.unify(f, BindingDict([(G,f)]))
{G: f}
>>> print G.unify(f, BindingDict([(H,f)]))
{H: f, G: f}

>>> print G.unify(F, BindingDict())
{G: F}
>>> try: G.unify(F, BindingDict([(G,H)]))
... except UnificationException, e: print e
...
Cannot unify G with F given {G: H}
>>> print G.unify(F, BindingDict([(G,F)]))
{G: F}
>>> print G.unify(F, BindingDict([(H,F)]))
{H: F, G: F}

Test Compile

>>> print llp.parse('g').compile_pos(Counter(), GlueFormula)
(<ConstantExpression g>, [])
>>> print llp.parse('(g -o f)').compile_pos(Counter(), GlueFormula)
(<ImpExpression (g -o f)>, [])
>>> print llp.parse('(g -o (h -o f))').compile_pos(Counter(), GlueFormula)
(<ImpExpression (g -o (h -o f))>, [])

3 Glue

3.1 Demo of "John walks"

>>> john = GlueFormula("John", "g")
>>> print john
John : g
>>> walks = GlueFormula(r"\x.walks(x)", "(g -o f)")
>>> print walks
\x.walks(x) : (g -o f)
>>> print walks.applyto(john)
\x.walks(x)(John) : (g -o f)(g)
>>> print walks.applyto(john).simplify()
walks(John) : f

3.2 Demo of "A dog walks"

>>> a = GlueFormula("\P Q.some x.(P(x) and Q(x))", "((gv -o gr) -o ((g -o G) -o G))")
>>> print a
\P Q.exists x.(P(x) & Q(x)) : ((gv -o gr) -o ((g -o G) -o G))
>>> man = GlueFormula(r"\x.man(x)", "(gv -o gr)")
>>> print man
\x.man(x) : (gv -o gr)
>>> walks = GlueFormula(r"\x.walks(x)", "(g -o f)")
>>> print walks
\x.walks(x) : (g -o f)
>>> a_man = a.applyto(man)
>>> print a_man.simplify()
\Q.exists x.(man(x) & Q(x)) : ((g -o G) -o G)
>>> a_man_walks = a_man.applyto(walks)
>>> print a_man_walks.simplify()
exists x.(man(x) & walks(x)) : f

3.3 Demo of 'every girl chases a dog'

Individual words:

>>> every = GlueFormula("\P Q.all x.(P(x) -> Q(x))", "((gv -o gr) -o ((g -o G) -o G))")
>>> print every
\P Q.all x.(P(x) -> Q(x)) : ((gv -o gr) -o ((g -o G) -o G))
>>> girl = GlueFormula(r"\x.girl(x)", "(gv -o gr)")
>>> print girl
\x.girl(x) : (gv -o gr)
>>> chases = GlueFormula(r"\x y.chases(x,y)", "(g -o (h -o f))")
>>> print chases
\x y.chases(x,y) : (g -o (h -o f))
>>> a = GlueFormula("\P Q.some x.(P(x) and Q(x))", "((hv -o hr) -o ((h -o H) -o H))")
>>> print a
\P Q.exists x.(P(x) & Q(x)) : ((hv -o hr) -o ((h -o H) -o H))
>>> dog = GlueFormula(r"\x.dog(x)", "(hv -o hr)")
>>> print dog
\x.dog(x) : (hv -o hr)

Noun Quantification can only be done one way:

>>> every_girl = every.applyto(girl)
>>> print every_girl.simplify()
\Q.all x.(girl(x) -> Q(x)) : ((g -o G) -o G)
>>> a_dog = a.applyto(dog)
>>> print a_dog.simplify()
\Q.exists x.(dog(x) & Q(x)) : ((h -o H) -o H)

The first reading is achieved by combining 'chases' with 'a dog' first. Since 'a girl' requires something of the form '(h -o H)' we must get rid of the 'g' in the glue of 'see'. We will do this with the '-o elimination' rule. So, x1 will be our subject placeholder.

>>> xPrime = GlueFormula("x1", "g")
>>> print xPrime
x1 : g
>>> xPrime_chases = chases.applyto(xPrime)
>>> print xPrime_chases.simplify()
\y.chases(x1,y) : (h -o f)
>>> xPrime_chases_a_dog = a_dog.applyto(xPrime_chases)
>>> print xPrime_chases_a_dog.simplify()
exists x.(dog(x) & chases(x1,x)) : f

Now we can retract our subject placeholder using lambda-abstraction and combine with the true subject.

>>> chases_a_dog = xPrime_chases_a_dog.lambda_abstract(xPrime)
>>> print chases_a_dog.simplify()
\x1.exists x.(dog(x) & chases(x1,x)) : (g -o f)
>>> every_girl_chases_a_dog = every_girl.applyto(chases_a_dog)
>>> r1 = every_girl_chases_a_dog.simplify()
>>> r2 = GlueFormula(r'all x.(girl(x) -> exists z1.(dog(z1) & chases(x,z1)))', 'f')
>>> r1 == r2
True

The second reading is achieved by combining 'every girl' with 'chases' first.

>>> xPrime = GlueFormula("x1", "g")
>>> print xPrime
x1 : g
>>> xPrime_chases = chases.applyto(xPrime)
>>> print xPrime_chases.simplify()
\y.chases(x1,y) : (h -o f)
>>> yPrime = GlueFormula("x2", "h")
>>> print yPrime
x2 : h
>>> xPrime_chases_yPrime = xPrime_chases.applyto(yPrime)
>>> print xPrime_chases_yPrime.simplify()
chases(x1,x2) : f
>>> chases_yPrime = xPrime_chases_yPrime.lambda_abstract(xPrime)
>>> print chases_yPrime.simplify()
\x1.chases(x1,x2) : (g -o f)
>>> every_girl_chases_yPrime = every_girl.applyto(chases_yPrime)
>>> print every_girl_chases_yPrime.simplify()
all x.(girl(x) -> chases(x,x2)) : f
>>> every_girl_chases = every_girl_chases_yPrime.lambda_abstract(yPrime)
>>> print every_girl_chases.simplify()
\x2.all x.(girl(x) -> chases(x,x2)) : (h -o f)
>>> every_girl_chases_a_dog = a_dog.applyto(every_girl_chases)
>>> r1 = every_girl_chases_a_dog.simplify()
>>> r2 = GlueFormula(r'exists x.(dog(x) & all z2.(girl(z2) -> chases(z2,x)))', 'f')
>>> r1 == r2
True

3.4 Compilation

>>> for cp in GlueFormula('m', '(b -o a)').compile(Counter()): print cp
m : (b -o a) : {1}
>>> for cp in GlueFormula('m', '((c -o b) -o a)').compile(Counter()): print cp
v1 : c : {1}
m : (b[1] -o a) : {2}
>>> for cp in GlueFormula('m', '((d -o (c -o b)) -o a)').compile(Counter()): print cp
v1 : c : {1}
v2 : d : {2}
m : (b[1, 2] -o a) : {3}
>>> for cp in GlueFormula('m', '((d -o e) -o ((c -o b) -o a))').compile(Counter()): print cp
v1 : d : {1}
v2 : c : {2}
m : (e[1] -o (b[2] -o a)) : {3}
>>> for cp in GlueFormula('m', '(((d -o c) -o b) -o a)').compile(Counter()): print cp
v1 : (d -o c) : {1}
m : (b[1] -o a) : {2}
>>> for cp in GlueFormula('m', '((((e -o d) -o c) -o b) -o a)').compile(Counter()): print cp
v1 : e : {1}
v2 : (d[1] -o c) : {2}
m : (b[2] -o a) : {3}

3.5 Demo of 'a man walks' using Compilation

Premises

>>> a = GlueFormula('\\P Q.some x.(P(x) and Q(x))', '((gv -o gr) -o ((g -o G) -o G))')
>>> print a
\P Q.exists x.(P(x) & Q(x)) : ((gv -o gr) -o ((g -o G) -o G))

>>> man = GlueFormula('\\x.man(x)', '(gv -o gr)')
>>> print man
\x.man(x) : (gv -o gr)

>>> walks = GlueFormula('\\x.walks(x)', '(g -o f)')
>>> print walks
\x.walks(x) : (g -o f)

Compiled Premises:

>>> counter = Counter()
>>> ahc = a.compile(counter)
>>> g1 = ahc[0]
>>> print g1
v1 : gv : {1}
>>> g2 = ahc[1]
>>> print g2
v2 : g : {2}
>>> g3 = ahc[2]
>>> print g3
\P Q.exists x.(P(x) & Q(x)) : (gr[1] -o (G[2] -o G)) : {3}
>>> g4 = man.compile(counter)[0]
>>> print g4
\x.man(x) : (gv -o gr) : {4}
>>> g5 = walks.compile(counter)[0]
>>> print g5
\x.walks(x) : (g -o f) : {5}

Derivation:

>>> g14 = g4.applyto(g1)
>>> print g14.simplify()
man(v1) : gr : {1, 4}
>>> g134 = g3.applyto(g14)
>>> print g134.simplify()
\Q.exists x.(man(x) & Q(x)) : (G[2] -o G) : {1, 3, 4}
>>> g25 = g5.applyto(g2)
>>> print g25.simplify()
walks(v2) : f : {2, 5}
>>> g12345 = g134.applyto(g25)
>>> print g12345.simplify()
exists x.(man(x) & walks(x)) : f : {1, 2, 3, 4, 5}

Dependency Graph to Glue Formulas

>>> depgraph = DependencyGraph("""1 John    _       NNP     NNP     _       2       SUBJ    _       _
... 2       sees    _       VB      VB      _       0       ROOT    _       _
... 3       a       _       ex_quant        ex_quant        _       4       SPEC    _       _
... 4       dog     _       NN      NN      _       2       OBJ     _       _
... """)
>>> gfl = GlueDict('glue.semtype').to_glueformula_list(depgraph)
>>> for gf in gfl: print gf
\x y.sees(x,y) : (f -o (i -o g))
\P Q.exists x.(P(x) & Q(x)) : ((fv -o fr) -o ((f -o F2) -o F2))
\x.John(x) : (fv -o fr)
\x.dog(x) : (iv -o ir)
\P Q.exists x.(P(x) & Q(x)) : ((iv -o ir) -o ((i -o I5) -o I5))
>>> glue = Glue()
>>> for r in glue.get_readings(glue.gfl_to_compiled(gfl)):
...     print r.simplify().normalize()
exists x.(dog(x) & exists z1.(John(z1) & sees(z1,x)))
exists x.(John(x) & exists z1.(dog(z1) & sees(x,z1)))

Dependency Graph to LFG f-structure

>>> from nltk.sem.lfg import FStructure
>>> fstruct = FStructure.read_depgraph(depgraph)
>>> print fstruct
f:[pred 'sees'
   obj h:[pred 'dog'
          spec 'a']
   subj g:[pred 'John']]

LFG f-structure to Glue

>>> for gf in fstruct.to_glueformula_list(GlueDict('glue.semtype')):
...     print gf
\x y.sees(x,y) : (i -o (g -o f))
\x.dog(x) : (gv -o gr)
\P Q.exists x.(P(x) & Q(x)) : ((gv -o gr) -o ((g -o G3) -o G3))
\P Q.exists x.(P(x) & Q(x)) : ((iv -o ir) -o ((i -o I4) -o I4))
\x.John(x) : (iv -o ir)

Initialize the Dependency Parser

>>> tagger = RegexpTagger(
...     [('^(John|Mary)$', 'NNP'),
...      ('^(sees|chases)$', 'VB'),
...      ('^(a)$', 'ex_quant'),
...      ('^(every)$', 'univ_quant'),
...      ('^(girl|dog)$', 'NN')
... ])
>>> depparser = MaltParser(tagger=tagger)

Automated Derivation

>>> glue = Glue(depparser=depparser)
>>> for reading in glue.parse_to_meaning('every girl chases a dog'):
...     print reading.simplify().normalize()
all x.(girl(x) -> exists z1.(dog(z1) & chases(x,z1)))
exists x.(dog(x) & all z1.(girl(z1) -> chases(z1,x)))

>>> drtglue = DrtGlue(depparser=depparser)
>>> for reading in drtglue.parse_to_meaning('every girl chases a dog'):
...     print reading.simplify().normalize()
([],[(([x],[girl(x)]) -> ([z1],[dog(z1), chases(x,z1)]))])
([z1],[dog(z1), (([x],[girl(x)]) -> ([],[chases(x,z1)]))])

With inference

Checking for equality of two DRSs is very useful when generating readings of a sentence. For example, the glue module generates two readings for the sentence John sees Mary:

>>> from nltk.sem.glue import DrtGlue
>>> readings = drtglue.parse_to_meaning('John sees Mary')
>>> for drs in readings:
...     print drs.simplify().normalize()
([x,z1],[John(x), Mary(z1), sees(x,z1)])
([x,z1],[Mary(x), John(z1), sees(z1,x)])

However, it is easy to tell that these two readings are logically the same, and therefore one of them is superfluous. We can use the theorem prover to determine this equivalence, and then delete one of them. A particular theorem prover may be specified, or the argument may be left off to use the default.

>>> readings[0].tp_equals(readings[1])
True