Converting Combinatory Logic to and from Concatenative Calculus

  • Daniel Kiyoshi Hashimoto Vouzella de Andrade UFRJ
  • Hugo Musso Gualandi UFRJ

Resumo


Combinatory logic and its combinators BCKWI are a foundation for tacit (point-free) programming. But what does each letter mean? Informally, B stands for composing, C for swapping, K for discarding, W for duplicating and I is the identity function. However, B does more than that: depending on where it appears in the expression, it can also call functions or defer values for later. To help tell these purposes apart, we relate combinatory logic to the concatenative calculus of Kerby, which features separate primitives for the different facets of B. We provide translations from combinatory logic to concatenative calculus and vice versa. In both directions we have contributions. From concatenative to combinatory, we show that first-order stack programs map to regular combinators, and which patterns of combinators higher-order stack programs map to. From combinatory to concatenative, we extend an algorithm of Kerby to make it compatible with a call-by-value evaluation order, in addition to call-by-name. To enforce a strong association between the two worlds, our translations are simulations. That is, one evaluation step in the original program is simulated by zero or more evaluations steps in the translated program.

Palavras-chave: concatenative calculus, combinatory logic, stack languages, conversion, simulation, tacit programming, point-free programming

Referências

Haskell Brooks Curry, Robert Feys, William Craig, J Roger Hindley, and Jonathan P Seldin. 1958. Combinatory logic. Vol. 1. North-Holland Amsterdam. (Regular combinators are discussed in chapter 5).

Daniel Kiyoshi Hashimoto Vouzella de Andrade. 2024. From Combinatory to Concatenative and Back Again. Bachelor’s Thesis. Universidade Federal do Rio de Janeiro. [link].

Brent Kerby. 2002. The Theory of Concatenative Combinators. Published online at [link]. Accessed 05/09/2023.

Robert Kleffner. 2017. A Foundation for Typed Concatenative Languages. Master’s thesis. Northeastern University.

Peter J Landin. 1964. The mechanical evaluation of expressions. The computer journal 6, 4 (1964), 208–230. DOI: 10.1093/comjnl/6.4.308

Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.

Charles H Moore and Geoffrey C Leach. 1970. Forth–a language for interactive computing. Amsterdam: Mohasco Industries Inc (1970).

Sviatoslav Pestov, Daniel Ehrenberg, and Joe Groff. 2010. Factor: A dynamic stack-based programming language. ACM SIGPLAN Notices 45, 12 (2010), 43–58.

Adolfo Piperno. 1989. Abstraction problems in combinatory logic: a compositive approach. Theoretical computer science 66, 1 (1989), 27–43.

Elizabeth D Rather, Donald R Colburn, and Charles H Moore. 1996. The evolution of Forth. In History of programming languages—II. 625–670.

Moses Schönfinkel. 1924. Über die Bausteine der mathematischen Logik. Mathematische annalen 92, 3-4 (1924), 305–316.

Manfred von Thun. 1994. Mathematical foundations of Joy. Published online at [link]. Archived in 2011 at [link].

Manfred von Thun and Reuben Thomas. 2001. Joy: Forth’s Functional Cousin. In Proceedings of the 17th EuroForth Conference.
Publicado
30/09/2024
ANDRADE, Daniel Kiyoshi Hashimoto Vouzella de; GUALANDI, Hugo Musso. Converting Combinatory Logic to and from Concatenative Calculus. In: SIMPÓSIO BRASILEIRO DE LINGUAGENS DE PROGRAMAÇÃO (SBLP), 28. , 2024, Curitiba/PR. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2024 . p. 17-25.