.. -*- mode: rst -*-
.. include:: ../../doc/definitions.rst

.. standard global imports

    >>> import nltk, re, pprint

.. |multimap| unicode:: U+22B8
.. |vdash| unicode:: U+22A6
.. |nvdash| unicode:: U+22AC
.. |delta| unicode:: U+03B4
.. |Delta| unicode:: U+0394
.. |emptyset| unicode:: U+2205
.. |dagger| unicode:: U+2020
.. |tab| unicode:: U+00A0 U+00A0 U+00A0 U+00A0 U+00A0 U+00A0 U+00A0 U+00A0


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

:Author: Daniel H. Garrette

------------
Introduction
------------

This chapter expands on the ideas about Semantic Interpretation presented in Chapter 12.  The `Principle of Compositionality`:dt: states that the meaning of a whole is a function of the meanings of the parts and of the way they are syntactically combined. Chapter 11 described an algorithm to perform this composition.  However, as it was noted in the chapter, there are some limitations that quickly arise.  For example, note (43), (44a), and (44b) from Chapter 11 repeated here as compexa_--compexc_ respectively.

.. _compex:
.. ex::

   .. _compexa:
   .. ex::
     Every girl chases a dog.

   .. _compexb:
   .. ex::
      all x.(girl(x) |rarr| exists y.(dog(y) & chase(x, y)))

   .. _compexc:
   .. ex::
      exists y.(dog(y) & all x.(girl(x) |rarr| chase(x, y)))

In this example, compexa_ should give rise to both readings compexb_ and compexc_. However, the procedure described in Chapter 11 only generates compexb_. The reason for this discrepancy is that semantic interpretation in Chapter 11 is too closely tied to syntax. In reading compexb_, the word `every`:lx: out-scopes the word `a`:lx:. This is a result of the sentence's word order: `every`:lx: comes before `a`:lx:. In the semantic composition, `every`:lx: combines with `boy`:lx: and `a`:lx: with `girl`:lx:. But since `a girl`:lx: is a sub-part of the VP `chases a girl`:lx:, `a girl`:lx: is combined with `chases`:lx: before `every boy`:lx: is.

In contrast, Glue Semantics, offers an elegant approach to determining scope based on the use of resource-sensitive logic as a means to "glue" the |lambda|\-calculus meaning terms together.

------------
Linear Logic
------------

The particular "glue" logic that we will use is `Implicational Linear Logic`:dt:. It is a subset of Propositional Logic (see Chapter 12.3). The logic is "implicational" because it's only operator is the implication. However, we will use the symbol |multimap| for linear logic implication instead of the symbol |rarr| which was used in the propositional and first order logics. Just as in propositional logic, the implication is used in the following way:

.. _imp1:
.. ex::
    A, (A |multimap| B) |vdash| B

Linear Logic is `resource-sensitive`:dt: because every premise in a resource-sensitive proof must be used *once and only once*.  Therefore, unlike propositional or first order logics, we have the following rules:

.. _imp2:
.. ex::

   .. _imp2a:
   .. ex::
      A, (A |multimap| B) |nvdash| A, B

   .. _imp2b:
   .. ex::
      A, A, (A |multimap| B) |nvdash| B

The best way to think about these rules is consider the linear logic implicational statement as a function that **consumes** its antecedent and itself to **produce** its consequent.  Example imp1_ is valid because `A`:mathit: is applied to `(A`:mathit: |multimap| `B)`:mathit: which consumes both and produces `B`:mathit:.  On the other hand imp2a_ is invalid because the premise `A`:mathit: is consumed by the implication and therefore cannot appear in the conclusion.  Finally, imp2b_ is invalid because the premise `A`:mathit: appears twice, but there is only one implication to consume it, and since every premise must be used exactly once, the second instance of `A`:mathit: cannot be ignored.

Linear Logic in NLTK
~~~~~~~~~~~~~~~~~~~~

All the tools needed to work in implicational linear logic are found in the file ``linearlogic.py``.  This module is modeled after the module ``logic.py``.  Strings can be parsed using the class ``Parser``; ``ApplicationExpression``\s can be applied to other ``Expression``\s using the method ``applyto()``.  Note that ``applyto()`` will only succeed if the application is legal, otherwise it will raise an exception.

    >>> from nltk_contrib.gluesemantics import linearlogic
    >>> llp = linearlogic.LinearLogicParser()
    >>> p = llp.parse('p')
    >>> print p
    p
    >>> p_q = llp.parse('(p -o q)')
    >>> print p_q 
    (p -o q) 
    >>> q = p_q.applyto(p) 
    >>> q 
    <ApplicationExpression (p -o q)(p)>
    >>> print q.simplify() 
    q 
    >>> p = p_q.applyto(q) 
    LinearLogicApplicationError: Cannot apply (p -o q) to q 

