Лямбда-исчисление как формальная система

λ-исчисление — это исчисление безымянных (анонимных) функций. Как и всякая формальная система, оно включает

• синтаксис представления выражений (правильно построенных формул),
• набор правил вывода для синтаксического преобразования выражений.

Алфавит состоит из следующих символов:

• x, y, z,... - переменные,
• λ - aбстрактор,
• ( ) - скобки,
• = - равенство.