Isomorphic Data Encodings in Haskell and their
Generalization to Hylomorphisms on
Hereditarily Finite Data Types
Paul Tarau

arXiv:0808.2953v4 [cs.PL] 19 Jan 2009

Department of Computer Science and Engineering
University of North Texas
E-mail: tarau@cs.unt.edu

Abstract. This paper is an exploration in a functional programming
framework of isomorphisms between elementary data types (natural numbers, sets, multisets, finite functions, permutations binary decision diagrams, graphs, hypergraphs, parenthesis languages, dyadic rationals,
primes, DNA sequences etc.) and their extension to hereditarily finite
universes through hylomorphisms derived from ranking/unranking and
pairing/unpairing operations.
An embedded higher order combinator language provides any-to-any encodings automatically.
Besides applications to experimental mathematics, a few examples of
“free algorithms” obtained by transferring operations between data types
are shown. Other applications range from stream iterators on combinatorial objects to self-delimiting codes, succinct data representations and
generation of random instances.
The paper covers 59 data types and, through the use of the embedded
combinator language, provides 3540 distinct bijective transformations
between them.
The self-contained source code of the paper, as generated from a literate
Haskell program, is available at http://logic.csci.unt.edu/tarau/
research/2008/fISO.zip.
A short, 5 page version of the paper, published as [1] describes the idea
of organizing various data transformations as encodings to sequences of
natural numbers and gives a few examples of hylomorphisms that lift the
encodings to related hereditarily finite universes.
Keywords: Haskell data representations, data type isomorphisms, declarative combinatorics, computational mathematics, Ackermann encoding,
Gödel numberings, arithmetization, ranking/unranking, hereditarily finite sets, functions and permutations, encodings of binary decision diagrams, dyadic rationals, DNA encodings

1

Introduction

Analogical/metaphorical thinking routinely shifts entities and operations from
a field to another hoping to uncover similarities in representation or use [2].

Compilers convert programs from human centered to machine centered representations - sometime reversibly.
Complexity classes are defined through compilation with limited resources
(time or space) to similar problems [3,4].
Mathematical theories often borrow proof patterns and reasoning techniques
across close and sometime not so close fields.
A relatively small number of universal data types are used as basic building
blocks in programming languages and their runtime interpreters, corresponding to a few well tested mathematical abstractions like sets, functions, graphs,
groups, categories etc.
A less obvious leap is that if heterogeneous objects can be seen in some way
as isomorphic, then we can share them and compress the underlying informational universe by collapsing isomorphic encodings of data or programs whenever
possible.
Sharing heterogeneous data objects faces two problems:
– some form of equivalence needs to be proven between two objects A and
B before A can replace B in a data structure, a possibly tedious and error
prone task
– the fast growing diversity of data types makes harder and harder to recognize
sharing opportunities.
Besides, this rises the question: what guaranties do we have that sharing
across heterogeneous data types is useful and safe?
The techniques introduced in this paper provide a generic solution to these
problems, through isomorphic mappings between heterogeneous data types, such
that unified internal representations make equivalence checking and sharing possible. The added benefit of these “shapeshifting” data types is that the functors
transporting their data content will also transport their operations, resulting in
shortcuts that provide, for free, implementations of interesting algorithms. The
simplest instance is the case of isomorphisms – reversible mappings that also
transport operations. In their simplest form such isomorphisms show up as encodings to some simpler and easier to manipulate representation, for instance
natural numbers.
Such encodings can be traced back to Gödel numberings [5,6] associated to
formulae, but a wide diversity of common computer operations, ranging from
data compression and serialization to wireless data transmissions and cryptographic codes qualify.
Encodings between data types provide a variety of services ranging from free
iterators and random objects to data compression and succinct representations.
Tasks like serialization and persistence are facilitated by simplification of reading
or writing operations without the need of special purpose parsers. Sensitivity
to internal data representation format or size limitations can be circumvented
without extra programming effort.

2

An Embedded Data Transformation Language

We will start by designing an embedded transformation language as a set of
operations on a groupoid of isomorphisms. We will then extended it with a set
of higher order combinators mediating the composition of the encodings and the
transfer of operations between data types.
2.1

The Groupoid of Isomorphisms

We implement an isomorphism between two objects X and Y as a Haskell data
type encapsulating a bijection f and its inverse g. We will call the from function
the first component (a section in category theory parlance) and the to function
the second component (a retraction) defining the isomorphism. We can organize
isomorphisms as a groupoid as follows:
f = g −1
.........................................................................................................................................
X ......................................................................................................................................... Y
g = f −1
data Iso a b = Iso (a→b) (b→a)
from (Iso f _) = f
to (Iso _ g) = g
compose :: Iso a b → Iso b c → Iso a c
compose (Iso f g) (Iso f’ g’) = Iso (f’ . f) (g . g’)
itself = Iso id id
invert (Iso f g) = Iso g f

Assuming that for any pair of type Iso a b, f ◦ g = ida and g ◦ f = idb , we can
now formulate laws about isomorphisms that can be used to test correctness of
implementations with tools like QuickCheck [7].
Proposition 1 The data type Iso has a groupoid structure, i.e. the compose
operation, when defined, is associative, itself acts as an identity element and
invert computes the inverse of an isomorphism.
We can transport operations from an object to another with borrow and lend
combinators defined as follows:
borrow :: Iso t s → (t → t) → s → s
borrow (Iso f g) h x = f (h (g x))
borrow2 (Iso f g) h x y = f (h (g x) (g y))
borrowN (Iso f g) h xs = f (h (map g xs))
lend :: Iso s t
lend = borrow .
lend2 = borrow2
lendN = borrowN

→ (t → t) → s → s
invert
. invert
. invert

The combinators fit and retrofit just transport an object x through an
isomorphism and and apply to it an operation op available on the other side:
fit :: (b → c) → Iso a b → a → c
fit op iso x = op ((from iso) x)
retrofit :: (a → c) → Iso a b → b → c
retrofit op iso x = op ((to iso) x)

We can see the combinators from, to, compose, itself, invert, borrow,
lend, fit etc. as part of an embedded data transformation language. Note that
in this design we borrow from our strongly typed host programming language its
abstraction layers and safety mechanisms that continue to check the semantic
validity of the embedded language constructs.
2.2

Choosing a Root

To avoid defining n(n − 1)/2 isomorphisms between n objects, we choose a Root
object to/from which we will actually implement isomorphisms. We will extend
our embedded combinator language using the groupoid structure of the isomorphisms to connect any two objects through isomorphisms to/from the Root.
Choosing a Root object is somewhat arbitrary, but it makes sense to pick
a representation that is relatively easy convertible to various others, efficiently
implementable and, last but not least, scalable to accommodate large objects up
to the runtime system’s actual memory limits.
We will choose as our Root object finite sequences of natural numbers. They
can be seen as finite functions from an initial segment of N at, say [0..n],
to N at. This implies that a finite function can be seen as an array or a list of
natural numbers except that we do not limit the size of the representation of its
values. We will represent them as lists i.e. their Haskell type is [N at].
type Nat = Integer
type Root = [Nat]

We can now define an Encoder as an isomorphism connecting an object to Root
type Encoder a = Iso a Root

together with the combinators with and as providing an embedded transformation
language for routing isomorphisms through two Encoders.
with :: Encoder a→Encoder b→Iso a b
with this that = compose this (invert that)
as :: Encoder a → Encoder b → b → a
as that this thing = to (with that this) thing

The combinator with turns two Encoders into an arbitrary isomorphism, i.e.
acts as a connection hub between their domains. The combinator as adds a
more convenient syntax such that converters between A and B can be designed
as:

a2b x = as A B x
b2a x = as B A x

a2b = as B A

A

.........................................................................................................................................
.........................................................................................................................................
......
.......
........
.......
.....
......
.....
.....
.....
......
.....
.
.
.
.
.
.....
.
.....
......
....
.....
.....
−1
−1 ..............
......
.....
.....
.
.
.
.
.......
.........
.......
........

B

b2a = as A B
a
b

b

a

Root
A particularly useful combinator that transports binary operations from an Encoder to another, borrow from, can be defined as follows:
borrow_from :: Encoder a → (a → a → a) → Encoder b → b → b → b
borrow_from other op this x y = borrow2 (with other this) op x y

Note that one can also use the more intuitive equivalent definition
borrow_from’ other op this x y = z where
x’ = as other this x
y’ = as other this y
z’ = op x’ y’
z = as this other z’

given that the following equivalence always holds:
borrow f rom ≡ borrow f rom0

(1)

We will provide extensive use cases for these combinators as we populate our
groupoid of isomorphisms. Given that [N at] has been chosen as the root, we will
define our finite function data type fun simply as the identity isomorphism on
sequences in [N at].
fun :: Encoder [Nat]
fun = itself

3

Extending the Groupoid of Isomorphisms

We will now populate our groupoid of isomorphisms with combinators based on
a few primitive converters.
3.1

An Isomorphism between Finite Multisets and Finite Functions

Multisets [8] are unordered collections with repeated elements. Non-decreasing
sequences provide a canonical representation for multisets of natural numbers.
The isomorphism between finite multisets and finite functions is specified with
two bijections mset2fun and fun2mset.
mset :: Encoder [Nat]
mset = Iso mset2fun fun2mset

While finite multisets and sequences representing finite functions share a common representation [N at], multisets are subject to the implicit constraint that
their order is immaterial 1 . This suggest that a multiset like [4, 4, 1, 3, 3, 3] could
be represented by first ordering it as [1, 3, 3, 3, 4, 4] and then compute the differences between consecutive elements i.e. [x0 . . . xi , xi+1 . . .] → [x0 . . . xi+1 −xi . . .].
This gives [1, 2, 0, 0, 1, 0], with the first element 1 followed by the increments
[2, 0, 0, 1, 0], as implemented by mset2fun:
mset2fun = to_diffs . sort . (map must_be_nat)
to_diffs xs = zipWith (-) (xs) (0:xs)
must_be_nat n | n ≥ 0 = n

It can now be verified easily that incremental sums of the numbers in such a
sequence return the original set in sorted form, as implemented by fun2mset:
fun2mset ns = tail (scanl (+) 0 (map must_be_nat ns))

The resulting isomorphism mset can be applied directly using its two components
mset2fun and fun2mset. Equivalently, it can be expressed more “generically”
by using the as combinator, as follows:
∗ISO> mset2fun [1,3,3,3,4,4]
[1,2,0,0,1,0]
∗ISO> fun2mset [1,2,0,0,1,0]
[1,3,3,3,4,4]
∗ISO> as fun mset [1,3,3,3,4,4]
[1,2,0,0,1,0]
∗ISO> as mset fun [1,2,0,0,1,0]
[1,3,3,3,4,4]

3.2

An Isomorphism to Finite Sets of Natural Numbers

While finite sets and sequences share a common representation [N at], sets are
subject to the implicit constraints that all their elements are distinct and order
is immaterial. Like in the case of multisets, this suggest that a set like {7, 1, 4, 3}
could be represented by first ordering it as {1, 3, 4, 7} and then compute the
differences between consecutive elements. This gives [1, 2, 1, 3], with the first
element 1 followed by the increments [2, 1, 3]. To turn it into a bijection, including
0 as a possible member of a sequence, another adjustment is needed: elements in
the sequence of increments should be replaced by their predecessors. This gives
[1, 1, 0, 2] as implemented by set2fun:
set2fun xs | is_set xs = shift_tail pred (mset2fun xs)
1

Such constraints can be regarded as laws that we assume about a given data type,
when needed, restricting it to the appropriate domain of the underlying mathematical concept.

shift_tail _ [] = []
shift_tail f (x:xs) = x:(map f xs)
is_set ns = ns==nub ns

It can now be verified easily that predecessors of the incremental sums of the
successors of numbers in such a sequence, return the original set in sorted form,
as implemented by fun2set:
fun2set = (map pred) . fun2mset . (map succ)

The Encoder (an isomorphism with fun) can be specified with the two bijections
set2fun and fun2set.
set :: Encoder [Nat]
set = Iso set2fun fun2set

The Encoder (set) is now ready to interoperate with another Encoder:
∗ISO> as fun set [0,2,3,4,9]
[0,1,0,0,4]
∗ISO> as set fun [0,1,0,0,4]
[0,2,3,4,9]
∗ISO> as mset set [0,2,3,4,9]
[0,1,1,1,5]
∗ISO> as set mset [0,1,1,1,5]
[0,2,3,4,9]

As the example shows,the Encoder set connects arbitrary lists of natural numbers representing finite functions to strictly increasing sequences of (distinct)
natural numbers representing sets. Then, through the use of the combinator as,
sets represented by set are connected to multisets represented by mset. This
connection is (implicitly) routed through a connection to fun, as if
∗ISO> as mset fun [0,1,0,0,4]
[0,1,1,1,5]

were executed.
3.3

Folding Sets into Natural Numbers

We can fold a set, represented as a list of distinct natural numbers into a single natural number, reversibly, by observing that it can be seen as the list of
exponents of 2 in the number’s base 2 representation.
nat_set = Iso nat2set set2nat
nat2set n | n ≥ 0 = nat2exps n 0 where
nat2exps 0 _ = []
nat2exps n x =
if (even n) then xs else (x:xs) where
xs=nat2exps (n ‘div‘ 2) (succ x)
set2nat ns | is_set ns = sum (map (2^) ns)

We will standardize this pair of operations as an Encoder for a natural number
using our Root as a mediator:
nat :: Encoder Nat
nat = compose nat_set set

Given that nat is an isomorphism with the Root fun, one can use directly its
from and to components:
∗ISO> from nat 2008
[3,0,1,0,0,0,0]
∗ISO> to nat it
2008

Moreover, the resulting Encoder (nat) is now ready to interoperate with any
Encoder, in a generic way:
∗ISO> as fun nat 2008
[3,0,1,0,0,0,0]
∗ISO> as set nat 2008
[3,4,6,7,8,9,10]
∗ISO> as nat set [3,4,6,7,8,9,10]
2008
∗ISO> lend nat reverse 2008
1135
∗ISO> lend nat_set reverse 2008
2008
∗ISO> borrow nat_set succ [1,2,3]
[0,1,2,3]
∗ISO> as set nat 42
[1,3,5]
∗ISO> fit length nat 42
3
∗ISO> retrofit succ nat_set [1,3,5]
43

The reader might notice at this point that we have already made full circle
- as finite sets can be seen as instances of finite sequences. Injective functions
that are not surjections with wider and wider gaps can be generated using the
fact that one of the representations is information theoretically “denser” than
the other, for a given range:
∗ISO> as set fun [0,1,2,3]
[0,2,5,9]
∗ISO> as set fun $ as set fun [0,1,2,3]
[0,3,9,19]
∗ISO> as set fun $ as set fun $ as set fun [0,1,2,3]
[0,4,14,34]

One can now define, for instance, a mapping from natural numbers to multi-sets
simply as:
nat2mset = as mset nat
mset2nat = as nat mset

but we will not explicitly need such definitions as the the equivalent function is
clearly provided by the combinator as. One can now borrow operations between
set and nat as follows:
∗ISO> borrow_from
2042
∗ISO> 42 . | . 2008
2042
∗ISO> borrow_from
8
∗ISO> 42 .&. 2008
8
∗ISO> borrow_from
[5,7,9]
∗ISO> borrow_from
[1,2,6]

set union nat 42 2008
:: Nat
set intersect nat 42 2008
:: Nat
nat (∗) set [1,2,3] [4,5]
nat (+) set [1,2,3] [3,4,5]

and notice that operations like union and intersection of sets map to boolean
operations on numbers as expected, while other operations are not necessarily
meaningful at first sight. We will show next a few cases where such “shapshiftings” of operations reveal more interesting analogies.
3.4

Encoding Finite Multisets with Primes

A factorization of a natural number is uniquely described as multi-set or primes.
We will use the fact that each prime number is uniquely associated to its position
in the infinite stream of primes to obtain a bijection from multisets of natural
numbers to natural numbers. We assume defined a prime generator primes and
a factoring function to factors (see Appendix).
The function nat2pmset maps a natural number to the multiset of prime
positions in its factoring. Note that we treat 0 as [] and shift n to n+1 to
accomodate 0 and 1, to which prime factoring operations do not apply.
nat2pmset 0 = []
nat2pmset n = map (to_pos_in (h:ts)) (to_factors (n+1) h ts) where
(h:ts)=genericTake (n+1) primes
to_pos_in xs x = fromIntegral i where
Just i=elemIndex x xs

The function pmset2nat maps back a multiset of positions of primes to the
result of the product of the corresponding primes. Again, we map [] to 0 and
shift back by 1 the result.
pmset2nat [] = 0
pmset2nat ns = (product ks)-1 where
ks=map (from_pos_in ps) ns
ps=primes
from_pos_in xs n = xs !! (fromIntegral n)

We obtain the Encoder:
pmset :: Encoder [Nat]
pmset = compose (Iso pmset2nat nat2pmset) nat

working as follows:
∗ISO> as pmset nat 2008
[3,3,12]
∗ISO> as nat pmset it
2008
∗ISO> map (as pmset nat) [0..7]
[[],[0],[1],[0,0],[2],[0,1],[3],[0,0,0]]

Note that the mappings from a set or sequence to a number work in time and
space linear in the bitsize of the number. On the other hand, as prime number enumeration and factoring are involved in the mapping from numbers to
multisets this encoding is intractable for all but small values.
We are now ready to “shapeshift” between data types while watching for
interesting landscapes to show up.
3.5

Exploring the analogy between multiset decompositions and
factoring

As natural numbers can be uniquely represented as a multiset of prime factors
and, independently, they can also be represented as a multiset with the Encoder
mset described in subsection 3.1, the following question arises naturally:
Can in any way the “easy to reverse” encoding mset emulate or predict properties of the the difficult to reverse factoring operation?
The first step is to define an analog of the multiplication operation in terms of
the computationally easy multiset encoding mset. Clearly, it makes sense to take
inspiration from the fact that factoring of an ordinary product of two numbers
can be computed by concatenating the multisets of prime factors of its operands.
mprod = borrow_from mset (++) nat

Proposition 2 < N, mprod, 0 > is a commutative monoid i.e. mprod is defined
for all pairs of natural numbers and it is associative, commutative and has 0 as
an identity element.
After rewriting the definition of mprod as the equivalent:
mprod_alt n m = as nat mset ((as mset nat n) ++ (as mset nat m))

the proposition follows immediately from the associativity of the concatenation
operation and the order independence of the multiset encoding provided by mset.
We can derive an exponentiation operation as a repeated application of
mprod:
mexp n 0 = 0
mexp n k = mprod n (mexp n (k-1))

Here are a few examples comparing mprod to ordinary multiplication and
exponentiation:
∗ISO>
3539
∗ISO>
3539
∗ISO>
605
∗ISO>
605
∗ISO>
712
∗ISO>
5513

mprod 41 (mprod 33 88)
mprod (mprod 41 33)

88

mprod 33 46
mprod 46 33
mprod 0 712
mprod 5513 0

∗ISO> (41∗33)∗88
119064
∗ISO> 41∗(33∗88)
119064
∗ISO> 33∗46
1518
∗ISO> 46∗33
1518
∗ISO> 1∗712
712
∗ISO> 5513∗1
5513
∗ISO> map (λx→mexp x 2) [0..15]
[0,3,6,15,12,27,30,63,24,51,54,111,60,123,126,255]
∗ISO> map (λx→x^2) [0..15]
[0,1,4,9,16,25,36,49,64,81,100,121,144,169,196,225]

Note also that any multiset encoding of natural numbers can be used to define
a similar commutative monoid structure. In the case of pmset we obtain:
pmprod n m = as nat pmset ((as pmset nat n) ++ (as pmset nat m))

If one defines:
pmprod’ n m = (n+1)∗(m+1)-1

it follows immediately from the definition of mprod that:
pmprod ≡ pmprod0

(2)

This is useful as computing pmprod’ is easy while computing mprod is intractable
for large values. This brings us back to observe that:
Proposition 3 < N, pmprod, 0 > is a commutative monoid i.e. pmprod is defined for all pairs of natural numbers and it is associative, commutative and has
0 as an identity element.

