> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/340-lambda-calculi/lambda-calculus/introduction.md).

# Lambda Calculus: Introduction

Considered as the very **minimal programming language**, λ-calculus lacks almost every concept and construction found in PLs; in fact, there are no other values but functions.

This means that LC deals with the first-class functions, such that a function can be taken as an argument of a function, and a function can be returned as a value from a function. Moreover, there is nothing predefined, there is no standard library of routines and anything similar, the evaluation environment is completely empty. There are only the rules for defining a new function and the rules for applying it an argument (that is again a function).

With nothing predefined, you work with a completely blank slate, free to determine for yourself what the various functions you define will represent.

***

Lambda calculus is a formal system for expressing computation. The grammar rules are divided in two parts: function abstraction and function application.

Function abstraction is a function definition, it defines what a function does. A function definition is static, it does nothing by itself. It stays inactive until it is applied.

A function application "computes" a function. When a function is applied to some arguments is when the action really happens; calling a function is a call to action.

For example, using mathematical notation, `f(x) = x + 1` is a function abstraction, but `f(3)` is a function application.

In lambda calculus, the equality sign `=` from function definition is replaced by a dot

To represent a function `f(x) = x + 1` we write `λx.x + 1`. The big difference is that, unlike in math, in LC all functions are anonymous, so there are no external binders (identifiers), like `f` is in the math notation.

In function application, instead of writing `f(x)`, we must give the definition of a function (abstraction) and immediately follow it by the arguments.

In math, `f(5)`, but in the LC, `(λx.x + 1) (5)` (just for illustration, things like numbers do not exist, nothing exists, until defined explicitly).