5 ms·

All you need is λ, part one: booleans

133 points by azhenley 6y ago

Gehinnn 6y ago
A friend of me implemented a lambda evaluator that he used to teach various concepts in the lambda calculus (https://srtobi.github.io/lambda/docs/ https://srtobi.github.io/lambda/docs/). You can find examples here: https://github.com/SrTobi/lambda/blob/master/stddef/stddef.lambda https://github.com/SrTobi/lambda/blob/master/stddef/stddef.l...
ggm 6y ago
"First define your notation. Then define your terms" Shadowed? Is that like.. peter pan?
caseyohara 6y ago
On the same topic, Jim Weirich's 2012 talk "Y Not - Adventures in Functional Programming" on lambda calculus and the (little 'c') Y combinator is fantastic. https://www.youtube.com/watch?v=FITJMJjASUs https://www.youtube.com/watch?v=FITJMJjASUs
MBlume 6y ago
In roughly this vein, I wrote a brainfuck interpreter in the lambda calculus a while back, it was fun https://github.com/MichaelBlume/lambdafuck https://github.com/MichaelBlume/lambdafuck
- axaxs 6y ago
  I just wanted to say that this project both horrifies and impresses me.
triyambakam 6y ago
Just last night I found this excellent introduction to the Lambda Calculus by Gabriel Lebec [1]. It's one of the best I've come across and covers briefly history, building up combinators (using Smullyan's names) leading up to implementing Church encodings and gives Javascript equivalents (or approximations when not possible). The slides themselves are also very aesthetically pleasing, Gabriel has a good sense of colour and design [1] https://youtu.be/3VQ382QG-y4 https://youtu.be/3VQ382QG-y4
- gralx 6y ago
  You're right about the aesthetically pleasing slides. I usually find slides a distraction. Here they're pure elucidation.
dejawu 6y ago
After a few failed attempts to begin to understand the Lambda calculus, this is the one that finally "stuck" with me. Looking forward to future articles in this series! This part: > encoding a datatype with lambdas means representing the datatype as functions supporting all of its operations was the key in being able to make practical sense of its purpose.
supercasio 6y ago
The first part of the first paragraph is wrong: > Nearly a century ago, Alonzo Church invented the simple, elegant, and yet elusive lambda calculus. Along with Alan Turing, he then proved the Church-Turing thesis: that anything computable with a Turing machine can also be computed in the lambda calculus. The Church-Turing thesis is not something one can prove. It's more like an intuition and/or definition we have. It states that anything that is computable can be computed with a Turing machine. See [1]. "Anything computable with a Turing machine can also be computed in the lambda calculus" this is true but it not the Church-Turing thesis and its called a Turing-equivalence. This was also not proved by Church, but by Turing in an appendix to his paper [2]. About a computation model being Turing-equivalent: the fact that most reasonable computation models we came up with were proven to be Turing-equivalent is one of the reasons we believe in the Church-Turing thesis. [1] https://plato.stanford.edu/entries/church-turing/ https://plato.stanford.edu/entries/church-turing/ [2] https://link.springer.com/article/10.1007/s10506-017-9200-2 https://link.springer.com/article/10.1007/s10506-017-9200-2
- naniwaduni 6y ago
  Another statement of the Church-Turing thesis is to say that the the functions computable by a Turing machine (or lambda-computable, or general recursive) makes a good proxy for the intuitive concept of computability. From this perspective, "thesis" is a misnomer: it just happens to be a useful definition for "computability". That's not to say that there aren't edge cases where intuitive "computability" and Turing computability disagree; for most people, any number of oracle machine constructions will fall under the former but not the latter. We've just chosen to define the term in a way that's "easy" to define somewhat rigorously and has useful properties. It's kind of just like if we were to call the usual definition of the reals "Cauchy's thesis" or somesuch.
  - 30f0fn 6y ago
    The Church-Turing proposition carries an implicit challenge: find an algorithm to evaluate a function which is not Turing computable. Because it can be challenged in this way, it’s not just a definition (mere stipulation how to use the word “computable”).
martyalain 6y ago
Another approach can be seen here http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy without closures, lexical syntax and laziness. I don't know if it's still lambda calculus but we can still have fun.
deleted 6y ago
[deleted]
shoo 6y ago
see also John Tromp's 2012 entry to the IOCCC: https://www.ioccc.org/2012/tromp/hint.html https://www.ioccc.org/2012/tromp/hint.html > This program celebrates the close connection between obfuscation and conciseness, by implementing the most concise language known, Binary Lambda Calculus (BLC). > BLC was developed to make Algorithmic Information Theory, the theory of smallest programs, more concrete. It starts with the simplest model of computation, the lambda calculus, and adds the minimum amount of machinery to enable binary input and output. > More specifically, it defines a universal machine, which, from an input stream of bits, parses the binary encoding of a lambda calculus term, applies that to the remainder of input (translated to a lazy list of booleans, which have a standard representation in lambda calculus), and translates the evaluated result back into a stream of bits to be output. > Lambda is encoded as 00, application as 01, and the variable bound by the n'th enclosing lambda (denoted n in so-called De Bruijn notation) as 1^{n}0. That’s all there is to BLC! > For example the encoding of lambda term S = \x \y \z (x z) (y z), with De Bruijn notation \ \ \ (3 1) (2 1), is 00 00 00 01 01 1110 10 01 110 10
lisper 6y ago
Another take on the same topic: http://www.flownet.com/ron/lambda-calculus.html http://www.flownet.com/ron/lambda-calculus.html Culminating in computing the factorial of 10 in pure lambda calculus on an actual computer in non-geologic time.

133 points by azhenley 6y ago

A friend of me implemented a lambda evaluator that he used to teach various concepts in the lambda calculus (https://srtobi.github.io/lambda/docs/ https://srtobi.github.io/lambda/docs/). You can find examples here: https://github.com/SrTobi/lambda/blob/master/stddef/stddef.lambda https://github.com/SrTobi/lambda/blob/master/stddef/stddef.l...

ggm 6y ago

"First define your notation. Then define your terms" Shadowed? Is that like.. peter pan?

caseyohara 6y ago

On the same topic, Jim Weirich's 2012 talk "Y Not - Adventures in Functional Programming" on lambda calculus and the (little 'c') Y combinator is fantastic. https://www.youtube.com/watch?v=FITJMJjASUs https://www.youtube.com/watch?v=FITJMJjASUs

MBlume 6y ago

In roughly this vein, I wrote a brainfuck interpreter in the lambda calculus a while back, it was fun https://github.com/MichaelBlume/lambdafuck https://github.com/MichaelBlume/lambdafuck

axaxs 6y ago
I just wanted to say that this project both horrifies and impresses me.

triyambakam 6y ago

Just last night I found this excellent introduction to the Lambda Calculus by Gabriel Lebec [1]. It's one of the best I've come across and covers briefly history, building up combinators (using Smullyan's names) leading up to implementing Church encodings and gives Javascript equivalents (or approximations when not possible). The slides themselves are also very aesthetically pleasing, Gabriel has a good sense of colour and design [1] https://youtu.be/3VQ382QG-y4 https://youtu.be/3VQ382QG-y4

gralx 6y ago
You're right about the aesthetically pleasing slides. I usually find slides a distraction. Here they're pure elucidation.

dejawu 6y ago

After a few failed attempts to begin to understand the Lambda calculus, this is the one that finally "stuck" with me. Looking forward to future articles in this series! This part: > encoding a datatype with lambdas means representing the datatype as functions supporting all of its operations was the key in being able to make practical sense of its purpose.

supercasio 6y ago

The first part of the first paragraph is wrong: > Nearly a century ago, Alonzo Church invented the simple, elegant, and yet elusive lambda calculus. Along with Alan Turing, he then proved the Church-Turing thesis: that anything computable with a Turing machine can also be computed in the lambda calculus. The Church-Turing thesis is not something one can prove. It's more like an intuition and/or definition we have. It states that anything that is computable can be computed with a Turing machine. See [1]. "Anything computable with a Turing machine can also be computed in the lambda calculus" this is true but it not the Church-Turing thesis and its called a Turing-equivalence. This was also not proved by Church, but by Turing in an appendix to his paper [2]. About a computation model being Turing-equivalent: the fact that most reasonable computation models we came up with were proven to be Turing-equivalent is one of the reasons we believe in the Church-Turing thesis. [1] https://plato.stanford.edu/entries/church-turing/ https://plato.stanford.edu/entries/church-turing/ [2] https://link.springer.com/article/10.1007/s10506-017-9200-2 https://link.springer.com/article/10.1007/s10506-017-9200-2

naniwaduni 6y ago
Another statement of the Church-Turing thesis is to say that the the functions computable by a Turing machine (or lambda-computable, or general recursive) makes a good proxy for the intuitive concept of computability. From this perspective, "thesis" is a misnomer: it just happens to be a useful definition for "computability". That's not to say that there aren't edge cases where intuitive "computability" and Turing computability disagree; for most people, any number of oracle machine constructions will fall under the former but not the latter. We've just chosen to define the term in a way that's "easy" to define somewhat rigorously and has useful properties. It's kind of just like if we were to call the usual definition of the reals "Cauchy's thesis" or somesuch.
- 30f0fn 6y ago
  The Church-Turing proposition carries an implicit challenge: find an algorithm to evaluate a function which is not Turing computable. Because it can be challenged in this way, it’s not just a definition (mere stipulation how to use the word “computable”).

martyalain 6y ago

Another approach can be seen here http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy without closures, lexical syntax and laziness. I don't know if it's still lambda calculus but we can still have fun.

deleted 6y ago

[deleted]

shoo 6y ago

see also John Tromp's 2012 entry to the IOCCC: https://www.ioccc.org/2012/tromp/hint.html https://www.ioccc.org/2012/tromp/hint.html > This program celebrates the close connection between obfuscation and conciseness, by implementing the most concise language known, Binary Lambda Calculus (BLC). > BLC was developed to make Algorithmic Information Theory, the theory of smallest programs, more concrete. It starts with the simplest model of computation, the lambda calculus, and adds the minimum amount of machinery to enable binary input and output. > More specifically, it defines a universal machine, which, from an input stream of bits, parses the binary encoding of a lambda calculus term, applies that to the remainder of input (translated to a lazy list of booleans, which have a standard representation in lambda calculus), and translates the evaluated result back into a stream of bits to be output. > Lambda is encoded as 00, application as 01, and the variable bound by the n'th enclosing lambda (denoted n in so-called De Bruijn notation) as 1^{n}0. That’s all there is to BLC! > For example the encoding of lambda term S = \x \y \z (x z) (y z), with De Bruijn notation \ \ \ (3 1) (2 1), is 00 00 00 01 01 1110 10 01 110 10

lisper 6y ago

Another take on the same topic: http://www.flownet.com/ron/lambda-calculus.html http://www.flownet.com/ron/lambda-calculus.html Culminating in computing the factorial of 10 in pure lambda calculus on an actual computer in non-geologic time.