The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

In addition to Jan's work, I would add references to:

- The work of Pierre Lescanne ( https://dblp.uni-trier.de/pers/hd/l/Lescanne:Pierre ) on combinatorics of various flavors of lambda-terms (counting and generation).

- The work of Noam Zeilberger on the structure families of linear lambda-terms and their correspondence to various families of planar graphs ( http://noamz.org/#recent_papers ).

- In terms of "interesting theorems" but following a very different approach, there is interesting work in our community on "Lemma Discovery" and "Theory Exploration" (generating candidate lemmas, using testing to make guesses at which may be true, trying to prove them, and then assess their usefulness to prove further lemmas). See for example the work of Moa Johansson http://www.cse.chalmers.se/~jomoa/

Of these three topics, I think that the last one is the least related to the approach you suggest (it is not based on the structures of types and terms), and the closest to the sort of applications you seem to have in mind (it is useful in practice to assist the user in developing theorems for their theory of interest).

 

On Mon, Feb 3, 2020 at 5:02 AM Jan Bessai <jan.bessai AT tu-dortmund.de> wrote:

Hi,

> Are there research efforts to enumarate all such lambda types and terms,
> and find interesting motifs in types (=interesting theorems) and in terms
> (=interesting tactics)? Maybe combinatorics on words can be of help here?
> Maybe combinatorics on words have been applied to the Coq types and terms?
> There is work of S. Colton in the notions of "interesting theorem" and also
> recursive mathematics experience that some axioms are very valuable, more
> valuable than other. Maybe there is grammatical approach for gaining
> insight and explanation into this.

Sorry for the commercial, but this sounds related to my thesis, where I
studied type inhabitation with combinatory logic and intersection types,
as well as its relation to abstract algebra (CFGs are a restricted form
of signatures):

https://eldorado.tu-dortmund.de/handle/2003/38387

Intersection types might be helpful with your task because they can
guide the search procedure with semantic types (you can literally
express that a piece of syntax also has type "Interesting"). The thesis
includes an extractable Coq implementation.

-- Jan