.. -*- 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


===============================
Discourse Representation Theory
===============================

:Author: Daniel H. Garrette

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

This chapter discusses Discourse Representation Theory (DRT), which is used for the 
representation of semantic information.  

----------------------------------
Discourse Representation Structure
----------------------------------

The main component of DRT is the Discourse Representation Structure (DRS).  A DRS
consists of two parts: the set of **discourse referents** and the set of **conditions**.
The discourse referents are variables representing all of the entities in the DRS.
The conditions are the logical statements about these entities.  For example, the 
following DRS represents the sentence `a man walks`:lx:\ :

.. _drs1:
.. ex::
	.. image:: images/drs1.png
	
DRS conditions may take several different forms:  

* `(R x`:mathit:\ :subscript:`1`\ `, ..., x`:mathit:\ :subscript:`n`\ `)`:mathit:\ , where `R`:mathit: is a first-order relation and `x`:mathit:\ :subscript:`1`\ `, ..., x`:mathit:\ :subscript:`n` are discourse referents 

* `K`:mathit:\ , where `K`:mathit: is a DRS

* `(not K)`:mathit:\ , where `K`:mathit: is a DRS

* `(K`:mathit:\ :subscript:`1` `implies K`:mathit:\ :subscript:`2` `)`:mathit:, where `K`:mathit:\ :subscript:`1` and `K`:mathit:\ :subscript:`2` are DRSs

* `(K`:mathit:\ :subscript:`1` `or K`:mathit:\ :subscript:`2` `)`:mathit:, where `K`:mathit:\ :subscript:`1` and `K`:mathit:\ :subscript:`2` are DRSs

* `(x = y)`:mathit:\ , where `x`:mathit: and `y`:mathit: are discourse referents

Discourse Representation Structures in NLTK
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

In NLTK, Discourse Representation Structures can be created as follows:

	>>> from nltk_contrib.drt import DRT
	>>> d = DRT.Parser().parse(r'DRS([x],[(man x), (walks x)])')
	>>> print d
	DRS([x],[(man x),(walks x)])
	
Notice that a DRS is predicated by `DRS`:mathit:\ , which takes two lists as arguments:
a list of discourse referents and a list of DRS conditions.  The demo function 
`DRT.demo()`:mathit: displays a list of example DRSs that demonstrate various 
functionalities such as |lambda|\-DRSs and DRS concatenations.
	
Additionally, the instance method `draw()`:mathit: of a DRS will open a window with a 
graphical representation of that DRS.  So, as a continuation of the previous block of
code, if we type the following:

	>>> d.draw()
	
A window will appear with the following image:

.. image:: images/gui_drs1.png
	
DRS Concatenation
~~~~~~~~~~~~~~~~~

This allows us to combine multiple DRSs.  We will use the symbol "\ `+`:mathit:\ " to 
concatenate DRSs.  Concatenation is performed by adding the 
sets of discourse referents and adding the sets of conditions to produce the 
sets of discourse referents and conditions for the resultant DRS.  For example,
the concatenation in concat1_ results in the DRS in concat2_\ . 

.. _concat1:
.. ex::
	.. image:: images/concat1.png

.. _concat2:
.. ex::
	.. image:: images/concat2.png

The following example shows the concatenation of two DRSs in NLTK:

	>>> a = DRT.Parser().parse(r'DRS([x],[(man x), (walks x)])')
	>>> b = DRT.Parser().parse(r'DRS([y],[(woman y), (stops y)])')
	>>> (a+b).simplify().infixify()
	DRS([x,y],[(man x),(walks x),(woman y),(stops y)])

Accessibility
~~~~~~~~~~~~~

The concept of accessibility is a critical one to DRT.  Accessibility determines which
discourse referents may be used by particular DRS conditions: if DRS `A`:mathit: is 
accessible from DRS `B`:mathit:\ , then the conditions of DRS `B`:mathit: may contain 
any discourse referent of DRS `A`:mathit:\ .  

DRS `K`:mathit:\ :subscript:`1` is accessible from DRS `K`:mathit:\ :subscript:`2` when:

* `K`:mathit:\ :subscript:`2` is a DRS-condition of `K`:mathit:\ :subscript:`1`

