5 ms·

To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus (1996)

102 points by dpatru 7y ago

genezeta 7y ago
Link has been updated
- dang 7y ago
  Whoops - changed from http://www.cs.virginia.edu/~evans/cs655-S00/readings/mockingbird.html http://www.cs.virginia.edu/~evans/cs655-S00/readings/mocking.... This was an invited repost of https://news.ycombinator.com/item?id=890715 https://news.ycombinator.com/item?id=890715 and I forgot to update the link from long ago. See https://hn.algolia.com/?dateRange=all&page=0&prefix=true&query=by%3Adang%20repost%20invit&sort=byDate&type=comment https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que... for more about invited reposts. There is a list of them at https://news.ycombinator.com/invited https://news.ycombinator.com/invited.
asplake 7y ago
Oh wow, a reference to Laws of Form (George Spencer-Brown), takes me back!
- bordercases 7y ago
  Definitely an underrated piece of work.
  - carapace 7y ago
    "The Markable Mark" site is a great exposition of the Laws of Form: http://www.markability.net/ http://www.markability.net/
    - bordercases 7y ago
      I think I benefited less from the letter of the Law, than through the spirit of it. My first exposure was very indirect coming from a decision analysis textbook, that motivated the construction of decision trees from something like the benefits of making distinctions, which were well-defined. (From that representation it becomes simple to analyze what conditional probabilities are relevant to your decision-making context.) They cited GSB through Francisco Varela who proposed that making distinctions was the fundamental operation of all cognitive thought. I found the idea compelling (if we know the roots of thinking, could that give us the levers to improve it?) but found Varela to be near-impenetrable. So I picked up GSB in hopes that this thin tome could shed some light on the manner. My god. You start seeing distinctions then you start seeing them everywhere. You understand what computational types are and why the adjunctions are ubquitous – and important. You get a sense of why psychological time must exist. You get why information always requires there to be an observer, and how the combination of all perspectives will necessarily be empty - our limitations to comprehension form the richness of our universe. You see the freedom we have in letting some things be distinguished over others and why people get confused about whether mathematics is discovered or invented. Surely it is neither, or both: we let something be to find out what it is. And the fact that you can draw a knot-theorist, a biologist, a decision theorist, and a Taoist out from the conceptual framework is a testament to how rich it is. Still, eventually I'm going to have to learn how to calculate with it.
joe_the_user 7y ago
Is there are relationship between the lambda calculus and Brainfuck and other few instruction set languages? Edit: well, an easy find, https://esolangs.org/wiki/Lambda_Calculus_to_Brainfuck https://esolangs.org/wiki/Lambda_Calculus_to_Brainfuck
- c1ccccc1 7y ago
  Also: https://esolangs.org/wiki/Iota https://esolangs.org/wiki/Iota
- posterboy 7y ago
  there's an isomorphism, because bf is np complete, as is simply typed lc. simply speaking, bf can implement lc, and vice versa, which would proof the claim. Edit: the ugly bit is that IO is always an ugly hack and potentially makes the program indetermined and thus impossible to proof a priory. but one can probably prove that they are equivalently unprovable.
  - anchpop 7y ago
    > because bf is np complete, as is simply typed lc. Do you mean turing complete?