Fig. 1 compares the shapes of pmprod’ (virtually the same as ordinary multiplication) and mprod for operands in [0..27 − 1]. One can see the contrast
between the regular shape of ordinary multiplication and the recursively “selfsimilar” landscape induced by mprod.
One can also bring mprod closer to ordinary multiplication by defining
mprod’ 0 _ = 0
mprod’ _ 0 = 0
mprod’ m n = (mprod (n-1) (m-1)) + 1
mexp’ n 0 = 1
mexp’ n k = mprod’ n (mexp’ n (k-1))

and by observing that they correlate as follows:
∗ISO> map (λx→mexp’ x 2) [0..16]
[0,1,4,7,16,13,28,31,64,25,52,55,112,61,124,127,256]
∗ISO> map (λx→x^2) [0..16]
[0,1,4,9,16,25,36,49,64,81,100,121,144,169,196,225,256]
[0,1,8,15,64,29,120,127,512,57,232,239,960,253,1016,1023,4096]
∗ISO> map (λx→x^3) [0..16]
[0,1,8,27,64,125,216,343,512,729,1000,1331,1728,2197,2744,3375,4096]

Fig. 2 shows that values for mexp’ follow from below those of the x2 function
and that equality only holds when x is a power of 2.
Note that the structure induced by mprod’ is similar to ordinary multiplication:
Proposition 4 < N, mprod0 , 1 > is a commutative monoid i.e. mprod’ is defined for all pairs of natural numbers and it is associative, commutative and has
1 as an identity element.
Interestingly, mprod’ coincides with ordinary multiplication if one of the operands
is a power of 2. More precisely, the following holds:
Proposition 5 mprod0 x y = x ∗ y if and only if ∃n ≥ 0 such that x = 2n or
y = 2n . Otherwise, mprod0 x y < x ∗ y.
Fig. 3 shows the (scaled up by 1000) self-similar landscape generated by the
[0..1]-valued function (mprod’ x y) / (x*y)
Besides the connection with products, natural mappings worth investigating
are the analogies between multiset intersection and gcd of the corresponding
numbers or between multiset union and the lcm of the corresponding numbers.
Assuming the definitions of multiset operations provided in the Appendix, one
can define:
mgcd :: Nat → Nat → Nat
mgcd = borrow_from mset msetInter nat
mlcm :: Nat → Nat → Nat
mlcm = borrow_from mset msetUnion nat

Fig. 1: multiplication vs mprod: pmprod’ and mprod

Fig. 2: Square vs. mexp’ n 2

Fig. 3: Ratio between mprod’ and product

mdiv :: Nat → Nat → Nat
mdiv = borrow_from mset msetDif nat

and note that properties similar to usual arithmetic operations hold:
mprod(mgcd x y)(mlcm x y) ≡ mprod x y

(3)

mdiv(mprod x y) y ≡ x

(4)

mdiv(mprod x y) x ≡ y

(5)

While mprod,mprod’,pmprod’ and pmprod are not distributive with ordinary
addition, it looks like an interesting problem to find for each of them compatible
additive operations.
3.6

Unfolding Natural Numbers into Bitstrings

The isomorphism between natural numbers and bitstring is well known, except
that it is usually ignored that conventional bit representations of integers need
a twist to be mapped one-to-one to arbitrary sequences of 0s and 1s. As the
usual binary representation always has 1 as its highest digit, nat2bits will drop
this bit, given that the length of the list of digits is (implicitly) known. This
transformation (a variant of the so called bijective base n representation), brings
us an isomorphism between N at and the regular language {0, 1}∗ .
bits :: Encoder [Nat]
bits = compose (Iso bits2nat nat2bits) nat
nat2bits = drop_last . (to_base 2) . succ
drop_last bs=
genericTake ((genericLength bs)-1) bs
to_base base n = d :
(if q==0 then [] else (to_base base q)) where
(q,d) = quotRem n base
bits2nat bs = pred (from_base 2 (bs ++ [1]))
from_base base [] = 0
from_base base (x:xs) | x ≥ 0 && x<base =
x+base∗(from_base base xs)

Note also that, strictly speaking, this is only an isomorphism when the digits
in the bitlist are in {0, 1}, therefore we shall assume this constraint as a law
governing this Encoder. The following examples show two conversion operations
and bits borrowing a multiplication operation from nat.

∗ISO> as bits nat 42
[1,1,0,1,0]
∗ISO> as nat bits [1,1,0,1,0]
42
∗ISO> borrow2 (with nat bits) (∗) [1,1,0] [1,0,1,1]
[1,0,0,1,1,0,0,0]

The reader might notice at this point that we have made full circle again as bitstrings can be seen as instances of finite sequences. Injective functions that
are not surjections with wider and wider gaps can be generated by composing
the as combinators:
∗ISO> as bits fun [1,1]
[1,1,0]
∗ISO> as bits fun (as bits fun [1,1])
[1,1,0,1]
∗ISO> as bits fun $ as bits fun $ as bits fun [1,1]
[1,1,0,1,1,0]

3.7

Encoding Signed Integers

To encode signed integers one can map positive numbers to even numbers and
strictly negative numbers to odd numbers. This gives the Encoder:
type Z = Integer
z:: Encoder Z
z = compose (Iso z2nat nat2z) nat
nat2z n = if even n then n ‘div‘ 2 else (-n-1) ‘div‘ 2
z2nat n = if n<0 then -2∗n-1 else 2∗n

working as follows:
∗ISO> as set z (-42)
[0,1,4,6]
∗ISO> as z set [0,1,4,6]
-42

3.8

Functional Binary Numbers

Church numerals are well known as a functional representation for Peano arithmetic. While benefiting from lazy evaluation, they implement a form of unary
arithmetic that uses O(n) space to represent n. This suggest devising a functional representation that mimics binary numbers. We will do this following the
model described in subsection 3.6 to provide an isomorphism between N at and
the functional equivalent of the regular language {0, 1}∗ . We will view each bit
as a N at → N at transformer:

b
o
i
e

x = pred x
x = 2∗x+0
x = 2∗x+1
=1

-----

begin
bit 0
bit 1
end

As the following example shows, composition of functions o and i closely parallels
the corresponding bitlists:
∗ISO> b$i$o$o$i$i$o$i$i$i$i$e
2008
∗ISO> as bits nat 2008
[1,0,0,1,1,0,1,1,1,1]

We can follow the same model with an abstract data type:
data D = E | O D | I D deriving (Eq,Ord,Show,Read)
data B = B D deriving (Eq,Ord,Show,Read)

from which we can generate functional bitstrings as an instance of a fold operation:
funbits2nat :: B → Nat
funbits2nat = bfold b o i e
bfold fb fo fi fe (B d) = fb (dfold d) where
dfold E = fe
dfold (O x) = fo (dfold x)
dfold (I x) = fi (dfold x)

Dually, we can reverse the effect of the functions b, o, i, e as:
b’
o’
i’
e’

x = succ x
x | even x = x ‘div‘ 2
x | odd x = (x-1) ‘div‘ 2
=1

and define a generator for our data type as an unfold operation:
nat2funbits :: Nat → B
nat2funbits = bunfold b’ o’ i’ e’
bunfold fb fo
dunfold n |
dunfold n |
dunfold n |

fi fe x = B (dunfold (fb x)) where
n==fe = E
even n = O (dunfold (fo n))
odd n = I (dunfold (fi n))

The two operations form an isomorphism:
∗ISO> funbits2nat (B $ I $ O $ O $ I $ I $ O $ I $ I $ I $ I $ E)
2008
∗ISO> nat2funbits it
B (I (O (O (I (I (O (I (I (I (I E))))))))))

We can define our Encoder as follows:

funbits :: Encoder B
funbits = compose (Iso funbits2nat nat2funbits) nat

Arithmetic operations can now be performed directly on this representation.
For instance, one can define a successor function as:
bsucc (B d) = B (dsucc d) where
dsucc E = O E
dsucc (O x) = I x
dsucc (I x) = O (dsucc x)

Equivalently arithmetics can be borrowed from N at:
∗ISO> bsucc (B $ I $ O $ O $ I $ I $ O $ I $ I $ I $ I $ E)
B (O (I (O (I (I (O (I (I (I (I E))))))))))
∗ISO> as nat funbits it
2009
∗ISO> borrow (with nat funbits)
succ (B $ I $ O $ O $ I $ I $ O $ I $ I $ I $ I $ E)
B (O (I (O (I (I (O (I (I (I (I E))))))))))
∗ISO> as nat funbits it
2009

While Haskell’s C-based arbitrary length integers are likely to be more efficient
for most operations, this representation, like Church numerals, has the benefit
of supporting partial or delayed computations through lazy evaluation.

4

Generic Unranking and Ranking Hylomorphisms

The ranking problem for a family of combinatorial objects is finding a unique
natural number associated to it, called its rank. The inverse unranking problem
consists of generating a unique combinatorial object associated to each natural
number.
4.1

Pure Hereditarily Finite Data Types

The unranking operation is seen here as an instance of a generic anamorphism
mechanism (an unfold operation), while the ranking operation is seen as an instance of the corresponding catamorphism (a fold operation) [9,10]. Together
they form a mixed transformation called hylomorphism. We will use such hylomorphisms to lift isomorphisms between lists and natural numbers to isomorphisms between a derived “self-similar” tree data type and natural numbers. In
particular we will derive Ackermann’s encoding from Hereditarily Finite Sets to
Natural Numbers.
The data type representing hereditarily finite structures will be a generic
multi-way tree with a single leaf type [].
data T = H [T] deriving (Eq,Ord,Read,Show)

The two sides of our hylomorphism are parameterized by two transformations f
and g forming an isomorphism Iso f g:
unrank f n = H (unranks f (f n))
unranks f ns = map (unrank f) ns
rank g (H ts) = g (ranks g ts)
ranks g ts = map (rank g) ts

Both combinators can be seen as a form of “structured recursion” that propagate
a simpler operation guided by the structure of the data type. For instance, the
size of a tree of type T is obtained as:
tsize = rank (λxs→1 + (sum xs))

Note also that unrank and rank work on T in cooperation with unranks and
ranks working on [T ].
We can now combine an anamorphism+catamorphism pair into an isomorphism hylo defined with rank and unrank on the corresponding hereditarily
finite data types:
hylo :: Iso b [b] → Iso T b
hylo (Iso f g) = Iso (rank g) (unrank f)
hylos :: Iso b [b] → Iso [T] [b]
hylos (Iso f g) = Iso (ranks g) (unranks f)

Hereditarily Finite Sets Hereditarily Finite Sets will be represented as an
Encoder for the tree type T:
hfs :: Encoder T
hfs = compose (hylo nat_set) nat

The hfs Encoder can now borrow operations from sets or natural numbers as
follows:
hfs_union = borrow2 (with set hfs) union
hfs_succ = borrow (with nat hfs) succ
hfs_pred = borrow (with nat hfs) pred
∗ISO> hfs_succ (H [])
H [H []]
∗ISO> hfs_union (H [H []] ) (H [])
H [H []]

Otherwise, hylomorphism induced isomorphisms work as usual with our embedded transformation language:
∗ISO> as hfs nat 42
H [H [H []],H [H [],H [H []]],H [H [],H [H [H []]]]]
∗ISO> as hfs nat 2008
H [H [H [],H [H []]],H [H [H [H []]]],H [H [H []],

H [H [H []]]],H [H [],H [H []],H [H [H []]]],
H [H [H [],H [H []]]],H [H [],H [H [],H [H []]]],
H [H [H []],H [H [],H [H []]]]]

One can notice that we have just derived as a “free algorithm” Ackermann’s
encoding [11,12] from Hereditarily Finite Sets to Natural Numbers:
P
f (x) = if x = {} then 0 else a∈x 2f (a)
together with its inverse:
ackermann = as nat hfs
inverse_ackermann = as hfs nat

One can represent the action of a hylomorphism unfolding a natural number into
a hereditarily finite set as a directed graph with outgoing edges induced by by
applying the inverse ackermann function as shown in Fig. 4.

2008

6

4

7

10

2

8

9

3

1

0

Fig. 4: 2008 as a HFS

Hereditarily Finite Functions The same tree data type can host a hylomorphism derived from finite functions instead of finite sets:
hff :: Encoder T
hff = compose (hylo nat) nat

The hff Encoder can be seen as another “free algorithm”, providing data compression/succinct representation for Hereditarily Finite Sets. Note, for instance,
the significantly smaller tree size in:

∗ISO> as hff nat 42
H [H [H []],H [H []],H [H []]]
ISO> as hff nat 2008
H [H [H [],H []],H [],H [H []],H [],H [],H [],H []]

As the cognoscenti might observe this is explained by the fact that hff provides higher information density than hfs, by incorporating order information
that matters in the case of a sequence and is ignored in the case of a set. One
can represent the action of a hylomorphism unfolding a natural number into a
hereditarily finite function as a directed ordered multi-graph as shown in Fig. 5.
Note that as the mapping as fun nat generates a sequence where the order of
the edges matters, this order is indicated integers starting from 0 labeling the
edges.

2008
2
6

5

4

3 1

0
1

0

3
1

0

0

Fig. 5: 2008 as a HFF

It is also interesting to connect sequences and HFF directly - in case one
wants to represent giant “sparse numbers” that correspond to sequences that
would overflow memory if represented as natural numbers but have a relatively
simple structure as formulae used to compute them. We obtain the Encoder:
hffs :: Encoder T
hffs = Iso hff2fun fun2hff
fun2hff ns = H (map (as hff nat) ns)
hff2fun (H hs) = map (as nat hff) hs

which can be used to generate HFFs associated to very large numbers:
∗ISO> as hffs fun [2^65,2^131]
H [H [H [H [],H [H [],H [H []]]]],H [H [H [],H [],H [H [],H [H []]]]]]

4.2

Hereditarily Finite Multisets

In a similar way, one can derive an Encoder for Hereditarily Finite Multisets
based on either the mset or the pmset isomorphisms:
nat_mset = Iso nat2mset mset2nat
hfm :: Encoder T
hfm = compose (hylo nat_mset) nat
nat_pmset = Iso nat2pmset pmset2nat
hfpm :: Encoder T
hfpm = compose (hylo nat_pmset) nat

working as follows:
∗ISO> as hfm nat 2008
H [H [H [],H []],H [H [],H []],H [H [H [H []]]],H [H [H [H []]]],
H [H [H [H []]]],H [H [H [H []]]],H [H [H [H []]]]]
∗ISO> as nat hfm it
2008
∗ISO> as hfpm nat 2008
H [H [H [],H []],H [H [],H []],H [H [H [],H [H []]]]]
∗ISO> as nat hfpm it
2008

After implementing this encoding some Google search revealed that it is essentially the same as [13] where it appears as an encoding of rooted trees.
4.3

A Hylomorphism with Atoms/Urelements

A similar construction can be carried out for the more practical case when Atoms
(Urelements in Set Theory parlance) are present. Hereditarily Finite Sets with
Urelements are represented as generic multi-way trees with a leaf type holding
urelements/atoms:
data UT a = A a | F [UT a] deriving (Eq,Ord,Read,Show)

Atoms will be mapped to natural numbers in [0..ulimit-1]. Assuming for
simplicity that ulimit is fixed, we denote this set A and denote U T the set of
trees of type U T with atoms in A.
Unranking As an adaptation of the unfold operation, natural numbers will be
mapped to elements of U T with a generic higher order function unrankU f,
defined from N at to U T , parameterized by the natural number ulimit and the
transformer function f:
ulimit = 4

unrankU = unrankUL ulimit
unranksU = unranksUL ulimit
unrankUL l _ n | n ≥ 0 && n<l = A n
unrankUL l f n = F (unranksUL l f (f (n-l)))
unranksUL l f ns = map (unrankUL l f) ns

Ranking Similarly, as an adaptation of fold, a generic inverse mapping rankU is
defined as:
rankU = rankUL ulimit
ranksU = ranksUL ulimit
rankUL l _ (A n) | n ≥ 0 && n<l = n
rankUL l g (F ts) = l+(g (ranksUL l g ts))
ranksUL l g ts = map (rankUL l g) ts

where rankU g maps trees to numbers and ranksU g maps lists of trees to lists
of numbers.
The following proposition describes conditions under which rankU and unrankU
can be used to lift isomorphisms between [N at] and N at to isomorphisms involving hereditarily finite structures:
Proposition 6 If the transformer function f : N at → [N at] is a bijection
with inverse g, such that n ≥ ulimit ∧ f (n) = [n0 , ...ni , ...nk ] ⇒ ni < n, then
(unrankU f ) : N at → U T is a bijection with inverse (rankU g) : U T →
N at and the recursive computations defining both functions terminate in a finite
number of steps.
Proof. Note that unrankU terminates as its arguments strictly decrease at each
step and rankU terminates as leaf nodes are eventually reached. That both are
bijections, follows by induction on the structure of N at and U T , given that map
preserves bijections and that adding/subtracting ulimit ensures that encodings
of atoms and sets never overlap.
The resulting hylomorphisms are defined as previously:
hyloU (Iso f g) = Iso (rankU g) (unrankU f)
hylosU (Iso f g) = Iso (ranksU g) (unranksU f)

An Encoder for Hereditarily Finite Sets with Urelements is defined as:
uhfs :: Encoder (UT Nat)
uhfs = compose (hyloU nat_set) nat

Note that this encoder provides a generalization of Ackermann’s mapping, to
Hereditarily Finite Sets with Urelements in [0..u − 1] defined as:
P
fu (x) = if x < u then x else u + a∈x 2fu (a)

A similar Encoder for Hereditarily Finite Functions with Urelements is defined as:
uhff :: Encoder (UT Nat)
uhff = compose (hyloU nat) nat

4.4

Extending the encoding for the case of an infinite set of
Atoms/Urelements

An adaptation of the previous construction for the case when an infinite supply
of atoms/urelements is needed (i.e. when their number is not known in advance)
follows.
Unranking As an adaptation of the unfold operation, natural numbers will be
mapped to elements of U T with a generic higher order function unrankIU f,
defined from N at to U T , parameterized by the transformer function f:
unrankIU _ n | even n = A (n ‘div‘ 2)
unrankIU f n = F (unranksIU f (f ((n-1) ‘div‘ 2)))
unranksIU f ns = map (unrankIU f) ns

Note that (an infinite supply of) even numbers provides codes for atoms, while
odd numbers are used to encode the non-leaf structure of the trees in UT.
Ranking Similarly, as an adaptation of fold, a generic inverse mapping rankIU
g is defined as:
rankIU _ (A n) = 2∗n
rankIU g (F ts) = 1+2∗(g (ranksIU g ts))
ranksIU g ts = map (rankIU g) ts

where rankIU g maps trees to numbers and ranksIU g maps lists of trees to
lists of numbers.
The resulting hylomorphisms are defined as previously:
hyloIU (Iso f g) = Iso (rankIU g) (unrankIU f)
hylosIU (Iso f g) = Iso (ranksIU g) (unranksIU f)

An Encoder for Hereditarily Finite Sets with an infinite supply of Urelements is
defined as:
iuhfs :: Encoder (UT Nat)
iuhfs = compose (hyloIU nat_set) nat

A similar Encoder for Hereditarily Finite Functions with and infinite supply
of Urelements is defined as:
iuhff :: Encoder (UT Nat)
iuhff = compose (hyloIU nat) nat

5

Permutations and Hereditarily Finite Permutations

We have seen that finite sets and their derivatives represent information in an
order independent way, focusing exclusively on information content. We will
now look at data representations that focus exclusively on order in a content
independent way - finite permutations and their hereditarily finite derivatives.
To obtain an encoding for finite permutations we will first review a ranking/unranking mechanism for permutations that involves an unconventional numeric representation, factoradics.
5.1

The Factoradic Numeral System

The factoradic numeral system [14] replaces digits multiplied by a power of a
base n with digits that multiply successive values of the factorial of n. In the
increasing order variant fr the first digit d0 is 0, the second is d1 ∈ {0, 1} and
the n-th is dn ∈ [0..n]. For instance, 42 = 0 ∗ 0! + 0 ∗ 1! + 0 ∗ 2! + 3 ∗ 3! + 1 ∗ 4!.
The left-to-right, decreasing order variant fl is obtained by reversing the digits
of fr.
fr 42
[0,0,0,3,1]
rf [0,0,0,3,1]
42
fl 42
[1,3,0,0,0]
lf [1,3,0,0,0]
42

The function fr generating the factoradics of n, right to left, handles the special
case of 0 and calls a local function f which recurses and divides with increasing
values of n while collecting digits with mod:
fr 0 =
fr n =
f _
f j

