www.wikidata.uk-ua.nina.az

Лямбда числення Ля мбда чи слення або λ чи слення формальна система що використовується в теоретичній кібернетиці для до

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

Ля́мбда-чи́слення, або λ-чи́слення — формальна система, що використовується в теоретичній кібернетиці для дослідження визначення функції, застосування функції, та рекурсії. Це числення було запропоноване Алонсо Черчем та Стівеном Кліні в 1930-ті роки, як частина більшої спроби розробити базис математики на основі функцій, а не множин (задля уникнення таких перешкод, як Парадокс Рассела). Однак Парадокс Кліні-Россера[en] демонструє, що лямбда-числення не здатне уникнути теоретико-множинних парадоксів. Незважаючи на це, лямбда-числення виявилось зручним інструментом в дослідженні обчислюваності функцій, та лягло в основу парадигми функціонального програмування.

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

Ядро λ-числення ґрунтується трохи більше ніж на визначені змінних, області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто, семантика мови може бути визначена на основі еквівалентності виразів (або термів) самої мови.

Визначення лямбда-виразів Редагувати

Множину λ-виразів можна визначити індуктивно таким чином:

  • будь-яка змінна — це λ-вираз;
  • -абстракція  — це λ-вираз, якщо x — це змінна, а  — λ-вираз;
  • аплікація  — це λ-вираз, якщо та  — λ-вирази.

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

На цій множині ми визначаємо відношення , що називається бета-редукція:

,

де означає, що вираз підставляється всюди замість змінної x у виразі .

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

Ремарка: Як і у випадку логіки першого порядку, важливо слідкувати за вільними змінними, коли йдеться про абстракцію та підстановки.

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

Хоча дужки таки не пропадають. Вони використовуються для групування. Наприклад математичний вираз в лямбда-численні записується як .

Якщо вираз містить змінну, то він може описувати функцію, як залежність свого значення від значення змінної, наприклад . Лямбда-числення має спеціальний синтаксис, який не зобов'язує задавати ім'я функції (як для ). Для запису функції переводимо вираз в правій частині в префіксну форму (), і дописуємо спереду «». Отримуємо . Грецька літера має роль, подібну до тої що має слово «function» в деяких мовах програмування. Вона вказує читачу що змінна після неї — не частина виразу, а формальний параметр функції, що задається. Крапка після параметра позначає початок тіла функції.

Мова Приклад
Лямбда-числення
Pascal 
function f(x: integer): integer begin f:= 3*x end;
(не зовсім лямбда-вираз, оскільки є назва функції, але суть та ж)
Lisp 
(lambda (x) (* 3 x))
Python 
lambda x: x*3
C++11 
 [](int x) { return x * 3 }
Swift 
  { return $0 * 3 }

Щоб застосувати створену функцію до якихось аргументів, її просто підставляють в вираз, наприклад так: . Дужки навколо функції потрібні, щоб чітко знати де вона закінчується. Якщо б ми написали то це могло б сприйматись як функція, що повертає , якщо * — тернарний оператор, або як синтаксична помилка, якщо * — завжди бінарне.

Для зручності ми можемо позначити нашу функцію якоюсь буквою:

і потім просто писати .

Залишилось розглянути ще один цікавий випадок:

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

Можна записати це в скороченій формі, без дужок:

Чи ще коротше:

Наступний розділ цієї статті пояснює те ж саме, але трохи в іншому стилі.

Нотація λ-числення Редагувати

Функція n змінних в λ-численні позначається так:

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

Застосування функції (або абстракції) з назвою до виразу з аргументами позначається:

Де не обов'язково має дорівнювати .

Особливим випадком є застосування абстракції до абстрагованих змінних, що повертає тіло абстракції:

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

Використовуючи цю нотацію, застосування n-арної абстракції до r аргументів, наведене вище, матиме такий вигляд:

Такий підхід скорочує побудову виразів λ-числення до наступних синтаксичних правил:

Тобто, λ-вираз це: або змінна, що позначається v, константа c, застосування λ-виразу до λ-виразу , або абстракція змінної v від λ-виразу відповідно.

λ-числення називається чистим, якщо множина констант порожня. В іншому випадку числення називається аплікативним.

Див. також Редагувати

Примітки Редагувати

  1. Henk Barendregt 1997
  2. Kluge 2005, сторінка 51.
  3. M.H. Sorensen and P. Urzyczyn «Lectures on the Curry-Howard Isomorphism» (2006)

