What is lambda calculus?

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.

What is the syntax for lambda abstraction?

λx.M Where x is a variable and M is a lambda term.

How is function application represented in lambda calculus?

(M N) Where M and N are lambda terms.

What are free variables in lambda calculus?

Variables in a lambda term that are not bound by a lambda abstraction.

What are bound variables in lambda calculus?

Variables in a lambda term that are bound by a lambda abstraction.

What is alpha conversion in lambda calculus?

The renaming of bound variables in a lambda term. It states that (λx.M) is equivalent to (λy.M[x:=y]) if y is not free in M.

What is beta reduction in lambda calculus?

The process of applying a function to its argument. It involves substituting the argument for the bound variable in the function body.

What are Church numerals in lambda calculus?

A representation of natural numbers using lambda terms. The Church numeral for n is a function that takes a function f as argument and returns the n-fold composition of f.

What is the Y combinator in lambda calculus?

A higher-order function that finds fixed points of other functions, enabling recursive definitions in the lambda calculus.

What is a normal form in lambda calculus?

A lambda term to which no more beta reductions can be applied.