TY - GEN
T1 - λ to ski, semantically
T2 - 14th International Symposium on Functional and Logic Programming, FLOPS 2018
AU - Kiselyov, Oleg
N1 - Publisher Copyright:
© 2018, Springer International Publishing AG, part of Springer Nature.
PY - 2018
Y1 - 2018
N2 - We present a technique for compiling lambda-calculus expressions into SKI combinators. Unlike the well-known bracket abstraction based on (syntactic) term re-writing, our algorithm relies on a specially chosen, compositional semantic model of generally open lambda terms. The meaning of a closed lambda term is the corresponding SKI combination. For simply-typed as well as unityped terms, the meaning derivation mirrors the typing derivation. One may also view the algorithm as an algebra, or a non-standard evaluator for lambda-terms (i.e., denotational semantics). The algorithm is implemented as a tagless-final compiler for (uni)typed lambda-calculus embedded as a DSL into OCaml. Its type preservation is clear even to OCaml. The correctness of both the algorithm and of its implementation becomes clear. Our algorithm is easily amenable to optimizations. In particular, its output and the running time can both be made linear in the size (i.e., the number of all constructors) of the input De Bruijn-indexed term.
AB - We present a technique for compiling lambda-calculus expressions into SKI combinators. Unlike the well-known bracket abstraction based on (syntactic) term re-writing, our algorithm relies on a specially chosen, compositional semantic model of generally open lambda terms. The meaning of a closed lambda term is the corresponding SKI combination. For simply-typed as well as unityped terms, the meaning derivation mirrors the typing derivation. One may also view the algorithm as an algebra, or a non-standard evaluator for lambda-terms (i.e., denotational semantics). The algorithm is implemented as a tagless-final compiler for (uni)typed lambda-calculus embedded as a DSL into OCaml. Its type preservation is clear even to OCaml. The correctness of both the algorithm and of its implementation becomes clear. Our algorithm is easily amenable to optimizations. In particular, its output and the running time can both be made linear in the size (i.e., the number of all constructors) of the input De Bruijn-indexed term.
UR - http://www.scopus.com/inward/record.url?scp=85046829119&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85046829119&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-90686-7_3
DO - 10.1007/978-3-319-90686-7_3
M3 - Conference contribution
AN - SCOPUS:85046829119
SN - 9783319906850
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 33
EP - 50
BT - Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Proceedings
A2 - Gallagher, John P.
A2 - Sulzmann, Martin
A2 - Gallagher, John P.
PB - Springer Verlag
Y2 - 9 May 2018 through 11 May 2018
ER -