A224345 Number of closed normal forms of size n in lambda calculus with size 0 for the variables.

1, 3, 11, 53, 323, 2359, 19877, 188591, 1981963, 22795849, 284285351, 3815293199, 54762206985, 836280215979, 13527449608779, 230894574439485, 4144741143359355, 78017419806432567, 1535903379571939981, 31550210953904250759

Offset

1,2

Links

Pierre Lescanne, Table of n, a(n) for n = 1..500

Maciej Bendkowski, K Grygiel, P Tarau, Random generation of closed simply-typed lambda-terms: a synergy between logic programming and Boltzmann samplers, arXiv preprint arXiv:1612.07682, 2016

K. Grygiel and P. Lescanne, Counting and generating lambda-terms, arXiv preprint arXiv:1210.2610 [cs.LO], 2012-2013.

Paul Tarau, On logic programming representations of lambda terms: de Bruijn indices, compression, type inference, combinatorial generation, normalization, 2015.

P. Tarau, A Logic Programming Playground for Lambda Terms, Combinators, Types and Tree-based Arithmetic Computations, arXiv preprint arXiv:1507.06944 [cs.LO], 2015.

Paul Tarau, A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms, arXiv preprint arXiv:1608.03912 [cs.PL], 2016.

Formula

a(n) = F(n,0) where F(0,m) = m, F(n+1,m) = F(n,m+1) + G(n+1,m), and G(0,m) = m, G(n+1,m) = sum(k=0..n, G(n-k,m)*F(k,m)*d(n,0) ) where d(0,i) = [i = 1], d(n+1,i) = sum(j=i..n+1, binomial(j,i)*d(n,j) + g(n+1,j) ) and g(0,i) = [i = 1], g(n+1,i) = sum(j=0..i, sum(k=0..n, g(k,j)*d(n-k,i-j) ) ).

Mathematica

F[0, m_] := m; F[n_, m_] := F[n, m] = F[n-1, m+1] + G[n, m]; G[0, m_] := m; G[n_, m_] := G[n, m] = Sum[G[n-k-1, m]*F[k, m], {k, 0, n-1}]; a[n_] := F[n, 0]; Array[a, 20] (* Jean-François Alcover, May 23 2017 *)

Prog

(Haskell)
gtab :: [[Integer]]
gtab = [0..] : [[s n m |  m <- [0..]] | n <- [1..]]
  where s n m  = let fi =  [ftab !! i !! m | i <- [0..(n-1)]]
                     gi =  [gtab !! i !! m | i <- [0..(n-1)]]
                 in foldl (+) 0 (map (uncurry (*)) (zip fi (reverse gi)))
ftab :: [[Integer]]
ftab = [0..] : [[ftab !! (n-1) !! (m+1) + gtab !! n !! m | m<-[0..]] | n<-[1..]]
f(n, m) = ftab !! n !! m

Crossrefs

Cf. A220894, A135501, A220895, A220896, A220897.

Cf. A195691 for another size of the terms.

Sequence in context: A318912 A121580 A321732 * A081367 A156171 A129093

Adjacent sequences: A224342 A224343 A224344 * A224346 A224347 A224348

Keyword

nonn

Author

Pierre Lescanne, Apr 04 2013

Status

approved