Paper Info
Title
On Synergies between Type Inference, Generation and Normalization of SK-Combinator Trees.
Abstract
The S and K combinator expressions form a well-known Turing-complete subset of the lambda calculus. Using Prolog as a meta-language, we specify evaluation, type inference and combinatorial generation algorithms for SK-combinator trees. In the process, we unravel properties shedding new light on interesting aspects of their structure and distribution. We study the proportion of well-typed terms among size-limited SK-expressions as well as the type-directed generation of terms of sizes smaller than the size of their simple types. We also introduce the well-typed frontier of an untypable term and we use it to design a simplification algorithm for untypable terms taking advantage of the fact that well-typed terms are normalizable.
Year
DOI
Venue
2015
10.1109/SYNASC.2015.33
SYNASC
Keywords
Field
DocType
SK-combinator calculus, lambda calculus, type inference, normalization, generation of well-typed combinator expressions, logic programming as meta-language
Discrete mathematics,Lambda calculus,Normalization (statistics),Expression (mathematics),Combinatory logic,Binary tree,Theoretical computer science,Type inference,Prolog,Logic programming,Mathematics
Conference
ISSN
Citations 
PageRank 
2470-8801
0
0.34
References 
Authors
7
1
Name
Order
Citations
PageRank
Paul Tarau11529113.14