Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
Logic (xxiivv.com)
91 points by natly on May 11, 2022 | hide | past | favorite | 25 comments


Tangential: I highly recommend exploring the parent site https://wiki.xxiivv.com and the associated http://100r.co the author is working on with their sailing boat partner. Yes, they're living on a sail boat in the Pacific Ocean.

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.


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


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).


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.


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/


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.


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?


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!


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


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:

    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
Now if you want to read the definitions, you will need lambda calculus. It is basically an endless combination of two operations, one which is used to build and expression and one which is used to resolve it.

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 
The parentheses are redundant: `λx.λy.x`, and for notational sugar we contract the definition: `λxy.x`.

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
Now it's possible to read the previously nonsensical notation in the article, both intuitively and by thinking open the relationships promised:

    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₂
Now we can perform some tactical renaming (called α-conversion, we used this to avoid name collisions before):

    W := λxy.x y y
This is the official definition of the W-combinator and nearly the definition given to us, that being `W := λxyz.x y y z`. However, we can see that in application there is no difference:

    (λ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
Hence, we consider these equivalent through something called η-reduction (`λx.E x = E` if `x` is not free in E). We can see, then, that each three of these systems can create any lambda expression, which are proven to be isomorphic to Turing machines. This is a powerful way to manipulate not only logic, but computation itself.

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?


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.


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, ...}?


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:

      -- 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
The biggest leap to make is the first to the second line. S here is the x, a is the z, and (SK) is the y. Then with a little imagination you should be able to see that the expression morphed into xz(yz) with whatever wasn't touched, in this case bc, just kind of stuck on the end.

This also shows that the definition of the W-combinator given in the article

    Wxyz → xyyz
is a little overenthusiastic in having three arguments. The last one is actually never touched with the SK-definition!

    Wxy → xyy
would actually be enough, and it's the canonical definition for it when working with combinatory logic in a more serious context.


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.


> 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?


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
Similarly, because true is defined as K, and false as KI, if you evaluate Mxy where x and y are K or KI, and keep evaluating, you'll eventually end up with either K or KI, depending on whether (x or y) is true or false. I agree, though, that is confusing that the post didn't explain any of this; I assume it's not finished yet.


"Combinatory Forests are inhabited by talking birds, which speak words delimited by parentheses."

Are there any biologists around who can confirm this?


I wonder if To Dissect a Mockingbird inspired Urbit's Nock




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: