lspc.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Examples from Interfacing Language, Spatial Perception and Cognition in Type Theory with Records by Simon Dobnik and Robin Cooper"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The examples use the module `ttrtypes` and `records`.  We add a simple notion of equivalence between types.  If you have previously judged something to be of one type then it will also be a witness for the other type.  Ultimately, one would want a more general treatment of equivalence between predicates."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from ttrtypes import BType,Pred,PType,Possibility,RecType,Fun,ListType,FunType,Ty,LazyObj\n",
    "from records import Rec\n",
    "from utils import show,show_latex\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Section 4"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "Ind = BType('Ind')\n",
    "Ind.judge('a')\n",
    "Ind.judge('b')\n",
    "print(Ind.query('a'))\n",
    "print(Ind.query('b'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n",
      "\n",
      "M:\n",
      "_____________________________________________\n",
      "right(b, a): [s1, s2]\n",
      "left(a, b): [s2, s1]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "left = Pred('left',[Ind,Ind])\n",
    "right = Pred('right',[Ind,Ind])\n",
    "left.learn_witness_fun(lambda args: PType(right,[args[1],args[0]]))\n",
    "right.learn_witness_fun(lambda args: PType(left,[args[1],args[0]]))\n",
    "left_a_b = PType(left,['a','b'])\n",
    "right_b_a = PType(right,['b','a'])\n",
    "M = Possibility('M')\n",
    "right_b_a.in_poss(M).judge('s1')\n",
    "left_a_b.in_poss(M).judge('s2')\n",
    "print(left_a_b.in_poss(M).query('s1'))\n",
    "print(right_b_a.in_poss(M).query('s2'))\n",
    "print(show(M))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "left_a_b.in_poss(M).query('s3')"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 5,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{x : Ind, y : Ind, e : (lambda v1:Ind . lambda v2:Ind . left(v1, v2), [x, y])}\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\left[\\begin{array}{lcl}\n",
       "\\text{x} &:& \\textit{Ind}\\\\\n",
       "\\text{y} &:& \\textit{Ind}\\\\\n",
       "\\text{e} &:& \\langle \\lambda v_{1}:\\textit{Ind}\\ .\\ \\lambda v_{2}:\\textit{Ind}\\ .\\ \\text{left}(v_{1}, v_{2}), \\langle \\text{x}, \\text{y}\\rangle\\rangle\n",
       "\\end{array}\\right]\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },

     "execution_count": 5,

     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "T_left = RecType({'x':Ind,'y':Ind, 'e':(Fun('v1',Ind,Fun('v2',Ind,PType(left,['v1','v2']))),['x','y'])})\n",
    "print(show(T_left))\n",
    "show_latex(T_left)"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 6,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{x = a, y = b, e = s2}\n"
     ]
    }
   ],
   "source": [
    "r_left = Rec({'x':'a','y':'b','e':'s2'})\n",
    "print(show(r_left))"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 7,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "print(T_left.in_poss(M).query(r_left))"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 8,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "M:\n",
      "_____________________________________________\n",
      "right(b, a): [s1, s2]\n",
      "left(a, b): [s2, s1]\n",
      "Ind: [a, b]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "print(show(M))"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 9,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{x : Ind, y : Ind, c1 : (lambda v:Ind . target(v), [x]), c2 : (lambda v:Ind . landmark(v), [y]), e : (lambda v1:Ind . lambda v2:Ind . left(v1, v2), [x, y])}\n"
     ]
    }
   ],
   "source": [
    "target = Pred('target',[Ind])\n",
    "landmark = Pred('landmark',[Ind])\n",
    "T_relation = RecType({'x':Ind,\n",
    "                      'y':Ind,\n",
    "                      'c1':(Fun('v',Ind,PType(target,['v'])),['x']),\n",
    "                      'c2':(Fun('v',Ind,PType(landmark,['v'])),['y'])})\n",
    "T_relation_left = T_relation.merge(T_left)\n",
    "print(show(T_relation_left))"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 10,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "print(T_relation_left.subtype_of(T_relation))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Figure 8"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1."
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 11,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "[0.5]\n"
     ]
    }
   ],
   "source": [
    "Real = BType('Real')\n",
    "Real.learn_witness_condition(lambda n: isinstance(n,float))\n",
    "print(Real.query(0.5))\n",
    "print(Real.witness_cache)"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 12,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "Point = RecType({'x':Real,'y':Real,'z':Real})\n",
    "PointMap = ListType(Point)\n",
    "map =[Rec({'x':34.0,'y':24.0,'z':48.0}),Rec({'x':56.0,'y':78.0,'z':114.0}),Rec({'x':44.0,'y':46.5,'z':33.7})]\n",
    "print(PointMap.query(map))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 2."
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 13,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "chair = Pred('chair',[Ind])\n",
    "Ppty = FunType(Ind,Ty)\n",
    "chair_prop = Fun('v',Ind,PType(chair,['v']))\n",
    "print(Ppty.query(chair_prop))"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 14,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[{reg = [{x = 56.0, y = 78.0, z = 114.0}, {x = 34.0, y = 24.0, z = 48.0}], pfun = lambda v:Ind . chair(v)}]\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "PointMapPpty = RecType({'reg':PointMap,'pfun':Ppty})\n",
    "ParsedPointMap = ListType(PointMapPpty)  #should really be SetType\n",
    "ObjectDetector = FunType(PointMap,ParsedPointMap)\n",
    "\n",
    "\n",
    "def external_fake_object_detector(pmap):\n",
    "    chairs = [[i,j] for i in pmap for j in pmap if i.y - j.y == 54]\n",
    "    return [Rec({'reg':pmap,'pfun':chair_prop}) for pmap in chairs]\n",
    "\n",
    "parsed_map = external_fake_object_detector(map)\n",
    "print(show(parsed_map))\n",
    "print(ParsedPointMap.query(parsed_map))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 3."
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 15,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{a : Ind, loc : (lambda v:Ind . location(v, [{x = 56.0, y = 78.0, z = 114.0}, {x = 34.0, y = 24.0, z = 48.0}]), [a]), c : (lambda v:Ind . chair(v), [a])}\n"
     ]
    }
   ],
   "source": [
    "location = Pred('location',[Ind,PointMap])\n",
    "IndividualRec = RecType({'a':Ind,'loc':Ty,'c':Ty})\n",
    "IndividuationFun = FunType(PointMapPpty,IndividualRec)\n",
    "ind_fun = Fun('p',PointMapPpty,RecType({'a':Ind,\n",
    "                                'loc':(Fun('v',Ind,PType(location,['v',LazyObj(['p', '.','reg'])])),['a']),\n",
    "                        'c':(LazyObj(['p', '.', 'pfun']),['a'])}))\n",
    "print(show(ind_fun.app(parsed_map[0])))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Figure 9"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### (a)"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 16,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{x = _a0, c = _e0}\n",
      "\n",
      "M:\n",
      "_____________________________________________\n",
      "right(b, a): [s1, s2]\n",
      "left(a, b): [s2, s1]\n",
      "Ind: [a, b, _a0]\n",
      "person(_a0): [_e0]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "person = Pred('person',[Ind])\n",
    "organism = Pred('organism',[Ind])\n",
    "Person = RecType({'x':Ind,'c':(Fun('v',Ind, PType(person,['v'])),['x'])})\n",
    "Person.in_poss(M)\n",
    "Topos_pers_organism = Fun('r',Person,PType(organism,[LazyObj(['r','.','x'])]))\n",
    "r1 = Person.create()\n",
    "print(show(r1))\n",
    "print(show(Person.poss))"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 17,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "organism(_a0)\n"
     ]
    }
   ],
   "source": [
    "T_organism = Topos_pers_organism.app(r1)\n",
    "print(show(T_organism))"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 18,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "\n",
      "M:\n",
      "_____________________________________________\n",
      "right(b, a): [s1, s2]\n",
      "left(a, b): [s2, s1]\n",
      "Ind: [a, b, _a0]\n",
      "person(_a0): [_e0]\n",
      "organism(_a0): [_e1]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "def Apply_topos_non_specific(topos,arg,m):\n",
    "    if topos.domain_type.query(arg):\n",
    "        res = topos.app(arg)\n",
    "        res.judge_nonspec()\n",
    "        return res.in_poss(m)\n",
    "T_organism_M = Apply_topos_non_specific(Topos_pers_organism,r1,M)\n",
    "print(show(T_organism_M.query_nonspec()))\n",
    "print(show(M))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### (b)"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 19,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "organism(_a0)\n",
      "True\n",
      "\n",
      "M:\n",
      "_____________________________________________\n",
      "right(b, a): [s1, s2]\n",
      "left(a, b): [s2, s1]\n",
      "Ind: [a, b, _a0]\n",
      "person(_a0): [_e0]\n",
      "organism(_a0): [_e1, _e0]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "Dep_Topos_pers_organism = Fun('v',Ind,Fun('s',PType(person,['v']),PType(organism,['v'])))\n",
    "def Apply_topos_specific(topos,arg,m):\n",
    "    if topos.domain_type.in_poss(m).query(arg):\n",
    "        res = topos.in_poss(m).app(arg)\n",
    "        res.in_poss(m).judge(arg)\n",
    "        return res.in_poss(m)\n",
    "#T1_organism_M = Apply_topos_specific(Dep_Topos_pers_organism.app('_a_{0}'),'_e_{0}',M)\n",
    "T1_organism_M = Apply_topos_specific(Dep_Topos_pers_organism.app('_a0'),'_e0',M)\n",
    "\n",
    "#print(show(Dep_Topos_pers_organism.app('_a_{0}').domain_type.in_poss(M).query('_e_{0}')))\n",
    "print(show(Dep_Topos_pers_organism.app('_a0').domain_type.in_poss(M).query('_e0')))\n",
    "\n",
    "print(show(T1_organism_M))\n",
    "#print(show(T1_organism_M.query('_e_{0}')))\n",
    "print(show(T1_organism_M.query('_e0')))\n",
    "print(show(M))\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Figure 10"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 20,


   "metadata": {},
   "outputs": [],
   "source": [
    "artefact = Pred('artefact',[Ind])\n",
    "spatial_template_under1 = Pred('st_under1',[PointMap,PointMap])\n",
    "spatial_template_under2 = Pred('st_under2',[PointMap,PointMap])\n",
    "under1 = Pred('under1',[Ind,Ind])\n",
    "under2 = Pred('under2',[Ind,Ind])\n",
    "PersonInd = RecType({'a':Ind,'reg':PointMap,'c':(Fun('v',Ind,PType(person,['v'])),['a'])})\n",
    "ArtefactInd = RecType({'a':Ind,'reg':PointMap,'c':(Fun('v',Ind,PType(artefact,['v'])),['a'])})\n",
    "Under1_sit = RecType({'o1':PersonInd,\n",
    "                      'o2':ArtefactInd,\n",
    "                      'st':(Fun('v1',PointMap,\n",
    "                                Fun('v2',PointMap,PType(spatial_template_under1,['v1','v2']))),\n",
    "                            ['o1.reg','o2.reg'])})\n",
    "Under2_sit = RecType({'o1':PersonInd,\n",
    "                      'o2':ArtefactInd,\n",
    "                      'st':(Fun('v1',PointMap,\n",
    "                                Fun('v2',PointMap,PType(spatial_template_under2,['v1','v2']))),\n",
    "                            ['o1.reg','o2.reg'])})\n",
    "Topos_under1 = Fun('r',Under1_sit,PType(under1,[LazyObj([LazyObj(['r','.','o1']),'.','a']),\n",
    "                                                LazyObj([LazyObj(['r','.','o2']),'.','a'])]))\n",
    "Topos_under2 = Fun('r',Under2_sit,PType(under2,[LazyObj([LazyObj(['r','.','o1']),'.','a']),\n",
    "                                                LazyObj([LazyObj(['r','.','o2']),'.','a'])]))\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 21,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{o1 = {a = _a1, reg = _a2, c = _e2}, o2 = {a = _a3, reg = _a4, c = _e3}, st = _e4}\n",
      "{o1 = {a = _a5, reg = _a6, c = _e5}, o2 = {a = _a7, reg = _a8, c = _e6}, st = _e7}\n",
      "\n",
      "M1:\n",
      "_____________________________________________\n",
      "Ind: [a, b, _a1, _a3, _a5, _a7]\n",
      "person(_a1): [_e2]\n",
      "artefact(_a3): [_e3]\n",
      "st_under1(_a2, _a4): [_e4]\n",
      "person(_a5): [_e5]\n",
      "artefact(_a7): [_e6]\n",
      "st_under2(_a6, _a8): [_e7]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "M1 = Possibility('M1')\n",
    "u1 = Under1_sit.in_poss(M1).create()\n",
    "print(show(u1))\n",
    "u2 = Under2_sit.in_poss(M1).create()\n",
    "print(show(u2))\n",
    "print(show(M1))"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 22,

   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "under1(_a1, _a3)\n",
      "under2(_a5, _a7)\n"
     ]
    }
   ],
   "source": [
    "print(show(Topos_under1.app(u1)))\n",
    "print(show(Topos_under2.app(u2)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Figure 11"
   ]
  },
  {
   "cell_type": "code",

   "execution_count": 23,

   "metadata": {},
   "outputs": [],
   "source": [
    "#Objs_Alex_Sam = RecType({'o0':PersonInd,'o1':PersonInd,'o2':ArtefactInd,'o3':ArtefactInd})\n",
    "#Priv_Alex = RecType({'objs':Objs_Alex_Sam, 'bel':(Fun('v',Ind,\n",
    "#                                                    RecType({'c_me':SingletonType(RecType,)})))})#"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}