Недавно я изучал расчет лямбда, и у меня много сомнений по поводу сокращения и замены. Что такое альфа- и бета-редукция? А когда и зачем они используются?.
Было бы здорово, если бы кто-нибудь мог рассказать о каких-либо хороших ресурсах по сокращению и замене в лямбда-исчислении.
Бета-редукция - это просто основное правило приложения, используемое для вычислений в рамках лямбда-исчисления. Он применяется путем замены, как показано:
Если бы у вас был лямбда-член: (\x.x) и некоторое значение справа от него: y
Затем вы замените все связанные переменные справа от (.) в вашем лямбда-термине. Связанные переменные — это переменные, соответствующие переменной слева от (.), поэтому в данном случае x.
The reduction would be of the form:
(\x.x)y //y gets bound to all occurences of x to the right of the period
y
Где y привязан ко всем вхождениям x в лямбда-выражении. Это функция тождества.
Альфа-«редукции» обычно называют альфа-эквивалентностью или альфа-правилами перезаписи. Они заявляют, что вы можете изменить имя любого лямбда-терма и связанных с ним переменных без изменения значения выражения.
Например, используя приведенную выше функцию тождества, мы могли бы так же легко записать лямбда-член как (\j.j). Это не изменит результат нашего приложения, как показано ниже:
(\j.j)y //y gets bound to all occurrences of j to the right of the period
y
Что касается учебных ресурсов: страница в Википедии довольно подробная, но нотация тяжелая и, вероятно, потребует нескольких хороших повторных прочтений.
Если вы просто ищете лучшее представление о том, как работает лямбда-исчисление, на большинстве факультетов информатики есть слайды.
Они могут оказаться полезными: http://www.classes.cs.uchicago.edu/archive/2002/winter/CS33600/slides/Lesson2.pdf https://www.utdallas.edu/~gupta/courses/apl/lambda.pdf
