{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "reload_lamb()" ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [ { "data": { "text/latex": [ "Type system with atomic types: $s, n, e, t$" ], "text/plain": [ "" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "type_s = types.BasicType(\"s\")\n", "lang.get_system().add_basic_type(type_s)\n", "intensional_types = meta.get_type_system()\n", "intensional_types" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Intensional scope\n", "### Notebook author: Kyle Rawlins / Apr 2018\n", "\n", "This notebook goes through the basics of three approaches to scope in an intensional context. It is not intended as an introduction to the linguistic issues, but rather as a technical supplement to such an overview (which can be partially found in the von Fintel and Heim lecture notes). That is, this notebook presupposes familiarity with notions like \"de re\", \"the third reading\", etc.\n", "\n", "The three approaches are:\n", "* Intensionalization triggered by selection for an intensional type, binding all world variables in the scope of the selecting item (von Fintel and Heim lecture notes).\n", "* World variables in the syntax (Percus 2000).\n", "* Split intensionality (Keshet 2011).\n", "\n", "I will focus on two main examples:\n", "\n", " (1) Joanna believes my brother is Canadian. (After one of Percus's examples)\n", " (2) Alfonso wants to buy an inexpensive coat. (After Keshet's version of Fodor's famous third reading example.)\n", " \n" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Scope with indices, intensionalization, and QR\n", "\n", "We begin with the von Fintel & Heim first treatment of intensionalization. In this approach, selection of an intensional type triggers abstraction over the world of evaluation for the complement. I have implemented this here as a type shift feeding FA, rather than a separate composition operation." ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "data": { "text/html": [ "Composition system 'H&K simple (copy)'
Operations: {
    Binary composition rule FA, built on python function 'lamb.lang.fa_fun'
    Binary composition rule PM, built on python function 'lamb.lang.pm_fun'
    Binary composition rule PA, built on python function 'lamb.lang.pa_fun'
    Typeshift INT, built on python function '__main__.intension_fun'
}" ], "text/plain": [ "Composition system: H&K simple (copy)" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# set up evaluation world as a parameter to the interpretation function\n", "int_system = lang.td_system.copy()\n", "eval_w = lang.te(\"w_s\")\n", "int_system.assign_controller = lang.AssignmentController(specials=[eval_w])\n", "lang.set_system(int_system)\n", "\n", "# code to abstract over the evaluation world.\n", "def intension_fun(f, assignment=None):\n", " new_a = lang.Assignment(assignment)\n", " new_a.update({\"w\": lang.te(\"w_s\")})\n", " result = meta.LFun(\"w_s\", f.content.under_assignment(new_a))\n", " return lang.UnaryComposite(f, result, source=\"INT(%s)\" % (f.name))\n", "\n", "int_system.add_rule(lang.UnaryCompositionOp(\"INT\", intension_fun, typeshift=True))\n", "int_system.typeshift = True\n", "int_system" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "For the sake of being explicit about scope in these derivations, I will implement `my` using an existential quantifier." ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Brother_t' into <(e,e,s),t>, to match argument '(x_e, y_e, w_s)'\n", "INFO (meta): Coerced guessed type for 'Canadian_t' into <(e,s),t>, to match argument '(x_e, w_s)'\n" ] }, { "data": { "text/html": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$" ], "text/latex": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$" ], "text/plain": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "||brother|| = L x_e : L y_e : Brother(x,y,w)\n", "||canadian|| = L x_e : Canadian(x,w)\n", "||joanna|| = Joanna_e\n", "||my|| = L f_> : L g_ : Exists x_e : f(Speaker_e)(x) & g(x)\n", "dox = Dox_<(e,s),{s}>\n", "||believe|| = L p_ : L x_e : Forall w2_s : w2 << dox(x, w_s) >> p(w2)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "First, the basic unembedded sentence:" ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[my brother] canadian]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {w}_{s}))$" ], "text/plain": [ "CompositionResult(results=[⟦[[my brother] canadian]⟧[w_s, type s, g] = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & Canadian_<(e,s),t>(x_e, w_s)))], failures=[⟦[canadian [my brother]]⟧[w_s, type s, g] = Type mismatch: '⟦canadian⟧[w_s, type s, g] = (λ x_e: Canadian_<(e,s),t>(x_e, w_s))'/ and '⟦[my brother]⟧[w_s, type s, g] = (λ g_: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & g_(x_e))))'/<,t> conflict (mode: Function Application), ⟦[[my brother] canadian]⟧[w_s, type s, g] = Type mismatch: '⟦[my brother]⟧[w_s, type s, g] = (λ g_: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & g_(x_e))))'/<,t> and '⟦canadian⟧[w_s, type s, g] = (λ x_e: Canadian_<(e,s),t>(x_e, w_s))'/ conflict (mode: Predicate Modification), ⟦[[my brother] canadian]⟧[w_s, type s, g] = Type mismatch: '⟦[my brother]⟧[w_s, type s, g] = (λ g_: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & g_(x_e))))'/<,t> and '⟦canadian⟧[w_s, type s, g] = (λ x_e: Canadian_<(e,s),t>(x_e, w_s))'/ conflict (mode: Predicate Abstraction), ⟦[canadian [my brother]]⟧[w_s, type s, g] = Type mismatch: '⟦canadian⟧[w_s, type s, g] = (λ x_e: Canadian_<(e,s),t>(x_e, w_s))'/ and '⟦[my brother]⟧[w_s, type s, g] = (λ g_: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & g_(x_e))))'/<,t> conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "(my * brother) * canadian" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Surface scope, everything in situ:" ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[believe INT([[my brother] canadian])] joanna]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[[believe INT([[my brother] canadian])] joanna]⟧[w_s, type s, g] = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s)))))], failures=[⟦[joanna [believe INT([[my brother] canadian])]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe INT([[my brother] canadian])]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ conflict (mode: Function Application), ⟦[joanna [believe INT([[my brother] canadian])]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe INT([[my brother] canadian])]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ conflict (mode: Predicate Modification), ⟦[joanna [believe INT([[my brother] canadian])]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe INT([[my brother] canadian])]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ conflict (mode: Predicate Abstraction), ⟦[[believe INT([[my brother] canadian])] joanna]⟧[w_s, type s, g] = Type mismatch: '⟦[believe INT([[my brother] canadian])]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ and '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "(joanna * (believe * ((my * brother) * canadian))) #.tree()" ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [], "source": [ "trace = lang.Trace.index_factory(typ=types.type_e)\n", "from lamb.lang import Binder" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Wide scope (de re), DP has raised via QR (assuming this is possible across a finite clause boundary):" ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[my brother] [11 [[believe INT([canadian t11])] joanna]]]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} {Canadian}({x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[[my brother] [11 [[believe INT([canadian t11])] joanna]]]⟧[w_s, type s, g] = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> Canadian_<(e,s),t>(x_e, w2_s)))))], failures=[⟦[[11 [[believe INT([canadian t11])] joanna]] [my brother]]⟧[w_s, type s, g] = Type mismatch: '⟦[11 [[believe INT([canadian t11])] joanna]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> Canadian_<(e,s),t>(x_e, w2_s))))'/ and '⟦[my brother]⟧[w_s, type s, g] = (λ g_: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & g_(x_e))))'/<,t> conflict (mode: Function Application), ⟦[[my brother] [11 [[believe INT([canadian t11])] joanna]]]⟧[w_s, type s, g] = Type mismatch: '⟦[my brother]⟧[w_s, type s, g] = (λ g_: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & g_(x_e))))'/<,t> and '⟦[11 [[believe INT([canadian t11])] joanna]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> Canadian_<(e,s),t>(x_e, w2_s))))'/ conflict (mode: Predicate Modification), ⟦[[my brother] [11 [[believe INT([canadian t11])] joanna]]]⟧[w_s, type s, g] = Type mismatch: '⟦[my brother]⟧[w_s, type s, g] = (λ g_: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & g_(x_e))))'/<,t> and '⟦[11 [[believe INT([canadian t11])] joanna]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> Canadian_<(e,s),t>(x_e, w2_s))))'/ conflict (mode: Predicate Abstraction), ⟦[[11 [[believe INT([canadian t11])] joanna]] [my brother]]⟧[w_s, type s, g] = Type mismatch: '⟦[11 [[believe INT([canadian t11])] joanna]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> Canadian_<(e,s),t>(x_e, w2_s))))'/ and '⟦[my brother]⟧[w_s, type s, g] = (λ g_: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & g_(x_e))))'/<,t> conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "((my * brother) *\n", " (Binder(11) *\n", " (joanna * (believe *\n", " (trace(11) * canadian))))) #.tree()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "With just these tools, there is no other way to get another reading." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# World variables\n", "\n", "This is the barest sketch of the world variable proposal in Percus 2000, *Constraints on some other variables in syntax*, Natural Language Semantics 8." ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [], "source": [ "w = lang.IndexedPronoun.index_factory(\"w\", typ=type_s)" ] }, { "cell_type": "code", "execution_count": 10, "metadata": {}, "outputs": [ { "data": { "text/html": [ "Composition system 'H&K simple (copy)'
Operations: {
    Binary composition rule FA, built on python function 'lamb.lang.fa_fun'
    Binary composition rule PM, built on python function 'lamb.lang.pm_fun'
    Binary composition rule PA, built on python function 'lamb.lang.pa_fun'
    Binary composition rule WPA, built on python function '__main__.world_pa'
}" ], "text/plain": [ "Composition system: H&K simple (copy)" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# back to the basic composition system, just need to generalize PA\n", "world_binding_system = lang.td_system.copy()\n", "\n", "from lamb.types import TypeMismatch\n", "from lamb.lang import BinaryComposite\n", "\n", "# Predicate abstraction for world variables. Based on lang.sbc_pa\n", "def world_pa(binder, content, assignment=None):\n", " if (binder.content is not None) or not binder.name.strip().isnumeric():\n", " raise TypeMismatch(binder, content, \"Predicate Abstraction (type s)\")\n", " index = int(binder.name.strip())\n", " vname = \"var%i\" % index\n", " bound_var = meta.term(vname, type_s)\n", " f = meta.LFun(type_s, content.content.calculate_partiality({bound_var}), vname)\n", " return BinaryComposite(binder, content, f)\n", "\n", "world_binding_system.add_rule(lang.BinaryCompositionOp(\"WPA\", world_pa, allow_none=True))\n", "lang.set_system(world_binding_system)\n", "world_binding_system" ] }, { "cell_type": "code", "execution_count": 11, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Brother_t' into <(e,e,s),t>, to match argument '(x_e, y_e, w_s)'\n", "INFO (meta): Coerced guessed type for 'Canadian_t' into <(e,s),t>, to match argument '(x_e, w_s)'\n" ] }, { "data": { "text/html": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w})) \\rightarrow{} {p}({w2}))$" ], "text/latex": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w})) \\rightarrow{} {p}({w2}))$" ], "text/plain": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: \\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w})) \\rightarrow{} {p}({w2}))$" ] }, "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "||brother|| = L w_s : L x_e : L y_e : Brother(x,y,w)\n", "||canadian|| = L w_s : L x_e : Canadian(x,w)\n", "||joanna|| = Joanna_e\n", "||my|| = L f_> : L g_ : Exists x_e : f(Speaker_e)(x) & g(x)\n", "dox = Dox_<(e,s),{s}>\n", "||believe|| = L w_s : L p_ : L x_e : Forall w2_s : w2 << dox(x, w_s) >> p(w2)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Basic unembedded sentence. As long as all world variables must be bound, and binders are only inserted up to interpretability to achieve a type $\\langle s,t \\rangle$ at the root, this is the only possible binding configuration for this sentence." ] }, { "cell_type": "code", "execution_count": 12, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[1 [[my [brother w1]] [canadian w1]]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}} \\:=\\: $$\\lambda{} var1_{s} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}) \\wedge{} {Canadian}({x}, {var1}))$" ], "text/plain": [ "CompositionResult(results=[⟦[1 [[my [brother w1]] [canadian w1]]]⟧ = (λ var1_s: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var1_s) & Canadian_<(e,s),t>(x_e, var1_s))))], failures=[⟦[1 [[my [brother w1]] [canadian w1]]]⟧ = Type mismatch: '⟦1⟧ = None' and '⟦[[my [brother w1]] [canadian w1]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var1_s) & Canadian_<(e,s),t>(x_e, var1_s)))'/t conflict (mode: FA), ⟦[[[my [brother w1]] [canadian w1]] 1]⟧ = Type mismatch: '⟦[[my [brother w1]] [canadian w1]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var1_s) & Canadian_<(e,s),t>(x_e, var1_s)))'/t and '⟦1⟧ = None' conflict (mode: FA), ⟦[1 [[my [brother w1]] [canadian w1]]]⟧ = Type mismatch: '⟦1⟧ = None' and '⟦[[my [brother w1]] [canadian w1]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var1_s) & Canadian_<(e,s),t>(x_e, var1_s)))'/t conflict (mode: PM), ⟦[1 [[my [brother w1]] [canadian w1]]]⟧ = Type mismatch: 'var1_s'/s and 'var1_e'/e conflict (mode: Variable replace (unify failed)), ⟦[[[my [brother w1]] [canadian w1]] 1]⟧ = Type mismatch: '⟦[[my [brother w1]] [canadian w1]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var1_s) & Canadian_<(e,s),t>(x_e, var1_s)))'/t and '⟦1⟧ = None' conflict (mode: Predicate Abstraction), ⟦[[[my [brother w1]] [canadian w1]] 1]⟧ = Type mismatch: '⟦[[my [brother w1]] [canadian w1]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var1_s) & Canadian_<(e,s),t>(x_e, var1_s)))'/t and '⟦1⟧ = None' conflict (mode: Predicate Abstraction (type s))])" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "Binder(1) * ((my * (brother * w(1))) * (canadian * w(1)))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Pure de dicto sentence:" ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[5 [[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}} \\:=\\: $$\\lambda{} var5_{s} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[5 [[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]]⟧ = (λ var5_s: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s))))))], failures=[⟦[5 [[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t conflict (mode: FA), ⟦[[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: FA), ⟦[5 [[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t conflict (mode: PM), ⟦[5 [[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]]⟧ = Type mismatch: 'var5_s'/s and 'var5_e'/e conflict (mode: Variable replace (unify failed)), ⟦[[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: Predicate Abstraction), ⟦[[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: Predicate Abstraction (type s))])" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = Binder(5) * (joanna *\n", " ((believe * w(5)) *\n", " (Binder(1) * ((my * (brother * w(1))) * (canadian * w(1))))))\n", "r" ] }, { "cell_type": "code", "execution_count": 14, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path:
$[\\![\\mathbf{\\text{5}}]\\!]^{}$
N/A
*
$[\\![\\mathbf{\\text{believe}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{w}}_{5}]\\!]^{}_{s}$
${var5}_{s}$
[FA]
$[\\![\\mathbf{\\text{[believe w5]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {var5}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{1}}]\\!]^{}$
N/A
*
$[\\![\\mathbf{\\text{my}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w})$
*
$[\\![\\mathbf{\\text{w}}_{1}]\\!]^{}_{s}$
${var1}_{s}$
[FA]
$[\\![\\mathbf{\\text{[brother w1]}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {var1}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my [brother w1]]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}}$
$\\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}_{s}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w})$
*
$[\\![\\mathbf{\\text{w}}_{1}]\\!]^{}_{s}$
${var1}_{s}$
[FA]
$[\\![\\mathbf{\\text{[canadian w1]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {var1}_{s})$
[FA]
$[\\![\\mathbf{\\text{[[my [brother w1]] [canadian w1]]}}]\\!]^{}_{t}$
$\\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}_{s}) \\wedge{} {Canadian}({x}, {var1}_{s}))$
[WPA]
$[\\![\\mathbf{\\text{[1 [[my [brother w1]] [canadian w1]]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} var1_{s} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}) \\wedge{} {Canadian}({x}, {var1}))$
[FA]
$[\\![\\mathbf{\\text{[[believe w5] [1 [[my [brother w1]] [canadian w1]]]]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {var5}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]}}]\\!]^{}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$
[WPA]
$[\\![\\mathbf{\\text{[5 [[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} var5_{s} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$


" ], "text/latex": [ "1 composition path:
$[\\![\\mathbf{\\text{5}}]\\!]^{}$
N/A
*
$[\\![\\mathbf{\\text{believe}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{w}}_{5}]\\!]^{}_{s}$
${var5}_{s}$
[FA]
$[\\![\\mathbf{\\text{[believe w5]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {var5}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{1}}]\\!]^{}$
N/A
*
$[\\![\\mathbf{\\text{my}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w})$
*
$[\\![\\mathbf{\\text{w}}_{1}]\\!]^{}_{s}$
${var1}_{s}$
[FA]
$[\\![\\mathbf{\\text{[brother w1]}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {var1}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my [brother w1]]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}}$
$\\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}_{s}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w})$
*
$[\\![\\mathbf{\\text{w}}_{1}]\\!]^{}_{s}$
${var1}_{s}$
[FA]
$[\\![\\mathbf{\\text{[canadian w1]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {var1}_{s})$
[FA]
$[\\![\\mathbf{\\text{[[my [brother w1]] [canadian w1]]}}]\\!]^{}_{t}$
$\\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}_{s}) \\wedge{} {Canadian}({x}, {var1}_{s}))$
[WPA]
$[\\![\\mathbf{\\text{[1 [[my [brother w1]] [canadian w1]]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} var1_{s} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}) \\wedge{} {Canadian}({x}, {var1}))$
[FA]
$[\\![\\mathbf{\\text{[[believe w5] [1 [[my [brother w1]] [canadian w1]]]]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {var5}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]}}]\\!]^{}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$
[WPA]
$[\\![\\mathbf{\\text{[5 [[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} var5_{s} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$


" ], "text/plain": [ "1 composition path:
$[\\![\\mathbf{\\text{5}}]\\!]^{}$
N/A
*
$[\\![\\mathbf{\\text{believe}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{w}}_{5}]\\!]^{}_{s}$
${var5}_{s}$
[FA]
$[\\![\\mathbf{\\text{[believe w5]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {var5}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{1}}]\\!]^{}$
N/A
*
$[\\![\\mathbf{\\text{my}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w})$
*
$[\\![\\mathbf{\\text{w}}_{1}]\\!]^{}_{s}$
${var1}_{s}$
[FA]
$[\\![\\mathbf{\\text{[brother w1]}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {var1}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my [brother w1]]}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}}$
$\\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}_{s}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{}_{\\left\\langle{}s,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: \\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w})$
*
$[\\![\\mathbf{\\text{w}}_{1}]\\!]^{}_{s}$
${var1}_{s}$
[FA]
$[\\![\\mathbf{\\text{[canadian w1]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {var1}_{s})$
[FA]
$[\\![\\mathbf{\\text{[[my [brother w1]] [canadian w1]]}}]\\!]^{}_{t}$
$\\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}_{s}) \\wedge{} {Canadian}({x}, {var1}_{s}))$
[WPA]
$[\\![\\mathbf{\\text{[1 [[my [brother w1]] [canadian w1]]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} var1_{s} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var1}) \\wedge{} {Canadian}({x}, {var1}))$
[FA]
$[\\![\\mathbf{\\text{[[believe w5] [1 [[my [brother w1]] [canadian w1]]]]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {var5}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]}}]\\!]^{}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$
[WPA]
$[\\![\\mathbf{\\text{[5 [[[believe w5] [1 [[my [brother w1]] [canadian w1]]]] joanna]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} var5_{s} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {w2})))$


" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r.tree()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "In principle there are several other binding configurations that are possible even without QR. Let's also assume a constraint against vacuous binding, with the effect that `Binder(1)` being inserted (required for semantic composition) forces at least one bound variable downstairs." ] }, { "cell_type": "code", "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[5 [[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}} \\:=\\: $$\\lambda{} var5_{s} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var5}) \\wedge{} {Canadian}({x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[5 [[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]]⟧ = (λ var5_s: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & Canadian_<(e,s),t>(x_e, w2_s))))))], failures=[⟦[5 [[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t conflict (mode: FA), ⟦[[[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: FA), ⟦[5 [[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t conflict (mode: PM), ⟦[5 [[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]]⟧ = Type mismatch: 'var5_s'/s and 'var5_e'/e conflict (mode: Variable replace (unify failed)), ⟦[[[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: Predicate Abstraction), ⟦[[[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w5]] [canadian w1]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: Predicate Abstraction (type s))])" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = Binder(5) * (joanna * ((believe * w(5)) *\n", " (Binder(1) *\n", " ((my * (brother * w(5))) * (canadian * w(1))))))\n", "r" ] }, { "cell_type": "code", "execution_count": 16, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[5 [[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}} \\:=\\: $$\\lambda{} var5_{s} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w2}) \\wedge{} {Canadian}({x}, {var5})))$" ], "text/plain": [ "CompositionResult(results=[⟦[5 [[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]]⟧ = (λ var5_s: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, var5_s))))))], failures=[⟦[5 [[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, var5_s)))))'/t conflict (mode: FA), ⟦[[[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, var5_s)))))'/t and '⟦5⟧ = None' conflict (mode: FA), ⟦[5 [[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, var5_s)))))'/t conflict (mode: PM), ⟦[5 [[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]]⟧ = Type mismatch: 'var5_s'/s and 'var5_e'/e conflict (mode: Variable replace (unify failed)), ⟦[[[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, var5_s)))))'/t and '⟦5⟧ = None' conflict (mode: Predicate Abstraction), ⟦[[[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna] 5]⟧ = Type mismatch: '⟦[[[believe w5] [1 [[my [brother w1]] [canadian w5]]]] joanna]⟧ = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s) & Canadian_<(e,s),t>(x_e, var5_s)))))'/t and '⟦5⟧ = None' conflict (mode: Predicate Abstraction (type s))])" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = Binder(5) * (joanna * ((believe * w(5)) * (Binder(1) * ((my * (brother * w(1))) * (canadian * w(5))))))\n", "r" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The second of these binding configurations would be banned by Percus's *Generalization X*. A slightly reformulated version of this condition: the world variable that a VP predicate selects most be coindexed with the nearest c-commanding binder.\n", "\n", "With QR we would get another possibility. This binding configuration is really the only possibility for this scope configuration." ] }, { "cell_type": "code", "execution_count": 17, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[5 [[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]]}}]\\!]^{}_{\\left\\langle{}s,t\\right\\rangle{}} \\:=\\: $$\\lambda{} var5_{s} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {var5}) \\wedge{} \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {var5})) \\rightarrow{} {Canadian}({x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[5 [[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]]⟧ = (λ var5_s: (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> Canadian_<(e,s),t>(x_e, w2_s))))))], failures=[⟦[5 [[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> Canadian_<(e,s),t>(x_e, w2_s)))))'/t conflict (mode: FA), ⟦[[[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]] 5]⟧ = Type mismatch: '⟦[[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: FA), ⟦[5 [[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> Canadian_<(e,s),t>(x_e, w2_s)))))'/t conflict (mode: PM), ⟦[5 [[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]]⟧ = Type mismatch: 'var5_s'/s and 'var5_e'/e conflict (mode: Variable replace (unify failed)), ⟦[[[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]] 5]⟧ = Type mismatch: '⟦[[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: Predicate Abstraction), ⟦[[[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]] 5]⟧ = Type mismatch: '⟦[[my [brother w5]] [3 [[[believe w5] [1 [[canadian w1] t3]]] joanna]]]⟧ = (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, var5_s) & (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, var5_s)) >> Canadian_<(e,s),t>(x_e, w2_s)))))'/t and '⟦5⟧ = None' conflict (mode: Predicate Abstraction (type s))])" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = Binder(5) * ((my * (brother * w(5))) *\n", " (Binder(3) * (joanna * ((believe * w(5)) *\n", " (Binder(1) *\n", " (trace(3) * (canadian * w(1))))))))\n", "r" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Split intensionality\n", "\n", "This approach illustrates the core of the analysis in Keshet 2011, *Split intensionality: a new scope theory of de re and de dicto*, Linguistics and Philosophy 33. I will set things up slightly differently, implementing his intensionalization operation as a unary composition operation, rather than an operator. (This is mainly because it is a bit more straightforward in the lambda notebook, rather than for any deep reasons.)" ] }, { "cell_type": "code", "execution_count": 18, "metadata": {}, "outputs": [ { "data": { "text/html": [ "Composition system 'H&K simple (copy)'
Operations: {
    Binary composition rule FA, built on python function 'lamb.lang.fa_fun'
    Binary composition rule PM, built on python function 'lamb.lang.pm_fun'
    Binary composition rule PA, built on python function 'lamb.lang.pa_fun'
    Unary composition rule INT, built on python function '__main__.intension_fun'
}" ], "text/plain": [ "Composition system: H&K simple (copy)" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# set up evaluation world as a parameter to the interpretation function\n", "int_system = lang.td_system.copy()\n", "eval_w = lang.te(\"w_s\")\n", "int_system.assign_controller = lang.AssignmentController(specials=[eval_w])\n", "lang.set_system(int_system)\n", "\n", "# same intensionalization code as in the first version\n", "def intension_fun(f, assignment=None):\n", " new_a = lang.Assignment(assignment)\n", " new_a.update({\"w\": lang.te(\"w_s\")})\n", " result = meta.LFun(\"w_s\", f.content.under_assignment(new_a))\n", " return lang.UnaryComposite(f, result, source=\"INT(%s)\" % (f.name))\n", "\n", "# add INT as a unary operation, *not* a type shift.\n", "int_system.add_rule(lang.UnaryCompositionOp(\"INT\", intension_fun))\n", "int_system" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "There are two key ideas: (i) instead of generating propositions via a world binder inserted up to interpretability, we generate propositions with a shifting intensionalization operator (I will call this operator `INT`, Keshet notates it as ${}^{\\wedge}$ after Montague). (ii) this intensionalization operator has syntactic presence, and QR can target a position above the operator or below it. The position above it generates transparent non-specific readings, but doesn't involve movement across a clause boundary." ] }, { "cell_type": "code", "execution_count": 19, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Brother_t' into <(e,e,s),t>, to match argument '(x_e, y_e, w_s)'\n", "INFO (meta): Coerced guessed type for 'Canadian_t' into <(e,s),t>, to match argument '(x_e, w_s)'\n" ] }, { "data": { "text/html": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({Speaker}_{e})({x})$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$" ], "text/latex": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({Speaker}_{e})({x})$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$" ], "text/plain": [ "$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Joanna}_{e}$
\n", "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({Speaker}_{e})({x})$
\n", "${dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}\\:=\\:{Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}$
\n", "$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "||brother|| = L x_e : L y_e : Brother(x,y,w)\n", "||canadian|| = L x_e : Canadian(x,w)\n", "||joanna|| = Joanna_e\n", "||my|| = L f_> : Iota x_e : f(Speaker_e)(x) # note change from above -- discussed below\n", "dox = Dox_<(e,s),{s}>\n", "||believe|| = L p_ : L x_e : Forall w2_s : w2 << dox(x, w_s) >> p(w2)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The basic case is much the same as on the starting approach. To trigger unary composition, compose with `None`:" ] }, { "cell_type": "code", "execution_count": 20, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{INT([canadian [my brother]])}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}} \\:=\\: $$\\lambda{} w_{s} \\: . \\: {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}), {w})$" ], "text/plain": [ "CompositionResult(results=[⟦INT([canadian [my brother]])⟧[w_s, type s, g] = (λ w_s: Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s)), w_s))], failures=[])" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "((my * brother) * canadian) * None" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The pure de dicto reading is not especially new or exciting; where before there was a type-shift, now we have an intensionalization operator:" ] }, { "cell_type": "code", "execution_count": 21, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[believe INT([canadian [my brother]])] joanna]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w2}), {w2}))$" ], "text/plain": [ "CompositionResult(results=[⟦[[believe INT([canadian [my brother]])] joanna]⟧[w_s, type s, g] = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s)), w2_s)))], failures=[⟦[joanna [believe INT([canadian [my brother]])]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe INT([canadian [my brother]])]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s)), w2_s))))'/ conflict (mode: Function Application), ⟦[joanna [believe INT([canadian [my brother]])]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe INT([canadian [my brother]])]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s)), w2_s))))'/ conflict (mode: Predicate Modification), ⟦[joanna [believe INT([canadian [my brother]])]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe INT([canadian [my brother]])]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s)), w2_s))))'/ conflict (mode: Predicate Abstraction), ⟦[[believe INT([canadian [my brother]])] joanna]⟧[w_s, type s, g] = Type mismatch: '⟦[believe INT([canadian [my brother]])]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w2_s)), w2_s))))'/ and '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 21, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = (joanna * (believe *\n", " (((my * brother) * canadian) * None)))\n", "r" ] }, { "cell_type": "code", "execution_count": 22, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path:
$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
*
$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},e\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({Speaker}_{e})({x})$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my brother]}}]\\!]^{{w}_{s}, g}_{e}$
$\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[canadian [my brother]]}}]\\!]^{{w}_{s}, g}_{t}$
${Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}_{s}), {w}_{s})$
[INT]
$[\\![\\mathbf{\\text{INT([canadian [my brother]])}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}), {w})$
[FA]
$[\\![\\mathbf{\\text{[believe INT([canadian [my brother]])]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w2}), {w2}))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[believe INT([canadian [my brother]])] joanna]}}]\\!]^{{w}_{s}, g}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w2}), {w2}))$


