7 ms·

Algebra and the Lambda Calculus (1993)

196 points by espeed 8y ago

mesarvagya 8y ago
I have found paper by Raúl Rojas, which is also a good start to learn λ-calculus. Here it is http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf
- geoalchimista 8y ago
  There is an updated version of this tutorial on arxiv: https://arxiv.org/abs/1503.09060 https://arxiv.org/abs/1503.09060
- espeed 8y ago
  The significance of this paper is not about learning the λ-calculus. Rather, to me the significance of this paper is that it presents a novel way of "implementing the lambda calculus in an algebraic system" and provides a correspondence between the λ-calculus and the matrix model of computation: Vector and matrix valued functions can be represented by vectors and matrices some of whose entries are lambda expressions. I have been looking for a lingua franca for programming languages, a way to unify the langs and make use of the decades of wisdom encoded into our langs' Great Libs. Maybe the matrix model and linear algebra is the lingua franca I seek.
  - carapace 8y ago
    Paul Halmos' work on Algebraic Logic may be relevant. (And see also Conal Elliott's "Compiling to Categories" http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/ )
  - deleted 8y ago
    [deleted]
rbonvall 8y ago
I took the liberty of converting this to LaTeX: https://www.overleaf.com/read/vbnkshcwhcyk https://www.overleaf.com/read/vbnkshcwhcyk
- deleted 8y ago
  [deleted]
- lewisinc 8y ago
  Looks great, but did you mean to use `@` as a symbol?
  - rbonvall 8y ago
    Yes, that's how it's introduced in the original.
    - lewisinc 8y ago
      Cool, just pointing it out because it seemed typographically out of place.
- headsupftw 8y ago
  Thanks for doing this. There's an error on page 2 though: 0 = 1^2 + g - g@ It should be 0 = 1 + g^2 - g@
  - rbonvall 8y ago
    Good catch. Fixed.
joe_the_user 8y ago
I like the article's discussion of algebraic operations and computer representation as well as how to implement the lambda operation. That's all abstract algebra and its extensions. What I'm still mystified by when confronted by these discussions is the way the lambda calculus is considered equivalent to a Turing machine. Is it essentially that you have these complex variable substitution schemes which can "encode" a Turing machines' tape and transitions or is there something more straightforward?
- rbonvall 8y ago
  It is exactly that: you can simulate a Turing machine using lambda calculus and vice versa. But the variable substitution schemes you mention are not complex at all. The main rule is beta-reduction, which is really simple: just replace all appearances of the parameter with the value of the argument. (λ x . (x y) x) m → (m y) m β
  - WorldMaker 8y ago
    It's designed as a silly game for kids, but I still think Alligator Eggs is a good example of how fundamentally simple the Lambda Calculus substitution rules are (especially for people that want a more visual/metaphorical representation): http://worrydream.com/AlligatorEggs/ http://worrydream.com/AlligatorEggs/
- s_m_t 8y ago
  I guess the tape is just a linked list of bits? What confuses me about lambda calculus, and a lot of math in general, I guess, as opposed to something like the turing machine, is that, how do I put this... To actually implement Lisp or lambda calculus in real life you need "cons", right(?), and some way to increment your equivalent to an "instruction pointer". Or else you don't have any memory or information to operate on and you don't have any way to move on to the next step. If you are doing it on paper I guess the act of moving your pen to an empty space is your cons and moving your eyes across the page is like incrementing your instruction pointer... In the idea of the turing machine this is all explicitly explained but every time I try and read about lambda calculus it seems like they just expect you to know it right away. This might seem really trivial to other people but its how I tend to think.
