Logic(wiki.xxiivv.com)
wiki.xxiivv.com
Logic
https://wiki.xxiivv.com/site/logic.html
27 comments
Yeah and make sure to check out their patreon if you want to incentivize and support people living alternative lifestyles and creating things with love like this:
https://www.patreon.com/100
https://www.patreon.com/100
Some context for puzzled readers:
This site uses combinatory logic (https://en.wikipedia.org/wiki/Combinatory_logic).
Combinatory logic is a way to express logic without using variables and quantifiers (e.g., no "x", no "forall x").
In combinatory logic, formulae are strings of combinators: (e.g., "SKK").
To help introduce readers to combinatory logic, some people think it is helpful to have analogies where a combinator (like S) is explained as a type of bird.
To my knowledge, this was first suggested by Raymond Smullyan (https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird).
This site uses combinatory logic (https://en.wikipedia.org/wiki/Combinatory_logic).
Combinatory logic is a way to express logic without using variables and quantifiers (e.g., no "x", no "forall x").
In combinatory logic, formulae are strings of combinators: (e.g., "SKK").
To help introduce readers to combinatory logic, some people think it is helpful to have analogies where a combinator (like S) is explained as a type of bird.
To my knowledge, this was first suggested by Raymond Smullyan (https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird).
The webpage adds some unnecessary confusion by
1) using colored shapes instead of variable names.
2) (initially) presenting combinators as having 3 arguments, where they only need 1 or 2. So instead of the usual M x = x x, you see M x y z = x x y z.
One (improper) bird I find very interesting is the Starling's cousin S* x y z = x z (y (K z)), from which all other birds can be reconstructed.
1) using colored shapes instead of variable names.
2) (initially) presenting combinators as having 3 arguments, where they only need 1 or 2. So instead of the usual M x = x x, you see M x y z = x x y z.
One (improper) bird I find very interesting is the Starling's cousin S* x y z = x z (y (K z)), from which all other birds can be reconstructed.
Fair enough, but not sure if it was meant for general consumption or just the author.
I don't get it. This post appears to be an intro to lambda calculus, but renamed to birds, and without enough detail to do anything interesting or worthwhile. Can someone enlighten me about what's interesting enough about this post to make it to the front page?
(I think) this is a modern rendition of David Keenan's To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction [1], also linked in the OP. Perhaps you might appreciate the original better.
[1] https://dkeenan.com/Lambda/
[1] https://dkeenan.com/Lambda/
Also: https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird - To Mock a Mockingbird by Smullyan, the origin for the birds in To Dissect a Mockingbird.
[deleted]
I see! Thank you lifthrasiir.
Longer and more familiar tokens that don't all just look like piles of meaningless letters make it so a non-math person can follow it right up until they start taking about booleans. They totally lost me there. But I'm impressed that they explained it in a way that let me even get that far.
After that it starts not making sense without prior knowledge.
I vaguely remember something about there being no data other than functions, so I assume the values of true and false are represented by functions represented by birds?
What does a doubling one of the words have to do with an OR? I'm assuming that when you pass one of these birds to another bird, there's something special happening, and the mockingbird is no longer just repeating a value, and there's some kind of function composition happening?
After that it starts not making sense without prior knowledge.
I vaguely remember something about there being no data other than functions, so I assume the values of true and false are represented by functions represented by birds?
What does a doubling one of the words have to do with an OR? I'm assuming that when you pass one of these birds to another bird, there's something special happening, and the mockingbird is no longer just repeating a value, and there's some kind of function composition happening?
Its like a version of math where you're representation of "2" is "++" so the expression 2 + 2 becomes "++" + "++".
"It is a wonderfully bizarre fact that each song of a combinatory bird is not merely the name of another bird but is actually a complete description of the internal plumbing of that other bird. That is, each song is actually a brain map of some bird. Since a song is a complete description of how some bird will respond when it hears another bird, and the only important thing about a combinatory bird is how it responds when it hears another bird, we see that songs and singers are interchangeable. So we can say that the birds sing birds to each other, or we can equally say that what we have is a bunch of songs that sing songs to each other! Combinatory birds exist at an almost mystical level. Their language has no distinction between verbs and nouns. A description of action can equally well be a name."
https://dkeenan.com/Lambda/
The bird K was defined as True, and KI as False (try not to think about the fact True(x) / False(x) evaluates to something).
The claim is that the bird M is logical OR. We can test this exhaustively. M repeats the first word twice, K omits the 2nd word, and I is just there. Leftmost bird is always the next in line for evaluation.
or(false,false): M(KI)(KI) : (KI)(KI)(KI) : I(KI)(KI) : (KI)(KI): I(KI) : (KI) = false
or(true,false): MK(KI) : KK(KI) : K = true
or(false,true): M(KI)K : (KI)(KI)K: I(KI)K : (KI)K : IK : K = true
or(true,true): MKK : KKK : K = true
So it works as claimed!
"It is a wonderfully bizarre fact that each song of a combinatory bird is not merely the name of another bird but is actually a complete description of the internal plumbing of that other bird. That is, each song is actually a brain map of some bird. Since a song is a complete description of how some bird will respond when it hears another bird, and the only important thing about a combinatory bird is how it responds when it hears another bird, we see that songs and singers are interchangeable. So we can say that the birds sing birds to each other, or we can equally say that what we have is a bunch of songs that sing songs to each other! Combinatory birds exist at an almost mystical level. Their language has no distinction between verbs and nouns. A description of action can equally well be a name."
https://dkeenan.com/Lambda/
The bird K was defined as True, and KI as False (try not to think about the fact True(x) / False(x) evaluates to something).
The claim is that the bird M is logical OR. We can test this exhaustively. M repeats the first word twice, K omits the 2nd word, and I is just there. Leftmost bird is always the next in line for evaluation.
or(false,false): M(KI)(KI) : (KI)(KI)(KI) : I(KI)(KI) : (KI)(KI): I(KI) : (KI) = false
or(true,false): MK(KI) : KK(KI) : K = true
or(false,true): M(KI)K : (KI)(KI)K: I(KI)K : (KI)K : IK : K = true
or(true,true): MKK : KKK : K = true
So it works as claimed!
If you go down the page, there's a "webring" logo, taking you to plenty of different websites, an excellent rabbit hole to fall into.
A lot of effort went into this post but the author didnt do enough preliminary explanation. I have some limited background in logic / FP but wasn't able to follow along.
Can someone explain the notation? Might be difficult without images
Can someone explain the notation? Might be difficult without images
Combinatory logic, underneath being lambda calculus.
For a simple explanation: think of `SKI` etc. as functions or transformations which do what is described, how they are described mathematically is discussed later. They act on all values, including each other. For this reason, they are called combinators, as combining them can give rise to any computation. Why that is is also discussed a bit later. Combinatoric application is left-associative, meaning that `SK` is equivalent to `S(K)` in more conventional mathematical notation.
For an easy example, think about the equivalence of the W-combinator and the expression SS(SK). If we apply some abstract values, say a, b, and c to these, we can make sure that the result is `a b b c`, keeping in mind that other combinators are a valid value for a combinator to take in:
The most important is abstraction, which isn't explained in the post. You write a lambda (λ), the name of a bound variable (say, x), and then a full stop and the "body" of the abstraction. This can be thought of as a mathematical function definition, so that you can think of `f(x) = x` and `f := λx.x` as identical. Note, however, that the latter is anonymous and has to be assigned a name separately.
The second operation is application. This is left-associative, and we do not use parenthesis. `f x` is the same as `f(x)` in conventional notation. `(λx.x) y)` is then the application of `y` to `λx.x`. We replace the bound variable in the expression with the applied value: `(λx.x) y → y`.
We can create more complex multi-variable functions by nesting these:
Armed with all of this, we can read the definitions of the "birds", or combinators:
Not the best explanation, but I feel like introducing lambda calculus is necessary to truly intuitively understand how the operators manipulate each other.
For a simple explanation: think of `SKI` etc. as functions or transformations which do what is described, how they are described mathematically is discussed later. They act on all values, including each other. For this reason, they are called combinators, as combining them can give rise to any computation. Why that is is also discussed a bit later. Combinatoric application is left-associative, meaning that `SK` is equivalent to `S(K)` in more conventional mathematical notation.
For an easy example, think about the equivalence of the W-combinator and the expression SS(SK). If we apply some abstract values, say a, b, and c to these, we can make sure that the result is `a b b c`, keeping in mind that other combinators are a valid value for a combinator to take in:
SS(SK) abc
→ S a (SK a) bc
→ a b (SK a b) c
→ a b (K b (a b)) c
→ a b (b) c = a b b c
The most important is abstraction, which isn't explained in the post. You write a lambda (λ), the name of a bound variable (say, x), and then a full stop and the "body" of the abstraction. This can be thought of as a mathematical function definition, so that you can think of `f(x) = x` and `f := λx.x` as identical. Note, however, that the latter is anonymous and has to be assigned a name separately.
The second operation is application. This is left-associative, and we do not use parenthesis. `f x` is the same as `f(x)` in conventional notation. `(λx.x) y)` is then the application of `y` to `λx.x`. We replace the bound variable in the expression with the applied value: `(λx.x) y → y`.
We can create more complex multi-variable functions by nesting these:
(λx.(λy.x)) 0 1
→ (λy.0) 1
→ 0
Armed with all of this, we can read the definitions of the "birds", or combinators:
S := λxyz.x z (y z)
K := λxyz.x z
I := λx.x
W := SS(SK)
→ (λxyz.x z (y z)) S (SK)
→ λz.S z (SK z)
→ λz.(λxyz₂.x z₂ (y z₂)) z (SK z)
→ λzz₂.z z₂ (SK z z₂)
→ λzz₂.z z₂ ((λxyz₃.x z₃ (y z₃)) K z z₂)
→ λzz₂.z z₂ (K z₂ (z z₂)
→ λzz₂.z z₂ ((λxy.x) z₂ (z z₂))
→ λzz₂.z z₂ z₂
W := λxy.x y y
(λxy.x y y) a b c = (λxyz.x y y z) a b c
→ (a b b) c = a b b c
→ a b b c = a b b c
Not the best explanation, but I feel like introducing lambda calculus is necessary to truly intuitively understand how the operators manipulate each other.
OFF: I am so annoyed of some people spending hours of writing an answer that is not searchable, and will not be useful for anyone but one person (but could be useful for dozens of people if they could find it).
Can't you e.g. open a stackoverflow question with parents question, and answer it, then link it here? Or any other method to make this answer to be available for the people that may need it in the future?
Can't you e.g. open a stackoverflow question with parents question, and answer it, then link it here? Or any other method to make this answer to be available for the people that may need it in the future?
I don't really think it's a good enough answer to count for that. There are plenty of good answers for this already out there, I just happened to write out a more mediocre one as I'd have no clue of what to search for. The article sure doesn't make it easy to recognize this as combinatory logic nor the fact that this is common notation for combinatory logic.
http://icfpc2011.blogspot.com/2011/06/task-description-conte...
The 2011 ICFP Contest was called Lambda: The Gathering. Its combinator card art, and some of the others, is based on this same idea of birds for the combinators.
The 2011 ICFP Contest was called Lambda: The Gathering. Its combinator card art, and some of the others, is based on this same idea of birds for the combinators.
For anyone interested in the topic (combinatory logic as told through the medium of birds) I adore Gabriel Lebec's talk "A Flock Of Functions: Combinators, Lambda Calculus & Church Encodings in JavaScript" https://youtu.be/3VQ382QG-y4
> The Starling does parenthesising, reordering, and duplication. Applied to three combinators, it applies each of the first two combinators to the last, then applies the first result of that to the second:
Can someone help me understand this leap? Thus far, the birds (functions) have been applied to shapes (perhaps "letters", if we are calling parenthesized-sequences of shapes "words"), but now this bird is being applied to combinators (presumably, another word for functions). How should I map from the set {yellow-triangle, red diamond, green circle} to the set {Mockingbird, Kestrel, Thrush, Bluebird, Warbler, ...}?
Can someone help me understand this leap? Thus far, the birds (functions) have been applied to shapes (perhaps "letters", if we are calling parenthesized-sequences of shapes "words"), but now this bird is being applied to combinators (presumably, another word for functions). How should I map from the set {yellow-triangle, red diamond, green circle} to the set {Mockingbird, Kestrel, Thrush, Bluebird, Warbler, ...}?
Think of the "birds" (combinators) acting on a combined set of both the birds and the shapes. Don't forget that parenthesized blocks of birds and shapes are considered a single "letter" for manipulation. For an example of these in action, take this application to SS(SK), equivalent to W, with three inputs a, b, and c:
This also shows that the definition of the W-combinator given in the article
-- reminder of the definitions
Sxyz → xz(yz)
Kxy → x
-- always expanding the leftmost combinator
SS(SK)abc
→ Sa(SKa)bc
→ ab(SKab)c
→ ab(Kb(ab))c
→ abbc
This also shows that the definition of the W-combinator given in the article
Wxyz → xyyz
Wxy → xyy
The colored shapes are arbitrary symbols, variables like in algebra. They could be other combinators or anything in the system. Kx, for instance, always produces whatever x, a variable, happens to be when applied to something else. So KKI will produce K. KIS produces I.
So there is no one for one mapping. Any of those birds/combinators or some parenthesized expression of them can be put in place of the colored shapes.
So there is no one for one mapping. Any of those birds/combinators or some parenthesized expression of them can be put in place of the colored shapes.
> The Mockingbird takes 2 booleans and returns True if at least one of them is True
But earlier on we were told:
> The first bird that we observe is the Mockingbird, which repeats the first word.
Can both of these things be true?
It also seems confusing that K, I, and KI are 3 different types of bird. How do you distinguish KI from KI?
But earlier on we were told:
> The first bird that we observe is the Mockingbird, which repeats the first word.
Can both of these things be true?
It also seems confusing that K, I, and KI are 3 different types of bird. How do you distinguish KI from KI?
You don't need to distinguish KI (the kite) from KI (the kestrel followed by the idiot bird), because they evaluate to the same thing. Kite xy is y, and if you evaluate Kestrel Idiot xy, you get:
KIxy -> Iy -> y
"Combinatory Forests are inhabited by talking birds, which speak words delimited by parentheses."
Are there any biologists around who can confirm this?
Are there any biologists around who can confirm this?
[deleted]
I wonder if To Dissect a Mockingbird inspired Urbit's Nock
Some cool software they've developed:
- http://100r.co/site/orca.html
- http://100r.co/site/ronin.html
- http://100r.co/site/uxn.html
It's such a deep rabbit hole of talent, passion and intellectual gratification. I'm not affiliated, just a fan, I really love their stuff.