Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Ламбда-исчисление - это теория, рассматривающая функции как правила, а не как графики и фактически выделяющая вычислительный аспект при введении функций. Чёрч предложил использовать ламбда-исчисление для формализации понятия эффективной вычислимости. Тьюринг показал, что вычислимость по Тьюрингу эквивалентна ламбда-вычислимости. Таким образом, несмотря на свой очень простой синтаксис, ламбда-исчисление способно реализовать все механически вычислимые функции. Синтаксис ламбда-исчисления. Выражение в ламбда-исчислении представлено в префиксной форме, т.е. вначале располагается оператор, например, вместо а+Ь пишется +аЬ, а вместо aAj+bxc пишется (+(/ab)(xbc)). Все программы представляются в виде выражений, а процесс выполнения программы заключается в определении значения этого выражения и это называется оценкой выражения. Оценка выражения производится повторением операции выбора и упрощением тех частей этого выражения, которые можно упростить. Такая часть выражения называется редексом, а операция упрощения называется редукцией. Процесс редукции завершается, когда выражение, преобразованное редукцией, не содержит больше редекса. Выражение, не содержащее редекса, называется нормальной формой. Например, при оценке выражения (+(/62)(х25)) сначала выбираются редексы и упрощаются соответственно до 3 и 10. Полученное выражение (+3 10) также является редуцируемым, поэтому имеем (+3 10)^13. Результат (оценка выражения) 13 невозможно упростить, поэтому он считается нормальной формой. Применение функции. Применение функции/к аргументу х обозначается как (fx). Функция от нескольких аргументов представляется, например, следующим образом if{x,y,z)). Однако функцию от нескольких аргументов можно интерпретировать как результат синтеза функций от одного аргумента. Например (+3 4) можно интерпретировать как (+3)4, т.е. как прибавление тройки к аргументу 4. В ламбда-исчислении вводятся специальные операции как ламбда- абстракция и у^- преобразование. Дадим их краткое описание. Ламбда-абстракция - это одно выражение, определяющее функцию. Например, выражение (Ях.+х1) 174