Using the prover and parser - Example 1. Conventional implicatures.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "# Conventional implicatures\n",
    "\n",
    "In this notebook we will explore how to construct a lexicon that includes expressions conveying some form of conventional implicature. Let's start right away with a simple example involving an expletive like *fucking*. Let's see how we can get an analysis for a simple sentence such as *John loves fucking McDonald's*. As usual we start by importing the necessary theorem prover code:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from mb.tp import *"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Then we are going to define a simple set of resources. *John*, *McDonald's* and *loves* will have be represented with resources having their standard semantic types that we are used to:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "e_type = AtomicType('e')\n",
    "t_type = AtomicType('t')\n",
    "john = Atom('j', e_type)\n",
    "mcdonalds = Atom('m', e_type)\n",
    "loves = mcdonalds ** john ** Atom('l', t_type)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The expletive *fucking* will be represented by a resource of type $e \\rightarrow \\lozenge e$, basically attaching to the sentence a side-comment related to its argument (McDonald's) and returning its argument untouched for the at-issue component of meaning:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fucking = mcdonalds ** Monad(mcdonalds, 'ci')\n",
    "goal = Monad(Atom('l', t_type), 'ci')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "``goal`` is the resource corresponding to the meaning of a sentence with both the at-issue and the side-issue material. Here we use the ``ci`` modality. While it's not important in this case, when we will analyse different types of side-effecting expressions interacting this will allow us to separate the various semantic contributions. Now we can ask the theorem prover to construct the readings (in this case a single one) associated with the sentence:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from mb.lambda_calc import Const\n",
    "s = Sequent([john, loves, fucking, mcdonalds], goal)\n",
    "proofs = prove(s, [Const('john'), Const('love'), Const('fucking'), Const('McD')])\n",
    "proofs.group_proofs()\n",
    "proofs.show(True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next let us consider a slightly more complicated example with an appositive: *John Lee Hooker, the bluesman from Tennessee, appeared in The Blues Brothers*. For this example we are going to use the categorial grammar parser by defining the appropriate syntactic types and binding them to the meanings using a ``Lexicon`` object. First we import the necessary material:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from mb.cg import *\n",
    "from mb.lambda_calc import *"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "And then we define the syntactic types and the lexicon:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "np = Atom('np', AtomicType('e'))\n",
    "s = Atom('s', AtomicType('t'))\n",
    "n = Atom('n', AtomicType('n'))\n",
    "lexicon = Lexicon()\n",
    "lexicon.add_entry('JLH', np, Const('jlh'))\n",
    "lexicon.add_entry('the', (np >> s) << n, Var('x') ^ Var('x'))\n",
    "lexicon.add_entry('bluesman', n, Const('bluesman'))\n",
    "lexicon.add_entry('from', (n >> n) << np, Var('x') ^ (Var('P') ^ (Var('y') ^ (Const('AND')(Var('P')(Var('y')))(Const('from')(Var('y'))(Var('x'))))))) \n",
    "lexicon.add_entry('Tennessee', np, Const('Tennessee'))\n",
    "lexicon.add_entry('appeared_in', (np >> s) << np, Var('x') ^ (Var('y') ^ (Const('appeared_in')(Var('y'))(Var('x')))))\n",
    "lexicon.add_entry('TBB', np, Const('tbb'))\n",
    "lexicon.add_entry(',', (np >> Monad(np, 'ci')) << (np >> s), Var('P') ^ (Var ('x') ^ ((Const('WRITE')(Var('P')(Var('x')))) ** (Var('y') ^ Unit(Var('x'))))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we can do a proof for the sentence (notice that we have to make some orthographical modifications to make it palatable for the parser, such as having just one comma and joining *appeared in* into a single word token):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "proofs = prove_sentence('JLH , the bluesman from Tennessee appeared_in TBB', Monad(s, 'ci'), lexicon)\n",
    "proofs.show(True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "(Notice that the proof is quite wide so you may have to scroll right to admire it in its entirety)."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}