login
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 i-th enclosing lambda (corresponding to a binary encoding).
6

%I #28 May 23 2017 06:21:21

%S 0,0,0,0,1,0,1,1,2,1,4,4,8,7,18,23,42,50,105,153,271,385,721,1135,

%T 1992,3112,5535,9105,15916,26219,45815,77334,135029,229189,399498,

%U 685710,1198828,2070207,3619677,6286268,11024475,19241836,33795365,59197968,104234931

%N 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 i-th enclosing lambda (corresponding to a binary encoding).

%H Wikipedia, <a href="http://en.wikipedia.org/wiki/Binary_lambda_calculus">Binary lambda calculus</a>

%H John Tromp, <a href="/A195691/a195691.hs.txt">A195691.hs</a>

%F a(n) = N(1,0,n) with

%F N(q,k,0) = N(q,k,1) = 0

%F N(q,k,n+2) = (if k>n then 1 else 0) +

%F q * N(1,k+1,n) +

%F Sum_{i=0..n} N(0,k,i) * N(1,k,n-i)

%e 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 = 6-2 = 4.

%t A[_, _, 0] = A[_, _, 1] = 0; A[q_, k_, n_] := A[q, k, n] = Boole[k > n-2] + q*A[1, k+1, n-2] + Sum[A[0, k, i]*A[1, k, n-i-2], {i, 0, n-2}];

%t a[n_] := A[1, 0, n];

%t Table[a[n], {n, 0, 44}] (* _Jean-François Alcover_, May 23 2017 *)

%o (Haskell)

%o a195691 = normal True 0 where

%o normal qLam k n = if n<2 then 0 else

%o (if n-2<k then 1 else 0) +

%o (if qLam then normal True (k+1) (n-2) else 0) +

%o sum [normal False k i * normal True k (n-2-i) | i <- [0..n-2]]

%o -- See link for a more efficient version.

%Y Cf. A114851, A114852.

%Y Cf. A224345 for another way of counting normal forms in lambda-calculus.

%K nonn

%O 0,9

%A _John Tromp_, Sep 22 2011