4 ms·
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 tra
by tromp 3y ago
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 https://tromp.github.io/cl/diagrams.html
- tromp 3y agoBtw, 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_ 3y agoSomething 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
- doubloon 3y agomy 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 3y agoNo; 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.
- tromp 3y agoThey 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) https://en.wikipedia.org/wiki/SASL_(programming_language) [2] https://crypto.stanford.edu/~blynn/compiler/ioccc.html https://crypto.stanford.edu/~blynn/compiler/ioccc.html https://en.wikipedia.org/wiki/Miranda_(programming_language) https://en.wikipedia.org/wiki/Miranda_(programming_language)
- 082349872349872 3y ago> the alternative Omega diagram ... ... looks to me like a "Kilroy was here"