λ-calculus

Summary

Rules

mostly for omitting extra parentheses

Concept

Untyped lambda calculus

• everything is a λ-term

Free and Bound variables

• application creates a bound variable
• rest within the term are free

Substitution

• substituting free occurrences of variables(at the variable level)

α-conversion

• avoid situations where the save variable is both free and bound in an expression

rename bound variables in λ-term such that they differ from free variables

Identity

• returns the input

Little ω

Application

Free variables of a lambda term