[Prev][Next][Index][Thread]
thanks, and generating simply-typed terms
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
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