MathOverflow Stack Exchange
MathOverflow Stack Exchange

Questions tagged [lambda-calculus]

For questions on the formal system in mathematical logic for expressing effective functions, programs and computation, and proofs, using abstract notions of functions and combining them through binding and substitution.

Lambda Calculus

Its dynamics is a rewriting system representing computation by mean of the beta-reduction, that substitutes each occurrence of the variable with the argument term. From this operational point of view, it represents the ideal formal model of a functional programming language and it can be enriched with constant values and datatypes. Such a typed restriction constitutes the bridge across logic's proof-theory and computer science's theory of computability known as the Curry-Howard correspondence: a term is a proof of its type formula.

Bibliography

  1. Henk Barendregt, Lambda Calculus. Its Syntax and Semantics, 1981. The monograph of the subject.
81 questions
7
votes
3 answers

Relationship of lambda calculus to the rest of math

I just started reading "The calculi of lambda conversion" by Church. Church defines functions like: id x = x, and says the domain and range are understood to be as permissible as possible. Permitting even itself, id id = id In my experience, I've…
Polymer
  • 181
1
vote
1 answer

Selection terms in the untyped lambda calculus

In the untyped $\lambda$-calculus, are there terms $S$ and $T$ such that for any $n$ and any terms $t_1, \dotsc, t_n$, $$S(T(t_1)\dots(t_n)) \twoheadrightarrow_{\beta} t_1$$ Of course, if $n$ is fixed or known in advance, then such terms $S$ and $T$…
provocateur
  • 332