documentation/loop-guards-termination.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "source": [
    "# Loop Guards & Moments After Termination"
   ],
   "metadata": {
    "collapsed": false
   }
  },
  {
   "cell_type": "markdown",
   "source": [
    "Polar can analyze stochastic processes that do not stop given by a probabilistic loop with the loop guard `true`.\n",
    "However, Polar can also analyze loops with a proper guard. Allowing for any loop guard quickly gets us in the real of undecidability and uncomputable problems.\n",
    "But, Polar guarantees that for the loops it accepts it will theoretically be able to give an answer. That is why not any loop guard is allowed.\n",
    "The restrictions on the loop guard are the same as the ones for the if-conditions: *all variables in the loop guard must only assume finitely many values*.\n",
    "In fact, when Polar converts the input loop into its normal form, the loop guard is converted into an if-statement that wraps to whole loop body. Let's look at an example:"
   ],
   "metadata": {
    "collapsed": false
   }
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\r\n",
      "stop = 0\r\n",
      "steps = 0\r\n",
      "x = 1\r\n",
      "while stop == 0:\r\n",
      "    stop = Bernoulli(1/2)\r\n",
      "    x = 2*x\r\n",
      "    steps = steps + 1\r\n",
      "end\r\n"
     ]
    }
   ],
   "source": [
    "!cat loops/geometric.prob"
   ],
   "metadata": {
    "collapsed": false,
    "pycharm": {
     "name": "#%%\n"
    }
   }
  },
  {
   "cell_type": "markdown",
   "source": [
    "The variable `stop` in the guard can only assume the values `0` and `1`. Hence, the guard is supported by Polar.\n",
    "We can still ask Polar to compute closed-form formulas for moments of program variables parameterized by the number of loop iterations `n`.\n",
    "An important question is: \"What is the meaning of this formula if the loop terminates in less than `n` many iterations?\".\n",
    "As mentioned, Polar converts a guarded loop into an unguarded loop by wrapping the loop body into an if-statement for which the condition is the original loop guard.\n",
    "Hence, every variable still corresponds to an infinite sequence of numbers. However, after the loop guard is falsified (and the loop would terminate), the values of the program variables stay the same. Let's compute some closed-form formulas for the exepcted values of the program variables:"
   ],
   "metadata": {
    "collapsed": false
   }
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001B[32m\r\n",
      "8888888b.   .d88888b.  888             d8888 8888888b.\r\n",
      "888   Y88b d88P\" \"Y88b 888            d88888 888   Y88b\r\n",
      "888    888 888     888 888           d88P888 888    888\r\n",
      "888   d88P 888     888 888          d88P 888 888   d88P\r\n",
      "8888888P\"  888     888 888         d88P  888 8888888P\"\r\n",
      "888        888     888 888        d88P   888 888 T88b\r\n",
      "888        Y88b. .d88P 888       d8888888888 888  T88b\r\n",
      "888         \"Y88888P\"  88888888 d88P     888 888   T88b\r\n",
      "\r\n",
      "By the ProbInG group\r\n",
      "\u001B[0m\r\n",
      "\r\n",
      "\r\n",
      "\u001B[36m-------------------\u001B[0m\r\n",
      "\u001B[36m- Analysis Result -\u001B[0m\r\n",
      "\u001B[36m-------------------\u001B[0m\r\n",
      "\r\n",
      "E(stop) = 0; 1 - 1/2**n\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "E(steps) = 0; 2 - 2/2**n\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "E(x) = 1; 2; n + 1\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "Elapsed time: 0.42545104026794434 s\r\n"
     ]
    }
   ],
   "source": [
    "!python ../polar.py loops/geometric.prob --goals \"E(stop)\" \"E(steps)\" \"E(x)\""
   ],
   "metadata": {
    "collapsed": false,
    "pycharm": {
     "name": "#%%\n"
    }
   }
  },
  {
   "cell_type": "markdown",
   "source": [
    "The closed-form for `E(stop)` is `1 - 1/2**n`. Which can intuitively be explained as follows: once stop becomes `1` it will remain `1` forever. Moreover, in every iteration there is a fifty-fifty chance of `stop` becoming `1`.\n",
    "\n",
    "Polar also provides functionality to compute the moments of program variables after termination by using the `after_loop` parameter:"
   ],
   "metadata": {
    "collapsed": false
   }
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001B[32m\r\n",
      "8888888b.   .d88888b.  888             d8888 8888888b.\r\n",
      "888   Y88b d88P\" \"Y88b 888            d88888 888   Y88b\r\n",
      "888    888 888     888 888           d88P888 888    888\r\n",
      "888   d88P 888     888 888          d88P 888 888   d88P\r\n",
      "8888888P\"  888     888 888         d88P  888 8888888P\"\r\n",
      "888        888     888 888        d88P   888 888 T88b\r\n",
      "888        Y88b. .d88P 888       d8888888888 888  T88b\r\n",
      "888         \"Y88888P\"  88888888 d88P     888 888   T88b\r\n",
      "\r\n",
      "By the ProbInG group\r\n",
      "\u001B[0m\r\n",
      "\r\n",
      "\r\n",
      "\u001B[36m-------------------\u001B[0m\r\n",
      "\u001B[36m- Analysis Result -\u001B[0m\r\n",
      "\u001B[36m-------------------\u001B[0m\r\n",
      "\r\n",
      "E(stop) = 1\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "E(steps) = 2\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "E(x) = oo\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "Elapsed time: 1.2863147258758545 s\r\n"
     ]
    }
   ],
   "source": [
    "!python ../polar.py loops/geometric.prob --goals \"E(stop)\" \"E(steps)\" \"E(x)\" --after_loop"
   ]
  },
  {
   "cell_type": "markdown",
   "source": [
    "We can see that the expected value of `stop` is `1` after termination. In fact, `stop` will be `1` with absolute certainty, because the loop terminates precisely when `stop` is `1`. Moreover, the loop has an expected runtime of `2` and surprisingly the expected value of `x` after termination is infinite. This phenomenon can be intuitively explained as follows: later iterations become more and more unlikely. The chance of not terminating decreases exponentially. However, the value of `x` increases exponentially. The exponential decrease of the probability of non-termination and the exponential increase of `x` cancel each other out.\n",
    "\n",
    "Another possibility the get some information after the loop terminates is to compute the invariant ideal ([see the notebook on this topic](invariants.ipynb)).\n",
    "The invariants Polar computes are equations among the moments of program variables that are true after every iteration of the loop. Because of our mechanism of converting guarded loops into unguarded loops by using an if-statement the computed invariants are also true after termination of the loop. Let's see what we get for our example:"
   ],
   "metadata": {
    "collapsed": false
   }
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001B[32m\r\n",
      "8888888b.   .d88888b.  888             d8888 8888888b.\r\n",
      "888   Y88b d88P\" \"Y88b 888            d88888 888   Y88b\r\n",
      "888    888 888     888 888           d88P888 888    888\r\n",
      "888   d88P 888     888 888          d88P 888 888   d88P\r\n",
      "8888888P\"  888     888 888         d88P  888 8888888P\"\r\n",
      "888        888     888 888        d88P   888 888 T88b\r\n",
      "888        Y88b. .d88P 888       d8888888888 888  T88b\r\n",
      "888         \"Y88888P\"  88888888 d88P     888 888   T88b\r\n",
      "\r\n",
      "By the ProbInG group\r\n",
      "\u001B[0m\r\n",
      "\r\n",
      "\r\n",
      "\u001B[36m-------------------\u001B[0m\r\n",
      "\u001B[36m- Analysis Result -\u001B[0m\r\n",
      "\u001B[36m-------------------\u001B[0m\r\n",
      "\r\n",
      "E(stop) = 0; 1 - 1/2**n\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "E(steps) = 0; 2 - 2/2**n\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "E(x) = 1; 2; n + 1\r\n",
      "\u001B[32mSolution is exact\u001B[0m\r\n",
      "\r\n",
      "\r\n",
      "\u001B[36m-------------------\u001B[0m\r\n",
      "\u001B[36m-   Invariants    -\u001B[0m\r\n",
      "\u001B[36m-------------------\u001B[0m\r\n",
      "\r\n",
      "Following is a gröbner basis for the invariant ideal:\r\n",
      "\r\n",
      "-E(steps) + 2*E(stop) = 0\r\n",
      "\r\n",
      "Elapsed time: 0.45613980293273926 s\r\n"
     ]
    }
   ],
   "source": [
    "!python ../polar.py loops/geometric.prob --goals \"E(stop)\" \"E(steps)\" \"E(x)\" --invariants"
   ],
   "metadata": {
    "collapsed": false,
    "pycharm": {
     "name": "#%%\n"
    }
   }
  },
  {
   "cell_type": "markdown",
   "source": [
    "Rewritten, the invariant we get states `E(steps) = 2*E(stop)`. We know from the previous output that after termination `E(steps) = 2` and `E(stop) = 1` which is consistent with the invariant we got.\n",
    "\n",
    "We can compute the basis for the invariant ideal also using Python code as follows:"
   ],
   "metadata": {
    "collapsed": false
   }
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{E(steps) - 2*E(stop)}\n"
     ]
    }
   ],
   "source": [
    "from inputparser import Parser\n",
    "from program import normalize_program\n",
    "from recurrences import RecBuilder\n",
    "from recurrences.solver import RecurrenceSolver\n",
    "from invariants import InvariantIdeal\n",
    "\n",
    "program = Parser().parse_file(\"loops/geometric.prob\")\n",
    "# Construct normal form so that Polar can analyze it\n",
    "program = normalize_program(program)\n",
    "\n",
    "# Construct and solve recurrences\n",
    "rec_builder = RecBuilder(program)\n",
    "monomials = [\"steps\", \"stop\", \"x\"]\n",
    "closed_forms = {}\n",
    "for monomial in monomials:\n",
    "    # Construct the recurrences describing E(monomial) -> expected value of monomial\n",
    "    recurrences = rec_builder.get_recurrences(monomial)\n",
    "    # solve and save the closed-forms (use E(monomial) as the id because the loop is probabilistic)\n",
    "    closed_forms[f\"E({monomial})\"] = RecurrenceSolver(recurrences).get(monomial)\n",
    "\n",
    "# Construct the invariant ideal\n",
    "invariant_ideal = InvariantIdeal(closed_forms)\n",
    "basis = invariant_ideal.compute_basis()\n",
    "print(basis)"
   ],
   "metadata": {
    "collapsed": false,
    "pycharm": {
     "name": "#%%\n"
    }
   }
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 2
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython2",
   "version": "2.7.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}