Six Ways to Implement Divisibility by Three in miniKanren

TL;DR

The paper investigates six ways to implement the relation $n \equiv 0 \pmod{3}$ in miniKanren using unary Oleg numerals, ranging from brute-force arithmetic to DFA-based and bit-difference approaches. It demonstrates that a finite ground set cannot capture all multiples of three and introduces a framework for comparing relational implementations, including an intrinsic reach metric that reflects non-ground solutions. The contributions include a detailed empirical study of termination, speed, and solution reach across implementations, plus practical guidance on selecting canonical div3o strategies and converting automata constructs to miniKanren code. By linking hardware-style bit tricks with relational programming techniques, the work offers actionable insights for miniKanren programmers on performance tuning and method selection.

Abstract

This paper explores options for implementing the relation $n \equiv 0 \ (\text{mod} \ 3)$ within miniKanren using miniKanren numbers and its arithmetic suite. We examine different approaches starting from straightforward implementations to more optimized versions. The implementations discussed include brute-force arithmetic methods, divisibility tricks, and derivation from a finite automaton. Our contributions include an in-depth look at the process of implementing a miniKanren relation and observations on benchmarking \texttt{defrel}s. This study aims to provide practical insights for miniKanren programmers on both performance and implementation techniques.

Figures (16)

• Figure 1: The poso relation.
• Figure 2: The definitions of olego, which unifies its argument to a ground Oleg number.
• Figure 3: The div2o relation and a query for all solutions.
• Figure 4: Two div3o implementations that use relational multiplication.
• Figure 5: Two more div3o implementations that use relational addition.

Theorems & Definitions (2)

• lemma 1
• proof