All you need is λ, part one: booleans

https://antitypical.com/posts/2020-03-29-all-you-need-is-lambda-1-booleans/

by azhenley • 6 years ago

133 31 6 years ago

antitypical.com

ggm• 6 years ago

"First define your notation. Then define your terms"

Shadowed? Is that like.. peter pan?

caseyohara• 6 years 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

MBlume• 6 years 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

axaxs• 6 years ago

I just wanted to say that this project both horrifies and impresses me.

Gehinnn• 6 years 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/).

You can find examples here: https://github.com/SrTobi/lambda/blob/master/stddef/stddef.l...

triyambakam• 6 years 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

gralx• 6 years ago

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

dejawu• 6 years 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.

supercasio3• 6 years 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/

[2] https://link.springer.com/article/10.1007/s10506-017-9200-2

naniwaduni2• 6 years 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• 6 years 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• 6 years ago

Another approach can be seen here 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.

shoo• 6 years ago

see also John Tromp's 2012 entry to the IOCCC: 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• 6 years ago

Another take on the same topic:

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.

All you need is λ, part one: booleans

Related Stories