A correct-by-construction conversion from lambda calculus to combinatory logic

[matt_d]

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/correctbyconstruction-conversion-from-lambda-calculus-to-combinatory-logic/B2A7BCF12A7A5D52B294C78A6F04191F

[tromp]

Kudos to the Journal of Functional Programming for making its articles available freely online in such easy to read form.

Note that this article presents a translation for the simply typed lambda calculus, which is strongly normalizing and doesn't allow for general recursion. But it still allows you to compute things like the factorial function

     λn.λf.n(λf.λn.n(f(λf.λx.n f(f x))))(λx.f)(λx.x)

or in graphical form [1]

    ┬────────────────
    ┼─────────────┬──
    │ ──┬──────── ┼ ┬
    │ ┬─┼─┬────── │ │
    │ │ │ ┼─┬─┬── │ │
    │ │ │ ┼─┼─┼─┬ │ │
    │ │ │ └─┤ ├─┘ │ │
    │ │ │   ├─┘   │ │
    │ │ ├───┘     │ │
    │ ├─┘         │ │
    └─┤           │ │
      └───────────┤ │
                  └─┘

which only needs the built-in iteration of Church numerals.

[1] https://tromp.github.io/cl/diagrams.html

[tromp → tromp]

Btw, that factorial translates to S (K (S S (K (S K)))) (S (K (S (K (S S (K K))) K)) (S I (K (S (K (S I)) (S (K (S S (K (S (K (S S (S K))) (S (K (S (K S) K))))))) K))))) over the basis {S,K,I} that the paper uses. Widening the basis with combinators C and W allows for the less verbose C (B C (C (B B (C I (B W (B (B (C I)) (C B (B W (B B))))))) K)) I.

[_a_a_a_ → tromp]

Something I've never understood about combinators, perhaps you can help. Are they of any practical use, or really of mathematical interest only?

I realise there are probably different kinds of combinatorsand the above are, I assume the SKI combinators, so are the SKI combinators of practical use? In fact, what are 'combinators' anyway? TIA

[tromp → _a_a_a_]

They are of some practical interest as well. I think David Turner was the first to use them in his SASL language [1]. When combined with a graph rewriting implementation, combinators offer an excellent balance of simplicity and efficiency, as demonstrated in Ben Lynn's IOCCC-winning Haskell compiler [2].

[1] https://en.wikipedia.org/wiki/SASL_(programming_language)

[2] https://crypto.stanford.edu/~blynn/compiler/ioccc.html https://en.wikipedia.org/wiki/Miranda_(programming_language)

[doubloon → _a_a_a_]

my question is - since combinators have no variables, can you use this process to turn a piece of functional programming language code directly into an optimized circuit board using logic gates ?

[tromp → doubloon]

No; combinators do not correspond to logic gates. Combinator S in particular duplicates its 3rd argument:

    S x y z = x z (y z)

producing larger terms, while logic gates just compute fixed size boolean functions.

[082349872349872 → tromp]

> the alternative Omega diagram ...

... looks to me like a "Kilroy was here"