ttr-overview-aics2021.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Examples from TTR overview lecture in `pyttr`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from ttrtypes import Type,BType,PType,Pred,Possibility,RecType,Fun,\\\n",
    "                     TTRStringType,KPlusStringType,LazyObj,TTRString\n",
    "from records import Rec\n",
    "from utils import show, show_latex,print_latex,forall"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Judgement"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\textit{T}_{\\textit{0}}\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "T = Type()\n",
    "T.judge('a')\n",
    "\n",
    "print(T.query('a'))\n",
    "show_latex(T)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Basic types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\textit{Ind}\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Ind = BType('Ind')\n",
    "Ind.judge('a')\n",
    "\n",
    "print(Ind.query('a'))\n",
    "show_latex(Ind)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Witness conditions for types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "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": "markdown",
   "metadata": {},
   "source": [
    "## Intensionality"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "['a', 'b']\n",
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "T1 = Type()\n",
    "T2 = Type()\n",
    "T1.judge('a')\n",
    "T1.judge('b')\n",
    "T2.judge('b')\n",
    "T2.judge('a')\n",
    "\n",
    "print(T1.witness_cache)\n",
    "print(set(T1.witness_cache) == set(T2.witness_cache))\n",
    "print(T1==T2)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Ptypes"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "run = Pred('run',[Ind])\n",
    "hug = Pred('hug',[Ind,Ind])\n",
    "Ind.judge('b')\n",
    "Ind.judge('d')\n",
    "run_d = PType(run,['d'])\n",
    "hug_b_d = PType(hug,['b','d'])\n",
    "run_d.judge('e1')\n",
    "hug_b_d.judge('e2')\n",
    "\n",
    "print(run_d.query('e1'))\n",
    "print(hug_b_d.query('e1'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\text{hug}(\\text{b}, \\text{d})\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "show_latex(hug_b_d)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\text{run}(\\text{d})\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "show_latex(run_d)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Possibilities (models)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "M1:\n",
      "_____________________________________________\n",
      "Ind: [a, b, d]\n",
      "run(d): [e1]\n",
      "hug(b, d): [e2]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "M1 = Possibility('M1')\n",
    "\n",
    "Ind.in_poss(M1)\n",
    "run_d.in_poss(M1)\n",
    "hug_b_d.in_poss(M1)\n",
    "\n",
    "print(show(M1))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "M2:\n",
      "_____________________________________________\n",
      "Ind: [c]\n",
      "run(c): [e1]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "M2 = Possibility('M2')\n",
    "\n",
    "BType('Ind',M2).judge('c')\n",
    "PType(run,['c'],M2).judge('e1')\n",
    "\n",
    "print(show(M2))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Witness conditions associated with ptypes"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "M:\n",
      "_____________________________________________\n",
      "right(b, a): [s1]\n",
      "left(a, b): [s2]\n",
      "_____________________________________________\n",
      "\n",
      "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(show(M))\n",
    "print(left_a_b.in_poss(M).query('s1'))\n",
    "print(right_b_a.in_poss(M).query('s2'))\n",
    "print(show(M))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Record Types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{x : Ind, c_boy : (lambda v:Ind . boy(v), [x]), y : Ind, c_dog : (lambda v:Ind . dog(v), [y]), e : (lambda v1:Ind . lambda v2:Ind . hug(v1, v2), [x, y])}\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\left[\\begin{array}{lcl}\n",
       "\\text{x} &:& \\textit{Ind}\\\\\n",
       "\\text{c}_{\\text{boy}} &:& \\langle \\lambda v:\\textit{Ind}\\ .\\ \\text{boy}(v), \\langle \\text{x}\\rangle\\rangle\\\\\n",
       "\\text{y} &:& \\textit{Ind}\\\\\n",
       "\\text{c}_{\\text{dog}} &:& \\langle \\lambda v:\\textit{Ind}\\ .\\ \\text{dog}(v), \\langle \\text{y}\\rangle\\rangle\\\\\n",
       "\\text{e} &:& \\langle \\lambda v_{1}:\\textit{Ind}\\ .\\ \\lambda v_{2}:\\textit{Ind}\\ .\\ \\text{hug}(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": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "boy = Pred('boy',[Ind])\n",
    "dog = Pred('dog',[Ind])\n",
    "a_boy_hugs_a_dog = RecType({'x':Ind,\n",
    "                            'c_boy':(Fun('v',Ind,PType(boy,['v'])), ['x']),\n",
    "                            'y':Ind,\n",
    "                            'c_dog':(Fun('v',Ind,PType(dog,['v'])), ['y']),\n",
    "                            'e':(Fun('v1',Ind,Fun('v2',Ind, PType(hug,['v1','v2']))), \n",
    "                                     ['x','y'])})\n",
    "print(show(a_boy_hugs_a_dog))\n",
    "show_latex(a_boy_hugs_a_dog)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "M3:\n",
      "_____________________________________________\n",
      "Ind: [a, b]\n",
      "boy(a): [s1]\n",
      "dog(b): [s2]\n",
      "hug(a, b): [s3]\n",
      "_____________________________________________\n",
      "\n"
     ]
    }
   ],
   "source": [
    "M3 = Possibility('M3')\n",
    "Ind3 = BType('Ind',M3)\n",
    "Ind3.judge('a')\n",
    "Ind3.judge('b')\n",
    "PType(boy,['a']).in_poss(M3).judge('s1')\n",
    "PType(dog,['b']).in_poss(M3).judge('s2')\n",
    "PType(hug,['a','b']).in_poss(M3).judge('s3')\n",
    "\n",
    "print(show(M3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{x = a, c_boy = s1, y = b, c_dog = s2, e = s3}\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\left[\\begin{array}{rcl}\n",
       "\\text{x} &=& \\text{a}\\\\\n",
       "\\text{c}_{\\text{boy}} &=& \\text{s}_{\\text{1}}\\\\\n",
       "\\text{y} &=& \\text{b}\\\\\n",
       "\\text{c}_{\\text{dog}} &=& \\text{s}_{\\text{2}}\\\\\n",
       "\\text{e} &=& \\text{s}_{\\text{3}}\n",
       "\\end{array}\\right]\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r1 = Rec({'x':'a','c_boy':'s1','y':'b','c_dog':'s2','e':'s3'})\n",
    "\n",
    "print(show(r1))\n",
    "show_latex(r1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "print(a_boy_hugs_a_dog.in_poss(M3).query(r1))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## String types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(pick_up(a, c)^attract_attention(a, b)^throw(a, c)^run_after(b, c)^pick_up(b, c)^return_stick(b, c, a))+\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}(\\text{pick_up}(\\text{a}, \\text{c})⁀\\text{attract_attention}(\\text{a}, \\text{b})⁀\\text{throw}(\\text{a}, \\text{c})⁀\\text{run_after}(\\text{b}, \\text{c})⁀\\text{pick_up}(\\text{b}, \\text{c})⁀\\text{return_stick}(\\text{b}, \\text{c}, \\text{a}))^+\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "M4 = Possibility('M4')\n",
    "pick_up = Pred('pick_up',[Ind,Ind])\n",
    "attract_attention = Pred('attract_attention',[Ind,Ind])\n",
    "throw = Pred('throw',[Ind,Ind])\n",
    "run_after = Pred('run_after',[Ind,Ind])\n",
    "return_stick = Pred('return_stick',[Ind,Ind,Ind])\n",
    "Ind4 = BType('Ind')\n",
    "Ind4.in_poss(M4)\n",
    "Ind4.judge('a')\n",
    "Ind4.judge('b')\n",
    "Ind4.judge('c')\n",
    "pick_up_a_c = PType(pick_up,['a','c'])\n",
    "attract_attention_a_b = PType(attract_attention,['a','b'])\n",
    "throw_a_c = PType(throw,['a','c'])\n",
    "run_after_b_c = PType(run_after,['b','c'])\n",
    "pick_up_b_c = PType(pick_up,['b','c'])\n",
    "return_stick_b_c_a = PType(return_stick,['b','c','a'])\n",
    "\n",
    "FetchOnce_a_b_c = TTRStringType([pick_up_a_c,attract_attention_a_b,throw_a_c,run_after_b_c,\n",
    "                                 pick_up_b_c,return_stick_b_c_a])\n",
    "Fetch_a_b_c = KPlusStringType(FetchOnce_a_b_c)\n",
    "print(show(Fetch_a_b_c))\n",
    "show_latex(Fetch_a_b_c)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\"e1 e2 e3 e4 e5 e6\"\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\text{e}_{\\text{1}}\\ \\text{e}_{\\text{2}}\\ \\text{e}_{\\text{3}}\\ \\text{e}_{\\text{4}}\\ \\text{e}_{\\text{5}}\\ \\text{e}_{\\text{6}}\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pick_up_a_c.in_poss(M4).judge('e1')\n",
    "attract_attention_a_b.in_poss(M4).judge('e2')\n",
    "throw_a_c.in_poss(M4).judge('e3')\n",
    "run_after_b_c.in_poss(M4).judge('e4')\n",
    "pick_up_b_c.in_poss(M4).judge('e5')\n",
    "return_stick_b_c_a.in_poss(M4).judge('e6')\n",
    "e1_6 = TTRString(['e1','e2','e3','e4','e5','e6'])\n",
    "print(show(e1_6))\n",
    "show_latex(e1_6)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "print(FetchOnce_a_b_c.in_poss(M4).query(e1_6))\n",
    "print(Fetch_a_b_c.in_poss(M4).query(e1_6))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "lambda r:{x : Ind, c_human : (lambda v:Ind . human(v), [x]), y : Ind, c_dog : (lambda v:Ind . dog(v), [y]), z : Ind, c_stick : (lambda v:Ind . stick(v), [z]), e : (lambda v1:Ind . lambda v2:Ind . lambda v3:Ind . pick_up(v1, v3)^attract_attention(v1, v2), [x, y, z])} . {e : play_fetch([r, ., x], [r, ., y])}\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\lambda r:\\left[\\begin{array}{lcl}\n",
       "\\text{x} &:& \\textit{Ind}\\\\\n",
       "\\text{c}_{\\text{human}} &:& \\langle \\lambda v:\\textit{Ind}\\ .\\ \\text{human}(v), \\langle \\text{x}\\rangle\\rangle\\\\\n",
       "\\text{y} &:& \\textit{Ind}\\\\\n",
       "\\text{c}_{\\text{dog}} &:& \\langle \\lambda v:\\textit{Ind}\\ .\\ \\text{dog}(v), \\langle \\text{y}\\rangle\\rangle\\\\\n",
       "\\text{z} &:& \\textit{Ind}\\\\\n",
       "\\text{c}_{\\text{stick}} &:& \\langle \\lambda v:\\textit{Ind}\\ .\\ \\text{stick}(v), \\langle \\text{z}\\rangle\\rangle\\\\\n",
       "\\text{e} &:& \\langle \\lambda v_{1}:\\textit{Ind}\\ .\\ \\lambda v_{2}:\\textit{Ind}\\ .\\ \\lambda v_{3}:\\textit{Ind}\\ .\\ \\text{pick_up}(v_{1}, v_{3})⁀\\text{attract_attention}(v_{1}, v_{2}), \\langle \\text{x}, \\text{y}, \\text{z}\\rangle\\rangle\n",
       "\\end{array}\\right]\\ .\\ \\left[\\begin{array}{lcl}\n",
       "\\text{e} &:& \\text{play_fetch}(r\\text{.}\\text{x}, r\\text{.}\\text{y})\n",
       "\\end{array}\\right]\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "human = Pred('human',[Ind])\n",
    "stick = Pred('stick',[Ind])\n",
    "play_fetch = Pred('play_fetch',[Ind,Ind])\n",
    "T = RecType({'x':Ind,\n",
    "             'c_human':(Fun('v',Ind,PType(human,['v'])),['x']),\n",
    "             'y':Ind,\n",
    "             'c_dog':(Fun('v',Ind,PType(dog,['v'])),['y']),\n",
    "             'z':Ind,\n",
    "             'c_stick':(Fun('v',Ind,PType(stick,['v'])),['z']),\n",
    "             'e':(Fun('v1',Ind,Fun('v2',Ind,Fun('v3',Ind, \n",
    "                                                TTRStringType([PType(pick_up,['v1','v3']),\n",
    "                                                               PType(attract_attention,['v1','v2'])])))),\n",
    "                 ['x','y','z'])})\n",
    "f = Fun('r',T,RecType({'e':PType(play_fetch,[LazyObj(['r','.','x']),LazyObj(['r','.','y'])])}))\n",
    "\n",
    "print(show(f))\n",
    "show_latex(f)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "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.9.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}