A circuit-like notation for lambda calculus (2015) | Hacker News Reader

A circuit-like notation for lambda calculus (2015)

csvoss.github.io

80 pointsIvoah14 comments

At some point in my CS career i distinctly remember a "flip" i had in how i thought. The revelation was the fact that complexity and more generally information has an infinite number of ways of being represented. Somehow by stating that explicitly i was able to tackle new problems by first asking myself "is there a better model for this that expresses the same information and obeys similar constraints as what i am modeling". I started taking my Calculus notes in "code-like" ways, for example, using while loops and if's, adding arrows and other weird non-math syntax. To me they were more efficient ways of learning and remembering the information

New ways of modeling the same information always excite me. This is fantastic work.

That's funny. It sounds like you exploit the same mechanism that causes trained chess players to remember chess positions more accurately than novices (I think it might be similar to the 'memory palace' technique to remember things).

This is a nice find but it is very old news.

In mathematics (and mathematical physics), these are called string diagrams.

The short and simplified version of the story:

The (typed) lambda calculus 'corresponds' to cartesian closed categories. Such CCCs are a special case of monoidal categories. String diagrams are a notation for morphisms in monoidal categories.

To get you started, here's a related blog post on the n-category café

https://golem.ph.utexas.edu/category/2006/08/categorifying_c...

I'm a big fan of this idea! An automatated tool based on this would be really great for teaching the concepts of lambda calculus - similarly to how Lambda Bubble Pop http://chrisuehlinger.com/LambdaBubblePop/ can give you really strongs intuitions about eager & lazy evaluation.

The author gave a talk on this & related work at the excellent Deconstruct conference, definitely recommend it if you're into notations! https://www.deconstructconf.com/2017/chelsea-voss-programmin...

Reminds me of http://graphicallinearalgebra.net which is also super cool.

Lambda Diagrams [1] are a more abstract, less circuit-like, notation.

[1] http://tromp.github.io/cl/diagrams.html

It's not that similar, but this somewhat reminded me of Alligator eggs[0]

[0] http://worrydream.com/AlligatorEggs/

It's mentioned in the prior work section.

I got a vague association to Penrose’s graphical tensor notation https://en.m.wikipedia.org/wiki/Penrose_graphical_notation

There are a lot of examples in modern physics where people have come up with graphical notations to handle the kind of recursive complexity found in the article. There’s a lot of low-hanging fruit to be discovered in the last century of physics. Especially now that Machine Learning is all the buzz about tensors.

Very neat, but why it is drawn backwards, the inputs coming from left instead of right?

> inputs coming from left

["No, the other left" ;- ]

I'd assume they are using the math/programming "left-hand-side variable gets assigned right-hand-side value", instead of the "sources/inputs flow from the left to sinks/outputs at the right" usual in engineering drawings.

> ["No, the other left" ;- ]

It is amazing how you can grow old and still get some things wrong all the time, almost to the point of consistency.

I'd strongly recommend comparing that notation to this notation:

https://en.wikipedia.org/wiki/Cirquent_calculus

Nice notation! Do these relate in any way to the interaction combinators?

Reply on news.ycombinator.com