{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "d5f11bfa",
   "metadata": {
    "tags": []
   },
   "source": [
    "# Introduction of using the `theodias` package"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0ece8f88",
   "metadata": {},
   "source": [
    "The `theodias` package provides different classes and methods to apply the theory of dialectical structures (as introduced in [Betz (2010)](https://doi.org/10.5771/9783465136293) and [Betz (2013)](https://www.springer.com/de/book/9789400745988)). \n",
    "\n",
    "The provided functionalities are described by two abstract classes. Implementations of `DialecticalStructure` can be used to create, manipulate and calculate properties of dialectical structures. Implementations of `Position` represent positions on a sentence pool.\n",
    "\n",
    "The `theodias` package includes different implementations of these abstract classes, which differ w.r.t. their runtime performance:\n",
    "\n",
    "+ *DAG (directed acyclic graphs) based dialectical structures:* All important properties of the stucture are calculated and stored during instantiation. This implementation is fast for small sentence pools ($n<15$).\n",
    "    + We recommend to use the following standard implementation: `DAGDialecticalStructure`.\n",
    "+ *BDD (binary decision diagramm) based dialectical structures:* Important properties of the structure are calculated by using binary decision trees. This representation is comparably fast for most properties of the graph even if the sentence pool is larger ($n>10$). However, for larger sentence pools it will become more difficult to calculate all dialectically consistent positions, axiomatic bases (without a confining source) and minimal positions.\n",
    "   + We recommend to use the following standard implementation: `BDDDialecticalStructure`."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ac3e219b-769b-4684-ae2b-da8f9616e820",
   "metadata": {},
   "source": [
    "## How to run this notebook"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a677881a-a56f-4515-b7ec-1c27a4e41563",
   "metadata": {},
   "source": [
    "There are several possibilities to execute this notebook. You can, for instance,\n",
    "\n",
    "1. execute this notebook on Colab: [![Open In Colab](https://colab.research.google.com/assets/colab-badge.svg)](https://colab.research.google.com/github/re-models/theodias/blob/master/docs-source/tutorials/theodias-tutorial.ipynb), or\n",
    "2. execute this notebook locally in, for instance, [JupyterLab](https://jupyter.org/). You can download this notebook from [here](https://github.com/re-models/theodias/blob/master/docs-source/tutorials/theodias-tutorial.ipynb)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fdc458b6-15cd-4129-9a37-557bf17462e7",
   "metadata": {},
   "source": [
    "## Installing libraries"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "958c5eaf-d87c-4154-8abd-d2e14faafae9",
   "metadata": {},
   "outputs": [],
   "source": [
    "%pip install theodias"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "02a222d0-d84b-402a-a393-41ea573b757d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Are we on Colab? No!\n"
     ]
    }
   ],
   "source": [
    "# Are we on Colab?\n",
    "on_colab = 'google.colab' in str(get_ipython())\n",
    "print(f\"Are we on Colab? {'Yes' if on_colab else 'No'}!\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1d3490f0",
   "metadata": {},
   "source": [
    "## Instantiation of dialectical structures and positions"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fe545b46",
   "metadata": {},
   "source": [
    "A dialectical structure is a tupel  $\\left<S,A\\right>$ of a sentence pool $S = \\{ s_1, s_2, \\dots, s_n, \\neg s_1, \\neg s_2, \\dots, \\neg s_n \\}$ and a set $A$ of arguments.\n",
    "\n",
    "An argument $a=(P_a, c_a)$ is defined as a pair consisting of premises $P_a \\subset S$ and a conclusion $c_a \\in S$.\n",
    "\n",
    "A dialectical structure is instantiated by specifying the size $n$ of the sentence pool and a list of arguments, in which sententences are represented numerals. The minus sign is used to indicate the negation of a sentence. For instance, the list `[1,3,-4]` represents an argument with the premsises $P_a=\\{s_1,s_3\\}$ and the conclusion $\\neg s_4$.   "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "a7d673a7",
   "metadata": {},
   "outputs": [],
   "source": [
    "from theodias import DAGDialecticalStructure\n",
    "\n",
    "# size of the sentencepool\n",
    "n = 7\n",
    "# a list of arguments\n",
    "arguments = [[1, 3],[1, 4],[1, 5],[1, -6], [2, -4],[2, 5],[2, 6],[2, 7]]\n",
    "# instantiation of a dialectical structure tau\n",
    "tau = DAGDialecticalStructure.from_arguments(arguments, n)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1d27589c",
   "metadata": {},
   "source": [
    "A position is a binary belief state that is represented by a subset $\\mathcal{A}\\subset S$ over the sentence pool $S$. The internal representation depends on the implementation. However, independent of their implementation, positions can be instantiated by specifying the set of sentences the agent believes:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "503b3c85",
   "metadata": {},
   "outputs": [],
   "source": [
    "from theodias import StandardPosition\n",
    "\n",
    "# believing s_3, s_4 and s_5\n",
    "belief_state_a = StandardPosition.from_set({3, 4, 5}, n)\n",
    "\n",
    "# believing s_2 and believing that s_4 is false \n",
    "belief_state_b = StandardPosition.from_set({2,-4}, n)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e7f5ba6a",
   "metadata": {},
   "source": [
    "The `theodias` package provides several methods to manipulate dialectical structures and to determine properties of positions with regard to a given dialectical structure. For instance:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "a75ca4fd",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Implications of {3, 4, 5}: {3, 4, 5, -2}\n",
      "Implications of {2, -4}: {2, 5, 6, 7, -4, -1}\n",
      "Is {3, 4, 5} consistent? True\n",
      "Is {2, -4} consistent? True\n",
      "Are {3, 4, 5} and {2, -4} consistent with each other? False\n"
     ]
    }
   ],
   "source": [
    "# implications of a believed sentences w.r.t. the \n",
    "# inferential relationships encoded in tau\n",
    "print(f\"Implications of {belief_state_a}: {tau.closure(belief_state_a)}\")\n",
    "print(f\"Implications of {belief_state_b}: {tau.closure(belief_state_b)}\")\n",
    "\n",
    "# checking whether a position is consistent w.r.t. tau\n",
    "print(f\"Is {belief_state_a} consistent? {tau.is_consistent(belief_state_a)}\")\n",
    "print(f\"Is {belief_state_b} consistent? {tau.is_consistent(belief_state_b)}\")\n",
    "\n",
    "# checking whether two positions are consistent with each other (w.r.t tau)\n",
    "print(f\"Are {belief_state_a} and {belief_state_b} consistent with each other?\" +\n",
    "      f\" {tau.are_compatible(belief_state_a,belief_state_b)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a8917961-0c49-4017-8214-b93ed259bf01",
   "metadata": {},
   "source": [
    "### Important notes"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "544e78dd-68a1-464a-93cd-8e63d05fcb69",
   "metadata": {},
   "source": [
    "You can operate with position in the usual set-theoretic fashion:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "bcd40bda-af9b-43d3-aad0-91898edb729a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{3, 4, 5, 6}\n",
      "{4, 5}\n",
      "{3}\n"
     ]
    }
   ],
   "source": [
    "pos1 = StandardPosition.from_set({3, 4, 5}, n)\n",
    "pos2 = StandardPosition.from_set({4, 5, 6}, n)\n",
    "# set-theoretic union\n",
    "print(pos1 | pos2)\n",
    "# set-theoretic intersection\n",
    "print(pos1 & pos2)\n",
    "# set-theoretic difference\n",
    "print(pos1 - pos2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "743a6131-0a28-447a-b02a-20462455ce27",
   "metadata": {},
   "source": [
    "Positions are **immutable**---that is, you cannot change them once instantiated. If you want to change, for instance, the underlying sentence pool, you can reinstantiate the position:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "6102fe3c-d52b-46e8-88f9-0574c6bfd861",
   "metadata": {},
   "outputs": [],
   "source": [
    "# instantiating {3, 4, 5} with a sentence pool of size 5\n",
    "pos_n5 = StandardPosition.from_set({3, 4, 5}, 5)\n",
    "# changing the underlying sentence to a larger sentence-pool size.\n",
    "pos_n6 = StandardPosition.from_set(pos_n5.as_set(), 6)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d7f7f421-7a91-4566-8c3a-5039542e313f",
   "metadata": {},
   "source": [
    "Since positions are immutable, you can use them as keys in, e.g., dictionaries and form sets of positions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "99e7e24b-2624-443d-ba32-adf6b0b6b50c",
   "metadata": {},
   "outputs": [],
   "source": [
    "set_of_positions = {pos_n5, pos_n6}"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d9ecb45a-883d-4c65-a265-1aa5252bfffa",
   "metadata": {},
   "source": [
    "**Identity criteria:** A position is determined by its sentences and the corresponding sentence pool. Consequently, whether two numerically distinct positions are considered the same (as in :code:`pos1 == pos2`) does not depend on the implementation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "8f845af7-5a0b-4abb-9cdc-da808acfc982",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "from theodias import SetBasedPosition, BitarrayPosition, NumpyPosition\n",
    "# instantiating {3, 4, 5} with a sentence pool of size 5 with different implementations\n",
    "\n",
    "pos_setbased = SetBasedPosition.from_set({3, 4, 5}, 5)\n",
    "pos_bitarray = BitarrayPosition.from_set({3, 4, 5}, 5)\n",
    "pos_np = NumpyPosition.from_set({3, 4, 5}, 5)\n",
    "\n",
    "print(pos_setbased == pos_bitarray)\n",
    "print(pos_setbased == pos_np)\n",
    "print(pos_np == pos_bitarray)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d08b35f1-018a-4a9f-82ab-39765d44930b",
   "metadata": {},
   "source": [
    "A position is **bound to a specific sentence pool**. If you pass positions to functions that have non-matching sentence pools, the function will raise a `ValueError`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "2f4a7f88-f3c5-4efc-b384-14e82bba38e9",
   "metadata": {},
   "outputs": [],
   "source": [
    "# size of the sentencepool\n",
    "n = 3\n",
    "# a list of arguments\n",
    "arguments = [[1, 3],[1, 2]]\n",
    "# instantiation of a dialectical structure tau\n",
    "tau = DAGDialecticalStructure.from_arguments(arguments, n)\n",
    "\n",
    "print(tau.is_complete(StandardPosition.from_set({1, 3}, n=3)))\n",
    "# calling a function with the \"same\" position based on another sentence pool: Raises a ValueError\n",
    "print(tau.is_complete(StandardPosition.from_set({1, 3}, n=4)))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "109c3058",
   "metadata": {
    "tags": []
   },
   "source": [
    "## Export to JSON"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b91b15e4",
   "metadata": {},
   "source": [
    "### Serializing `theodias` objects"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "52797210",
   "metadata": {},
   "source": [
    "You can serialize `theodias` positions and dialectical structures and any compounds thereof, as long as the `json` python module can handle them (e.g., lists, dictionaries).\n",
    "\n",
    "For instance, the following code will serialize a position:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "5d68b149",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{\n",
      "    \"n_unnegated_sentence_pool\": 4,\n",
      "    \"position\": [\n",
      "        1,\n",
      "        2\n",
      "    ]\n",
      "}\n",
      "[\n",
      "    {\n",
      "        \"n_unnegated_sentence_pool\": 4,\n",
      "        \"position\": [\n",
      "            1,\n",
      "            2\n",
      "        ]\n",
      "    },\n",
      "    {\n",
      "        \"n_unnegated_sentence_pool\": 4,\n",
      "        \"position\": [\n",
      "            1,\n",
      "            3\n",
      "        ]\n",
      "    },\n",
      "    {\n",
      "        \"n_unnegated_sentence_pool\": 0,\n",
      "        \"position\": []\n",
      "    }\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "from theodias import StandardPosition\n",
    "from theodias.util import tau_dumps, tau_dump\n",
    "from os import getcwd, path\n",
    "\n",
    "# serializing a position as JSON String\n",
    "pos_json_str = tau_dumps(StandardPosition.from_set({1,2},4),\n",
    "                         indent=4)\n",
    "print(pos_json_str)\n",
    "\n",
    "# serializing a list of positions\n",
    "pos_list = [StandardPosition.from_set({1,2},4),\n",
    "            StandardPosition.from_set({1,3},4),\n",
    "            StandardPosition.from_set(set(),0)]\n",
    "print(tau_dumps(pos_list, indent=4))\n",
    "\n",
    "# serializing a list of position into a file\n",
    "# only if we are not on colab\n",
    "if not on_colab:\n",
    "    output_file_path = path.join(getcwd(),'positions.json')\n",
    "    with open(file=output_file_path, mode='w') as output_file:\n",
    "        tau_dump(pos_list, output_file, indent=4)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4e4b110d",
   "metadata": {},
   "source": [
    "If important, you can save the implementation details (module and class name), which can be considered later to deserialize the objects:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "c11cdb11",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{\n",
      "    \"n_unnegated_sentence_pool\": 4,\n",
      "    \"position\": [\n",
      "        1,\n",
      "        2\n",
      "    ],\n",
      "    \"module_name\": \"theodias.numpy_implementation\",\n",
      "    \"class_name\": \"NumpyPosition\"\n",
      "}\n"
     ]
    }
   ],
   "source": [
    "from theodias import SetBasedPosition\n",
    "from theodias.util import tau_dumps\n",
    "\n",
    "# serializing a position as JSON String\n",
    "pos_json_str = tau_dumps(StandardPosition.from_set({1,2},4),\n",
    "                         indent=4,\n",
    "                         serialize_implementation=True)\n",
    "print(pos_json_str)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9341fcc3",
   "metadata": {},
   "source": [
    "### Deserializing `theodias` objects"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cbc950a9",
   "metadata": {},
   "source": [
    "The deserialization of objects is similarly simple. The implementation details can either be taken from the json file or can be explicitly given via parameters."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "f07551e1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{1, 2} of type <class 'theodias.set_implementation.SetBasedPosition'>\n",
      "{1, 2} of type <class 'theodias.bitarray_implementation.BitarrayPosition'>\n",
      "[{1, 2}, {1, 3}, set()]\n"
     ]
    }
   ],
   "source": [
    "from theodias import SetBasedPosition, BitarrayPosition\n",
    "from theodias.util import tau_dumps, tau_loads, tau_load\n",
    "from os import getcwd, path\n",
    "\n",
    "# serializing a position as JSON String\n",
    "pos_json_str = tau_dumps(SetBasedPosition.from_set({1,2},4),\n",
    "                         indent=4,\n",
    "                         serialize_implementation=True)\n",
    "# deserializing it\n",
    "position = tau_loads(pos_json_str, use_json_specified_type = True )\n",
    "print(f\"{position} of type {type(position)}\")\n",
    "\n",
    "# deserializing it and using another implementation\n",
    "position = tau_loads(pos_json_str,\n",
    "                     position_module = 'theodias',\n",
    "                     position_class = 'BitarrayPosition' )\n",
    "print(f\"{position} of type {type(position)}\")\n",
    "\n",
    "# deserializing tau objects from a file (only if we are not on colab)\n",
    "if not on_colab:\n",
    "    input_file_path = path.join(getcwd(),'positions.json')\n",
    "    with open(file=input_file_path, mode='r') as input_file:\n",
    "        obj = tau_load(input_file)\n",
    "    print(obj)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "py39",
   "language": "python",
   "name": "py39"
  },
  "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.16"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}