{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": { "collapsed": true }, "outputs": [], "source": [ "reload_lamb()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Compositional DRT in the Lambda Notebook\n", "\n", "### Notebook author: Dee Reisinger\n", "\n", "This notebook outlines one way to implement (part of) compositional DRT as developed in Reinhard Muskens, \"[Combining Montague semantics and discourse representation,](http://cogprints.org/4715/2/combining.pdf)\" Linguistics and Philosophy 19, 1996." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "First, I define a new type $b$, which will be the type of a DRS \n", "box in the typed lambda calculus." ] }, { "cell_type": "code", "execution_count": 2, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/latex": [ "Type system with atomic types: $b, n, t, e$" ], "text/plain": [ "" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# Add a type for boxes\n", "drt_types = meta.get_type_system()\n", "type_b = types.BasicType(\"b\") # Type of boxes\n", "drt_types.add_atomic(type_b)\n", "meta.set_type_system(drt_types)\n", "drt_types" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Next, I define a new binding operator, $\\text{Box}$, in the metalanguage.\n", "\n", "The metalanguage expression $\\text{Box}~u_1, u_2, \\ldots, u_n~.~\\phi(u_1, u_2, \\ldots, u_n)$ is equivalent to the more conventional\n", "linearized box expression $[\\;u_1, u_2, \\ldots, u_n \\mid \\phi(u_1, u_2, \\ldots, u_n)\\;]$." ] }, { "cell_type": "code", "execution_count": 3, "metadata": { "collapsed": false }, "outputs": [], "source": [ "class DRTBox(meta.BindingOp):\n", " canonical_name = \"Box\"\n", " op_name_latex = \"\\\\text{Box}~\"\n", " allow_multivars=True # A box can introduce more than one\n", " # discourse referent.\n", " allow_novars=True # A box can also introduce no new\n", " # discourse referents.\n", " \n", " # Many of the following methods will be implemented in a\n", " # future version of meta.BindingOp, so DRTBox will inherit\n", " # them automatically.\n", " def __init__(self, var_sequence, body, assignment=None):\n", " self.derivation = None\n", " self.type_guessed = False\n", " self.defer = False\n", " self.let = False\n", " self.type = type_b\n", " new_seq = list()\n", " if isinstance(var_sequence, meta.Tuple):\n", " var_sequence = var_sequence.tuple()\n", " for v in var_sequence:\n", " if isinstance(v, tuple):\n", " v = meta.TypedExpr.term_factory(v[0], typ=v[1])\n", " v = self.ensure_typed_expr(v)\n", " if not isinstance(v.type, types.BasicType):\n", " raise types.TypeMismatch(v, v.type, \"DRTBox requires atomic non-variable type for universe\")\n", " if not meta.is_var_symbol(v.op):\n", " raise ValueError(\"Need variable name (got '%s')\" % v.op)\n", " new_seq.append(v)\n", " self.var_sequence = new_seq\n", " self.init_body(self.ensure_typed_expr(body, types.type_t, assignment=self.scope_assignment(assignment)))\n", " self.op = \"%s:\" % (self.canonical_name)\n", " self.args[0] = meta.Tuple(self.var_sequence)\n", " \n", " def scope_assignment(self, assignment=None):\n", " if assignment is None:\n", " assignment = dict()\n", " else:\n", " assignment = assignment.copy()\n", " for v in self.var_sequence:\n", " assignment[v.op] = v\n", "\n", " @property\n", " def varname(self):\n", " return None\n", "\n", " @property\n", " def vartype(self):\n", " return None\n", "\n", " @property\n", " def var_instance(self):\n", " return meta.Tuple(self.var_sequence)\n", "\n", "\n", " def latex_str(self, **kwargs):\n", " var_repr = [v.latex_str() for v in self.var_sequence]\n", " if self.body == meta.true_term:\n", " return meta.ensuremath(\"[~%s~\\mid~]\" % (\",\".join(var_repr))) \n", " else:\n", " return meta.ensuremath(\"[~%s~\\mid~%s~]\" % (\",\".join(var_repr), \n", " self.body.latex_str())) \n", " def copy(self):\n", " return DRTBox(self.var_sequence, self.body)\n", " \n", " def copy_local(self, var_seq, body):\n", " return DRTBox(var_seq, body)\n", " \n", "meta.BindingOp.add_op(DRTBox)" ] }, { "cell_type": "code", "execution_count": 4, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/latex": [ "$[~{x}_{e},{y}_{e}~\\mid~{P}({x}_{e})~]$" ], "text/plain": [ "(Box (x_e, y_e): P_(x_e))" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DRTBox([te(\"x_e\"), te(\"y_e\")], te(\"P_(x_e)\"))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The next cell demonstrates how to create a box in the Lambda Notebook metalanguage.\n", "\n", "The following points are particularly important:\n", "* The variables introduced by a box must be of type $e$. This differs from Muskens 1996, who defines a new type $\\pi$ for _registers_.\n", "* The _conditions_ in the body of the box must be of type $t$. If a box has multiple conditions, they are linked using conjunction `&`.\n", "* Boxes can also have empty variable lists if they introduce no new discourse referents.\n", "* Boxes with no conditions—that is, boxes that _only_ introduce new discourse referents—should have $True$ as their body." ] }, { "cell_type": "code", "execution_count": 5, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Man_t' into , to match argument 'x1_e'\n", "INFO (meta): Coerced guessed type for 'Woman_t' into , to match argument 'x2_e'\n", "INFO (meta): Coerced guessed type for 'Adores_t' into <(e,e),t>, to match argument '(x1_e, x2_e)'\n", "INFO (meta): Coerced guessed type for 'Abhors_t' into <(e,e),t>, to match argument '(x2_e, x1_e)'\n", "INFO (meta): Coerced guessed type for 'Adores_t' into <(e,e),t>, to match argument '(John_e, Mary_e)'\n" ] }, { "data": { "text/html": [ "${box1}_{b}\\:=\\:[~{x1}_{e},{x2}_{e}~\\mid~((({Man}({x1}_{e}) \\wedge{} {Woman}({x2}_{e})) \\wedge{} {Adores}({x1}_{e}, {x2}_{e})) \\wedge{} {Abhors}({x2}_{e}, {x1}_{e}))~]$
\n", "${box2}_{b}\\:=\\:[~~\\mid~{Adores}({John}_{e}, {Mary}_{e})~]$
\n", "${box3}_{b}\\:=\\:[~{x}_{e},{y}_{e},{z}_{e}~\\mid~]$" ], "text/latex": [ "${box1}_{b}\\:=\\:[~{x1}_{e},{x2}_{e}~\\mid~((({Man}({x1}_{e}) \\wedge{} {Woman}({x2}_{e})) \\wedge{} {Adores}({x1}_{e}, {x2}_{e})) \\wedge{} {Abhors}({x2}_{e}, {x1}_{e}))~]$
\n", "${box2}_{b}\\:=\\:[~~\\mid~{Adores}({John}_{e}, {Mary}_{e})~]$
\n", "${box3}_{b}\\:=\\:[~{x}_{e},{y}_{e},{z}_{e}~\\mid~]$" ], "text/plain": [ "${box1}_{b}\\:=\\:[~{x1}_{e},{x2}_{e}~\\mid~((({Man}({x1}_{e}) \\wedge{} {Woman}({x2}_{e})) \\wedge{} {Adores}({x1}_{e}, {x2}_{e})) \\wedge{} {Abhors}({x2}_{e}, {x1}_{e}))~]$
\n", "${box2}_{b}\\:=\\:[~~\\mid~{Adores}({John}_{e}, {Mary}_{e})~]$
\n", "${box3}_{b}\\:=\\:[~{x}_{e},{y}_{e},{z}_{e}~\\mid~]$" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "# This is the denotation of example (1), \"A man adores a woman. She abhors him.\", in Muskens 1996.\n", "box1 = Box x1_e, x2_e : Man(x1) & Woman(x2) & Adores(x1, x2) & Abhors(x2, x1)\n", " \n", "# An example of a box with an empty variable list\n", "box2 = Box : Adores(John_e, Mary_e)\n", " \n", "# An example of a box with an \"empty\" body\n", "box3 = Box x_e, y_e, z_e : True" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Next, I define the semicolon operator that \"chains\" two boxes together. This is equivalent to sentential conjunction in dynamic semantics and hence will be denoted by '&' in the metalanguage; in Muskens 1996, it is denoted by the semicolon operator. Additionally, I define a reduction operation on boxes that merges them together as described by Muskens's _Merging Lemma_." ] }, { "cell_type": "code", "execution_count": 6, "metadata": { "collapsed": false }, "outputs": [], "source": [ "class BinaryJoinExpr(meta.BinaryOpExpr):\n", " def __init__(self, arg1, arg2):\n", " super().__init__(type_b, \"&\", arg1, arg2, op_name_latex = \";\")\n", " \n", " def reducible(self):\n", " return all(isinstance(x, DRTBox) for x in self.args)\n", " \n", " def reduce(self):\n", " b1 = self.args[0]; b2 = self.args[1]\n", " b1_free_vars = b1.body.free_variables()\n", " # Only merge if none of the variables introduced by the second\n", " # argument are free in the body of the first\n", " if all(x.op not in b1_free_vars for x in b2.var_sequence):\n", " combined_vars = b1.var_sequence + b2.var_sequence\n", " combined_body = meta.BinaryAndExpr(b1.body, b2.body).simplify_all()\n", " return meta.derived(DRTBox(combined_vars, combined_body), self, desc=\"Merging Lemma\")\n", " else:\n", " return BinaryJoinExpr(b1, b2)\n", " \n", "# Add the new operation to the metalanguage\n", "def and_factory(arg1, arg2):\n", " arg1 = meta.TypedExpr.ensure_typed_expr(arg1)\n", " arg2 = meta.TypedExpr.ensure_typed_expr(arg2)\n", " ts = meta.get_type_system()\n", " if ts.eq_check(arg1.type, types.type_t):\n", " return meta.BinaryAndExpr(arg1, arg2)\n", " elif ts.eq_check(arg1.type, type_b):\n", " return BinaryJoinExpr(arg1, arg2)\n", " else:\n", " raise types.TypeMismatch(arg1, arg2, \"Unknown types for operator &\")\n", " \n", "\n", "meta.binary_symbols_to_op_exprs['&'] = and_factory" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The following cell shows the semicolon operator in action." ] }, { "cell_type": "code", "execution_count": 7, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Man_t' into , to match argument 'x1_e'\n", "INFO (meta): Coerced guessed type for 'Woman_t' into , to match argument 'x2_e'\n" ] }, { "data": { "text/html": [ "${box1}_{b}\\:=\\:[~{x1}_{e},{x2}_{e}~\\mid~]$
\n", "${box2}_{b}\\:=\\:[~~\\mid~{Man}({x1}_{e})~]$
\n", "${box3}_{b}\\:=\\:[~~\\mid~{Woman}({x2}_{e})~]$
\n", "${box4}_{b}\\:=\\:(([~{x1}_{e},{x2}_{e}~\\mid~] ; [~~\\mid~{Man}({x1}_{e})~]) ; [~~\\mid~{Woman}({x2}_{e})~])$" ], "text/latex": [ "${box1}_{b}\\:=\\:[~{x1}_{e},{x2}_{e}~\\mid~]$
\n", "${box2}_{b}\\:=\\:[~~\\mid~{Man}({x1}_{e})~]$
\n", "${box3}_{b}\\:=\\:[~~\\mid~{Woman}({x2}_{e})~]$
\n", "${box4}_{b}\\:=\\:(([~{x1}_{e},{x2}_{e}~\\mid~] ; [~~\\mid~{Man}({x1}_{e})~]) ; [~~\\mid~{Woman}({x2}_{e})~])$" ], "text/plain": [ "${box1}_{b}\\:=\\:[~{x1}_{e},{x2}_{e}~\\mid~]$
\n", "${box2}_{b}\\:=\\:[~~\\mid~{Man}({x1}_{e})~]$
\n", "${box3}_{b}\\:=\\:[~~\\mid~{Woman}({x2}_{e})~]$
\n", "${box4}_{b}\\:=\\:(([~{x1}_{e},{x2}_{e}~\\mid~] ; [~~\\mid~{Man}({x1}_{e})~]) ; [~~\\mid~{Woman}({x2}_{e})~])$" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "box1 = Box x1_e, x2_e : True\n", "box2 = Box : Man(x1_e)\n", "box3 = Box : Woman(x2_e)\n", "box4 = box1 & box2 & box3" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The last box, which contains several boxes linked by the semicolon operator, can be reduced with the Merging Lemma; note that the compositional system will automaticallly apply this operation by default." ] }, { "cell_type": "code", "execution_count": 8, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/latex": [ "$[~{x1}_{e},{x2}_{e}~\\mid~({Man}({x1}_{e}) \\wedge{} {Woman}({x2}_{e}))~]$" ], "text/plain": [ "(Box (x1_e, x2_e): (Man_(x1_e) & Woman_(x2_e)))" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "box4.reduce_all()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "We now have all the machinery needed to define some simple lexical entries from Muskens 1996." ] }, { "cell_type": "code", "execution_count": 9, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Man_t' into , to match argument 'u_e'\n", "INFO (meta): Coerced guessed type for 'Runs_t' into , to match argument 'u_e'\n", "INFO (meta): Coerced guessed type for 'Loves_t' into <(e,e),t>, to match argument '(u_e, v_e)'\n", "INFO (meta): Coerced guessed type for 'Cat_t' into , to match argument 'u_e'\n" ] }, { "data": { "text/html": [ "$[\\![\\mathbf{\\text{man}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Man}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Runs}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: {p}({Fluffy}_{e})$
\n", "$[\\![\\mathbf{\\text{loves}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{},\\left\\langle{}e,b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\: . \\: \\lambda{} u_{e} \\: . \\: {p}(\\lambda{} v_{e} \\: . \\: [~~\\mid~{Loves}({u}_{e}, {v}_{e})~])$
\n", "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Cat}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{a1}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u1}_{e}~\\mid~] ; {p}({u1}_{e})) ; {q}({u1}_{e}))$
\n", "$[\\![\\mathbf{\\text{a2}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u2}_{e}~\\mid~] ; {p}({u2}_{e})) ; {q}({u2}_{e}))$" ], "text/latex": [ "$[\\![\\mathbf{\\text{man}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Man}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Runs}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: {p}({Fluffy}_{e})$
\n", "$[\\![\\mathbf{\\text{loves}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{},\\left\\langle{}e,b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\: . \\: \\lambda{} u_{e} \\: . \\: {p}(\\lambda{} v_{e} \\: . \\: [~~\\mid~{Loves}({u}_{e}, {v}_{e})~])$
\n", "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Cat}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{a1}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u1}_{e}~\\mid~] ; {p}({u1}_{e})) ; {q}({u1}_{e}))$
\n", "$[\\![\\mathbf{\\text{a2}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u2}_{e}~\\mid~] ; {p}({u2}_{e})) ; {q}({u2}_{e}))$" ], "text/plain": [ "$[\\![\\mathbf{\\text{man}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Man}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Runs}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: {p}({Fluffy}_{e})$
\n", "$[\\![\\mathbf{\\text{loves}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{},\\left\\langle{}e,b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\: . \\: \\lambda{} u_{e} \\: . \\: {p}(\\lambda{} v_{e} \\: . \\: [~~\\mid~{Loves}({u}_{e}, {v}_{e})~])$
\n", "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Cat}({u}_{e})~]$
\n", "$[\\![\\mathbf{\\text{a1}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u1}_{e}~\\mid~] ; {p}({u1}_{e})) ; {q}({u1}_{e}))$
\n", "$[\\![\\mathbf{\\text{a2}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u2}_{e}~\\mid~] ; {p}({u2}_{e})) ; {q}({u2}_{e}))$" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "||man|| = L u_e : (Box : Man(u))\n", "||runs|| = L u_e : (Box : Runs(u))\n", "||fluffy|| = L p_ : p(Fluffy_e)\n", "||loves|| = L p_<,b> : L u_e : p(L v_e : (Box : Loves(u, v)))\n", "||cat|| = L u_e : (Box : Cat(u))\n", "# The next entry is the indefinite article \"a\" with the subscript 1;\n", "# Later, we will see a more elegant way to handle indexed lexical entries.\n", "||a1|| = L p_ : L q_ : (Box u1 : True_t) & p(u1) & q(u1)\n", "# The indefinite article \"a\" with the subscript 2\n", "||a2|| = L p_ : L q_ : (Box u2 : True_t) & p(u2) & q(u2)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Composition now works as expected:" ] }, { "cell_type": "code", "execution_count": 10, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "Full composition trace. 1 path:
\n", "    Step 1: $[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: {p}({Fluffy}_{e})$
\n", "    Step 2: $[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Runs}({u}_{e})~]$
\n", "    Step 3: $[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$ leads to: $[\\![\\mathbf{\\text{[fluffy runs]}}]\\!]^{}_{b} \\:=\\: $$[~~\\mid~{Runs}({Fluffy}_{e})~]$ [by FA]
\n" ], "text/latex": [ "Full composition trace. 1 path:
\n", "    Step 1: $[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: {p}({Fluffy}_{e})$
\n", "    Step 2: $[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Runs}({u}_{e})~]$
\n", "    Step 3: $[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$ leads to: $[\\![\\mathbf{\\text{[fluffy runs]}}]\\!]^{}_{b} \\:=\\: $$[~~\\mid~{Runs}({Fluffy}_{e})~]$ [by FA]
\n" ], "text/plain": [ "Full composition trace. 1 path:
\n", "    Step 1: $[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: {p}({Fluffy}_{e})$
\n", "    Step 2: $[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}} \\:=\\: $$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Runs}({u}_{e})~]$
\n", "    Step 3: $[\\![\\mathbf{\\text{fluffy}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{runs}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$ leads to: $[\\![\\mathbf{\\text{[fluffy runs]}}]\\!]^{}_{b} \\:=\\: $$[~~\\mid~{Runs}({Fluffy}_{e})~]$ [by FA]
" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "(fluffy * runs).trace()" ] }, { "cell_type": "code", "execution_count": 11, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[a1 cat] [loves [a2 man]]]}}]\\!]^{}_{b} \\:=\\: $$[~{u1}_{e},{u2}_{e}~\\mid~({Cat}({u1}_{e}) \\wedge{} ({Man}({u2}_{e}) \\wedge{} {Loves}({u1}_{e}, {u2}_{e})))~]$" ], "text/plain": [ "CompositionResult(results=[⟦[[a1 cat] [loves [a2 man]]]⟧ = (Box (u1_e, u2_e): (Cat_(u1_e) & (Man_(u2_e) & Loves_<(e,e),t>(u1_e, u2_e))))], failures=[⟦[[loves [a2 man]] [a1 cat]]⟧ = Type mismatch: '⟦[loves [a2 man]]⟧ = (λ u_e: (Box (u2_e): (Man_(u2_e) & Loves_<(e,e),t>(u_e, u2_e))))'/ and '⟦[a1 cat]⟧ = (λ q_: ((Box (u1_e): Cat_(u1_e)) & q_(u1_e)))'/<,b> conflict (mode: Function Application), ⟦[[a1 cat] [loves [a2 man]]]⟧ = Type mismatch: '⟦[a1 cat]⟧ = (λ q_: ((Box (u1_e): Cat_(u1_e)) & q_(u1_e)))'/<,b> and '⟦[loves [a2 man]]⟧ = (λ u_e: (Box (u2_e): (Man_(u2_e) & Loves_<(e,e),t>(u_e, u2_e))))'/ conflict (mode: Predicate Modification), ⟦[[a1 cat] [loves [a2 man]]]⟧ = Type mismatch: '⟦[a1 cat]⟧ = (λ q_: ((Box (u1_e): Cat_(u1_e)) & q_(u1_e)))'/<,b> and '⟦[loves [a2 man]]⟧ = (λ u_e: (Box (u2_e): (Man_(u2_e) & Loves_<(e,e),t>(u_e, u2_e))))'/ conflict (mode: Predicate Abstraction), ⟦[[loves [a2 man]] [a1 cat]]⟧ = Type mismatch: '⟦[loves [a2 man]]⟧ = (λ u_e: (Box (u2_e): (Man_(u2_e) & Loves_<(e,e),t>(u_e, u2_e))))'/ and '⟦[a1 cat]⟧ = (λ q_: ((Box (u1_e): Cat_(u1_e)) & q_(u1_e)))'/<,b> conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = ((a1 * cat) * (loves * (a2 * man)))\n", "r" ] }, { "cell_type": "code", "execution_count": 12, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "1 composition path:
$[\\![\\mathbf{\\text{a1}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u1}_{e}~\\mid~] ; {p}({u1}_{e})) ; {q}({u1}_{e}))$
*
$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Cat}({u}_{e})~]$
[FA]
$[\\![\\mathbf{\\text{[a1 cat]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$
$\\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: ([~{u1}_{e}~\\mid~{Cat}({u1}_{e})~] ; {q}({u1}_{e}))$
*
$[\\![\\mathbf{\\text{loves}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{},\\left\\langle{}e,b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\: . \\: \\lambda{} u_{e} \\: . \\: {p}(\\lambda{} v_{e} \\: . \\: [~~\\mid~{Loves}({u}_{e}, {v}_{e})~])$
*
$[\\![\\mathbf{\\text{a2}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u2}_{e}~\\mid~] ; {p}({u2}_{e})) ; {q}({u2}_{e}))$
*
$[\\![\\mathbf{\\text{man}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Man}({u}_{e})~]$
[FA]
$[\\![\\mathbf{\\text{[a2 man]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$
$\\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: ([~{u2}_{e}~\\mid~{Man}({u2}_{e})~] ; {q}({u2}_{e}))$
[FA]
$[\\![\\mathbf{\\text{[loves [a2 man]]}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~{u2}_{e}~\\mid~({Man}({u2}_{e}) \\wedge{} {Loves}({u}_{e}, {u2}_{e}))~]$
[FA]
$[\\![\\mathbf{\\text{[[a1 cat] [loves [a2 man]]]}}]\\!]^{}_{b}$
$[~{u1}_{e},{u2}_{e}~\\mid~({Cat}({u1}_{e}) \\wedge{} ({Man}({u2}_{e}) \\wedge{} {Loves}({u1}_{e}, {u2}_{e})))~]$


" ], "text/latex": [ "1 composition path:
$[\\![\\mathbf{\\text{a1}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u1}_{e}~\\mid~] ; {p}({u1}_{e})) ; {q}({u1}_{e}))$
*
$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Cat}({u}_{e})~]$
[FA]
$[\\![\\mathbf{\\text{[a1 cat]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$
$\\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: ([~{u1}_{e}~\\mid~{Cat}({u1}_{e})~] ; {q}({u1}_{e}))$
*
$[\\![\\mathbf{\\text{loves}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{},\\left\\langle{}e,b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\: . \\: \\lambda{} u_{e} \\: . \\: {p}(\\lambda{} v_{e} \\: . \\: [~~\\mid~{Loves}({u}_{e}, {v}_{e})~])$
*
$[\\![\\mathbf{\\text{a2}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u2}_{e}~\\mid~] ; {p}({u2}_{e})) ; {q}({u2}_{e}))$
*
$[\\![\\mathbf{\\text{man}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Man}({u}_{e})~]$
[FA]
$[\\![\\mathbf{\\text{[a2 man]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$
$\\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: ([~{u2}_{e}~\\mid~{Man}({u2}_{e})~] ; {q}({u2}_{e}))$
[FA]
$[\\![\\mathbf{\\text{[loves [a2 man]]}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~{u2}_{e}~\\mid~({Man}({u2}_{e}) \\wedge{} {Loves}({u}_{e}, {u2}_{e}))~]$
[FA]
$[\\![\\mathbf{\\text{[[a1 cat] [loves [a2 man]]]}}]\\!]^{}_{b}$
$[~{u1}_{e},{u2}_{e}~\\mid~({Cat}({u1}_{e}) \\wedge{} ({Man}({u2}_{e}) \\wedge{} {Loves}({u1}_{e}, {u2}_{e})))~]$


" ], "text/plain": [ "1 composition path:
$[\\![\\mathbf{\\text{a1}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u1}_{e}~\\mid~] ; {p}({u1}_{e})) ; {q}({u1}_{e}))$
*
$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Cat}({u}_{e})~]$
[FA]
$[\\![\\mathbf{\\text{[a1 cat]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$
$\\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: ([~{u1}_{e}~\\mid~{Cat}({u1}_{e})~] ; {q}({u1}_{e}))$
*
$[\\![\\mathbf{\\text{loves}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{},\\left\\langle{}e,b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}} \\: . \\: \\lambda{} u_{e} \\: . \\: {p}(\\lambda{} v_{e} \\: . \\: [~~\\mid~{Loves}({u}_{e}, {v}_{e})~])$
*
$[\\![\\mathbf{\\text{a2}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: \\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: (([~{u2}_{e}~\\mid~] ; {p}({u2}_{e})) ; {q}({u2}_{e}))$
*
$[\\![\\mathbf{\\text{man}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~~\\mid~{Man}({u}_{e})~]$
[FA]
$[\\![\\mathbf{\\text{[a2 man]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,b\\right\\rangle{},b\\right\\rangle{}}$
$\\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: ([~{u2}_{e}~\\mid~{Man}({u2}_{e})~] ; {q}({u2}_{e}))$
[FA]
$[\\![\\mathbf{\\text{[loves [a2 man]]}}]\\!]^{}_{\\left\\langle{}e,b\\right\\rangle{}}$
$\\lambda{} u_{e} \\: . \\: [~{u2}_{e}~\\mid~({Man}({u2}_{e}) \\wedge{} {Loves}({u}_{e}, {u2}_{e}))~]$
[FA]
$[\\![\\mathbf{\\text{[[a1 cat] [loves [a2 man]]]}}]\\!]^{}_{b}$
$[~{u1}_{e},{u2}_{e}~\\mid~({Cat}({u1}_{e}) \\wedge{} ({Man}({u2}_{e}) \\wedge{} {Loves}({u1}_{e}, {u2}_{e})))~]$


" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r.tree()" ] }, { "cell_type": "code", "execution_count": 13, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
1.
${[\\lambda{} q_{\\left\\langle{}e,b\\right\\rangle{}} \\: . \\: ([~{u1}_{e}~\\mid~{Cat}({u1}_{e})~] ; {q}({u1}_{e}))]}(\\lambda{} u_{e} \\: . \\: [~{u2}_{e}~\\mid~({Man}({u2}_{e}) \\wedge{} {Loves}({u}_{e}, {u2}_{e}))~])$
2.
$([~{u1}_{e}~\\mid~{Cat}({u1}_{e})~] ; {[\\lambda{} u_{e} \\: . \\: [~{u2}_{e}~\\mid~({Man}({u2}_{e}) \\wedge{} {Loves}({u}_{e}, {u2}_{e}))~]]}({u1}_{e}))$
Reduction
3.
$([~{u1}_{e}~\\mid~{Cat}({u1}_{e})~] ; [~{u2}_{e}~\\mid~({Man}({u2}_{e}) \\wedge{} {Loves}({u1}_{e}, {u2}_{e}))~])$
Recursive reduction of operand 1
4.
$[~{u1}_{e},{u2}_{e}~\\mid~({Cat}({u1}_{e}) \\wedge{} ({Man}({u2}_{e}) \\wedge{} {Loves}({u1}_{e}, {u2}_{e})))~]$
Merging Lemma
" ], "text/plain": [ " 1. ((λ q_: ((Box (u1_e): Cat_(u1_e)) & q_(u1_e))))((λ u_e: (Box (u2_e): (Man_(u2_e) & Loves_<(e,e),t>(u_e, u2_e)))))\n", " 2. ((Box (u1_e): Cat_(u1_e)) & ((λ u_e: (Box (u2_e): (Man_(u2_e) & Loves_<(e,e),t>(u_e, u2_e)))))(u1_e)) (Reduction)\n", " 3. ((Box (u1_e): Cat_(u1_e)) & (Box (u2_e): (Man_(u2_e) & Loves_<(e,e),t>(u1_e, u2_e)))) (Recursive reduction of operand 1)\n", " 4. (Box (u1_e, u2_e): (Cat_(u1_e) & (Man_(u2_e) & Loves_<(e,e),t>(u1_e, u2_e)))) (Merging Lemma)" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r[0].content.derivation # show the reduction / simplification of the last step" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Finally, the current solution of defining a separate lexical entry for each index that a word like \"a\" or \"himself\" can take is cumbersome. The `indexed_item` function defined in the next cell is one way around this problem. The first argument of `indexed_item` is a string defining the name of the lexical item, and the second is a lambda calculus expression defining its content. Wherever something should depend on the value of an index, such as in the name of a discourse referent introduced by \"a\", use the `#` character." ] }, { "cell_type": "code", "execution_count": 14, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def indexed_item(name, raw_string):\n", " new_name = name + \"{0}\"\n", " ex_string = raw_string.replace(\"#\", \"{0}\")\n", " return lambda n: lang.Item(new_name.format(n), te(ex_string.format(n)))\n", "\n", "a = indexed_item(\"a\", \"L p_ : L q_ : (Box u# : True_t) & p(u#) & q(u#)\")\n", "himself = indexed_item(\"himself\", \"L p_ : p(u#)\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The following cells show how these indexed items can be used in composition." ] }, { "cell_type": "code", "execution_count": 15, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[a1 man] [loves himself1]]}}]\\!]^{}_{b} \\:=\\: $$[~{u1}_{e}~\\mid~({Man}({u1}_{e}) \\wedge{} {Loves}({u1}_{e}, {u1}_{e}))~]$" ], "text/plain": [ "CompositionResult(results=[⟦[[a1 man] [loves himself1]]⟧ = (Box (u1_e): (Man_(u1_e) & Loves_<(e,e),t>(u1_e, u1_e)))], failures=[⟦[[loves himself1] [a1 man]]⟧ = Type mismatch: '⟦[loves himself1]⟧ = (λ u_e: (Box (): Loves_<(e,e),t>(u_e, u1_e)))'/ and '⟦[a1 man]⟧ = (λ q_: ((Box (u1_e): Man_(u1_e)) & q_(u1_e)))'/<,b> conflict (mode: Function Application), ⟦[[a1 man] [loves himself1]]⟧ = Type mismatch: '⟦[a1 man]⟧ = (λ q_: ((Box (u1_e): Man_(u1_e)) & q_(u1_e)))'/<,b> and '⟦[loves himself1]⟧ = (λ u_e: (Box (): Loves_<(e,e),t>(u_e, u1_e)))'/ conflict (mode: Predicate Modification), ⟦[[a1 man] [loves himself1]]⟧ = Type mismatch: '⟦[a1 man]⟧ = (λ q_: ((Box (u1_e): Man_(u1_e)) & q_(u1_e)))'/<,b> and '⟦[loves himself1]⟧ = (λ u_e: (Box (): Loves_<(e,e),t>(u_e, u1_e)))'/ conflict (mode: Predicate Abstraction), ⟦[[loves himself1] [a1 man]]⟧ = Type mismatch: '⟦[loves himself1]⟧ = (λ u_e: (Box (): Loves_<(e,e),t>(u_e, u1_e)))'/ and '⟦[a1 man]⟧ = (λ q_: ((Box (u1_e): Man_(u1_e)) & q_(u1_e)))'/<,b> conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "((a(1) * man) * (loves * himself(1)))" ] }, { "cell_type": "code", "execution_count": 16, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[a3 cat] [loves [a5 man]]]}}]\\!]^{}_{b} \\:=\\: $$[~{u3}_{e},{u5}_{e}~\\mid~({Cat}({u3}_{e}) \\wedge{} ({Man}({u5}_{e}) \\wedge{} {Loves}({u3}_{e}, {u5}_{e})))~]$" ], "text/plain": [ "CompositionResult(results=[⟦[[a3 cat] [loves [a5 man]]]⟧ = (Box (u3_e, u5_e): (Cat_(u3_e) & (Man_(u5_e) & Loves_<(e,e),t>(u3_e, u5_e))))], failures=[⟦[[loves [a5 man]] [a3 cat]]⟧ = Type mismatch: '⟦[loves [a5 man]]⟧ = (λ u_e: (Box (u5_e): (Man_(u5_e) & Loves_<(e,e),t>(u_e, u5_e))))'/ and '⟦[a3 cat]⟧ = (λ q_: ((Box (u3_e): Cat_(u3_e)) & q_(u3_e)))'/<,b> conflict (mode: Function Application), ⟦[[a3 cat] [loves [a5 man]]]⟧ = Type mismatch: '⟦[a3 cat]⟧ = (λ q_: ((Box (u3_e): Cat_(u3_e)) & q_(u3_e)))'/<,b> and '⟦[loves [a5 man]]⟧ = (λ u_e: (Box (u5_e): (Man_(u5_e) & Loves_<(e,e),t>(u_e, u5_e))))'/ conflict (mode: Predicate Modification), ⟦[[a3 cat] [loves [a5 man]]]⟧ = Type mismatch: '⟦[a3 cat]⟧ = (λ q_: ((Box (u3_e): Cat_(u3_e)) & q_(u3_e)))'/<,b> and '⟦[loves [a5 man]]⟧ = (λ u_e: (Box (u5_e): (Man_(u5_e) & Loves_<(e,e),t>(u_e, u5_e))))'/ conflict (mode: Predicate Abstraction), ⟦[[loves [a5 man]] [a3 cat]]⟧ = Type mismatch: '⟦[loves [a5 man]]⟧ = (λ u_e: (Box (u5_e): (Man_(u5_e) & Loves_<(e,e),t>(u_e, u5_e))))'/ and '⟦[a3 cat]⟧ = (λ q_: ((Box (u3_e): Cat_(u3_e)) & q_(u3_e)))'/<,b> conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "(a(3) * cat) * (loves * (a(5) * man))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### TODO:\n", "\n", "* Operations that take boxes to conditions, like **not**, **or**, and $\\implies$\n", "* Other composition operations, like Muskens's $T_3$ SEQUENCING and $T_4$ QUANTIFYING-IN\n", "* Referent accessibility" ] }, { "cell_type": "code", "execution_count": 17, "metadata": { "collapsed": true }, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "display_name": "Lambda Notebook (Python 3)", "language": "python", "name": "lambda-notebook" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.5.1" } }, "nbformat": 4, "nbformat_minor": 0 }