<p>Due to the highly context-sensitive nature of typed lambda calculus I would be surprised if there were an efficient algorithm, or rather a "natural" efficient algorithm.</p>

<p><a href="http://arxiv.org/abs/1210.2610" rel="nofollow">This paper</a> has nice formulae for counting <em>untyped</em> lambda terms and from that they derive a fairly simple function for enumerating untyped terms. They also provide a counting function for normal forms which should be easy to adapt to a generating function too. Unfortunately, they only make a typed generator function by filtering that which is absurdly expensive (one of the results of the paper is just how absurd it is).</p>

<p>As for a more efficient way to generate typed terms, my advice would be to generate <em>typing derivations</em> instead of terms and then type checking them.</p>
What is a mapping between natural numbers and valid simply typed lambda calculus terms?
<p>Is there any efficient algorithm that maps between well-typed, closed terms of the simply typed lambda calculus and natural numbers? For example, using bruijn indexes (and probably on incorrect order):</p>

<pre><code>0 → (λ 0)
1 → (λ (λ (0 1)))
2 → (λ (λ (1 0)))
3 → (λ 0 (λ 0))
4 → (λ (λ 0) 0)
5 → (λ (λ 1) 0)
6 → ... so on
</code></pre>

<p>Related questions: is there an algorithm that maps between natural numbers and <strong>normalized</strong> terms of the simply typed lambda calculus? Also, the same questions applied to the untyped lambda calculus.</p>