The module also binds variables correctly and stores those bindings for
future applications.  The when printing an ``Expression``, the bindings are
displayed as a list at the end.

    >>> gf = llp.parse('(g -o f)')
    >>> gGG = llp.parse('((g -o G) -o G)')
    >>> f = gGG.applyto(gf)
    >>> f
    <ApplicationExpression ((g -o G) -o G)((g -o f))>
    >>> print f.simplify()
    f
    >>> HHG = llp.parse('(H -o (H -o G))')
    >>> ff = HHG.applyto(f)
    >>> print ff
    (H -o (H -o G))(((g -o G) -o G)((g -o f)))
    >>> print ff.simplify()
    (f -o f)

-------------
Glue Formulas
-------------

In chapter 12, we introduced the idea that words can be associated with meaning terms stated in |lambda|\-calculus.  For example, the verb `walk`:lx: can be represented as a function from a value of type **Ind** to a value of type **Bool**, |lambda|\ `x.walk(x)`:mathit:. Glue semantics extends this system by dictating that a Glue Formula is comprised of a meaning term and a "Glue Term".  The Glue Term is a linear logic statement that constrains the ways that the Glue Formula may combine with other glue formulas. For the verb `walks`:lx:, the glue statement would be `(g`:mathit: |multimap| `f)`:mathit: where `g`:mathit: represents the verb's subject (an **Ind**) and `f`:mathit: represents the verb's clause.  Thus the Glue Formula for the verb `walk`:lx: is a pair |lambda|\ `x.(walk x) : (g`:mathit: |multimap| `f)`:mathit:.

To show how this Glue Formula is used, let us assume that a proper noun, such as `John`:lx:, is represented with the Glue Formula `John : g`:mathit: since John is of the type **Ind**. If we want to combine these formulas to get the meaning of the sentence `John walks`:lx: we will do so by allowing the glue terms to dictate how the meaning terms will be applied. The glue terms can be combined as a proof of `f`:mathit:, which represents the entire sentence. This is shown as ex7_:

.. _ex7:
.. ex::
   g, (g |multimap| f) |vdash| f

In order to produce the reading for the sentence from this linear logic proof, we will have to attach the meaning terms to the glue terms and apply them appropriately at each step of the proof.  The rule for applying one glue formula to another is shown in ex8_:

.. _ex8:
.. ex::
    .. image:: images/proof_app_abstract.png

Therefore, all together we have the following proof that produces a semantic meaning for the sentence `John walks`:lx: in ex9_:

.. _ex9:
.. ex::
    .. image:: images/proof_app_concrete.png

And |lambda|\ `x.walks(x)(John)`:mathit: |beta|\-reduces to `walk(John)`:mathit:.


Glue Formulas in NLTK
~~~~~~~~~~~~~~~~~~~~~

The tools available for using Glue Semantics are found in the file "glue.py".  The ``GlueFormula`` class is used for glue formulas.  It contains an ``appyto()`` method for performing applications on other ``GlueFormulas``\.

    >>> from nltk_contrib.gluesemantics import glue
    >>> walks = glue.GlueFormula(r'\x.walks(x)', '(g -o f)')
    >>> walks
    \x.walks(x) : (g -o f)
    >>> john = glue.GlueFormula('John', 'g')
    >>> john
    John : g
    >>> john_walks = walks.applyto(john)
    >>> john_walks
    \x.walks(x)(John) : (g -o f)(g)
    >>> john_walks.simplify()
    walks(John) : f


--------------------------
Syntax-Semantics Interface
--------------------------

An appropriate next question would ask how we determine which propositions to use in the glue terms.  For example, in ex9_, why is `John`:lx: paired with `g`:mathit: and `walks`:lx: with `(g`:mathit: |multimap| `f)`:mathit:?  The answer is that `walks`:lx: is an intransitive verb and the meaning of an intransitive verb is a function that takes the verb's subject as input and returns the truth value of the verb's clause.  In our example, `g`:mathit: is the proposition representing the verb's subject, so it is natural that it is the antecedent in the verb's glue term.
    
The traditional way that syntactic relationships are shown in Glue literature is with Lexical Functional Grammar (Dal01).  The sentence `John walks`:lx: would be represented as ex10_:

.. _ex10:
.. ex::
    .. image:: images/fstruct_subj.png

This style of marking syntactic structure allows us to clearly see that `f`:mathit: represented the entire sentence and that `g`:mathit: represents the subject of the sentence. Let us compare this to the representation and subsequent proof (with |beta|\-reductions done as we progress) of the sentence `John sees Mary`:lx:, shown as ex11_ and ex12_ respectively:
        
