Mockingbird lattices

TL;DR

This paper explores the combinatorial and order-theoretic structures generated by the Mockingbird combinator in combinatory logic, revealing lattice structures within its rewrite graph and providing enumeration methods for these lattices.

Contribution

It establishes that the rewrite relation forms a partial order with lattice structures and introduces enumeration techniques using formal power series.

Findings

The rewrite relation on the Mockingbird combinator forms a partial order.

Connected components of the rewrite graph are lattices.

Enumeration of elements and intervals using formal power series.

Abstract

We study combinatorial and order theoretic structures arising from the fragment of combinatory logic spanned by the basic combinator ${\bf M}$. This basic combinator, named as the Mockingbird by Smullyan, is defined by the rewrite rule ${\bf M} x_1 \to x_1 x_1$. We prove that the reflexive and transitive closure of this rewrite relation is a partial order on terms on ${\bf M}$ and that all connected components of its rewrite graph are Hasse diagrams of lattices. This last result is based on the introduction of lattices on some forests. We enumerate the elements, the edges of the Hasse diagrams, and the intervals of these lattices with the help of formal power series on terms and on forests.