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 -