Специальная математика. Соловьев А.Е. - 71 стр.

-исчисление (нотация, способ записи) формализует понятие функции не как множества или
графика, а как правила.
В основе -исчисления лежит операция аппликации.
Аппликация - применение функции к аргументу (можно применить только известную
функцию).

Язык состоит из:
1. Множества переменных (х1...).
2. Множества констант(с1...).
3. Символа аппликации     .   .
4. Символа абстракции .
5. Символа равенства =.

-терм:
1. Переменная или константа - -терм.
2. Если х - переменная, и М - некоторый -терм, то х.М тоже -терм.
3. Если М и N -термы, то MN тоже -терм.

Формула - любое выражение вида M=N, где M и N -термы.

Замечание. В литературе прикладного плана нередко используется несколько иная терминология и
форма записи.
f = x.x + x
f - название, ранее не названной функции.
 - оператор.
х - аргумент.
.-комбинатор.
х + х - выражение, задающее значение функции.

Аксиомы:
1. M = M.
2. (x.M)N = M {N/x} -редукция.
где {N/x} – подстановка N вместо всех вхождений x в М.
[В альтернативном представлении часто используемая -редукция записывается, например,
так (x.f(x))(a) = f(a)]
3. x.M = y.M при {y/x} -конверсия.
где {у/x} – подстановка у вместо всех вхождений x в М.

Правила вывода:
1. M = N
     N = M.
2.   M = N, N = P
         M = P.
3.   M=N
   PM = PN.
4.   M=N
    MP = NP.
5.    M=N
   x.M = x.N.


                                            — 71 —