On k-colored Lambda Terms and their Skeletons
The paper describes an application of logic programming to the modeling of difficult combinatorial properties of lambda terms, with focus on the class of simply typed terms. Lambda terms in de Bruijn notation are Motzkin trees (also called binary-unary trees) with indices at their leaves counting up on the path to the root the steps to their lambda binder. As a generalization of {\em affine lambda terms}, we introduce {\em k-colored lambda terms} obtained by labeling their lambda nodes with counts of the variables they bind. We define the {\em skeleton of a k-colored lambda term} as the Motzkin tree obtained by erasing the de Bruijn indices labeling its leaves and we give a bijection between 2-colored skeletons and binary trees that reveals their connection to the Catalan family of combinatorial objects. After a statistical study of properties of {\em k-colored lambda terms} and their skeletons, we focus on the case of simply-typed k-colored lambda terms for which a new combinatorial generation algorithm is given and some interesting relations between maximal coloring, size of type expressions and typability are explored. The paper is structured as a literate Prolog program to facilitate an easily replicable, concise and declarative expression of our concepts and algorithms.
Mon 8 JanDisplayed time zone: Tijuana, Baja California change
14:30 - 15:30 | |||
14:30 30mTalk | Exploiting Term Hiding to Reduce Run-time Checking Overhead PADL A: Nataliia Stulova IMDEA Software Institute and T.U. of Madrid (UPM), A: José Morales IMDEA Software Institute, A: Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid (UPM) | ||
15:00 30mTalk | On k-colored Lambda Terms and their Skeletons PADL |