deleted 8y ago
[deleted]
emmanueloga_ 8y ago
I was looking at the references at the bottom and saw `6`, I thought "Hygienic Macro Expansion? M.Fellinson? He probably must be referring to Matthias Felleisen...". Effectively: [1] Doesn't mean I understood the rest of the paper... sigh :-p 1: https://dl.acm.org/citation.cfm?id=319859 https://dl.acm.org/citation.cfm?id=319859
emmanueloga_ 8y ago
I wonder if this correspondence could be used for program transformations/optimizations? code -tx-> polynomial -tx-> simplification -tx-> [possibly more efficient] code
- espeed 8y ago
  My burgeoning conjecture (as hinted at in a previous comment) is that all can be unified, transformed, and optimized for modern hardware under the matrix model of computation -- type theory, the lambda calculus, the actor model, neural nets, graph computing -- I'm starting to see a path to where all models are aligned across vectors of unity. Here are some the correspondences I've been looking at... * Graph algos in the lang of linear algebra now realized and encoded into GraphBLAS [1] * The three normed division algebras are unified under a complex Hilbert space [2] * Ascent sequences and the bijections discovered between four classes of combinatorial objects [3] * Dependent Types and Homotopy Type Theory [4] * Bruhat–Tits buildings, symmetry, and spatial decomposition [5] * Distributed lattices, topological encodings, and succinct representations [6] * Zonotopes and Matroids and Minkowski Sums [7] * Holographic associative memory and entanglement renormalization [8] [1] Graph Algorithms in the Language of Linear Algebra (Jeremy Kepner) http://www.mit.edu/~kepner/ http://www.mit.edu/~kepner/ Discussion: https://news.ycombinator.com/item?id=18099520 https://news.ycombinator.com/item?id=18099520 [2] Division Algebras and Quantum Theory (John Baez) http://math.ucr.edu/home/baez/rch.pdf http://math.ucr.edu/home/baez/rch.pdf [3] (2 + 2)-free posets, ascent sequences and pattern avoiding permutations [pdf] https://www.sciencedirect.com/science/article/pii/S0097316509001885/pdf https://www.sciencedirect.com/science/article/pii/S009731650... [4] Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities [pdf] https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf [5] Bruhat–Tits buildings and p-adic Lie groups https://en.wikipedia.org/wiki/Building_(mathematics) https://en.wikipedia.org/wiki/Building_(mathematics) [6] Distributive lattices and Stone-space dualities https://en.wikipedia.org/wiki/Distributive_lattice#Representation_theory https://en.wikipedia.org/wiki/Distributive_lattice#Represent... [7] Solving Low-Dimensional Optimization Problems via Zonotope Vertex Enumeration [video] https://www.youtube.com/watch?v=NH_CpMYe3tw https://www.youtube.com/watch?v=NH_CpMYe3tw https://en.wikipedia.org/wiki/Zonohedron https://en.wikipedia.org/wiki/Zonohedron [8] Entanglement Renormalization (G Vidal) https://authors.library.caltech.edu/9242/1/VIDprl07.pdf?hovno=/ https://authors.library.caltech.edu/9242/1/VIDprl07.pdf?hovn... Holography https://en.wikipedia.org/wiki/Holographic_associative_memory https://en.wikipedia.org/wiki/Holographic_associative_memory Google Scholar: https://scholar.google.com/scholar?q=related:Yi-GtarGxh0J:scholar.google.com/&scioq=entanglement+renormalization+and+holography&hl=en&as_sdt=0,44&as_vis=1 https://scholar.google.com/scholar?q=related:Yi-GtarGxh0J:sc...
