Комбінатор нерухомої точки

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

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

Один з найвідоміших (і, ймовірно, з найпростіших) комбінаторів нерухомої точки в Нетипізовані λ-численні називається комбінатором Y. Він був розроблений Хаскелл Каррі і визначається наступним чином:

Необхідно відзначити, що комбінатор Y призначений для використання спільно з обчислювальної стратегією «виклик на ім'я», оскільки вираз (Yg) зациклюється для довільного g в стратегії «виклик за значенням».

Комбінатор нерухомої точки в строгих і нестрогих мовах [ред]

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

У деяких інших системах, наприклад в просто типизированном λ-численні. добре збірний комбінатор нерухомої точки не може бути побудований. У таких системах будь-яка підтримка рекурсії повинна бути явно задана в нотації. В інших системах, таких як просто типізоване λ-числення з доданими рекурсивними типами. комбінатори нерухомої точки можуть бути побудовані, але тип «корисних» комбінаторів (таких, застосування яких завжди повертає значення) може бути забороненим.

Наприклад, в мові програмування Standard ML варіант комбінатора Y для виклику за значенням має тип ∀a.∀b. ((A → b) → (a → b)) → (a → b), в той час як варіант для виклику по імені має тип ∀a. (a → a) → a. Варіант для виклику по імені зациклюється при застосуванні в строгих мовами. оскільки будь-яке застосування Yf завжди розгортається в f (Yf). Далі обчислюється аргумент зовнішньої функції f. як того вимагається стратегія виклику за значенням, і виходить значення f (f (Yf)). Цей процес буде продовжуватися до безкінечності, але значення цього застосування отримано ніколи не буде.

Приклад [ред]

Розглянемо функцію для обчислення факторіала (в нотації А. Черча). Звичайне рекурсивне математичне визначення виглядає так:

Можна розглянути один крок обчислення цієї рекурсії в нотації λ-числення:

F = λf.λx. (ISZERO x) 1 (MULT x (f (PRED x)))

де «f» - параметр для отримання функції обчислення факторіала. Функція F обчислює один крок рекурсії в вищенаведеної формулі. При застосуванні до неї комбінатора нерухомої точки fix вийде наступна послідовність виразів:

Далі можна перейменувати застосування fix (F) в fact. а тому:

fact (n) = (ISZERO n) 1 (MULT n (fact (PRED n)))

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

Інші комбінатори нерухомої точки [ред]

Версія комбінатора Y. яка може бути використана у викликах-по-значенням (визначається за допомогою η-редукції):

Комбінатор Y може бути виражений в комбинаторном базисі SKI наступним чином:

Найпростіший (вимагає найменшу кількість базових комбінаторів для розкладання в базисі) комбінатор нерухомої точки в базисі SK. знайдений Д. Тромп:

Ця запис відповідає наступному λ-вираженню.

Інший комбінатор нерухомої точки знайдений А. Тьюрингом.

Цей комбінатор також имет просту форму для виклику за значенням:

Комбінатори нерухомої точки зустрічаються не так рідко (їх взагалі існує безліч). Деякі використовуються в якості розваг (терм L зустрічається в ньому 26 разів):

Див. Також [ред]