what is lambda Calculus?

[u/NationalStill6968]

/r/mathematics/comments/1xe176v/what_is_lambda_calculus/

[u/joao_rosac]

O Cálculo Lambda é um sistema matemático criado por Alonzo Church nos anos 1930, a ideia principal é usar funções anônimas. Tem duas regras apenas, ele foi provado matematicamente como tendo exatamente o mesmo poder de resolução da Máquina de Turing, quase como o modelo teórico fundamental do software (focado em funções puras), enquanto a máquina de Turing representa o hardware (focado em memória e estado). Na prática, esse modelo baseou a criação do paradigma da programação funcional (como em Lisp e Haskell) e originou o conceito de expressões lambda — as famosas funções anônimas (como as arrow functions do JavaScript).

[u/Vigintillionn]

The Lambda Calculus is a tiny formal system, invented by Alonzo Church in the 1930s? (correct me if I'm wrong). And it's used to describe computation using nothing but functions. It's very minimal, yet it can express any computation a computer can (aka it's Turing-complete).

It has just three building blocks, a variable like `x`, function definitions (aka abstractions) `λx. x + 1` is a function that takes `x` and returns `x+1` and function application `(λx. x + 1) 6` applies that function to 6 giving 7 (six-seven, sorry).

Computation and transformation of expressions happen through three rewrite rules:
- alpha conversion (renaming) means you can rename a bound variable without changing the meaning, eg. `λx. x + 1` becomes `λy. y + 1`
- beta reduction (applying a function) is the actual computation where you replace the parameter with the argument inside the body, eg. `(λx. x + 1) 6` becomes `6 + 1 = 7`
- eta reduction means a function that just passes its argument to another function is the same as that function, eg. `λx. f x` is the same as `f`

Lambda calculus doesn't really apply to turing machines, tehy are just two separate models of computation. But they are proven to be equally powerful: anything a Turing machine can compute can be expressed in lambda calculus and computed via beta reduction (and vice verse). This equivalence was proven by Turing, and it underpins the Church–Turing thesis: the claim that these models capture everything that is mechanically computable. You can see this intuitively if you think of the beta reduction of lambda calculus as a state transition of a Turing machine. One cool thing to note is that both Church and Turing came up with this around the same time, both trying to solve Hilbert's Etscheidungsproblem (the decision problem), and both proved it unsolvable by showing that certain questions about computations (like whether a program halts) can’t be decided.

Actually after writing his paper Turing actually went to go do his PhD under Church!

Both lambda calculus and Turing machines were very influential to programming languages. Turing machines more so for hardware and lambda calculus for languages. Lisp was directly based on lambda calculus, and so were later functional languages like ML, OCaml and Haskell. The lambda calculus also produced a family of formal systems that basically underlie type checkers, stuff like System F (the theory behind generics) and Hindley-Milner (type inference in Haskell and OCaml) were designed for lambda-calculus based languages. Many compilers translate source code first to a lambda-calculus style intermediate language for optimizations (inlining is just beta reductions AOT). In research around PL and compilers, we typically model language features as a small extension of lambda calculus and writing proofs in assistens like Coq, Agda and Lean you are basically doing lambda expressions as the Curry-Howard correspondance shows that typed lambda expressions and logical proofs are the same thing!

[u/MitchAlsup → u/Vigintillionn]

"Both lambda calculus and Turing machines were very influential to programming languages. Turing machines more so for hardware and lambda calculus for languages."

Touring machines are more closely related to what we call Hardware today, as they feature explicit storage.

Lambda calculators are more closely related to dynamic programming languages {Lisp, Smalltalk, ...}