PaperlayerView exact revision on arXiv

Source-linked AI summary

Finite $\mathbf{BM}$-algebras and fixed-point combinators

Takuma Imamura

arXiv:2610.37108v1math.LOcs.LO

TL;DR

The paper asks whether fixed-point combinators exist for the BMI-fragment and investigates the corresponding algebraic question across finite and infinite algebras. It proves that finite BM-algebras have Y-elements but that an infinite BMI-algebra need not, and derives a consequence for the variety of BM-algebras.

  • Problem

    The paper addresses whether a closed BMI-term Y satisfies Yx = x(Yx), and whether every BMI-algebra contains a corresponding Y-element.

    Source: Introduction · p. 1

  • Method

    It analyzes the fixed-point question through the structure of finite and infinite algebras for the combinatory fragments.

    Source: Introduction · p. 2

  • Results

    Every finite BM-algebra has a Y-element, while an infinite BMI-algebra exists without one; the variety of BM-algebras is not generated by finite BM-algebras.

    Source: Introduction · p. 2

  • Takeaways & Limitations

    Finite BM-algebras do not generate the variety of BM-algebras.

    Source: Introduction · p. 2

    The fixed-point combinator discussed does not satisfy the stronger YBWI fixed-point property.

    Source: §5.1 · p. 14

Abstract

from arXiv · show

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$.

Introduction

The introduction asks whether fixed-point combinators exist across BMI-algebras and whether finite BM-algebras must contain a Y-element. It answers the finite BM question affirmatively while giving an infinite BMI-algebra without a Y-element.

Introduction

  • The algebraic formulation asks whether every BMI-algebra has a Y-element, corresponding to a closed BMI-term Y with Yx = x(Yx) for a fresh variable.The introduction connects this formulation to Smullyan’s question about fixed-point combinators.Source: Introduction · pp. 1–2
  • An infinite BMI-algebra exists with no Y-element, giving a negative answer to the algebraic BMI question.The cited trace result separates Yx from x^r(Yx) for every x-free BMI-term Y and r ≥ 1 [6].Source: Introduction · p. 2
  • Every BM-algebra of cardinality at most 12 has a Y-element, and exhaustive searches found most examined BM- and BMI-algebras had simple structures forcing one.These observations motivate the question of whether every finite BM-algebra has a Y-element.Source: Introduction · p. 2
  • Every finite BM-algebra has a Y-element, answering the finite analogue of the fixed-point question.The paper also concludes that the variety of BM-algebras is not generated by finite BM-algebras.Source: Introduction · p. 2
  • Finite BMI-algebras are characterized as finite idempotent semigroups with distinguished left units B, M, and I, and each has a Y-element.The introduction also reports the analogous finite BI characterization using B and I as distinguished left units.Source: Introduction · p. 2
  • The paper studies finite BM-algebras by constructing a finite BI-algebra quotient and showing that each left translation’s eventual image equals its fixed-point set.It then uses non-standard fixed-point combinators to establish the finite BM result.Source: Introduction · p. 2

1. Preliminaries

The preliminaries set conventions for application and reduction, define term powers, and describe the free algebras and interpretation used later.

1. Preliminaries

  • Application and magma multiplication are left-associative, and the operation symbol is omitted unless needed for clarity.Thus uvw means ((uv)w), and u ∗ v ∗ w means (u ∗ v) ∗ w.Source: §1 · p. 3
  • Term and magma powers are defined recursively by repeated left-nested application of the base operation.The term recursion is t^(n+1)u = t(t^n u).Source: §1 · p. 3
  • Terms modulo weak equivalence form the free BMI-algebra or BM-algebra on variable symbols, and closed terms with algebra elements as constants are interpreted in the algebra.The preliminaries distinguish one-step weak reduction, its reflexive-transitive closure, and its equivalence closure.Source: §1 · p. 3

2. An infinite BMI–algebra without Y

Section 2 presents the infinite BMI-algebra ABMI, which has no Y-element, and recalls the trace construction used to study it.

2. An infinite BMI–algebra without Y

  • The infinite BMI-algebra ABMI provides an example with no Y-element.The section recalls ABMI and the homomorphism Trx from BMI-terms into it.Source: §2 · p. 3, §2.1 · p. 3

2.1. Definition of the BMI–algebra ABMI.

  • The trace construction uses tail-equivalence classes of sequences and shift operators that preserve tail equivalence.The resulting maps act on the quotient of (N × N)^N by tail equivalence.Source: §2.1 · p. 3
  • For terms without a weak normal form, the x-trace is formed from the successive contractions of M in the unique leftmost-innermost reduction sequence.Its coordinates count x occurrences before the contracted M and within the associated Ai term.Source: §2.1 · p. 4

⋆x : ABMI × ABMI →ABMI

The trace operation makes ABMI a BMI-algebra and supports the proof that it has no Y-element. The proof gives a stronger obstruction by restricting the witness to x or ω.

⋆x : ABMI × ABMI →ABMI

  • The trace map preserves application as ⋆x and is invariant under weak equivalence, so it factors through terms modulo weak equivalence.The paper describes such a homomorphism into a BMI-algebra as an invariant for the BMI-fragment.Source: ⋆x : ABMI × ABMI →ABMI · p. 4