" ], "text/latex": [ "1 composition path:
$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
*
$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},e\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({Speaker}_{e})({x})$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my brother]}}]\\!]^{{w}_{s}, g}_{e}$
$\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[canadian [my brother]]}}]\\!]^{{w}_{s}, g}_{t}$
${Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}_{s}), {w}_{s})$
[INT]
$[\\![\\mathbf{\\text{INT([canadian [my brother]])}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}), {w})$
[FA]
$[\\![\\mathbf{\\text{[believe INT([canadian [my brother]])]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w2}), {w2}))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[believe INT([canadian [my brother]])] joanna]}}]\\!]^{{w}_{s}, g}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w2}), {w2}))$


" ], "text/plain": [ "1 composition path:
$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
*
$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},e\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({Speaker}_{e})({x})$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my brother]}}]\\!]^{{w}_{s}, g}_{e}$
$\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[canadian [my brother]]}}]\\!]^{{w}_{s}, g}_{t}$
${Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}_{s}), {w}_{s})$
[INT]
$[\\![\\mathbf{\\text{INT([canadian [my brother]])}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}), {w})$
[FA]
$[\\![\\mathbf{\\text{[believe INT([canadian [my brother]])]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w2}), {w2}))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[believe INT([canadian [my brother]])] joanna]}}]\\!]^{{w}_{s}, g}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w2}), {w2}))$


" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r.tree()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "What is new is the intermediate QR derivation:" ] }, { "cell_type": "code", "execution_count": 23, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[believe [[3 INT([canadian t3])] [my brother]]] joanna]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}_{s}), {w2}))$" ], "text/plain": [ "CompositionResult(results=[⟦[[believe [[3 INT([canadian t3])] [my brother]]] joanna]⟧[w_s, type s, g] = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s)), w2_s)))], failures=[⟦[joanna [believe [[3 INT([canadian t3])] [my brother]]]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe [[3 INT([canadian t3])] [my brother]]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s)), w2_s))))'/ conflict (mode: Function Application), ⟦[joanna [believe [[3 INT([canadian t3])] [my brother]]]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe [[3 INT([canadian t3])] [my brother]]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s)), w2_s))))'/ conflict (mode: Predicate Modification), ⟦[joanna [believe [[3 INT([canadian t3])] [my brother]]]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe [[3 INT([canadian t3])] [my brother]]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s)), w2_s))))'/ conflict (mode: Predicate Abstraction), ⟦[[believe [[3 INT([canadian t3])] [my brother]]] joanna]⟧[w_s, type s, g] = Type mismatch: '⟦[believe [[3 INT([canadian t3])] [my brother]]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s)), w2_s))))'/ and '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = (joanna * (believe *\n", " ((my * brother) * (Binder(3) *\n", " ((trace(3) * canadian) * None)))))\n", "r" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "And finally, the pure de re reading. There is no way to generate the reading that Percus needed to ban with generalization X, because intensional scope is still parasitic on DP scope." ] }, { "cell_type": "code", "execution_count": 24, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[3 INT([canadian t3])] [my brother]]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}} \\:=\\: $$\\lambda{} w1_{s} \\: . \\: {Canadian}(\\iota{} x_{e} \\: . \\: {Brother}({Speaker}_{e}, {x}, {w}_{s}), {w1})$" ], "text/plain": [ "CompositionResult(results=[⟦[[3 INT([canadian t3])] [my brother]]⟧[w_s, type s, g] = (λ w1_s: Canadian_<(e,s),t>((ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s)), w1_s))], failures=[⟦[[my brother] [3 INT([canadian t3])]]⟧[w_s, type s, g] = Type mismatch: '⟦[my brother]⟧[w_s, type s, g] = (ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s))'/e and '⟦[3 INT([canadian t3])]⟧[w_s, type s, g] = (λ x_e: (λ w_s: Canadian_<(e,s),t>(x_e, w_s)))'/> conflict (mode: Function Application), ⟦[[my brother] [3 INT([canadian t3])]]⟧[w_s, type s, g] = Type mismatch: '⟦[my brother]⟧[w_s, type s, g] = (ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s))'/e and '⟦[3 INT([canadian t3])]⟧[w_s, type s, g] = (λ x_e: (λ w_s: Canadian_<(e,s),t>(x_e, w_s)))'/> conflict (mode: Predicate Modification), ⟦[[my brother] [3 INT([canadian t3])]]⟧[w_s, type s, g] = Type mismatch: '⟦[my brother]⟧[w_s, type s, g] = (ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s))'/e and '⟦[3 INT([canadian t3])]⟧[w_s, type s, g] = (λ x_e: (λ w_s: Canadian_<(e,s),t>(x_e, w_s)))'/> conflict (mode: Predicate Abstraction), ⟦[[3 INT([canadian t3])] [my brother]]⟧[w_s, type s, g] = Type mismatch: '⟦[3 INT([canadian t3])]⟧[w_s, type s, g] = (λ x_e: (λ w_s: Canadian_<(e,s),t>(x_e, w_s)))'/> and '⟦[my brother]⟧[w_s, type s, g] = (ι x_e: Brother_<(e,e,s),t>(Speaker_e, x_e, w_s))'/e conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 24, "metadata": {}, "output_type": "execute_result" } ], "source": [ "((my * brother) * (Binder(3) *\n", " ((trace(3) * canadian) * None)))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "One complication is that a regular generalized quantifier type won't work with regular FA on this approach, if it scopes above `INT`. You can see this by examining the type generated for a binder scoping over `INT`:" ] }, { "cell_type": "code", "execution_count": 25, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[3 INT([canadian t3])]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}s,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} w_{s} \\: . \\: {Canadian}({x}, {w})$" ], "text/plain": [ "CompositionResult(results=[⟦[3 INT([canadian t3])]⟧[w_s, type s, g] = (λ x_e: (λ w_s: Canadian_<(e,s),t>(x_e, w_s)))], failures=[⟦[3 INT([canadian t3])]⟧[w_s, type s, g] = Type mismatch: '⟦3⟧[w_s, type s, g] = None' and '⟦INT([canadian t3])⟧[w_s, type s, g] = (λ w_s: Canadian_<(e,s),t>(var3_e, w_s))'/ conflict (mode: FA), ⟦[INT([canadian t3]) 3]⟧[w_s, type s, g] = Type mismatch: '⟦INT([canadian t3])⟧[w_s, type s, g] = (λ w_s: Canadian_<(e,s),t>(var3_e, w_s))'/ and '⟦3⟧[w_s, type s, g] = None' conflict (mode: FA), ⟦[3 INT([canadian t3])]⟧[w_s, type s, g] = Type mismatch: '⟦3⟧[w_s, type s, g] = None' and '⟦INT([canadian t3])⟧[w_s, type s, g] = (λ w_s: Canadian_<(e,s),t>(var3_e, w_s))'/ conflict (mode: PM), ⟦[INT([canadian t3]) 3]⟧[w_s, type s, g] = Type mismatch: '⟦INT([canadian t3])⟧[w_s, type s, g] = (λ w_s: Canadian_<(e,s),t>(var3_e, w_s))'/ and '⟦3⟧[w_s, type s, g] = None' conflict (mode: Predicate Abstraction)])" ] }, "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ "Binder(3) * ((trace(3) * canadian) * None)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "That is, an (extensional) generalized quantifier DP will be type $\\langle \\langle e,t \\rangle , t \\rangle$, but we really need something of type $\\langle \\langle e,\\langle s,t\\rangle \\rangle , \\langle s,t\\rangle \\rangle$. Keshet proposes a solution to this using a different composition operation for generalized quantifiers due to Daniel Buring; this operation also allows composition in object position without QR. This operation is rather complex and general, but for dealing with `INT` we really only need one special case, which I implement here as a binary composition via the following combinator. 'AS' stands for Argument Saturation." ] }, { "cell_type": "code", "execution_count": 26, "metadata": {}, "outputs": [ { "data": { "text/latex": [ "$\\lambda{} quant_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}} \\: . \\: \\lambda{} f_{\\left\\langle{}e,\\left\\langle{}X,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} y_{X} \\: . \\: {quant}(\\lambda{} x_{e} \\: . \\: {f}({x})({y}))$" ], "text/plain": [ "(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))" ] }, "execution_count": 26, "metadata": {}, "output_type": "execute_result" } ], "source": [ "as_combinator = %te L quant_<,t> : L f_> : L y_X : quant(L x_e : f(x)(y))\n", "as_combinator" ] }, { "cell_type": "code", "execution_count": 27, "metadata": {}, "outputs": [ { "data": { "text/html": [ "Composition system 'H&K simple (copy)'
Operations: {
    Binary composition rule FA, built on python function 'lamb.lang.fa_fun'
    Binary composition rule PM, built on python function 'lamb.lang.pm_fun'
    Binary composition rule PA, built on python function 'lamb.lang.pa_fun'
    Unary composition rule INT, built on python function '__main__.intension_fun'
    Binary composition rule AS, built on combinator '$\\lambda{} quant_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}} \\: . \\: \\lambda{} f_{\\left\\langle{}e,\\left\\langle{}X,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} y_{X} \\: . \\: {quant}(\\lambda{} x_{e} \\: . \\: {f}({x})({y}))$'
}" ], "text/plain": [ "Composition system: H&K simple (copy)" ] }, "execution_count": 27, "metadata": {}, "output_type": "execute_result" } ], "source": [ "#int_system.add_typeshift(as_combinator, \"AS\")\n", "#int_system.typeshift = True\n", "int_system.add_binary_rule(as_combinator, \"AS\")\n", "int_system" ] }, { "cell_type": "code", "execution_count": 28, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$" ], "text/latex": [ "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$" ], "text/plain": [ "$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$" ] }, "execution_count": 28, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "||my|| = L f_> : L g_ : Exists x_e : f(Speaker_e)(x) & g(x)" ] }, { "cell_type": "code", "execution_count": 29, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[believe [[my brother] [3 INT([canadian t3])]]] joanna]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[[believe [[my brother] [3 INT([canadian t3])]]] joanna]⟧[w_s, type s, g] = (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(Joanna_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & Canadian_<(e,s),t>(x_e, w2_s)))))], failures=[⟦[joanna [believe [[my brother] [3 INT([canadian t3])]]]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe [[my brother] [3 INT([canadian t3])]]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ conflict (mode: Function Application), ⟦[joanna [believe [[my brother] [3 INT([canadian t3])]]]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe [[my brother] [3 INT([canadian t3])]]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ conflict (mode: Predicate Modification), ⟦[joanna [believe [[my brother] [3 INT([canadian t3])]]]]⟧[w_s, type s, g] = Type mismatch: '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e and '⟦[believe [[my brother] [3 INT([canadian t3])]]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ conflict (mode: Predicate Abstraction), ⟦[[believe [[my brother] [3 INT([canadian t3])]]] joanna]⟧[w_s, type s, g] = Type mismatch: '⟦[believe [[my brother] [3 INT([canadian t3])]]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ and '⟦joanna⟧[w_s, type s, g] = Joanna_e'/e conflict (mode: Predicate Abstraction), ⟦[joanna [believe [[my brother] [3 INT([canadian t3])]]]]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and 'Joanna_e'/e conflict (mode: Function argument combination (unification failed)), ⟦[[believe [[my brother] [3 INT([canadian t3])]]] joanna]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and '(λ x_e: (Forall w2_s: ((w2_s << Dox_<(e,s),{s}>(x_e, w_s)) >> (Exists x_e: (Brother_<(e,e,s),t>(Speaker_e, x_e, w_s) & Canadian_<(e,s),t>(x_e, w2_s))))))'/ conflict (mode: Function argument combination (unification failed))])" ] }, "execution_count": 29, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = (joanna * (believe *\n", " ((my * brother) * (Binder(3) *\n", " ((trace(3) * canadian) * None)))))\n", "r" ] }, { "cell_type": "code", "execution_count": 30, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path:
$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my brother]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}}$
$\\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{3}}]\\!]^{{w}_{s}, g}$
N/A
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
*
$[\\![\\mathbf{\\text{t}}_{3}]\\!]^{{w}_{s}, g}_{e}$
${var3}_{e}$
[FA]
$[\\![\\mathbf{\\text{[canadian t3]}}]\\!]^{{w}_{s}, g}_{t}$
${Canadian}({var3}_{e}, {w}_{s})$
[INT]
$[\\![\\mathbf{\\text{INT([canadian t3])}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: {Canadian}({var3}_{e}, {w})$
[PA]
$[\\![\\mathbf{\\text{[3 INT([canadian t3])]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}s,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} w_{s} \\: . \\: {Canadian}({x}, {w})$
[AS]
$[\\![\\mathbf{\\text{[[my brother] [3 INT([canadian t3])]]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} y_{s} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {y}))$
[FA]
$[\\![\\mathbf{\\text{[believe [[my brother] [3 INT([canadian t3])]]]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {w2})))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[believe [[my brother] [3 INT([canadian t3])]]] joanna]}}]\\!]^{{w}_{s}, g}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {w2})))$


