Sciweavers

PADL
2015
Springer

On Logic Programming Representations of Lambda Terms: de Bruijn Indices, Compression, Type Inference, Combinatorial Generation,

8 years 6 months ago
On Logic Programming Representations of Lambda Terms: de Bruijn Indices, Compression, Type Inference, Combinatorial Generation,
We introduce a compressed de Bruijn representation of lambda terms and define its bijections to standard representations. Compact combinatorial generation algorithms are given for several families of lambda terms, including open, closed, simply typed and linear terms as well as type inference and normal order reduction algorithms. We specify our algorithms as a literate Prolog program. In the process, we rely in creative ways on unification of logic variables, cyclic terms, backtracking and definite clause grammars.
Paul Tarau
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where PADL
Authors Paul Tarau
Comments (0)