7 ms·

A circuit-like notation for lambda calculus (2015)

80 points by Ivoah 9y ago

stevemk14ebr 9y ago
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.
- meuk 9y ago
  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).
tathougies 9y ago
Nice notation! Do these relate in any way to the interaction combinators?
Phrodo_00 9y ago
It's not that similar, but this somewhat reminded me of Alligator eggs[0] [0] http://worrydream.com/AlligatorEggs/ http://worrydream.com/AlligatorEggs/
- rch 9y ago
  It's mentioned in the prior work section.
lachenmayer 9y ago
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/ 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-programming-languages-as-notations https://www.deconstructconf.com/2017/chelsea-voss-programmin...
no_identd 9y ago
I'd strongly recommend comparing that notation to this notation: https://en.wikipedia.org/wiki/Cirquent_calculus https://en.wikipedia.org/wiki/Cirquent_calculus
Garlef 9y ago
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_cccs_seeing_comp.html https://golem.ph.utexas.edu/category/2006/08/categorifying_c...
zokier 9y ago
Very neat, but why it is drawn backwards, the inputs coming from left instead of right?
- B1FF_PSUVM 9y ago
  > 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.
  - zokier 9y ago
    > ["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.
tromp 9y ago
Lambda Diagrams [1] are a more abstract, less circuit-like, notation. [1] http://tromp.github.io/cl/diagrams.html http://tromp.github.io/cl/diagrams.html
grenoire 9y ago
Reminds me of http://graphicallinearalgebra.net http://graphicallinearalgebra.net which is also super cool.
lokimedes 9y ago
I got a vague association to Penrose’s graphical tensor notation https://en.m.wikipedia.org/wiki/Penrose_graphical_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.

80 points by Ivoah 9y ago

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.

meuk 9y ago
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).

tathougies 9y ago

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

Phrodo_00 9y ago

It's not that similar, but this somewhat reminded me of Alligator eggs[0] [0] http://worrydream.com/AlligatorEggs/ http://worrydream.com/AlligatorEggs/

rch 9y ago
It's mentioned in the prior work section.

lachenmayer 9y ago

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/ 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-programming-languages-as-notations https://www.deconstructconf.com/2017/chelsea-voss-programmin...

no_identd 9y ago

I'd strongly recommend comparing that notation to this notation: https://en.wikipedia.org/wiki/Cirquent_calculus https://en.wikipedia.org/wiki/Cirquent_calculus

Garlef 9y ago

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_cccs_seeing_comp.html https://golem.ph.utexas.edu/category/2006/08/categorifying_c...

zokier 9y ago

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

B1FF_PSUVM 9y ago
> 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.
- zokier 9y ago
  > ["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.

tromp 9y ago

Lambda Diagrams [1] are a more abstract, less circuit-like, notation. [1] http://tromp.github.io/cl/diagrams.html http://tromp.github.io/cl/diagrams.html

grenoire 9y ago

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

lokimedes 9y ago

I got a vague association to Penrose’s graphical tensor notation https://en.m.wikipedia.org/wiki/Penrose_graphical_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.