Знаймо

Додати знання

приховати рекламу

Цей текст може містити помилки.

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



План:


Введення

Лямбда-числення (λ-числення, лямбда-числення) - формальна система, розроблена американським математиком Алонзо Черчем, для формалізації та аналізу поняття обчислюваності.

λ-числення може розглядатися як сімейство прототипних мов програмування. Їх основна особливість полягає в тому, що вони є мовами вищих порядків. Тим самим забезпечується систематичний підхід до дослідження операторів, аргументами яких можуть бути інші оператори, а значенням також може бути оператор. Мови в цьому сімействі є функціональними, оскільки вони засновані на уявленні про функції або операторі, включаючи функціональну аплікацію та функціональну абстракцію. λ-числення реалізовано Джоном Маккарті в мові Лісп. На початку реалізація ідеї λ-числення була дуже громіздкою. Але в міру розвитку Лісп-технології (що пройшла етап апаратної реалізації у вигляді Лісп-машини) ідеї отримали ясну і чітку реалізацію.


1. Чисте λ-числення

Це найпростіший з сімейства прототипних мов програмування, чисте λ-числення, терми якого, звані також об'єктами (Обами), або λ -термами, побудовані виключно з змінних застосуванням аплікації та абстракції. Спочатку наявності будь-яких констант не передбачається.

2. Аплікація і абстракція

В основу λ-числення покладені дві фундаментальні операції:

  • Аплікація означає застосування чи виклик функції по відношенню до заданого значення. Її зазвичай позначають f \ a , Де f - Функція, а a - Значення. Це відповідає загальноприйнятій в математиці записи f (a) , Яка теж іноді використовується, проте для λ-числення важливо те, що f трактується як алгоритм, який обчислює результат по заданому вхідному значенню. У цьому сенсі аплікація f до a може розглядатися двояко: як результат застосування f до a , Або ж як процес обчислення f \ a . Остання інтерпретація аплікації пов'язана з поняттям β-редукції.
  • Абстракція або λ-абстракція в свою чергу будує функції по заданих виразами. Саме, якщо t \ equiv t [x] - Вираз, вільно містить x , Тоді запис \ \ Lambda x.t [x] означає: λ функція від аргументу x , Яка має вигляд t [x] ) Позначає функцію x \ mapsto t [x] . Таким чином, за допомогою абстракції можна конструювати нові функції. Вимога, щоб x вільно входило в t , Не дуже суттєво - досить припустити, що \ Lambda x.t \ equiv t , Якщо це не так.

3. β-редукція

Оскільки вираз \ Lambda x. 2 \ cdot x + 1 позначає функцію, яка ставить у відповідність кожному x значення 2 \ cdot x + 1 , То для обчислення виразу

(\ Lambda x. 2 \ cdot x + 1) \ 3 ,

в яке входять і аплікація і абстракція, необхідно виконати підстановку числа 3 в терм 2 \ cdot x + 1 замість змінної x . У результаті виходить 2 \ cdot 3 +1 = 7 . Це міркування в загальному вигляді записується як

(\ Lambda x.t) \ a = t [x: = a],

і носить назву β-редукція. Вираз вигляду (\ Lambda x.t) \ a , Тобто застосування абстракції до нікому терму, називається редексом (redex). Незважаючи на те, що β-редукція по суті є єдиною "істотною" аксіомою λ-числення, вона призводить до вельми змістовною і складної теорії. Разом з нею λ-числення має властивість повноти за Тьюрингу і, отже, являє собою найпростіший мова програмування.


4. η-перетворення

