Ноу Інти, лекція, введення в лямбда числення

Анотація: В лекції розглядаються основи лямбда числення. Ця теорія дозволяє краще розуміти властивості агентів і їх застосування. У лекції докладно обговорюються питання, пов'язані з перетворенням функцій, перейменуванням змінних, підстановкою. Вивчаються дві основні операції, застосовні до лямбда-виразів, - бета-редукція і альфа-перетворення. Обговорюється зв'язок теорії з практикою програмування в Eiffel та іншими мовами програмування.

Лямбда-числення

Ми вже познайомилися з основами агентів і навіть деякими деталями. Сподіваюся, ви відчули міць цього механізму та можливі області його застосування.

Фактично можливий наступний рівень гнучкості. Перш ніж його освоїти, слід розглянути математичні ідеї, що лежать в основі. Лямбда-числення дасть нам більш глибоке розуміння агентів, зокрема, концепції відкритих і закритих операндів.

Ця чудова теорія розроблена в 1930 році ще до появи комп'ютерів. Через 30 років виявилося, що вона дає ясну і міцну основу багатьох концепцій мов програмування. Це пожвавило інтерес до лямбда-числення. і воно стало плідної областю досліджень.

Лямбда-числення дає нам теорію поняття функції. Воно займається основами поняття, не вивчаючи спеціальні види функцій, таких як функції тригонометрії або функції дійсних змінних. Тут вивчається сама ідея функції як механізму, що приймає аргументи і виробляє результат. Це математичне поняття, але воно дуже схоже з поняттям програми в комп'ютерних науках. Теорія дозволяє нам краще зрозуміти, що є областю визначення змінної, яка роль аргументів, а також можливість розглядати програму як об'єкт. відповідаючи цілям цієї лекції - перетворити програми в агенти.

Операції над функціями

Основна ідея проста: нотація і правила трансформації дозволяють нам поводитися з функціями так само, як і з іншими математичним об'єктами.

Для заданих двох чисел a і b можна утворювати різні комбінації, наприклад: a + b або sin (a) + cos (b). використовуючи функції з добре визначеною сигнатурою.

Чи можна "грати" в подібні гри не з числами, а з функціями? Навіть в елементарної операції ми зустрічаємося з операціями над функціями. Якщо f і g - це функції з відповідними сигнатурами, то можна задати їх композицію, яка записується як g o f або f; g (нотація, яку ми будемо використовувати, оскільки вона явно вказує порядок виконання). Результатом композиції є функція h (x), така, що h (x) = g (f (x)) для будь-якого застосовного аргументу x. Композиція є такою ж операцією над функціями, як "+" над числами.

Лямбда-числення дозволить нам визначити над функціями багато операцій.

Ми можемо продовжити сходження по сходах абстракцій. Композиція функцій є функцією, тому і до неї може бути застосована композиція. Нехай X. Y. Z - деякі множини і задані сигнатури функцій f і g:

Композиція цих функцій, названа вище функцією h. має сигнатуру X → Z. Визначимо тепер композицію ";" як функцію, якої передаються два аргументи f і g і яка виробляє результат h. Ця функція має сигнатуру:

Ми можемо продовжити визначення функцій, які оперують функціями, які, в свою чергу, оперують функціями, і так далі. Лямбда-числення дає нам словник і правила - теорію - для роботи з такими функціями на довільному рівні.

Лямбда-вирази

Перш за все, нам необхідна проста нотація для визначення функцій. Будемо припускати, що у нас є базис з функцій, таких як "+", над цілими і речовими. Це припущення робиться для простоти, так як лямбда-числення може бути визначено без посилань на існуючі математичні теорії. Символ буде, як завжди, означатиме "за визначенням". Визначимо функцію square з сигнатурою

Функція як результат повертає квадрат числа. Її визначення можна поставити відповідним лямбда-виразом: