A Unified Formal Description of Arithmetic and Set Theoretical Data Types

TL;DR

This paper introduces a unified formal framework for natural numbers and hereditarily finite sets using a polymorphic approach based on bijective base-2 arithmetics, with practical implementations and algorithms.

Contribution

It presents a shared axiomatization that unifies natural numbers and finite sets through a refined type class hierarchy and efficient algorithms.

Findings

Unified axiomatization of numbers and sets

Efficient algorithms for hereditarily finite sets

Implementation in Haskell with bit operations

Abstract

We provide a "shared axiomatization" of natural numbers and hereditarily finite sets built around a polymorphic abstraction of bijective base-2 arithmetics. The "axiomatization" is described as a progressive refinement of Haskell type classes with examples of instances converging to an efficient implementation in terms of arbitrary length integers and bit operations. As an instance, we derive algorithms to perform arithmetic operations efficiently directly with hereditarily finite sets. The self-contained source code of the paper is available at http://logic.cse.unt.edu/tarau/research/2010/unified.hs .