On Uniquely Closable and Uniquely Typable Skeletons of Lambda Terms

TL;DR

This paper studies the combinatorial structures of lambda term skeletons that are uniquely closable or typable, providing grammars for their generation and exploring their statistical and asymptotic properties.

Contribution

It introduces context-free grammars for these skeletons, derives efficient generation algorithms, and investigates their statistical properties and connections to binary trees.

Findings

Context-free grammars for skeletons of lambda terms.

Efficient algorithms for combinatorial generation.

Bijection between typable skeletons and binary trees.

Abstract

Uniquely closable skeletons of lambda terms are Motzkin-trees that predetermine the unique closed lambda term that can be obtained by labeling their leaves with de Bruijn indices. Likewise, uniquely typable skeletons of closed lambda terms predetermine the unique simply-typed lambda term that can be obtained by labeling their leaves with de Bruijn indices. We derive, through a sequence of logic program transformations, efficient code for their combinatorial generation and study their statistical properties. As a result, we obtain context-free grammars describing closable and uniquely closable skeletons of lambda terms, opening the door for their in-depth study with tools from analytic combinatorics. Our empirical study of the more difficult case of (uniquely) typable terms reveals some interesting open problems about their density and asymptotic behavior. As a connection between the two classes of terms, we also show that uniquely typable closed lambda term skeletons of size $3n+1$ are in a bijection with binary trees of size $n$.