* `(not K`:mathit:\ :subscript:`2` `)`:mathit: is a DRS-condition of `K`:mathit:\ :subscript:`1`

* `(K`:mathit:\ :subscript:`2` `or K`:mathit:\ :subscript:`3` `)`:mathit: is a DRS-condition of `K`:mathit:\ :subscript:`1`\ , for any DRS `K`:mathit:\ :subscript:`3`

* `(K`:mathit:\ :subscript:`3` `or K`:mathit:\ :subscript:`2` `)`:mathit: is a DRS-condition of `K`:mathit:\ :subscript:`1`\ , for any DRS `K`:mathit:\ :subscript:`3`

* `(K`:mathit:\ :subscript:`1` `implies K`:mathit:\ :subscript:`2` `)`:mathit:

* There is a DRS `K`:mathit:\ :subscript:`3` such that `K`:mathit:\ :subscript:`1` is accessible from `K`:mathit:\ :subscript:`3` and `K`:mathit:\ :subscript:`3` is accessible from `K`:mathit:\ :subscript:`2`

Less formally, if we think about the graphical representations of DRSs then we can say that a DRS 
is accessible to any DRS that it encloses, that the left side of an implication is accessible from
the right, and that the accessibility relationship is transitive.

-------------------------
DRT and First Order Logic
-------------------------

DRT and First Order Logic represent the exact same set logical formulas.  This allows 
us to convert between the two types of representations.  The following is the algorithm
for converting a DRS into an expression in first order logic:

* `(K`:mathit:\ :subscript:`1` `implies K`:mathit:\ :subscript:`2` `)`:mathit:, where `K`:mathit:\ :subscript:`1` and `K`:mathit:\ :subscript:`2` are DRSs

* `(K`:mathit:\ :subscript:`1` `or K`:mathit:\ :subscript:`2` `)`:mathit:, where `K`:mathit:\ :subscript:`1` and `K`:mathit:\ :subscript:`2` are DRSs


.. _drtToFolAlg:
.. ex::
	**DRT to First Order Logic Conversion Algorithm**

	| **function** ``toFol(`` `K`:mathit: ``)``\ , where `K`:mathit: is a DRS
	| |tab| `accumulator`:mathit: = the first DRS-condition in `K`:mathit:
	| |tab| for each additional DRS-condition `c`:mathit: in `K`:mathit:
	| |tab| |tab| `accumulator`:mathit: = ( `accumulator`:mathit: and ``toFol(`` `c`:mathit: ``)`` )
	| |tab| for each discourse referent `r`:mathit: in `K`:mathit:
	| |tab| |tab| `accumulator`:mathit: = some `r`:mathit:\ .( `accumulator`:mathit: ) 
	| |tab| **return** `accumulator`:mathit:

	| **function** ``toFol(`` (not `K`:mathit:\ ) ``)``\ , where `K`:mathit: is a DRS
	| |tab| **return** (not ``toFol(`` `K`:mathit: ``)``\ )

	| **function** ``toFol(`` (\ `K`:mathit:\ :subscript:`1` implies `K`:mathit:\ :subscript:`2`\ ) ``)``\ , where `K`:mathit:\ :subscript:`1` and `K`:mathit:\ :subscript:`2` are DRSs
	| |tab| `accumulator`:mathit: = the first DRS-condition in `K`:mathit:\ :subscript:`1`
	| |tab| for each additional DRS-condition `c`:mathit: in `K`:mathit:
	| |tab| |tab| `accumulator`:mathit: = ( `accumulator`:mathit: and ``toFol(`` `c`:mathit: ``)`` )
	| |tab| `accumulator`:mathit: = ( `accumulator`:mathit: implies ``toFol(`` `K`:mathit:\ :subscript:`2` ``)`` )
	| |tab| for each discourse referent `r`:mathit: in `K`:mathit:\ :subscript:`1`
	| |tab| |tab| `accumulator`:mathit: = all `r`:mathit:\ .( `accumulator`:mathit: ) 
	| |tab| **return** `accumulator`:mathit:

	| **function** ``toFol(`` (\ `K`:mathit:\ :subscript:`1` or `K`:mathit:\ :subscript:`2`\ ) ``)``\ , where `K`:mathit:\ :subscript:`1` and `K`:mathit:\ :subscript:`2` are DRSs
	| |tab| **return** (\ ``toFol(`` `K`:mathit:\ :subscript:`1` ``)`` or ``toFol(`` `K`:mathit:\ :subscript:`2` ``)``\ )

	| **function** ``toFol(`` (\ `x`:mathit: = `y`:mathit:\ ) ``)``\ , where `x`:mathit: and `y`:mathit: are discourse referents
	| |tab| **return** (\ `x`:mathit: = `y`:mathit:\ )

	| **function** ``toFol(`` (\ `R x`:mathit:\ :subscript:`1`\ `, ..., x`:mathit:\ :subscript:`n`\ ) ``)``\ , where `R`:mathit: is a first-order relation and `x`:mathit:\ :subscript:`1`\ `, ..., x`:mathit:\ :subscript:`n` are discourse referents
	| |tab| **return** (\ `R x`:mathit:\ :subscript:`1`\ `, ..., x`:mathit:\ :subscript:`n`\ )

