coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Grammatical motifs in lambda terms and lambda types - source for discovery of interesting theorems and Coq tactics?

From: Jan Bessai <jan.bessai AT tu-dortmund.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Grammatical motifs in lambda terms and lambda types - source for discovery of interesting theorems and Coq tactics?
Date: Mon, 3 Feb 2020 05:01:52 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jan.bessai AT tu-dortmund.de; spf=Pass smtp.mailfrom=jan.bessai AT tu-dortmund.de; spf=None smtp.helo=postmaster AT unimail.uni-dortmund.de
Ironport-phdr: 9a23:E6GvGRDgel3JenTTbnBFUyQJP3N1i/DPJgcQr6AfoPdwSPT4osbcNUDSrc9gkEXOFd2Cra4d16yK7eu+AiRAuc/H7ClZNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULjoZuMKk8xxrGrnZJdeld2GdkKU6Okxrm6cq84ZBu/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnNTAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhygZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4cSGFcXMheSjZBD5uyYYUPEeQPIOVWr4fyqFQSsBSxBxKhBP/zxjJSmnP6wbE23/onHArb3AIgBdUOsHHModvxLqgSV/2+wbTWwjXYdPNZwzb945XPfxAju/6MW6h8ftHPxkk0DAPKlFSQpJf5PzOIz+gCrm+b7/B8VeKqlm4nrRx+riKyycgyk4TEgJ8exF7D9SV82ok1JNu4RVZnYd65CZdfqiaaN5FqQsMnXmFovjs1xqcbtpGleiUB1ZcpxwbHZvCabYSF5gjvWPiMLTp6nn5pZayzihWo/UWg1+HwTsq53VZQoiZbjNXArG4B2h3J5sSZVvdw/EGs0iuV2Q/J8OFLO0U0mLLbK5E/xr4wkYIesVnFHi/3nUX5lq6WdkE+9ui17eTnY6zqqYKbN49ulgH+N7kumsqiDugiLwcBQXCX+eW61LL94U30WKhGguMyn6XDrpzWOMYWqrSkDwNL0Ysv8RayAyq+3NQdh3YHLVZFeBydj4juPlHDOPL4Au25g1i2izhk2evGPqb7DZXMNXXDjKrhca9g5E5b0goz0dVf549SCr4cOv78R1H+uMTCDhAlKwy03/rnCNJl24wCXmKPG7aVP7/WsV+V/e0iOPKMZY8QuDblMfcp/f/ujXkjmV8cZ6alx5UXaGrrVshhdk6eeD/nhsoLOWYMpAs3CuLw23OYVjsGRX+0F4gx/SoyCcryD47FAIqgm6eI3Q+nA9haYXpaD02KHTHketPXCL83dCuOL5o5wXQ/Xr+7Rtp5jE38hErB07Nia9Hs1GgAr5u6iopp+qjfkgsu8CFyA4KR3jPVFjAmriYzXzYzmZtHjwl4w1aH37J/hqUGR8BOov9OSBs/KJjQieB3WYmrB1DxO+yRQVPjee2IRDE8StVrno0TZUd4EtSmyA3F3m+mBKUJkqGNCNo4//CE0g==

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

[Coq-Club] Grammatical motifs in lambda terms and lambda types - source for discovery of interesting theorems and Coq tactics?, Alex Meyer, 02/02/2020
- Re: [Coq-Club] Grammatical motifs in lambda terms and lambda types - source for discovery of interesting theorems and Coq tactics?, Jim Fehrle, 02/03/2020
  - Re: [Coq-Club] Grammatical motifs in lambda terms and lambda types - source for discovery of interesting theorems and Coq tactics?, Jan Bessai, 02/03/2020
    - Re: [Coq-Club] Grammatical motifs in lambda terms and lambda types - source for discovery of interesting theorems and Coq tactics?, Gabriel Scherer, 02/03/2020