- tromp 7y ago
  I wrote a Brainfuck interpreter in (binary) Lambda Calculus [1], which was included in my 2012 IOCC submission [2]. Writing a lambda calculus interpreter in BF would be a fun challenge. [1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Brainfuck https://tromp.github.io/cl/Binary_lambda_calculus.html#Brain... [2] http://www.ioccc.org/2012/tromp/hint.html http://www.ioccc.org/2012/tromp/hint.html
motohagiography 7y ago
I have this naive intuition that graphs are a universal encoding scheme, all theorems of category theory can be expressed as graphs, with the implication there is a massive unifying leap forward in maths that will result from expressing existing problems in terms that are consistent with such a representation. Maybe it's literary sci fi handwaving, but there must be a rules based level of abstraction that contains all we can conceive of and express. These diagrams appear to be an example of it.
- posterboy 7y ago
  > Maybe it's literary sci fi handwaving, but there must be rules based level of abstraction that contains all we can conceive of and express. > rules based level of abstraction that's not literature, that's bad grammar. Sorry.
  - motohagiography 7y ago
    Please.If only egregious crimes against the language were the bar.
- zozbot234 7y ago
  What kinds of graphs? There are a number of graphical representations that turn out to be incredibly useful in category theory, but they're far from equivalent. IIRC, https://arxiv.org/abs/1803.05316 https://arxiv.org/abs/1803.05316 introduces some of them.
  - motohagiography 7y ago
    Just saying objects and morphisms. The types of each are found in CT, which abstract-up to these, but are bounded/encompassed by the limits we know of regarding elementary ideas like cliques, cycles, paths, colouring, various morphisms. Compression, folding, encoding, and other information theory ideas have analogues represented as these, and the bottom up/depth first search of the problem space seems to come at it from the wrong direction. We're well into indulging Internet crank territory here but I'm naively speculating that for every known theorem, there is a consistent object/morphism representation of it, and the rules we're getting good at finding for these relationships (graphs) will yield insights we were missing for lack of an encompassing consistent abstraction.
galaxyLogic 7y ago
Another approach for visualizing lambda calculus is presented in https://ycombinator.chibicode.com/functional-programming-emojis https://ycombinator.chibicode.com/functional-programming-emo... . It looks quite different and I wonder which one is better? Or are they the same really?
- tromp 7y ago
  Yet another is my Lambda Diagrams [1], an obsolete link for which appears at the bottom of the article. [1] https://tromp.github.io/cl/diagrams.htm https://tromp.github.io/cl/diagrams.htm
xorand 7y ago
A js lambda to graphs parser and reducer https://mbuliga.github.io/quinegraphs/lambda2mol.html https://mbuliga.github.io/quinegraphs/lambda2mol.html

102 points by dpatru 7y ago

genezeta 7y ago

Link has been updated

dang 7y ago
Whoops - changed from http://www.cs.virginia.edu/~evans/cs655-S00/readings/mockingbird.html http://www.cs.virginia.edu/~evans/cs655-S00/readings/mocking.... This was an invited repost of https://news.ycombinator.com/item?id=890715 https://news.ycombinator.com/item?id=890715 and I forgot to update the link from long ago. See https://hn.algolia.com/?dateRange=all&page=0&prefix=true&query=by%3Adang%20repost%20invit&sort=byDate&type=comment https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que... for more about invited reposts. There is a list of them at https://news.ycombinator.com/invited https://news.ycombinator.com/invited.

asplake 7y ago

Oh wow, a reference to Laws of Form (George Spencer-Brown), takes me back!

bordercases 7y ago
Definitely an underrated piece of work.
- carapace 7y ago
  "The Markable Mark" site is a great exposition of the Laws of Form: http://www.markability.net/ http://www.markability.net/
  - bordercases 7y ago
    I think I benefited less from the letter of the Law, than through the spirit of it. My first exposure was very indirect coming from a decision analysis textbook, that motivated the construction of decision trees from something like the benefits of making distinctions, which were well-defined. (From that representation it becomes simple to analyze what conditional probabilities are relevant to your decision-making context.) They cited GSB through Francisco Varela who proposed that making distinctions was the fundamental operation of all cognitive thought. I found the idea compelling (if we know the roots of thinking, could that give us the levers to improve it?) but found Varela to be near-impenetrable. So I picked up GSB in hopes that this thin tome could shed some light on the manner. My god. You start seeing distinctions then you start seeing them everywhere. You understand what computational types are and why the adjunctions are ubquitous – and important. You get a sense of why psychological time must exist. You get why information always requires there to be an observer, and how the combination of all perspectives will necessarily be empty - our limitations to comprehension form the richness of our universe. You see the freedom we have in letting some things be distinguished over others and why people get confused about whether mathematics is discovered or invented. Surely it is neither, or both: we let something be to find out what it is. And the fact that you can draw a knot-theorist, a biologist, a decision theorist, and a Taoist out from the conceptual framework is a testament to how rich it is. Still, eventually I'm going to have to learn how to calculate with it.

joe_the_user 7y ago

Is there are relationship between the lambda calculus and Brainfuck and other few instruction set languages? Edit: well, an easy find, https://esolangs.org/wiki/Lambda_Calculus_to_Brainfuck https://esolangs.org/wiki/Lambda_Calculus_to_Brainfuck

c1ccccc1 7y ago
Also: https://esolangs.org/wiki/Iota https://esolangs.org/wiki/Iota
posterboy 7y ago
there's an isomorphism, because bf is np complete, as is simply typed lc. simply speaking, bf can implement lc, and vice versa, which would proof the claim. Edit: the ugly bit is that IO is always an ugly hack and potentially makes the program indetermined and thus impossible to proof a priory. but one can probably prove that they are equivalently unprovable.
- anchpop 7y ago
  > because bf is np complete, as is simply typed lc. Do you mean turing complete?
tromp 7y ago
I wrote a Brainfuck interpreter in (binary) Lambda Calculus [1], which was included in my 2012 IOCC submission [2]. Writing a lambda calculus interpreter in BF would be a fun challenge. [1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Brainfuck https://tromp.github.io/cl/Binary_lambda_calculus.html#Brain... [2] http://www.ioccc.org/2012/tromp/hint.html http://www.ioccc.org/2012/tromp/hint.html

motohagiography 7y ago

I have this naive intuition that graphs are a universal encoding scheme, all theorems of category theory can be expressed as graphs, with the implication there is a massive unifying leap forward in maths that will result from expressing existing problems in terms that are consistent with such a representation. Maybe it's literary sci fi handwaving, but there must be a rules based level of abstraction that contains all we can conceive of and express. These diagrams appear to be an example of it.

posterboy 7y ago
> Maybe it's literary sci fi handwaving, but there must be rules based level of abstraction that contains all we can conceive of and express. > rules based level of abstraction that's not literature, that's bad grammar. Sorry.
- motohagiography 7y ago
  Please.If only egregious crimes against the language were the bar.
zozbot234 7y ago
What kinds of graphs? There are a number of graphical representations that turn out to be incredibly useful in category theory, but they're far from equivalent. IIRC, https://arxiv.org/abs/1803.05316 https://arxiv.org/abs/1803.05316 introduces some of them.
- motohagiography 7y ago
  Just saying objects and morphisms. The types of each are found in CT, which abstract-up to these, but are bounded/encompassed by the limits we know of regarding elementary ideas like cliques, cycles, paths, colouring, various morphisms. Compression, folding, encoding, and other information theory ideas have analogues represented as these, and the bottom up/depth first search of the problem space seems to come at it from the wrong direction. We're well into indulging Internet crank territory here but I'm naively speculating that for every known theorem, there is a consistent object/morphism representation of it, and the rules we're getting good at finding for these relationships (graphs) will yield insights we were missing for lack of an encompassing consistent abstraction.

galaxyLogic 7y ago

Another approach for visualizing lambda calculus is presented in https://ycombinator.chibicode.com/functional-programming-emojis https://ycombinator.chibicode.com/functional-programming-emo... . It looks quite different and I wonder which one is better? Or are they the same really?

tromp 7y ago
Yet another is my Lambda Diagrams [1], an obsolete link for which appears at the bottom of the article. [1] https://tromp.github.io/cl/diagrams.htm https://tromp.github.io/cl/diagrams.htm

xorand 7y ago

A js lambda to graphs parser and reducer https://mbuliga.github.io/quinegraphs/lambda2mol.html https://mbuliga.github.io/quinegraphs/lambda2mol.html