In NLTK, the ``toFol()`` method can be used on a DRS to return its first order logic representation:

	>>> print DRT.Parser().parse(r'DRS([x],[(man x), (walks x)])').toFol()
	some x.(and (man x) (walks x))
	>>> print DRT.Parser().parse(r'DRS([],[(DRS([x],[(man x)]) implies DRS([],[(walks x)]))])').toFol()
	all x.(implies (man x) (walks x))

-------------------
Anaphora Resolution
-------------------

Consider the discourse in anaphora1sent_ and its DRS representation in anaphora1_ below:

.. _anaphora1sent:
.. ex::
	`John is a man.  He walks.`:lx:

.. _anaphora1:
.. ex::
	.. image:: images/anaphora1.png
	
In the DRS, the discourse referent `y`:mathit: represents the individual identified by `He`:lx: and 
`(PRO y)`:mathit: is a placeholder for the resolution of `y`:mathit:\ .  The process of anaphora
resolution is therefore the replacement of `(PRO y)`:mathit: with an expression equating `y`:mathit: with a *suitable* 
antecedent to `y`:mathit:\ .
The nature of DRT makes the process of finding this suitable antecedent simpler.  For an anaphor that appears in a DRS, 
its antecedent will be a discourse referent from its own DRS or any accessible DRS.  In this case, the only
suitable antecedent is `x`:mathit: and so anaphora1_ is resolved to anaphora1res_\ , where the discourse
referents `x`:mathit: and `y`:mathit: are equal, meaning that they refer to the same individual.  Thus, `He`:lx: refers
to the individual `John`:lx:\ . 
	
.. _anaphora1res:
.. ex::
	.. image:: images/anaphora1_res.png
	
Anaphora Resolution in NLTK
~~~~~~~~~~~~~~~~~~~~~~~~~~~

In NLTK, the `resolve_anaphora()`:mathit: method replaces a formula of the form `(PRO y)`:mathit: with
and expression equating `y`:mathit: with a list of all possible antecedents of `y`:mathit:\ .

	>>> a = DRT.Parser().parse(r'DRS([x,y],[(x = John), (man x), (PRO y), (walks y)])')
	>>> a.resolve_anaphora().infixify()
	DRS([x,y],[(x = John),(man x),(y = [x]),(walks y)])
	
Multiple Possible Resolutions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The discourse in anaphora2sent_ introduces multiple individuals.  The proper noun `John`:lx: in the first
sentence introduces one individual and the phrase `Every man`:lx: in the second sentence introduces more. 
The pronoun `He`:lx: can refer to either `John`:lx: or to `Every man`:lx:\ .    

.. _anaphora2sent:
.. ex::
	`John smiles.  Every man knows that he is happy.`:lx:

The DRS for this discourse is shown below in anaphora2_\ .

.. _anaphora2:
.. ex::
	.. image:: images/anaphora2.png

The DRS structure shows that both `John`:lx: and `Every man`:lx: are suitable candidates because both
discourse referents `x`:mathit: and `y`:mathit: are accessible from `(PRO z)`:mathit:\ .

