A333479 -id:A333479

Search: a333479 -id:a333479

Displaying 1-2 of 2 results found.

page 1

A333958

The number of closed lambda calculus terms of size n that have a normal form, where size(lambda M)=2+size(M), size(M N)=2+size(M)+size(N), and size(V)=1+i for a variable V bound by the i-th enclosing lambda.

+10
1

0, 0, 0, 1, 0, 1, 1, 2, 1, 6, 5, 13, 14, 37, 44, 101, 134, 297, 431, 882, 1361, 2729, 4404, 8548, 14310, 27397, 47095, 89014, 156049, 292954, 521639, 975319, 1757422, 3277997, 5960021, 11109379

(list; graph; refs; listen; history; text; internal format)

OFFSET

1,8

COMMENTS

This sequence is uncomputable, like the corresponding Busy Beaver sequence A333479, which takes the maximum normal form size of the a(n) terms that have one.

LINKS

Table of n, a(n) for n=1..36.

Computed by changing "maximum $ (n,0,P Bot) :" in the main function of this Haskell program for analyzing Busy Beaver numbers to "length".

EXAMPLE

This sequence first differs from A114852 at n=18 where it excludes the shortest term without a normal form (lambda x. x x)(lambda x. x x), hence a(18) = 298-1 = 297.

CROSSREFS

Cf. A114852, A195691, A333479, A004147.

KEYWORD

nonn,more

AUTHOR

John Tromp, Apr 22 2020

STATUS

approved

A361211

Busy Beaver for the Binary Lambda Calculus (BLC) language BBλ2: the maximum output size of self-delimiting BLC programs of size n, or 0 if no program of size n exists.

+10
1

0, 0, 0, 0, 0, 4, 0, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 22, 24, 26, 30, 42, 52, 44, 64, 223, 160

(list; graph; refs; listen; history; text; internal format)

OFFSET

1,6

COMMENTS

Self-delimiting BLC programs are inputs p to the BLC universal machine U (defined in first link) that make U read all bits of p and none beyond. Formally, the only prefix p' of p for which U(p':Omega) has a normal form is p itself. The output of p is that normal form.

This Busy Beaver is directly related to Kolmogorov Complexity: a(n) = max {size(x)| KP(x) = n }, where KP is the prefix Kolmogorov complexity (defined in first link).

Because programs for U are at most a constant number of bits longer than programs for any prefix-free programming language, this busy beaver is optimal: for any other busy beaver BB based on self-delimiting programs, there is a constant c such that a(c+n) >= BB(n).

In particular, a(2+n) >= A333479(n), since for every closed term T, U(00 code(T) : Omega) = (lambda _. T) Omega = T. All entries above except for n=30 are of this form.

We can show that for some k, a(ceiling((113/114)*n) + k) > A333479(n), i.e., universality eventually pays off for BLC. See program link for the supporting computation. - Bertram Felgenhauer, Apr 10 2023

LINKS

Table of n, a(n) for n=1..32.

John Tromp, Binary Lambda Calculus

John Tromp, Haskell program to compute initial terms

John Tromp, program demonstrating BLC compressibility

EXAMPLE

The smallest closed lambda term is lambda x.x but its application to the unsolvable Omega lacks a normal form. The next smallest is lambda x.lambda y.y with encoding 000010 of size 6, which applied to Omega yields the normal form lambda x.x, giving a(6)=4.

a(30) = 64 because, with T=lambda x.lambda y.lambda z.x(z x), (lambda x.x x) T applied to Omega yields maximum size normal form lambda x.lambda y.lambda z.x T(z (x T)).