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

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

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,n-i)

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

Mathematica

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}];
a[n_] := A[1, 0, n];
Table[a[n], {n, 0, 44}] (* Jean-François Alcover, May 23 2017 *)

Prog

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

Crossrefs

Cf. A114851, A114852.

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

Sequence in context: A345442 A060723 A300622 * A074763 A099932 A175000

Adjacent sequences: A195688 A195689 A195690 * A195692 A195693 A195694

Keyword

nonn

Author

John Tromp, Sep 22 2011

Status

approved