1
   Glue Semantics

2   Linear logic

  
>>> from nltk_contrib.gluesemantics.linearlogic import *
>>> from nltk_contrib.gluesemantics.glue import *
  
>>> llp = LinearLogicParser()
  
>>> from nltk.sem import logic
>>> logic.n = logic.Tokens.NEW_NLTK

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("\\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("\\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)
>>> 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) implies 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("\\x.girl(x)", "(gv -o gr)")
>>> print girl
\x.girl(x) : (gv -o gr)
>>> chases = GlueFormula("\\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("\\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}