Finite bm-algebras always contain special fixed-point elements
Finite $\mathbf{BM}$-algebras and fixed-point combinators
Logic in Computer Science
Summary
The paper explores mathematical structures called BM-algebras used in logic and computer science. It finds that every finite BM-algebra has a special element that acts like a fixed point, meaning it repeats its own behavior when combined with others. The authors also show that this property doesn’t hold for some infinite versions of these algebras. Additionally, they describe how these algebras relate to known algebraic structures called semigroups with special units.
What this means in practice
- •For programming language designers: Understand the limitations and properties of finite algebraic models for fixed-point operators used in functional programming languages.
- •For formal methods engineers: Leverage algebraic characterizations of fixed points to improve verification tools that reason about recursion and self-application.
A theory result. No direct application yet.
Authors
Takuma Imamura
Abstract
We study algebras for the $\mathbf{BM}$-, $\mathbf{BI}$-, and $\mathbf{BMI}$-fragments of combinatory logic, where $\mathbf{B} xyz \to_{w} x\left(yz\right)$, $\mathbf{M} x \to_{w} xx$ and $\mathbf{I} x \to_{w} x$. We prove that every finite $\mathbf{BM}$-algebra $\mathcal{A}$ contains an element $Y$ satisfying $Yx = x\left(Yx\right)$ for all $x\in A$. Moreover, a single closed $\mathbf{BM}$-term represents such an element in every finite $\mathbf{BM}$-algebra. On the other hand, we show that there exists an infinite $\mathbf{BMI}$-algebra with no such element. Consequently, the variety of $\mathbf{BM}$-algebras is not generated by finite $\mathbf{BM}$-algebras. We also characterise finite $\mathbf{BI}$-algebras as finite semigroups with two distinguished left units $B$ and $I$, and finite $\mathbf{BMI}$-algebras as finite idempotent semigroups with three distinguished left units $B$, $M$ and $I$.