η-перетворення висловлює ту ідею, що дві функції є ідентичними тоді і тільки тоді, коли, будучи застосовані до будь-якого аргументу, дають однакові результати. η-перетворення переводить один в одного формули \ Lambda x. \ f x і f (У зворотний бік - тільки якщо x не має вільних входжень в f : Інакше вільна мінлива x після перетворення стане пов'язаної зовнішньої абстракцією).


5. Каррірованіе (каррінг)

Функція двох змінних x і y f (x, y) = x + y може бути розглянута як функція однієї змінної x , Що повертає функцію однієї змінної y , Тобто як вираз \ \ Lambda x. \ lambda y.x + y . Такий прийом працює точно так само для функцій будь арності. Це показує, що функції багатьох змінних можуть бути без проблем виражені в λ-численні і є " синтаксичним цукром ". Описаний процес перетворення функцій багатьох змінних в функцію однієї змінної називається каррінг (також: каррірованіе), на честь американського математика Хаскелл Каррі, хоча першим його запропонував М. І. Шейнфінкель ( 1924).


6. Семантика безтипових λ-числення

Той факт, що терми λ-числення діють як функції, що застосовуються до термів λ-числення (тобто, можливо, до самих себе), призводить до складнощів побудови адекватної семантики λ-числення. Чи можна приписати λ-числення будь-який сенс? Бажано мати безліч D, в яке вкладалося б його простір функцій D → D. У загальному випадку такого D не існує з міркувань обмежень на потужності цих двох множин, D і функцій з D в D: друге має більшу потужність, ніж перше.

Цю трудність подолав Д. С. Скотт, побудувавши поняття області D ( повної решітки [1] або, більш загально, повного частково упорядкованої множини зі спеціальною топологією) і урізавши D → D до безперервних (в наявній топології) функцій [2]. Після цього також стало зрозуміло, як можна будувати денотаціонную семантику мов програмування. Це сталося завдяки тому, що за допомогою конструкцій Скотта можна надати значення також двом важливим конструкцій мов програмування - рекурсії і типам даних.

Для безлічі D, яке було б ізоморфно його простору функцій D → D, є моделі лямбда-числення в теорії множин з самопрінадлежностью (на ці безлічі теорема Кантора про порядок безлічі підмножин вже не діє), доказ непоротіворечівості лямбда-числення в цьому випадку, в семантиці самопрінадлежності, відрізняється стислістю, див. [Чечулін].


7. Зв'язок з рекурсивними функціями

Рекурсія - це визначення функції через себе; на перший погляд, лямбда-числення не дозволяє цього, але це враження оманливе. Наприклад, розглянемо рекурсивну функцію, яка обчислює факторіал :

f (n) = 1, if n = 0; else n f (n - 1).

В лямбда-численні, функція не може безпосередньо посилатися на себе. Тим не менш, функції може бути переданий параметр, пов'язаний з нею. Як правило, цей аргумент стоїть на першому місці. Зв'язавши його з функцією, ми отримуємо нову, вже рекурсивну функцію. Для цього, аргумент, який посилається на себе (тут позначений як r), обов'язково повинен бути переданий в тіло функції.

g: = λr. λn. (1, if n = 0; else n (rr (n-1)))
f: = gg

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

Y = λg. (Λx.g (xx)) (λx.g (xx))

В лямбда-численні, Y g - нерухома точка g; продемонструємо це:

Y g
λh. ((λx.h (xx)) (λx.h (xx))) g
(Λx.g (xx)) (λx.g (xx))
g ((λx.g (xx)) (λx.g (xx)))
g (Y g).

Тепер, щоб визначити факторіал, як рекурсивну функцію, ми можемо просто написати g (Y g) n, де n - число, для якого обчислюється факторіал. Нехай n = 4, отримуємо:

 g (Y g) 4 (λfn. (1, if n = 0; and n (f (n-1)), if n> 0)) (Y g) 4 (λn. (1, if n = 0 ; and n ((Y g) (n-1)), if n> 0)) 4 1, if 4 = 0; and 4 (g (Y g) (4-1)), if 4> 0 4 (g (Y g) 3) 4 (λn. (1, if n = 0; and n ((Y g) (n-1)), if n> 0) 3) 4 (1, if 3 = 0; and 3 (g (Y g) (3-1)), if 3> 0) 4 (3 (g (Y g) 2)) 4 (3 (λn. (1 , if n = 0; and n ((Y g) (n-1)), if n> 0) 2)) 4 (3 (1, if 2 = 0; and 2 (g (Y g ) (2-1)), if 2> 0)) 4 (3 (2 ​​ (g (Y g) 1))) 4 (3 (2 ​​ (λn. (1, if n = 0 ; and n ((Y g) (n-1)), if n> 0) 1))) 4 (3 (2 ​​ (1, if 1 = 0; and 1 ((Y g) ( 1-1)), if 1> 0))) 4 (3 (2 ​​ (1 ((Y g) 0)))) 4 (3 (2 ​​ (1 ((λn. ( 1, if n = 0; and n ((Y g) (n-1)), if n> 0) 0)))) 4 (3 (2 ​​ (1 (1, if 0 = 0 ; and 0 ((Y g) (0-1)), if 0> 0)))) 4 (3 (2 ​​ (1 (1)))) 24 

Кожне визначення рекурсивної функції може бути представлено як нерухома точка відповідної функції, отже, використовуючи Y, кожне рекурсивне визначення може бути виражене як лямбда-вираз. Зокрема, ми можемо визначити віднімання, множення, порівняння натуральних чисел рекурсивно.


8. У мовах програмування

У мовах програмування під "λ-обчисленням" часто розуміється механізм " анонімних функцій "- callback -функцій, які можна визначити прямо в тому місці, де вони використовуються, і які мають доступ до локальних змінних поточної функції.


Цей текст може містити помилки.

Схожі роботи | скачати

Схожі роботи:
Типізовані лямбда-числення
Лямбда
Лямбда-вирази
Лямбда-Баріон
Лямбда-матриці
Лямбда-точка
Лямбда-куб
Модель Лямбда-CDM
© Усі права захищені
написати до нас
Рейтинг@Mail.ru