[0]
f 1 n where
0 = []
k = (k ‘mod‘ j) :
(f (j+1) (k ‘div‘ j))

The function fl, with digits left to right is obtained as follows:
fl = reverse . fr

The function lf (inverse of fl) converts back to decimals by summing up results
while computing the factorial progressively:
rf ns = sum (zipWith (∗) ns factorials) where
factorials=scanl (∗) 1 [1..]

Finally, lf, the inverse of fl is obtained as:
lf = rf . reverse

5.2

Ranking and unranking permutations of given size with Lehmer
codes and factoradics

The Lehmer code of a permutation f of size n is defined as the sequence l(f ) =
(l1 (f ) . . . li (f ) . . . ln (f )) where li (f ) is the number of elements of the set {j >
i|f (j) < f (i)} [15].
Proposition 7 The Lehmer code of a permutation determines the permutation
uniquely.
The function perm2nth computes a rank for a permutation ps of size>0. It starts
by first computing its Lehmer code ls with perm2lehmer. Then it associates a
unique natural number n to ls, by converting it with the function lf from
factoradics to decimals. Note that the Lehmer code Ls is used as the list of
digits in the factoradic representation.
perm2nth ps = (l,lf ls) where
ls=perm2lehmer ps
l=genericLength ls
perm2lehmer [] = []
perm2lehmer (i:is) = l:(perm2lehmer is) where
l=genericLength [j | j←is,j<i]

The function nat2perm provides the matching unranking operation associating a permutation ps to a given size>0 and a natural number n. It generates
the n-th permutation of a given size.
nth2perm (size,n) =
apply_lehmer2perm (zs++xs) [0..size-1] where
xs=fl n
l=genericLength xs
k=size-l
zs=genericReplicate k 0

The following function extracts a permutation from a “digit” list in factoradic
representation.
apply_lehmer2perm [] [] = []
apply_lehmer2perm (n:ns) ps@(x:xs) =
y : (apply_lehmer2perm ns ys) where
(y,ys) = pick n ps
pick i xs = (x,ys++zs) where
(ys,(x:zs)) = genericSplitAt i xs

Note also that apply lehmer2perm is used this time to reconstruct the permutation ps from its Lehmer code, which in turn is computed from the permutation’s
factoradic representation.
One can try out this bijective mapping as follows:

nth2perm (5,42)
[1,4,0,2,3]
perm2nth [1,4,0,2,3]
(5,42)
nth2perm (8,2008)
[0,3,6,5,4,7,1,2]
perm2nth [0,3,6,5,4,7,1,2]
(8,2008)

5.3

A bijective mapping from permutations to natural numbers

Like in the case of BDDs, one more step is needed to to extend the mapping
between permutations of a given length to a bijective mapping from/to N at:
we will have to “shift towards infinity” the starting point of each new bloc of
permutations in N at as permutations of larger and larger sizes are enumerated.
First, we need to know by how much - so we compute the sum of all factorials
up to n!.
sf n = rf (genericReplicate n 1)

This is done by noticing that the factoradic representation of [0,1,1,..] does just
that.
What we are really interested into, is decomposing n into the distance to the
last sum of factorials smaller than n, n m and the its index in the sum, k.
to_sf n = (k,n-m) where
k=pred (head [x | x←[0..],sf x>n])
m=sf k

Unranking of an arbitrary permutation is now easy - the index k determines the
size of the permutation and n-m determines the rank. Together they select the
right permutation with nth2perm.
nat2perm 0 = []
nat2perm n = nth2perm (to_sf n)

Ranking of a permutation is even easier: we first compute its size and its rank,
then we shift the rank by the sum of all factorials up to its size, enumerating
the ranks previously assigned.
perm2nat ps = (sf l)+k where
(l,k) = perm2nth ps

It works as follows:
nat2perm 2008
[0,2,3,1,4]
perm2nat [0,2,3,1,4]
42
nat2perm 2008
[1,4,3,2,0,5,6]
perm2nat [1,4,3,2,0,5,6]
2008

We can now define the Encoder as:
perm :: Encoder [Nat]
perm = compose (Iso perm2nat nat2perm) nat

The Encoder works as follows:
∗ISO> as perm nat 2008
[1,4,3,2,0,5,6]
∗ISO> as nat perm it
2008
∗ISO> as perm nat 1234567890
[1,6,11,2,0,3,10,7,8,5,9,4,12]
∗ISO> as nat perm it
1234567890

5.4

Hereditarily Finite Permutations

By using the generic unrank and rank functions defined in section 4 we can
extend the isomorphism defined by nat2perm and perm2nat to encodings of
Hereditarily Finite Permutations (HF P ).
nat2hfp = unrank nat2perm
hfp2nat = rank perm2nat

The encoding works as follows:
∗ISO> nat2hfp 42
H [H [],H [H [],H [H []]],H [H [H []],H []],
H [H []],H [H [],H [H []],H [H [],H [H []]]]]
∗ISO> hfp2nat it
42

We can now define the Encoder as:
hfp :: Encoder T
hfp = compose (Iso hfp2nat nat2hfp) nat

The Encoder works as follows:
∗ISO> as hfp nat 42
H [H [],H [H [],H [H []]],H [H [H []],H []],
H [H []],H [H [],H [H []],H [H [],H [H []]]]]
∗ISO> as nat hfp it
42
∗JFISO> as hfp nat 2008
H [H [H []],H [H [],H [H []],H [H [],H [H []]]],H [H [H []],H []],
H [H [],H [H []]],H [],H [H [],H [H [],H [H []]],H [H []]],
H [H [H []],H [],H [H [],H [H []]]]]
∗ISO> as nat hfp it
2008

2008
5
5

6

4
1
2

0

1

0

3

2

6

2

2

2

0

1
1

0
1

0

3

4

0
1

1

0
0

Fig. 6: 2008 as a HFP

As shown in Fig 6 an ordered digraph (with labels starting from 0 representing
the order of outgoing edges) can be used to represent the unfolding of a natural
number to the associated hereditarily finite permutation. An interesting property of graphs associated to hereditarily finite permutations is that moving from
a number n to its successor typically only induces a reordering of the labeled
edges, as shown in Fig. 7.

6

Hereditary base-k represenations and Goodstein
sequences

Definition 1 Hereditary base-k representation of a number x is obtained by representing x as a sum of powers of k followed by expression of each of the exponents
with nonzero coeficients as a sum of powers of k, recursively.
First we express a single step of this transformation to/from a polynomial in
base k as a pair of bijections:
nat2kpoly k n = filter (λp→0/=fst p) ps where
ns=to_base k n
l=genericLength ns
is=[0..l-1]
ps=zip ns is

2009
6
5

5

4
1
2

0

1
3

2

6

2

2

2

0

1

0

1

0
1

0

3

4

0
1

1

0
0

Fig. 7: 2009 as a HFP

kpoly2nat k ps = sum (map (λ(d,e)→d∗k^e) ps)

The transformation works as follows:
∗ISO> nat2kpoly 3 2009
[(2,0),(1,2),(2,3),(2,5),(2,6)]
∗ISO> kpoly2nat 3 it
2009

The recursive process generates a tree, with coeficients of each expansion labeling
nodes. We can host this expansion in the data type HB:
data HB a = HB a [HB a]

deriving (Eq,Ord,Show,Read)

We will define, for each base k, two isomorphisms nat2hb k and hb2nat k between natural numbers and polynomials:
nat2hb :: Nat→Nat→[HB Nat]
nat2hb _k 0 = []
nat2hb k n | n<k = [HB n []]
nat2hb k n = gs where
ps’=nat2kpoly k n
gs=map (nat2hb1 k) ps’
nat2hb1 k (d,e) = HB d (nat2hb k e)

hb2nat :: Nat → [HB Nat] → Nat
hb2nat k [] = 0
hb2nat k ts = kpoly2nat k ps where
ps=map (hb2nat1 k) ts
hb2nat1 k (HB d ts) = (d,hb2nat k ts)

We can now define a family of Encoders, one for each base k, as follows:
hb :: Nat→Encoder [HB Nat]
hb k = compose (Iso (hb2nat k) (nat2hb k)) nat

The new concept here is working with a parametric family of Encoders. With a
small adaptation, the syntax of the as combinator scales up naturally:
∗ISO> as (hb 3) nat 42
[HB 2 [HB 1 []],HB 1 [HB 2 []],HB 1 [HB 1 [HB 1 []]]]
∗ISO> as nat (hb 3) it
42

Note that the base does not occur as such in the hereditary base-k expression
obtained with the Encoder hb. This property can be used to obtain Goodstein
sequences by bumping the base from k to k+1 i.e. interpreting a (hb k) expression as a (hb (k+1)) expression and then subtracting 1 from the result,
i.e:
goodsteinStep k n = (hb2nat (k+1) (nat2hb k n)) - 1
goodsteinSeq _ 0 = []
goodsteinSeq k n = n:(goodsteinSeq (k+1) m) where
m=goodsteinStep k n
goodstein m = goodsteinSeq 2 m
∗ISO> goodstein 3
[3,3,3,2,1]
∗ISO> take 12 (goodstein 4)
[4,26,41,60,83,109,139,173,211,253,299,348]

Goodstein’s Theorem (provable in second order arithmetics) states that this
sequence always terminates at 0. The remarkable thing about it is that it is
an undecidable statement in first order Peano arithmetics, that in contrast to
Gödel’s therorem, involves only “conventional” numerical relations.

7

Pairing/Unpairing

A pairing function is an isomorphism f : N at × N at → N at. Its inverse is called
unpairing.

7.1

The Pepis-Kalmar-Robinson Pairing Function

An classic pairing function is pepis J, together with its left and right unpairing
companions pepis K and pepis L that have been used, by Pepis, Kalmar and
Robinson together with Cantor’s functions, in some fundamental work on recursion theory, decidability and Hilbert’s Tenth Problem in [16,17,18,19,20,21,22,23,24].
The function pepis J combines two numbers reversibly by multiplying a power
of 2 derived from the first and an odd number derived from the second:
f (x, y) = 2x ∗ (2 ∗ y + 1) − 1

(6)

Its Haskell implementation, together with its inverse is:
pepis_J x y = pred ((2^x)∗(succ (2∗y)))
pepis_K n = two_s (succ n)
pepis_L n = (pred (no_two_s (succ n))) ‘div‘ 2
two_s n | even n = succ (two_s (n ‘div‘ 2))
two_s _ = 0
no_two_s n = n ‘div‘ (2^(two_s n))

This pairing function (slower in the second argument) works as follows:
pepis_J 1 10
41
pepis_J 10 1
3071
[pepis_J i j | i←[0..3],j←[0..3]]
[0,2,4,6,1,5,9,13,3,11,19,27,7,23,39,55]

As Haskell provides a built-in ordered pair, it is convenient to regroup the functions J, K, L (given in Julia Robinson’s original notation) as mappings to/from
built-in ordered pairs:
pepis_pair (x,y) = pepis_J x y
pepis_unpair n = (pepis_K n,pepis_L n)

Observing that the number of 0s in front of the representation of a natural
number n as a sequence equals pepis K n, an alternative implementation could
be:
pepis_pair’ (x,y) = (fun2nat (x:(nat2fun y)))-1
pepis_unpair’ n = (x,fun2nat ns) where
(x:ns)=nat2fun (n+1)
fun2nat = set2nat . fun2set
nat2fun = set2fun . nat2set

Note also that pepis unpair is “asymmetrical” in the sense that its first component grows much slower than the second, when applied to [0..]. Sometimes
it is more useful to have the opposite behavior
rpepis_pair (x,y) = pepis_pair (y,x)
rpepis_unpair n = (y,x) where (x,y)=pepis_unpair n

After defining
type Nat2 = (Nat,Nat)

we obtain the encoder
pnat2 :: Encoder Nat2
pnat2 = compose (Iso pepis_pair pepis_unpair) nat
rpnat2 :: Encoder Nat2
rpnat2 = compose (Iso rpepis_pair rpepis_unpair) nat

7.2

A Bitwise Pairing/Unpairing Function

We will now introduce an unusually simple pairing function (also mentioned in
[25], p.142).
The function bitpair works by splitting a number’s big endian bitstring
representation into odd and even bits, while its inverse bitunpair blends the
odd and even bits back together.
bitpair :: Nat2 → Nat
bitpair (i,j) =
set2nat ((evens i) ++ (odds j)) where
evens x = map (2∗) (nat2set x)
odds y = map succ (evens y)
bitunpair :: Nat→Nat2
bitunpair n = (f xs,f ys) where
(xs,ys) = partition even (nat2set n)
f = set2nat . (map (‘div‘ 2))

The transformation of the bitlists is shown in the following example with
bitstrings aligned:
∗ISO> bitunpair 2008
(60,26)
-- 2008:[0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 1]
-60:[0,
0,
1,
1,
1,
1]
-26:[
0,
1,
0,
1,
1
]

We can derive the following Encoder:
nat2 :: Encoder Nat2
nat2 = compose (Iso bitpair bitunpair) nat

working as follows:
∗ISO> as nat2 nat 2008
(60,26)
∗ISO> as nat nat2 (60,26)
2008

In a way similar to hereditarily finite trees generated by unfoldings one
can apply strictly decreasing2 unpairing functions recursively. Figures 8 and
9 show the directed graphs describing recursive application of bitunpair and
pepis unpair.

2008
1
1004
1
502
1

0

251
0

0

1

2

0

31
0 0
1

5

1
0

10
1

Fig. 8: Graph obtained by recursive application of pepis unpair for 2008

Given that unpairing functions are bijections from N at to N at × N at they
will progressively cover all points having natural number coordinates in their
range in the plane. Figures 10, 11 show the curves generated by bitunpair and
pepis unpair.
Fig. 12 shows the action of the pairing function bitpair on its two arguments
arguments in [0..63].
2

except for 0 and 1, typically

2008
1
26

60

0
4

0 1
1

0
1

0

0

6
0

2

3

0

1 01

1

1

Fig. 9: Graph obtained by recursive application of bitunpair for 2008

Fig. 10: 2D curve connecting values of bitunpair n for n ∈ [0..210 − 1]

Fig. 11: 2D curve connecting values of pepis unpair n for n ∈ [0..210 − 1]

Fig. 12: Values of bitpair x y with x,y in [0..63]

7.3

Encoding Unordered Pairs

To derive an encoding of unordered pairs, i.e. 2 element sets, one can combine
pairing/unpairing with conversion between sequences and sets:
pair2unord_pair (x,y) = fun2set [x,y]
unord_pair2pair [a,b] = (x,y) where
[x,y]=set2fun [a,b]
unord_unpair = pair2unord_pair . bitunpair
unord_pair = bitpair . unord_pair2pair

We can derive the following equivalent Encoders:
set2 :: Encoder [Nat]
set2 = compose (Iso unord_pair2pair pair2unord_pair) nat2

that goes through nat2, working as follows:
∗ISO> as set2 nat 2008
[60,87]
∗ISO> as nat set2 it
2008

and
set2’ :: Encoder [Nat]
set2’ = compose (Iso unord_pair unord_unpair) nat

that goes through nat, working as follows:
∗ISO> as set2’ nat 2008
[60,87]
∗ISO> as nat set2’ [60,87]
2008
∗ISO> as nat set2’ [87,60]
2008

7.4

Encodings Multiset Pairs

To derive an encoding of 2 element multisets, one can combine pairing/unpairing
with conversion between sequences and multisets:
pair2mset_pair (x,y) = (a,b) where [a,b]=fun2mset [x,y]
mset_unpair2pair (a,b) = (x,y) where [x,y]=mset2fun [a,b]
mset_unpair = pair2mset_pair . bitunpair
mset_pair = bitpair . mset_unpair2pair

We can derive the following Encoder:
mset2 :: Encoder Nat2
mset2 = compose (Iso mset_unpair2pair pair2mset_pair) nat2

working as follows:

∗ISO> as mset2 nat 2008
(60,86)
∗ISO> as nat mset2 it
2008

Figure 13 shows the curve generated by mset unpair covering the lattice of
points in its range.

Fig. 13: 2D curve connecting values of mset unpair n for n ∈ [0..210 − 1]

7.5

Extending Pairing/Unpairing to Signed Integers

Given the bijection from nat to z one can easily extend pairing/unpairing operations to signed integers. We obtain the Encoder:
type Z2 = (Z,Z)
z2 :: Encoder Z2
z2 = compose (Iso zpair zunpair) nat
zpair (x,y) = (nat2z . bitpair) (z2nat x,z2nat y)
zunpair z = (nat2z n,nat2z m) where (n,m)= (bitunpair . z2nat) z

working as follows:

∗ISO> map zunpair [-5..5]
[(-1,1),(-2,-1),(-2,0),(-1,-1),(-1,0),(0,0),(0,-1),(1,0),(1,-1),(0,1),(0,-2)]
∗ISO> map zpair it
[-5,-4,-3,-2,-1,0,1,2,3,4,5]
∗ISO> as z2 z (-2008)
(63,-26)
∗ISO> as z z2 it
-2008

Figure 14 shows the curve covering the lattice of integer coordinates generated
by the function zunpair.

Fig. 14: Curve generated by unpairing function on signed integers

The same construction can be extended to multiset pairing functions:
mz2 :: Encoder Z2
mz2 = compose (Iso mzpair mzunpair) nat
mzpair (x,y) = (nat2z . mset_pair) (z2nat x,z2nat y)
mzunpair z = (nat2z n,nat2z m) where (n,m)= (mset_unpair . z2nat) z

working as follows:
∗ISO> as mz2 z (-42)

(1,-8)
∗ISO> as z mz2 it
-42

7.6

Gauss Integers and Pairing Functions

Visualizing complex variable functions requires 4 dimensions even for 1-variable
functions. This is usually handled by associating a color/hue value to the phase
while representing the modulus along the z-axis. However, for 2-argument complex functions as simple as the sum, difference and the product 6 dimensions
would be needed. Let us start shapeshifting operations on Gauss Integers (pairs
of integers with a real and imaginary part) in combination with a mapping to
ordinary integers using the (commutative!) multiset pairing/unpairing isomorphism provided by the Encoder mz2:
gauss_sum (ab,cd) = mzpair (a+b,c+d) where
(a,b)=mzunpair ab
(c,d)=mzunpair cd
gauss_dif (ab,cd) = mzpair (a-b,c-d) where
(a,b)=mzunpair ab
(c,d)=mzunpair cd
gauss_prod (ab,cd) = mzpair (a∗c-b∗d,b∗c+a∗d) where
(a,b)=mzunpair ab
(c,d)=mzunpair cd

Clearly one can now fit these operations in 3-dimensions as shown in Figures 15,
16, 17 visualizing sums, differences and products of Gauss Integers obtained by
unpairing integers in [−24 ..24 − 1].
7.7

Some algebraic properties of pairing functions

The following propositions state some simple algebraic identities between pairing
operations acting on ordered, unordered and multiset pairs.
Proposition 8 Given the function definitions:
bitlift x = bitpair (x,0)
bitlift’ = (from_base 4) . (to_base 2)
bitclip = fst . bitunpair
bitclip’ = (from_base 2) . (map (‘div‘ 2)) . (to_base 4) . (∗2)
bitpair’ (x,y) = (bitpair (x,0)) + (bitpair(0,y))
xbitpair (x,y) = (bitpair (x,0)) ‘xor‘ (bitpair (0,y))
obitpair (x,y) = (bitpair (x,0)) . | . (bitpair (0,y))
pair_product (x,y) = a+b where

Fig. 15: Sums of Gauss Integers visualized with Pairing functions

Fig. 16: Differences of Gauss Integers visualized with Pairing functions

Fig. 17: Products of Gauss Integers visualized with Pairing functions

x’=bitpair (x,0)
y’=bitpair (0,y)
ab=x’∗y’
(a,b)=bitunpair ab

the following identities hold:
bitlif t ≡ bitlif t0

(7)

bitclip ≡ bitclip0

(8)

bitclip ◦ bitlif t ≡ id

(9)

bitpair(0, n) ≡ 2 ∗ bitpair(n, 0)

(10)

bitpair(0, n) ≡ 2 ∗ (bitlif t n)

(11)

bitpair(n, n) ≡ 3 ∗ (bitlif t n)

(12)

bitpair(2n , 0) ≡ (2n )2

(13)

n

n+1

bitpair(22 + 1, 0) ≡ 22

+1

0

(14)

bitpair ≡ bitpair ≡ xbitpair ≡ obitpair

(15)

bitpair(x, y) ≡ (bitlif t x) + 2 ∗ (bitlif t y)

(16)

pair product ≡ ∗

(17)

Proposition 9 Given the function definitions
bitpair’’ (x,y) = mset_pair (min x y,x+y)
bitpair’’’ (x,y) = unord_pair [min x y,x+y+1]
mset_pair’ (a,b) = bitpair (min a b, (max a b) - (min a b))
mset_pair’’ (a,b) = unord_pair [min a b, (max a b)+1]
unord_pair’ [a,b] = bitpair (min a b, (max a b) - (min a b) -1)
unord_pair’’ [a,b] = mset_pair (min a b, (max a b)-1)

the following identities hold:

8

bitpair ≡ bitpair00 ≡ bitpair000

(18)

mset pair ≡ mset pair0 ≡ mset pair00

(19)

unord pair ≡ unord pair0 ≡ unord pair00

(20)

Cons-Lists with Pairing/Unpairing

The simplest application of pairing/unpairing operations is encoding of cons-lists
of natural numbers, defined as the data type:
data CList = Atom Nat | Cons CList CList
deriving (Eq,Ord,Show,Read)

First, to provide an infinite supply of atoms, we encode them as even numbers:
to_atom n = 2∗n
from_atom a | is_atom a = a ‘div‘ 2
is_atom n = even n && n ≥ 0

Next, as we want atoms and cons cell disjoint, we will encode the later as odd
numbers:
is_cons n = odd n && n>0
decons z | is_cons z = pepis_unpair ((z-1) ‘div‘ 2)
cons x y = 2∗(pepis_pair (x,y))+1

We can deconstruct a natural number by recursing over applications of the
unpairing-based decons combinator:
nat2cons n | is_atom
nat2cons n | is_cons
Cons (nat2cons hd)
(nat2cons tl)
(hd,tl) = decons

n = Atom (from_atom n)
n=
where
n

We can reverse this process by recursing with the cons combinator on the CList
data type:
cons2nat (Atom a) = to_atom a
cons2nat (Cons h t) = cons (cons2nat h) (cons2nat t)

The following example shows both transformations as inverses.
∗ISO> cons2nat (Cons (Atom 0) (Cons (Atom 1) (Cons (Atom 2) (Atom 3))))
26589
∗ISO> nat2cons 26589
Cons (Atom 0) (Cons (Atom 1) (Cons (Atom 2) (Atom 3)))

We obtain the Encoder:
clist :: Encoder CList
clist = compose (Iso cons2nat nat2cons) nat

The Encoder works as follows:
∗ISO> as clist nat 101
Cons (Atom 0) (Cons (Atom 0) (Atom 3))

and can be used to generate random LISP-like data and code skeletons from
natural numbers.

9

Revisiting Multiset Encodings

We will now use pairing/unpairing functions, in combination with mappings to
sequences and sets to design an efficient encoding of multisets.
The function fmset2nat starts by grouping the elements of a multiset. The
lengths of the groups (decremented by 1), as well as an element of each are then
collected in 2 lists. Then the second list is morphed from a set to a sequence, as
this provides a more compact representation without changing the length of the
list. The first list, seen as a sequence is then paired element by element with the
second list. Finally, the resulting numbers, seen as a sequence, are then fused
together.
fmset2nat pairingf ms = m where
mss= group (sort ms)
xs=map (pred . genericLength) mss
zs=map head mss
ys=set2fun zs
ps=zip xs ys
ns=map pairingf ps
m=fun2nat ns

The function fnat2mset reverses the process step by step:
fnat2mset unpairingf m = rs where
ns=nat2fun m
ps=map unpairingf ns
(xs,ys)=unzip ps

xs’=map succ xs
zs=fun2set ys
f k x = genericTake k (repeat x)
rs = concat (zipWith f xs’ zs)

After instantiating these generic functions to interesting pairing/unpairing functions
bmset2nat = fmset2nat bitpair
nat2bmset = fnat2mset bitunpair
bmset2nat’ = fmset2nat pepis_pair
nat2bmset’ = fnat2mset pepis_unpair

We obtain the Encoders:
bmset :: Encoder [Nat]
bmset = compose (Iso bmset2nat nat2bmset) nat
bmset’ :: Encoder [Nat]
bmset’ = compose (Iso bmset2nat’ nat2bmset’) nat

working as follows:
ISO> as bmset nat 2008
[1,1,2,3,3,4,5,6,7]
∗ISO> as nat bmset it
2008
∗ISO> map (as bmset nat) [0..7]
[[],[0],[0,0],[0,1],[1],[0,1,1],[0,0,1],[0,1,2]]
∗ISO> as bmset’ nat 2008
[0,0,0,1,2,2,3,4,5,6]

Note that, in contrast to the intractable prime number based multiset encoding
pmset, this time we obtain an encoding, linear in the bitsize of the natural
numbers involved, as in the case of mset. Note also that the construction is
generic in the sense that it works with any pairing / unpairing function. Like in
the case of mset and pmset multiset encodings we can extend these encodings
to a hylomorphism hfbm:
nat_bmset = Iso nat2bmset bmset2nat
hfbm :: Encoder T
hfbm = compose (hylo nat_bmset) nat
nat_bmset’ = Iso nat2bmset’ bmset2nat’
hfbm’ :: Encoder T
hfbm’ = compose (hylo nat_bmset’) nat

working as follows:
∗ISO> as hfbm nat 42
H [H [],H [],H [H []],H [H []],H [H [],H []],H [H [],H []]]

∗ISO> as nat hfbm it
42
∗ISO> as hfbm’ nat 2008
H [H [],H [],H [],H [H []],H [H [],H []],
H [H [],H []],H [H [],H [H []]],H [H [H []]],
H [H [],H [H []],H [H []]],H [H [],H [],H [H []]]]
∗ISO> as nat hfbm’ it
2008

10

Pairing Functions and Encodings of Binary Decision
Diagrams

As a variation on the theme of pairing/unpairing functions, we will show in this
section that a Binary Decision Diagram (BDD) representing the same logic function as an n-variable 2n bit truth table can be obtained by applying bitunpair
recursively to tt. More precisely, we will show that applying this unfolding operation results in a complete binary tree of depth n representing a BDD that
returns tt when evaluated applying its boolean operations.
The binary tree type BT has the constants B0 and B1 as leaves representing
the boolean values 0 and 1. Internal nodes (that will represent if-then-else
decision points), will be marked with the constructor D. We will also add integers
to represent logic variables, ordered identically in each branch, as first arguments
of D. The two other arguments will be subtrees that represent THEN and ELSE
branches:
data BT a = B0 | B1 | D a (BT a) (BT a)
deriving (Eq,Ord,Read,Show)

The constructor BDD wraps together a tree of type BT and the number of logic
variables occurring in it.
data BDD a = BDD a (BT a) deriving (Eq,Ord,Read,Show)

10.1

Unfolding natural numbers to binary trees

The following functions apply bitunpair recursively, on a Natural Number tt,
seen as an n-variable 2n bit truth table, to build a complete binary tree of depth
n, that we will represent using the BDD data type.
unfold_bdd :: Nat2 → BDD Nat
unfold_bdd (n,tt) = BDD n bt where
bt=if tt<max then split_with bitunpair n tt
else error
("unfold_bdd: last arg "++ (show tt)++
" should be < " ++ (show max))
where max = 2^2^n

split_with _ n 0 | n<1 = B0
split_with _ n 1 | n<1 = B1
split_with f n tt = D k (split_with f k tt1)
(split_with f k tt2) where
k=pred n
(tt1,tt2)=f tt
n

The following examples show results returned by unfold bdd for the 22 truth
tables associated to n variables, for n = 2:
BDD
BDD
BDD
...
BDD

2 (D 1 (D 0 B0 B0) (D 0 B0 B0))
2 (D 1 (D 0 B1 B0) (D 0 B0 B0))
2 (D 1 (D 0 B0 B0) (D 0 B1 B0))
2 (D 1 (D 0 B1 B1) (D 0 B1 B1))

Note that no boolean operations have been performed so far and that we still
have to prove that such trees actually represent BDDs associated to truth tables.
10.2

Folding binary trees to natural numbers

One can “evaluate back” the binary tree of data type BDD, by using the pairing
function bitpair. The inverse of unfold bdd is implemented as follows:
fold_bdd :: BDD Nat → Nat2
fold_bdd (BDD n bt) =
(n,fuse_with bitpair bt) where
fuse_with rf B0 = 0
fuse_with rf B1 = 1
fuse_with rf (D _ l r) =
rf (fuse_with rf l,fuse_with rf r)

Note that this is a purely structural operation and that integers in first argument
position of the constructor D are actually ignored.
The two bijections work as follows:
∗ISO>unfold_bdd
BDD 3
(D 2
(D 1 (D 0
(D 0
(D 1 (D 0
(D 0

(3,42)

B0
B0
B1
B1

B0)
B0))
B1)
B0)))

∗ISO>fold_bdd it
42

10.3

Boolean Evaluation of BDDs

Practical uses of BDDs involve reducing them by sharing nodes and eliminating
identical branches [26]. Note that in this case bdd2nat might give a different

result as it computes different pairing operations. Fortunately, we can try to
fold the binary tree back to a natural number by evaluating it as a boolean
function.
The function eval bdd describes the BDD evaluator:
eval_bdd (BDD n bt) = eval_with_mask (bigone n) n bt
eval_with_mask m _ B0 = 0
eval_with_mask m _ B1 = m
eval_with_mask m n (D x l r) =
ite_ (var_mn m n x)
(eval_with_mask m n l)
(eval_with_mask m n r)
var_mn mask n k = mask ‘div‘ (2^(2^(n-k-1))+1)
bigone nvars = 2^2^nvars - 1

The projection functions var mn can be combined with the usual bitwise
integer operators, to obtain new bitstring truth tables, encoding all possible
value combinations of their arguments, as shown in [27]. Note that the constant
n
0 evaluates to 0 while the constant 1 is evaluated as 22 − 1 by the function
bigone.
The function ite used in eval with mask implements the boolean function
if x then t else e using arbitrary length bitvector operations:
ite_ x t e = ((t ‘xor‘ e).&.x) ‘xor‘ e

As the following example shows, it turns out that boolean evaluation eval bdd
faithfully emulates fold bdd!
∗ISO> unfold_bdd (3,42)
BDD 3 (D 2 (D 1 (D 0 B0 B0) (D 0 B0 B0))
(D 1 (D 0 B1 B1) (D 0 B1 B0)))
∗ISO> eval_bdd it
42

10.4

The Equivalence

We will now state the surprising (and new!) result that boolean evaluation and
structural transformation with repeated application of pairing produce the same
result:
Proposition 10 The complete binary tree of depth n, obtained by recursive applications of bitunpair on a truth table tt computes an (unreduced) BDD, that,
when evaluated, returns the truth table, i.e.
f old bdd ◦ unf old bdd ≡ id

(21)

eval bdd ◦ unf old bdd ≡ id

(22)

Proof. The function unfold bdd builds a binary tree by splitting the bitstring
tt ∈ [0..2n − 1] up to depth n. Observe that this corresponds to the Shannon
expansion [28] of the formula associated to the truth table, using variable order
[n − 1, ..., 0]. Observe that the effect of bitunpair is the same as
– the effect of var mn m n (n-1) acting as a mask selecting the left branch,
and
– the effect of its complement, acting as a mask selecting the right branch.
Given that 2n is the double of 2n−1 , the same invariant holds at each step, as
the bitstring length of the truth table reduces to half.
We can thus assume from now on, that the BDD data type defined in section
10 actually represents BDDs mapped one-to-one to truth tables given as natural numbers. An interesting application of this result would be to investigate
practical uses of bitpair/bitunpair operations in actual circuit design.

11

Ranking and Unranking of BDDs

One more step is needed to extend the mapping between BDDs with n variables
to a bijective mapping from/to N at: we will have to “shift towards infinity” the
starting point of each new block3 of BDDs in N at as BDDs of larger and larger
sizes are enumerated.
First, we need to know by how much - so we will count the number of boolean
functions with up to n variables.
bsum 0 = 0
bsum n | n>0 = bsum1 (n-1)
bsum1 0 = 2
bsum1 n | n>0 = bsum1 (n-1)+ 2^2^n

The stream of all such sums can now be generated as usual4 :
bsums = map bsum [0..]
∗ISO> genericTake 7 bsums
[0,2,6,22,278,65814,4295033110]

What we are really interested into, is decomposing n into the distance n-m
to the last bsum m smaller than n, and the index that generates the sum, k.
to_bsum n = (k,n-m) where
k=pred (head [x | x←[0..],bsum x>n])
m=bsum k
3
4

defined by the same number of variables
bsums is sequence A060803 in The On-Line Encyclopedia of Integer Sequences, http:
//www.research.att.com/∼njas/sequences

Unranking of an arbitrary BDD is now easy - the index k determines the number
of variables and n-m determines the rank. Together they select the right BDD
with unfold bdd and bdd.
nat2bdd n = unfold_bdd (k,n_m) where (k,n_m)=to_bsum n

Ranking of a BDD is even easier: we shift its rank within the set of BDDs with
nv variables, by the value (bsum nv) that counts the ranks previously assigned.
bdd2nat bdd@(BDD nv _) = (bsum nv)+tt where
(_,tt) =fold_bdd bdd

As the following example shows bdd2nat implements the inverse of nat2bdd.
∗ISO> nat2bdd 42
BDD 3 (D 2 (D 1 (D 0 B0 B1) (D 0 B1 B0))
(D 1 (D 0 B0 B0) (D 0 B0 B0)))
∗ISO> bdd2nat it
42

This provides the Encoder:
pbdd :: Encoder (BDD Nat)
pbdd = compose (Iso bdd2nat nat2bdd) nat

working as follows:
∗ISO> as pbdd nat 2008
BDD 4 (D 3 (D 2 B0 (D 1 (D 0 B0 B1) B1))
(D 2 (D 1 (D 0 B1 B1) B0) (D 1 B0 B1)))
∗ISO> as nat pbdd it
2008

We can now repeat the ranking function construction for eval bdd:
ev_bdd2nat bdd@(BDD nv _) = (bsum nv)+(eval_bdd bdd)

We can confirm that ev bdd2nat also acts as an inverse to nat2bdd:
∗ISO> ev_bdd2nat (nat2bdd 2008)
2008

We obtain the Encoder:
bdd :: Encoder (BDD Nat)
bdd = compose (Iso ev_bdd2nat nat2bdd) nat

working as follows:
∗ISO> as bdd nat 2008
BDD 4 (D 3 (D 2 (D 1 (D
(D 1 (D
(D 2 (D 1 (D
(D 1 (D
∗ISO> as nat bdd it
2008

0
0
0
0

B0
B0
B1
B0

B0)
B1)
B1)
B0)

(D 0 B0 B0))
(D 0 B1 B0)))
(D 0 B0 B0))
(D0 B1 B0))))

This result can be seen as an intriguing isomorphism between boolean, arithmetic
and symbolic computations.

11.1

Reducing the BDDs

We will sketch here a simplified reduction mechanism for BDDs eliminating
identical branches. As nodes of a BDD are mapped bijectively to unique natural
numbers we will omit the (trivial) implementation of node sharing, with the
implicit assumption that subtrees having the same encoding are shared.
The function bdd reduce reduces a BDD by collapsing identical left and
right subtrees, and the function bdd associates this reduced form to n ∈ N at.
bdd_reduce (BDD n bt) = BDD n (reduce bt) where
reduce B0 = B0
reduce B1 = B1
reduce (D _ l r) | l == r = reduce l
reduce (D v l r) = D v (reduce l) (reduce r)
unfold_rbdd = bdd_reduce . unfold_bdd

The results returned by unfold rbdd for n=2 are:
BDD
BDD
BDD
BDD
...
BDD
BDD

2
2
2
2

(C
(D
(D
(D

0)
1 (D 0 (C 1) (C 0)) (C 0))
1 (C 0) (D 0 (C 1) (C 0)))
0 (C 1) (C 0))

2 (D 1 (D 0 (C 0) (C 1)) (C 1))
2 (C 1)

We can now define the unranking operation on reduced BDDs
nat2rbdd = bdd_reduce . nat2bdd

and obtain the Encoder
rbdd :: Encoder (BDD Nat)
rbdd = compose (Iso ev_bdd2nat nat2rbdd) nat

working as follows
∗ISO> as rbdd nat 2008
BDD 4 (D 3 (D 2 B0 (D 1 (D 0 B0 B1) (D 0 B1 B0)))
(D 2 (D 1 B1 B0) (D 1 B0 (D 0 B1 B0))))
∗ISO> as nat rbdd it
2008

To be able to compare its space complexity with other representations we
will define a size operation on a BDD as follows:
bdd_size (BDD _ t) = 1+(size t) where
size B0 = 1
size B1 = 1
size (D _ l r) = 1+(size l)+(size r)

This measures the size of the BDD or reduced BDD as an expression tree. To
take into account sharing (as present in a standard ROBDD implementation)
one can simply eliminate duplicated subtrees:

robdd_size (BDD _ t) = 1+(rsize t) where
rsize = genericLength . nub . rbdd_nodes
rbdd_nodes B0 = [B0]
rbdd_nodes B1 = [B1]
rbdd_nodes (D v l r) =
[(D v l r)] ++ (rbdd_nodes l) ++ (rbdd_nodes r)

12
12.1

Generalizing BDD ranking/unranking functions
Encoding BDDs with Arbitrary Variable Order

While the encoding built around the equivalence described in Prop. 10 between
bitwise pairing/unpairing operations and boolean decomposition is arguably as
simple and elegant as possible, it is useful to parametrize BDD generation with
respect to an arbitrary variable order. This is of particular importance when
using BDDs for circuit minimization, as different variable orders can make circuit
sizes flip from linear to exponential in the number of variables [26].
Given a permutation of n variables represented as natural numbers in [0..n−1]
n
and a truth table tt ∈ [0..22 − 1] we can define:
to_bdd vs tt | 0 ≤ tt && tt ≤ m =
BDD n (to_bdd_mn vs tt m n) where
n=genericLength vs
m=bigone n
to_bdd _ tt = error
("bad arg in to_bdd⇒" ++ (show tt))

where the function to bdd mn recurses over the list of variables vs and applies Shannon expansion [28], expressed as bitvector operations. This computes
branches f 1 and f 0, to be used as then and else parts, when evaluating back
the BDD to a truth table with if-the-else functions.
to_bdd_mn []
0 _ _ = B0
to_bdd_mn []
_ _ _ = B1
to_bdd_mn (v:vs) tt m n = D v l r where
cond=var_mn m n v
f0= (m ‘xor‘ cond) .&. tt
f1= cond .&. tt
l=to_bdd_mn vs f1 m n
r=to_bdd_mn vs f0 m n

Proposition 11 The function to bdd builds an (unreduced) BDD corresponding to a truth table tt for variable order vs that returns tt when evaluated as a
boolean function.
We can reduce the resulting BDDs, and convert back from BDDs and reduced
BDDs to truth tables with boolean evaluation:

to_rbdd vs tt = bdd_reduce (to_bdd vs tt)
from_bdd bdd = eval_bdd bdd

We can obtain BDDs and reduced BDDs of various sizes as follows:
∗ISO> as perm nat 5
[0,2,1]
∗ISO> to_bdd (as perm nat 5) 42
BDD 3 (D 0 (D 2 (D 1 B0 B0) (D 1 B1 B1))
(D 2 (D 1 B0 B0) (D 1 B1 B0)))
∗ISO> to_rbdd (as perm nat 5) 42
BDD 3 (D 0 (D 2 B0 B1) (D 2 B0 (D 1 B1 B0)))
∗ISO> to_rbdd (as perm nat 8) 42
BDD 3 (D 2 B0 (D 0 B1 (D 1 B1 B0)))
ISO> from_bdd it
42

Finally, we can, obtain a minimal BDD expressing a logic function of n variables
given as a truth table as follows:
to_min_bdd n t = search_bdd min n t
search_bdd f n tt = snd $ foldl1 f
(map (sized_rbdd tt) (all_permutations n)) where
sized_rbdd tt vs = (robdd_size b,b) where
b=to_rbdd vs tt
all_permutations n = if n==0 then [[]] else
[nth2perm (n,i) | i←[0..(factorial n)-1]] where
factorial n=foldl1 (∗) [1..n]

As the following examples show, this can provide an effective multilevel boolean
formula minimization up to functions with 6-7 arguments.
∗ISO>
BDD 3
∗ISO>
BDD 4

to_min_bdd 3
(D 0 (D 2 B0
to_min_bdd 4
(D 3 (D 1 (D
(D 2 (D 1 (D
∗ISO> to_min_bdd 7
BDD 7 (D 0 (D 1 (D

42
B1) (D 1 (D 2 B0 B1) B0))
2008
0 B0 B1) (D 0 B1 B0))
0 B0 B1) B0) (D 0 B1 B0)))
2008
2 (D 6
(D 4 (D 3 B0 B1) (D 3 B1 B0))
(D 5 (D 4 (D 3 B0 B1) B0)
(D 3 B1 B0))) B0) B0) B0)
∗ISO> robdd_size it
12

12.2

Multi-Terminal Binary Decision Diagrams (MTBDD)

MTBDDs [29,30] are a natural generalization of BDDs allowing non-binary values as leaves. Such values are typically bitstrings representing the outputs of a
multi-terminal boolean function, encoded as unsigned integers.

We shall now describe an encoding of M T BDDs that can be extended to
ranking/unranking functions, in a way similar to BDDs as shown in section 11.
Our MTBDD data type is a binary tree like the one used for BDDs, parameterized by two integers m and n, indicating that an MTBDD represents a function
from [0..n − 1] to [0..m − 1], or equivalently, an n-input/m-output boolean function.
data MT a = L a | M a (MT a) (MT a) deriving (Eq,Ord,Read,Show)
data MTBDD a = MTBDD a a (MT a) deriving (Show,Eq)

The function to mtbdd creates, from a natural number tt representing a
truth table, an MTBDD representing functions of type N → M with M =
[0..2m − 1], N = [0..2n − 1]. Similarly to a BDD, it is represented as binary tree
of n levels, except that its leaves are in [0..2m − 1].
to_mtbdd m n tt = MTBDD m n r where
mlimit=2^m
nlimit=2^n
ttlimit=mlimit^nlimit
r=if tt<ttlimit
then (to_mtbdd_ mlimit n tt)
else error
("bt: last arg "++ (show tt)++
" should be < " ++ (show ttlimit))

Given that correctness of the range of tt has been checked, the function to mtbdd
applies bitmerge unpair recursively up to depth n, where leaves in range [0..mlimit−
1] are created.
to_mtbdd_ mlimit n tt | (n<1)&&(tt<mlimit) = L tt
to_mtbdd_ mlimit n tt = (M k l r) where
(x,y)=bitunpair tt
k=pred n
l=to_mtbdd_ mlimit k x
r=to_mtbdd_ mlimit k y

Converting back from M T BDDs to natural numbers is basically the same thing
as for BDDs, except that assertions about the range of leaf data are enforced.
from_mtbdd (MTBDD m n b) = from_mtbdd_ (2^m) n b
from_mtbdd_ mlimit n (L
from_mtbdd_ mlimit n (M
k=pred n
x=from_mtbdd_ mlimit
y=from_mtbdd_ mlimit
tt=bitpair (x,y)

tt) | (n<1)&&(tt<mlimit)=tt
_ l r) = tt where
k l
k r

The following examples show that to mtbdd and from mtbdd are indeed inverses
values in [0..2n − 1] × [0..2m − 1].
>to_mtbdd 3 3 2008
MTBDD 3 3

(M 2
(M 1
(M
(M
(M 1
(M
(M

0 (L 2) (L 1))
0 (L 2) (L 1)))
0 (L 2) (L 0))
0 (L 1) (L 1))))

>from_mtbdd it
2008
>mprint (to_mtbdd 2
MTBDD 2 2
(M 1 (M 0 (L 0)
MTBDD 2 2
(M 1 (M 0 (L 1)
MTBDD 2 2
(M 1 (M 0 (L 0)
MTBDD 2 2
(M 1 (M 0 (L 1)

13

2) [0..3]
(L 0)) (M 0 (L 0) (L 0)))
(L 0)) (M 0 (L 0) (L 0)))
(L 0)) (M 0 (L 1) (L 0)))
(L 0)) (M 0 (L 1) (L 0)))

Revisiting Encodings of Finite Functions

We will now generalize the bitpair pairing function to k-tuples and then we
will derive an alternative encoding for finite functions.
13.1

Tuple Encodings as Generalized Bitpair

The function to tuple: N at → N atk converts a natural number to a k-tuple
by splitting its bit representation into k groups, from which the k members in
the tuple are finally rebuilt. This operation can be seen as a transposition of a
bit matrix obtained by expanding the number in base 2k :
to_tuple k n = map (from_base 2) (
transpose (
map (to_maxbits k) (
to_base (2^k) n
)
)
)

To convert a k-tuple back to a natural number we will merge their bits, k at a
time. This operation uses the transposition of a bit matrix obtained from the
tuple, seen as a number in base 2k , with help from bit crunching functions given
in APPENDIX:
from_tuple ns = from_base (2^k) (
map (from_base 2) (
transpose (

map (to_maxbits l) ns
)
)
) where
k=genericLength ns
l=max_bitcount ns

The following example shows the decoding of 42, its decomposition in bits (right
to left), the formation of a 3-tuple and the encoding of the tuple back to 42.
∗ISO> to_base 2 42
[0,1,0,1,0,1]
∗ISO> to_tuple 3 42
[2,1,2]
∗ISO> to_base 2 2
[0,1]
∗ISO> to_base 2 1
[1]
∗ISO> from_tuple [2,1,2]
42

Fig. 18 shows multiple steps of the same decomposition, with shared nodes collected in a DAG.

2008
1 0
42

2

14

2 0
1

2
1

1

0
4

20

2

01
0

0

2 2

0

2 1
1
1

Fig. 18: Repeated 3-tuple expansions: 42 and 2008

13.2

Encoding Finite Functions as Tuples

As finite sets can be put in a bijection with an initial segment of N at, a finite
function can be seen as a function defined from an initial segment of N at to
N at. We can encode and decode a finite function from [0..k − 1] to N at (seen as
the list of its values), as a natural number:

ftuple2nat [] = 0
ftuple2nat ns = succ (pepis_pair (pred k,t)) where
k=genericLength ns
t=from_tuple ns
nat2ftuple 0 = []
nat2ftuple kf = to_tuple (succ k) f where
(k,f)=pepis_unpair (pred kf)

As the length of the tuple, k, is usually smaller than the number obtained by
merging the bits of the k-tuple, we have picked the Pepis pairing function, exponential in its first argument and linear in its second, to embed the length of the
tuple needed for the decoding. This suggest the following alternative Encoder
for finite functions:
fun’ :: Encoder [Nat]
fun’ = compose (Iso ftuple2nat nat2ftuple) nat

as well as the related alternative hylomorphism:
nat_fun’ = Iso nat2ftuple ftuple2nat
hff’ :: Encoder T
hff’ = compose (hylo nat_fun’) nat

The encoding/decoding and the hylomorphism work as follows:
∗ISO> as fun’ nat 2008
[3,2,3,1]
∗ISO> as nat fun’ it
2008
∗ISO> as hff’ nat 2008
H [H [H [H []]],H [H [],H []],H [H [H []]],H [H []]]
∗ISO> as nat hff’ it
2008

14

Directed Graphs, Undirected graphs, Multigraphs
and Hypergraphs

We will now show that more complex data types like digraphs and hypergraphs
have extremely simple encoders. This shows once more the importance of compositionality in the design of our embedded transformation language.
14.1

Encoding Directed Graphs

We can find a bijection from directed graphs (with no isolated vertices, corresponding to their view as binary relations), to finite sets by fusing their list of
ordered pair representation into finite sets with a pairing function:

digraph2set ps = map bitpair ps
set2digraph ns = map bitunpair ns

The resulting Encoder is:
digraph :: Encoder [Nat2]
digraph = compose (Iso digraph2set set2digraph) set

working as follows:
∗ISO> as digraph nat 2008
[(1,1),(2,0),(2,1),(3,1),(0,2),(1,2),(0,3)]
∗ISO> as nat digraph it
2008
∗ISO> as rbdd digraph [(1,1),(2,0),(2,1),
(3,1),(0,2),(1,2),(0,3)]
BDD 4 (D 3 (D 2 B0 (D 1 (D 0 B0 B1) (D 0 B1 B0)))
(D 2 (D 1 B1 B0) (D 1 B0 (D 0 B1 B0))))

Fig. 19 shows the digraph associated to 2008.

0

3

1

2

Fig. 19: 2008 as a digraph

14.2

Encoding Undirected Graphs

We can find a bijection from undirected graphs to finite sets by fusing their
list of unordered pair representation into finite sets with a pairing function on
unordered pairs:
graph2set ps = map unord_pair ps
set2graph ns = map unord_unpair ns

The resulting Encoder is:

graph :: Encoder [[Nat]]
graph = compose (Iso graph2set set2graph) set

working as follows:
∗ISO> as graph nat 2008
[[1,3],[2,3],[2,4],[3,5],[0,3],[1,4],[0,4]]
∗ISO> as nat graph it
2008
∗ISO> as nat graph
[[1,3],[3,2],[2,4],[5,3],[0,3],[4,1],[0,4]]
2008

Note that, as expected, the result is invariant to changing the order of elements
in pairs like [1,4] and [3,5] to [4,1] and [5,3].
14.3

Encoding Directed Multigraphs

We can find a bijection from directed multigraphs (directed graphs with multiple
edges between pairs of vertices) to finite sequences by fusing their list of ordered
pair representation into finite sequences with a pairing function:
The resulting Encoder is:
mdigraph :: Encoder [Nat2]
mdigraph = compose (Iso digraph2set set2digraph) fun

working as follows:
∗ISO> as mdigraph nat 2008
[(1,1),(0,0),(1,0),(0,0),(0,0),(0,0),(0,0)]
∗ISO> as nat mdigraph it
2008

Note that the only change to the digraph Encoder is replacing the composition
with set by a composition with fun.
14.4

Encoding Undirected Multigraphs

We can find a bijection from undirected multigraphs (undirected graphs with
multiple edges between unordered pairs of vertices) to finite sequences by fusing
their list of pair representation into finite sequences with a pairing function on
unordered pairs:
The resulting Encoder is:
mgraph :: Encoder [[Nat]]
mgraph = compose (Iso graph2set set2graph) fun

working as follows:
∗ISO> as mgraph nat 2008
[[1,3],[0,1],[1,2],[0,1],[0,1],[0,1],[0,1]]
∗ISO> as nat mgraph it
2008

Note that the only change to the graph Encoder is replacing the composition
with set by a composition with fun.
14.5

Encoding Hypergraphs

Definition 2 A hypergraph (also called set system) is a pair H = (X, E) where
X is a set and E is a set of non-empty subsets of X.
We can easily derive a bijective encoding of hypergraphs, represented as sets of
sets:
set2hypergraph = map nat2set
hypergraph2set = map set2nat

The resulting Encoder is:
hypergraph :: Encoder [[Nat]]
hypergraph = compose (Iso hypergraph2set set2hypergraph) set

working as follows
∗ISO> as hypergraph nat 2008
[[0,1],[2],[1,2],[0,1,2],[3],[0,3],[1,3]]
∗ISO> as nat hypergraph it
2008

15

Encoding SAT problems

Boolean Satisfiability (SAT) problems are encoded as lists of lists representing
conjunctions of disjunctions of positive or negative propositional symbols.
After defining:
set2sat = map (set2disj . nat2set) where
shift0 z = if (z<0) then z else z+1
set2disj = map (shift0. nat2z)
sat2set = map (set2nat . disj2set) where
shiftback0 z = if(z<0) then z else z-1
disj2set = map (z2nat . shiftback0)

we obtain the Encoder
sat :: Encoder [[Z]]
sat = compose (Iso sat2set set2sat) set

working as follows:
∗ISO> as sat nat 2008
[[1,-1],[2],[-1,2],[1,-1,2],[-2],[1,-2],[-1,-2]]
∗ISO> as nat sat it
2008

Clearly this encoding can be used to generate random SAT problems out of
easier to generate random natural numbers.

16

An Encoder for Graph Models

Graph models [31,32] provide a semantics of λ-calculus (Y-combinator included)
in terms of sets of finite sets of natural numbers. Following [31] a graph model
is a pair (D, p) where D is an infinite set and p : D∗ × D → D is an injective
total function. We will strengthen this to be a bijection, for the case D = N at
as follows.
gmodel2nat (set,m) = pred (fun2nat (m : (set2fun set)))
nat2gmodel n = (fun2set xs,m) where (m:xs) = nat2fun (succ n)

This provides the Encoder:
type Gdomain= ([Nat],Nat)
gmodel :: Encoder Gdomain
gmodel = compose (Iso gmodel2nat nat2gmodel) nat

working as follows:
∗ISO> as gmodel nat 42
([0,2,4],0)
∗ISO> as nat gmodel it
42

The interests of such models is that they provide an accurate set theoretic semantics for untyped lambda calculus describing key computational mechanisms
like β-conversion and fixpoint combinators.

17

A mapping to a dense set: Dyadic Rationals in [0, 1)

So far our isomorphisms have focused on natural numbers, finite sets and other
discrete data types. Dyadic rationals are fractions with denominators restricted
to be exponents of 2. They are a dense set in R i.e. they provide arbitrarily close
approximations for any real number. An interesting isomorphism to such a set
would allow borrowing things like distance or average functions that could have
interesting interpretations in symbolic or boolean domains. It also makes sense
to pick a bounded subdomain of the dyadic rationals that can be meaningful
as the range of probabilistic boolean functions or fuzzy sets. We will build an
Encoder for Dyadic Rationals in [0, 1) by providing a bijection from finite sets
of natural numbers seen this time as negative exponents of 2.
dyadic :: Encoder (Ratio Nat)
dyadic = compose (Iso dyadic2set set2dyadic) set

The function set2dyadic mimics set2nat defined in subsection 3.3, except for
the use of negative exponents and computation on rationals.
set2dyadic :: [Nat] → Ratio Nat
set2dyadic ns = rsum (map nexp2 ns) where
nexp2 0 = 1%2
nexp2 n = (nexp2 (n-1))∗(1%2)

rsum [] = 0%1
rsum (x:xs) = x+(rsum xs)

The function dyadic2set extracts negative exponents of two from a dyadic
rational and it is modeled after nat2set defined in subsection 3.3.
dyadic2set :: Ratio Nat → [Nat]
dyadic2set n | good_dyadic n = dyadic2exps n 0 where
dyadic2exps 0 _ = []
dyadic2exps n x =
if (d<1) then xs else (x:xs) where
d = 2∗n
m = if d<1 then d else (pred d)
xs=dyadic2exps m (succ x)
dyadic2set _ =
error "dyadic2set: argument not a dyadic rational"

As not all rational numbers are dyadics in [0, 1), the predicate good dyadic is
needed validate the input of dyadic2set. This also ensures that dyadic2set
always terminates returning a finite set.
good_dyadic kn = (k==0 && n==1)
| | ((kn>0%1) && (kn<1%1) && (is_exp2 n)) where
k=numerator kn
n=denominator kn
is_exp2 1 = True
is_exp2 n | even n = is_exp2 (n ‘div‘ 2)
is_exp2 n = False

Some examples of borrow/lend operations are:
dyadic_dist x y = abs (x-y)
dist_for t x y = as dyadic t
(borrow2 (with dyadic t) dyadic_dist x y)
dsucc = borrow (with nat dyadic) succ
dplus = borrow2 (with nat dyadic) (+)
dconcat = lend2 dyadic (++)
∗ISO> dist_for nat 6 7
1%2
∗ISO> dist_for set [1,2,3] [3,4,5]
21%64
∗ISO> dsucc (3%8)
7%8

Fig. 20 shows the dyadic rationals associated to natural numbers in [0..255].

Fig. 20: Dyadic rationals associated to n in [0..255]

18
18.1

Strings and Parenthesis Languages
Encoding Strings

As strings can be seen just as a notational equivalent of lists of natural numbers
we obtain an Encoder immediately as:
string :: Encoder String
string = Iso string2fun fun2string
string2fun cs = map (fromIntegral . ord) cs
fun2string ns = map (chr . fromIntegral) ns

Note however that this is only an isomorphism within the chr/ord conversion
range, therefore we shall assume this constraint as a law governing this Encoder.
∗ISO> as set string "hello"
[104,206,315,424,536]
∗ISO> as string set it
"hello"

18.2

Encoding a Parenthesis Language

An encoder for a parenthesis language is obtained by combining a parser and
writer. As Hereditarily Finite Functions naturally map one-to-one to a parenthesis expression we will choose them as target of the transformers.
pars :: Encoder [Char]
pars = compose (Iso pars2hff hff2pars) hff

The parser recurses over a string and builds a HFF as follows:
pars2hff cs = parse_pars ’(’ ’)’ cs
parse_pars l r cs | newcs == [] = t where
(t,newcs)=pars_expr l r cs
pars_expr l r (c:cs) | c==l = ((H ts),newcs) where
(ts,newcs) = pars_list l r cs
pars_list l r (c:cs) | c==r = ([],cs)
pars_list l r (c:cs) = ((t:ts),cs2) where
(t,cs1)=pars_expr l r (c:cs)
(ts,cs2)=pars_list l r cs1

The writer recurses over a HFF and collects matching parenthesis pairs:
hff2pars = collect_pars ’(’ ’)’
collect_pars l r (H ns) =
[l]++
(concatMap (collect_pars l r) ns)
++[r]

The transformations of 42 look as follows:
∗ISO> as pars nat 42
"((())(())(()))"
∗ISO> as hff pars it
H [H [H []],H [H []],H [H []]]
∗ISO> as nat hff it
42

Alternatively, by using a 0 and 1 as left and right parenthesis we can define:
bitpars2hff cs = parse_pars 0 1 cs
hff2bitpars = collect_pars 0 1
hff_pars :: Encoder [Nat]
hff_pars = compose (Iso bitpars2hff hff2bitpars) hff

working as follows:
∗ISO> as hff_pars nat 2008
[0,0,0,1,0,1,1,0,1,0,0,1,1,0,1,0,1,0,1,0,1,1]
∗ISO> as nat hff_pars it

2008
∗ISO> as nat bits (as hff_pars nat 2008)
7690599

As the last example shows, the information density of a parenthesis representation is lower. This is expected, given that order is constrained by balancing and
content is constrained by having the same number of 0s and 1s. The following
example
∗ISO> map ((as nat bits) . (as hff_pars nat)) [0..7]
[5,27,119,115,495,483,471,467]

shows that this application is injective only. Therefore a succinct representation
of an abstract tree structure can be obtained by encoding it as a natural number
as in:
∗ISO> as nat pars "((()())()(())()()()())"
2008

Note however, that
∗ISO> as nat bits (as hff_pars nat (2^2^16))
32639

while the conventional representation of the same number would have a few
thousand digits. This suggest defining:
nat2parnat n = as nat bits (as hff_pars nat n)
parnat2nat n = as nat hff_pars (as bits nat n)

and find out that
∗ISO> [x | x←[0..2^16],nat2parnat x<x]
[8192,16384,32768,32769,49152,65536]

One can see that more compact representations only happen for a few numbers
that are powers of two or “sparse” sums of powers of two. A good way to evaluate “information density” for an arbitrary data type that is isomorphic to Nat
through one of our encoders is to compute the total bitsize of its actual encoding
over an interval like [0..2n−1 ]. For instance,
hff_bitsize n= sum (map hff_bsize [0..2^n-1])
hff_bsize k=genericLength (as bits nat (nat2parnat k))

Knowing that the optimal bit representation of all numbers in [0..2n−1 ] totals
n ∗ 2n (2n of them, n bits each), we can define a measure of information density
for a bit-encoded parenthesis language seen as a representation for HFF as:
info_density_hff n = (n∗2^n)%(hff_bitsize n)

One can see that information density progressively increases to converge to a
value above half of the “perfect” value of 1:

∗ISO> map info_density_hff [0..12]
[0%1,1%3,4%9,12%25,1%2,80%157,16%31,112%215,
32%61,48%91,1024%1933,2816%5297,2048%3841]
∗ISO> map fromRational it
[0.0,0.3333333333333333,0.4444444444444444,0.48,0.5,
0.5095541401273885,0.5161290322580645,0.5209302325581395,
0.5245901639344263,0.5274725274725275,0.5297465080186239,
0.5316216726448934,0.5331944806040094]

To compare this with the information density of hereditarily finite sets, multisets and permutations, we can also map their structure to a bit-represented
parenthesis language by defining the encoder:
pars_hf=Iso bitpars2hff hff2bitpars
hff_pars’ :: Encoder [Nat]
hff_pars’ = compose pars_hf hff’
hfs_pars :: Encoder [Nat]
hfs_pars = compose pars_hf hfs
hfpm_pars :: Encoder [Nat]
hfpm_pars = compose pars_hf hfpm
hfm_pars :: Encoder [Nat]
hfm_pars = compose pars_hf hfm
bhfm_pars :: Encoder [Nat]
bhfm_pars = compose pars_hf hfbm
bhfm_pars’ :: Encoder [Nat]
bhfm_pars’ = compose pars_hf hfbm’
hfp_pars :: Encoder [Nat]
hfp_pars = compose pars_hf hfp

and then defining:
parsize_as t n = genericLength (hff2bitpars (as t nat n))
parsizes_to m t = map (parsize_as t) [0..2^m-1]
nat2hfsnat n = as nat bits (as hfs_pars nat n)
hfs_bitsize n= sum (map hfs_bsize [0..2^n-1])
hfs_bsize k=genericLength (as bits nat (nat2hfsnat k))
info_density_hfs n = (n∗2^n)%(hfs_bitsize n)

The intuition that hereditarily finite functions have higher information density
than hereditarily finite sets can now be conjectured:

∗ISO> map info_density_hfs [0..12]
[0%1,1%3,2%5,3%8,1%3,5%16,2%7,7%27,4%17,3%13,2%9,11%52,1%5]
∗ISO> map fromRational it
[0.0,0.3333333333333333,0.4,0.375,0.3333333333333333,
0.3125,0.2857142857142857,0.25925925925925924,0.23529411764705882,
0.23076923076923078,0.2222222222222222,0.21153846153846154,0.2]

Contrary to the case of bit-encoded HFFs, in this case information density is
decreasing for larger values - an observation that can help with finding a simple
proof for the conjecture. More generally, such techniques suggest applications to
experimental mathematics.

19

Self-delimiting codes

A more precise estimate of the actual size of various bitstring representations requires also counting the overhead for “delimiting” their components. An asymptotically optimal mechanism for this is the use of a universal self-delimiting code
for instance, the Elias omega code. To implement it, the encoder proceeds by
recursively encoding length of the string, the length of the length of the strings
etc.
to_elias :: Nat → [Nat]
to_elias n = (to_eliasx (succ n))++[0]
to_eliasx 1 = []
to_eliasx n = xs where
bs=to_lbits n
l=(genericLength bs)-1
xs = if l<2 then bs else (to_eliasx l)++bs

The decoder first rebuilds recursively the sequence of lengths and then the actual
bitstring. It makes sense to design the decoder to extract the number represented
by the self-delimiting code from a sequence/stream of bits and also return what
is left after the extraction.
from_elias :: [Nat] → (Nat, [Nat])
from_elias bs = (pred n,cs) where (n,cs)=from_eliasx 1 bs
from_eliasx n (0:bs) = (n,bs)
from_eliasx n (1:bs) = r where
hs=genericTake n bs
ts=genericDrop n bs
n’=from_lbits (1:hs)
r=from_eliasx n’ ts
to_lbits = reverse . (to_base 2)
from_lbits = (from_base 2) . reverse

We obtain the Encoder:

elias :: Encoder [Nat]
elias = compose (Iso (fst . from_elias) to_elias) nat

working as follows:
∗ISO> as elias nat 42
[1,0,1,0,1,1,0,1,0,1,1,0]
∗ISO> as nat elias it
42
∗ISO> as elias nat 2008
[1,1,1,0,1,0,1,1,1,1,1,0,1,1,0,0,1,0]
∗ISO> as nat elias it
2008

Note that self-delimiting codes are not onto the regular language {0, 1}∗ , therefore this Encoder cannot be used to map arbitrary bitstrings to numbers.

20

Encoding DNA

We have covered so far encodings for “artificial entities” used in various fields.
We will now add an encoding of “natural origin”, DNA bases and strands. While
it is an (utterly) simplified model of the real thing, it captures some essential
algebraic properties of DNA bases and strands.
We start with a DNA data type, following [33,34]:
data Base = Adenine | Cytosine | Guanine | Thymine
deriving(Eq,Ord,Show,Read)
type DNA = [Base]

We will encode/decode the DNA base alphabet as follows:
alphabet2code
alphabet2code
alphabet2code
alphabet2code

Adenine = 0
Cytosine = 1
Guanine = 2
Thymine = 3

code2alphabet
code2alphabet
code2alphabet
code2alphabet

0
1
2
3

=
=
=
=

Adenine
Cytosine
Guanine
Thymine

The mapping is simply a symbolic variant of conversion to/from base 4:
dna2nat = (from_base 4) . (map alphabet2code)
nat2dna = (map code2alphabet) . (to_base 4)

We can now define a decoder for base sequences as follows:
dna :: Encoder DNA
dna = compose (Iso dna2nat nat2dna)

nat

A first set of DNA operations act on base sequences. The transformation
between complements looks as follows:
dna_complement :: DNA → DNA
dna_complement = map to_compl where
to_compl Adenine = Thymine
to_compl Cytosine = Guanine
to_compl Guanine = Cytosine
to_compl Thymine = Adenine

Reversing is just list reversal.
dna_reverse :: DNA → DNA
dna_reverse = reverse

As reversal and complement are independent operations their composition is
commutative - we can pick reversing first and then complementing:
dna_comprev :: DNA → DNA
dna_comprev = dna_complement . dna_reverse

The following examples show interaction of DNA codes with other data types
and their operations:
∗ISO> as dna nat 2008
[Adenine,Guanine,Cytosine,Thymine,Thymine,Cytosine]
∗ISO> borrow (with dna nat) dna_reverse 42
42
∗ISO> borrow (with dna nat) dna_reverse 2008
637
∗ISO> borrow (with dna nat) dna_complement 2008
2087
∗ISO> borrow (with dna nat) dna_comprev 2008
3458
∗ISO> borrow (with dna bits)
dna_comprev [1,0,1,0,1,1,0,1,0,1]
[1,1,1,0,1,0,0,0,0,1,1]

Note that each of these DNA operations induces a bijection N at → N at.
Like signed integers, DNA strands have “polarity” - their direction matters:
data Polarity = P3x5 | P5x3
deriving(Eq,Ord,Show,Read)
data DNAstrand = DNAstrand Polarity DNA
deriving(Eq,Ord,Show,Read)

Polarity can be easily encoded as parity even/odd:
strand2nat (DNAstrand polarity strand) =
add_polarity polarity (dna2nat strand) where
add_polarity P3x5 x = 2∗x
add_polarity P5x3 x = 2∗x-1

nat2strand n =
if even n
then DNAstrand P3x5 (nat2dna (n ‘div‘ 2))
else DNAstrand P5x3 (nat2dna ((n+1) ‘div‘ 2))

We can now define an Encoder for DNA strands:
dnaStrand :: Encoder DNAstrand
dnaStrand = compose (Iso strand2nat nat2strand) nat

Two additional operations lift DNA sequences to strands with polarities:
dna_down :: DNA → DNAstrand
dna_down = (DNAstrand P3x5) . dna_complement
dna_up :: DNA → DNAstrand
dna_up = DNAstrand P5x3

We can now lend or borrow operations as follows:
∗ISO> as dnaStrand nat 1234
DNA P3x5 [Cytosine,Guanine,Guanine,Cytosine,Guanine]
∗ISO> lend (with dnaStrand nat) succ
(DNAstrand P5x3 [Adenine,Cytosine,Guanine,Thymine])
DNAstrand P5x3 [Cytosine,Cytosine,Guanine,Thymine]

The DoubleHelix is a stable combination of two complementary strands. This
built-in redundancy protects against unwanted mutations.
data DoubleHelix = DoubleHelix DNAstrand DNAstrand
deriving(Eq,Ord,Show,Read)
dna_double_helix :: DNA → DoubleHelix
dna_double_helix s =
DoubleHelix (dna_up s) (dna_down s)

We can now generate a double helix from a natural number:
∗ISO> dna_double_helix (nat2dna 33)
DoubleHelix
(DNAstrand P5x3 [Cytosine,Adenine,Guanine])
(DNAstrand P3x5 [Guanine,Thymine,Cytosine])

This can be used for generating random instances of double helixes by reusing
a random generator for natural numbers.

21

Testing It All

We will now describe a random testing mechanism to validate our Encoders.
While QuickCheck [7] provides an elegant general purpose random tester, it
would require writing a specific adaptor for each isomorphism. We will describe
here a shortcut through a few higher order combinators.
First, we build a simple random generator for nat

rannat = rand (2^50)
rand :: Nat→Nat→Nat
rand max seed = n where
(n,g)=randomR (0,max) (mkStdGen (fromIntegral seed))

We can now design a generic random test for any Encoder as follows:
rantest :: Encoder t→Bool
rantest t = and (map (rantest1 t) [0..255])
rantest1 t n = x==(visit_as t x) where

x=rannat n

visit_as t = (to nat) . (from t) . (to t) . (from nat)

Note that in rantest1, visit at starts with a random natural number from
which it generates its test data of a given type. After testing the encoder, the
result is brought back as a natural number that should be the same as the
original random number.
We can now implement our tester isotest that in a few seconds goes over
of thousands of test cases and aggregates the result with a final and:
isotest = and (map rt [0..25])
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt
rt

0 = rantest nat
1 = rantest fun
2 = rantest set
3 = rantest bits
4 = rantest funbits
5 = rantest hfs
6 = rantest hff
7 = rantest uhfs
8 = rantest uhff
9 = rantest perm
10 = rantest hfp
11 = rantest nat2
12 = rantest set2
13 = rantest clist
14 = rantest pbdd
15 = rantest bdd
16 = rantest rbdd
17 = rantest digraph
18 = rantest graph
19 = rantest mdigraph
20 = rantest mgraph
21 = rantest hypergraph
22 = rantest dyadic
23 = rantest string
24 = rantest pars
25 = rantest dna

The empirical correctness test of the “whole enchilada” follows:

∗ISO> isotest
True

suggesting that the probability of having errors in the code described so far is
extremely small.

22

Applications

Besides their utility as a uniform basis for a general purpose data conversion
library, let us point out some specific applications of our isomorphisms.
22.1

Combinatorial Generation

A free combinatorial generation algorithm (providing a constructive proof of
recursive enumerability) for a given structure is obtained simply through an
isomorphism from nat:
nth thing = as thing nat
nths thing = map (nth thing)
stream_of thing = nths thing [0..]
∗ISO> nth set 42
[1,3,5]
∗ISO> nth bits 42
[1,1,0,1,0]
∗ISO> take 3 (stream_of hfs)
[H [],H [H []],H [H [H []]]]
∗ISO> take 3 (stream_of bdd)
[BDD 0 B0,BDD 0 B1,BDD 1 (D 0 B0 B0)]

22.2

Random Generation

Combining nth with a random generator for nat provides free algorithms for
random generation of complex objects of customizable size:
ran thing seed largest = head (random_gen thing seed largest 1)
random_gen thing seed largest n = genericTake n
(nths thing (rans seed largest))
rans seed largest =
randomRs (0,largest) (mkStdGen seed)

For instance
∗ISO> random_gen set 11 999 3
[[0,2,5],[0,5,9],[0,1,5,6]]

generates a list of 3 random sets.
For instance
∗ISO>ran digraph 5 (2^31)
[(1,0),(0,1),(2,1),(1,3),(2,2),(3,2),(4,0),(4,1),
(5,1),(6,0),(6,1),(7,1),(5,3),(6,2),(6,3)]
∗ISO> ran hfs 7 30
H [H [],H [H [],H [H []]],H [H [H [H []]]]]
∗ISO> ran dnaStrand 1 123456789
DNAstrand P5x3 [Guanine,Thymine,Guanine,Cytosine,
Cytosine,Thymine,Thymine,Thymine,Thymine,
Adenine,Thymine,Cytosine,Cytosine]

generate a random digraph, a hereditarily finite set and a DNA strand.
Random generator for various data types are useful for further automating
test generators in tools like QuickCheck [7] by generating customized random
tests.
An interesting other application is generating random problems or programs
of a given type and size. For instance
∗ISO> ran sat 8 (2^31)
[[-1],[1,-1],[-1,2],[1,-1,2],[-2],[1,-2],[-1,-2],[1,-1,-2],
[2,-2],[1,2,-2],[-1,2,-2],[3],[1,-1,3],[1,-1,2,3],[1,-2,3],
[-1,-2,3],[2,-2,3],[1,2,-2,3],[-1,2,-2,3]]
∗ISO> ran clist 8 12345
Cons (Atom 0) (Cons (Cons (Atom 0) (Atom 0)) (Atom 100))

generate, respectively, a random SAT-problem and a random Cons-list.
22.3

Succinct Representations

Depending on the information theoretical density of various data representations
as well as on the constant factors involved in various data structures, significant
data compression can be achieved by choosing an alternate isomorphic representation, as shown in the following examples:
∗ISO> as hff hfs (H [H [H []],H [H [],
H [H []]],H [H [],H [H [H []]]]])
H [H [H []],H [H []],H [H []]]
∗ISO> as nat hff (H [H [H []],H [H []],H [H []]])
42
∗ISO> as fun bits [0,1,0,0,0,0,0,0,0,0,0]
[0,10]
∗ISO> as rbdd hfs (H [H [],H [H [],H [H []]],
H [H [H []],H [H [H []]]]])
BDD 3 (D 1 B1 B0)
∗ISO> as hff bdd (BDD 3 (D 2
(D 1 (D 0 B1 B0) (D 0 B0 B1))

(D 1 (D 0 B1 B1) (D 0 B1 B1))))
H [H [],H [H [],H [],H []]]

In particular, mapping to efficient arbitrary length integer implementations
(usually C-based libraries), can provide more compact representations or improved performance for isomorphic higher level data representations. Alternatively, lazy representations as provided by functional binary numbers or BDDs,
for very large integers encapsulating results of some computations might turn
out to be more effective space-wise or time-wise.
We can compare representations sharing a common datatype to conjecture
about their asymptotic information density.
22.4

Experimental Mathematics

Comparing compactness of representations For instance, after defining:
length_as t = fit genericLength (with nat t)
sum_as t = fit sum (with nat t)
size_as t = fit tsize (with nat t)

one can conjecture that finite functions are more compact than permutations
which are more compact than sets asymptotically
∗ISO>
54
∗ISO>
28
∗ISO>
54
∗ISO>
2690
∗ISO>
378
∗ISO>
43

length_as set 123456789012345678901234567890
length_as perm 123456789012345678901234567890
length_as fun 123456789012345678901234567890
sum_as set 123456789012345678901234567890
sum_as perm 123456789012345678901234567890
sum_as fun 123456789012345678901234567890

One might observe that the same trend applies also to their hereditarily finite
derivatives:
∗ISO> size_as hfs 123456789012345678901234567890
627
∗ISO> size_as hfp 123456789012345678901234567890
276
∗ISO> size_as hff 123456789012345678901234567890
91

While confirming or refuting this conjecture is beyond the scope of this paper,
the affirmative case would imply, interestingly, that “order” (permutations) has
asymptotically higher information density than “content” (sets), and explain
why finite functions (that involve both) dominate data representations in various
computing fields.

Based on the same experiment, reduced BDDs (especially if one implements
sharing, as computed by robdd size) also provide relatively compact representations:
∗ISO> bdd_size $ as bdd
nat 123456789012345678901234567890
256
∗ISO> bdd_size $ as rbdd
nat 123456789012345678901234567890
144
∗ISO> robdd_size $ as rbdd
nat 123456789012345678901234567890
39

Figures 21, 22, 23 compare the sizes of bitstring, BDD, HFF, HFS, HFP representations, first with the most succinct ones (bitstring, BDDs, HFF) grouped
together in Fig. 21, then the less succinct ones (HFS and HFP) in Fig. 22 and
finally all representations together for n in the larger interval [0..216 − 1].

Fig. 21: Comparison of curve1=Bit, curve2=BDD and curve3=HFF sizes

It is also interesting to observe the ability of some representations to express
huge numbers that normally overflow computer memory but which are genuinely
“low complexity” as a result of a small numbers of simple computational steps
that generate them.

Fig. 22: Comparison of curve1=HFS and curve1=HFP sizes

Fig. 23: Comparison of all representation sizes at a larger scale

For instance,
∗ISO> map (as nat pars)
[ "()","(())","((()))","(((())))", "((((()))))","(((((())))))"]
[0,1,2,4,16,65536]
∗ISO> as hff pars "((()))"
H [H [H []]]

shows that parenthesis sequences (structurally isomorphic to hereditarily finite
functions) can represent succinctly the fast growing but low complexity series
n
an = 22 . Clearly, terms of the series would exhaust computer memory quite
quickly using a conventional bitvector based arbitrary size integer representation! This suggest the usefulness of a universal possibly lazy “shapeshifting”
algorithm, that can decide on the most efficient data representation automatically, using size estimates, at the time when data is actually constructed.
Sparseness criteria As a first step, one can introduce a “sparseness criteria”
by comparing the size of a representation f with the size of the self-delimiting
Elias omega code.
One can obtain an encoding of such sequences by encoding its length and
then encoding each term, parametrized by a function f : N at → [N at]:
nat2self f n = (to_elias l) ++ concatMap to_elias ns where
ns = f n
l=genericLength ns
nat2sfun n = nat2self (as fun nat) n

This function is injective (but not onto!) and its action can be reversed by first
decoding the length l and then extracting self delimited sequences l times.
self2nat g ts = (g xs,ts’) where
(l,ns) = from_elias ts
(xs,ts’)=take_from_elias l ns
take_from_elias 0 ns = ([],ns)
take_from_elias k ns = ((x:xs),ns’’) where
(x,ns’)=from_elias ns
(xs,ns’’)=take_from_elias (k-1) ns’
sfun2nat ns = xs where
(xs,[])=self2nat (as nat fun) ns

We obtain the Encoder:
sfun :: Encoder [Nat]
sfun = compose (Iso sfun2nat nat2sfun) nat

working as follows:
∗ISO> as sfun nat 42
[1,0,1,0,0,0,1,0,0,1,0,0,1,0,0]

∗ISO> as nat sfun it
42

A simple concept of sparseness is derived by comparing the size of a selfdelimiting code for a number n vs. the size of its self-delimiting representation
as a finite sequence, finite set or finite permutation as shown in Fig. 24, computed
as follows:
linear_sparseness_pair t n =
(genericLength (to_elias n),genericLength (nat2self (as t nat) n))
linear_sparseness f n = x/y where (x,y)=linear_sparseness_pair f n

Fig. 24: Sparseness measures with curve1=fun, curve2=set, curve3=perm up to
27

We can also extend this comparison the hereditarily finite representations,
which, as a pleasant surprise, turn out to provide self-delimiting codes.
sparseness_pair f n =
(genericLength (to_elias n),genericLength (as f nat n))
sparseness f n = x/y where (x,y)=sparseness_pair f n

One can then compare (self-delimiting) parenthesis language representations
for hereditarily finite encoders provided by HFF, HFS, HFP and discover the
“peaks” of sparseness as shown in Fig. 25 and 26.

Fig. 25: Sparseness measures with curve1=HFF, curve2=HFS, curve3=HFP up
to 28

A new self-delimiting code While the HFF representation is generally less
compact than Elias omega code, its simplicity suggest it as a possibly useful selfdelimiting code, especially interesting for streams of “sparse” values, as shown
in Fig. 27.
One can collect values that have smaller HFF codes than Elias omega codes
i.e. “sparse numbers” with:
sparses_to m = [n | n←[0..m-1],
(genericLength (as hff_pars nat n))
<
(genericLength (as elias nat n))]

working as follows
ISO> sparses_to (2^11)
[15,16,17,24,32,64,65,96,128,129,192,256,257,258,259,320,384,
385,448,512,513,514,515,516,517,518,519,520,544,576,640,641,704,768,

Fig. 26: Sparseness measures with curve1=HFF curve2=HFS, curve3=HFP up
to 214

769,770,771,832,896,897,960,1024,1025,1026,1027,1028,1029,1030,1031,
1032,1088,1152,1280,1281,1408,1536,1537,1538,1539,1664,1792,1793,1920]

and notice that the list collects an unusually large number of various popular
memory chip and computer screen sizes. Figure 28 shows distribution of “sparse
numbers” in [0..218 ].
Primes and Pairing Functions Products of two prime numbers have the
interesting property that they are special a case where no information is lost
by multiplication in the sense of [35]. Indeed, in this case multiplication is reversible, i.e. the two factors can be recovered given the product. As the product
is comparatively easy to compute, while in case of large primes factoring is believed intractable, this property has well-known uses in cryptography. Given the
isomorphism between natural numbers and primes mapping a prime to its position in the sequence of primes, one can transport pairing/unpairing operations
to prime numbers
ppair pairingf (p1,p2) | is_prime p1 && is_prime p2 =
from_pos_in ps (pairingf (to_pos_in ps p1,to_pos_in ps p2)) where
ps = primes
punpair unpairingf p | is_prime p = (from_pos_in ps n1,from_pos_in ps n2) where

Fig. 27: Comparison of codes: curve1=Undelimited curve2=Elias, curve3=HFF
up to 27

Fig. 28: Sparse numbers in [0..218 ], x=nth sparse number, y=its value

ps=primes
(n1,n2)=unpairingf (to_pos_in ps p)

working as follows:
∗ISO> ppair bitpair (11,17)
269
∗ISO> punpair bitunpair it
(11,17)

Clearly, this defines a bijection f : P rimes×P rimes → P rimes that is tempting
to compare with the product of two primes. Figs. 29 and 30 shows the surfaces
generated by products and multiset pairings of primes. While both commutative
operations are reversible and likely to be asymptotically equivalent in terms of
information density, one can notice the much smoother transition in the case of
lossless multiplication.

Fig. 29: Lossless multiplication of primes

We have seen that recursive application of the unpairing function bitunpair
provided an isomorphisms between natural numbers and BDDs. Given an unpairing function u : N at → N at × N at and a predicate p(n) over the set of
natural numbers, it makes sense to investigate subsets of N at such that if p
holds for n then it also holds after applying the unpairing function u to n. More
interestingly, one can look at subsets for which this property holds recursively.

Fig. 30: Lossless multiset pairing of primes

Assuming a prime recognizer is prime and a generator primes for the stream
of prime numbers (see Appendix), we can define:
hyper_primes u = [n | n←primes, all_are_primes (uparts u n)] where
all_are_primes ns = and (map is_prime ns)
uparts u = sort . nub . tail . (split_with u) where
split_with _ 0 = []
split_with _ 1 = []
split_with u n = n:(split_with u n0)++(split_with u n1) where
(n0,n1)=u n

working as follows:
∗ISO> take 20 (hyper_primes bitunpair)
[2,3,5,7,11,13,17,19,23,29,31,43,47,59,71,79,83,89,103,139]
∗ISO> take 20 (hyper_primes pepis_unpair)
[2,3,5,7,11,13,19,23,29,31,43,53,59,107,127,173,223,251,311,347]

This leads to the following conjectures, in increasing order of generality:
Conjecture 1 The sets generated by (hyper primes bitpair) and (hyper primes
pepis unpair) are infinite.
Conjecture 2 If u is a bijection from u : N at → N at × N at such that:

1. if n > 1 and u n = (n0 , n1 ) then n0 < n and n1 < n
2. p is a predicate on N at such that P = {n : p(n)} is infinite
then the set P ∩ {n : uparts u n} is also infinite.
Figure 31 shows the complete unpairing graph for two hyper-primes obtained
with bitunpair.

2109167
1
1783
1

0
0

29
0

2

43

1
0
0

1

1
1

7

0
0

0
47

1

1151

1

1
7

0

0
3

0
1

1 0
1

47

3
1 0

1

Fig. 31: mset unpair hyper-primes: 1783 and 2109167

It is interesting to compare the action of pairing of natural numbers with their
action on functions on primes and hyper-primes with products. Clearly products
are not reversible, except when numbers are primes, while pairing functions are
always reversible. To factor in the fact that products commute while pairing
functions do not, we have considered 2xy instead of xy.
Figures 32 and 33 show this comparison.

Fig. 32: Pairing of primes vs. 2xy

Fig. 33: Pairing of hyper-primes vs. 2xy

Hyper-primes and Fermat primes One could expect to model more closely
the behavior of primes and products by focusing on commutative functions like
the multiset pairing function mset pair:
∗ISO> take 16 (hyper_primes mset_unpair)
[2,3,5,13,17,113,173,257,10753,17489,34897,34961,43633,43777,65537,142781101]

We remind that:
n

Definition 3 A Fermat-prime is a prime of the form 22 + 1 with n > 0.
Fig. 34 shows a hyper-prime that is also a Fermat prime and a hyper-prime that
is not a Fermat prime.

65537

34897

10

1

257

0

173

10

1

17

13

17

10

1

5

10

0

5

10

1 0

3

3
1

0

1

1
2

1

0

0
0
0

2
1

1

0
0

Fig. 34: mset unpair hyper-primes: Fermat prime and Non-Fermat prime

This time a more interesting conjecture emerges. We can now state that:
Conjecture 3 All Fermat primes are mset unpair induced hyper-primes.
We will just observe that this would follow from the widely believed conjecture
that there the only Fermat primes are [3,5,17,257,65537] as these 5 primes are
indeed on our list of mset unpair hyperprimes.
In the event of the alternative, we will now state:

Proposition 12 If there are Fermat primes other than [3,5,17,257,65537] then
there are Fermat primes that are not mset unpair hyper-primes.
To prove Prop. 12 we need a few additional results. First, the following known
fact, implying that we only need to prove that there are primes of the form
n
22 + 1 that are not hyper-primes.
Lemma 1 If n > 0 and 2n + 1 is prime then n is a power of 2.
It is easy to prove, from the definition of mset pair that:
Lemma 2

n

n

n+1

mset pair (22 + 1, 22 + 1) ≡ 22

+1

(23)

Indeed, from the identity 19 we obtain
mset pair(a, a) ≡ bitpair(a, 0)

(24)

and then observe that from 14 it follows that
n

n+1

bitpair(22 + 1, 0) ≡ 22

+1

(25)

n+1

We can now prove Prop. 34. If 22
+ 1 is a Fermat prime that is also a hypern
prime, then 22 +1 would be also a Fermat prime that is hyper-prime. This would
form a descending sequence of consecutive Fermat primes - a contradiction,
given that it has been proven (by Leonhard Euler in 1732) that for instance,
232 + 1 = 641 ∗ 6, 700, 417 is not a prime.
22.5

A surprising “free algorithm”: strange sort

A simple isomorphism like nat set can exhibit interesting properties as a building block of more intricate mappings like Ackermann’s encoding, but let’s also
note a (surprising to us) “free algorithm” – sorting a list of distinct elements
without explicit use of comparison operations:
strange_sort = (from nat_set) . (to nat_set)
∗ISO> strange_sort [2,9,3,1,5,0,7,4,8,6]
[0,1,2,3,4,5,6,7,8,9]

This algorithm emerges as a consequence of the commutativity of addition and
the unicity of the decomposition of a natural number as a sum of powers of 2.
The cognoscenti might notice that such surprises are not totally unexpected in
the world of functional programming. In a different context, they go back as
early as Wadler’s Free Theorems [36]. In a similar way, to sort sequences with
repeated elements one can write
strange_sort’ = (to mset) . (from mset)
strange_sort’’ = (as mset nat) . (as nat mset)
∗ISO> strange_sort’ [2,4,1,1,0,3,17,1.4]
[0,1,1,1,2,3,4,4,17]
∗ISO> strange_sort’’ [2,4,1,1,0,3,17,1,4]
[0,1,1,1,2,3,4,4,17]

22.6

Circuit Minimization

Let us consider the classic problem of synthesizing a half adder, composed of an
XOR (^) and an AND (*) function. We can combine the two functions with an ifthen-else with selector variable A to obtain: ITE(A,B^C,B*C) with the following
truth table:
[0,0,0]:0
[0,0,1]:0
[0,1,0]:0
[0,1,1]:1
[1,0,0]:0
[1,0,1]:1
[1,1,0]:1
[1,1,1]:0

Note that this 3 argument single output function (encoded as the natural number
22 by reading its value column in binary), fuses the two operations with the upper
half of the truth table representing the AND and the lower half representing the
XOR. When running to min bdd on this function we obtain:
ISO> from_base 2 [0,1,1,0, 1,0,0,0]
22
∗ISO> to_min_bdd 3 22
BDD 3 (D 0
(D 1 (D 2 B0 B1) (D 2 B1 B0))
(D 1 (D 2 B1 B0) B0))

22.7

Other Applications

A fairly large number of useful algorithms in fields ranging from data compression, coding theory and cryptography to compilers, circuit design and computational complexity involve bijective functions between heterogeneous data types.
Their systematic encapsulation in a generic API that coexists well with strong
typing can bring significant simplifications to various software modules with the
added benefits of reliability and easier maintenance. In a Genetic Programming
context [37] the use of isomorphisms between bitvectors/natural numbers on
one side, and trees/graphs representing HFSs, HFFs on the other side, looks
like a promising phenotype-genotype connection. Mutations and crossovers in
a data type close to the problem domain are transparently mapped to numerical domains where evaluation functions can be computed easily. In particular,
“biological proven” encodings like DNA strands are likely to provide interesting genotypes implementations. In the context of Software Transaction Memory
implementations (like Haskell’s STM [38]), encodings through isomorphisms are
subject to efficient shortcuts, as undo operations in case of transaction failure
can be performed by applying inverse transformations without the need to save
the intermediate chain of data structures involved.

23

Related work

The closest reference on encapsulating bijections as a Haskell data type is [39]
and Conal Elliott’s composable bijections module [40], where, in a more complex
setting, Arrows [41] are used as the underlying abstractions. While our Iso
data type is similar to the Bij data type in [40] and BiArrow concept of [39],
the techniques for using such isomorphisms as building blocks of an embedded
composition language centered around encodings as Natural Numbers are new.
As the domains between which we define our isomorphisms can be organized
as categories, it is likely that some of our constructs would benefit from natural
transformation [42] and n-category formulations [43].
Ranking functions can be traced back to Gödel numberings [5,6] associated to
formulae. Together with their inverse unranking functions they are also used in
combinatorial generation algorithms [44,27,45,46]. However the generic view of
such transformations as hylomorphisms obtained compositionally from simpler
isomorphisms, as described in this paper, is new.
Natural Number encodings of Hereditarily Finite Sets have triggered the
interest of researchers in fields ranging from Axiomatic Set Theory and Foundations of Logic to Complexity Theory and Combinatorics [47,48,49,50,51,52].
Computational and Data Representation aspects of Finite Set Theory have been
described in logic programming and theorem proving contexts in [12,53].
Pairing functions have been used in work on decision problems as early as
[20,23]. A typical use in the foundations of mathematics is [54]. An extensive
study of various pairing functions and their computational properties is presented in [55].
Various mappings from natural numbers to rational numbers are described
in [56], also in a functional programming framework.
We have learned from Knuth’s recent work on combinatorial algorithms [27]
the techniques related to bitvector encodings of projection functions and boolean
operations and about BDDs and reduced ordered BDDs from Bryant’s seminal
paper on the topic [26]. However, the connection with pairing/unpairing functions and the equivalence results of subsection 10.4 are new.
The concepts of hereditarily finite functions and permutations as well as their
encodings, are likely to be new, given that our sustained search efforts have not
lead so far to anything similar.
Some other techniques, ranging from factoradics to cons-lists and functional
binary numbers to DNA encodings and dyadic rationals are for sure part of
the scientific commons. In that case our focus was to express them as elegantly
ans possible in a uniform framework. In these cases as well, most of the time it
was faster to “just do it”, by implementing them from scratch in a functional
programming framework, rather than adapting procedural algorithms found elsewhere.

24

Conclusion

We have shown the expressiveness of Haskell as a metalanguage for executable
mathematics, by describing encodings for functions and finite sets in a uniform
framework as data type isomorphisms with a groupoid structure. Haskell’s higher
order functions and recursion patterns have helped the design of an embedded data transformation language. Using higher order combinators a simplified
QuickCheck style random testing mechanism has been implemented as an empirical correctness test. The framework has been extended with hylomorphisms
providing generic mechanisms for encoding Hereditarily Finite Sets and Hereditarily Finite Functions. In the process, a few surprising “free algorithms” have
emerged as well as a generalization of Ackermann’s encoding to Hereditarily Finite Sets with Urelements. We plan to explore in depth in the near future, some
of the results that are likely to be of interest in fields ranging from combinatorics and boolean logic to data compression and arbitrary precision numerical
computations.

References
1. Tarau, P.: Isomorphisms, Hylomorphisms and Hereditarily Finite Data Types in
Haskell. In: Proceedings of ACM SAC’09, Honolulu, Hawaii, ACM (March 2009)
2. Lakoff, G., Johnson, M.: Metaphors We Live By. University of Chicago Press,
Chicago, IL, USA (1980)
3. Cook, S.: Theories for complexity classes and their propositional translations. In:
Complexity of computations and proofs. (2004) 1–36
4. Cook, S., Urquhart, A.: Functional interpretations of feasibly constructive arithmetic. Annals of Pure and Applied Logic 63 (1993) 103–200
5. Gödel, K.: Über formal unentscheidbare Sätze der Principia Mathematica und
verwandter Systeme I. Monatshefte für Mathematik und Physik 38 (1931) 173–
198
6. Hartmanis, J., Baker, T.P.: On simple goedel numberings and translations. In
Loeckx, J., ed.: ICALP. Volume 14 of Lecture Notes in Computer Science., Springer
(1974) 301–316
7. Claessen, K., Hughes, J.: Testing monadic code with quickcheck. SIGPLAN Notices
37(12) (2002) 47–59
8. Singh, D., Ibrahim, A.M., Yohanna, T., Singh, J.N.: An overview of the applications of multisets. Novi Sad J. Math 52(2) (2007) 73–92
9. Hutton, G.: A Tutorial on the Universality and Expressiveness of Fold. J. Funct.
Program. 9(4) (1999) 355–372
10. Meijer, E., Hutton, G.: Bananas in Space: Extending Fold and Unfold to Exponential Types. In: FPCA. (1995) 324–333
11. Ackermann, W.F.: Die Widerspruchsfreiheit der allgemeinen Mengenlhere. Mathematische Annalen (114) (1937) 305–315
12. Piazza, C., Policriti, A.: Ackermann Encoding, Bisimulations, and OBDDs. TPLP
4(5-6) (2004) 695–718
13. Göbel, F.: On a 1-1-correspondence between rooted trees and natural numbers. J.
Comb. Theory, Ser. B 29(1) (1980) 141–143

14. Knuth, D.E.: The art of computer programming, volume 2 (3rd ed.): seminumerical
algorithms. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA
(1997)
15. Mantaci, R., Rakotondrajao, F.: A permutations representation that knows what
”eulerian” means. Discrete Mathematics & Theoretical Computer Science 4(2)
(2001) 101–108
16. Pepis, J.: Ein verfahren der mathematischen logik. The Journal of Symbolic Logic
3(2) (jun 1938) 61–76
17. Kalmar, L.: On the reduction of the decision problem. first paper. ackermann
prefix, a single binary predicate. The Journal of Symbolic Logic 4(1) (mar 1939)
1–9
18. Kalmar, Laszlo, Suranyi, Janos: On the reduction of the decision problem. The
Journal of Symbolic Logic 12(3) (sep 1947) 65–73
19. Kalmar, Laszlo, Suranyi, Janos: On the reduction of the decision problem: Third
paper. pepis prefix, a single binary predicate. The Journal of Symbolic Logic 15(3)
(sep 1950) 161–173
20. Robinson, J.: General recursive functions. Proceedings of the American Mathematical Society 1(6) (dec 1950) 703–718
21. Robinson, J.: A note on primitive recursive functions. Proceedings of the American
Mathematical Society 6(4) (aug 1955) 667–670
22. Robinson, J.: Recursive functions of one variable. Proceedings of the American
Mathematical Society 19(4) (aug 1968) 815–820
23. Robinson, J.: Finite generation of recursively enumerable sets. Proceedings of the
American Mathematical Society 19(6) (dec 1968) 1480–1486
24. Robinson, J.: An introduction to hyperarithmetical functions. The Journal of
Symbolic Logic 32(3) (sep 1967) 325–342
25. Pigeon, S.: Contributions à la compression de données. Ph.d. thesis, Université de
Montréal, Montréal (2001)
26. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE
Transactions on Computers 35(8) (1986) 677–691
27. Knuth, D.:
The Art of Computer Programming, Volume 4, draft (2006)
http://www-cs-faculty.stanford.edu/∼knuth/taocp.html.
28. Shannon, C.E.: Claude Elwood Shannon: collected papers. IEEE Press, Piscataway,
NJ, USA (1993)
29. Fujita, M., McGeer, P.C., Yang, J.C.Y.: Multi-terminal binary decision diagrams:
An efficient data structure for matrix representation. Formal Methods in System
Design 10(2/3) (1997) 149–169
30. Ciesinski, F., Baier, C., Groesser, M., Parker, D.: Generating compact MTBDDrepresentations from Probmela specifications. In: Proc. 15th International SPIN
Workshop on Model Checking of Software (SPIN’08). (2008)
31. Bucciarelli, A., Salibra, A.: The sensible graph theories of lambda calculus. In:
LICS ’04: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer
Science, Washington, DC, USA, IEEE Computer Society (2004) 276–285
32. Berline, C.: Graph models of λ-calculus at work, and variations. Mathematical.
Structures in Comp. Sci. 16(2) (2006) 185–221
33. Li, Z.: Algebraic properties of dna operations. Biosystems 52 (October 1999)
55–61(7)
34. Hinze, T., Sturm, M.: A universal functional approach to dna computing and
its experimental practicability. In: Proceedings 6th DIMACS Workshop on DNA
Based Computers, held at the University of Leiden, Leiden, The Netherlands, 13 17. (2000) 257–266

35. Pippenger, N.: The average amount of information lost in multiplication. IEEE
Transactions on Information Theory 51(2) (2005) 684–687
36. Wadler, P.: Theorems for free! In: FPCA ’89: Proceedings of the fourth international conference on Functional programming languages and computer architecture, New York, NY, USA, ACM (1989) 347–359
37. Koza, J.R.: Genetic Programming: On the Programming of Computers by Means
of Natural Selection. MIT Press, Cambridge, MA, USA (1992)
38. Harris, T., Marlow, S., Jones, S.L.P., Herlihy, M.: Composable memory transactions. Commun. ACM 51(8) (2008) 91–100
39. Alimarine, A., Smetsers, S., van Weelden, A., van Eekelen, M., Plasmeijer, R.:
There and back again: arrows for invertible programming. In: Haskell ’05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, New York, NY, USA,
ACM Press (2005) 86–97
40. Conal
Elliott:
Data.Bijections
Haskell
Module.
http://haskell.org/haskellwiki/TypeCompose.
41. Hughes, J.: Generalizing Monads to Arrows Science of Computer Programming
37, pp. 67-111, May 2000.
42. Mac Lane, S.: Categories for the Working Mathematician. Springer-Verlag, New
York, NY, USA (1998)
43. Baez, J.C.: An introduction to n-categories. In: In 7th Conference on Category
Theory and Computer Science, Springer-Verlag (1997) 1–33
44. Martinez, C., Molinero, X.: Generic algorithms for the generation of combinatorial
objects. In Rovan, B., Vojtas, P., eds.: MFCS. Volume 2747 of Lecture Notes in
Computer Science., Springer (2003) 572–581
45. Ruskey, F., Proskurowski, A.: Generating binary trees by transpositions. J. Algorithms 11 (1990) 68–84
46. Myrvold, W., Ruskey, F.: Ranking and unranking permutations in linear time.
Information Processing Letters 79 (2001) 281–284
47. Takahashi, M.o.: A Foundation of Finite Mathematics. Publ. Res. Inst. Math. Sci.
12(3) (1976) 577–708
48. Kaye, R., Wong, T.L.: On Interpretations of Arithmetic and Set Theory. Notre
Dame J. Formal Logic Volume 48(4) (2007) 497–510
49. Abian, A., Lamacchia, S.: On the consistency and independence of some settheoretical constructs. Notre Dame Journal of Formal Logic X1X(1) (1978) 155–
158
50. Avigad, J.: The Combinatorics of Propositional Provability. In: ASL Winter
Meeting, San Diego (January 1997)
51. Kirby, L.: Addition and multiplication of sets. Math. Log. Q. 53(1) (2007) 52–65
52. Leontjev, A., Sazonov, V.Y.: Capturing LOGSPACE over Hereditarily-Finite Sets.
In Schewe, K.D., Thalheim, B., eds.: FoIKS. Volume 1762 of Lecture Notes in
Computer Science., Springer (2000) 156–175
53. Paulson, L.C.: A Concrete Final Coalgebra Theorem for ZF Set Theory. In Dybjer,
P., Nordström, B., Smith, J.M., eds.: TYPES. Volume 996 of Lecture Notes in
Computer Science., Springer (1994) 120–139
54. Cégielski, P., Richard, D.: Decidability of the theory of the natural integers with
the cantor pairing function and the successor. Theor. Comput. Sci. 257(1-2) (2001)
51–77
55. Rosenberg, A.L.: Efficient pairing functions - and why you should care. International Journal of Foundations of Computer Science 14(1) (2003) 3–17
56. Gibbons, J., Lester, D., Bird, R.: Enumerating the rationals. Journal of Functional
Programming 16(4) (2006)