.. _ex11:
.. ex::
    .. image:: images/fstruct_obj.png

.. _ex12:
.. ex::
    .. image:: images/proof_trans.png

In this case the verb is transitive, so it must have a subject (`John`:lx:) and an object (`Mary`:lx:). 


Transitive Verbs in NLTK
~~~~~~~~~~~~~~~~~~~~~~~~

    >>> from nltk_contrib.gluesemantics import glue
    >>> john = glue.GlueFormula('John', 'g')
    >>> mary = glue.GlueFormula('Mary', 'h')
    >>> sees = glue.GlueFormula(r'\x y.sees(x,y)', '(g -o (h -o f))')
    >>> john_sees = sees.applyto(john)
    >>> john_sees.simplify()
    \y.sees(John,y) : (h -o f)
    >>> john_sees_mary = john_sees.applyto(mary)
    >>> john_sees_mary.simplify()
    sees(John,Mary) : f

Also, notice what happens if we try to apply the individuals in the wrong sequence: 

    >>> sees.applyto(mary)
    LinearLogicApplicationException: \x.\y.sees(x,y) : (g -o (h -o f)) applied to Mary : h

--------------
Quantification
--------------

As was noted in chapter 12, a quantifier is of type  ((**Ind** |rarr| **Bool**) |rarr| ((**Ind** |rarr| **Bool**) |rarr| **Bool**)).   A quantifier can combine with a noun, which is of type (**Ind** |rarr| **Bool**) , to give a quantified noun,  which is of type  ((**Ind** |rarr| **Bool**) |rarr| **Bool**).  A quantified noun can then be combined with a verb to make a clause.

For reference, let us give the LFG f-structure for the sentence `a man walks`:lx:\ :

.. _ex16:
.. ex::
    .. image:: images/fstruct_quant.png

We will examine the noun first.  The meaning of a noun can be viewed as a function from an individual to a truth value.  For example, the glue formula for the word `man`:lx: is given in ex13_:

.. _ex13:
.. ex::
    |lambda|\ x.man(x) : (gv |multimap| gr)

The meaning term tells us that `man`:lx: is a function that takes an individual as input and returns a truth value for whether that individual is a man. The glue term naturally mirrors the single-argument-function pattern of the meaning term. Here we have `gv`:mathit:, which is `g`:mathit:'s VAR-value, and `gr`:mathit:, which is `g`:mathit:'s  RESTR-value.  We can see in ex17_ how a noun combines with a quantifier to create a quantified noun phrase.

.. _ex17:
.. ex::
    .. image:: images/proof_quant_noun.png

