.. Copyright (C) 2001-2012 NLTK Project
.. For license information, see LICENSE.TXT

==============================================================================
 Glue Semantics
==============================================================================

.. include:: ../../doc/definitions.rst


======================
Linear logic 
======================

    >>> from nltk.sem import logic
    >>> from nltk.sem.linearlogic import *
    >>> from nltk.sem import linearlogic as linlog 
    >>> from nltk.sem.glue import *
    
    >>> llp = LinearLogicParser()
    
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 = linlog.ConstantExpression('h')
    >>> g = linlog.ConstantExpression('g')
    >>> f = linlog.ConstantExpression('f')

    >>> H = linlog.VariableExpression('H')
    >>> G = linlog.VariableExpression('G')
    >>> F = linlog.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))>, [])


======================
Glue 
======================

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


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


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
    
    
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}
        

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
---------------------------------
    >>> from nltk.corpus.reader.dependency import DependencyGraph

    >>> 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 z1.(dog(z1) & exists z2.(John(z2) & sees(z2,z1)))
    exists z1.(John(z1) & exists z2.(dog(z2) & sees(z1,z2)))

-----------------------------------
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
--------------------------------
    >>> from nltk.parse.malt import MaltParser

    >>> 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'.split()): 
    ...     print reading.simplify().normalize()
    all z1.(girl(z1) -> exists z2.(dog(z2) & chases(z1,z2)))
    exists z1.(dog(z1) & all z2.(girl(z2) -> chases(z2,z1)))

    >>> drtglue = DrtGlue(depparser=depparser)
    >>> for reading in drtglue.parse_to_meaning('every girl chases a dog'.split()): 
    ...     print reading.simplify().normalize()
    ([],[(([z1],[girl(z1)]) -> ([z2],[dog(z2), chases(z1,z2)]))])
    ([z1],[dog(z1), (([z2],[girl(z2)]) -> ([],[chases(z2,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'.split())
    >>> for drs in readings: 
    ...     print drs.simplify().normalize()
    ([z1,z2],[John(z1), Mary(z2), sees(z1,z2)])
    ([z1,z2],[Mary(z1), John(z2), sees(z2,z1)])

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].equiv(readings[1])
    True