(no subject)

Лямбда-исчисление - это построение машин по переработке символьных последовательностей. Отсюда понятно, почему оно эквивалентно тому, что умеет делать машина Тьюринга. Возьмём, например, лямбда-функцию
λxyz.zzyxyx
Слева (от λ до точки) - что ожидается на входе, справа - что будет на выходе. Вместо одиночных букв на вход можно подавать последовательности, это называется β-редукцией. То есть, если функции λxyz.zzyxyx подать на вход (aa)(bb)(cc), то получим на выходе ccccbbaabbaa. Скобки нужны, чтобы отделять, что идёт вместо x, что вместо y, что вместо z. Поэтому λ-функции называются "комбинаторами" - они комбинируют из букв входа последовательность букв на выходе. Функции можно подать на вход её саму.

Второе занятие семинара

Записали формальные основы синтаксиса лямбда-исчисления, поговорили про понятие семантики, комбинаторы, их связь с парадоксом Рассела. Y-комбинатор, как один из видов парадокса Рассела и подозрительность бестипового лямбда-исчисления. Затем перешли к введению типов по Чёрчу, понятию контекста (есть такие, контекстные грамматики), аксиомам для выведения типов выражений. Я отвлёкся на попытку понять, как же из этих аксиом у кого-то всё-таки получается вывести тип и пропустил пару теорем - про единственность типа и независимость его от переименования переменных. Ещё, вроде, была теорема, что если у выражения удаётся вывести тип, то в нём нет свободных переменных. Теперь буду читать про это до следующего четверга.