[HN Gopher] Lambda Calculus Diagrams
___________________________________________________________________
Lambda Calculus Diagrams
Author : fanf2
Score : 73 points
Date : 2020-10-04 09:43 UTC (13 hours ago)
(HTM) web link (tromp.github.io)
(TXT) w3m dump (tromp.github.io)
| qsort wrote:
| 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.
| dan-robertson wrote:
| 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.
| qsort wrote:
| > 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.
| dan-robertson wrote:
| 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.
| th0ma5 wrote:
| 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?
| pickledish wrote:
| 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 :)
| RBerenguel wrote:
| 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
| tromp wrote:
| 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
| qubex wrote:
| 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.
| tromp wrote:
| 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...
| jdkee wrote:
| Great post and image here of Graham's number:
|
| https://mindsarentmagic.org/2020/02/19/a-picture-of-grahams-...
| [deleted]
| zitterbewegung wrote:
| 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
___________________________________________________________________
(page generated 2020-10-04 23:00 UTC)