Algebra and the Lambda Calculus (1993) | Hacker News Reader

Algebra and the Lambda Calculus (1993)

people.csail.mit.edu

196 pointsespeed39 comments

Open articleView on HN

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

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@

Good catch. Fixed.

Looks great, but did you mean to use `@` as a symbol?

Yes, that's how it's introduced in the original.

Cool, just pointing it out because it seemed typographically out of place.

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

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?

Philip Wadler provides an in depth discussion on the Curry–Howard correspondence [0] in his paper Propositions as Types [1], and he has given several talks under the same name that are on YouTube.

The talk Prof Wadler gave at Strange Loop is the most cited, but the talk he gave at Stanford [2] is the most interesting because Carl Hewitt was in the audience and was challenging him on the merits and long-term viability of functional programming in general vs Hewitt's Actor Model [3] for scalable concurrent computing.

[0] Curry–Howard correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence

[1] Propositions as Types [pdf] http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-...

[2] Propositions as Types (Stanford) [video] https://www.youtube.com/watch?v=ivzpaiw26wQ Slides [pdf] http://www.inf.ed.ac.uk/teaching/courses/tspl/pat.pdf

[3] Actor Model https://en.wikipedia.org/wiki/Category:Actor_model_(computer...

Philip Wadler also recently discussed this on the excellent programming podcast CoRecursive:

https://corecursive.com/021-gods-programming-language-with-p...

Turing himself proved them equivalent in his 1937 paper "Computability and λ-definability" which I've so far only found in image form:

http://www.turingarchive.org/browse.php/b/11

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
                        β

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/

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.

Lambda calculus (LC) isn't Lisp. LC does not represent its own notation as an object manipulated by lambda calculus and has nothing like a quote operator; to implement/simulate LC calculus, you don't require any specific data structure like a cons cell; there is nothing in LC to dictate it. You will need some sort of parser for a notation, and some run-time representation of functions (objects corresponding to the lambda terms) plus environments for the named parameters. Speaking of which, those names are not required to be anything like Lisp interned symbols.

I don't know if this helps, but the way I see lambda calculus works is that you assemble one expression in which you build all the things you need and then evaluate it to yield a result. After that, everything vanishes from existence.

For example, here I'm building cons, car and cdr just to create a list, from which I'll get its second value:

    (cons => car => cdr =>
    
        // this block is my little world where I have lists
        car(cdr(cons(1)(cons(2)(cons(3)(4)))))
    
    )(  // cons
        carValue => cdrValue => extractor => extractor(carValue)(cdrValue)
    )(  // car
        consValue => (consValue)(x => y => x)
    )(  // cdr
        consValue => (consValue)(x => y => y)
    )

(This is JavaScript-looking lambda calculus, so you can evaluate it in your browser's developer console).

Lambda calculus is simple, mechanical symbol substitution. There’s no information or memory needed outside of the initial ‘program’ other than the substitution rules.

Read about church encodings to see how numbers, pairs, conditionals, etc are encoded.

I doubt it; substitution will blow up on self-referential tricks like the Y combinator, where a function receives itself as an argument: any attempt to substitute the raw lambda text for this argument leads to infinite regress (à la Droste effect).

It’s still just an infinite series of substitutions.

That's a failure to reduce, showing that the reduction by substitution is an incomplete evaluation strategy at best. The Y combinator works under call-by-value and other strategies; you can stick it in production code, if you're so inclined.

You don't need cons, car, cdr, etc. They can all be implemented using lambda. For example:

  ;; excuse my possibly hybrid notation
  (defun cons (car cdr)
    (lambda (m)
      (if (eq? m 'car) car
          (if (eq? m 'cdr) cdr
              nil))))
  (defun car (obj) (obj 'car))
  (defun cdr (obj) (obj 'cdr))

This is neat, but doesn't it beg the question a little bit? You've used a conditional here in your definition. Can you define cond using only lambdas? (My apologies if the linked article does this, I haven't made it all the way through yet.)

Yes. You encode true as λx.λy.x and false as λx.λy.y and then (if p then a else b) becomes just (p a b).

See https://en.wikipedia.org/wiki/Church_encoding#Church_Boolean.... That page also has encodings of pairs and lists.

Whoa. That's really cool! Thanks for the link.

The tape is probably more easily represented as a lambda sending a number n to the content of the nth cell

    initial_tape = λn. 0
    read tape idx = tape idx
    write tape idx x = λn. if n = idx then x else (tape n)

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

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.

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/ )

There is an updated version of this tutorial on arxiv: https://arxiv.org/abs/1503.09060

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

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

[2] https://en.wikipedia.org/wiki/Multiple_discovery

[3] https://en.wikipedia.org/wiki/Church–Turing_thesis

It's the frequency illusion (also known as the Baader-Meinhof phenomenon).

https://rationalwiki.org/wiki/Frequency_illusion

also known coloquially as 'blue car syndrome'.

https://www.urbandictionary.com/define.php?term=Blue%20Car%2...

How do we know this is an illusion? Has anyone reproduced the illusion reliably?

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.

I wonder if this correspondence could be used for program transformations/optimizations?

code -tx-> polynomial -tx-> simplification -tx-> [possibly more efficient] code

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/ Discussion: https://news.ycombinator.com/item?id=18099520

[2] Division Algebras and Quantum Theory (John Baez) 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/S009731650...

[4] Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities [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)

[6] Distributive lattices and Stone-space dualities 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://en.wikipedia.org/wiki/Zonohedron

[8] Entanglement Renormalization (G Vidal) https://authors.library.caltech.edu/9242/1/VIDprl07.pdf?hovn... Holography https://en.wikipedia.org/wiki/Holographic_associative_memory

Google Scholar: https://scholar.google.com/scholar?q=related:Yi-GtarGxh0J:sc...

Can you expand on what you mean? What is "the matrix model of computation" and "vectors of unity"?

Which actor model are you talking about? The variants are very different and Hewitt's original paper is mainly referenced for coming up with the name rather and kicking off the field than inventing a usable model.

Type theory is even vaster. Are we talking homotopy type theory? Calculus of constructions? System F?