Lambda Calculus Diagrams (2015) | Hacker News Reader

Lambda Calculus Diagrams (2015)

tromp.github.io

172 pointsfanf232 comments

The notation looks familiar to me because there is a similar knotation that Louis Kauffman uses to describe recursion in knot theory. See http://homepages.math.uic.edu/~kauffman/KnotLogic.pdf pages 5-7 .

For my last undergraduate research project I created a lambda calculus that would have a self distributed magma. Basically for all x,y,z you could do x @ (y @ z) = ( x @ y) @ (x @ z)

I didn't publish it because it took me another two years to implement the system in Mathematica after trying Javascript and also I didn't know what it could be used for. Also, the above self distributed operator could be implemented as a combinator or so forth.

The self distribution would have an interesting property that if you had an element in the magma then you could perform the above operator forever or you could think of it as a stream.

I have it in GitHub though if anyone wants to play with it. Ive been meaning to make video about it but I don't know if anyone would find it interesting.

https://github.com/zitterbewegung/lambda-magma-experiments

> a similar knotation that Louis Kauffman

that's much simpler to understand than the lambda diagram.

Yea, the representation is essentially a very restricted form of to parenthesis matching.

Kauffman’s book looks like a treasure trove! Reminds me of Penrosee’s RTR. Thanks for linking.

Kauffman has some papers with Buliga about graphical lambda calculus -- it seems like it's working with the string diagrams for a reflexive category, but with some extra goodies from an algebraic structure.

I was about to say "oh, you found a quandle/rack in the lambda calculus," but it seems you're already aware of this, given some of the filenames in your repository :-) In the Buliga/Kauffman papers, there are sections about representations of knot crossings as lambda calculus, which presumably forms a quandle (actually, probably a rack). Could you direct me to how your @ operation works? This seems very interesting.

I recently added quandles/racks to mathlib[1], the Lean standard math library. I think mathlib has some lambda calculus formalization, so it might be interesting adding a quandle instance for your operation.

[1] https://github.com/leanprover-community/mathlib/blob/master/...

I tried to work with Bulgia and Kauffman to move forward on that project but it was too complicated and also learning awk is very painful.

I have encountered your GitHub code (specifically the software you use to draw knots).

The lambda calculus with the self distributive magma basically would have all of the axioms of the lambda calculus but also with every valid statement in lambda calculus you also add the left self distributively law.

This was a simplification of the project due to time constraints. The original goal were to have all of the quandle operations to operate on every welf formed statement that would be a rewriting system.

https://ncatlab.org/nlab/show/self-distributive+operation

(a (b c)) => (a b) (a c)

So lets say we have the following church numeral.

λf.λx.f (f (f x))

We would be able to do an operation using the self-distributive operation

λf.λx.f (f (f x)) => λf.λx.f (f f) (f x)

This is a bit hand-wavy though.

This does feel like a language of glyphs that can effectively communicate complexity, although, much like spark graphs, could obscure detail. But ultimately it seems like this could be powerful. Am I just acclimated to higher information density or is it really promising?

I'm totally with you -- I sometimes wonder what a less-pure-text representation of code could look like, what advantages and disadvantages it would have compared to lines of text, and this is one of the first full examples I've found, which is really interesting. It does seem powerful.

I think the argument could be made that this is only possible with a language that uses barely any syntax, like the lambda calculus, since how would Python's 20+ keywords all translate into a graphical representation while preserving their true meaning (if statements and recursion could be straightforward, async and try/except... uh?). But it's nice to see that it's possible in simple cases, and that alone makes these harder questions seem more tractable IMO :)

Would it not make sense to do a compiler pass on the Python first?

Great post and image here of Graham's number:

https://mindsarentmagic.org/2020/02/19/a-picture-of-grahams-...

This is similar to the many proposals to replace the notation for numerals, or hexadecimal, or other math notation. I understand and agree that the set of squiggles we use is completely arbitrary, but the sets of squiggles known as "latin alphabet", "greek alphabet", and "arabic numerals" are the set of squiggles I grew up with. And using them has some advantages, for example, my proficiency with those particular sets of squiggles allowed me to notice in short order that the Y combinator is not, in fact, the one reported in the linked article.

The expression given in the OP is, according to Wikipedia, sometimes cited as the y combinator itself (and is beta equivalent).

The arbitrariness in the notation here isn’t about whether to use Latin letters or some other alphabet, or to write application on the left or the right, but rather about whether to use expressions in a formal language or some other representation. In many fields, different notations or finding eg some graph structure, may reveal interesting aspects of the underlying structure of something (eg why do we write permutations with cycle notation not permutation notation? Eg Conway’s notation for knots).

Also there are issues with the lambda calculus notation using letters for variables: whenever you do a substitution you may need to rename some variables if their meaning would change. I think this can be confusing to people and is perhaps an annoying thing to have in your notation.

