{
 "metadata": {
  "name": ""
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Lamb demo v. 0.6.1, Last updated Sep 10, 2013\n",
      "\n",
      " * 0.5: first version\n",
      " * 0.6: updated to work with refactored class hierarchy (Apr 2013)\n",
      " * 0.6.1: small fixes to adapt to changes in various places (Sep 2013"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "# load some classes and then put some convenience names into the local namespace\n",
      "import lamb\n",
      "from lamb import *\n",
      "from lamb.tree_mini import Tree\n",
      "from lamb.utils import *\n",
      "import imp\n",
      "#imp.reload(lamb)\n",
      "#imp.reload(lang)\n",
      "from lamb.types import TypeMismatch, type_e, type_t, type_property\n",
      "from lamb.lang import te\n",
      "from lamb.utils import ltx_print\n",
      "from lamb.meta import TypedTerm, TypedExpr, LFun, CustomTerm"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "warning: coerced guessed type t for 'Cat' into <e,t>, to match argument 'x'\n",
        "warning: coerced guessed type t for 'Gray' into <e,t>, to match argument 'x'\n",
        "warning: coerced guessed type t for 'In' into <e,t>, to match argument 'y'\n",
        "warning: coerced guessed type t for 'In(y)' into <e,t>, to match argument 'x'\n"
       ]
      }
     ],
     "prompt_number": 1
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "# it will become clear what this does later\n",
      "lamb.meta.constants_use_custom(False)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 2
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "# Two problems in formal semantics #\n",
      "\n",
      "1. Grammar fragments as in Montague Grammar: good idea in principle, hard to use in practice.\n",
      "2. Type-driven computation could be a lot easier to visualize and check.  (Q: could it be made too easy?)\n",
      "\n",
      "Solution: a system for developing interactive fragments: \"*lamb*\"\n",
      "\n",
      "* Creator can work interactively with analysis -- accelerate development, limit time spent on tedious details.\n",
      "* Reader can explore derivations in ways that are not typically possible in typical paper format.\n",
      "* Creator and reader can be certain that derivations work, verified by the system.\n",
      "\n",
      "Inspired (to some degree) by interactive/automatic proof assistants such as _agda_ and _coq_.  In the python world, _SymPy_ provides some of this functionality but has very little overlap with what is needed for formal semantics.\n",
      "\n",
      "### Grammar fragments: pros and cons ###\n",
      "\n",
      "Pros:\n",
      "\n",
      "* Require writer to set out a complete set of assumptions.\n",
      "* What are the stipulations?  (E.g. Stump's diss: turns out that distinction between weak and strong is syntactic.)\n",
      "  * No need to read between the lines / fill in assumptions.  Even a textbook like Heim and Kratzer doesn't always achieve this degree of detail.  Ex: Kratzer and Shimoyama's Alternative Semantics.\n",
      "* Serve as a kind of certificate of validity.\n",
      "* Can allow text of paper to focus on ideas, not as much on example derivations etc.  (Ex: Elbourne's book.)\n",
      "\n",
      "Cons:\n",
      "\n",
      "* Difficult to impossible to use, for readers who are not deeply embedded in a very particular set of assumptions.\n",
      "  * Error in a fragment may remain undetected?  Note, I don't have any cases of this in mind and hesitate to really take on this task.\n",
      "* Historically, tied to a very different view of syntax.  (Not everyone would take this as a con...)\n",
      "* More generally: not modular.  Typically, cannot easily take pieces without a _tremendous_ amount of work.\n",
      "\n",
      "Some solutions exist, but are not widely known / adopted, and are ad-hoc to varying degrees.\n",
      "\n",
      "* John Hale's LF code for implementing QR in ML.  (Where I first encountered the idea.)\n",
      "* UPenn teaching tool for compositional semantics (not designed for working semanticist, not currently in development)\n",
      "* Book: van Eijck and Unger 2010, *Computational semantics with functional programming*\n",
      "  * Implementation of type-driven composition + some syntax in Haskell.\n",
      "  * Use Haskell itself for most of the inference.  (This is what Haskell is good for after all.)  But, Haskell, is not widely known / used.\n",
      "  * Centered more around understanding the programming task / implementation, than producing the kind of tool I'm aiming at.\n",
      "  * Possible seminar in spring, if I can get enough people interested?\n"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "## Part 1: an interface using ipython notebook ##\n",
      "\n",
      " * Client-server system where an ipython \"kernel\" is running in the background.\n",
      " * Page broken down into cells in which can be entered python code, markdown code, or raw text\n",
      " * ipython provides frameworks for graphical representations of python objects in this kind of setup\n",
      " * most importantly, notebook uses the \"MathJax\" framework to enable it to render most math-mode latex\n",
      "\n",
      "This all basically worked off-the-shelf, all I had to do was write the latex/html code that gets handed off to mathjax!"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "meta.pmw_test1._repr_latex_()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "text": [
        "'$\\\\lambda{} p_{t} \\\\: . \\\\: \\\\lambda{} x_{e} \\\\: . \\\\: ({P}({x}_{e}) \\\\wedge{} {p}_{t})$'"
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "meta.pmw_test1"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\lambda{} p_{t} \\: . \\: \\lambda{} x_{e} \\: . \\: ({P}({x}_{e}) \\wedge{} {p}_{t})$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 4,
       "text": [
        "(\u03bb p). (\u03bb x). (P(x) & p)"
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "&nbsp;\n",
      "\n",
      "## Part 2: a typed metalanguage ##"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Starting point: a few implementations of things like predicate logic do exist, this is an intro AI exercise sometimes.  I started with the [AIMA python](http://code.google.com/p/aima-python/) _Expr_ class, based on the standard Russell and Norvig AI text.  But, had to scrap most of it.\n",
      "\n",
      "Class _TypedExpr_: parent class for typed expressions\n",
      "\n",
      "* TypedTerm: variables, constants of arbitrary type\n",
      "* BindingOp: operators that bind a single variable\n",
      "  * LFun: lambda expression\n",
      "\n",
      "Many straightforward expressions can be parsed.  Most expressions are created using a call to TypedExpr.factory, which is abbreviate as \"te\" in the following examples."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "te(\"x_e\")"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "${x}_{e}$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 5,
       "text": [
        "x"
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "meta.TypedTerm(\"x\", types.type_e)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "${x}_{e}$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 6,
       "text": [
        "x"
       ]
      }
     ],
     "prompt_number": 6
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Future: IPython cell magic for metalanguage"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Terms: capital letters are constants, lower case are variables.  Some convenience type guessing to make expressions shorter."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "te(\"Cat(x_e)\")"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "warning: coerced guessed type t for 'Cat' into <e,t>, to match argument 'x'\n"
       ]
      },
      {
       "latex": [
        "${Cat}({x}_{e})$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 7,
       "text": [
        "Cat(x)"
       ]
      }
     ],
     "prompt_number": 7
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "x1 = te(\"L x_e: Cat(x)\")\n",
      "x2 = te(\"\u03bbx: Dog(x_e)\")\n",
      "\n",
      "ltx_print(x1, x2)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "warning: coerced guessed type t for 'Cat' into <e,t>, to match argument 'x'\n",
        "warning: coerced guessed type t for 'Dog' into <e,t>, to match argument 'x'\n"
       ]
      },
      {
       "latex": [
        "$\\lambda{} x_{e} \\: . \\: {Cat}({x}_{e})$<br />$\\lambda{} x_{e} \\: . \\: {Dog}({x}_{e})$<br />"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 8,
       "text": [
        "$\\lambda{} x_{e} \\: . \\: {Cat}({x}_{e})$<br />$\\lambda{} x_{e} \\: . \\: {Dog}({x}_{e})$<br />"
       ]
      }
     ],
     "prompt_number": 8
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "cat_term = meta.CustomTerm(\"Cat\", typ=types.type_property)\n",
      "var = te(\"x_e\")\n",
      "cat_term(var)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "${x}_{e} \\text{ is a }{\\rm C {\\small AT}}$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 9,
       "text": [
        "x CAT is a"
       ]
      }
     ],
     "prompt_number": 9
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "(cat_term(var)).type"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$t$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 10,
       "text": [
        "t"
       ]
      }
     ],
     "prompt_number": 10
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "cat_term.type"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\langle{}e,t\\rangle{}$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 11,
       "text": [
        "<e,t>"
       ]
      }
     ],
     "prompt_number": 11
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Various convenience python operators are overloaded:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "(cat_term(var) & te(\"p_t\")) >> te(\"q_t\")"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$(({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {p}_{t}) \\rightarrow{} {q}_{t})$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 12,
       "text": [
        "((x CAT is a & p) >> q)"
       ]
      }
     ],
     "prompt_number": 12
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "cat_fun = meta.LFun(types.type_e, cat_term(var), \"x\")\n",
      "cat_fun"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 13,
       "text": [
        "(\u03bb x). x CAT is a"
       ]
      }
     ],
     "prompt_number": 13
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "cat_fun(te(\"y_e\")) #.reduce()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$[\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}]({y}_{e})$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 14,
       "text": [
        "[(\u03bb x). x CAT is a](y)"
       ]
      }
     ],
     "prompt_number": 14
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "_TypedExpr_ s in general consist of an operator followed by some number of arguments, possibly 0."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "P = TypedTerm(\"P\", types.FunType(type_e, type_t))\n",
      "Q = TypedTerm(\"Q\", types.FunType(type_e, type_t))\n",
      "x = TypedTerm(\"x\", type_e)\n",
      "y = TypedTerm(\"y\", type_e)\n",
      "t = TypedExpr.factory(P, x)\n",
      "t2 = TypedExpr.factory(Q, x)\n",
      "# shorter way: t = te(\"P(x_e)\")\n",
      "\n",
      "ltx_print(P, t2)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "${P}$<br />${Q}({x}_{e})$<br />"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 15,
       "text": [
        "${P}$<br />${Q}({x}_{e})$<br />"
       ]
      }
     ],
     "prompt_number": 15
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "# propositional variable\n",
      "p = TypedTerm(\"p\", type_t)\n",
      "\n",
      "pmw_test1 = LFun(type_t, LFun(type_e, t & p, \"x\"), \"p\")\n",
      "pmw_test1b = LFun(type_e, t & t2, \"x\")\n",
      "\n",
      "ltx_print(pmw_test1, pmw_test1.type,\n",
      "  pmw_test1b, pmw_test1b.type,\n",
      "  t2)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\lambda{} p_{t} \\: . \\: \\lambda{} x_{e} \\: . \\: ({P}({x}_{e}) \\wedge{} {p}_{t})$<br />$\\langle{}t,\\langle{}e,t\\rangle{}\\rangle{}$<br />$\\lambda{} x_{e} \\: . \\: ({P}({x}_{e}) \\wedge{} {Q}({x}_{e}))$<br />$\\langle{}e,t\\rangle{}$<br />${Q}({x}_{e})$<br />"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 16,
       "text": [
        "$\\lambda{} p_{t} \\: . \\: \\lambda{} x_{e} \\: . \\: ({P}({x}_{e}) \\wedge{} {p}_{t})$<br />$\\langle{}t,\\langle{}e,t\\rangle{}\\rangle{}$<br />$\\lambda{} x_{e} \\: . \\: ({P}({x}_{e}) \\wedge{} {Q}({x}_{e}))$<br />$\\langle{}e,t\\rangle{}$<br />${Q}({x}_{e})$<br />"
       ]
      }
     ],
     "prompt_number": 16
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "pmw_test1(t2).reduce()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\lambda{} x1_{e} \\: . \\: ({P}({x1}_{e}) \\wedge{} {Q}({x}_{e}))$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 17,
       "text": [
        "(\u03bb x1). (P(x1) & Q(x))"
       ]
      }
     ],
     "prompt_number": 17
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "pmw_test1(x) # function is type <t<et>>"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "ename": "TypeMismatch",
       "evalue": "Type mismatch: '(\u03bb p). (\u03bb x). (P(x) & p)'/<t,<e,t>> and 'x'/e conflict (mode: Lambda term+arg expression)",
       "output_type": "pyerr",
       "traceback": [
        "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mTypeMismatch\u001b[0m                              Traceback (most recent call last)",
        "\u001b[0;32m<ipython-input-20-ddac926bdda2>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mpmw_test1\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mx\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;31m# function is type <t<et>>\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
        "\u001b[0;32m/Users/advil/Projects/lambda/lamb/meta.py\u001b[0m in \u001b[0;36m__call__\u001b[0;34m(self, *args)\u001b[0m\n\u001b[1;32m   1416\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m   1417\u001b[0m         call + reduce is equivalent to apply, for an LFun\"\"\"\n\u001b[0;32m-> 1418\u001b[0;31m         \u001b[0;32mreturn\u001b[0m \u001b[0mTypedExpr\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m*\u001b[0m\u001b[0margs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m   1419\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m   1420\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0munsafe_variables\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfun\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0marg\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
        "\u001b[0;32m/Users/advil/Projects/lambda/lamb/meta.py\u001b[0m in \u001b[0;36m__init__\u001b[0;34m(self, op, *args)\u001b[0m\n\u001b[1;32m    115\u001b[0m             \u001b[0;31m#if arg.type != op.argtype and not arg.type.undetermined:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    116\u001b[0m             \u001b[0;32mif\u001b[0m \u001b[0munify_f\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0;32mNone\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 117\u001b[0;31m                 \u001b[0;32mraise\u001b[0m \u001b[0mTypeMismatch\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mop\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0marg\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m\"Lambda term+arg expression\"\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;31m#TODO: do I always want to check types here?\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    118\u001b[0m             \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtype\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0munify_r\u001b[0m \u001b[0;31m#op.returntype\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    119\u001b[0m             \u001b[0;31m#TODO is unification here the right thing?\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
        "\u001b[0;31mTypeMismatch\u001b[0m: Type mismatch: '(\u03bb p). (\u03bb x). (P(x) & p)'/<t,<e,t>> and 'x'/e conflict (mode: Lambda term+arg expression)"
       ]
      }
     ],
     "prompt_number": 20
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "&nbsp;\n",
      "\n",
      "## Part 3: composition systems for an object language ##\n",
      "\n",
      " * Focus on type-driven composition, current syntactic implementation fairly minimal\n",
      " * lots more to do here.\n",
      "\n",
      "Key class(/mixin): _Composable_.  Some key subclasses:\n",
      "\n",
      " * _Item_: representation of a lexical item\n",
      " * _BinaryComposite_: result of composing any two _Composables_ using a single composition method.  Inherits from _nltk.Tree_!\n",
      " * _CompositionResult_: result of composing any two _Composables_ -- may represent multiple possible composition paths\n",
      "\n",
      "Key class: _CompositionSystem_.  Describes a set of composition operations.\n",
      "\n",
      "Future key class: _Grammar_.  Describes a composition system along with a lexicon."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def demo_fa_fun(fun, arg, assignment=None):\n",
      "    if (not fun.type.functional()) or fun.type.left != arg.type:\n",
      "        raise TypeMismatch(fun, arg, \"Function Application\")\n",
      "    return lang.BinaryComposite(fun, arg, \n",
      "                (fun.content.under_assignment(assignment)(arg.content.under_assignment(assignment))).reduce())\n",
      "\n",
      "pm_op = lang.te(\"L f_<e,t> : L g_<e,t> : L x_e : f(x) & g(x)\")\n",
      "\n",
      "def demo_pm_fun(fun1, fun2, assignment=None):\n",
      "    \"\"\"H&K predicate modification -- restricted to type <et>.\"\"\"\n",
      "    ts = meta.get_type_system()\n",
      "    if not (ts.eq_check(fun1.type, types.type_property) and \n",
      "            ts.eq_check(fun2.type, types.type_property)):\n",
      "        raise TypeMismatch(fun1, fun2, \"Predicate Modification\")\n",
      "    #if fun1.type != fun2.type or fun1.type != type_property:\n",
      "    #    raise TypeMismatch(fun1, fun2, \"Predicate Modification\")\n",
      "    varname = fun1.content.varname\n",
      "    c1 = fun1.content.under_assignment(assignment)\n",
      "    c2 = fun2.content.under_assignment(assignment)\n",
      "    result = pm_op.apply(c1).apply(c2).reduce_all()\n",
      "    return lang.BinaryComposite(fun1, fun2, result)\n",
      "\n",
      "pm = lang.BinaryCompositionOp(\"PM\", demo_pm_fun, commutative=False)\n",
      "fa = lang.BinaryCompositionOp(\"FA\", demo_fa_fun)\n",
      "pa = lang.BinaryCompositionOp(\"PA\", lang.pa_fun, allow_none=True)\n",
      "demo_hk_system = lang.CompositionSystem(rules=[fa, pm, pa], basictypes={type_e, type_t})\n",
      "lang.set_system(demo_hk_system)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 18
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "#imp.reload(lamb)\n",
      "meta.constants_use_custom(True)\n",
      "cat = lang.Item(\"cat\", \"L x_e: Cat(x)\")\n",
      "gray = lang.Item(\"gray\", \"L x_e: Gray(x)\")\n",
      "gray.content.args[0].op.custom = \"is\"\n",
      "john = lang.Item(\"John\", \"John_e\")\n",
      "julius = lang.Item(\"Julius\", \"Julius_e\")\n",
      "inP = lang.Item(\"in\", \"L x: L y: In(y)(x)\")\n",
      "inP.content.args[0].args[0].op.op.custom = \"is\"\n",
      "texas = lang.Item(\"Texas\", \"Texas_e\")\n",
      "\n",
      "ltx_print(cat,gray, julius, inP, texas)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "warning: coerced guessed type t for 'CAT' into <e,t>, to match argument 'x'\n",
        "warning: coerced guessed type t for 'GRAY' into <e,t>, to match argument 'x'\n",
        "warning: coerced guessed type t for 'IN' into <e,t>, to match argument 'y'\n",
        "warning: coerced guessed type t for 'y IN is a' into <e,t>, to match argument 'x'\n"
       ]
      },
      {
       "latex": [
        "$|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />$|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 19,
       "text": [
        "$|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />$|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />"
       ]
      }
     ],
     "prompt_number": 19
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "#pvar = meta.TypedTerm(\"p\", types.type_property)\n",
      "#isV = lang.Item(\"is\", meta.LFun(types.type_property, pvar, \"p\"))\n",
      "isV = lang.Item(\"is\", lang.te(\"L p_<e,t> : p\"))\n",
      "\n",
      "isV # identity function over properties"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 20,
       "text": [
        "||is|| = (\u03bb p). p"
       ]
      }
     ],
     "prompt_number": 20
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "In the purely type-driven mode, composition is triggered by using the '*' operator on a composable."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "inP * texas"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "1 composition path.  Result:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 21,
       "text": [
        "[BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])]"
       ]
      }
     ],
     "prompt_number": 21
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sentence1 = julius * (isV * (inP * texas))\n",
      "sentence1"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "1 composition path.  Result:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [in Texas]] Julius]}}|\\!|^{}_{t} \\:=\\: $${\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 22,
       "text": [
        "[BinaryComposite(JULIUS IN is(TEXAS), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])]), ||Julius|| = JULIUS])]"
       ]
      }
     ],
     "prompt_number": 22
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sentence1.full_trace_latex()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "Full composition trace.  1 path:<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{[is [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [in Texas]] Julius]}}|\\!|^{}_{t} \\:=\\: $${\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 23,
       "text": [
        "Full composition trace.  1 path:<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{[is [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [in Texas]] Julius]}}|\\!|^{}_{t} \\:=\\: $${\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n"
       ]
      }
     ],
     "prompt_number": 23
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "I have temporarily disabled the fact that standard PM is symmetric, to illustrated multiple composition paths:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "gray * cat"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "2 composition paths. Results:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}})$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 24,
       "text": [
        "[BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a]), BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is])]"
       ]
      }
     ],
     "prompt_number": 24
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "gray * cat * (inP * texas)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "4 composition paths. Results:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[in Texas] [gray cat]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[cat gray] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[in Texas] [cat gray]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}))$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 25,
       "text": [
        "[BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])]), BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a])]), BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])]), BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is])])]"
       ]
      }
     ],
     "prompt_number": 25
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a = lang.Item(\"a\", lang.isV.content) # identity function for copula as well\n",
      "isV * (a * (gray * cat * (inP * texas)))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "4 composition paths. Results:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[is [a [[gray cat] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[is [a [[in Texas] [gray cat]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[is [a [[cat gray] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[is [a [[in Texas] [cat gray]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}))$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 26,
       "text": [
        "[BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])])])]), BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a])])])]), BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])])])]), BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is])])])])]"
       ]
      }
     ],
     "prompt_number": 26
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "np = ((gray * cat) * (inP * texas))\n",
      "vp = (isV * (a * np))\n",
      "sentence2 = julius * vp\n",
      "sentence2"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "4 composition paths. Results:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[gray cat] [in Texas]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$(({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[in Texas] [gray cat]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[cat gray] [in Texas]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$(({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[in Texas] [cat gray]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}}))$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 27,
       "text": [
        "[BinaryComposite(((JULIUS GRAY is & JULIUS CAT is a) & JULIUS IN is(TEXAS)), [BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])])])]), ||Julius|| = JULIUS]), BinaryComposite((JULIUS IN is(TEXAS) & (JULIUS GRAY is & JULIUS CAT is a)), [BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a])])])]), ||Julius|| = JULIUS]), BinaryComposite(((JULIUS CAT is a & JULIUS GRAY is) & JULIUS IN is(TEXAS)), [BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])])])]), ||Julius|| = JULIUS]), BinaryComposite((JULIUS IN is(TEXAS) & (JULIUS CAT is a & JULIUS GRAY is)), [BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is])])])]), ||Julius|| = JULIUS])]"
       ]
      }
     ],
     "prompt_number": 27
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "julius * isV"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "Composition failed.  Attempts:<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Type mismatch: '$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$'/$e$ and '$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$'/$\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}$ conflict (mode: Function Application)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Type mismatch: '$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$'/$\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}$ and '$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$'/$e$ conflict (mode: Function Application)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Type mismatch: '$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$'/$e$ and '$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$'/$\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}$ conflict (mode: Predicate Modification)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Type mismatch: '$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$'/$\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}$ and '$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$'/$e$ conflict (mode: Predicate Modification)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Type mismatch: '$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$'/$e$ and '$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$'/$\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}$ conflict (mode: Predicate Abstraction)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Type mismatch: '$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$'/$\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}$ and '$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$'/$e$ conflict (mode: Predicate Abstraction)<br />\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 32,
       "text": [
        "[]"
       ]
      }
     ],
     "prompt_number": 32
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sentence2.full_trace_latex()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "Full composition trace.  4 paths:<br />\n",
        "Path 1<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 10: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[a [[gray cat] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 11: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[a [[gray cat] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [a [[gray cat] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 12: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 13: $|\\!|\\mathbf{\\text{[is [a [[gray cat] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [a [[gray cat] [in Texas]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$(({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "Path 2<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[[in Texas] [gray cat]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}))$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 10: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[[in Texas] [gray cat]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[a [[in Texas] [gray cat]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 11: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[a [[in Texas] [gray cat]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [a [[in Texas] [gray cat]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 12: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 13: $|\\!|\\mathbf{\\text{[is [a [[in Texas] [gray cat]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [a [[in Texas] [gray cat]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}))$ (by FA)<br />\n",
        "Path 3<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}})$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[[cat gray] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 10: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[[cat gray] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[a [[cat gray] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 11: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[a [[cat gray] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [a [[cat gray] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 12: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 13: $|\\!|\\mathbf{\\text{[is [a [[cat gray] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [a [[cat gray] [in Texas]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$(({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "Path 4<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}})$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[[in Texas] [cat gray]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}))$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 10: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[[in Texas] [cat gray]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[a [[in Texas] [cat gray]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 11: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[a [[in Texas] [cat gray]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [a [[in Texas] [cat gray]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 12: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 13: $|\\!|\\mathbf{\\text{[is [a [[in Texas] [cat gray]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [a [[in Texas] [cat gray]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}}))$ (by FA)<br />\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 28,
       "text": [
        "Full composition trace.  4 paths:<br />\n",
        "Path 1<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 10: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[a [[gray cat] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 11: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[a [[gray cat] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [a [[gray cat] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 12: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 13: $|\\!|\\mathbf{\\text{[is [a [[gray cat] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [a [[gray cat] [in Texas]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$(({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "Path 2<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[[in Texas] [gray cat]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}))$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 10: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[[in Texas] [gray cat]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[a [[in Texas] [gray cat]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 11: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[a [[in Texas] [gray cat]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [a [[in Texas] [gray cat]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 12: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 13: $|\\!|\\mathbf{\\text{[is [a [[in Texas] [gray cat]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [a [[in Texas] [gray cat]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}))$ (by FA)<br />\n",
        "Path 3<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}})$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[[cat gray] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 10: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[[cat gray] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[a [[cat gray] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 11: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[a [[cat gray] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [a [[cat gray] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 12: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 13: $|\\!|\\mathbf{\\text{[is [a [[cat gray] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [a [[cat gray] [in Texas]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$(({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$ (by FA)<br />\n",
        "Path 4<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e} \\:=\\: $${\\rm T {\\small EXAS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}})$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{[cat gray]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[[in Texas] [cat gray]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}))$ (by PM)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 10: $|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[[in Texas] [cat gray]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[a [[in Texas] [cat gray]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 11: $|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{[a [[in Texas] [cat gray]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[is [a [[in Texas] [cat gray]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({x}_{e} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {x}_{e} \\text{ is }{\\rm G {\\small RAY}}))$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 12: $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e} \\:=\\: $${\\rm J {\\small ULIUS}}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 13: $|\\!|\\mathbf{\\text{[is [a [[in Texas] [cat gray]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[is [a [[in Texas] [cat gray]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}}))$ (by FA)<br />\n"
       ]
      }
     ],
     "prompt_number": 28
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sentence1.results[0]"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$|\\!|\\mathbf{\\text{[[is [in Texas]] Julius]}}|\\!|^{}_{t} \\:=\\: $${\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 33,
       "text": [
        "BinaryComposite(JULIUS IN is(TEXAS), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])]), ||Julius|| = JULIUS])"
       ]
      }
     ],
     "prompt_number": 33
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sentence1.results[0].latex_step_tree()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm T {\\small EXAS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[is [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm J {\\small ULIUS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[is [in Texas]] Julius]}}|\\!|^{}_{t}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">${\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 34,
       "text": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm T {\\small EXAS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[is [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm J {\\small ULIUS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[is [in Texas]] Julius]}}|\\!|^{}_{t}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">${\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ]
      }
     ],
     "prompt_number": 34
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sentence2.results[0].latex_step_tree()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm T {\\small EXAS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[a [[gray cat] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[is [a [[gray cat] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm J {\\small ULIUS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[is [a [[gray cat] [in Texas]]]] Julius]}}|\\!|^{}_{t}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$(({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 35,
       "text": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm T {\\small EXAS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[a [[gray cat] [in Texas]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[is [a [[gray cat] [in Texas]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm J {\\small ULIUS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[is [a [[gray cat] [in Texas]]]] Julius]}}|\\!|^{}_{t}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$(({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ]
      }
     ],
     "prompt_number": 35
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "One of the infamous examples from Heim and Kratzer (names different):\n",
      "\n",
      " * Julius is a gray cat in Texas fond of John."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "fond = lang.Item(\"fond\", \"L x_e : L y_e : Fond(y)(x)\")\n",
      "ofP = lang.Item(\"of\", \"L x_e : x\")\n",
      "sentence3 = julius * (lang.isV * (a * (np * (fond * (ofP * lang.john)))))\n",
      "sentence3"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "warning: coerced guessed type t for 'FOND' into <e,t>, to match argument 'y'\n",
        "warning: coerced guessed type t for 'y FOND is a' into <e,t>, to match argument 'x'\n"
       ]
      },
      {
       "latex": [
        "8 composition paths. Results:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[[gray cat] [in Texas]] [fond [of John]]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$((({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[fond [of John]] [[gray cat] [in Texas]]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}) \\wedge{} (({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[[in Texas] [gray cat]] [fond [of John]]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$(({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}})) \\wedge{} {\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[fond [of John]] [[in Texas] [gray cat]]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}})))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[[cat gray] [in Texas]] [fond [of John]]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$((({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[fond [of John]] [[cat gray] [in Texas]]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}) \\wedge{} (({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[[in Texas] [cat gray]] [fond [of John]]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$(({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}})) \\wedge{} {\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[[is [a [[fond [of John]] [[in Texas] [cat gray]]]]] Julius]}}|\\!|^{}_{t} \\:=\\: $$({\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}) \\wedge{} ({\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}})))$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 36,
       "text": [
        "[BinaryComposite((((JULIUS GRAY is & JULIUS CAT is a) & JULIUS IN is(TEXAS)) & JULIUS FOND (John)), [BinaryComposite((\u03bb x). (((x GRAY is & x CAT is a) & x IN is(TEXAS)) & x FOND (John)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (((x GRAY is & x CAT is a) & x IN is(TEXAS)) & x FOND (John)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (((x GRAY is & x CAT is a) & x IN is(TEXAS)) & x FOND (John)), [BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])]), BinaryComposite((\u03bb y). y FOND (John), [||fond|| = (\u03bb x). (\u03bb y). y FOND (x), BinaryComposite(John, [||of|| = (\u03bb x). x, ||John|| = John])])])])]), ||Julius|| = JULIUS]), BinaryComposite((JULIUS FOND (John) & ((JULIUS GRAY is & JULIUS CAT is a) & JULIUS IN is(TEXAS))), [BinaryComposite((\u03bb x). (x FOND (John) & ((x GRAY is & x CAT is a) & x IN is(TEXAS))), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x FOND (John) & ((x GRAY is & x CAT is a) & x IN is(TEXAS))), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x FOND (John) & ((x GRAY is & x CAT is a) & x IN is(TEXAS))), [BinaryComposite((\u03bb y). y FOND (John), [||fond|| = (\u03bb x). (\u03bb y). y FOND (x), BinaryComposite(John, [||of|| = (\u03bb x). x, ||John|| = John])]), BinaryComposite((\u03bb x). ((x GRAY is & x CAT is a) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])])])])]), ||Julius|| = JULIUS]), BinaryComposite(((JULIUS IN is(TEXAS) & (JULIUS GRAY is & JULIUS CAT is a)) & JULIUS FOND (John)), [BinaryComposite((\u03bb x). ((x IN is(TEXAS) & (x GRAY is & x CAT is a)) & x FOND (John)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x IN is(TEXAS) & (x GRAY is & x CAT is a)) & x FOND (John)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x IN is(TEXAS) & (x GRAY is & x CAT is a)) & x FOND (John)), [BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a])]), BinaryComposite((\u03bb y). y FOND (John), [||fond|| = (\u03bb x). (\u03bb y). y FOND (x), BinaryComposite(John, [||of|| = (\u03bb x). x, ||John|| = John])])])])]), ||Julius|| = JULIUS]), BinaryComposite((JULIUS FOND (John) & (JULIUS IN is(TEXAS) & (JULIUS GRAY is & JULIUS CAT is a))), [BinaryComposite((\u03bb x). (x FOND (John) & (x IN is(TEXAS) & (x GRAY is & x CAT is a))), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x FOND (John) & (x IN is(TEXAS) & (x GRAY is & x CAT is a))), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x FOND (John) & (x IN is(TEXAS) & (x GRAY is & x CAT is a))), [BinaryComposite((\u03bb y). y FOND (John), [||fond|| = (\u03bb x). (\u03bb y). y FOND (x), BinaryComposite(John, [||of|| = (\u03bb x). x, ||John|| = John])]), BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x GRAY is & x CAT is a)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x GRAY is & x CAT is a), [||gray|| = (\u03bb x). x GRAY is, ||cat|| = (\u03bb x). x CAT is a])])])])]), ||Julius|| = JULIUS]), BinaryComposite((((JULIUS CAT is a & JULIUS GRAY is) & JULIUS IN is(TEXAS)) & JULIUS FOND (John)), [BinaryComposite((\u03bb x). (((x CAT is a & x GRAY is) & x IN is(TEXAS)) & x FOND (John)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (((x CAT is a & x GRAY is) & x IN is(TEXAS)) & x FOND (John)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (((x CAT is a & x GRAY is) & x IN is(TEXAS)) & x FOND (John)), [BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])]), BinaryComposite((\u03bb y). y FOND (John), [||fond|| = (\u03bb x). (\u03bb y). y FOND (x), BinaryComposite(John, [||of|| = (\u03bb x). x, ||John|| = John])])])])]), ||Julius|| = JULIUS]), BinaryComposite((JULIUS FOND (John) & ((JULIUS CAT is a & JULIUS GRAY is) & JULIUS IN is(TEXAS))), [BinaryComposite((\u03bb x). (x FOND (John) & ((x CAT is a & x GRAY is) & x IN is(TEXAS))), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x FOND (John) & ((x CAT is a & x GRAY is) & x IN is(TEXAS))), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x FOND (John) & ((x CAT is a & x GRAY is) & x IN is(TEXAS))), [BinaryComposite((\u03bb y). y FOND (John), [||fond|| = (\u03bb x). (\u03bb y). y FOND (x), BinaryComposite(John, [||of|| = (\u03bb x). x, ||John|| = John])]), BinaryComposite((\u03bb x). ((x CAT is a & x GRAY is) & x IN is(TEXAS)), [BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is]), BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS])])])])]), ||Julius|| = JULIUS]), BinaryComposite(((JULIUS IN is(TEXAS) & (JULIUS CAT is a & JULIUS GRAY is)) & JULIUS FOND (John)), [BinaryComposite((\u03bb x). ((x IN is(TEXAS) & (x CAT is a & x GRAY is)) & x FOND (John)), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x IN is(TEXAS) & (x CAT is a & x GRAY is)) & x FOND (John)), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). ((x IN is(TEXAS) & (x CAT is a & x GRAY is)) & x FOND (John)), [BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is])]), BinaryComposite((\u03bb y). y FOND (John), [||fond|| = (\u03bb x). (\u03bb y). y FOND (x), BinaryComposite(John, [||of|| = (\u03bb x). x, ||John|| = John])])])])]), ||Julius|| = JULIUS]), BinaryComposite((JULIUS FOND (John) & (JULIUS IN is(TEXAS) & (JULIUS CAT is a & JULIUS GRAY is))), [BinaryComposite((\u03bb x). (x FOND (John) & (x IN is(TEXAS) & (x CAT is a & x GRAY is))), [||is|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x FOND (John) & (x IN is(TEXAS) & (x CAT is a & x GRAY is))), [||a|| = (\u03bb p). p, BinaryComposite((\u03bb x). (x FOND (John) & (x IN is(TEXAS) & (x CAT is a & x GRAY is))), [BinaryComposite((\u03bb y). y FOND (John), [||fond|| = (\u03bb x). (\u03bb y). y FOND (x), BinaryComposite(John, [||of|| = (\u03bb x). x, ||John|| = John])]), BinaryComposite((\u03bb x). (x IN is(TEXAS) & (x CAT is a & x GRAY is)), [BinaryComposite((\u03bb y). y IN is(TEXAS), [||in|| = (\u03bb x). (\u03bb y). y IN is(x), ||Texas|| = TEXAS]), BinaryComposite((\u03bb x). (x CAT is a & x GRAY is), [||cat|| = (\u03bb x). x CAT is a, ||gray|| = (\u03bb x). x GRAY is])])])])]), ||Julius|| = JULIUS])]"
       ]
      }
     ],
     "prompt_number": 36
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "sentence3.results[0].latex_step_tree()\n"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm T {\\small EXAS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{fond}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{  }{\\rm F {\\small OND}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{of}}|\\!|^{}_{\\langle{}e,e\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{John}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${John}_{e}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[of John]}}|\\!|^{}_{e}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">${John}_{e}$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[fond [of John]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[[gray cat] [in Texas]] [fond [of John]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ((({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {x}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[a [[[gray cat] [in Texas]] [fond [of John]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ((({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {x}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[is [a [[[gray cat] [in Texas]] [fond [of John]]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ((({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {x}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm J {\\small ULIUS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[is [a [[[gray cat] [in Texas]] [fond [of John]]]]] Julius]}}|\\!|^{}_{t}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$((({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 38,
       "text": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{is}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{a}}|\\!|^{}_{\\langle{}\\langle{}e,t\\rangle{},\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} p_{\\langle{}e,t\\rangle{}} \\: . \\: {p}_{\\langle{}e,t\\rangle{}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm T {\\small EXAS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{fond}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{  }{\\rm F {\\small OND}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{of}}|\\!|^{}_{\\langle{}e,e\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{John}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${John}_{e}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[of John]}}|\\!|^{}_{e}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">${John}_{e}$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[fond [of John]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[[gray cat] [in Texas]] [fond [of John]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ((({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {x}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[a [[[gray cat] [in Texas]] [fond [of John]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ((({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {x}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[is [a [[[gray cat] [in Texas]] [fond [of John]]]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ((({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {x}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Julius}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm J {\\small ULIUS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[is [a [[[gray cat] [in Texas]] [fond [of John]]]]] Julius]}}|\\!|^{}_{t}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$((({\\rm J {\\small ULIUS}} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {\\rm J {\\small ULIUS}} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {\\rm J {\\small ULIUS}} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ]
      }
     ],
     "prompt_number": 38
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The _Composite_ class subclasses _nltk.Tree_, and so supports the things that class does.  E.g. []-based paths:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "parse_tree3 = sentence3.results[0]\n",
      "parse_tree3[0][1][1].latex_step_tree()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm T {\\small EXAS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{fond}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{  }{\\rm F {\\small OND}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{of}}|\\!|^{}_{\\langle{}e,e\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{John}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${John}_{e}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[of John]}}|\\!|^{}_{e}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">${John}_{e}$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[fond [of John]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[[gray cat] [in Texas]] [fond [of John]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ((({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {x}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 39,
       "text": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{gray}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is }{\\rm G {\\small RAY}}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{cat}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e} \\text{ is a }{\\rm C {\\small AT}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[gray cat]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{Texas}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${\\rm T {\\small EXAS}}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in Texas]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[gray cat] [in Texas]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{fond}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {y}_{e} \\text{  }{\\rm F {\\small OND}}({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{of}}|\\!|^{}_{\\langle{}e,e\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: {x}_{e}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{John}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${John}_{e}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[of John]}}|\\!|^{}_{e}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">${John}_{e}$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[fond [of John]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {y}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[[gray cat] [in Texas]] [fond [of John]]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: ((({x}_{e} \\text{ is }{\\rm G {\\small RAY}} \\wedge{} {x}_{e} \\text{ is a }{\\rm C {\\small AT}}) \\wedge{} {x}_{e} \\text{ is }{\\rm I {\\small N}}({\\rm T {\\small EXAS}})) \\wedge{} {x}_{e} \\text{  }{\\rm F {\\small OND}}({John}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ]
      }
     ],
     "prompt_number": 39
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Some rudimentary support for traces."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "binder = lang.Item(\"23\", None)\n",
      "binder2 = lang.Item(\"5\", None)\n",
      "t = lang.Trace(23, types.type_e)\n",
      "t2 = lang.Trace(5)\n",
      "ltx_print(t, t2, binder)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$|\\!|\\mathbf{\\text{t23}}|\\!|^{}_{e} \\:=\\: $${t23}_{e}$<br />$|\\!|\\mathbf{\\text{t5}}|\\!|^{}_{e} \\:=\\: $${t5}_{e}$<br />$|\\!|\\mathbf{\\text{23}}|\\!|^{}$<br />"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 40,
       "text": [
        "$|\\!|\\mathbf{\\text{t23}}|\\!|^{}_{e} \\:=\\: $${t23}_{e}$<br />$|\\!|\\mathbf{\\text{t5}}|\\!|^{}_{e} \\:=\\: $${t5}_{e}$<br />$|\\!|\\mathbf{\\text{23}}|\\!|^{}$<br />"
       ]
      }
     ],
     "prompt_number": 40
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "((t * gray))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "1 composition path.  Result:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[gray t23]}}|\\!|^{}_{t} \\:=\\: $${t23}_{e} \\text{ is }{\\rm G {\\small RAY}}$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 41,
       "text": [
        "[BinaryComposite(t23 GRAY is, [||gray|| = (\u03bb x). x GRAY is, ||t23|| = t23])]"
       ]
      }
     ],
     "prompt_number": 41
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "b1 = (binder * (binder2 * (t * (lang.inP * t2))))\n",
      "b2 = (binder2 * (binder * (t * (lang.inP * t2))))\n",
      "ltx_print(b1, b2)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "1 composition path.  Result:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[23 [5 [[in t5] t23]]]}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({x1}_{e})({x}_{e})$<br />1 composition path.  Result:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[5 [23 [[in t5] t23]]]}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({x}_{e})({x1}_{e})$<br />"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 44,
       "text": [
        "1 composition path.  Result:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[23 [5 [[in t5] t23]]]}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({x1}_{e})({x}_{e})$<br />1 composition path.  Result:\n",
        "<br />&nbsp;&nbsp;&nbsp;&nbsp;$|\\!|\\mathbf{\\text{[5 [23 [[in t5] t23]]]}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({x}_{e})({x1}_{e})$<br />"
       ]
      }
     ],
     "prompt_number": 44
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "b1.full_trace_latex()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "Full composition trace.  1 path:<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{23}}|\\!|^{}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{5}}|\\!|^{}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({y}_{e})({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{t5}}|\\!|^{}_{e} \\:=\\: $${t5}_{e}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{t5}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in t5]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({y}_{e})({t5}_{e})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{t23}}|\\!|^{}_{e} \\:=\\: $${t23}_{e}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{[in t5]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{t23}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[in t5] t23]}}|\\!|^{}_{t} \\:=\\: $${In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({t23}_{e})({t5}_{e})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{5}}|\\!|^{}$ * $|\\!|\\mathbf{\\text{[[in t5] t23]}}|\\!|^{}_{t}$ leads to: $|\\!|\\mathbf{\\text{[5 [[in t5] t23]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({t23}_{e})({x}_{e})$ (by PA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{23}}|\\!|^{}$ * $|\\!|\\mathbf{\\text{[5 [[in t5] t23]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[23 [5 [[in t5] t23]]]}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({x1}_{e})({x}_{e})$ (by PA)<br />\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 45,
       "text": [
        "Full composition trace.  1 path:<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 1: $|\\!|\\mathbf{\\text{23}}|\\!|^{}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 2: $|\\!|\\mathbf{\\text{5}}|\\!|^{}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 3: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({y}_{e})({x}_{e})$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 4: $|\\!|\\mathbf{\\text{t5}}|\\!|^{}_{e} \\:=\\: $${t5}_{e}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 5: $|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$ * $|\\!|\\mathbf{\\text{t5}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[in t5]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} y_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({y}_{e})({t5}_{e})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 6: $|\\!|\\mathbf{\\text{t23}}|\\!|^{}_{e} \\:=\\: $${t23}_{e}$<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 7: $|\\!|\\mathbf{\\text{[in t5]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ * $|\\!|\\mathbf{\\text{t23}}|\\!|^{}_{e}$ leads to: $|\\!|\\mathbf{\\text{[[in t5] t23]}}|\\!|^{}_{t} \\:=\\: $${In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({t23}_{e})({t5}_{e})$ (by FA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 8: $|\\!|\\mathbf{\\text{5}}|\\!|^{}$ * $|\\!|\\mathbf{\\text{[[in t5] t23]}}|\\!|^{}_{t}$ leads to: $|\\!|\\mathbf{\\text{[5 [[in t5] t23]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({t23}_{e})({x}_{e})$ (by PA)<br />\n",
        "&nbsp;&nbsp;&nbsp;&nbsp;Step 9: $|\\!|\\mathbf{\\text{23}}|\\!|^{}$ * $|\\!|\\mathbf{\\text{[5 [[in t5] t23]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$ leads to: $|\\!|\\mathbf{\\text{[23 [5 [[in t5] t23]]]}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}} \\:=\\: $$\\lambda{} x1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({x1}_{e})({x}_{e})$ (by PA)<br />\n"
       ]
      }
     ],
     "prompt_number": 45
    },
    {
     "cell_type": "code",
     "collapsed": true,
     "input": [
      "b1.results[0].latex_step_tree()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{23}}|\\!|^{}$</td></tr><tr><td align=\"center\"><i>N/A</i></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{5}}|\\!|^{}$</td></tr><tr><td align=\"center\"><i>N/A</i></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({y}_{e})({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{t5}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${t5}_{e}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in t5]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({y}_{e})({t5}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{t23}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${t23}_{e}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[in t5] t23]}}|\\!|^{}_{t}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">${In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({t23}_{e})({t5}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[5 [[in t5] t23]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({t23}_{e})({x}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[23 [5 [[in t5] t23]]]}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({x1}_{e})({x}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 46,
       "text": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{23}}|\\!|^{}$</td></tr><tr><td align=\"center\"><i>N/A</i></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{5}}|\\!|^{}$</td></tr><tr><td align=\"center\"><i>N/A</i></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{in}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td align=\"center\">$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({y}_{e})({x}_{e})$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{t5}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${t5}_{e}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[in t5]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} y_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({y}_{e})({t5}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{t23}}|\\!|^{}_{e}$</td></tr><tr><td align=\"center\">${t23}_{e}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[FA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[[in t5] t23]}}|\\!|^{}_{t}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">${In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({t23}_{e})({t5}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[5 [[in t5] t23]]}}|\\!|^{}_{\\langle{}e,t\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({t23}_{e})({x}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PA]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{[23 [5 [[in t5] t23]]]}}|\\!|^{}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: {In}_{\\langle{}e,\\langle{}e,t\\rangle{}\\rangle{}}({x1}_{e})({x}_{e})$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ]
      }
     ],
     "prompt_number": 46
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Current work: implementing tree-based computation, and top-down/deferred computation\n",
      "\n",
      "* using nltk Tree objects.\n",
      "* system for deferred / uncertain types -- rudimentary inference over unknown types (really primitive right now)"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "t2 = Tree(\"S\", [\"NP\", \"VP\"])\n",
      "r2 = lang.hk3_system.compose(t2)\n",
      "r2.results[2].latex_step_tree() #._repr_latex_()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{NP}}|\\!|^{}_{?}$</td></tr><tr><td align=\"center\">$|\\!|\\mathbf{\\text{NP}}|\\!|^{}_{?}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{VP}}|\\!|^{}_{?}$</td></tr><tr><td align=\"center\">$|\\!|\\mathbf{\\text{VP}}|\\!|^{}_{?}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{S}}|\\!|^{}_{\\langle{}e,t\\rangle{}_{?}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (|\\!|\\mathbf{\\text{NP}}|\\!|^{}_{\\langle{}e,t_{?}\\rangle{}_{?}}({x}_{e}) \\wedge{} |\\!|\\mathbf{\\text{VP}}|\\!|^{}_{\\langle{}e,t_{?}\\rangle{}_{?}}({x}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 61,
       "text": [
        "<table><tr><td style=\"vertical-align:bottom;padding:0px 10px\" align=\"center\"><table><tr><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{NP}}|\\!|^{}_{?}$</td></tr><tr><td align=\"center\">$|\\!|\\mathbf{\\text{NP}}|\\!|^{}_{?}$</td></tr></table>\n",
        "</td><td style=\"vertical-align:bottom;padding-bottom:5px\">&nbsp;&nbsp;&nbsp;$\\circ$&nbsp;&nbsp;&nbsp;</td><td style=\"vertical-align:bottom\"><table align=\"center\"><tr><td align=\"center\">$|\\!|\\mathbf{\\text{VP}}|\\!|^{}_{?}$</td></tr><tr><td align=\"center\">$|\\!|\\mathbf{\\text{VP}}|\\!|^{}_{?}$</td></tr></table>\n",
        "</td></tr></table></td><td style=\"vertical-align:bottom;padding-bottom:5px;padding-left:10px\"><b>[PM]</b></td></tr><tr style=\"border-top: 1px solid #848482\"><td align=\"center\"><table style=\"margin-top:10px\"><tr><td style=\"vertical-align:bottom\" align=\"center\">$|\\!|\\mathbf{\\text{S}}|\\!|^{}_{\\langle{}e,t\\rangle{}_{?}}$</td></tr><tr><td style=\"vertical-align:bottom\" align=\"center\">$\\lambda{} x_{e} \\: . \\: (|\\!|\\mathbf{\\text{NP}}|\\!|^{}_{\\langle{}e,t_{?}\\rangle{}_{?}}({x}_{e}) \\wedge{} |\\!|\\mathbf{\\text{VP}}|\\!|^{}_{\\langle{}e,t_{?}\\rangle{}_{?}}({x}_{e}))$</td></tr></table>\n",
        "</td><td></td></tr></table>\n"
       ]
      }
     ],
     "prompt_number": 61
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 59
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "from lamb.tree_mini import Tree # hacked package to work with python 3\n",
      "t = Tree(\"S\", [cat, \"VP\"])  # this is a tree with a missing VP.  Exploit the fact that Composites are trees and nodes can be Items in lamb.\n",
      "local_tree = lang.tfa_l.build_local(t)\n",
      "local_tree # need to implement ipython output routines for nltk.Tree.\n",
      "#lang.hk3_system.compose(t)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "ltx_print(local_tree[0], local_tree[0].type, \"missing VP:\", local_tree[1], local_tree[1].type) # type not yet inferred"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "r = lang.hk3_system.compose(t)\n",
      "r"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "r = lang.tfa_l(t)\n",
      "ltx_print(r,r.type)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "l = lang.tfa_r(t)\n",
      "l"
     ],
     "language": "python",
     "metadata": {},
     "outputs": []
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "&nbsp;\n",
      "\n",
      "## Some future projects, non-exhaustive ##\n",
      "\n",
      "* complete fragment of Heim and Kratzer\n",
      "* extend fragment coverage.  Some interesting targets where interactivity would be useful to understanding:\n",
      "  * Continuations and quantification (Cf. van Eijck and Unger's Haskell implementation)\n",
      "  * Jacobson-style analyses of pronouns\n",
      "  * Compositional hamblin semantics\n",
      "  * Compositional DRT\n",
      "* better inference over types.  (Standard algorithms from type-logical grammar?)\n",
      "* variables over types -- for type-flexible denotations.\n",
      "* type shifts.  (Quite easy in this framework.)\n",
      "* underlying model theory.\n",
      "* various improvements to the graphics -- trees (?), double brackets (hard in mathjax), ...\n",
      "* full latex output (trees in tikz-qtree and so on).\n",
      "* better set theory mechanisms\n",
      "* presuppositions and some form of projection (Starting point, Heim and Kratzer)\n",
      "\n",
      "Longer term:\n",
      "\n",
      "* integration with SymPy (?)\n",
      "* release as an app\n",
      "* deeper integration with nltk (once nltk is compatible with python 3)\n",
      "* parsing that makes less use of python `eval`, and is generally less ad-hoc.  (This is an issue inherited from AIMA-python's logic.py.)\n",
      "  * this is an issue where in principle, a language like Haskell is a better choice than python.  But I think the usability / robustness of python and its libraries has the edge here overall, not to mention ipython notebook...\n",
      "* toy spatial system\n",
      "* side-by-side comparison of e.g. multiple analyses of presupposition projection"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [],
     "language": "python",
     "metadata": {},
     "outputs": []
    }
   ],
   "metadata": {}
  }
 ]
}