" ], "text/latex": [ "1 composition path:
$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my brother]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}}$
$\\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{3}}]\\!]^{{w}_{s}, g}$
N/A
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
*
$[\\![\\mathbf{\\text{t}}_{3}]\\!]^{{w}_{s}, g}_{e}$
${var3}_{e}$
[FA]
$[\\![\\mathbf{\\text{[canadian t3]}}]\\!]^{{w}_{s}, g}_{t}$
${Canadian}({var3}_{e}, {w}_{s})$
[INT]
$[\\![\\mathbf{\\text{INT([canadian t3])}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: {Canadian}({var3}_{e}, {w})$
[PA]
$[\\![\\mathbf{\\text{[3 INT([canadian t3])]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}s,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} w_{s} \\: . \\: {Canadian}({x}, {w})$
[AS]
$[\\![\\mathbf{\\text{[[my brother] [3 INT([canadian t3])]]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} y_{s} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {y}))$
[FA]
$[\\![\\mathbf{\\text{[believe [[my brother] [3 INT([canadian t3])]]]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {w2})))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[believe [[my brother] [3 INT([canadian t3])]]] joanna]}}]\\!]^{{w}_{s}, g}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {w2})))$


" ], "text/plain": [ "1 composition path:
$[\\![\\mathbf{\\text{believe}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
*
$[\\![\\mathbf{\\text{my}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} f_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({Speaker}_{e})({x}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{brother}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Brother}({x}, {y}, {w}_{s})$
[FA]
$[\\![\\mathbf{\\text{[my brother]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}}$
$\\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {g}({x}))$
*
$[\\![\\mathbf{\\text{3}}]\\!]^{{w}_{s}, g}$
N/A
*
$[\\![\\mathbf{\\text{canadian}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: {Canadian}({x}, {w}_{s})$
*
$[\\![\\mathbf{\\text{t}}_{3}]\\!]^{{w}_{s}, g}_{e}$
${var3}_{e}$
[FA]
$[\\![\\mathbf{\\text{[canadian t3]}}]\\!]^{{w}_{s}, g}_{t}$
${Canadian}({var3}_{e}, {w}_{s})$
[INT]
$[\\![\\mathbf{\\text{INT([canadian t3])}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} w_{s} \\: . \\: {Canadian}({var3}_{e}, {w})$
[PA]
$[\\![\\mathbf{\\text{[3 INT([canadian t3])]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}s,t\\right\\rangle{}\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\lambda{} w_{s} \\: . \\: {Canadian}({x}, {w})$
[AS]
$[\\![\\mathbf{\\text{[[my brother] [3 INT([canadian t3])]]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}s,t\\right\\rangle{}}$
$\\lambda{} y_{s} \\: . \\: \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {y}))$
[FA]
$[\\![\\mathbf{\\text{[believe [[my brother] [3 INT([canadian t3])]]]}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}}$
$\\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {w2})))$
*
$[\\![\\mathbf{\\text{joanna}}]\\!]^{{w}_{s}, g}_{e}$
${Joanna}_{e}$
[FA]
$[\\![\\mathbf{\\text{[[believe [[my brother] [3 INT([canadian t3])]]] joanna]}}]\\!]^{{w}_{s}, g}_{t}$
$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Dox}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Joanna}_{e}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: ({Brother}({Speaker}_{e}, {x}, {w}_{s}) \\wedge{} {Canadian}({x}, {w2})))$


" ] }, "execution_count": 30, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r.tree()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "In any case where QR above the intensional lexical item is possible, Keshet's system generates Fodor's three readings: a pure de dicto reading (non-specific/opaque), a pure de re reading (specific/transparent), and the third reading (non-specific/transparent). Here are the readings in an example more tailored to have them:" ] }, { "cell_type": "code", "execution_count": 31, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Buy_t' into <(e,e,s),t>, to match argument '(y_e, x_e, w_s)'\n", "INFO (meta): Coerced guessed type for 'Coat_t' into <(e,s),t>, to match argument '(x_e, w_s)'\n", "INFO (meta): Coerced guessed type for 'Inexpensive_t' into <(e,s),t>, to match argument '(x_e, w_s)'\n" ] }, { "data": { "text/html": [ "$[\\![\\mathbf{\\text{buy}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Buy}({y}, {x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{coat}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Coat}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{inexpensive}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Inexpensive}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{want}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Des}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
\n", "$[\\![\\mathbf{\\text{alfonso}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Alfonso}_{e}$
\n", "$[\\![\\mathbf{\\text{an}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({x}) \\wedge{} {g}({x}))$" ], "text/latex": [ "$[\\![\\mathbf{\\text{buy}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Buy}({y}, {x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{coat}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Coat}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{inexpensive}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Inexpensive}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{want}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Des}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
\n", "$[\\![\\mathbf{\\text{alfonso}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Alfonso}_{e}$
\n", "$[\\![\\mathbf{\\text{an}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({x}) \\wedge{} {g}({x}))$" ], "text/plain": [ "$[\\![\\mathbf{\\text{buy}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Buy}({y}, {x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{coat}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Coat}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{inexpensive}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Inexpensive}({x}, {w}_{s})$
\n", "$[\\![\\mathbf{\\text{want}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}s,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}s,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Des}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({x}, {w}_{s})) \\rightarrow{} {p}({w2}))$
\n", "$[\\![\\mathbf{\\text{alfonso}}]\\!]^{{w}_{s}, g}_{e} \\:=\\: $${Alfonso}_{e}$
\n", "$[\\![\\mathbf{\\text{an}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: ({f}({x}) \\wedge{} {g}({x}))$" ] }, "execution_count": 31, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "||buy|| = L x_e : L y_e : Buy(y,x,w)\n", "||coat|| = L x_e : Coat(x,w)\n", "||inexpensive|| = L x_e : Inexpensive(x,w)\n", "||want|| = L p_ : L x_e : Forall w2_s : w2 << Des_<(e,s),{s}>(x,w) >> p(w2)\n", "||alfonso|| = Alfonso_e\n", "||an|| = L f_ : L g_ : Exists x_e : f(x) & g(x)" ] }, { "cell_type": "code", "execution_count": 32, "metadata": {}, "outputs": [], "source": [ "PRO = lang.IndexedPronoun.index_factory(\"PRO\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Pure de dicto (non-specific / opaque), quantifier scopes under `INT`:" ] }, { "cell_type": "code", "execution_count": 33, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]] alfonso]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Des}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Alfonso}_{e}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: (({Inexpensive}({x}, {w2}) \\wedge{} {Coat}({x}, {w2})) \\wedge{} {Buy}({Alfonso}_{e}, {x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[[10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]] alfonso]⟧[w_s, type s, g] = (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s)))))], failures=[⟦[alfonso [10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]]]⟧[w_s, type s, g] = Type mismatch: '⟦alfonso⟧[w_s, type s, g] = Alfonso_e'/e and '⟦[10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ conflict (mode: Function Application), ⟦[alfonso [10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]]]⟧[w_s, type s, g] = Type mismatch: '⟦alfonso⟧[w_s, type s, g] = Alfonso_e'/e and '⟦[10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ conflict (mode: Predicate Modification), ⟦[alfonso [10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]]]⟧[w_s, type s, g] = Type mismatch: '⟦alfonso⟧[w_s, type s, g] = Alfonso_e'/e and '⟦[10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ conflict (mode: Predicate Abstraction), ⟦[[10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]] alfonso]⟧[w_s, type s, g] = Type mismatch: '⟦[10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ and '⟦alfonso⟧[w_s, type s, g] = Alfonso_e'/e conflict (mode: Predicate Abstraction), ⟦[alfonso [10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]]]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and 'Alfonso_e'/e conflict (mode: Function argument combination (unification failed)), ⟦[[10 [[want INT([[an [inexpensive coat]] [3 [[buy t3] PRO10]]])] t10]] alfonso]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and '(λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ conflict (mode: Function argument combination (unification failed))])" ] }, "execution_count": 33, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = alfonso * (Binder(10) *\n", " (trace(10) * (want *\n", " (((an * (inexpensive * coat)) * (Binder(3) *\n", " (PRO(10) * (buy * trace(3)))))\n", " * None))))\n", "r" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Mixed (non-specific / transparent), quantifier scopes over `INT` but within clause:" ] }, { "cell_type": "code", "execution_count": 34, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]] alfonso]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Des}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Alfonso}_{e}, {w}_{s})) \\rightarrow{} \\exists{} x_{e} \\: . \\: (({Inexpensive}({x}, {w}_{s}) \\wedge{} {Coat}({x}, {w}_{s})) \\wedge{} {Buy}({Alfonso}_{e}, {x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[[10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]] alfonso]⟧[w_s, type s, g] = (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s)))))], failures=[⟦[alfonso [10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]]]⟧[w_s, type s, g] = Type mismatch: '⟦alfonso⟧[w_s, type s, g] = Alfonso_e'/e and '⟦[10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ conflict (mode: Function Application), ⟦[alfonso [10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]]]⟧[w_s, type s, g] = Type mismatch: '⟦alfonso⟧[w_s, type s, g] = Alfonso_e'/e and '⟦[10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ conflict (mode: Predicate Modification), ⟦[alfonso [10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]]]⟧[w_s, type s, g] = Type mismatch: '⟦alfonso⟧[w_s, type s, g] = Alfonso_e'/e and '⟦[10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ conflict (mode: Predicate Abstraction), ⟦[[10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]] alfonso]⟧[w_s, type s, g] = Type mismatch: '⟦[10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ and '⟦alfonso⟧[w_s, type s, g] = Alfonso_e'/e conflict (mode: Predicate Abstraction), ⟦[alfonso [10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]]]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and 'Alfonso_e'/e conflict (mode: Function argument combination (unification failed)), ⟦[[10 [[want [[an [inexpensive coat]] [3 INT([[buy t3] PRO10])]]] t10]] alfonso]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and '(λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(x1_e, w_s)) >> (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & Buy_<(e,e,s),t>(x1_e, x_e, w2_s))))))'/ conflict (mode: Function argument combination (unification failed))])" ] }, "execution_count": 34, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = alfonso * (Binder(10) *\n", " (trace(10) * (want *\n", " ((an * (inexpensive * coat)) * (Binder(3) *\n", " ((PRO(10) * (buy * trace(3)))\n", " * None))))))\n", "r" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Pure de re (specific/transparent), quantifier QRs all the way out across the non-finite clause boundary:" ] }, { "cell_type": "code", "execution_count": 35, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[an [inexpensive coat]] [3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: (({Inexpensive}({x}, {w}_{s}) \\wedge{} {Coat}({x}, {w}_{s})) \\wedge{} \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Des}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Alfonso}_{e}, {w}_{s})) \\rightarrow{} {Buy}({Alfonso}_{e}, {x}, {w2})))$" ], "text/plain": [ "CompositionResult(results=[⟦[[an [inexpensive coat]] [3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]]⟧[w_s, type s, g] = (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s)))))], failures=[⟦[[3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]] [an [inexpensive coat]]]⟧[w_s, type s, g] = Type mismatch: '⟦[3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s))))'/ and '⟦[an [inexpensive coat]]⟧[w_s, type s, g] = (λ g_: (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & g_(x_e))))'/<,t> conflict (mode: Function Application), ⟦[[an [inexpensive coat]] [3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '⟦[an [inexpensive coat]]⟧[w_s, type s, g] = (λ g_: (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & g_(x_e))))'/<,t> and '⟦[3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s))))'/ conflict (mode: Predicate Modification), ⟦[[an [inexpensive coat]] [3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '⟦[an [inexpensive coat]]⟧[w_s, type s, g] = (λ g_: (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & g_(x_e))))'/<,t> and '⟦[3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s))))'/ conflict (mode: Predicate Abstraction), ⟦[[3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]] [an [inexpensive coat]]]⟧[w_s, type s, g] = Type mismatch: '⟦[3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]⟧[w_s, type s, g] = (λ x_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s))))'/ and '⟦[an [inexpensive coat]]⟧[w_s, type s, g] = (λ g_: (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & g_(x_e))))'/<,t> conflict (mode: Predicate Abstraction), ⟦[[an [inexpensive coat]] [3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '((λ quant_<,t>: (λ f_>: (λ y_I799: quant_<,t>((λ x_e: f_>(x_e)(y_I799)))))))((λ g_: (Exists x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & g_(x_e)))))'/<>,> and '(λ x_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s))))'/ conflict (mode: Function argument combination (unification failed)), ⟦[[3 [[10 [[want INT([[buy t3] PRO10])] t10]] alfonso]] [an [inexpensive coat]]]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and '(λ x_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, x_e, w2_s))))'/ conflict (mode: Function argument combination (unification failed))])" ] }, "execution_count": 35, "metadata": {}, "output_type": "execute_result" } ], "source": [ "r = ((an * (inexpensive * coat)) * (Binder(3) *\n", " (alfonso * (Binder(10) * (trace(10) *\n", " (want *\n", " ((PRO(10) * (buy * trace(3)))\n", " * None)))))))\n", "r" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Fourth readings\n", "\n", "None of the systems above generate the so-called fourth reading: specific/opaque. This is because with QR as the scope mechanism, the QR target position provides a lower bound on the world binding, and this kind of reading would require a world binding that is local, but a quantifier position that is not. There has been some debate about whether the fourth reading exists, so perhaps this is a virtue: see Keshet 2011 footnotes 4,15 for an argument along these lines. However, Szabo in a 2010 Amsterdam Colloquium paper (*Specific, yet opaque*) provides fairly convincing cases of the fourth reading.\n", "\n", "If you do want to derive this reading, there are various options.\n", "* Szabo: add a new QR operation that moves only the determiner.\n", "* Do partial reconstruction of the NP from a pure de re reading into a position where the world variable for the NP gets locally bound. (For Percus, under the world binder, for Keshet or a type-shifting approach, under the `INT` operator.)\n", "\n", "Both of these are a bit convoluted. Here's a sketch of what Szabo's new QR operation would do. This operation moves a quantifier with a silent `thing` restrictor, and leaves a trace that gets interpreted via a variant (of sorts) of Fox's Trace Conversion rule. In Szabo's system, there is a specialized composition rule for this, but for the sake of simplicity, I just hard-code this in a specialized pre-indexed trace entry `rt3`.\n", "\n", "Unfortunately some of the simplification involved in this use of Iota is not currently implemented in the lambda notebook." ] }, { "cell_type": "code", "execution_count": 36, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$[\\![\\mathbf{\\text{thing}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {True}_{t}$
\n", "$[\\![\\mathbf{\\text{rt3}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: ({f}({x}) \\wedge{} ({x} = {var3}_{e}))$" ], "text/latex": [ "$[\\![\\mathbf{\\text{thing}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {True}_{t}$
\n", "$[\\![\\mathbf{\\text{rt3}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: ({f}({x}) \\wedge{} ({x} = {var3}_{e}))$" ], "text/plain": [ "$[\\![\\mathbf{\\text{thing}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {True}_{t}$
\n", "$[\\![\\mathbf{\\text{rt3}}]\\!]^{{w}_{s}, g}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: ({f}({x}) \\wedge{} ({x} = {var3}_{e}))$" ] }, "execution_count": 36, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%%lamb\n", "||thing|| = L x_e : True\n", "||rt3|| = L f_ : Iota x_e: f(x) & x==var3" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "First, it may be helpful to see a derivation without an intensional lexical item where this rule has applied. In the result, the formula will be false for any potential witnesses for the existential that don't verify the properties under the $\\iota$ operator, leading to equivalence with the standard truth-conditions. (This is not something that the lambda notebook knows how to simplify for you.)" ] }, { "cell_type": "code", "execution_count": 37, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[an thing] [3 [[buy [rt3 [inexpensive coat]]] alfonso]]]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: {Buy}({Alfonso}_{e}, \\iota{} x2_{e} \\: . \\: (({Inexpensive}({x2}, {w}_{s}) \\wedge{} {Coat}({x2}, {w}_{s})) \\wedge{} ({x2} = {x})), {w}_{s})$" ], "text/plain": [ "CompositionResult(results=[⟦[[an thing] [3 [[buy [rt3 [inexpensive coat]]] alfonso]]]⟧[w_s, type s, g] = (Exists x_e: Buy_<(e,e,s),t>(Alfonso_e, (ι x2_e: ((Inexpensive_<(e,s),t>(x2_e, w_s) & Coat_<(e,s),t>(x2_e, w_s)) & (x2_e <=> x_e))), w_s))], failures=[⟦[[3 [[buy [rt3 [inexpensive coat]]] alfonso]] [an thing]]⟧[w_s, type s, g] = Type mismatch: '⟦[3 [[buy [rt3 [inexpensive coat]]] alfonso]]⟧[w_s, type s, g] = (λ x1_e: Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & (x_e <=> x1_e))), w_s))'/ and '⟦[an thing]⟧[w_s, type s, g] = (λ g_: (Exists x_e: g_(x_e)))'/<,t> conflict (mode: Function Application), ⟦[[an thing] [3 [[buy [rt3 [inexpensive coat]]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '⟦[an thing]⟧[w_s, type s, g] = (λ g_: (Exists x_e: g_(x_e)))'/<,t> and '⟦[3 [[buy [rt3 [inexpensive coat]]] alfonso]]⟧[w_s, type s, g] = (λ x1_e: Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & (x_e <=> x1_e))), w_s))'/ conflict (mode: Predicate Modification), ⟦[[an thing] [3 [[buy [rt3 [inexpensive coat]]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '⟦[an thing]⟧[w_s, type s, g] = (λ g_: (Exists x_e: g_(x_e)))'/<,t> and '⟦[3 [[buy [rt3 [inexpensive coat]]] alfonso]]⟧[w_s, type s, g] = (λ x1_e: Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & (x_e <=> x1_e))), w_s))'/ conflict (mode: Predicate Abstraction), ⟦[[3 [[buy [rt3 [inexpensive coat]]] alfonso]] [an thing]]⟧[w_s, type s, g] = Type mismatch: '⟦[3 [[buy [rt3 [inexpensive coat]]] alfonso]]⟧[w_s, type s, g] = (λ x1_e: Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & (x_e <=> x1_e))), w_s))'/ and '⟦[an thing]⟧[w_s, type s, g] = (λ g_: (Exists x_e: g_(x_e)))'/<,t> conflict (mode: Predicate Abstraction), ⟦[[an thing] [3 [[buy [rt3 [inexpensive coat]]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '((λ quant_<,t>: (λ f_>: (λ y_I872: quant_<,t>((λ x_e: f_>(x_e)(y_I872)))))))((λ g_: (Exists x_e: g_(x_e))))'/<>,> and '(λ x1_e: Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & (x_e <=> x1_e))), w_s))'/ conflict (mode: Function argument combination (unification failed)), ⟦[[3 [[buy [rt3 [inexpensive coat]]] alfonso]] [an thing]]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and '(λ x1_e: Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w_s) & Coat_<(e,s),t>(x_e, w_s)) & (x_e <=> x1_e))), w_s))'/ conflict (mode: Function argument combination (unification failed))])" ] }, "execution_count": 37, "metadata": {}, "output_type": "execute_result" } ], "source": [ "((an * thing) * (Binder(3) * (alfonso * (buy * (rt3 * (inexpensive * coat))))))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Here is a fourth reading derivation, using Keshet's intensionalization operator from above." ] }, { "cell_type": "code", "execution_count": 38, "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", "
    [0]: $[\\![\\mathbf{\\text{[[an thing] [3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]]}}]\\!]^{{w}_{s}, g}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: \\forall{} w2_{s} \\: . \\: (({w2} \\in{} {Des}_{\\left\\langle{}\\left(e, s\\right),\\left\\{s\\right\\}\\right\\rangle{}}({Alfonso}_{e}, {w}_{s})) \\rightarrow{} {Buy}({Alfonso}_{e}, \\iota{} x2_{e} \\: . \\: (({Inexpensive}({x2}, {w2}) \\wedge{} {Coat}({x2}, {w2})) \\wedge{} ({x2} = {x})), {w2}))$" ], "text/plain": [ "CompositionResult(results=[⟦[[an thing] [3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]]⟧[w_s, type s, g] = (Exists x_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, (ι x2_e: ((Inexpensive_<(e,s),t>(x2_e, w2_s) & Coat_<(e,s),t>(x2_e, w2_s)) & (x2_e <=> x_e))), w2_s))))], failures=[⟦[[3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]] [an thing]]⟧[w_s, type s, g] = Type mismatch: '⟦[3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & (x_e <=> x1_e))), w2_s))))'/ and '⟦[an thing]⟧[w_s, type s, g] = (λ g_: (Exists x_e: g_(x_e)))'/<,t> conflict (mode: Function Application), ⟦[[an thing] [3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '⟦[an thing]⟧[w_s, type s, g] = (λ g_: (Exists x_e: g_(x_e)))'/<,t> and '⟦[3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & (x_e <=> x1_e))), w2_s))))'/ conflict (mode: Predicate Modification), ⟦[[an thing] [3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '⟦[an thing]⟧[w_s, type s, g] = (λ g_: (Exists x_e: g_(x_e)))'/<,t> and '⟦[3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & (x_e <=> x1_e))), w2_s))))'/ conflict (mode: Predicate Abstraction), ⟦[[3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]] [an thing]]⟧[w_s, type s, g] = Type mismatch: '⟦[3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]⟧[w_s, type s, g] = (λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & (x_e <=> x1_e))), w2_s))))'/ and '⟦[an thing]⟧[w_s, type s, g] = (λ g_: (Exists x_e: g_(x_e)))'/<,t> conflict (mode: Predicate Abstraction), ⟦[[an thing] [3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]]]⟧[w_s, type s, g] = Type mismatch: '((λ quant_<,t>: (λ f_>: (λ y_I974: quant_<,t>((λ x_e: f_>(x_e)(y_I974)))))))((λ g_: (Exists x_e: g_(x_e))))'/<>,> and '(λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & (x_e <=> x1_e))), w2_s))))'/ conflict (mode: Function argument combination (unification failed)), ⟦[[3 [[10 [[want INT([[buy [rt3 [inexpensive coat]]] PRO10])] t10]] alfonso]] [an thing]]⟧[w_s, type s, g] = Type mismatch: '(λ quant_<,t>: (λ f_>: (λ y_X: quant_<,t>((λ x_e: f_>(x_e)(y_X))))))'/<<,t>,<>,>> and '(λ x1_e: (Forall w2_s: ((w2_s << Des_<(e,s),{s}>(Alfonso_e, w_s)) >> Buy_<(e,e,s),t>(Alfonso_e, (ι x_e: ((Inexpensive_<(e,s),t>(x_e, w2_s) & Coat_<(e,s),t>(x_e, w2_s)) & (x_e <=> x1_e))), w2_s))))'/ conflict (mode: Function argument combination (unification failed))])" ] }, "execution_count": 38, "metadata": {}, "output_type": "execute_result" } ], "source": [ "((an * thing) * (Binder(3) * (alfonso * (Binder(10) *\n", " (trace(10) * (want * ((PRO(10) *\n", " (buy * (rt3 * (inexpensive * coat))))\n", " * None)))))))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Basically, the $\\iota$ condition on $x$s requires that any witness for the outer quantifier satisfy the properties inside the $\\iota$ condition, and so the formula is only true if there are values of $x$ that do satisfy these conditions. (Is it false or undefined if not? As I understand it, the intent is that it would be false. The Russellian model-theoretic interpretation for inverted $\\iota$ in, e.g., Gamut vol 1 sec 5.2 would derive the result needed.)\n", "\n", "In conclusion: I hope that if fourth readings are real, there is another way to derive them." ] }, { "cell_type": "code", "execution_count": 39, "metadata": {}, "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.6.4" } }, "nbformat": 4, "nbformat_minor": 2 }