thanks, and generating simply-typed terms

[jhines at haverford.edu]

Thank you very much for all of your many answers to my previous question. 
I suspect that it was inappropriately simple, because I was asking about
a proof checker, and people responded with provers; as Dr. Huet said, it
would be an exercise in deterministic programming.
I am still digesting the various answers, but I'd like to ask another question.

I would like to generate (all) small simply-typed lambda-terms of a given 
type. Is there a system or technique which would make this easy?

An "application" of this might be to approximate Kolmogorov complexity of 
numbers; instead of "the length of the smallest turing-machine program
that outputs the number", you could have "the length of the smallest
simply-typed lambda-term that reduces to the number", which, unlike
Kolmogorov complexity, would be computable.
(and having a list of numbers ordered simplest to more complex would be cool.)

If you are about to write a function, and have already written its type
and some test cases, possibly this enumeration procedure could generate a 
decent guess for what function you are about to write.

I have read a paper "Fixpoint Technique For Counting Terms In Typed
lambda Calculus" 
by Marek Zaionc, which talks about counting normal-form terms of a given type.
Unfortunately, that paper does not help with generating non-normal terms.

I can encode the concept of "well-formed lambda-term" into MACE4 (an
automatic finite model finder for first-order logic), and generate
lambda-terms. Encoding "simply-typed lambda-term" into MACE4 is probably
possible, but there must be a better way. If I understand the
Curry-Howard Isomorphism correctly, I would be looking for a brute-force
enumeration of Fitch-style proofs in the implicational fragment of
intuitionistic logic, i.e. FH_{->}.

Thanks very much.

Johnicholas Hines