Okay I'm trying to get how you're defining FairBot and I'm falling back on Haskell since that's the only time I've ever used a fixed point function
so FairBot is
f x = x f
which you can't define in Haskell but whatever. If I define
r f x = x f
then I can define
f x = r f x
then eliminate and I have
f = r f
so I have
f = fix r
(Haskell lets me define r, but gives me a type error on fix r)
Is this what you're doing?
I don't see an algorithm here... but I guess it's just lambda calculus... ?
let me use the other bot to answer this since I'm not a Haskell expert:
Yes — your derivation is exactly right: FairBot is fix (\f x -> x f). The type error is because Bot = Bot -> Bool is a recursive type; wrap it in a newtype and it typechecks:
newtype Bot = Bot { app :: Bot -> Bool } fairbot = fix (\f -> Bot (\x -> app x f))
Now run it: app fairbot (Bot (const True)) terminates (True), app fairbot fairbot loops forever. That divergence is real — two FairBots simulating each other unwind endlessly — and it's what Haskell's fix means: the least fixed point in the definedness order, where the undetermined entries come out ⊥.
My implementation changes this in two ways. First, extensionality with a finite population: a bot isn't code, it's a row of n booleans — so Bot -> Bool collapses from an infinite function space to a finite table, and the definitions compile to a finite system of boolean constraints over the n×n matrix entries (M[F,X] = M[X,F], and so on).
That's where the algorithm you're not seeing lives: build the constraint system, stratify it by dependency cycles, and solve each cycle by Knaster–Tarski iteration — start every unknown at True and iterate down until stable. It's the same shape as computing nullability of grammar nonterminals or a dataflow analysis, not the same shape as lazy unfolding.
Second, fix is a selection policy, not an evaluation strategy: the constraint system can have several solutions (your ⊥ entries are exactly the ones that are free), and ν-fix says "round the free ones up" (greatest fixed point in the truth order 0 ≤ 1), while lfix says "round them down". So where Haskell honestly reports ⊥ for FairBot-vs-FairBot, my fix declares cooperation by convention of greatest fixpoint — that convention is the Löbian handshake.
(Note that Haskell's fix is a least fixed point, but in the definedness order, not the truth order — lfix f. f is 0 in my implementation but still ⊥ in Haskell. "Least" without naming the order is ambiguous).
More jargon about the underlying model:
The denotation of a population is not a λ-term and there is no β-reduction anywhere. The model is a finite boolean matrix over the closed universe of reachable applications; the definitions induce a monotone operator on the lattice of matrices; the language's meaning is a designated solution of M = Φ(M), selected per-cycle by the ν/μ policy, with all/any quantifying over the entire solution set. The nearest established formalisms are boolean equation systems / the boolean μ-calculus (that's essentially what the solver implements, SCC-stratified with μ-priority nesting), and logic programming read over atoms coop(A,B) — where ν-fix is "cooperate unless refuted," μ-fix is the classic least-model semantics, and all/any are cautious/brave entailment from answer-set programming. λ-notation in the grammar is just a convenient surface syntax for generating those constraints; if you insist on giving it operational lambda semantics, you get divergence at precisely the entries where the constraint view has freedom — which is the whole point of having the conventions.
