λ to ski, semantically: Declarative pearl

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationFunctional and Logic Programming - 14th International Symposium, FLOPS 2018, Proceedings
EditorsJohn P. Gallagher, Martin Sulzmann, John P. Gallagher
PublisherSpringer-Verlag
Pages33-50
Number of pages18
ISBN (Print)9783319906850
DOIs
Publication statusPublished - 2018 Jan 1
Event14th International Symposium on Functional and Logic Programming, FLOPS 2018 - Nagoya, Japan
Duration: 2018 May 92018 May 11

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10818 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other14th International Symposium on Functional and Logic Programming, FLOPS 2018
CountryJapan
CityNagoya
Period18/5/918/5/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'λ to ski, semantically: Declarative pearl'. Together they form a unique fingerprint.

  • Cite this

    Kiselyov, O. E. (2018). λ to ski, semantically: Declarative pearl. In J. P. Gallagher, M. Sulzmann, & J. P. Gallagher (Eds.), Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Proceedings (pp. 33-50). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10818 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-90686-7_3