That really depends on what you want to do with it! My original question still stands: what is it that you want this program of yours to do? I can’t really imagine too many practical applications of the main theorem of the paper for a program written in Python. (Don’t get me wrong: it’s a really interesting paper, and I thank you for the link.)

As the type hints suggest, `omniscience`

accepts a function `f`

from `Ninf`

to `bool`

, and returns either an element of `Ninf`

or `None`

, telling you whether `f`

has a root or not (i.e., an input for which the returned value is `False`

rather than `True`

). If `f`

has a root (possibly many roots), `omniscience(f)`

returns one of those roots. If `f`

has no root, it returns `None`

. The truly remarkable part (and the point of the paper) is that this is possible at all - that there’s a decision algorithm to determine whether `f`

has a `root`

. There’s no such decision algorithm if you replace `Ninf`

with the natural numbers, even though `Ninf`

is in some sense larger than the natural numbers, being a copy of the natural numbers plus one extra “point at infinity”.

Here are some examples in Python, using the functions defined in my previous post. First, here’s a function that has a roots at `3`

and `5`

(really at `inj(3)`

and `inj(5)`

):

```
def f(x : Ninf) -> bool:
return x(2) <= x(3) and x(4) <= x(5)
```

Checking those roots:

```
>>> f(inj(3)) # 3 is a root
False
>>> f(inj(5)) # 5 is a root
False
>>> f(inj(17)) # all other inputs give True - no root
True
>>> f(inj(0))
True
>>> f(inj(2))
True
>>> f(lambda n: True) # no root at infinity, either
True
```

Now because `f`

has roots, `omniscience(f)`

should return one of those roots (in fact, it always returns the first root), and it does: it returns an element of `Ninf`

equivalent to `inj(3)`

.

```
>>> x = omniscience(f)
>>> x(2)
True
>>> x(3)
False
```

In contrast, if `f`

has no roots, `omniscience(f)`

is None:

```
>>> def f(x: Ninf) -> bool:
... return True
...
>>> omniscience(f)
>>> omniscience(f) is None
True
```

Note that all our functions need to be pure, total functions: completely deterministic, no dependence on external state, no exceptions, no infinite loops, etc… This is why something like Lean (or Agda, or Coq, or …) is much better suited to this kind of experimentation than Python - these restrictions are built in.