Література Редагувати


Це незавершена стаття про інформаційні технології.
Ви можете допомогти проєкту, виправивши або дописавши її.
Це незавершена стаття з математики.
Ви можете допомогти проєкту, виправивши або дописавши її.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри
Дата публікації:
Lya mbda chi slennya abo l chi slennya formalna sistema sho vikoristovuyetsya v teoretichnij kibernetici dlya doslidzhennya viznachennya funkciyi zastosuvannya funkciyi ta rekursiyi Ce chislennya bulo zaproponovane Alonso Cherchem ta Stivenom Klini v 1930 ti roki yak chastina bilshoyi sprobi rozrobiti bazis matematiki na osnovi funkcij a ne mnozhin zadlya uniknennya takih pereshkod yak Paradoks Rassela Odnak Paradoks Klini Rossera en demonstruye sho lyambda chislennya ne zdatne uniknuti teoretiko mnozhinnih paradoksiv Nezvazhayuchi na ce lyambda chislennya viyavilos zruchnim instrumentom v doslidzhenni obchislyuvanosti funkcij ta lyaglo v osnovu paradigmi funkcionalnogo programuvannya 1 Lyambda chislennya mozhna rozglyadati yak idealizovanu minimalistichnu movu programuvannya v comu sensi lyambda chislennya podibne do mashini Tyuringa inshoyi minimalistichnoyi abstrakciyi zdatnoyi viznachati bud yakij algoritm Vidminnist mizh nimi polyagaye v tomu sho lyambda chislennya vidpovidaye funkcionalnij paradigmi viznachennya algoritmiv a mashina Tyuringa natomist imperativnij Tobto mashina Tyuringa maye pevnij stan perelik simvoliv sho mozhut zminyuvatis iz kozhnoyu nastupnoyu instrukciyeyu Na vidminu vid cogo lyambda chislennya unikaye staniv vono maye spravu z funkciyami kotri otrimuyut znachennya parametriv ta povertayut rezultati obchislen mozhlivo inshi funkciyi ale ne sprichinyayut do zmini vhidnih danih stalist Yadro l chislennya gruntuyetsya trohi bilshe nizh na viznacheni zminnih oblasti vidimosti zminnih ta vporyadkovanomu zamishenni zminnih virazami l chislennya ye zamknenoyu movoyu tobto semantika movi mozhe buti viznachena na osnovi ekvivalentnosti viraziv abo termiv samoyi movi 2 Zmist 1 Viznachennya lyambda viraziv 2 Notaciya l chislennya 3 Div takozh 4 Primitki 5 LiteraturaViznachennya lyambda viraziv RedaguvatiMnozhinu l viraziv mozhna viznachiti induktivno takim chinom 3 bud yaka zminna ce l viraz l displaystyle lambda nbsp abstrakciya l x M displaystyle lambda x M nbsp ce l viraz yaksho x ce zminna a M displaystyle M nbsp l viraz aplikaciya M N displaystyle MN nbsp ce l viraz yaksho M displaystyle M nbsp ta N displaystyle N nbsp l virazi Intuyitivno abstrakciyi vidpovidayut funkciyam a aplikaciyi yih zastosuvannyu Osoblivistyu lyambda chislennya ye te sho argumenti funkcij viznachenih takim chinom ce tezh funkciyi Napriklad l x x displaystyle lambda x x nbsp ce l viraz sho vidpovidaye funkciyi identichnosti a l x x M displaystyle lambda x xM nbsp ce aplikaciya ciyeyi funkciyi do M displaystyle M nbsp u vipadku koli M displaystyle M nbsp ce tezh l viraz Na cij mnozhini mi viznachayemo vidnoshennya b displaystyle rightarrow beta nbsp sho nazivayetsya beta redukciya l x M N b M x N displaystyle lambda xM N rightarrow beta M x N nbsp de M x N displaystyle M x N nbsp oznachaye sho viraz N displaystyle N nbsp pidstavlyayetsya vsyudi zamist zminnoyi x u virazi M displaystyle M nbsp Todi u poperednomu prikladi matimemo l x x M b x x M M displaystyle lambda x x M rightarrow beta x x M M nbsp Yak i ochikuvano zastosuvannya funkciyi identichnosti do pevnogo virazu povertaye cej viraz Remarka Yak i u vipadku logiki pershogo poryadku vazhlivo slidkuvati za vilnimi zminnimi koli jdetsya pro abstrakciyu ta pidstanovki l virazi ne taki skladni yak zdayutsya na pershij poglyad Prosto treba zviknuti do prefiksnoyi formi zapisu Bilshe nemaye ni infiksnih displaystyle nbsp ni postfiksnih x 2 displaystyle x 2 nbsp operacij Krim togo argumenti funkcij prosto zapisuyutsya v spisok pislya funkciyi rozdileni propuskom Tomu vsyudi de matematiki pishut sin x displaystyle sin x nbsp v lyambda chislenni pishut sin x displaystyle sin x nbsp Tak samo zamist x y displaystyle x y nbsp pishut x y displaystyle x y nbsp a zamist x 2 displaystyle x 2 nbsp x x displaystyle x x nbsp Hocha duzhki taki ne propadayut Voni vikoristovuyutsya dlya grupuvannya Napriklad matematichnij viraz sin x 4 displaystyle sin x 4 nbsp v lyambda chislenni zapisuyetsya yak sin x 4 displaystyle sin x 4 nbsp Yaksho viraz mistit zminnu to vin mozhe opisuvati funkciyu yak zalezhnist svogo znachennya vid znachennya zminnoyi napriklad f x 3 x displaystyle f x 3x nbsp Lyambda chislennya maye specialnij sintaksis yakij ne zobov yazuye zadavati im ya funkciyi yak dlya f displaystyle f nbsp Dlya zapisu funkciyi perevodimo viraz v pravij chastini v prefiksnu formu 3 x displaystyle 3 x nbsp i dopisuyemo speredu l x displaystyle lambda x nbsp Otrimuyemo l x 3 x displaystyle lambda x 3 x nbsp Grecka litera l displaystyle lambda nbsp maye rol podibnu do toyi sho maye slovo function v deyakih movah programuvannya Vona vkazuye chitachu sho zminna pislya neyi ne chastina virazu a formalnij parametr funkciyi sho zadayetsya Krapka pislya parametra poznachaye pochatok tila funkciyi Mova PrikladLyambda chislennya l x 3 x displaystyle lambda x 3 x nbsp Pascal function f x integer integer begin f 3 x end ne zovsim lyambda viraz oskilki ye nazva funkciyi ale sut ta zh Lisp lambda x 3 x Python lambda x x 3C 11 int x return x 3 Swift return 0 3 Shob zastosuvati stvorenu funkciyu do yakihos argumentiv yiyi prosto pidstavlyayut v viraz napriklad tak l x 3 x 4 displaystyle lambda x 3 x 4 nbsp Duzhki navkolo funkciyi potribni shob chitko znati de vona zakinchuyetsya Yaksho b mi napisali l x 3 x 4 displaystyle lambda x 3 x4 nbsp to ce moglo b sprijmatis yak funkciya sho povertaye 3 x 4 12 x displaystyle 3 x 4 12x nbsp yaksho ternarnij operator abo yak sintaksichna pomilka yaksho zavzhdi binarne Dlya zruchnosti mi mozhemo poznachiti nashu funkciyu yakoyus bukvoyu F l x 3 x displaystyle F equiv lambda x 3 x nbsp i potim prosto pisati F 4 displaystyle F4 nbsp Zalishilos rozglyanuti she odin cikavij vipadok N l y l x y x displaystyle N equiv lambda y lambda x y x nbsp yaksho peredati N 3 displaystyle N 3 nbsp to vona poverne nashu staru funkciyu l x 3 x displaystyle lambda x 3 x nbsp Tobto N 3 displaystyle N3 nbsp pracyuye yak F displaystyle F nbsp yakij mi mozhemo peredati napriklad 4 zapisavshi ce yak N 3 4 displaystyle N 3 4 nbsp Abo mi mozhemo rozglyadati yiyi yak funkciyu vid dvoh argumentiv Mozhna zapisati ce v skorochenij formi bez duzhok l y l x x y displaystyle lambda y lambda x x y nbsp Chi she korotshe l y x x y displaystyle lambda y x x y nbsp Nastupnij rozdil ciyeyi statti poyasnyuye te zh same ale trohi v inshomu stili Notaciya l chislennya RedaguvatiFunkciya n zminnih v 1 v n displaystyle v 1 dots v n nbsp v l chislenni poznachayetsya tak f l v 1 v n e 0 displaystyle f lambda v 1 ldots v n e 0 nbsp Simvol f displaystyle f nbsp v livij chastini cogo rivnyannya zadaye nazvu funkciyi abo identifikator za yakim mozhna posilatis na cyu funkciyu v inshih virazah Viraz u pravij chastini rivnyannya viznachaye abstrakciyu zminnih v 1 v n displaystyle v 1 ldots v n nbsp vid virazu e 0 displaystyle e 0 nbsp kotrij nazivayetsya tilom abstrakciyi Konstrukciya l v 1 v n displaystyle lambda v 1 ldots v n nbsp ye abstraktorom poyavi vilnih zminnih v 1 v n displaystyle v 1 dots v n nbsp v tili funkciyi e 0 displaystyle e 0 nbsp Zastosuvannya funkciyi abo abstrakciyi z nazvoyu f displaystyle f nbsp do virazu z r displaystyle r nbsp argumentami e 1 e r displaystyle e 1 ldots e r nbsp poznachayetsya f e 1 e r l v 1 v n e 0 e 1 e r displaystyle fe 1 ldots e r lambda v 1 ldots v n e 0 e 1 ldots e r nbsp De r displaystyle r nbsp ne obov yazkovo maye dorivnyuvati n displaystyle n nbsp Osoblivim vipadkom ye zastosuvannya abstrakciyi do abstragovanih zminnih sho povertaye tilo abstrakciyi l v 1 v n e 0 v 1 v n e 0 displaystyle lambda v 1 ldots v n e 0 v 1 ldots v n e 0 nbsp Zadlya sproshennya v l chislenni rozglyadayutsya funkciyi vid odniyeyi zminnoyi Yak bulo pokazano u vinahodi Shejnfinkelya ta Karri n arni abstrakciyi mozhna predstavlyati u viglyadi n kratnogo vkladennya unarnih abstrakcij tobto f l v 1 v n e 0 l v 1 l v 2 l v n e 0 displaystyle f lambda v 1 ldots v n e 0 equiv lambda v 1 lambda v 2 ldots lambda v n e 0 nbsp Vikoristovuyuchi cyu notaciyu zastosuvannya n arnoyi abstrakciyi do r argumentiv navedene vishe matime takij viglyad f e 1 e r f e 1 e 2 e r displaystyle f e 1 ldots e r dots f e 1 e 2 e r nbsp Takij pidhid skorochuye pobudovu viraziv l chislennya do nastupnih sintaksichnih pravil e s v c e 0 e 1 l v e 0 displaystyle e s v c e 0 e 1 lambda v e 0 nbsp Tobto l viraz ce abo zminna sho poznachayetsya v konstanta c zastosuvannya l virazu e 0 displaystyle e 0 nbsp do l virazu e 1 displaystyle e 1 nbsp abo abstrakciya zminnoyi v vid l virazu e 0 displaystyle e 0 nbsp vidpovidno l chislennya nazivayetsya chistim yaksho mnozhina konstant porozhnya V inshomu vipadku chislennya nazivayetsya aplikativnim Div takozh RedaguvatiTipizovane lyambda chislennya Sistema F Funkcijne programuvannya Pi chislennya Mashina Tyuringa Pidstanovka Lyambda kubPrimitki Redaguvati Henk Barendregt 1997 Kluge 2005 storinka 51 M H Sorensen and P Urzyczyn Lectures on the Curry Howard Isomorphism 2006 Literatura RedaguvatiAchim Jung A Short Introduction to the Lambda Calculus Arhivovano 23 kvitnya 2021 u Wayback Machine PDF Henk Barendregt The Bulletin of Symbolic Logic Volume 3 Number 2 June 1997 The Impact of the Lambda Calculus in Logic and Computer Science W Kluge 2005 Abstract Computing Machines The Lambda Calculus perspective Springer Verlag ISBN 3 540 21146 2 Raul Rojas A Tutorial Introduction to the Lambda Calculus Arhivovano 1 listopada 2013 u Wayback Machine angl PDF Wolfengagen V E Combinatory logic in programming Computations with objects through examples and exercises 2 nd ed M Center JurInfoR Ltd 2003 x 337 s ISBN 5 89158 101 9 nbsp Ce nezavershena stattya pro informacijni tehnologiyi Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi nbsp Ce nezavershena stattya z matematiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi Otrimano z https uk wikipedia org w index php title Lyambda chislennya amp oldid 37263107