Анотація: В лекції розглядаються основи лямбда числення. Ця теорія дозволяє краще розуміти властивості агентів і їх застосування. У лекції докладно обговорюються питання, пов'язані з перетворенням функцій, перейменуванням змінних, підстановкою. Вивчаються дві основні операції, застосовні до лямбда-виразів, - бета-редукція і альфа-перетворення. Обговорюється зв'язок теорії з практикою програмування в Eiffel та іншими мовами програмування.
Лямбда-числення
Ми вже познайомилися з основами агентів і навіть деякими деталями. Сподіваюся, ви відчули міць цього механізму та можливі області його застосування.
Фактично можливий наступний рівень гнучкості. Перш ніж його освоїти, слід розглянути математичні ідеї, що лежать в основі. Лямбда-числення дасть нам більш глибоке розуміння агентів, зокрема, концепції відкритих і закритих операндів.
Ця чудова теорія розроблена в 1930 році ще до появи комп'ютерів. Через 30 років виявилося, що вона дає ясну і міцну основу багатьох концепцій мов програмування. Це пожвавило інтерес до лямбда-числення, і воно стало плідної областю досліджень.
Лямбда-числення дає нам теорію поняття функції. Воно займається основами поняття, не вивчаючи спеціальні види функцій, таких як функції тригонометрії або функції дійсних змінних. Тут вивчається сама ідея функції як механізму, що приймає аргументи і виробляє результат. Це математичне поняття, але воно дуже схоже з поняттям програми в комп'ютерних науках. Теорія дозволяє нам краще зрозуміти, що є областю визначення змінної, яка роль аргументів, а також можливість розглядати програму як об'єкт, відповідаючи цілям цієї лекції - перетворити програми в агенти.
Операції над функціями
Основна ідея проста: нотація і правила трансформації дозволяють нам поводитися з функціями так само, як і з іншими математичним об'єктами.
Для заданих двох чисел a і b можна утворювати різні комбінації, наприклад: a + b або sin (a) + cos (b), використовуючи функції з добре визначеною сигнатурою.
sin: REAL → REAL - Сенс: Для будь-якого аргументу типу REAL функція sin - виробляє результат типу REAL "+": [REAL х REAL] → REAL - х декартовій твір, квадратні дужки - застосовуються для угруповання аргументів
Чи можна "грати" в подібні гри не з числами, а з функціями? Навіть в елементарної операції ми зустрічаємося з операціями над функціями. Якщо f і g - це функції з відповідними сигнатурами, то можна задати їх композицію, яка записується як gof або f; g (нотація, яку ми будемо використовувати, оскільки вона явно вказує порядок виконання). Результатом композиції є функція h (x), така, що h (x) = g (f (x)) для будь-якого застосовного аргументу x. Композиція є такою ж операцією над функціями, як "+" над числами.
Лямбда-числення дозволить нам визначити над функціями багато операцій.
Ми можемо продовжити сходження по сходах абстракцій. Композиція функцій є функцією, тому і до неї може бути застосована композиція. Нехай X, Y, Z - деякі множини і задані сигнатури функцій f і g:
Композиція цих функцій, названа вище функцією h, має сигнатуру X → Z. Визначимо тепер композицію ";" як функцію, якої передаються два аргументи f і g і яка виробляє результат h. Ця функція має сигнатуру:
";": [[X → Y] х [Y → Z]] х [X → Z] Лістинг 6.1.
Ми можемо продовжити визначення функцій, які оперують функціями, які, в свою чергу, оперують функціями, і так далі. Лямбда-числення дає нам словник і правила - теорію - для роботи з такими функціями на довільному рівні.
Лямбда-вирази
Перш за все, нам необхідна проста нотація для визначення функцій. Будемо припускати, що у нас є базис з функцій, таких як "+", над цілими і речовими. Це припущення робиться для простоти, так як лямбда-числення може бути визначено без посилань на існуючі математичні теорії. символ 
буде, як завжди, означатиме "за визначенням". Визначимо функцію square з сигнатурою
Функція як результат повертає квадрат числа. Її визначення можна поставити відповідним лямбда-виразом:
Права частина визначення є лямбда-виразом, запис якого однозначно дозволяє встановити, що для будь-якого x типу REAL результатом функції буде x * x.
Символ λ (лямбда) - справа угоди, але він дав ім'я всьому підходу. У математичній літературі сигнатуру від визначення функції відокремлює символ точки, але в ОО-програмуванні точка грає іншу важливу роль, тому замість точки застосовується символ "|" вертикальної риси.
Лямбда-визначення функції нагадує її визначення в програмуванні
square (x: REAL): REAL - x в квадраті. do Result: = x * x end Лістинг 6.3.
Як правило, математична нотація завжди компактніше програмістської. У цій нотації змінна, наступна за λ, називається пов'язаної змінної лямбда-вирази, вона подібна до формального аргументу методу.
Подібно імені формального аргументу, ім'я пов'язаної змінної не впливає на зміст виразу і може бути будь-яким. Так що таке визначення задає ту ж саму функцію, яка обчислює квадрат числа:
Це спостереження буде формалізовано нижче, використовуючи поняття альфа-перетворення. Лямбда-вираз може мати більше однієї пов'язаної змінної, потрібно лише, щоб у них були різні імена:
λ x, y: INTEGER | x + y - Функція складання λ x: NATURAL, z: REAL | zx - Нотація для випадку різних типів
Чим добре лямбда-вираз? На перший погляд, замість нього можна було б використовувати вже знайому запис, наприклад, для функції square:
∀ x: REAL | square (x) = x * x Лістинг 6.4.
Різниця в тому, що [6.4] визначає властивості функції, в той час як [6.2] визначає функцію - математичний об'єкт з усіма правами, аналогічно тому, як можна визначити константу π, задавши її значення.
Одним з безпосередніх переваг є можливість визначення функцій вищих порядків, таких як композиція, сигнатура якої задана в [6.1] :
Передбачається, що безлічі X, Y, Z відомі. Так як вони довільні, ми можемо ввести механізм універсальності в лямбда-вираз, як для класів, перетворюючи імена множин в формальні родові параметри. У нашому короткому огляді немає необхідності в такій нотації.
У цьому прикладі вихідне безліч в сигнатурі є декартових твором [X → Y * [Y → Z]; відповідно, лямбда-вираз має дві зв'язані змінні - f і g.
До сих пір кожному визначенню функції лямбда-виразом передувало завдання сигнатури функції, а кожна пов'язана змінна супроводжувалася зазначенням її типу. В принципі, можливо Нетипізовані лямбда-вираз, але ми будемо продовжувати використовувати тільки типізовані, аналогічно тому, як ми використовуємо в програмуванні типізовані мови, такі як Eiffel, підвищуючи читабельність і уникаючи помилок.
Відчуй методологію
оголошення сигнатури
Оголошення сигнатури функції повинно передувати визначення функції лямбда-виразом.
Якщо сигнатура з'являється безпосередньо перед визначенням, то у визначенні можна опускати зв'язані змінні, як в цьому прикладі: