Pairing Functions, Boolean Evaluation and Binary Decision Diagrams in Prolog

A pairing function J associates a unique natural number z to any two natural numbers x,y such that for two unpairing functions K and L, the equalities K(J(x,y))=x, L(J(x,y))=y and J(K(z),L(z))=z hold. Using pairing functions on natural number representations of truth tables, we derive an encoding for Binary Decision Diagrams with the unique property that its boolean evaluation faithfully mimics its structural conversion to a a natural number through recursive application of a matching pairing function. We then use this result to derive {em ranking} and {em unranking} functions for BDDs and reduced BDDs. The paper is organized as a self-contained literate Prolog program, available at http://logic.csci.unt.edu/tarau/research/2008/pBDD.zip Keywords: logic programming and computational mathematics, pairing/unpairing functions, encodings of boolean functions, binary decision diagrams, natural number representations of truth tables

A Functional Hitchhikers Guide to Hereditarily Finite Sets, Ackermann Encodings and Pairing Functions

The paper is organized as a self-contained literate Haskell program that implements elements of an executable finite set theory with focus on combinatorial generation and arithmetic encodings. The code, tested under GHC 6.6.1, is available at http://logic.csci.unt.edu/tarau/research/2008/fSET.zip . We introduce ranking and unranking functions generalizing Ackermanns encoding to the universe of Hereditarily Finite Sets with Urelements. Then we build a lazy enumerator for Hereditarily Finite Sets with Urelements that matches the unranking function provided by the inverse of Ackermanns encoding and we describe functors between them resulting in arithmetic encodings for powersets, hypergraphs, ordinals and choice functions. After implementing a digraph representation of Hereditarily Finite Sets we define {em decoration functions} that can recover well-founded sets from encodings of their associated acyclic digraphs. We conclude with an encoding of arbitrary digraphs and discuss a concept of duality induced by the set membership relation. Keywords: hereditarily finite sets, ranking and unranking functions, executable set theory, arithmetic encodings, Haskell data representations, functional programming and computational mathematics

Ranking and Unranking of Hereditarily Finite Functions and Permutations

Prologs ability to return multiple answers on backtracking provides an elegant mechanism to derive reversible encodings of combinatorial objects as Natural Numbers i.e. {em ranking} and {em unranking} functions. Starting from a generalization of Ackermans encoding of Hereditarily Finite Sets with Urelements and a novel tupling/untupling operation, we derive encodings for Finite Functions and use them as building blocks for an executable theory of {em Hereditarily Finite Functions}. The more difficult problem of {em ranking} and {em unranking} {em Hereditarily Finite Permutations} is then tackled using Lehmer codes and factoradics. The paper is organized as a self-contained literate Prolog program available at url{http://logic.csci.unt.edu/tarau/research/2008/pHFF.zip}