Computing with Hereditarily Finite Sequences

TL;DR

This paper demonstrates how hereditarily finite sequences can be represented as trees and used to perform efficient arbitrary-length integer computations within Prolog, bridging symbolic and numeric computation paradigms.

Contribution

It introduces a novel approach to represent and compute with hereditarily finite sequences using tree structures, enabling efficient symbolic arbitrary-length integer arithmetic.

Findings

Representations are isomorphic to natural numbers and combinatorial objects.

Arithmetic operations on symbolic structures are asymptotically efficient.

Prolog implementations perform comparably to bitstring-based arbitrary-length arithmetic.

Abstract

e use Prolog as a flexible meta-language to provide executable specifications of some fundamental mathematical objects and their transformations. In the process, isomorphisms are unraveled between natural numbers and combinatorial objects (rooted ordered trees representing hereditarily finite sequences and rooted ordered binary trees representing G\"odel's System {\bf T} types). This paper focuses on an application that can be seen as an unexpected "paradigm shift": we provide recursive definitions showing that the resulting representations are directly usable to perform symbolically arbitrary-length integer computations. Besides the theoretically interesting fact of "breaking the arithmetic/symbolic barrier", the arithmetic operations performed with symbolic objects like trees or types turn out to be genuinely efficient -- we derive implementations with asymptotic performance comparable to ordinary bitstring implementations of arbitrary-length integer arithmetic. The source code of the paper, organized as a literate Prolog program, is available at \url{http://logic.cse.unt.edu/tarau/research/2011/pPAR.pl}