> The expression given in the OP is, according to Wikipedia, sometimes cited as the y combinator itself (and is beta equivalent).

That's actually true, and very obviously so. I'm sorry.

> The arbitrariness...

I agree that clear notation is important; the pictorial style made me think of Feynman diagrams. My comment was a bit tongue-in-cheek, maybe unnecessarily so, but the point is that I fail to see how those pictures are clearer than plain text: you are not replacing complex stuff with a simple representation, you are just rewriting a simple formula in a different style.

> Also there are issues with the lambda calculus notation...

Are there? That's the same problem you face whenever you have dummy variables, e.g. the 'dx' in integrals.

Yeah I don’t see much from this notation (I also find it hard to tell the difference between the result of an abstraction and an application which feels like a somewhat important difference). I mostly wanted to suggest that diagrams or notation changes in general can be very useful.

It’s true that variable renaming comes up in other parts of mathematics but scope matters a lot less in most other mathematics, so much so that it is basically implicit and left to be inferred based on the mathematical context. You wouldn’t normally rename a variable to avoid a conflict so much as you would avoid giving it a conflicting name in the first place. The recursive nature of the lambda calculus means you can’t avoid the problem this way.

> Eg Conway’s notation for knots

I'm not sure how well-known this is, but Conway notation can be thought of as taking a Tait graph of the knot (i.e., a checkerboard graph) then reducing all the series-parallel networks until you get some irreducible graph. He noticed that certain kinds of series-parallel networks can be represented by an extended rational number (includes infinity), which can dramatically simplify the analysis of small knots -- to the point he was able to classify all of them in an afternoon! So, Conway notation corresponds to an irreducible planar graph with an expansion of each edge by a series-parallel network, with each edge in the expansion labeled by a rational number. You can even work out a set of moves such that if two such diagrams correspond to the same knot then there is a sequence of such moves connecting them.

I do wonder if there's a similar analysis for lambda calculus represented as graphs... It might be that certain expressions play the role of rational tangles. (Though very likely not :-) )

Knots correspond to graphs and the categorial diagrams commute. You basically have a closed compact category too.

http://personal.denison.edu/~ludwigl/2009ludwigfoisy.pdf

I wonder if some examples of this notation were etched on a metallic plate which we send to outer space, would the extra-terrestrials figure out what their meaning is?

Note that the author is the same John Tromp as in the Tromp-Taylor rules for the game of go [0].

    [0]: https://senseis.xmp.net/?TrompTaylorRules

Note that the submitter is the same fanf as in this winning entry [1] in the 1998 International Obfuscated C Code Contest (a bracket abstraction algorithm from lambda calculus into combinatory logic).

[1] https://www.ioccc.org/years.html#1998_fanf

This is really neat, but I don't understand why the diagram version have a little added drop-down. Take for example S [\x\y\z(x z)(y z)], the alternative version doesn't have the little extra vertical line segment. Is there a reason for it?

EDIT: Curiously, the Omega doesn't have it either.

No particular reason, except having different aesthetics. The regular diagrams always connect through their bottom left, so I let them stick out. The alternative diagrams are supposed to look prettier, which precluded having a leg stick out on the right of the bottom line .

OT: but hoping the reach you; is there a less obfuscated version of your binary lambda evaluator?

Slightly off-topic, but at the foot of the document a reference is provided to Keegan’s To Dissect A Mockingbird, another effort to provide a graphical notation for the lambda calculus.

Anyway, to cut a long story short: his notation for the Turing Theta Combinatory is now a tattoo on my arm.

Is there a picture of your tattoo online? I guess it's not this one [1], depicting the Y-combinator.

[1] https://math.stackexchange.com/questions/98011/is-this-formu...

is it the same Dave Keenan, who is the co-author of Sagittal microtonal notation [1]? (upd: oh, actually it's him, nice)

[1] http://sagittal.org

Imagine something like this for, say, a predicate calculus! Oh wait, there is: Frege's notation, and even though it historically was first, it never caught up. Hmmm, I wonder why?

So, I was expecting to see a Y-shaped graph for the Y-combinator, but it doesn’t look like that. Do anyone have a link to a resource showing why the Y-combinator is named thus?

Did you see the Note at the bottom?

"The diagram in the title, produced by the postscript code below, is a slightly deformed alternative Y diagram made to look like a Y."

That's not the reason it's called Y combinator though...

Oh, I red somewhere it was called thus due to some diagram shape. Is that completely wrong, or does it refer simply to an other kind of diagram?

Can someone explain what's going on here? I feel like this might be really interesting but I don't quite get the notation

it would be really cool to annotate the diagram with their corresponding equations

Reply on news.ycombinator.com