Exhaustive search over the Cantor space in Python

exhaustive-search-conaturals.ipynb

{
  "cells": [
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Exhaustive search over the Cantor space in Python\n\n*[Ilya V. Schurov](https://ilya.schurov.com/)*\n\nThis is an implementation of weak exhaustive search over the Cantor space (Ulrich Berger, 1990), based on [this Twitter thread](https://twitter.com/shachaf/status/1530038181503987718) by @shachaf, which is based on [this post](http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/) by Martin Escardo."
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "### Conaturals\nThe set of conaturals consists of all natural numbers (beginning with 0) and $\\infty$. In @shachaf's thread, they were represented (in Haskell) as a sort of (possibly infinite) sequence of `S` with one `Z` at the end (for finite conaturals). \n\nThe natural way to represent possibly infinite sequences in Python is to use iterators. However, iterators are tricky: they can be consumed only once and thus cannot be reused. Thus we will respresent conatural as an iterable, either finite (in this case, conatural is equal to the number of elements in the iterable) or infinite (that corresponds to $\\infty$).\n\nAs I'd like to use generators to create conaturals and functions that return conatural, and generators create iterators and not iterables, I need a helper decorator to convert former to latter."
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def conatural(f):\n    \"\"\"\n    Makes a conatural out of generator by remembering its arguments\n    \"\"\"\n\n    class Conatural:\n        def __init__(self, *args, **kwargs):\n            self._args = args\n            self._kwargs = kwargs\n\n        def __iter__(self):\n            yield from f(*self._args, **self._kwargs)\n\n        def __add__(self, other):\n\n            # We have to return a conatural\n            @conatural\n            def add(cn, cm):\n                yield from cn\n                yield from cm\n\n            return add(self, other)\n\n    return Conatural\n\n\n# TEST\n@conatural\ndef cnrange(n):\n    for i in range(n):\n        yield i\n\n\nx = cnrange(3)\nassert list(x) == [0, 1, 2]\nassert list(x) == [0, 1, 2]\n# can consume it twice\n\nassert len(list(cnrange(3) + cnrange(4))) == 3 + 4\nassert len(list(cnrange(1) + cnrange(2) + cnrange(3))) == 1 + 2 + 3\n# addition works",
      "execution_count": 24,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "### Predicates"
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "Now let's define some total predicates on the set of conaturals. Due to totality assumption, they are guaranteed to halt, and therefore consume only finite part of the input. In other words, they cannot distinguish between infinity and “really large number”. I will make it explicit by defining the following helper function."
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def value_or_inf(cn, inf_border=100):\n    i = 0\n    for i, _ in enumerate(cn, 1):\n        if i >= inf_border:\n            return \"inf\"\n    return i\n\n\nassert value_or_inf([]) == 0\nassert value_or_inf(range(10)) == 10\nassert value_or_inf(range(100)) == \"inf\"",
      "execution_count": 2,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def is_huge(cn):\n    return value_or_inf(cn) == \"inf\"",
      "execution_count": 3,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def is_even_or_huge(cn):\n    value = value_or_inf(cn)\n    return value == \"inf\" or value % 2 == 0",
      "execution_count": 4,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "assert not is_even_or_huge(range(3))\nassert is_even_or_huge(range(0))\nassert is_even_or_huge(range(2))\nassert is_even_or_huge(range(10001))",
      "execution_count": 5,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def is_odd_or_huge(cn):\n    value = value_or_inf(cn)\n    return value == \"inf\" or value % 2 == 1",
      "execution_count": 6,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "assert is_odd_or_huge(range(3))\nassert not is_odd_or_huge(range(0))\nassert not is_odd_or_huge(range(2))\nassert is_odd_or_huge(range(10000))",
      "execution_count": 7,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def always_false(cn):\n    return False",
      "execution_count": 8,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def always_true(cn):\n    return True",
      "execution_count": 9,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "### `find`"
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "Now let's define `find`: a function of predicate `p` that yields such `n` that `p(n)` is `True` and `n` is the smallest with this property. If `p` never takes value `True`, `n` have to be $\\infty$. That's why we are working with conaturals here, and use `yield` instead of simply returning an index."
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "@conatural\ndef find(p):\n    i = 0\n    while True:\n        x = p(cnrange(i))\n        if not x:\n            yield i\n        else:\n            break\n        i += 1",
      "execution_count": 17,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "# helper function to get a value of conatural if it's finite\ndef resolve_finite(cn):\n    return sum(1 for x in cn)",
      "execution_count": 18,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "assert resolve_finite(find(is_even_or_huge)) == 0\nassert resolve_finite(find(is_odd_or_huge)) == 1\nassert resolve_finite(find(is_huge)) == 100",
      "execution_count": 19,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "### `exists` and `forall`"
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "The crucial part: let's implement `exists`, the function of a predicate `p` that tests are there any values of `n` such that `p(n)` is `True`."
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def exists(p):\n    return p(find(p))\n\n\nassert exists(is_even_or_huge)\nassert exists(is_odd_or_huge)\nassert not exists(always_false)",
      "execution_count": 20,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "Now it's easy to implement `forall`:"
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def forall(p):\n    return not exists(lambda x: not p(x))\n\n\nassert not forall(is_even_or_huge)\nassert not forall(is_odd_or_huge)\nassert forall(always_true)",
      "execution_count": 21,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "### Modulus of uniform continuity"
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "And finally we implement a function that finds *modulus of uniform continuity* of a predicate `p`, i.e. such number `k` that for all `n > k`, `p(n) == p(k)`. The implementation is rather straightforward. For any conatural `ck`, we define a predicate `q(cm)` that tests whether is it true that `p(ck + cm) == p(ck)`. If this predicate is `True` for all `cm`, then `ck` is larger or equal to the modulus of uniform continuity. Then we simply use `find` to get the first element `ck` that satisfies this property."
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "def modulus_of_uniform_cont(p):\n    def is_modulus(ck):\n        def q(cm):\n            return p(ck + cm) == p(ck)\n\n        return forall(q)\n\n    return find(is_modulus)",
      "execution_count": 22,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "assert resolve_finite(modulus_of_uniform_cont(is_huge)) == 100\nassert resolve_finite(modulus_of_uniform_cont(is_odd_or_huge)) == 99\nassert resolve_finite(modulus_of_uniform_cont(is_even_or_huge)) == 100\nassert resolve_finite(modulus_of_uniform_cont(always_true)) == 0\nassert resolve_finite(modulus_of_uniform_cont(always_false)) == 0",
      "execution_count": 23,
      "outputs": []
    }
  ],
  "metadata": {
    "kernelspec": {
      "name": "py3.10",
      "display_name": "Python 3.10",
      "language": "python"
    },
    "language_info": {
      "name": "python",
      "version": "3.10.0",
      "mimetype": "text/x-python",
      "codemirror_mode": {
        "name": "ipython",
        "version": 3
      },
      "pygments_lexer": "ipython3",
      "nbconvert_exporter": "python",
      "file_extension": ".py"
    },
    "@webio": {
      "lastKernelId": null,
      "lastCommId": null
    },
    "gist": {
      "id": "",
      "data": {
        "description": "Exhaustive search over the Cantor space in Python",
        "public": true
      }
    }
  },
  "nbformat": 4,
  "nbformat_minor": 5
}