{ "cells": [ { "cell_type": "code", "execution_count": 10, "id": "eaf064aa-385e-4467-8cfe-c361761e7436", "metadata": { "slideshow": { "slide_type": "skip" }, "tags": [] }, "outputs": [], "source": [ "import nltk\n", "import svgling\n", "from svgling.figure import Caption, SideBySide" ] }, { "cell_type": "markdown", "id": "b61be98a-c9cf-4ac1-9632-71fb53c89882", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "# Towards a basic composition system\n", "\n", "#### NASSLLI 2022: implementing semantic compositionality\n", "#### Kyle Rawlins, [kgr@jhu.edu](mailto:kgr@jhu.edu)\n", "#### Johns Hopkins University, Department of Cognitive Science\n", "\n", "Goal for today: see how a \"composition system\" is implemented in the lambda notebook, and how it can both used and extended." ] }, { "cell_type": "markdown", "id": "f124edd1-65bd-41c3-913f-afeae96e7750", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Recap: compositionality (preliminary)\n", "\n", "_\"Frege's Conjecture\"_: semantic composition is function application.\n", "\n", "* Linguistic structure $\\Rightarrow$ function-argument groupings\n", "* How can we implement this?" ] }, { "cell_type": "markdown", "id": "d00a9535-da72-45e5-9525-27d262feedb3", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Compositionality: Heim and Kratzer ch. 3\n", "\n", "Perhaps the most influential presentation of a compositional system in linguistics (p. 43-44):\n", "\n", "1. **TN**: If $\\alpha$ is a terminal node, then $[[\\alpha]]$ is specified in the lexicon.\n", "2. **NN**: If $\\alpha$ is a non-branching node, and $\\beta$ its daughter node, then $[[\\alpha]] = [[\\beta]]$.\n", "3. **FA**: If $\\gamma$ is a branching node, $\\{\\alpha, \\beta\\}$ the set of $\\gamma$'s daughters, and $[[\\alpha]]$ is a function whose domain contains $[[\\beta]]$, then $[[\\gamma]] = [[\\alpha]]([[\\beta]])$\n" ] }, { "cell_type": "markdown", "id": "91eb7f32-653e-4763-b6af-e307f9c5f79c", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Revisiting the toy example\n", "\n", "Arithmeticese: object language with one verb (\"is\"), two coordinators (\"plus\", \"times\"), various numbers (\"two\", \"four\", ...).\n", "* ignore numbers not in \\[1..9\\]\n", "* Let's assume a binary branching syntax, including for coordinators.\n", "* Python already has the metalanguage that we need..\n", "\n", "\n", "```\n", "(1) Two plus two is four\n", "```" ] }, { "cell_type": "code", "execution_count": 11, "id": "324606a3-6dc5-4a5e-9b17-f3a2ab9cbe57", "metadata": { "tags": [ "hide_input" ] }, "outputs": [ { "data": { "image/svg+xml": [ "twoplustwoisfour" ], "text/plain": [ "Tree('', [Tree('', [Tree('two', []), Tree('', [Tree('plus', []), 'two'])]), Tree('', [Tree('is', []), 'four'])])" ] }, "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "nltk.Tree.fromstring(\"(((two) ((plus) two)) ((is) four))\")" ] }, { "cell_type": "markdown", "id": "0540df8d-4d91-47fb-830f-3a382766494a", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Arithmeticese: a pure python implementation" ] }, { "cell_type": "code", "execution_count": 12, "id": "1db1dd8e-1036-44e9-98f4-dd143ab3b37b", "metadata": {}, "outputs": [], "source": [ "# this is one way to write a \"curried\" function in python:\n", "def plus(x):\n", " return lambda y: y + x\n", "\n", "def isV(x): # `is` is a python reserved word\n", " return lambda y: x == y\n", "\n", "def two():\n", " return 2\n", "\n", "def four():\n", " return 4" ] }, { "cell_type": "code", "execution_count": 13, "id": "d7994f8e-61df-48d8-a646-4f5159619dc6", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/plain": [ "6" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "plus(two())(four())" ] }, { "cell_type": "code", "execution_count": 14, "id": "a401fa8a-9a48-43c6-a6d4-c5e9ee1372b6", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "isV(plus(two())(two()))(four())" ] }, { "cell_type": "markdown", "id": "219e8bf2-a94b-4aa8-8022-1a24bd8fe583", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "Weirdly adequate along a number of dimensions. But?" ] }, { "cell_type": "markdown", "id": "8c76891f-8212-4497-945f-3a0a625d0439", "metadata": { "slideshow": { "slide_type": "fragment" }, "tags": [] }, "source": [ "1. No object/meta-language distinction.\n", "2. Arity enforcement, but no type enforcement.\n", "3. Works, but can't inspect how it works.\n", "4. Relies on the relevant metalanguage operations being present in the programming language." ] }, { "cell_type": "code", "execution_count": 15, "id": "c95f767d-afb0-49cd-8c6a-2c10279060f9", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/plain": [ "False" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "isV(two())(plus)" ] }, { "cell_type": "code", "execution_count": 16, "id": "643f74ee-e96f-435e-b981-d2b17f5970e3", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "5" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "plus(isV(two())(two()))(four())" ] }, { "cell_type": "code", "execution_count": 17, "id": "859f4f24-ba7d-4cd3-8215-7486260c8e3e", "metadata": {}, "outputs": [ { "data": { "text/plain": [ ".(y)>" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "plus(two())" ] }, { "cell_type": "code", "execution_count": 18, "id": "bd5632b5-4791-47ed-9c10-7fb956fcc642", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "ename": "TypeError", "evalue": "unsupported operand type(s) for +: 'int' and 'function'", "output_type": "error", "traceback": [ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", "\u001b[0;31mTypeError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m/var/folders/wg/hnp9tqsn313f9dst_84rmsw80000gn/T/ipykernel_27872/4159620212.py\u001b[0m in \u001b[0;36m\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mplus\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0misV\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwo\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;31m# finally, an error\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", "\u001b[0;32m/var/folders/wg/hnp9tqsn313f9dst_84rmsw80000gn/T/ipykernel_27872/1325836745.py\u001b[0m in \u001b[0;36m\u001b[0;34m(y)\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0;31m# this is one way to write a \"curried\" function in python:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 2\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0mplus\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mx\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 3\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0;32mlambda\u001b[0m \u001b[0my\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0my\u001b[0m \u001b[0;34m+\u001b[0m \u001b[0mx\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 4\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 5\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0misV\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mx\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0;31m# `is` is a python reserved word\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mTypeError\u001b[0m: unsupported operand type(s) for +: 'int' and 'function'" ] } ], "source": [ "plus(isV)(two()) # finally, an error" ] }, { "cell_type": "markdown", "id": "d1f6de45-5dce-4b0b-a8ea-185dfa51883a", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "If you're a python hacker, you might come up with something like this as a solution to 1:" ] }, { "cell_type": "code", "execution_count": 19, "id": "f069f940-e705-4dca-9a29-7aa03a5f2300", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "4" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "lexicon = {\"two\": two(),\n", " \"four\": four(),\n", " \"plus\": plus,\n", " \"is\": isV}\n", "\n", "lexicon[\"plus\"](lexicon[\"two\"])(lexicon[\"two\"])" ] }, { "cell_type": "markdown", "id": "c37f8ddb-d9d6-466f-9d73-c8a6966e65eb", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "Even better, we can abstract the notion of \"composition\" into a function:" ] }, { "cell_type": "code", "execution_count": 20, "id": "49e168af-0f8c-4131-b26c-f261f6119b51", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/plain": [ "4" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "def compose(f, a, lex):\n", " # try looking up f and a in the lexicon, otherwise take them as given\n", " if f in lex:\n", " f = lex[f]\n", " if a in lex:\n", " a = lex[a]\n", " return f(a)\n", "\n", "compose(compose(\"plus\", \"two\", lexicon), \"two\", lexicon)" ] }, { "cell_type": "markdown", "id": "155ab78e-7add-4f4c-a3b4-d6c50fd68a78", "metadata": {}, "source": [ "This is essentially what we are aiming at!" ] }, { "cell_type": "markdown", "id": "0a9fe81f-013b-4f0f-a4fa-ed93bd0f050e", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "But, we need a real solution to 1-4:\n", "\n", "1. Object/meta-language distinction.\n", "2. Type enforcement.\n", "3. Introspection / derivational history.\n", "4. Expanding out the logical metalanguage beyond python (which essentially includes an extensional propositional logic only).\n", "\n", "**Abstract these ideas** into general functions and classes." ] }, { "cell_type": "markdown", "id": "46ecfe0d-84e5-4f41-9914-f451a3fb91ca", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Side note on the choice of languages\n", "\n", "Worth noting that other people doing this work often have picked Haskell exactly because it is arguably a better fit for the task than python.\n", "* Cf. the van Eijck and Unger 2010 text mentioned yesterday.\n", "* Haskell is a functional, strongly typed, programming language.\n", "* Its type system is adaptable/powerful, and can easily line up with what linguists typically assume.\n", "\n", "Flip-side: it is not \"mainstream\" or especially easy to learn. It is not a good first language. It isn't widely in demand in industry jobs. It is not used for introductory computing courses.\n", "* (Jupyter integration is also an advantage, but, there is actually a Haskell [Jupyter kernel](https://github.com/IHaskell/IHaskell)!)" ] }, { "cell_type": "markdown", "id": "4d86d55b-250b-43d8-abf5-9925dbb8ea24", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## A starting point: how to implement function application?\n", "\n", "**Function Application**: given two linguistic objects, one which is a function $f$ and the other an appropriate argument $a$, the result of composition is $f(a)$.\n", "\n", "In a nutshell: all the work is in the metalanguage, in particular, getting a good implementation of _beta reduction_.\n", "\n" ] }, { "cell_type": "markdown", "id": "47f39549-8a67-477d-a436-27534da74434", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Simple types\n", "\n", "Standard(ish) setup:\n", "\n", "1. e, n, t are types\n", "2. if $\\alpha, \\beta$ are types, then so is $\\langle \\alpha, \\beta \\rangle$\n", "3. nothing else is a type\n", "\n", "If $f$ has type $\\langle \\alpha, \\beta \\rangle$, then $f$ is a function from things of type $\\alpha$ to things of type $\\beta$.\n", " * That is $\\langle \\cdot, \\cdot \\rangle$ is a \"type constructor\" for functional types.\n", " * Let's set aside implementation questions for types for the moment." ] }, { "cell_type": "markdown", "id": "0fcc8ee2-4232-496c-a248-399b3e727a0f", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### A standard definition of Function Application\n", "\n", "(After Heim and Kratzer 1998, Coppock and Champollion's 2022 [Invitation to Formal Semantics](https://eecoppock.info/bootcamp/semantics-boot-camp.pdf) ch. 6)\n", "\n", "If $\\gamma$ is a syntax tree whose subtrees are $\\alpha$ and $\\beta$, where:\n", "* $[[\\alpha]]$ has type $\\langle \\sigma, \\tau \\rangle$\n", "* $[[\\beta]]$ has type $\\sigma$\n", "\n", "Then, $[[\\gamma]] = [[\\alpha]]([[\\beta]])$\n", "\n" ] }, { "cell_type": "code", "execution_count": 21, "id": "855f5447-428d-4063-8f88-d5792065f8fc", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "$[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", "$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$" ], "text/latex": [ "$[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", "$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$" ], "text/plain": [ "$[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", "$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "%%lamb\n", "||two|| = 2\n", "||plus|| = L x_n : L y_n : x + y" ] }, { "cell_type": "code", "execution_count": 22, "id": "b1da5f10-6806-41c9-bd60-3dcea17b4a79", "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", " [0]: $[\\![\\mathbf{\\text{[plus two]}}]\\!]^{}_{\\left\\langle{}n,n\\right\\rangle{}} \\:=\\: $$\\lambda{} y_{n} \\: . \\: ({2} + {y})$" ], "text/plain": [ "CompositionResult(results=[⟦[plus two]⟧ = (λ y_n: (2_n + y_n))], failures=[⟦[two plus]⟧ = Type mismatch: '⟦two⟧ = 2_n'/n and '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> conflict (Function Application), ⟦[plus two]⟧ = Type mismatch: '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> and '⟦two⟧ = 2_n'/n conflict (Predicate Modification), ⟦[plus two]⟧ = Composition failure (PA requires a valid binder) on: ⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n))) * ⟦two⟧ = 2_n, ⟦[two plus]⟧ = Composition failure (PA requires a valid binder) on: ⟦two⟧ = 2_n * ⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n))), ⟦[plus two]⟧ = Type mismatch: '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> and '⟦two⟧ = 2_n'/n conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "plus * two # let's switch to notebook and play around with this a bit" ] }, { "cell_type": "code", "execution_count": 23, "id": "0c9528ee-1209-4050-9084-4977e97c8f5e", "metadata": {}, "outputs": [ { "data": { "text/html": [ "Full composition trace. 1 path:\n", " Step 1: $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$\n", " Step 2: $[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", " Step 3: $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{two}}]\\!]^{}_{n}$ leads to: $[\\![\\mathbf{\\text{[plus two]}}]\\!]^{}_{\\left\\langle{}n,n\\right\\rangle{}} \\:=\\: $$\\lambda{} y_{n} \\: . \\: ({2} + {y})$ [by FA]\n" ], "text/latex": [ "Full composition trace. 1 path:\n", " Step 1: $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$\n", " Step 2: $[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", " Step 3: $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{two}}]\\!]^{}_{n}$ leads to: $[\\![\\mathbf{\\text{[plus two]}}]\\!]^{}_{\\left\\langle{}n,n\\right\\rangle{}} \\:=\\: $$\\lambda{} y_{n} \\: . \\: ({2} + {y})$ [by FA]\n" ], "text/plain": [ "Full composition trace. 1 path:\n", " Step 1: $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$\n", " Step 2: $[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", " Step 3: $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{two}}]\\!]^{}_{n}$ leads to: $[\\![\\mathbf{\\text{[plus two]}}]\\!]^{}_{\\left\\langle{}n,n\\right\\rangle{}} \\:=\\: $$\\lambda{} y_{n} \\: . \\: ({2} + {y})$ [by FA]" ] }, "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ "(plus * two).trace()" ] }, { "cell_type": "markdown", "id": "3deeb02d-f77d-4862-9c5f-6402ccbda0ed", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Function Application, procedurally\n", "\n", "For `a * b`:\n", "\n", "1. if `a.content` is a function, and `b.content` is an appropriate argument, then:\n", " 1. return `[[a b]] = a.content(b.content)`\n", "2. if `b.content` is a function, and `a.content` is an appropriate argument, then:\n", " 1. return `[[a b]] = b.content(a.content)`\n", "3. otherwise, fail" ] }, { "cell_type": "code", "execution_count": 24, "id": "0339d961-d49d-4feb-8c83-1dac5f1c3908", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "Composition of [plus plus] failed:\n", " Type mismatch: '$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$'/$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$ and '$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$'/$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$ conflict (Function Application)\n", " Type mismatch: '$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$'/$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$ and '$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$'/$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$ conflict (Function Application)\n", " Type mismatch: '$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$'/$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$ and '$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$'/$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$ conflict (Predicate Modification)\n", " Composition failure (PA requires a valid binder) on: $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$ * $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$\n", " Composition failure (PA requires a valid binder) on: $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$ * $[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$\n", " Type mismatch: '$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$'/$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$ and '$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$'/$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$ conflict (Need at least one fully vacuous element)\n" ], "text/plain": [ "CompositionResult(results=[], failures=[⟦[plus plus]⟧ = Type mismatch: '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> and '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> conflict (Function Application), ⟦[plus plus]⟧ = Type mismatch: '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> and '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> conflict (Function Application), ⟦[plus plus]⟧ = Type mismatch: '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> and '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> conflict (Predicate Modification), ⟦[plus plus]⟧ = Composition failure (PA requires a valid binder) on: ⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n))) * ⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n))), ⟦[plus plus]⟧ = Composition failure (PA requires a valid binder) on: ⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n))) * ⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n))), ⟦[plus plus]⟧ = Type mismatch: '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> and '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 24, "metadata": {}, "output_type": "execute_result" } ], "source": [ "plus * plus" ] }, { "cell_type": "markdown", "id": "2d5d0cdc-1fe9-4c89-b805-1e316c031d38", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Metalanguage objects\n", "\n", "The lambda notebook metalanguage is implemented via structured python objects that all share a common programmatic inferface." ] }, { "cell_type": "markdown", "id": "4bd20968-9320-421b-94fe-14214d94f042", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "The `%te` line magic (mnemonic: typed expression) lets you quickly build metalanguage objects:" ] }, { "cell_type": "code", "execution_count": 25, "id": "006c4b2a-589e-4811-92a5-31dd3fc50d5b", "metadata": {}, "outputs": [ { "data": { "text/latex": [ "$({p}_{t} \\wedge{} {q}_{t})$" ], "text/plain": [ "(p_t & q_t)" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "'&'" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "$t$" ], "text/plain": [ "t" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "[p_t, q_t]" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "lamb.meta.BinaryAndExpr" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "formula = %te p_t & q_t\n", "display(formula)\n", "display(formula.op) # typed expressions (may) have an operator\n", "display(formula.type) # typed expressions have a type\n", "display(list(formula)) # typed expressions have parts\n", "display(formula.__class__) # the python type of `formula`" ] }, { "cell_type": "code", "execution_count": 26, "id": "56187089-ec6c-423f-809d-8684f9b664c0", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/latex": [ "${p}_{t}$" ], "text/plain": [ "p_t" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "$t$" ], "text/plain": [ "t" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "lamb.meta.TypedTerm" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "# let's look at a part:\n", "display(formula[0])\n", "display(formula[0].type)\n", "display(formula[0].__class__)" ] }, { "cell_type": "markdown", "id": "f7d5cede-a421-4ab8-86c8-2cda659da294", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Metalanguage functions" ] }, { "cell_type": "markdown", "id": "f6bd1e10-edae-4ffd-a84a-7c746a0bcc25", "metadata": {}, "source": [ "Let's look a bit at a metalanguage function. Its parts are the variable, and the body, and its type is guaranteed to be a functional type." ] }, { "cell_type": "code", "execution_count": 27, "id": "f1094ac0-e48a-43ac-8c81-07926bc4b16a", "metadata": {}, "outputs": [ { "data": { "text/latex": [ "$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$" ], "text/plain": [ "(λ x_n: (λ y_n: (x_n + y_n)))" ] }, "execution_count": 27, "metadata": {}, "output_type": "execute_result" } ], "source": [ "f = %te L x_n : L y_n : x + y\n", "x = %te 2\n", "f" ] }, { "cell_type": "code", "execution_count": 28, "id": "76313658-58f7-4a42-b844-f56f6febf373", "metadata": {}, "outputs": [ { "data": { "text/latex": [ "$\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}$" ], "text/plain": [ ">" ] }, "execution_count": 28, "metadata": {}, "output_type": "execute_result" } ], "source": [ "f.type" ] }, { "cell_type": "code", "execution_count": 29, "id": "ebabf51b-af3c-4373-ae3e-2759513ba0e3", "metadata": {}, "outputs": [ { "data": { "text/latex": [ "${x}_{n}$" ], "text/plain": [ "x_n" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "$\\lambda{} y_{n} \\: . \\: ({x}_{n} + {y})$" ], "text/plain": [ "(λ y_n: (x_n + y_n))" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display(f[0], f[1])" ] }, { "cell_type": "markdown", "id": "13e2d103-c279-42bb-900b-5bfff1b83820", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Function-argument combination\n", "\n", "When a function combines with an argument, it builds a composite expression (an \"application expression\"):" ] }, { "cell_type": "code", "execution_count": 30, "id": "9044269e-1986-416b-b895-192a4a6efd5e", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/latex": [ "${[\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})]}({2})$" ], "text/plain": [ "((λ x_n: (λ y_n: (x_n + y_n))))(2_n)" ] }, "execution_count": 30, "metadata": {}, "output_type": "execute_result" } ], "source": [ "x = %te 2\n", "f(x)" ] }, { "cell_type": "code", "execution_count": 31, "id": "607b03ef-8231-4b3c-b2cf-8ac0fe839a57", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "lamb.meta.ApplicationExpr" ] }, "execution_count": 31, "metadata": {}, "output_type": "execute_result" } ], "source": [ "f(x).__class__" ] }, { "cell_type": "markdown", "id": "b2a1d1eb-33e8-4d12-bf17-f2b8f5acc27d", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "Reduction can be triggered by calling the function `reduce()`. (This works on any meta-language object, but most things aren't reducible!)" ] }, { "cell_type": "code", "execution_count": 32, "id": "109e5959-6da8-4b33-b368-2ab42cfa73bd", "metadata": {}, "outputs": [ { "data": { "text/html": [ " 1. ${[\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})]}({2})$ 2. $\\lambda{} y_{n} \\: . \\: ({2} + {y})$Reduction" ], "text/plain": [ " 1. ((λ x_n: (λ y_n: (x_n + y_n))))(2_n)\n", " 2. (λ y_n: (2_n + y_n)) (Reduction)" ] }, "execution_count": 32, "metadata": {}, "output_type": "execute_result" } ], "source": [ "f(x).reduce().derivation" ] }, { "cell_type": "markdown", "id": "a67dcf34-3d59-41d3-acac-62073a54e69a", "metadata": {}, "source": [ "All of the hard work is done in this function." ] }, { "cell_type": "markdown", "id": "a9b026aa-b7f3-4e04-813e-fc01504ef559", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Variable capture and renaming\n", "\n", "What is hard here? Consider the following case (based on an example in Partee, ter Meulen and Wall 1993, _Mathematical Methods in Linguistics_):" ] }, { "cell_type": "code", "execution_count": 33, "id": "e622f50f-abab-4149-af87-71c4f28c970c", "metadata": {}, "outputs": [ { "data": { "text/latex": [ "$\\lambda{} y_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: ({P}({x}) \\wedge{} {Q}({y}))$" ], "text/plain": [ "(λ y_e: (λ x_e: (P_(x_e) & Q_(y_e))))" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "${x}_{e}$" ], "text/plain": [ "x_e" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "${[\\lambda{} y_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: ({P}({x}) \\wedge{} {Q}({y}))]}({x}_{e})$" ], "text/plain": [ "((λ y_e: (λ x_e: (P_(x_e) & Q_(y_e)))))(x_e)" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "f1 = %te L y_e : L x_e : P_(x) & Q_(y)\n", "x = %te x_e\n", "\n", "display(f1, x, f1(x))" ] }, { "cell_type": "markdown", "id": "10f96284-82c8-4859-b7ec-fdbfdf9687ed", "metadata": {}, "source": [ "How should we reduce this? Need to _alpha-convert_ the bound variable:" ] }, { "cell_type": "code", "execution_count": 34, "id": "309e972d-d49b-4212-948a-b951c18b223b", "metadata": { "slideshow": { "slide_type": "subslide" }, "tags": [] }, "outputs": [ { "data": { "text/latex": [ "$\\lambda{} x1_{e} \\: . \\: ({P}({x1}) \\wedge{} {Q}({x}_{e}))$" ], "text/plain": [ "(λ x1_e: (P_(x1_e) & Q_(x_e)))" ] }, "execution_count": 34, "metadata": {}, "output_type": "execute_result" } ], "source": [ "f1(x).reduce_all()" ] }, { "cell_type": "markdown", "id": "f2aa44bb-eee7-490c-b21c-eb97b2582c60", "metadata": { "slideshow": { "slide_type": "fragment" }, "tags": [] }, "source": [ "That is, where reduction would result in a name collision between bound variables, the variables must be systematically renamed. The following would be wrong: $\\lambda x_e . P(x) \\wedge Q(x)$" ] }, { "cell_type": "markdown", "id": "c22e94d2-0031-4c80-a364-20811a42b556", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### A naive reduction algorithm\n", "\n", "Pseudocode. Given a `LFun` object `f`, and an arbitrary `TypedExpr` argument `a`:\n", "\n", "1. Check if `f.type` is compatible with `a.type`\n", "2. Return `f[1].subst(f[0], a)` (substitute instances of `f[0]` in `f[1]` with `a`)\n", "\n", "Where `t.subst(var, a)`:\n", "1. if `t` is a variable named `var`, return `a`\n", "2. otherwise, for all parts `i` in `t`:\n", " a. `t[i] = t[i].subst(var, a)`\n", " b. return the modified `t`\n" ] }, { "cell_type": "markdown", "id": "dcc1c955-f061-4962-928f-4d964233062c", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Adding in alpha conversion\n", "\n", "Rather subtle to get right! Somewhat imperfect sketch:\n", "\n", "1. find the set `blocklist` of variables used in `f` or in `a`\n", "2. find potential collisions between `f[0]` and any variables in `a`\n", "3. if there is a collision:\n", " a. find a variable name `x` not in `blocklist`\n", " b. systematically replace all bound instances in `f[1]` with `x`\n", "4. The tricky part: now we need to recurse and apply this to any lambda terms _within_ `f[1]`, avoiding collisions as well with the renames so far.\n", "\n", "* Note: this is definitely still a \"naive\" algorithm, and can be made much more efficient. (See [director strings](https://link.springer.com/chapter/10.1007/3-540-44881-0_5))\n", "* Note: if a single reduction would substitute in a way that would feed a second reduction, alpha conversion needs to be run separately for that step." ] }, { "cell_type": "code", "execution_count": 35, "id": "07cbbc90-ef82-4b5c-aa16-5fc8d250eef2", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/latex": [ "$\\lambda{} x_{e} \\: . \\: {[\\lambda{} y_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: ({P}({x}) \\wedge{} {Q}({y}))]}({x})$" ], "text/plain": [ "(λ x_e: ((λ y_e: (λ x_e: (P_(x_e) & Q_(y_e)))))(x_e))" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "$\\lambda{} x_{e} \\: . \\: \\lambda{} x1_{e} \\: . \\: ({P}({x1}) \\wedge{} {Q}({x}))$" ], "text/plain": [ "(λ x_e: (λ x1_e: (P_(x1_e) & Q_(x_e))))" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "t2 = %te L x_e : (L y_e : L x_e : P_(x) & Q_(y))(x_e)\n", "display(t2, t2.reduce_all())" ] }, { "cell_type": "code", "execution_count": 36, "id": "8b5c36e9-c81a-4ef8-93ce-941d74f57227", "metadata": {}, "outputs": [ { "data": { "text/latex": [ "${[\\lambda{} x_{e} \\: . \\: {[\\lambda{} y_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: ({P}({x}) \\wedge{} {Q}({y}))]}({x})]}({y}_{e})$" ], "text/plain": [ "((λ x_e: ((λ y_e: (λ x_e: (P_(x_e) & Q_(y_e)))))(x_e)))(y_e)" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "${[\\lambda{} y1_{e} \\: . \\: \\lambda{} x_{e} \\: . \\: ({P}({x}) \\wedge{} {Q}({y1}))]}({y}_{e})$" ], "text/plain": [ "((λ y1_e: (λ x_e: (P_(x_e) & Q_(y1_e)))))(y_e)" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "$\\lambda{} x1_{e} \\: . \\: ({P}({x1}) \\wedge{} {Q}({y}_{e}))$" ], "text/plain": [ "(λ x1_e: (P_(x1_e) & Q_(y_e)))" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "t3 = %te (L x_e : (L y_e : L x_e : P_(x) & Q_(y))(x_e))(y_e)\n", "display(t3, t3.reduce(), t3.reduce_all())" ] }, { "cell_type": "markdown", "id": "93dd065a-4a6f-46b1-80b9-4fb0fb66bfc4", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "***\n", "## Embedding metalanguage in semantic composition" ] }, { "cell_type": "code", "execution_count": 37, "id": "d54d133d-0d0a-4b2a-a0f3-3702e2cad083", "metadata": {}, "outputs": [ { "data": { "text/html": [ "$[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", "$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$" ], "text/latex": [ "$[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", "$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$" ], "text/plain": [ "$[\\![\\mathbf{\\text{two}}]\\!]^{}_{n} \\:=\\: $${2}$\n", "$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "%%lamb\n", "||two|| = 2\n", "||plus|| = L x_n : L y_n : x + y" ] }, { "cell_type": "markdown", "id": "6a11433e-277e-4ee7-886f-ed5c05a560b5", "metadata": {}, "source": [ "What is the nature of these sorts of definitions?" ] }, { "cell_type": "markdown", "id": "8df6a61a-e135-41fd-9d33-237cb1f9f143", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Items\n", "\n", "`two` and `plus` in this example are python _objects_ of class `lang.Item`. (`lang` is one of the lambda notebook modules.)\n", "\n", "* An `Item` is essentially a mapping between a string, representing an object language item, and a single metalanguage object." ] }, { "cell_type": "code", "execution_count": 38, "id": "5bc9d944-f526-49b3-b112-a5b1c24ee854", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "'plus'" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/latex": [ "$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$" ], "text/plain": [ "(λ x_n: (λ y_n: (x_n + y_n)))" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display(plus.name, plus.content)" ] }, { "cell_type": "markdown", "id": "e37d450a-d9ec-4c00-b272-98eb20956801", "metadata": { "slideshow": { "slide_type": "subslide" }, "tags": [] }, "source": [ "### Objects and classes (object-oriented-programming basics)\n", "\n", "A python _object_ is a bundle of data and behaviors, specified by its _class_\n", "* _data_: named variables that are part of the object, e.g. `plus.name`\n", "* _behavior_: functions that interact with some of the object's data in some way\n", "\n", "Example: `TypedExpr` is the main metalanguage class, and contains code for type inference, frontend rendering, reduction, variable substitution, etc.\n", "* Other metalanguage objects are _subclasses_ of `TypedExpr`, which means that they extend its behavior in various ways (while keeping the core behavior)." ] }, { "cell_type": "markdown", "id": "f5e259d2-e4cf-4085-9b00-8347addcfbbc", "metadata": { "slideshow": { "slide_type": "subslide" }, "tags": [] }, "source": [ "Interesting behavior change: you can change the behavior of most python operators by defining a special class function. E.g. `__call__` lets you change what happens when you use the standard function-argument python notation.\n", "\n", "Metalanguage `TypedExpr`s redefine `__call__` so that you can use this notation:" ] }, { "cell_type": "code", "execution_count": 39, "id": "88c505e0-c29f-4bc6-be6c-cd787ea6860c", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Cat_t' into , to match argument 'x_e'\n" ] }, { "data": { "text/latex": [ "${[\\lambda{} x_{e} \\: . \\: {Cat}({x})]}({A}_{e})$" ], "text/plain": [ "((λ x_e: Cat_(x_e)))(A_e)" ] }, "execution_count": 39, "metadata": {}, "output_type": "execute_result" } ], "source": [ "f = %te L x_e : Cat(x)\n", "x = %te A_e\n", "f(x)" ] }, { "cell_type": "markdown", "id": "75a5aac8-47c0-40aa-b19e-b6d6891a1369", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Composables, etc\n", "\n", "The `Item` class is a special case of a general abstract type called `Composable`. Any object that can undergo composition has this type.\n", "* This class is mostly \"glue\", but is where the `*` operator is implemented, via the `__mul__` special function.\n", "* The `lamb.lang` module contains a variety of subclasses of `Composable`, and mostly you don't need to know which is which." ] }, { "cell_type": "markdown", "id": "1b53feb0-0488-4f22-96f6-3988b13af5f0", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### CompositionResults" ] }, { "cell_type": "code", "execution_count": 40, "id": "0256c794-d7af-4a7f-9b17-454314799bc9", "metadata": { "tags": [] }, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", " [0]: $[\\![\\mathbf{\\text{[plus two]}}]\\!]^{}_{\\left\\langle{}n,n\\right\\rangle{}} \\:=\\: $$\\lambda{} y_{n} \\: . \\: ({2} + {y})$" ], "text/plain": [ "CompositionResult(results=[⟦[plus two]⟧ = (λ y_n: (2_n + y_n))], failures=[⟦[two plus]⟧ = Type mismatch: '⟦two⟧ = 2_n'/n and '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> conflict (Function Application), ⟦[plus two]⟧ = Type mismatch: '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> and '⟦two⟧ = 2_n'/n conflict (Predicate Modification), ⟦[plus two]⟧ = Composition failure (PA requires a valid binder) on: ⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n))) * ⟦two⟧ = 2_n, ⟦[two plus]⟧ = Composition failure (PA requires a valid binder) on: ⟦two⟧ = 2_n * ⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n))), ⟦[plus two]⟧ = Type mismatch: '⟦plus⟧ = (λ x_n: (λ y_n: (x_n + y_n)))'/> and '⟦two⟧ = 2_n'/n conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 40, "metadata": {}, "output_type": "execute_result" } ], "source": [ "result = plus * two\n", "result" ] }, { "cell_type": "markdown", "id": "9ae3f561-30d6-4af9-beec-09cffe776144", "metadata": {}, "source": [ "`result` here is a python object of class `lang.CompositionResult`.\n", "* a `CompositionResult` is a set of mappings between input `Composable`s and output metalanguage objects.\n", "* this class is itself a `Composable`." ] }, { "cell_type": "code", "execution_count": 41, "id": "a22192ad-8afe-4165-bfcf-f1f6459cc639", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "$[\\![\\mathbf{\\text{plus}}]\\!]^{}_{\\left\\langle{}n,\\left\\langle{}n,n\\right\\rangle{}\\right\\rangle{}}$$\\lambda{} x_{n} \\: . \\: \\lambda{} y_{n} \\: . \\: ({x} + {y})$*$[\\![\\mathbf{\\text{two}}]\\!]^{}_{n}$${2}$[FA]$[\\![\\mathbf{\\text{[plus two]}}]\\!]^{}_{\\left\\langle{}n,n\\right\\rangle{}}$$\\lambda{} y_{n} \\: . \\: ({2} + {y})$" ], "text/plain": [ "DisplayNode instance: HTML rendering only" ] }, "execution_count": 41, "metadata": {}, "output_type": "execute_result" } ], "source": [ "result.results[0].tree()" ] }, { "cell_type": "code", "execution_count": 42, "id": "4d178cf7-2ca5-4101-a9c9-7d049673c34c", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "'[plus two]'" ] }, "execution_count": 42, "metadata": {}, "output_type": "execute_result" } ], "source": [ "result.source" ] }, { "cell_type": "markdown", "id": "e1f3dcee-ef09-4da5-9b75-90e2b8d5dc0f", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Ambiguity in CompositionResults\n", "\n", "A `CompositionResult` can contain multiple results, representing ambiguity. For example, via lexical ambiguity. Here's the lexical notation to do this in the lambda notebook:" ] }, { "cell_type": "code", "execution_count": 43, "id": "e36b30e5-0719-46ed-a77d-168562c9a427", "metadata": {}, "outputs": [ { "data": { "text/html": [ "$[\\![\\mathbf{\\text{bank[0]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Riverbank}({x})$\n", "$[\\![\\mathbf{\\text{bank[1]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Moneybank}({x})$\n", "$[\\![\\mathbf{\\text{the}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({x})$" ], "text/latex": [ "$[\\![\\mathbf{\\text{bank[0]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Riverbank}({x})$\n", "$[\\![\\mathbf{\\text{bank[1]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Moneybank}({x})$\n", "$[\\![\\mathbf{\\text{the}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({x})$" ], "text/plain": [ "$[\\![\\mathbf{\\text{bank[0]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Riverbank}({x})$\n", "$[\\![\\mathbf{\\text{bank[1]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Moneybank}({x})$\n", "$[\\![\\mathbf{\\text{the}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},e\\right\\rangle{}} \\:=\\: $$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\iota{} x_{e} \\: . \\: {f}({x})$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "%%lamb\n", "||bank|| = L x_e : Riverbank_(x)\n", "||bank[*]|| = L x_e : Moneybank_(x)\n", "||the|| = L f_ : Iota x_e : f(x)" ] }, { "cell_type": "code", "execution_count": 44, "id": "af7e3c8a-7c76-4c1f-9e38-b53cc4b60243", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "2 composition paths. Results:\n", " [0]: $[\\![\\mathbf{\\text{[the bank]}}]\\!]^{}_{e} \\:=\\: $$\\iota{} x_{e} \\: . \\: {Riverbank}({x})$\n", " [1]: $[\\![\\mathbf{\\text{[the bank]}}]\\!]^{}_{e} \\:=\\: $$\\iota{} x_{e} \\: . \\: {Moneybank}({x})$" ], "text/plain": [ "CompositionResult(results=[⟦[the bank]⟧ = (ι x_e: Riverbank_(x_e)), ⟦[the bank]⟧ = (ι x_e: Moneybank_(x_e))], failures=[⟦[bank the]⟧ = Type mismatch: '⟦bank⟧ = (λ x_e: Riverbank_(x_e))'/ and '⟦the⟧ = (λ f_: (ι x_e: f_(x_e)))'/<,e> conflict (Function Application), ⟦[the bank]⟧ = Type mismatch: '⟦the⟧ = (λ f_: (ι x_e: f_(x_e)))'/<,e> and '⟦bank⟧ = (λ x_e: Riverbank_(x_e))'/ conflict (Predicate Modification), ⟦[the bank]⟧ = Composition failure (PA requires a valid binder) on: ⟦the⟧ = (λ f_: (ι x_e: f_(x_e))) * ⟦bank⟧ = (λ x_e: Riverbank_(x_e)), ⟦[bank the]⟧ = Composition failure (PA requires a valid binder) on: ⟦bank⟧ = (λ x_e: Riverbank_(x_e)) * ⟦the⟧ = (λ f_: (ι x_e: f_(x_e))), ⟦[the bank]⟧ = Type mismatch: '⟦the⟧ = (λ f_: (ι x_e: f_(x_e)))'/<,e> and '⟦bank⟧ = (λ x_e: Riverbank_(x_e))'/ conflict (Need at least one fully vacuous element), ⟦[bank the]⟧ = Type mismatch: '⟦bank⟧ = (λ x_e: Moneybank_(x_e))'/ and '⟦the⟧ = (λ f_: (ι x_e: f_(x_e)))'/<,e> conflict (Function Application), ⟦[the bank]⟧ = Type mismatch: '⟦the⟧ = (λ f_: (ι x_e: f_(x_e)))'/<,e> and '⟦bank⟧ = (λ x_e: Moneybank_(x_e))'/ conflict (Predicate Modification), ⟦[the bank]⟧ = Composition failure (PA requires a valid binder) on: ⟦the⟧ = (λ f_: (ι x_e: f_(x_e))) * ⟦bank⟧ = (λ x_e: Moneybank_(x_e)), ⟦[bank the]⟧ = Composition failure (PA requires a valid binder) on: ⟦bank⟧ = (λ x_e: Moneybank_(x_e)) * ⟦the⟧ = (λ f_: (ι x_e: f_(x_e))), ⟦[the bank]⟧ = Type mismatch: '⟦the⟧ = (λ f_: (ι x_e: f_(x_e)))'/<,e> and '⟦bank⟧ = (λ x_e: Moneybank_(x_e))'/ conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 44, "metadata": {}, "output_type": "execute_result" } ], "source": [ "the * bank" ] }, { "cell_type": "markdown", "id": "b6977061-d869-4c30-be10-37c752308e51", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Computing composition results\n", "\n", "Pretty straightforward brute force:\n", "\n", "For `a * b`\n", "1. For every composition operation in the system:\n", " 1. If `a` and `b` meet the preconditions of the composition operation `O`, add `O(a,b)` to the list of results\n", "2. Return the list of results" ] }, { "cell_type": "markdown", "id": "1f1537d0-7740-4299-aaf8-2e27370f2a0d", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "---\n", "## More composition operations" ] }, { "cell_type": "markdown", "id": "44748960-dac2-47f5-ade5-895b2b92bb38", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Predicate modification\n", "\n", "(This is again a Heim & Kratzer + Coppock and Champollion hybrid)\n", "\n", "**PM**: If $\\gamma$ is a syntax tree whose subtrees are $\\alpha$ and $\\beta$, where:\n", "* $[[\\alpha]]$ and $[[\\beta]]$ have type $\\langle e,t \\rangle$\n", "\n", "Then, $[[\\gamma]] = \\lambda x_e . [[\\alpha]](x) \\wedge [[\\beta]](x)$\n", "\n", "**Primary uses**: intersective adjectives, relative clauses" ] }, { "cell_type": "markdown", "id": "54608f5c-750c-49f6-b964-f3f035af1f10", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "#### First try at PM Procedurally\n", "\n", "For `a * b`\n", "\n", "1. If `a.content` and `b.content` have type $\\langle e,t \\rangle$, then:\n", " 1. construct a metalanguage object: `LFun(x, BinaryAndExpr(a.content(x), b.content(x))`\n", " 2. Let `f` = the fully reduced form of that object, and return `||a b|| = f`\n", "2. Otherwise, fail\n", "\n", "This is surprisingly annoying to implement!" ] }, { "cell_type": "markdown", "id": "314c2968-b6b7-4eb1-91e0-b3ec3861d0cc", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "#### The PM combinator\n", "\n", "The idea of PM has a different way it can be expressed:" ] }, { "cell_type": "code", "execution_count": 45, "id": "b124c2dd-fb2d-4c8a-88d7-d69d3a3976e1", "metadata": {}, "outputs": [ { "data": { "text/latex": [ "$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\lambda{} g_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\lambda{} x_{e} \\: . \\: ({f}({x}) \\wedge{} {g}({x}))$" ], "text/plain": [ "(λ f_: (λ g_: (λ x_e: (f_(x_e) & g_(x_e)))))" ] }, "execution_count": 45, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%te L f_ : L g_ : L x_e : f(x) & g(x)" ] }, { "cell_type": "markdown", "id": "500185f8-1962-46a4-85a1-7c693cdf245c", "metadata": {}, "source": [ "This is what is known as a [combinator](https://plato.stanford.edu/entries/lambda-calculus/#Com).\n", "* In this context, a combinator is simply a function with no free variables.\n", "* See also: [combinatory logic](https://plato.stanford.edu/entries/logic-combinatory/), [CCG](https://www.inf.ed.ac.uk/teaching/courses/nlg/readings/ccgintro.pdf)" ] }, { "cell_type": "markdown", "id": "f9ecfccb-f6da-45c4-b83f-abdf3d338c27", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "#### The combinator trick\n", "\n", "Many composition operations can be expressed as combinators." ] }, { "cell_type": "markdown", "id": "de46a1d5-e194-43fa-a714-f413624dfb5e", "metadata": { "slideshow": { "slide_type": "fragment" }, "tags": [] }, "source": [ "If $\\gamma$ is a syntax tree whose subtrees are $\\alpha$ and $\\beta$, and $C$ is a combinator designated as a composition operation, where\n", "1. $[[\\alpha]]$ has type $\\sigma$, and $[[\\beta]]$ has type $\\tau$,\n", "1. $C$ is a function of type $\\langle \\sigma, ... \\rangle$, and\n", "2. $C([[\\alpha]])$ is a function of type $\\langle \\tau, ... \\rangle$\n", "\n", "Then $[[\\gamma]] = C([[\\alpha]])([[\\beta]])$" ] }, { "cell_type": "markdown", "id": "2795be0c-c38b-4eb7-8f97-f3dc68d44278", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Existential closure\n", "\n", "This operation is commonly assumed in event semantics, and thought of as either a type-shift or a \"unary\" operation. For simplicity, I show here a variant of EC that operates on type $e$.\n", "\n", "**EC**: if $[[\\alpha]]$ has type $\\langle e, X \\rangle$ for some type $X$, then $[[EC(\\alpha)]] = \\exists x_e : [[\\alpha]](x)$" ] }, { "cell_type": "markdown", "id": "6f5102c4-0b2f-4dc6-99c1-a96835734426", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "#### Implementing EC\n", "\n", "The procedural attempt is straightforward, but again somewhat annoying to implement: build an object that introduces a $\\exists$ operator.\n", "\n", "Let's instead consider a combinator approach, again." ] }, { "cell_type": "code", "execution_count": 66, "id": "3d19e11e-1dd1-497e-ab6f-a80bc69552bc", "metadata": { "slideshow": { "slide_type": "fragment" }, "tags": [] }, "outputs": [ { "data": { "text/latex": [ "$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: {f}({x})$" ], "text/plain": [ "(λ f_: (Exists x_e: f_(x_e)))" ] }, "execution_count": 66, "metadata": {}, "output_type": "execute_result" } ], "source": [ "ec_combinator = %te L f_ : Exists x_e : f(x)\n", "ec_combinator" ] }, { "cell_type": "code", "execution_count": 67, "id": "a262ebb3-ed6d-4e35-b330-7e5de8fb2882", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "WARNING (lang): Composition rule named 'EC' already present in system, replacing\n" ] }, { "data": { "text/html": [ "Composition system 'H&K simple'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 VAC, built on python function 'lamb.lang.binary_vacuous' Unary composition rule EC, built on combinator '$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: {f}({x})$'}" ], "text/plain": [ "Composition system: H&K simple" ] }, "execution_count": 67, "metadata": {}, "output_type": "execute_result" } ], "source": [ "lang.get_system().add_unary_rule(ec_combinator, \"EC\")\n", "lang.get_system()" ] }, { "cell_type": "code", "execution_count": 68, "id": "60c75188-9c6e-4995-bf31-ddad67800d3e", "metadata": {}, "outputs": [ { "data": { "text/html": [ "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$" ], "text/latex": [ "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$" ], "text/plain": [ "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "1 composition path. Result:\n", " [0]: $[\\![\\mathbf{\\text{[cat]}}]\\!]^{}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: {Cat}({x})$" ], "text/plain": [ "CompositionResult(results=[⟦[cat]⟧ = (Exists x_e: Cat_(x_e))], failures=[])" ] }, "execution_count": 68, "metadata": {}, "output_type": "execute_result" } ], "source": [ "%lamb ||cat|| = L x_e : Cat_(x)\n", "cat.compose()" ] }, { "cell_type": "markdown", "id": "5460a70c-a935-4908-9dea-20a50dd5bb1a", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "#### Type-shifts\n", "\n", "Existential closure is often instead treated as a _type-shift_, applying as needed to get type $t$. Unary combinators can also be used for this." ] }, { "cell_type": "code", "execution_count": 53, "id": "02287065-4000-47c3-b4e0-d7af0cec6387", "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "WARNING (lang): Composition rule named 'EC' already present in system, replacing\n" ] }, { "data": { "text/html": [ "Composition system 'H&K simple'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 VAC, built on python function 'lamb.lang.binary_vacuous' Typeshift EC, built on combinator '$\\lambda{} f_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: \\exists{} x_{e} \\: . \\: {f}({x})$'}" ], "text/plain": [ "Composition system: H&K simple" ] }, "execution_count": 53, "metadata": {}, "output_type": "execute_result" } ], "source": [ "lang.get_system().add_typeshift(ec_combinator, \"EC\")\n", "lang.get_system().typeshift = True\n", "lang.get_system()" ] }, { "cell_type": "markdown", "id": "3578c0ff-f43a-44fa-b61c-bad66f81834a", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "Let's try it out:" ] }, { "cell_type": "code", "execution_count": 54, "id": "859369f0-2f80-4c24-95f9-a7949546426e", "metadata": { "tags": [] }, "outputs": [ { "data": { "text/html": [ "$[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{t} \\: . \\: \\neg{} {p}$" ], "text/latex": [ "$[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{t} \\: . \\: \\neg{} {p}$" ], "text/plain": [ "$[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{t} \\: . \\: \\neg{} {p}$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "%lamb ||neg|| = L p_t : ~p" ] }, { "cell_type": "code", "execution_count": 55, "id": "86d5a9b8-8476-4167-ab31-d86915ecd1ab", "metadata": {}, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", " [0]: $[\\![\\mathbf{\\text{[neg [cat]]}}]\\!]^{}_{t} \\:=\\: $$\\neg{} \\exists{} x_{e} \\: . \\: {Cat}({x})$" ], "text/plain": [ "CompositionResult(results=[⟦[neg [cat]]⟧ = ~(Exists x_e: Cat_(x_e))], failures=[⟦[neg cat]⟧ = Type mismatch: '⟦neg⟧ = (λ p_t: ~p_t)'/ and '⟦cat⟧ = (λ x_e: Cat_(x_e))'/ conflict (Function Application), ⟦[cat neg]⟧ = Type mismatch: '⟦cat⟧ = (λ x_e: Cat_(x_e))'/ and '⟦neg⟧ = (λ p_t: ~p_t)'/ conflict (Function Application), ⟦[neg cat]⟧ = Type mismatch: '⟦neg⟧ = (λ p_t: ~p_t)'/ and '⟦cat⟧ = (λ x_e: Cat_(x_e))'/ conflict (Predicate Modification), ⟦[neg cat]⟧ = Composition failure (PA requires a valid binder) on: ⟦neg⟧ = (λ p_t: ~p_t) * ⟦cat⟧ = (λ x_e: Cat_(x_e)), ⟦[cat neg]⟧ = Composition failure (PA requires a valid binder) on: ⟦cat⟧ = (λ x_e: Cat_(x_e)) * ⟦neg⟧ = (λ p_t: ~p_t), ⟦[neg cat]⟧ = Type mismatch: '⟦neg⟧ = (λ p_t: ~p_t)'/ and '⟦cat⟧ = (λ x_e: Cat_(x_e))'/ conflict (Need at least one fully vacuous element), ⟦[[cat] neg]⟧ = Type mismatch: '⟦[cat]⟧ = (Exists x_e: Cat_(x_e))'/t and '⟦neg⟧ = (λ p_t: ~p_t)'/ conflict (Function Application), ⟦[neg [cat]]⟧ = Type mismatch: '⟦neg⟧ = (λ p_t: ~p_t)'/ and '⟦[cat]⟧ = (Exists x_e: Cat_(x_e))'/t conflict (Predicate Modification), ⟦[neg [cat]]⟧ = Composition failure (PA requires a valid binder) on: ⟦neg⟧ = (λ p_t: ~p_t) * ⟦[cat]⟧ = (Exists x_e: Cat_(x_e)), ⟦[[cat] neg]⟧ = Composition failure (PA requires a valid binder) on: ⟦[cat]⟧ = (Exists x_e: Cat_(x_e)) * ⟦neg⟧ = (λ p_t: ~p_t), ⟦[neg [cat]]⟧ = Type mismatch: '⟦neg⟧ = (λ p_t: ~p_t)'/ and '⟦[cat]⟧ = (Exists x_e: Cat_(x_e))'/t conflict (Need at least one fully vacuous element), ⟦[neg cat]⟧ = Type mismatch: '⟦neg⟧ = (λ p_t: ~p_t)'/ and '⟦cat⟧ = (λ x_e: Cat_(x_e))'/ conflict (Function Application), ⟦[cat neg]⟧ = Type mismatch: '⟦cat⟧ = (λ x_e: Cat_(x_e))'/ and '⟦neg⟧ = (λ p_t: ~p_t)'/ conflict (Function Application), ⟦[neg cat]⟧ = Type mismatch: '⟦neg⟧ = (λ p_t: ~p_t)'/ and '⟦cat⟧ = (λ x_e: Cat_(x_e))'/ conflict (Predicate Modification), ⟦[neg cat]⟧ = Composition failure (PA requires a valid binder) on: ⟦neg⟧ = (λ p_t: ~p_t) * ⟦cat⟧ = (λ x_e: Cat_(x_e)), ⟦[cat neg]⟧ = Composition failure (PA requires a valid binder) on: ⟦cat⟧ = (λ x_e: Cat_(x_e)) * ⟦neg⟧ = (λ p_t: ~p_t), ⟦[neg cat]⟧ = Type mismatch: '⟦neg⟧ = (λ p_t: ~p_t)'/ and '⟦cat⟧ = (λ x_e: Cat_(x_e))'/ conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 55, "metadata": {}, "output_type": "execute_result" } ], "source": [ "neg * cat" ] }, { "cell_type": "code", "execution_count": 57, "id": "be9c0305-80ce-40e1-9ce5-699689f100d3", "metadata": { "slideshow": { "slide_type": "subslide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "Full composition trace. 1 path:\n", " Step 1: $[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{t} \\: . \\: \\neg{} {p}$\n", " Step 2: $[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$\n", " Step 3: $[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$ leads to: $[\\![\\mathbf{\\text{[cat]}}]\\!]^{}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: {Cat}({x})$ [by EC]\n", " Step 4: $[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{[cat]}}]\\!]^{}_{t}$ leads to: $[\\![\\mathbf{\\text{[neg [cat]]}}]\\!]^{}_{t} \\:=\\: $$\\neg{} \\exists{} x_{e} \\: . \\: {Cat}({x})$ [by FA]\n" ], "text/latex": [ "Full composition trace. 1 path:\n", " Step 1: $[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{t} \\: . \\: \\neg{} {p}$\n", " Step 2: $[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$\n", " Step 3: $[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$ leads to: $[\\![\\mathbf{\\text{[cat]}}]\\!]^{}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: {Cat}({x})$ [by EC]\n", " Step 4: $[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{[cat]}}]\\!]^{}_{t}$ leads to: $[\\![\\mathbf{\\text{[neg [cat]]}}]\\!]^{}_{t} \\:=\\: $$\\neg{} \\exists{} x_{e} \\: . \\: {Cat}({x})$ [by FA]\n" ], "text/plain": [ "Full composition trace. 1 path:\n", " Step 1: $[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{t} \\: . \\: \\neg{} {p}$\n", " Step 2: $[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$\n", " Step 3: $[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}}$ leads to: $[\\![\\mathbf{\\text{[cat]}}]\\!]^{}_{t} \\:=\\: $$\\exists{} x_{e} \\: . \\: {Cat}({x})$ [by EC]\n", " Step 4: $[\\![\\mathbf{\\text{neg}}]\\!]^{}_{\\left\\langle{}t,t\\right\\rangle{}}$ * $[\\![\\mathbf{\\text{[cat]}}]\\!]^{}_{t}$ leads to: $[\\![\\mathbf{\\text{[neg [cat]]}}]\\!]^{}_{t} \\:=\\: $$\\neg{} \\exists{} x_{e} \\: . \\: {Cat}({x})$ [by FA]" ] }, "execution_count": 57, "metadata": {}, "output_type": "execute_result" } ], "source": [ "(neg * cat).trace()" ] }, { "cell_type": "markdown", "id": "b7777900-85b4-4b54-b1fa-7c151df9d5cc", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "#### Computing composition results with type-shifts\n", "\n", "Still brute force. This is called _last-resort type-shifting_ (Partee):\n", "\n", "For `a * b`\n", "1. For every composition operation in the system:\n", " 1. If `a` and `b` meet the preconditions of the composition operation `O`, add `O(a,b)` to the list of results\n", "2. If the list is still empty, for each unary typeshift `t`:\n", " 1. Recurse and run the algorithm on t(a) * b\n", " 2. Recurse and run the algorithm on a * t(b)\n", "3. Return the list of results, including any discovered in step 2\n", "\n", "**Caveat**: need to be careful in case type-shifts lead to recursion!" ] }, { "cell_type": "markdown", "id": "a9def962-410a-4106-8436-5750fa9b15db", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### The combinator trick recap\n", "\n", "**Many** composition operations that have been proposed in the literature can be represented as combinators.\n", "\n", "The initial core Heim & Kratzer system is essentially the system determined by:\n", "\n", "1. **FA**: $\\lambda f . \\lambda x . f(x)$ (also called the **A** combinator)\n", "2. **NN**: $\\lambda x . x$ (also called the **I** combinator)\n", "3. **PM**: $\\lambda f_{\\langle e,t \\rangle} . \\lambda g_{\\langle e,t \\rangle} . \\lambda x_e . f(x) \\wedge g(x)$\n", "\n", "(However -- need to reconsider the types for the first two!)" ] }, { "cell_type": "markdown", "id": "a49f711f-3109-4ec8-8118-7ee955a015e9", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Predicate abstraction\n", "\n", "The \"Predicate Abstraction\" rule can't be expressed as a combinator.\n", "* Reason: it makes direct reference to the form of the object language, via an index.\n", "* Use the Coppock and Champollion version of PA here. Their trick: use the index as the variable name.\n", "\n", "**PA**: if $\\gamma$ is a branching node with daughters $\\alpha_i$ and $\\beta$, where $i$ is an LF index, then $[[\\gamma]] = \\lambda x^i_e . [[\\beta]]$\n" ] }, { "cell_type": "markdown", "id": "0089efcd-d2dc-48f6-944c-46e99b16a658", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "This one *is* implemented procedurally:\n", "\n", "```\n", "def sbc_pa(binder, content, assignment=None):\n", " if not tree_binder_check(binder):\n", " raise CompositionFailure(binder, content, reason=\"PA requires a valid binder\")\n", " vname = \"var%i\" % binder.get_index()\n", " bound_var = meta.term(vname, types.type_e)\n", " f = meta.LFun(types.type_e,\n", " content.content.calculate_partiality({bound_var}), vname)\n", " return BinaryComposite(binder, content, f)\n", "```" ] }, { "cell_type": "code", "execution_count": 58, "id": "626acdbd-f3fb-4473-b584-b93d3713aa81", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", " [0]: $[\\![\\mathbf{\\text{[5 [cat t5]]}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$" ], "text/plain": [ "CompositionResult(results=[⟦[5 [cat t5]]⟧ = (λ x_e: Cat_(x_e))], failures=[⟦[5 [cat t5]]⟧ = Composition failure (FA disallows None) on: ⟦5⟧ = None * ⟦[cat t5]⟧ = Cat_(var5_e), ⟦[[cat t5] 5]⟧ = Composition failure (FA disallows None) on: ⟦[cat t5]⟧ = Cat_(var5_e) * ⟦5⟧ = None, ⟦[5 [cat t5]]⟧ = Composition failure (PM disallows None) on: ⟦5⟧ = None * ⟦[cat t5]⟧ = Cat_(var5_e), ⟦[[cat t5] 5]⟧ = Composition failure (PA requires a valid binder) on: ⟦[cat t5]⟧ = Cat_(var5_e) * ⟦5⟧ = None, ⟦[5 [cat t5]]⟧ = Type mismatch: '⟦5⟧ = None' and '⟦[cat t5]⟧ = Cat_(var5_e)'/t conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 58, "metadata": {}, "output_type": "execute_result" } ], "source": [ "binder = lang.Binder(5)\n", "t = lang.Trace(5)\n", "binder * (t * cat)" ] }, { "cell_type": "markdown", "id": "fb108af4-afc4-4a56-a9c0-5fa0897f15fc", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "### Composition and the object-language\n", "\n", "More operations that can't be handled with combinators:\n", "* Operations that bind an evaluation parameter (world, time, context)\n", "* The `VAC` operation, which ignores vacuous items\n", "* Various operations that interact with arity in complex ways, e.g. Chung and Ladusaw's Restrict, Jacobson's implementation of quantifier typeshifts\n" ] }, { "cell_type": "markdown", "id": "1bdf2950-1786-4fd9-9855-4ff1c2d6b760", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Composition systems, recap\n", "\n", "What is a composition system in the end?\n", "1. A set of composition operations\n", " 1. Python: implemented via a python function that constructs a new metalanguage object given some input(s)\n", " 2. Combinator: implemented via a combinator\n", " 3. Unary operations can be designated as type-shifts\n", "2. A set of classes that describe object language$\\Leftrighatarrow$meta-language mappings, abstracted as `Composable`s\n", "2. A set of functions that given some `Composable`s, does a (brute-force) search over possible valid combinations\n" ] }, { "cell_type": "markdown", "id": "869cfc1a-0575-4548-9861-fed56cdaf138", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## A more interesting example to play with\n", "\n", "Switch to notebook for this:" ] }, { "cell_type": "code", "execution_count": 59, "id": "16fc7bbd-1561-4e32-a68d-bd86a3b92903", "metadata": { "tags": [ "hide_output" ] }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "INFO (meta): Coerced guessed type for 'Cat_t' into , to match argument 'x_e'\n", "INFO (meta): Coerced guessed type for 'Gray_t' into , to match argument 'x_e'\n", "INFO (meta): Coerced guessed type for 'In_t' into <(e,e),t>, to match argument '(y_e, x_e)'\n", "INFO (meta): Coerced guessed type for 'Fond_t' into <(e,e),t>, to match argument '(y_e, x_e)'\n" ] }, { "data": { "text/html": [ "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$\n", "$[\\![\\mathbf{\\text{gray}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Gray}({x})$\n", "$[\\![\\mathbf{\\text{kaline}}]\\!]^{}_{e} \\:=\\: $${Kaline}_{e}$\n", "$[\\![\\mathbf{\\text{julius}}]\\!]^{}_{e} \\:=\\: $${Julius}_{e}$\n", "$[\\![\\mathbf{\\text{inP}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {In}({y}, {x})$\n", "$[\\![\\mathbf{\\text{texas}}]\\!]^{}_{e} \\:=\\: $${Texas}_{e}$\n", "$[\\![\\mathbf{\\text{isV}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: {p}$\n", "$[\\![\\mathbf{\\text{fond}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Fond}({y}, {x})$" ], "text/latex": [ "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$\n", "$[\\![\\mathbf{\\text{gray}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Gray}({x})$\n", "$[\\![\\mathbf{\\text{kaline}}]\\!]^{}_{e} \\:=\\: $${Kaline}_{e}$\n", "$[\\![\\mathbf{\\text{julius}}]\\!]^{}_{e} \\:=\\: $${Julius}_{e}$\n", "$[\\![\\mathbf{\\text{inP}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {In}({y}, {x})$\n", "$[\\![\\mathbf{\\text{texas}}]\\!]^{}_{e} \\:=\\: $${Texas}_{e}$\n", "$[\\![\\mathbf{\\text{isV}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: {p}$\n", "$[\\![\\mathbf{\\text{fond}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Fond}({y}, {x})$" ], "text/plain": [ "$[\\![\\mathbf{\\text{cat}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Cat}({x})$\n", "$[\\![\\mathbf{\\text{gray}}]\\!]^{}_{\\left\\langle{}e,t\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: {Gray}({x})$\n", "$[\\![\\mathbf{\\text{kaline}}]\\!]^{}_{e} \\:=\\: $${Kaline}_{e}$\n", "$[\\![\\mathbf{\\text{julius}}]\\!]^{}_{e} \\:=\\: $${Julius}_{e}$\n", "$[\\![\\mathbf{\\text{inP}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {In}({y}, {x})$\n", "$[\\![\\mathbf{\\text{texas}}]\\!]^{}_{e} \\:=\\: $${Texas}_{e}$\n", "$[\\![\\mathbf{\\text{isV}}]\\!]^{}_{\\left\\langle{}\\left\\langle{}e,t\\right\\rangle{},\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} p_{\\left\\langle{}e,t\\right\\rangle{}} \\: . \\: {p}$\n", "$[\\![\\mathbf{\\text{fond}}]\\!]^{}_{\\left\\langle{}e,\\left\\langle{}e,t\\right\\rangle{}\\right\\rangle{}} \\:=\\: $$\\lambda{} x_{e} \\: . \\: \\lambda{} y_{e} \\: . \\: {Fond}({y}, {x})$" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "%%lamb\n", "||cat|| = L x_e: Cat(x)\n", "||gray|| = L x_e: Gray(x)\n", "||kaline|| = Kaline_e\n", "||julius|| = Julius_e\n", "||inP|| = L x_e : L y_e : In(y, x) # `in` is a reserved word in python\n", "||texas|| = Texas_e\n", "||isV|| = L p_ : p # `is` is a reserved word in python\n", "||fond|| = L x_e : L y_e : Fond(y, x)" ] }, { "cell_type": "code", "execution_count": 60, "id": "391f1098-c093-4c34-ab46-60c631ab33e8", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "image/svg+xml": [ "" ], "text/html": [ "$[\\![\\mathbf{\\text{of}}]\\!]^{}\\text{ [vacuous]}$" ], "text/latex": [ "$[\\![\\mathbf{\\text{of}}]\\!]^{}\\text{ [vacuous]}$" ], "text/plain": [ "⟦of⟧ = None" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "" ], "text/html": [ "$[\\![\\mathbf{\\text{a}}]\\!]^{}\\text{ [vacuous]}$" ], "text/latex": [ "$[\\![\\mathbf{\\text{a}}]\\!]^{}\\text{ [vacuous]}$" ], "text/plain": [ "⟦a⟧ = None" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "" ], "text/html": [ "$[\\![\\mathbf{\\text{5}}]\\!]^{}\\text{ [vacuous]}$" ], "text/latex": [ "$[\\![\\mathbf{\\text{5}}]\\!]^{}\\text{ [vacuous]}$" ], "text/plain": [ "⟦5⟧ = None" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "" ], "text/html": [ "$[\\![\\mathbf{\\text{t}}_{5}]\\!]^{}_{e} \\:=\\: $${var5}_{e}$" ], "text/latex": [ "$[\\![\\mathbf{\\text{t}}_{5}]\\!]^{}_{e} \\:=\\: $${var5}_{e}$" ], "text/plain": [ "⟦t5⟧ = var5_e" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "of = lang.Item(\"of\", content=None)\n", "a = lang.Item(\"a\", content=None)\n", "binder = lang.Binder(5)\n", "t5 = lang.Trace(5)\n", "\n", "display(of, a, binder, t5)" ] }, { "cell_type": "code", "execution_count": 61, "id": "226cefa7-0262-49d1-9e24-bae389ffa83b", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", " [0]: $[\\![\\mathbf{\\text{[[isV [a [gray cat]]] kaline]}}]\\!]^{}_{t} \\:=\\: $$({Gray}({Kaline}_{e}) \\wedge{} {Cat}({Kaline}_{e}))$" ], "text/plain": [ "CompositionResult(results=[⟦[[isV [a [gray cat]]] kaline]⟧ = (Gray_(Kaline_e) & Cat_(Kaline_e))], failures=[⟦[kaline [isV [a [gray cat]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [a [gray cat]]]⟧ = (λ x_e: (Gray_(x_e) & Cat_(x_e)))'/ conflict (Function Application), ⟦[kaline [isV [a [gray cat]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [a [gray cat]]]⟧ = (λ x_e: (Gray_(x_e) & Cat_(x_e)))'/ conflict (Predicate Modification), ⟦[kaline [isV [a [gray cat]]]]⟧ = Composition failure (PA requires a valid binder) on: ⟦kaline⟧ = Kaline_e * ⟦[isV [a [gray cat]]]⟧ = (λ x_e: (Gray_(x_e) & Cat_(x_e))), ⟦[[isV [a [gray cat]]] kaline]⟧ = Composition failure (PA requires a valid binder) on: ⟦[isV [a [gray cat]]]⟧ = (λ x_e: (Gray_(x_e) & Cat_(x_e))) * ⟦kaline⟧ = Kaline_e, ⟦[kaline [isV [a [gray cat]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [a [gray cat]]]⟧ = (λ x_e: (Gray_(x_e) & Cat_(x_e)))'/ conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 61, "metadata": {}, "output_type": "execute_result" } ], "source": [ "kaline * (isV * (a * (gray * cat)))" ] }, { "cell_type": "code", "execution_count": 62, "id": "01a80bfd-e967-4556-8ac5-cd500fb58295", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", " [0]: $[\\![\\mathbf{\\text{[[isV [[a [gray cat]] [inP texas]]] kaline]}}]\\!]^{}_{t} \\:=\\: $$(({Gray}({Kaline}_{e}) \\wedge{} {Cat}({Kaline}_{e})) \\wedge{} {In}({Kaline}_{e}, {Texas}_{e}))$" ], "text/plain": [ "CompositionResult(results=[⟦[[isV [[a [gray cat]] [inP texas]]] kaline]⟧ = ((Gray_(Kaline_e) & Cat_(Kaline_e)) & In_<(e,e),t>(Kaline_e, Texas_e))], failures=[⟦[kaline [isV [[a [gray cat]] [inP texas]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [[a [gray cat]] [inP texas]]]⟧ = (λ x_e: ((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e)))'/ conflict (Function Application), ⟦[kaline [isV [[a [gray cat]] [inP texas]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [[a [gray cat]] [inP texas]]]⟧ = (λ x_e: ((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e)))'/ conflict (Predicate Modification), ⟦[kaline [isV [[a [gray cat]] [inP texas]]]]⟧ = Composition failure (PA requires a valid binder) on: ⟦kaline⟧ = Kaline_e * ⟦[isV [[a [gray cat]] [inP texas]]]⟧ = (λ x_e: ((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e))), ⟦[[isV [[a [gray cat]] [inP texas]]] kaline]⟧ = Composition failure (PA requires a valid binder) on: ⟦[isV [[a [gray cat]] [inP texas]]]⟧ = (λ x_e: ((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e))) * ⟦kaline⟧ = Kaline_e, ⟦[kaline [isV [[a [gray cat]] [inP texas]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [[a [gray cat]] [inP texas]]]⟧ = (λ x_e: ((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e)))'/ conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 62, "metadata": {}, "output_type": "execute_result" } ], "source": [ "kaline * (isV * ((a * (gray * cat)) * (inP * texas)))" ] }, { "cell_type": "code", "execution_count": 63, "id": "efb1af65-2b5b-4ef6-9670-b014e5989081", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "outputs": [ { "data": { "text/html": [ "1 composition path. Result:\n", " [0]: $[\\![\\mathbf{\\text{[[isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]] kaline]}}]\\!]^{}_{t} \\:=\\: $$((({Gray}({Kaline}_{e}) \\wedge{} {Cat}({Kaline}_{e})) \\wedge{} {In}({Kaline}_{e}, {Texas}_{e})) \\wedge{} {Fond}({Kaline}_{e}, {Julius}_{e}))$" ], "text/plain": [ "CompositionResult(results=[⟦[[isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]] kaline]⟧ = (((Gray_(Kaline_e) & Cat_(Kaline_e)) & In_<(e,e),t>(Kaline_e, Texas_e)) & Fond_<(e,e),t>(Kaline_e, Julius_e))], failures=[⟦[kaline [isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]⟧ = (λ x_e: (((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e)) & Fond_<(e,e),t>(x_e, Julius_e)))'/ conflict (Function Application), ⟦[kaline [isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]⟧ = (λ x_e: (((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e)) & Fond_<(e,e),t>(x_e, Julius_e)))'/ conflict (Predicate Modification), ⟦[kaline [isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]]⟧ = Composition failure (PA requires a valid binder) on: ⟦kaline⟧ = Kaline_e * ⟦[isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]⟧ = (λ x_e: (((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e)) & Fond_<(e,e),t>(x_e, Julius_e))), ⟦[[isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]] kaline]⟧ = Composition failure (PA requires a valid binder) on: ⟦[isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]⟧ = (λ x_e: (((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e)) & Fond_<(e,e),t>(x_e, Julius_e))) * ⟦kaline⟧ = Kaline_e, ⟦[kaline [isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]]⟧ = Type mismatch: '⟦kaline⟧ = Kaline_e'/e and '⟦[isV [a [[[gray cat] [inP texas]] [5 [[fond [of julius]] t5]]]]]⟧ = (λ x_e: (((Gray_(x_e) & Cat_(x_e)) & In_<(e,e),t>(x_e, Texas_e)) & Fond_<(e,e),t>(x_e, Julius_e)))'/ conflict (Need at least one fully vacuous element)])" ] }, "execution_count": 63, "metadata": {}, "output_type": "execute_result" } ], "source": [ "kaline * (isV * (a * ((gray * cat) * (inP * texas)\n", " * (binder * (t5 * (fond * (of * julius)))))))" ] }, { "cell_type": "markdown", "id": "340c5a81-94a2-4a29-ac20-8c9ea773c462", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Another example\n", "\n", "Depending on time, let's look at the Neo-Davidsonian fragment" ] }, { "cell_type": "markdown", "id": "98c444d9-efa5-4b60-bbd3-00676af247f6", "metadata": { "slideshow": { "slide_type": "slide" }, "tags": [] }, "source": [ "## Recap: day 2\n", "\n", "1. Most of the work: getting a robust implementation of (meta-language) function application.\n", "2. Composition systems layered on the meta-language.\n", "3. Combinator-based composition operations (PM, EC, ...), type-shifts\n", "4. Example: a Heim & Kratzer-inspired basic case\n", "5. Example: extending to add events\n", "\n", "Next: more on the metalanguage; type inference" ] } ], "metadata": { "kernelspec": { "display_name": "Lambda Notebook-dev (Python 3)", "language": "python", "name": "lambda-notebook-dev" }, "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.7.6" } }, "nbformat": 4, "nbformat_minor": 5 }