Appendix
The code in the paper is organized in a module with the following dependencies:
module
import
import
import
import
import
import
import
import

ISO where
Data.List
Data.Bits
Data.Graph
Data.Graph.Inductive
Graphics.Gnuplot.Simple
Data.Char
Ratio
Random

Bit crunching functions
The function bitcount computes the number of bits needed to represent an integer and max bitcount computes the maximum bitcount for a list of integers.
bitcount n = head [x | x←[1..],(2^x)>n]
max_bitcount ns = foldl max 0 (map bitcount ns)

The following function convert a number to to binary, padded with 0s, up to
maxbits.
to_maxbits maxbits n =
bs ++ (genericTake (maxbits-l)) (repeat 0) where
bs=to_base 2 n
l=genericLength bs

Primes
The following code implements factoring function to primes a primality test
(is prime) and a generator for the infinite stream of prime numbers primes.
primes = 2 : filter is_prime [3,5..]
is_prime p = [p]==to_primes p
to_primes n | n>1 = to_factors n p ps where
(p:ps) = primes
to_factors n p ps | p∗p > n = [n]
to_factors n p ps | 0==n ‘mod‘ p = p : to_factors (n ‘div‘ p)
to_factors n p ps@(hd:tl) = to_factors n hd tl

p ps

We will briefly describe here the functions used to visualize various data types
with the help of Haskell libraries providing interfaces to graphviz and gnuplot.

Multiset Operations
The following functions provide multiset analogues of the usual set operations,
under the assumption that multisets are represented as non-decreasing sequences.
msetInter
msetInter
msetInter
msetInter
msetInter
msetDif
msetDif
msetDif
msetDif
msetDif

[] _ =
_ [] =
(x:xs)
(x:xs)
(x:xs)

[]
[]
(y:ys) | x==y = (x:zs) where zs=msetInter xs ys
(y:ys) | x<y = msetInter xs (y:ys)
(y:ys) | x>y = msetInter (x:xs) ys

[] _ = []
xs [] = xs
(x:xs) (y:ys) | x==y = zs where zs=msetDif xs ys
(x:xs) (y:ys) | x<y = (x:zs) where zs=msetDif xs (y:ys)
(x:xs) (y:ys) | x>y = zs where zs=msetDif (x:xs) ys

msetSymDif xs ys = sort ((msetDif xs ys) ++ (msetDif ys xs))
msetUnion xs ys = sort ((msetDif xs ys) ++ (msetInter xs ys) ++ (msetDif ys xs))

Building a multigraph from a natural number using a function
associating to each natural number a sequence or set of natural
numbers.
fun2g ns = nat2fgs nat2fun ns
set2g ns = nat2sgs nat2set ns
perm2g ns = nat2fgs nat2perm ns
pmset2g ns = nat2fgs nat2pmset ns
bmset2g ns = nat2fgs nat2bmset ns
nat2fg f n = nat2gx fun_edge f nat2pftree n :: Gr Nat Int
nat2fgs f ns = nat2gsx fun_edge f nat2pftree ns :: Gr Nat Int
nat2sg f n = nat2gx set_edge f nat2pftree n :: Gr Nat ()
nat2sgs f ns = nat2gsx set_edge f nat2pftree ns :: Gr Nat ()
set_edge xs (a,b,i) = (lookUp a xs,lookUp b xs,())
fun_edge xs (a,b,i) = (lookUp a xs,lookUp b xs,i)
nat2gx e f g n = mkGraph vs (map (e xs) es) where
es=g f n
(xs,vs)=labeledVertices es
nat2gsx e f g ns = mkGraph vs
es=nub (concatMap (g f) ns)

(map (e xs) es)

where

(xs,vs)=labeledVertices es
labeledVertices es= (xs,vs) where
xs=fvertices es
is=[0..(length xs)-1]
vs = zip is xs
nat2pftree f n = nub (nat2pftreex f (n,n,0))
nat2pftreex f (_,n,_) = ps ++ (concatMap (nat2pftreex f) ps) where
ps = nat2pfun f (n,n,0)
nat2pfun _ (_,0,_) = []
nat2pfun f (_,n,_) | n> 0 = ps where
ps = zipWith (λx i→(n,x,i)) (f n) [0..]
fvertices ps = (sort . nub) (concatMap f ps) where
f (a,b,_) = [a,b]
lookUp n ns = i where Just i=elemIndex n ns

Building Inductive Graphs from Lists of Pairs
pairs2gr ::

[(Nat,Nat)] → Gr Nat ()

pairs2gr ps = mkGraph lvs les where
vs=to_vertices ps
lvs=zip [0..] vs
es=to_edges vs ps
les=map f es
f (x,y) = (x,y,())
to_vertices es = sort $ nub $ concat [[fst p,snd p] | p←es]
to_edges vs ps = map (f vs) ps where
f vs (x,y) = (lookUp x vs,lookUp y vs)

Generating labeled edge triplets by recursing over unpairing
functions
The following function represents a number as a set of triplets expressing branches
of decomposition with an unpairing function f, for instance, in the case of BDDs
with function bitunpair.
unpairing_edges f tt = nub (h f tt) where
h _ tt | tt<2 = []
h f n = ys where
(n0,n1)=f n
ys= (n,n0,0):(n,n1,1):
(h f n0) ++
(h f n1)

The function works as follows:
∗ISO> unpairing_edges bitunpair 42
[(42,0,0),(42,7,1),(7,3,0),(7,1,1),(3,1,0),(3,1,1)]
∗JFISO> unpairing_edges pepis_unpair 42
[(42,0,0),(42,21,1),(21,1,0),(21,5,1),(5,1,0),(5,1,1)]
∗ISO>

Generating labeled edge triplets by recursing over untupling
functions
The following function represents a number as a set of triplets expressing branches
of decomposition with an untupling function fk, for instance to tuple k.
untupling_edges f k tt = nub (h f k tt) where
h _ _ tt | tt<2 = []
h f k n = ys where
ns = f k n
ys = (zip3 (repeat n) ns [0..]) ++
(concatMap (h f k) ns)

The function works as follows:
∗ISO> untupling_edges to_tuple 3 2008
[(2008,14,0),(2008,14,1),(2008,4,2),(14,2,0),(14,1,1),(14,1,2),
(2,0,0),(2,1,1),(2,0,2),(4,0,0),(4,0,1),(4,1,2)]

Building Inductive Graphs from Unpairing and Untupling Trees
We can now turn a BDD as well as any other unpairing function generated tree
into an inductive graph, as follows:
to_unpair_graph f tt = nat2fun_graph (unpairing_edges f) tt
to_untuple_graph f k tt = nat2fun_graph (untupling_edges f k) tt
nat2fun_graph f n = mkGraph vs fs :: Gr Nat Int where
es=f n
(xs,vs)=labeledVertices es
fs=map (fun_edge xs) es

The functions work as follows:
∗ISO> to_unpair_graph bitunpair 42
0:0→[]
1:1→[]
2:3→[(1,1),(0,1)]
3:7→[(0,2),(1,1)]
4:42→[(1,3),(0,0)]
∗ISO> to_unpair_graph pepis_unpair 42

0:0→[]
1:1→[]
2:5→[(1,1),(0,1)]
3:21→[(1,2),(0,1)]
4:42→[(1,3),(0,0)]
∗ISO> to_untuple_graph to_tuple 3 2008
0:0→[]
1:1→[]
2:2→[(2,0),(1,1),(0,0)]
3:4→[(2,1),(1,0),(0,0)]
4:14→[(0,2),(2,1),(1,1)]
5:2008→[(2,3),(1,4),(0,4)]

Visualization with graphviz
gviz g = writeFile "iso.gv"
((graphviz g "" (0.0,0.0) (2,2) Portrait)++"λn")
funviz f n = gviz (nat2fg f n)
setviz f n = gviz (nat2sg f n)
pviz t n = gviz (pairs2gr (as t nat n))
uviz f tt = gviz (to_unpair_graph f tt)
tviz f k tt = gviz (to_untuple_graph f k tt)

Plotting with gnuplot
plot3d f xs ys = plotFunc3d [Title ""] [] xs ys f
cplot3d f = plot3d (curry f)
plotpairs m | m ≤ 2^8 = cplot3d bitpair ls ls where ls=[0..m-1]
plotdyadics m = plotList
[Title "Dyadics"]
(map (fromRational . (as dyadic nat)) [0..m-1])
sizes_to m t = map (size_as t) [0..m-1]
plot_hf m = plotLists [Title "Bit, BDD, HFF, HFS, and HFP sizes"]
(
[bits_to m,bsizes_to m] ++
(map (sizes_to m) [hff,hfs,hfm,hfp])
)

plot_best m = plotLists [Title "Bit, BDD and HFF and HFF’ sizes"]
(
[bits_to m,bsizes_to m] ++
(map (sizes_to m) [hff,hff’])
)
plot_worse m = plotLists [Title "HFM, HFS and HFP sizes"]
(
(map (sizes_to m) [hfm,hfs,hfp])
)
plot hf m = plotx [hf] m
plotx hfx m = plotLists [Title "HF tree size"]
(
(map (sizes_to (2^m-1)) hfx)
)
-- plots pairs
pplot f m = plotPath [] (map (to_ints . f) [0..2^m-1])
zplot f m = plotPath [] (map (to_ints . f) [-(2^m)..2^m-1])
to_ints (i,j)=(fromIntegral i,fromIntegral j)
diplot n = plotPath [] (map to_ints (as digraph nat n))
bsize_of n = robdd_size (as rbdd nat n)
bsizes_to m = map bsize_of [0..m-1]
bits_to m = map s [0..m-1] where s n = genericLength (as bits nat n)
plot_linear_sparseness m =
[(map (linear_sparseness
(map (linear_sparseness
(map (linear_sparseness
(map (linear_sparseness
(map (linear_sparseness

plot_sparseness m =
[(map (sparseness
(map (sparseness
(map (sparseness
(map (sparseness
(map (sparseness

plotLists [Title "Linear Sparseness"]
fun) [0..m-1]),
pmset) [0..m-1]),
mset) [0..m-1]),
set) [0..m-1]),
perm) [0..m-1])]

plotLists [Title "Recursive Sparseness"]
hff_pars) [0..m-1]),
hfpm_pars) [0..m-1]),
hfm_pars) [0..m-1]),
hfs_pars) [0..m-1]),
hfp_pars) [0..m-1])]

plot_sparseness1 m = plotLists

[Title "Recursive Sequence vs. Multiset Sparseness"]
[
(map (sparseness hff_pars) [0..m-1]),
(map (sparseness hfpm_pars) [0..m-1])
]
plot_sparseness2 m = plotLists [Title "Recursive Multiset Sparseness"]
[
(map (sparseness bhfm_pars) [0..m-1]),
(map (sparseness hfm_pars) [0..m-1])
]
plot_sparseness3 m = plotLists [Title "Recursive Multiset Sparseness"]
[
(map (sparseness hff_pars) [0..m-1]),
(map (sparseness hff_pars’) [0..m-1])
]

plot_sparseness4 m = plotLists
[Title "Recursive Multiset vs Multiset with Primes Sparseness"] [
(map (sparseness hfm_pars) [0..m-1]),
(map (sparseness hfpm_pars) [0..m-1])
]
plot_sparseness5 m = plotLists
[Title "Recursive Multisets vs. Sequences"] [
(map (sparseness hff_pars) [0..m-1]),
(map (sparseness hfm_pars) [0..m-1])
]
plot_selfdels m = plotLists
[Title "Self-delimiting codes: Undelimited vs. Elias vs. HFF"]
[(map (genericLength . (as bits nat)) [0..m-1]),
(map (genericLength . (as elias nat)) [0..m-1]),
(map (genericLength . (as hff_pars nat)) [0..m-1])]
plot_pairs_prods m = plotLists [Title "Pairs vs. products"]
[ms,prods] where
ms=[1..m]
pairs=map bitunpair ms
prods=map prod pairs where prod (x,y)=2∗x∗y
plot_lifted_pairs m =
plotLists [Title "Lifted pairs"]
ms=[0..m-1]
pairs=map bitunpair ms
us0=map fst pairs
us1=map snd pairs

[us0,us1] where

plot_lifted_pairs1 m =
plotLists [Title "Lifted pairs and products"]
ms=[0..m-1]
pairs=map bitunpair ms
us0=map fst pairs
us1=map snd pairs
ps=zipWith (∗) us0 us1
s0=map (^2) us0
s1=map (^2) us1
xys=map f pairs where
f (x,y) = x∗y

[ps,s0,s1,xys] where

plot_primes_prods m = plotLists [Title "Primes vs. products"]
[ps,prods] where
ms=[0..m]
ps=genericTake m primes
pairs=map bitunpair ps
prods=map prod pairs where prod (x,y)=2∗x∗y
plot_hypers_prods m = plotLists [Title "Hyper-primes vs. products"]
[ps,prods] where
ms=[0..m]
ps=genericTake m (hyper_primes bitunpair)
pairs=map bitunpair ps
prods=map prod pairs where prod (x,y)=2∗x∗y

Generated Figures
f1=gviz (nat2sg nat2set 2008)
f2=gviz (nat2fg nat2fun 2008)
f2a=gviz (nat2fg nat2mset 2008)
f3=gviz (nat2fg nat2perm 2008)
f4=gviz (nat2fg nat2perm 2009)
f5=pviz digraph 2008
f6=plotpairs 64
f7=plotdyadics 256
f8=plot_best (2^6)
f9=plot_worse (2^10)
f10=plot_hf (2^8)
f11a=plot_linear_sparseness (2^7)
f11=plot_sparseness (2^8)
f11b=plot_sparseness1 (2^8)
f11c=plot_sparseness2 (2^10)
f12=plot_sparseness (2^14)

f13=plot_sparseness (2^17)
f14=plot_selfdels (2^7)
f15=plotList [] (sparses_to (2^18))

f16=gviz (nat2fgs nat2fun [0..7])
arp24 i =468395662504823 + 205619∗23∗i
arps24 = map arp24 [0..23]
arp25 i = 6171054912832631 + 366384∗23∗i
arps25 = map arp25 [0..24]
f17 = gviz (fun2g arps24)
f17a = gviz (fun2g arps25)
f18 = gviz (fun2g [2^65+1,2^131+3])
f18a = gviz (set2g [2^65+1,2^131+3])

f19 = gviz (fun2g [0..7])
f20 = gviz (pmset2g [0..7])
f20a = gviz (bmset2g [0..7])
f21 = gviz (set2g [0..7])
f22 = gviz (perm2g [0..7])
g1 tt= uviz bitunpair tt
g2 tt= uviz pepis_unpair tt
g2’ tt= uviz pepis_unpair’ tt
g3 tt= uviz rpepis_unpair tt
isofermat=uviz mset_unpair 65537
isofermat1=uviz mset_unpair 142781101
isonfermat=uviz mset_unpair 34897
isopairs = plot_pairs_prods 256
isoprimes = plot_primes_prods 256
isohypers = plot_hypers_prods 256
isounpair1=pplot bitunpair 10
isounpair2=pplot pepis_unpair 10
isounpair3=pplot mset_unpair 10

isozunpair n=zplot zunpair n
ms2pms n = as nat pmset (as mset nat n)
pms2ms n = as nat mset (as pmset nat n)
kms2pms 0 n = n
kms2pms k n = ms2pms (kms2pms (k-1) n)
kpms2ms 0 n = n
kpms2ms k n = pms2ms (kpms2ms (k-1) n)
lms k m = [x | x←[0..2^m-1], kms2pms k x < kpms2ms k x]
xms k m = [x | x←[0..2^m-1],kms2pms k x < x]
eqms k m = [x | x←[0..2^m-1],kms2pms k x == x]
xpms k m = [x | x←[0..2^m-1],kpms2ms k x < x]
eqpms k m = [x | x←[0..2^m-1],kpms2ms k x == x]
qms k m =
[(toRational (kpms2ms k x)) - (toRational (kms2pms k x)) | x←[1..2^m-1]]
q1 k m = plotList []

(qms k m)

q2 k m = plotLists []
[map (kms2pms k) xs,map (kpms2ms k) xs] where
xs = [0..2^m-1]
mult_vs_pairing p1 p2 = (p1∗p2) % (ppair bitpair (p1,p2))
mult_vs_mset_pairing p1 p2 = (p1∗p2) % (ppair mset_pair (p1,p2))
q3 n = plotFunc3d
[Title "Prime Multiplication vs. Prime Pairing"] []
ps ps mult_vs_pairing where
ps=genericTake n primes
q4 n = plotFunc3d
[Title "Prime Multiplication vs. Prime Multiset Pairing"] []
ps ps mult_vs_mset_pairing where
ps=genericTake n primes
n4a n = plotFunc3d [Title "Multiplication"] []
ps ps (∗) where
ps=[0..2^n-1]
n4b n = plotFunc3d [Title "Multiset Pairing"] []

ps ps (curry mset_pair) where
ps=[0..2^n-1]

n4c n = plotFunc3d [Title "mprod operation"] []
ps ps (mprod) where
ps=[0..2^n-1]
n4d n = plotFunc3d [Title "pmprod’ operation"] []
ps ps (pmprod’) where
ps=[0..2^n-1]
n4e n = plotFunc3d [Title "mprod’ operation"] []
ps ps (mprod’) where
ps=[0..2^n-1]

n4f n = plotFunc3d [Title "mprod’ x y/ x ∗ y"] []
ps ps (λx y→(mprod’ x y) % (x∗y)) where
ps=[1..2^n]
expMexp k m = plotLists []
[map (λx→x^k) xs, map (λx→mexp’ x k) xs] where
xs = [0..2^m]

p4a n = plotFunc3d [Title "Prime Multiplication"] []
ps ps (∗) where
ps=genericTake n primes
p4b n = plotFunc3d [Title "Prime Multiset Pairing"] []
xs ys (curry mset_pair) where
ps=genericTake n primes
xs=ps
ys=ps
p4c n = plotFunc3d [Title "mprod on primes"] []
xs ys (mprod) where
ps=genericTake n primes
xs=ps
ys=ps
p4d n = plotFunc3d [Title "pmprod on primes"] []
xs ys (pmprod) where
ps=genericTake n primes
xs=ps
ys=ps
p4f n = plotFunc3d [Title "mprod’ x y/ x ∗ y"] []
ps ps (λx y→(mprod’ x y) % (x∗y)) where

ps=genericTake n primes
q4c n = plotFunc3d [Title "Prime Pairing"] []
ps ps (curry bitpair) where
ps=genericTake n primes
q5 n = plotLists
[Title "Prime Multiplication vs. Prime Pairing curves"]
[prods,pairs] where
us= map bitunpair [0..2^n-1]
(xs,ys) = unzip us
ps=primes
xs’=map (from_pos_in ps) xs
ys’=map (from_pos_in ps) ys
prods = zipWith (∗) xs’ ys’
us’=zip xs’ ys’
pairs= map (ppair mset_pair) us’
plot_gauss_op f m = plotFunc3d title [] zs zs (curry f) where
title=[Title "Gauss Integer operations through Pairing Functions"]
zs=[-2^m..2^m-1]
gsum m = plot_gauss_op gauss_sum m
gdif m = plot_gauss_op gauss_dif m
gprod m = plot_gauss_op gauss_prod m