ssijak 8y ago
I don`t know how to call this effect, but often I look to learn about something specific and later that day the same topic pops up on the front page of HN. Earlier today I googled about "algebra and lambda calculus" and variations of that and lo and behold this peice on the front page few hours later. Is this some kind of advanced geek ad tracking or what? :D
- Zalastax 8y ago
  It's the frequency illusion (also known as the Baader-Meinhof phenomenon). https://rationalwiki.org/wiki/Frequency_illusion https://rationalwiki.org/wiki/Frequency_illusion
  - aaachilless 8y ago
    also known coloquially as 'blue car syndrome'. https://www.urbandictionary.com/define.php?term=Blue%20Car%20Syndrome https://www.urbandictionary.com/define.php?term=Blue%20Car%2...
  - yipbub 8y ago
    How do we know this is an illusion? Has anyone reproduced the illusion reliably?
- pasquinelli 8y ago
  It could be that, by searching for it, you're more likely to find it ;) Had you not searched for it, maybe this article wouldn't have been noticed. I think there's a name for this effect, but i can't recall it.
- espeed 8y ago
  Carl Jung termed the phenomenon synchronicity [1], "which holds that events are 'meaningful coincidences' if they occur with no causal relationship yet seem to be meaningfully related." Google the philosophy of information, phenomenology, and "the world is made of meaning." Also related is the phenomenon of multiple discovery / simultaneous invention [2]. Ironically, this is in-part what the Curry–Howard correspondence is about, with the Church–Turing thesis being a prime example [3]. [1] https://en.wikipedia.org/wiki/Synchronicity https://en.wikipedia.org/wiki/Synchronicity [2] https://en.wikipedia.org/wiki/Multiple_discovery https://en.wikipedia.org/wiki/Multiple_discovery [3] https://en.wikipedia.org/wiki/Church–Turing_thesis https://en.wikipedia.org/wiki/Church–Turing_thesis

196 points by espeed 8y ago

I have found paper by Raúl Rojas, which is also a good start to learn λ-calculus. Here it is http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf

geoalchimista 8y ago
There is an updated version of this tutorial on arxiv: https://arxiv.org/abs/1503.09060 https://arxiv.org/abs/1503.09060
espeed 8y ago
The significance of this paper is not about learning the λ-calculus. Rather, to me the significance of this paper is that it presents a novel way of "implementing the lambda calculus in an algebraic system" and provides a correspondence between the λ-calculus and the matrix model of computation: Vector and matrix valued functions can be represented by vectors and matrices some of whose entries are lambda expressions. I have been looking for a lingua franca for programming languages, a way to unify the langs and make use of the decades of wisdom encoded into our langs' Great Libs. Maybe the matrix model and linear algebra is the lingua franca I seek.
- carapace 8y ago
  Paul Halmos' work on Algebraic Logic may be relevant. (And see also Conal Elliott's "Compiling to Categories" http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/ )
- deleted 8y ago
  [deleted]

rbonvall 8y ago

I took the liberty of converting this to LaTeX: https://www.overleaf.com/read/vbnkshcwhcyk https://www.overleaf.com/read/vbnkshcwhcyk

deleted 8y ago
[deleted]
lewisinc 8y ago
Looks great, but did you mean to use `@` as a symbol?
- rbonvall 8y ago
  Yes, that's how it's introduced in the original.
  - lewisinc 8y ago
    Cool, just pointing it out because it seemed typographically out of place.
headsupftw 8y ago
Thanks for doing this. There's an error on page 2 though: 0 = 1^2 + g - g@ It should be 0 = 1 + g^2 - g@
- rbonvall 8y ago
  Good catch. Fixed.

joe_the_user 8y ago

I like the article's discussion of algebraic operations and computer representation as well as how to implement the lambda operation. That's all abstract algebra and its extensions. What I'm still mystified by when confronted by these discussions is the way the lambda calculus is considered equivalent to a Turing machine. Is it essentially that you have these complex variable substitution schemes which can "encode" a Turing machines' tape and transitions or is there something more straightforward?

rbonvall 8y ago
It is exactly that: you can simulate a Turing machine using lambda calculus and vice versa. But the variable substitution schemes you mention are not complex at all. The main rule is beta-reduction, which is really simple: just replace all appearances of the parameter with the value of the argument. (λ x . (x y) x) m → (m y) m β
- WorldMaker 8y ago
  It's designed as a silly game for kids, but I still think Alligator Eggs is a good example of how fundamentally simple the Lambda Calculus substitution rules are (especially for people that want a more visual/metaphorical representation): http://worrydream.com/AlligatorEggs/ http://worrydream.com/AlligatorEggs/
s_m_t 8y ago
I guess the tape is just a linked list of bits? What confuses me about lambda calculus, and a lot of math in general, I guess, as opposed to something like the turing machine, is that, how do I put this... To actually implement Lisp or lambda calculus in real life you need "cons", right(?), and some way to increment your equivalent to an "instruction pointer". Or else you don't have any memory or information to operate on and you don't have any way to move on to the next step. If you are doing it on paper I guess the act of moving your pen to an empty space is your cons and moving your eyes across the page is like incrementing your instruction pointer... In the idea of the turing machine this is all explicitly explained but every time I try and read about lambda calculus it seems like they just expect you to know it right away. This might seem really trivial to other people but its how I tend to think.

deleted 8y ago

[deleted]

emmanueloga_ 8y ago

I was looking at the references at the bottom and saw `6`, I thought "Hygienic Macro Expansion? M.Fellinson? He probably must be referring to Matthias Felleisen...". Effectively: [1] Doesn't mean I understood the rest of the paper... sigh :-p 1: https://dl.acm.org/citation.cfm?id=319859 https://dl.acm.org/citation.cfm?id=319859

emmanueloga_ 8y ago

I wonder if this correspondence could be used for program transformations/optimizations? code -tx-> polynomial -tx-> simplification -tx-> [possibly more efficient] code

espeed 8y ago
My burgeoning conjecture (as hinted at in a previous comment) is that all can be unified, transformed, and optimized for modern hardware under the matrix model of computation -- type theory, the lambda calculus, the actor model, neural nets, graph computing -- I'm starting to see a path to where all models are aligned across vectors of unity. Here are some the correspondences I've been looking at... * Graph algos in the lang of linear algebra now realized and encoded into GraphBLAS [1] * The three normed division algebras are unified under a complex Hilbert space [2] * Ascent sequences and the bijections discovered between four classes of combinatorial objects [3] * Dependent Types and Homotopy Type Theory [4] * Bruhat–Tits buildings, symmetry, and spatial decomposition [5] * Distributed lattices, topological encodings, and succinct representations [6] * Zonotopes and Matroids and Minkowski Sums [7] * Holographic associative memory and entanglement renormalization [8] [1] Graph Algorithms in the Language of Linear Algebra (Jeremy Kepner) http://www.mit.edu/~kepner/ http://www.mit.edu/~kepner/ Discussion: https://news.ycombinator.com/item?id=18099520 https://news.ycombinator.com/item?id=18099520 [2] Division Algebras and Quantum Theory (John Baez) http://math.ucr.edu/home/baez/rch.pdf http://math.ucr.edu/home/baez/rch.pdf [3] (2 + 2)-free posets, ascent sequences and pattern avoiding permutations [pdf] https://www.sciencedirect.com/science/article/pii/S0097316509001885/pdf https://www.sciencedirect.com/science/article/pii/S009731650... [4] Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities [pdf] https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf [5] Bruhat–Tits buildings and p-adic Lie groups https://en.wikipedia.org/wiki/Building_(mathematics) https://en.wikipedia.org/wiki/Building_(mathematics) [6] Distributive lattices and Stone-space dualities https://en.wikipedia.org/wiki/Distributive_lattice#Representation_theory https://en.wikipedia.org/wiki/Distributive_lattice#Represent... [7] Solving Low-Dimensional Optimization Problems via Zonotope Vertex Enumeration [video] https://www.youtube.com/watch?v=NH_CpMYe3tw https://www.youtube.com/watch?v=NH_CpMYe3tw https://en.wikipedia.org/wiki/Zonohedron https://en.wikipedia.org/wiki/Zonohedron [8] Entanglement Renormalization (G Vidal) https://authors.library.caltech.edu/9242/1/VIDprl07.pdf?hovno=/ https://authors.library.caltech.edu/9242/1/VIDprl07.pdf?hovn... Holography https://en.wikipedia.org/wiki/Holographic_associative_memory https://en.wikipedia.org/wiki/Holographic_associative_memory Google Scholar: https://scholar.google.com/scholar?q=related:Yi-GtarGxh0J:scholar.google.com/&scioq=entanglement+renormalization+and+holography&hl=en&as_sdt=0,44&as_vis=1 https://scholar.google.com/scholar?q=related:Yi-GtarGxh0J:sc...

ssijak 8y ago

I don`t know how to call this effect, but often I look to learn about something specific and later that day the same topic pops up on the front page of HN. Earlier today I googled about "algebra and lambda calculus" and variations of that and lo and behold this peice on the front page few hours later. Is this some kind of advanced geek ad tracking or what? :D

Zalastax 8y ago
It's the frequency illusion (also known as the Baader-Meinhof phenomenon). https://rationalwiki.org/wiki/Frequency_illusion https://rationalwiki.org/wiki/Frequency_illusion
- aaachilless 8y ago
  also known coloquially as 'blue car syndrome'. https://www.urbandictionary.com/define.php?term=Blue%20Car%20Syndrome https://www.urbandictionary.com/define.php?term=Blue%20Car%2...
- yipbub 8y ago
  How do we know this is an illusion? Has anyone reproduced the illusion reliably?
pasquinelli 8y ago
It could be that, by searching for it, you're more likely to find it ;) Had you not searched for it, maybe this article wouldn't have been noticed. I think there's a name for this effect, but i can't recall it.
espeed 8y ago
Carl Jung termed the phenomenon synchronicity [1], "which holds that events are 'meaningful coincidences' if they occur with no causal relationship yet seem to be meaningfully related." Google the philosophy of information, phenomenology, and "the world is made of meaning." Also related is the phenomenon of multiple discovery / simultaneous invention [2]. Ironically, this is in-part what the Curry–Howard correspondence is about, with the Church–Turing thesis being a prime example [3]. [1] https://en.wikipedia.org/wiki/Synchronicity https://en.wikipedia.org/wiki/Synchronicity [2] https://en.wikipedia.org/wiki/Multiple_discovery https://en.wikipedia.org/wiki/Multiple_discovery [3] https://en.wikipedia.org/wiki/Church–Turing_thesis https://en.wikipedia.org/wiki/Church–Turing_thesis