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.