.. _anaphora2res:
.. ex::
	.. image:: images/anaphora2_res.png

No Possible Resolutions
~~~~~~~~~~~~~~~~~~~~~~~

The property of accessibility correctly prevents anaphora binding in unresolvableAnaphora1_\ :

.. _unresolvableAnaphora1:
.. ex::
	No one walks.  He is tired.
	
The pair of sentences is expressed in DRS as unresolvableAnaphora2_\ :
	
.. _unresolvableAnaphora2:
.. ex::
	.. image:: images/unresolvable1.png

While `x`:mathit: is a discourse referent, it is not accessible to `(PRO y)`:mathit: 
and therefore cannot be used as a possible antecedent to `y`:mathit:\ .  This is demonstrated in 
the following code.  Notice that the list of possible antecedents for `y`:mathit: is empty since
there are no viable antecedents.

	>>> b = DRT.Parser().parse(r'DRS([y],[(not DRS([x],[(walks x)])),(PRO y),(tired y)])')
	>>> b.resolve_anaphora().infixify()
	DRS([y],[(not DRS([x],[(walks x)])),(y = []),(tired y)])
	
----------------
Building the DRS
----------------

DRT allows us to continually incorporate new information into a DRS as a discourse 
progresses.  We start with a **blank DRS**, which is a DRS that contains no referents 
no conditions.  Each time a sentence is uttered, a DRS representation for it is generated,
and that DRS is concatenated to the whole.  Anaphora resolution takes place after a sentence
is concatenated so that its anaphora may be bound to any accessible discourse referent from
any previous sentence.

A DRS Building Example
~~~~~~~~~~~~~~~~~~~~~~

To demonstrate will we build a representation of the following simple discourse:

`John walks.  Bill sees Him.  He stops.`:lx: 

We start with a blank DRS:

.. _building0:
.. ex::
	.. image:: images/building0.png

Then we create a representation of the first sentence and concatenate it to the whole (which is blank now).

.. _building1:
.. ex::
	.. image:: images/building1.png

This DRS has no anaphora to be resolved so we can create a representation of the second sentence and 
concatenate it to the whole.

.. _building2:
.. ex::
	.. image:: images/building2.png

Now we must resolve the anaphor `He`:lx:\ .  The only possible antecedent to `He`:lx: is `John`:lx: because
`He`:lx: is not reflexive and therefore cannot resolve to `Bill`:lx:\ , the subject of the sentence.  So,
we write `(z = x)`:mathit: to show that `He`:lx: and `John`:lx: describe the same individual.

.. _building2_res:
.. ex::
	.. image:: images/building2_res.png

Next we build the representation of the third sentence and concatenate that to the whole.

.. _building3:
.. ex::
	.. image:: images/building3.png

When we attempt to resolve the final anaphor, `w`:mathit:\, we find that there are three possible antecedents, 
`x`:mathit:\ , `y`:mathit:\ , and `z`:mathit:\ .

.. _building3_res:
.. ex::
	.. image:: images/building3_res.png
	
Since we have already determined that `z`:mathit: resolves to `x`:mathit: these three discourse referents 
actually refer to only two individuals.  Therefore, the final `He`:lx: refers to either `John`:lx: or `Bill`:lx:\ .

----
Demo
----

The following code triggers a demo application that will allow you to browse the possible readings of various sentences, 
drawn as DRSs.  

Also note the option in the Options menu to remove duplicate readings.  Turning this option on will track down logically
equivalent readings and remove all but one of them.  It uses the Prover9 theorem prover, which must be installed for this
feature to work.

>>> from nltk_contrib.gluesemantics import drt_glue_demo
>>> drt_glue_demo.demo()

.. image:: images/gui.png

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

Asher, Nicholas and Alex Lascarides (2003). *Logics of Conversation*. Cambridge University Press.

Kamp, Hans and Uwe Reyle (1993). *From Discourse to the Lexicon: Introduction to Modeltheoretic Semantics of Natural Language, Formal 
Logic and Discourse Representation Theory*. Kluwer Academic Publishers.

