

A195691


The number of closed normal form lambda calculus terms of size n, where size(lambda x.M)=2+size(M), size(M N)=2+size(M)+size(N), and size(V)=1+i for a variable V bound by the ith enclosing lambda (corresponding to a binary encoding).


4



0, 0, 0, 0, 1, 0, 1, 1, 2, 1, 4, 4, 8, 7, 18, 23, 42, 50, 105, 153, 271, 385, 721, 1135, 1992, 3112, 5535, 9105, 15916, 26219, 45815, 77334, 135029, 229189, 399498, 685710, 1198828, 2070207, 3619677, 6286268, 11024475, 19241836, 33795365, 59197968, 104234931
(list;
graph;
refs;
listen;
history;
text;
internal format)



OFFSET

0,9


LINKS

Table of n, a(n) for n=0..44.
Wikipedia, Binary lambda calculus
John Tromp, A195691.hs


FORMULA

a(n) = N(1,0,n) with
N(q,k,0) = N(q,k,1) = 0
N(q,k,n+2) = (if k>n then 1 else 0) +
q * N(1,k+1,n) +
Sum_{i=0..n} N(0,k,i) * N(1,k,ni)


EXAMPLE

This sequence first differs from A114852 at n=10, where it excludes the two reducible terms (lambda x.x)(lambda x.x) and lambda x.(lambda x.x)x, so normal 10 = (closed 10)2 = 62 = 4.


MATHEMATICA

A[_, _, 0] = A[_, _, 1] = 0; A[q_, k_, n_] := A[q, k, n] = Boole[k > n2] + q*A[1, k+1, n2] + Sum[A[0, k, i]*A[1, k, ni2], {i, 0, n2}];
a[n_] := A[1, 0, n];
Table[a[n], {n, 0, 44}] (* JeanFrançois Alcover, May 23 2017 *)


PROG

(Haskell)
a195691 = normal True 0 where
normal qLam k n = if n<2 then 0 else
(if n2<k then 1 else 0) +
(if qLam then normal True (k+1) (n2) else 0) +
sum [normal False k i * normal True k (n2i)  i < [0..n2]]
 See link for a more efficient version.


CROSSREFS

Cf. A114851, A114852.
Cf. A224345 for another way of counting normal forms in lambdacalculus.
Sequence in context: A008312 A060723 A300622 * A074763 A099932 A175000
Adjacent sequences: A195688 A195689 A195690 * A195692 A195693 A195694


KEYWORD

nonn


AUTHOR

John Tromp, Sep 22 2011


STATUS

approved



