Talk:Closed lambda term

Open question. What is the smallest complete closed λ-term in terms of Fokker size? It is at least three and at most seven.

Why three is the low boundary and not four? It's known that complete basis must include a combinator of rank 3. It's also known that complete basis must include duplicative combinator (i.e. a combinator with at least one application inside). 3 abstractions plus 1 application = Fokker size is at least 4, isn't it? --Blashyrkh (talk) 10:14, 16 January 2026 (UTC)

Your reasoning is solid. I was writing conservatively but I think that you are correct. Let me think over it a bit more before I edit the page. Thanks for pointing this out! Corbin (talk) 17:51, 16 January 2026 (UTC)

If you find me wrong, please let me know. I'm really curious to see a counter-example. --Blashyrkh (talk) 18:02, 16 January 2026 (UTC)

One more Fokker size seven complete combinator

That's indeed a variation of Tromp's Alpha, with x and y arguments swapped:

γ x y z = y z (x (K z))

K = γ(γ(γ(γγ)(γγ)γ)(γγγ(γγ))γ)γ
S = γγγ(γγ(γγ)γ)γ(γ(γ(γγ(γ(γ(γγ)(γγ))))))

So, there are at least three complete combinators of Fokker size seven: Alpha, Beta, and Gamma. Beta and Gamma are found by brute force search. --Blashyrkh (talk) 00:18, 5 July 2026 (UTC)

Proof(?) that Fokker size seven is the minimum

I tried searching for a complete closed lambda term of size six or smaller, and I might have a proof that none exist? Not sure, I haven't had anyone else look at it yet. I looked at Statman (2005) first to see what exactly the restriction was more precisely. The fact that closed lambda terms that can be expressed as HOT combinations are incomplete is useful, however I don't know how or even if it's possible to tell in general (e.g. a non-trivial example is \x. \y. \z. z (x y), since even though it has a rank of three, it can be expressed as \x. \y. T (x y)). However, it's still useful to find easily-checkable subsets. In particular, any lambda term where only two unique variables are used can be expressed as a HOT combination. Take for example \x. \_. x (\y. y (\_. y x)):

\x. \_. x (\y. y (\_. y x))
\x. K (x (\y. y (K (y x))))
\x. K (x ((\x1. \y. y (K (y x1))) x))

K a b = a
A1 a b = b (K (b a))
A2 a b = K (b (A1 b))

A2 K = \x. \_. x (\y. y (\_. y x))

Combining this with the requirement that a complete lambda term must be able to make duplicative (i.e. at least one variable must be used twice) and cancellative (i.e. at least one variable must not be used) combinators, I ran the script and it showed zero terms of Fokker size 6 or less. I think I can intuitively see why. The way to fulfill these conditions while minimizing the amount of total variable occurrences is to use four variables; two variables once, one variable twice, and one variable zero times. That requires four abstractions and three compositions, which already totals to seven. I'll also put my script here in case there are any errors in it:

import functools, itertools

@functools.cache
def enumerate_terms(size, depth=0):
    if size == 0:
        return tuple(range(depth))
    x = [(term,) for term in enumerate_terms(size-1, depth+1)]
    for i in range(size):
        x += itertools.product(enumerate_terms(i, depth), enumerate_terms(size-i-1, depth))
    return tuple(x)

def count_term(term, names=(), name_counter=None):
    if name_counter is None:
        name_counter = {}
    if isinstance(term, int):
        name_counter[names[~term]] += 1
    elif len(term) == 1:
        name_counter[new_name := len(name_counter)] = 0
        count_term(term[0], (*names, new_name), name_counter)
    else:
        count_term(term[0], names, name_counter)
        count_term(term[1], names, name_counter)
    return name_counter

def easily_incomplete(term):
    def hot_check(term):
        name_counts = count_term(term)
        return len([i for i in name_counts.values() if i]) <= 2
    def affine_check(term):
        name_counts = count_term(term)
        return all([i <= 1 for i in name_counts.values()])
    def non_cancellative_check(term):
        name_counts = count_term(term)
        return all([i >= 1 for i in name_counts.values()])
    return hot_check(term) or affine_check(term) or non_cancellative_check(term)

for i in range(7):
    holdouts = [term for term in enumerate_terms(i) if not easily_incomplete(term)]
    print(f"{len(holdouts)} holdouts of size {i}")

I also have a list of 2060 "holdouts" for size 7 after adding a few more checks, but I haven't tried reducing the list any further since then. I'll see if I can think of any more checks I can add. –PkmnQ (talk) 10:33, 6 July 2026 (UTC)

But what if we use one variable twice, one variable once and two variables zero times? Say, \x. \y. \z. x z (\w. z). It has 4 abstractions and 2 applications, Fokker size is 6. Why don't you consider it a candidate? --Blashyrkh (talk) 14:18, 6 July 2026 (UTC)

That would fall under hot_check, since it only uses two distinct variables. Using the same transformation as above: –PkmnQ (talk) 15:29, 6 July 2026 (UTC)

\x. \_. \z. x z (\_. z)
\x. K (\z. x z (K z))
\x. K ((\x1. \z. x1 z (K z)) x)

K a b = a
A1 a b = a b (K b)
A2 a b = K (A1 b)

A2 K = \x. \y. \z. x z (\w. z)

May you demonstrate it on \x. \y. \z. x (\w. z z)? --Blashyrkh (talk) 19:10, 6 July 2026 (UTC)

Sure:

\x. \_. \z. x (\_. z z)
\x. K (\z. x (K (z z)))
\x. K ((\x1. \z. x1 (K (z z))) x)

K a b = a
A1 a b = a (K (b b))
A2 a b = K (A1 b)

A2 K = \x. \y. \z. x (\w. z z)

I should maybe write code to do it automatically, but I can do it manually for now. –PkmnQ (talk) 13:58, 7 July 2026 (UTC)

My list of size-7 candidates contains 180 items:

- ABC(KD)

- AB(KD)C

- A(KD)BC

- A(BC)(KD)

- A(B(KD))C

- AB(C(KD))

- A(KD)(BC)

- A(BC(KD))

- A(B(KD)C)

- A(B(C(KD)))

where A,B,C,D ∈ {x,y,z}, A!=B!=C.

Currently about 33% are checked. "Checked" means "expressions of length up to 20 reduced and results are matched against the list of targets which includes B,C,K,S,W and many others". Three complete + one funny are found so far. --Blashyrkh (talk) 13:36, 6 July 2026 (UTC)

180 items is the recent narrowing of the list which was 10598 items initially (and two - Alpha and Beta - were found from that list, then I decided to narrow the search). --Blashyrkh (talk) 13:44, 6 July 2026 (UTC)