2.2. Absence of Y–elements.

  • The proof reduces the obstruction to checking whether a candidate Y yields fixed points at Trx(MM) and x simultaneously.The trace of MM supplies the element ω used in the witness argument.Source: §2.2 · p. 5
  • For every r ≥ 1 and every Y in ABMI, some a satisfies Y ⋆x a ≠ a^r ⋆x (Y ⋆x a), so ABMI has no Y-element.The witness a can be chosen from {x, ω}; ABMI has cardinality 2^ℵ0.Source: §2.2 · p. 5
  • For every infinite cardinality κ, there is a BMI-algebra of cardinality κ with no Y-element.This follows from Proposition 2.11 and the Löwenheim–Skolem theorem.Source: §2.2 · p. 6

3. Finite BMI–algebras

This section characterizes finite BMI-algebras through semigroup structure, building on the corresponding characterization of finite BI-algebras. The BMI characterization yields a Y-element in every finite BMI-algebra and rules out finite BMI homomorphisms that uniformly separate all fixed-point equations.

3.1. Finite BI–algebras as semigroups.

  • Every finite BI-algebra is precisely a finite semigroup with B and I as specified left units.Conversely, a semigroup with those left units forms a BI-algebra.Source: §3.1 · pp. 6–7

3.2. Finite BMI–algebras as idempotent semigroups.

  • Every finite BMI-algebra is precisely a finite idempotent semigroup with B, M, and I as specified left units.The converse also holds: any idempotent semigroup with those left units forms a BMI-algebra.Source: §3.2 · p. 7
  • Every finite BMI-algebra has a Y-element.A left unit Y satisfies the Y-element equation because the semigroup is idempotent.Source: §3.2 · p. 7
  • Finite-valued invariants cannot establish the absence of a fixed-point combinator.The section identifies this as a consequence of the finite BMI-algebra results.Source: §3.2 · p. 7
  • No finite BMI-algebra and homomorphism can distinguish Yx from x(Yx) for every closed Y and variable x.Thus no such finite-valued homomorphic interpretation separates all these equations at once.Source: §3.2 · p. 7

4. Finite BM–algebras

Finite BM-algebras need not be idempotent or associative, yet every finite BM-algebra has a Y-element.

4. Finite BM–algebras.

  • A finite BM-algebra can be neither idempotent nor associative.The paper gives a three-element example.Source: §4 · p. 8

4.1. Left ideals A∞of B–algebras.

  • For finite B-algebras, A∞ is an idempotent left ideal containing every left translation’s eventual image.In the finite case, A∞A∞ = A∞.Source: §4.1 · pp. 8–9

4.2. Extensional equivalence.

  • For finite B-algebras, extensional equivalence relative to A∞ is a congruence on A∞, and every equivalence class has a representative in A∞.For finite B-algebras, all of ∼1, ∼2, … are equivalent to each other.Source: §4.2 · p. 10

4.3. Quotient algebra A∞/∼.

  • The quotient Q = A∞/∼ is a semigroup with B- and I-elements, and β acts as the identity on Q.In finite BM-algebras, each left translation’s eventual image is precisely its set of fixed points.Source: §4.3 · pp. 11–12

4.4. Non-standard fixed-point combinators.

  • Every finite BM-algebra has a Y-element, and any non-standard fixed-point combinator interprets as one.The argument uses stabilisers and the result that each left translation’s eventual image is precisely its set of fixed points.Source: §4.3 · p. 12, §4.4 · p. 13
  • The proof requires an infinite-valued invariant to distinguish non-standard fixed-point combinators from true ones.Source: §4.4 · p. 13
  • The variety of BM-algebras is not generated by the class of finite BM-algebras.Here, generation means closure under direct products, subalgebras, and homomorphic images.Source: §4.4 · p. 13

5. Related open problems

The paper leaves open how reduction-rule structure relates to fixed-point combinators, including Turing-type combinators. Its examples show that absence of permutative effects alone does not settle the question.

5.1. Permutative effects.

  • The absence of permutative effects does not explain fixed-point-combinator absence: W has none, yet the BWI-fragment has a fixed-point combinator.That BWI combinator does not satisfy the stronger reduction Y_BWI x →* x(Y_BWI x).Source: §5.1 · p. 14
  • Open questions ask which reduction-rule properties govern fixed-point-combinator existence, including what distinguishes M from W and whether labelled trees reveal a root cause.Source: §5.1 · pp. 14–15

5.2. Turing-type fixed-point combinators.

  • The paper asks whether the BWI-fragment has a Turing-type fixed-point combinator and whether every partially ordered BWI-algebra has a Θ-element.The general question also asks whether absence of permutative effects rules out Turing-type combinators.Source: §5.2 · pp. 15–16

Appendix A. Code availability

The paper provides code for reproducing one observation and describes the finite-magma search tool, while noting that its results do not depend on computational experiments.

Appendix A. Code availability

  • Source code for reproducing Observation 0.6 is available at the magma-search repository.Source: Appendix A · p. 17
  • magma-search searches finite magmas by exhaustive isomorphism-class enumeration or a parallel SAT solver.It can test specified equations and output an example when one exists.Source: Appendix A · p. 17
  • The paper’s results do not depend on computational experiments; Observation 0.6 follows independently from Corollary 4.23.Source: Appendix A · p. 17
Loading 2610.37108v1…