Documentation

Check that the number is zero.

Check that the number is positive, i.e. greater than zero.

Check that the number is greater than one (i.e. at least two).

The naming comes from the paper.

Generate valid binary numbers.

Calculate the sum c of two numbers a and b.

>>> extract' <$> run (addo (inject' 3) (inject' 5))
[Just [O,O,O,I]]

One can turn it around to subtract from a number:

>>> extract' <$> run (\b -> addo (inject' 2) b (inject' 8))
[Just [O,I,I]]

When both summands are unknown, every possible pair will be enumerated.

>>> bimap extract' extract' <$> run (\(a, b) -> addo a b (inject' 2))
[(Just [O,I],Just []),(Just [],Just [O,I]),(Just [I],Just [I])]

If one of the summands is greater than the sum, the relation will produce no results.

>>> run (\a -> addo a (inject' 10) (inject' 3))
[]

The implementation of add is discussed in section 4 of the paper.

Calculate the difference c of two numbers a and b. This is just addo, but with parameters in different order.

Check that a is strictly less than b. Otherwise, the goal fails.

>>> run (\() -> lesso (inject' 3) (inject' 4))
[()]
>>> run (\() -> lesso (inject' 3) (inject' 2))
[]

One can turn this relation around to generate numbers less or greater than a given one.

>>> extract' <$> run (\x -> lesso x (inject' 4))
[Just [],Just [I],Just [I,I],Just [O,I]]
>>> take 5 $ extract' <$> run (\x -> lesso (inject' 4) x)
[Just [I,O,I],Just [O,I,I],Just [I,I,I],Just [O,O,O,I],Just [I,O,O,I]]

Calculate the product c of two numbers a and b.

>>> extract' <$> run (mulo (inject' 3) (inject' 4))
[Just [O,O,I,I]]

One can turn this around to factor a given number.

>>> extract' <$> run (\a -> mulo a (inject' 2) (inject' 12))
[Just [O,I,I]]
>>> bimap extract' extract' <$> run (\(a, b) -> mulo a b (inject' 4))
[(Just [I],Just [O,O,I]),(Just [O,I],Just [O,I]),(Just [O,O,I],Just [I])]

The goal will fail if any multiplier is not a factor of the product.

>>> run (\a -> mulo a (inject' 5) (inject' 7))
[]

The implementation of mul is discussed in section 5 of the paper.

Calculate the quotient q and remainder r of dividing n by m.

>>> bimap extract' extract' <$> run (\(q, r) -> divo (inject' 17) (inject' 5) q r)
[(Just [I,I],Just [O,I])]

One can turn this around to find divisors of a number.

>>> extract' <$> run (\m -> fresh >>= \q -> divo (inject' 12) m q (inject' 0))
[Just [O,O,I,I],Just [I],Just [I,I],Just [O,I,I],Just [O,I],Just [O,O,I]]

The implementation of div is discussed in section 6 of the paper.

Calculate discrete logarithm q of a number n in base b, perhaps with some remainder r.

>>> bimap extract' extract' <$> run (\(q, r) -> logo (inject' 9) (inject' 3) q r)
[(Just [O,I],Just [])]
>>> bimap extract' extract' <$> run (\(q, r) -> logo (inject' 15) (inject' 3) q r)
[(Just [O,I],Just [0,I,I])]

One can turn this around to find the number b raised to some power q:

>>> extract' <$> run (\n -> logo n (inject' 5) (inject' 2) (inject' 0))
[Just [I,O,O,I,I]]

or to find the q-th root of n:

>>> extract' <$> run (\b -> logo (inject' 8) b (inject' 3) (inject' 0))
[Just [O,I]]

If you want to enumerate solutions to logo n b q r, you probably shouldn't go beyond the first 16 solutions without an OOM killer.

The original implementation of this relation in Prolog can be found at https://okmij.org/ftp/Prolog/Arithm/pure-bin-arithm.prl. Although the paper mentions this relation in section 6, it does not discuss its implementation in detail.