At this point we must pause to discuss the glue proposition `G`:mathit:.  In the glue for this quantified noun phrase, `G`:mathit: is a variable\ [#capitals]_ standing for an expression of type **Bool**. As one would expect from a variable, it may bind with any proposition of type **Bool** in the course of a proof. We can now see how the result from ex17_ can be combined with the word `walks`:lx: to give the reading of the entire sentence.  The proof is given in ex18_:

.. _ex18:
.. ex::
    .. image:: images/proof_quant_sent.png

An existential quantifier such as `a`:lx: or `some`:lx: is represented as quanta_.  A universal quantifier such as `all`:lx: or `every`:lx: is represented as quantb_:

.. _quant:
.. ex::

    .. _quanta:
    .. ex::
       |lambda|\ P. |lambda|\ Q.exists x.(P(x) & Q(x)) : ((gv |multimap| gr) |multimap| ((g |multimap| G) |multimap| G))
    
    .. _quantb:
    .. ex::
       |lambda|\ P. |lambda|\ Q.all x.(P(x) |rarr| Q(x)) : ((gv |multimap| gr) |multimap| ((g |multimap| G) |multimap| G))


Quantification in NLTK
~~~~~~~~~~~~~~~~~~~~~~

    >>> a = glue.GlueFormula(r'\P Q.exists x.(P(x) & Q(x))', '((gv -o gr) -o ((g -o G) -o G))')
    >>> man = glue.GlueFormula(r'\x.man(x)', '(gv -o gr)')
    >>> walks = glue.GlueFormula(r'\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

------------------
Semantic Ambiguity
------------------

Semantic ambiguity is ambiguity that arises from semantics, even when the syntax is unambiguous.  An example of a semantically ambiguous sentence is compexa_, repeated here as ex19_.  It is ambiguous because it can be interpreted as either ex20_ or ex21_.

.. _compex2:
.. ex::

    .. _ex19:
    .. ex::
        Every girl chases a dog.
    
    .. _ex20:
    .. ex::
        all x.(girl(x) |rarr| exists y. (dog(y) & chase(x,y)))
    
    .. _ex21:
    .. ex::
        exists y.(dog(y) & all x. (girl(x) |rarr| chase(x,y)))

Glue semantics will allow us to generate both of these readings through the same proof strategies.  But first, we will have to introduce a new proof rule.  The rule in ex22_ allows us to create a unique\ [#fresh]_ temporary hypothesis and then to abstract it away.

.. _ex22:
.. ex::
    .. image:: images/proof_abstraction.png

So, to generate readings for ex19_, we start with a list of premises:

.. _premises:
.. ex::

    .. _ex23:
    .. ex::
       **[every]** |lambda|\ P.\ |lambda|\ Q.all x.(P(x) |rarr| Q(x)) : ((gv |multimap| gr) |multimap| ((g |multimap| G) |multimap| G))
    
    .. _ex24:
    .. ex::
       **[girl]** |lambda|\ x.girl(x) : (gv |multimap| gr)
    
    .. _ex25:
    .. ex::
       **[chases]** |lambda|\ x.\ |lambda|\ y.chase(x,y) : (g |multimap| (h |multimap| f))
    
    .. _ex26:
    .. ex::
       **[a]** |lambda|\ P.\ |lambda|\ Q.exists x.(P(x) & Q(x)) : ((hv |multimap| hr) |multimap| ((h |multimap| H) |multimap| H))
    
    .. _ex27:
    .. ex::
       **[dog]** |lambda|\ x.dog(x) : (hv |multimap| hr)

It is easy to see that `every`:lx: can only combine with `girl`:lx: and `a`:lx: only with `dog`:lx:.  We perform these combinations to generate both quantified nouns.

.. _quantNouns:
.. ex::

    .. _ex28:
    .. ex::
        **[every-girl]** |lambda|\ Q.all x.(girl(x) |rarr| Q(x)) : ((g |multimap| G) |multimap| G)
    
    .. _ex29:
    .. ex::
        **[a-dog]** |lambda|\ Q.exists x.(dog(x) & Q(x)) : ((h |multimap| H) |multimap| H)

Now we can generate exactly two readings from these two quantified nouns and the
verb `chases`:lx:.  The proofs are detailed as ex30_ and ex31_:

.. _semanticAmbiguity:
.. ex::

    .. _ex30:
    .. ex::
        .. image:: images/proof_semanticAmbiguity1.png
        
    .. _ex31:
    .. ex::
        .. image:: images/proof_semanticAmbiguity2.png

Semantic Ambiguity in NLTK
~~~~~~~~~~~~~~~~~~~~~~~~~~

To generate the readings of the sentence `Every girl chases a dog`:lx:, we must
generate the quantified noun phrases `every girl`:lx: and `a dog`:lx: first, along with
the verb `chases`:lx:.

    >>> every = glue.GlueFormula(r'\P Q.all x.(P(x) -> Q(x))', '((gv -o gr) -o ((g -o G) -o G))')
    >>> girl = glue.GlueFormula(r'\x.girl(x)', '(gv -o gr)')
    >>> every_girl = every.applyto(girl)
    >>> print every_girl.simplify()
    \Q.all x.(girl(x) -> Q(x)) : ((g -o G) -o G)
    >>> chases = glue.GlueFormula(r'\x y.chase(x,y)', '(g -o (h -o f))')
    >>> print chases
    \x.\y.chase(x,y) : (g -o (h -o f))
    >>> a = glue.GlueFormula(r'\P Q.exists x.(P(x) & Q(x))', '((hv -o hr) -o ((h -o H) -o H))')
    >>> dog = glue.GlueFormula(r'\x.dog(x)', '(hv -o hr)')
    >>> a_dog = a.applyto(dog)
    >>> print a_dog.simplify()
    \Q.exists x.(dog(x) & Q(x)) : ((h -o H) -o H)

Because the rest of the assembly requires the abstraction rule ex22_, we will need a new technique to achieve the functionality of this rule.  We will do this by creating a hypothesis glue formula whose meaning term is a variable and whose glue term is the glue expression needed.  We can then abstract this hypothesis away using the method ``lambda_abstract()`` which takes the hypothesis to be abstracted as its argument.

    >>> x1 = glue.GlueFormula('x1', 'A')
    >>> psi = glue.GlueFormula(r'\x.psi(x)', '(A -o B)')
    >>> psi_x1 = psi.applyto(x1)
    >>> print psi_x1.simplify()
    psi(x1) : B
    >>> psi2 = psi_x1.lambda_abstract(x1)
    >>> print psi2
    \x1.\x.psi(x)(x1) : (A -o (A -o B)(A))
    >>> print psi2.simplify()
    \x1.psi(x1) : (A -o B)

We can now use this technique to generate the readings for `Every girl chases
a dog`:lx: from the quantified nouns and the verb.  The first will be modeled after
ex30_:

    >>> x1 = glue.GlueFormula('x1', 'g')
    >>> x1_chases = chases.applyto(x1)
    >>> print x1_chases.simplify()
    \y.chase(x1,y) : (h -o f)
    >>> x1_chases_a_dog = a_dog.applyto(x1_chases)
    >>> print x1_chases_a_dog.simplify()
    exists x.(dog(x) & chase(x1,x)) : f
    >>> chases_a_dog = x1_chases_a_dog.lambda_abstract(x1)
    >>> print chases_a_dog.simplify()
    \x1.exists x.(dog(x) & chase(x1,x)) : (g -o f)
    >>> every_girl_chases_a_dog = every_girl.applyto(chases_a_dog)
    >>> print every_girl_chases_a_dog.simplify()
    all x.(girl(x) -> exists z1.(dog(z1) & chase(x,z1))) : f

The second will be modeled after ex31_:

    >>> x1 = glue.GlueFormula('x1', 'g')
    >>> x1_chases = chases.applyto(x1)
    >>> print x1_chases.simplify()
    \y.chase(x1,y) : (h -o f)
    >>> x2 = glue.GlueFormula('x2', 'h')
    >>> x1_chases_x2 = x1_chases.applyto(x2)
    >>> print x1_chases_x2.simplify()
    chase(x1,x2) : f
    >>> chases_x2 = x1_chases_x2.lambda_abstract(x1)
    >>> print chases_x2.simplify()
    \x1.chase(x1,x2) : (g -o f)
    >>> every_girl_chases_x2 = every_girl.applyto(chases_x2)
    >>> print every_girl_chases_x2.simplify()
    all x.(girl(x) -> chase(x,x2)) : f
    >>> every_girl_chases = every_girl_chases_x2.lambda_abstract(x2)
    >>> print every_girl_chases.simplify()
    \x2.all x.(girl(x) -> chase(x,x2)) : (h -o f)
    >>> every_girl_chases_a_dog = a_dog.applyto(every_girl_chases)
    >>> print every_girl_chases_a_dog.simplify()
    exists x.(dog(x) & all z1.(girl(z1) -> chase(z1,x))) : f

--------------------------------------
Computational Issues in Glue Semantics
--------------------------------------

Generation of Glue Formulas
~~~~~~~~~~~~~~~~~~~~~~~~~~~

To generate the glue formulas that will be used in the proof, we must first parse the sentence for syntax (see Chapters 7 and 8).  The glue module includes a class ``FStructure`` that is created from a parse tree.

    >>> from nltk.parse import load_earley
    >>> from nltk_contrib.gluesemantics import glue
    >>> from nltk_contrib.gluesemantics import lfg
    >>> cp = load_earley(r'grammars/gluesemantics.fcfg')
    >>> tokens = 'John sees a woman'.split()
    >>> trees = cp.nbest_parse(tokens)
    >>> glue_dict = glue.GlueDict('glue.semtype')
    >>> fstruct = lfg.FStructure.read_parsetree(trees[0])
    >>> print fstruct
    f:[pred 'sees'
       obj h:[pred 'woman'
              spec 'a']
       subj g:[pred 'John']]
    >>> for gf in fstruct.to_glueformula_list(glue_dict): print gf
    \x.\y.sees(x,y) : (g -o (h -o f))
    \x.woman(x) : (hv -o hr)
    \P.\Q.exists x.(P(x) & Q(x)) : ((hv -o hr) -o ((h -o H0) -o H0))
    John : g

Horn Clauses
~~~~~~~~~~~~~~~~~~~~~~~~

The problem of having the computer automatically assemble a sentence's glue premises into a proof becomes much more difficult with the rule given in ex22_ because the rule opens up the possibility of an infinite number of proofs for any valid set of premises.  This occurs because we are able to introduce and retract hypotheses at will, whether they are required or not.  So from the premises `g`:mathit: and `(g`:mathit: |multimap| `f)`:mathit: we can generate the following proofs ex32_-ex34_: 

.. _infiniteLoop:
.. ex::

    .. _ex32:
    .. ex::
        .. image:: images/proof_infLoop1.png
    
    .. _ex33:
    .. ex::
        .. image:: images/proof_infLoop2.png
    
    .. _ex34:
    .. ex::
        .. image:: images/proof_infLoop3.png

It should be clear that we could generate an infinite number of proofs following this pattern of hypothesizing and retracting variables.  It should also be clear that a single proof could involve an infinite number of these actions, and thus cause "proving" to take forever.  This is a major problem because in glue semantics we want to generate all possible proofs so that we can have all possible readings since each new proof could potentially give a different reading. 

The solution to this problem comes from [GL98]_.  The basic idea is to "compile" linear logic formulas into **horn clauses**, which are of the form (\ `g`:mathit:\ :subscript:`1` |multimap| (\ `g`:mathit:\ :subscript:`2` |multimap|  (\ |dots| |multimap| f))) where `g`:mathit:\ :subscript:`i` and `f`:mathit: are propositions.  By doing this we are generating new premises for all of the hypotheses that we would have needed to generate during the proof.  However, by compiling, we ensure that we will never need to make any hypotheses, and can therefore rid ourselves of the problematic rule ex22_.

The algorithm for linear logic compilation from [Lev07]_ is given as Figure compileAlgorithm_.


.. _compileAlgorithm:
.. ex::
    **Linear Logic Compilation Algorithm**

    | **function** ``compile-glue-formula``\ ( |psi| : X )
    | |tab| |langle|\ `Y`:mathit:, |Gamma|\ |rangle| := ``compile-pos``\ ( X )
    | |tab| **return** {\ |psi| : Y : {`i`:mathit:}} |cup| |Gamma| for a fresh index `i`:mathit:
    | **function** ``compile-pos``\ ( X ) where X is atomic
    | |tab| **return** |langle|\ X\ :subscript:`[]`, |emptyset|\ |rangle|
    | **function** ``compile-pos``\ ( X |multimap| Y )
    | |tab| |langle|\ |delta|, |Delta|\ |rangle| := ``compile-pos``\ ( Y )
    | |tab| |langle|\ |gamma|, |Gamma|\ |rangle| := ``compile-neg``\ ( X ) (\ |gamma| will be atomic)
    | |tab| **return** |langle| ( |gamma|\ |multimap|\ |delta|\ ), |Gamma| |cup| |Delta| |rangle|
    | **function** ``compile-neg``\ ( X ) where X is atomic
    | |tab| **return** |langle|\ X\ :subscript:`[]`, |emptyset|\ |rangle|
    | **function** ``compile-neg``\ ( X |multimap| Y )
    | |tab| |langle|\ |delta|\ :subscript:`L`, |Delta|\ |rangle| := ``compile-neg``\ ( Y ) (\ |delta| will be atomic)
    | |tab| |langle|\ |gamma|\ , |Gamma|\ |rangle| := ``compile-pos``\ ( X )
    | |tab| **return** |langle|\ |delta|\ :subscript:`[i|L]`, {v\ :subscript:`i` : |gamma| : {`i`:mathit:}} 
      |cup| |Gamma| |cup| |Delta|\ |rangle| for a fresh index `i`:mathit:\ :superscript:`|dagger|`
      
    :superscript:`|dagger|`\ [\ `i`:mathit:\ \|L] means a list whose head is `i`:mathit: and whose tail is `L`:mathit:

The compilation method changes our representation of a glue formula slightly because it affixes a **list of indices** to every glue formula.  When a premise is created, this list is instantiated with one unique index.  Additionally, every atomic linear logic expression will have its own **list of dependencies**. 

To turn our premises into horn clauses, we must get rid of any non-atomic  antecedents\ [#hornClauses]_. We will use ex35_ as an example.

.. _ex35:
.. ex::
    m : ((A |multimap| B) |multimap| C) 

To compile ex35_ we would turn `A`:mathit: into its own premise.  Since another premise `A`:mathit: might exist already, we must ensure that **this** `A`:mathit: is the one treated as the antecedent to `B`:mathit:.  We do this by adding the newly created  `A`:mathit: premise's index to `B`:mathit:\ 's list of dependencies.  Compilation of ex35_ will return glue formulas ex35compiledA_ and ex35compiledB_.

.. _ex35compiled:
.. ex::

    .. _ex35compiledA:
    .. ex::
        v1 : A : {1} 
    
    .. _ex35compiledB:
    .. ex::
        m : (B\ :subscript:`[1]` |multimap| C) : {2}

In the NLTK package, glue formula compilation can be performed using the ``compile()`` method:

    >>> from nltk_contrib.gluesemantics import glue
    >>> g = glue.GlueFormula('m', '((A -o B) -o C)')
    >>> gc = g.compile()
    >>> print gc[0]
    v1 : A : {1}
    >>> print gc[1]
    m : (B[1] -o C) : {2} 

Horn Clause Application
~~~~~~~~~~~~~~~~~~~~~~~

Naturally, we will have to incorporate the indices and dependencies into our application rule from ex8_.  The new rule is shown below as ex38_:

.. _ex38:
.. ex::
    .. image:: images/proof_hornClauseApp.png

You will notice that the set of indices of the conclusion is the sets of indices of both premises combined.  This means that a glue formula's set of indices is the set of premises that were consumed to generate that formula. It should be noted that |Gamma| and |Delta| will always be disjoint since the rules of linear logic say that no premise may be used more than once.  We also impose the condition that |alpha| must be a subset of |Gamma|.  This will ensure that the correct premises were used to generate the `A`:mathit: premise used in the application.

The requirement that `L`:mathit: be a subset of |Gamma| means that for the application to be successful, |phi| must have already incorporated all of the dependencies required by `L`:mathit:.

The meaning term of the conclusion formula of ex38_, |psi| is not applied directly to |phi|.  It is applied to a term that is generated by adding |lambda|\-abstractions of each meaning term of an glue formula indexed by an index in `L`:mathit:\ .  It is important to maintain the order of the elements of since the order of the abstractions does matter.  When `n=0`:mathit:\ , |lambda|\  `vi`:mathit:\ :subscript:`1`\ , |dots|\ , |lambda|\ `vi`:mathit:\ :subscript:`n`\ .\ |phi| is simply |phi|\ .

The example below demonstrates how the NLTK handles horn clause applications:

    >>> from nltk_contrib.gluesemantics import glue
    >>> a_man = glue.GlueFormula(r'\Q.exists x.(man(x) & Q(x))', '((g -o G) -o G)')
    >>> walks = glue.GlueFormula(r'\x.walks(x)', '(g -o f)')
    >>> from nltk.internals import Counter
    >>> counter = Counter()
    >>> amc = a_man.compile(counter)
    >>> g1 = amc[0]
    >>> g2 = amc[1]
    >>> g3 = walks.compile(counter)[0]
    >>> g1
    v1 : g : {1} 
    >>> g2
    \Q.exists x.(man(x) & Q(x)) : (G[1] -o G) : {2} 
    >>> g3
    \x.walks(x) : (g -o f) : {3} 
    >>> g13 = g3.applyto(g1)
    >>> g13
    \x.walks(x)(v1) : (g -o f)(g) : {1, 3} 
    >>> g13.simplify()
    walks(v1) : f : {1, 3} 
    >>> g123 = g2.applyto(g13)
    >>> g123
    (\Q.exists x.(man(x) & Q(x)))(\v1.\x.walks(x)(v1)) : (G[1] -o G)((g -o f)(g)) : {1, 2, 3}
    >>> g123.simplify()
    exists x.(man(x) & walks(x)) : f : {1, 2, 3}

Machine Derivation
~~~~~~~~~~~~~~~~~~

The algorithm we will use to have the computer automatically assemble glue proofs is from [Lev07]_.  The algorithm starts with a list of compiled glue formulas, called the `agenda`:mathit:.  When it begins, it initializes two dictionaries, one to hold atomic formulas, and the other to hold non-atomic formulas (implications).  The algorithm then iterates as follows:

.. _machineDeductionAlg:
.. ex::
    | While the agenda is not empty, remove an element `cur`:mathit:\ .
    | |tab| If `cur`:mathit: is non-atomic:
    | |tab| |tab| For each formula `atomic`:mathit: in the atomics dictionary that `cur`:mathit: can be applied to:
    | |tab| |tab| |tab| Apply `cur`:mathit: to `atomic`:mathit: and place the result in the `agenda`:mathit:
    | |tab| |tab| Place `cur`:mathit: in the nonatomics dictionary
    | |tab| Else `cur`:mathit: is atomic:
    | |tab| |tab| For each formula `nonatomic`:mathit: in the nonatomics dictionary that can be applied to `cur`:mathit:\ :
    | |tab| |tab| |tab| Apply `nonatomic`:mathit: to `cur`:mathit: and place the result in the `agenda`:mathit:
    | |tab| |tab| Place `cur`:mathit: in the atomics dictionary
    | Return the list of elements in the dictionaries with a complete set of indices


The algorithm is given as python code in machineDeductionCode_\ .  The argument passed to the function ``get_readings()`` is a list of compiled glue formulas.

.. _machineDeductionCode:
.. ex::
    **Machine Deduction Code**

    >>> def get_readings(agenda):
    ...     readings = []
    ...     agenda_length = len(agenda)
    ...     atomics = dict()
    ...     nonatomics = dict()
    ...     while agenda: # is not empty
    ...         cur = agenda.pop()
    ...         # if agenda.glue is non-atomic
    ...         if isinstance(cur.glue.simplify(), linearlogic.ApplicationExpression):
    ...             for key in atomics:
    ...                 if cur.glue.simplify().first.second.can_unify_with(key, cur.glue.varbindings):
    ...                     for atomic in atomics[key]:
    ...                         if cur.indices.intersection(atomic.indices):
    ...                             continue
    ...                         else: # if the sets of indices are disjoint
    ...                             try:
    ...                                 agenda.append(cur.applyto(atomic))
    ...                             except linearlogic.LinearLogicApplicationError:
    ...                                 pass
    ...             try:
    ...                 nonatomics[cur.glue.simplify().first.second].append(cur)
    ...             except KeyError:
    ...                 nonatomics[cur.glue.simplify().first.second] = [cur]
    ... 
    ...         else: # else agenda.glue is atomic
    ...             for key in nonatomics:
    ...                 for nonatomic in nonatomics[key]:
    ...                     if cur.glue.simplify().can_unify_with(key, nonatomic.glue.varbindings):
    ...                         if cur.indices.intersection(nonatomic.indices):
    ...                             continue
    ...                         else: # if the sets of indices are disjoint
    ...                             try:
    ...                                 agenda.append(nonatomic.applyto(cur))
    ...                             except linearlogic.LinearLogicApplicationError:
    ...                                 pass
    ...             try:
    ...                 atomics[cur.glue.simplify()].append(cur)
    ...             except KeyError:
    ...                 atomics[cur.glue.simplify()] = [cur]
    ...                 
    ...     for entry in atomics:
    ...         for gf in atomics[entry]:
    ...             if len(gf.indices) == agenda_length:
    ...                 readings.append(gf.meaning)
    ...     for entry in nonatomics:
    ...         for gf in nonatomics[entry]:
    ...             if len(gf.indices) == agenda_length:
    ...                 readings.append(gf.meaning)
    ...     return readings


Modifiers
~~~~~~~~~

Horn clauses can be classified into two groups.  The formulas in the first group are skeletons.  As we have mentioned earlier, these are of  the form "skeletons", which are of the form (\ `g`:mathit:\ :subscript:`1` |multimap| (\ `g`:mathit:\ :subscript:`2` |multimap| (\ |dots|  |multimap| f))) where `g`:mathit:\ :subscript:`i` and `f`:mathit: are propositions and `f`:mathit: is not equal to any `g`:mathit:\ :subscript:`i`.   The formulas in the second group are **modifiers**\ .  These are linear logic formulas of the form (\ `A`:mathit:\ |multimap| `A`:mathit:\ )\ , where `A`:mathit: is some linear logic formula.  

The distinction between skeletons and modifiers are important because for a given set of premises, modifiers do not affect provability of a set of premises.  For example, given the premises `g`:mathit:\ , `(g`:mathit: |multimap| `g)`:mathit:\ , and `(g`:mathit: |multimap| `f)`:mathit:\ , we can see that the modifier in mod2_ can not make or break the provability of the proof because it takes a linear logic term we already have,  `g`:mathit:\ , and returns an identical term.  Therefore, according to [GL98]_\ , we may remove all modifiers (as in mod1_\ ) if our goal is just to see if the glue premises may be assembled or to generate a basic reading.  
 
.. _modifiers:
.. ex::

    .. _mod2:
    .. ex::
        .. image:: images/proof_mod2.png
 
    .. _mod1:
    .. ex::
        .. image:: images/proof_mod1.png
    
The advantage to removing modifiers is an decrease in the time it takes to find proofs.  This advantage is made even more obvious in a situation where many modifiers exist that are modifying the same thing.  In examples mod2_\ -\ mod1_ there was no difference in the number of proofs.  However, if we add another glue formula with the glue term `(g`:mathit: |multimap| `g)`:mathit:  then the  number of proofs increases to two.  If we add a third `(g`:mathit: |multimap| `g)`:mathit: then the number of proofs increases to six.  The number of possible proofs is `n!`:mathit: for `n`:mathit:  similar modifiers.

This large increase in number of proofs does not necessarily correspond to an increase in the number of different readings.  After all, logically the sentences `The big, grey cat`:lx: and `The grey, big cat`:lx: are the same, and therefore, the extra time spent generating both readings is not necessary.  

---------------
Further Reading
---------------

See http://users.ox.ac.uk/~lina1301/GlueBibliography.htm for a
comprehensive bibliography of glue semantics literature.

----------
References
----------

.. [Dal01] Mary Dalrymple. *Lexical Functional Grammar*, volume 34 of *Syntax and Semantics*. Academic Press, New York, 2001.

.. [GL98] Vineet Gupta and John Lamping. Efficient linear logic meaning assembly. In *Proc. of COLING/ACL98*, 1998.

.. [Lev07] Iddo Lev. *Packed Computation of Exact Meaning Representations*. PhD thesis, Stanford University,2007.

---------------------------------------------------------------------------------------------------------------------------------

.. [#capitals] We will always use capital letters to distinguish linear logic variables.
.. [#fresh] The index `i`:mathit: in the proof must always be fresh to ensure uniqueness
.. [#hornclauses] We must also move through the formula recursively to ensure that all of its subformulas are also horn clauses.
