Ламбда рачун

Ламбда рачун (ознака λ-рачун) је формални систем у математичкој логици за представљање рачунања базираног на апстракцији функција и апликација користећи везивање и супституцију променљиве. Увео га је Алонзо Черч да формулише концепт ефективног рачунања, ламбда рачун је наишо на прве успехе на пољу теорије рачунања, као што је негативан одговор на Хилбертов проблем одлуке. Ламбда рачун је концептуално једноставан универзални модел рачунања (Тјуринг је показао 1937. године^[1] да Тјурингова машина једнака ламбда рачуну у експресивности). Име потиче од грчког слова ламбда (λ) коришћеног да означи везивање променљивих у функцији. Слово је само по себи произвољно и нема никакво специјално значење. Ламбда рачун се учи и користи у рачунарству због своје корисности у приказивању функционалног размишљања и итеративне редукције.^[2]

Због важности појма везивања променљиве и субституције, не постоји само један систем ламбда рачуна, и у пракси постоје "типске" и "нетипске" варијанте. Историјски гледано, најважнији систем је био нетипски ламбда рачун, у којем функција апликације нема рестрикција (појам домена функције није уграђен у систем. У Черч-Тјуринговој тези, нетипски ламбда рачун је подешен да буде могуће израчунати све ефективно израчуниве функције. Типски ламбда рачун је варијација која има рестрикције за функцију апликације, тако да се функција може применити само ако се прихвати улазни тип података.

Данас, ламбда рачун има улогу у много различитих свера, као нпр. у математици, филозофији,^[3] лингвистици,^[4][5] и рачунарству. Још увек се користи у области теорије рачунања, као и Тјурингова машина која је врло важан модел за рачунање. Ламбда рачун је одиграо веома важну улоу у развоју теорије програмских језика. Делови бројача, у ламбда рачуну у рачунарству, су функционални програми, који имплементирају ламбда рачун (повећати неке константе и типове података). Поред програмских језика, лабмда рачун игра улогу у теорији доказа. Главни пример тога је Кари-Хауардова кореспонденција, која даје кореспонденцију између различитих система типова ламбда рачуна и система формалне логике.

Историја ламбда рачуна у математици

Ламбда рачун је увео Алонзо Черч у 1930—им годинама као део истраге о основама математике.^[6][7] Оригинални систем је показан као логички противречан 1935. године када су Стивен Клин и Ј. Б. Росер развили Клин-Росеров парадокс.

Након тога, у 1936. години, Черч је изоловао и објавио само део битан за рачунање, који се данас зове нетипски ламбда рачун.^[8] У 1940. години, он је такође увео рачунски слабији, али логички доследнији систем, знан као једноставни типски ламбда рачун.^[9]

Мотивација

Рачунске функције представљају круцијалан концепт у рачунарству и математици. Ламбда рачун даје једноставу семантику за израчунавање, омогућавајући особине израчунавања да буду формално учене. Ламбда рачун укључује два упрошћавања која чине семантику једноставном. Прво поједностављење је то да Ламбда рачун третира функцију "анонимно", без давања експлицитних имена. На пример, функција 

${\displaystyle \operatorname {square\_sum} (x,y)=x\times x+y\times y}$

може се поново написати у анонимној форми као

${\displaystyle (x,y)\mapsto x\times x+y\times y}$

(чита се као "пар x и y је мапиран у ${\textstyle x\times x+y\times y}$"). Слично,

${\displaystyle \operatorname {id} (x)=x}$

се може написати у анонимној форми ${\textstyle x\mapsto x}$, где је улаз једноставно мапиран у самог себе 

Друго поједностављење је то да ламбда рачун користи само функције једног улаза. Обична функција која захтева два улаза , за инстанцу ${\textstyle \operatorname {square\_sum} }$ (збир квадрата) функције, може се написати као једна еквивалентна функција која прима један улаз, а да излаз враћа другу функцију, која заузврат прима један улаз. На пример,

${\displaystyle (x,y)\mapsto x\times x+y\times y}$

се може написати као

${\displaystyle x\mapsto (y\mapsto x\times x+y\times y)(y)}$

Ова метода, позната и као кариинг, трансформише функцију која узима више аргумената у ланац функција, где свака има један аргумент.

Функционално окружење  ${\textstyle \operatorname {square\_sum} }$ функције са аргументима (5, 2), добијено одједном

${\textstyle ((x,y)\mapsto x\times x+y\times y)(5,2)}$

${\textstyle =5\times 5+2\times 2}$

${\textstyle =29}$,

док процена каријеве верзије захтева још један корак

${\textstyle ((x\mapsto (y\mapsto x\times x+y\times y))(5))(2)}$

${\textstyle =(y\mapsto 5\times 5+y\times y)(2)}$

${\textstyle =5\times 5+2\times 2}$

${\textstyle =29}$

добија се исти резултат.

Ламбда рачун

Ламбда рачун се састоји од програма ламбда услова, који су дефинисани одређеном формалном синтаксом, и сетом трансформацијских правила, који допуштају манипулацију ламбда услова. Ова трансформацијска правила се могу представити као еквивалентна теорија или као операционализам.

Као што је већ описано, све функције у ламбда рачуну су у ствари анонимне функције, тј. немају име. Дозвољавају само једну улазну променљиву, са каријевом верзијом да се убаце функције са неколико променљивих.

Ламбда правила

Синтакса ламбда рачуна дефинише неке изразе као дозвољене изразе ламбда рачуна и неке неважеће, као што су на пример стрингови који се састоје од карактера валидних C програма а неки ипак нису. Дозвољени израз ламбда рачуна се назива ламбда израз.

Следећа три правила дају индуктивну дефиницију која се могу искористити за прављење синтатички исправних ламбда изрази:

• променљива, ${\displaystyle x}$, је сам по себи валидан ламбда израз
• ако је ${\displaystyle t}$ ламбда израз, а ${\displaystyle x}$ је променљива, онда је ${\displaystyle (\lambda x.t)}$ ламбда израз (назива се и  ламбда апстракцијом);
• ако су ${\displaystyle t}$ и ${\displaystyle s}$ ламбда изрази, онда је и ${\displaystyle (ts)}$ ламбда израз (апликација).

Ништа друго није ламбда услов. Ламбда услов је валидан ако и само ако се може добити применом ова три правила. Међутим, неке заграде могу бити изостављене у складу са неким правилима. На пример, спољашње заграде се обично не пишу. 

Ламбда апстракција ${\displaystyle \lambda x.t}$ је дефиниција анонимне функције која може да узме један улаз ${\displaystyle x}$ и замени га у израз ${\displaystyle t}$. На тај начин се дефинишу анонимне функције које узимају x а враћају t. На пример, ${\displaystyle \lambda x.x^{2}+2}$ је ламбда апстракција функције ${\displaystyle f(x)=x^{2}+2}$ користећи израз ${\displaystyle x^{2}+2}$ за ${\displaystyle t}$. Дефиниција функције са ламбда абрстракцијом само "поставља" функцију али је не уводи. Абрстракција везује променљиву ${\displaystyle x}$ у израз ${\displaystyle t}$.

Апликација ${\displaystyle ts}$ представља примену функције ${\displaystyle t}$ на улаз ${\displaystyle s}$, који представља чин позива функције ${\displaystyle t}$ у односу на улаз ${\displaystyle s}$ да би се добио ${\displaystyle t(s)}$.

Не постоји концепт променљивих декларација у ламбда рачуну. У дефиницији као што је ${\displaystyle \lambda x.x+y}$ (i.e. ${\displaystyle f(x)=x+y}$), ламбда рачун третира ${\displaystyle y}$ променљиву која још увек није дефинисана. Ламбда абрстракција ${\displaystyle \lambda x.x+y}$ је синтатички исправна, и представља функцију која додаје своје уносе за још увек непознату ${\displaystyle y}$.

Заграде се могу користити тј. могу бити потребне неким изразима. На пример, ${\displaystyle \lambda x.((\lambda x.x)x)}$ and ${\displaystyle (\lambda x.(\lambda x.x))x}$ означава резиличите изразе (иако се случајно сређивањем добија исти резултат). Ево првог примера дефинисања функције која дефинише функцију и враћа резултат узимајући х из дечије-функције (примени функцију а затим врати), док други пример дефинише функцију која враћа функцију за било који улаз враћа његову вредност узете х (враћа функцију а онда је примени).

Функције које оперишу (врше неку радњу) на друге функције

У ламбда рачуну, функције су узете да буду вредности прве класе, па тако функције могу бити коришћене као улази, или бити враћене као излази из других функција.

На пример, ${\displaystyle \lambda x.x}$ представља идентичну функцију, ${\displaystyle x\rightarrow x}$, а  ${\displaystyle (\lambda x.x)y}$ представља идентичну функцију примењену на  ${\displaystyle y}$. Дакле, ${\displaystyle (\lambda x.y)}$ представља константну функцију ${\displaystyle x\rightarrow y}$, функцију која увек враћа ${\displaystyle y}$, без обзира на улаз. У ламбда рачуну, апликација функције се сматра лево-асоцијативном, што значи да ${\displaystyle stx}$ значи ${\displaystyle (st)x}$.

Потоји неколико појмова "еквиваленције" и "редукције" која дозвољава ламбда изразима да буду "поједностављени" својим "еквивалентним" ламбда изразима.

Алфа еквиваленција

Основна форма еквиваленције, дефинисана на основу ламбда услова . Она нам казује да партикулатан избор ограничене променљиве није битан. Инстанце, ${\displaystyle \lambda x.x}$ и ${\displaystyle \lambda y.y}$ су алфа-еквивалентни изрази, и представљају исте функције (идентичне функције). Изрази ${\displaystyle x}$ и ${\displaystyle y}$ нису алфа-еквивалентни, зато што нису ограничене ламбда апстракцијом. У доста случајева, обично се прво индетификују алфа-еквивалентни изрази.

Ове дефиниције су неопходне у одредђивању бета редукције.

Слободне променљиве

Слободне променљиве су оне променљиве које нису ограничене лабда апстракцијом. Низ израза, који је сачињен од слободних променљивих, је дефинисан индуктивно:

• Слободне променљиве ${\displaystyle x}$ су само ${\displaystyle x}$
• Скуп слободних променљивих ${\displaystyle \lambda x.t}$ је скуп од слободних променљивих  ${\displaystyle t}$, али са брисањем ${\displaystyle x}$
• Скуп слободних променљивих ${\displaystyle ts}$ је унија свих скупова слободних променљивих ${\displaystyle t}$ и скупова слободних променљивих ${\displaystyle s}$.

На пример, ламбда израз представљен идентитетом ${\displaystyle \lambda x.x}$ нема слободне променљиве , али функција ${\displaystyle \lambda x.x+y}$ има једну слободну променљиву, ${\displaystyle y}$.

Избегавање-утврђених измена

Претпоставимо да су ${\displaystyle t}$, ${\displaystyle s}$ и ${\displaystyle r}$ ламбда изрази а ${\displaystyle x}$ и ${\displaystyle y}$ да су променљиве. Ознака ${\displaystyle t[x:=r]}$ означава замену ${\displaystyle r}$ за ${\displaystyle x}$ у ${\displaystyle t}$ у маниру ухватити-избегнуто. Ово је дефинисано као:

• ${\displaystyle x[x:=r]=r}$;
• ${\displaystyle y[x:=r]=y}$ if ${\displaystyle x\neq y}$;
• ${\displaystyle (ts)[x:=r]=(t[x:=r])(s[x:=r])}$;
• ${\displaystyle (\lambda x.t)[x:=r]=\lambda x.t}$;
• ${\displaystyle (\lambda y.t)[x:=r]=\lambda y.(t[x:=r])}$ ако је ${\displaystyle x\neq y}$, ${\displaystyle y}$ није у слободној променљивој ${\displaystyle r}$. За променљиву ${\displaystyle y}$ се каже да је свежа за r.

На пример, ${\displaystyle (\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x}$, и ${\displaystyle ((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y}$.

Услов свежине (захтева да ${\displaystyle y}$ није у слободној променљивој ${\displaystyle r}$) је круцијалан у смислу да осигурава да замена не мења значење функција. На пример, замена је направљена тако да игнорише услов свежине: ${\displaystyle (\lambda x.y)[y:=x]=\lambda x.(y[y:=x])=\lambda x.x}$. Ова замена претвара константну функцију ${\displaystyle \lambda x.y}$ у идентитет ${\displaystyle \lambda x.x}$ уз помоћ измене.

Генерално, неуспех у успостављању услова свежине се може исправити уз помоћ алфа-преименовања са одговорајућом свежом променљивом. На пример, враћајући се назад на нашу тачну нотацију замене, у ${\displaystyle (\lambda x.y)[y:=x]}$ ламбда апстракција се може преименовати уз помоћ нове променљиве ${\displaystyle z}$, да се добије ${\displaystyle (\lambda z.y)[y:=x]=\lambda z.(y[y:=x])=\lambda z.x}$, и значење функције је заштићено заменом.

Бета редукција

Правило бета редукције каже да се ${\displaystyle (\lambda x.t)s}$ редукује на израз ${\displaystyle t[x:=s]}$. Ознака ${\displaystyle (\lambda x.t)s\to t[x:=s]}$ се користи да означи да се ${\displaystyle (\lambda x.t)s}$ бета редукује до ${\displaystyle t[x:=s]}$. На пример, за свако ${\displaystyle s}$, ${\displaystyle (\lambda x.x)s\to x[x:=s]=s}$. Ово значи да је ${\displaystyle \lambda x.x}$ стварно идентитет. Слично, ${\displaystyle (\lambda x.y)s\to y[x:=s]=y}$, што показује да је ${\displaystyle \lambda x.y}$ константна функција.

Ламбда рачун се може представити као идеализовани функционални програм, као што је Хаскел или Стандард ML. Према томе, бета редукција одговара математичком кораку. Овај корак може бити поновљен у одговарајућој бета конверзији све док се не истроше све апликације. У нетипском ламбда рачуну, као што је овде показано, ова редукција се можда не би извршила. На пример, посматрати израз ${\displaystyle \Omega =(\lambda x.xx)(\lambda x.xx)}$. Here ${\displaystyle (\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)}$. Израз се упрошћава у једној бета редукцији, а самим тим се процес редукције никада неће извршити.

Други аспект нетипског ламбда рачуна је та да не прави разлику између различитих дипова података. На пример, може се тражити да се напише функција која врши одређену операцију само на бројеве. Међутим, у нетипском ламбда рачуну, не постоји начин да се сачува функција од примењивања истинитосних вредонсти, стрингова или других објеката који нису бројеви.

Дефиниција

Ламбда изрази се састоје од

• променљивих v₁, v₂, ..., v_n, ...
• апстрактних симбола лабда 'λ' и тачке '.'
• заграда ( )

Скуп ламбда израза, Λ, могу бити индуктивно дефинисани:

1. Ако је x променљива, онда x ∈ Λ
2. Ако је х променљива и М ∈ Λ, онда (λx.M) ∈ Λ
3. Ако M, N ∈ Λ, онда (M N) ∈ Λ

Инстанце правила 2 су познате као абрстракција а инстанце правила 3 су познате као апликације^[10]

Ознака

Да би се задржала ознака ламбда израза, обично се примењују следеће конвенције.

• Крајње заграде се одбацују: M N уместо (M N)
• Претпостављено је ду су апликације асоцијативне: M N P се може написати као ((M N) P)^[11]
• Тело абрстракције се проширује колико год је могуће: λx.M N значи λx.(M N) а не значи (λx.M) N
• Низ апстракција је повезано: λx.λy.λz.N је скраћено као λxyz.N^[12][13]

Слободне и ограничене променљиве

За апстракциони оператор, λ, се каже да везује своје променљиве кад год се појаве у телу апстракције. Променљиве које спадају у апстракцију су ограничене . Све остале су слободне. На пример, у пратећим изразима y је ограничена променљива а x слободна: λy.x x y. Такође се примећује да је променљива ограничена "најближом апстракцијом". У следећим примерима једно појављивање x у изразима је ограничено другим ламбда: λx.y (λx.z x)

Скуп слободних променљивих ламбда израза, М, је означен као FV(М) и дефинисан је рекурзијом структуре израза, као што је дато:

1. FV(x) = {x}, где је х променљива
2. FV(λx.M) = FV(M) \ {x}
3. FV(M N) = FV(M) ∪ FV(N)^[14]

За изразе који не садрже слободне променљиве, каже се да су затворени. Затворени ламбда изрази су такође познати и као комбинације и еквивалентне су изразима у комбинаторичкој логици.

Редукција

Значење ламбда израза је дефинисано према томе како ти изрази могу бити редуковани.^[15]

Постоје три типа редукција:

• α-конверзија: мењање ограничених променљивих (алфа);
• β-редукција: узимање функција за њихове аргументе (бета);
• η-конверзија: која обухвата ознаку за екстензије (ета).

Говорили смо такође о насталим једнакостима : два израза су  β-еквивалентна, ако се могу β-конвертовати у исти израз, такође је и α/η-еквиваленција дефинисана слично.

Термин редекс, скраћеница од упростити израз, се односи на подтермине који могу бити редуковани уз помоћ једног редукционог праила. На пример, (λx.M) N је бета-редекс за изражавање замене N за x in M; ако x није слободно у  M, λx.M x је ета-редекс. Израз где се примењује редекс редукција; користећи претходни пример, упросшћава дате редом дате изразе M[x:=N]и M.

α-конверзија

Алфа-конверзија, позната и као алфа-преименовање,^[16] дозвољава промену имена ограниченим променљивим. На пример, алфа-конверзија  λx.x гласи λy.y. Изрази који се разликују само по алфа-конверзији се називају а-еквивалентно. Често, у коришћењу ламбда рачуна, а-еквивалентни изрази се сматрају еквивалентним.

Прецизна правила за алфа-конверзију нису баш једноставна. Прво, када алфа-конвертује апстракцију, једина променљива која се појављује  и која је преименована је та која је огранилена истом апстракцијом. На пример, алфа-конверзија  λx.λx.x  даје  λy.λx.x, али не даје λy.λx.y. Овај други пример даје другачије значење од оригинала.

Друго, алфа-конверзија није могућа ако ће резултат бити променљива која је под контролом друге апстракције . На пример, ако заменимо x са y у λx.λy.x, добијамо λy.λy.y, што није исто.

У програмима који имају статичко језгро, алфа-конверзија се може користити да се направи име резолуције једноставније обезбеђујући да име променљиве маскира име у одговарајућем језгру (видети алфа преименовање да се направи тривијална резолуција

У Де Бружиновој индексној ознаци, било која два алфа-еквивалентна израза су идентична.

Замена

Замена, написана као E[V := R], је процес замене свих битнијих случајева променљиве V у изразу E са изразом R. Субституција израза λ-рачуна је дефинисана на основу рекурзије структура израза, као што је дато (приметити: x и y су једине променљиве док су M и N било који λ изрази).

x[x := N]       ≡ N
y[x := N]       ≡ y, if x ≠ y
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
(λx.M)[x := N]  ≡ λx.M
(λy.M)[x := N]  ≡ λy.(M[x := N]), if x ≠ y, дефинисано y ∉ FV(N)

Да би се трансформисало у ламбда апстракцију, понекад треба α-конвертовати израз. На пример, није тачно да (λx.y)[y := x] даје (λx.x), зато што је замењена вредност x претпостављена да буде слободна али на крају и ограничена. Исправна замена у овом случају је (λz.x), све до α-еквиваленције. Приметити да је замена дефинисана уникатно до α-еквиваленције.

β-редукција

Бета-редукција памти идеју апликације функције. Бета-редукција је дефинисана у оквирима замене: бета-редукција од((λV.E) E′) је  E[V := E′].

На пример, претпоставимо шивровање  2, 7, ×, имамо следећу β-редукцију: ((λn.n×2) 7) → 7×2.

η-конверзија

Ета-конверзија изражава идеју екстензије, која се у овом контексту састоји од две фунције које су исте ако и само ако дају исти резултат за све аргументе . Ета-конверзија конвертује између λx.(f x) и f  кад год се x не појављује слободно у f.

Нормалне форме и ушће

За нетипски ламбда рачун, β-редукција као повратно правило, нити нормализује снажно нити нормализује слабо

Међутим, може се показати да је β-редукција спојена. (Наравно, радимо до α-конверзије, тј. сматрамо да су две нормалне форме једнаке, ако је могуће да се α-конвертује дуално.)

Дакле, оба снажно нормализујућа израза и слабо нормализујућа израза имају уникатну нормалну форму. За снажне нормализујуће системе, било која редукциона стратегија гарантује позивање нормалне форме, док за слабо нормализујуће изразе, неке редукционе стратегије се можда неће извршити.

Шифровање типова података

Основе ламбда рачуна се могу користити за истинитосне вредности, аритметику, структуре података и рекурзију, као што је илустровано у наредним подељцима.

Аритметика у ламбда рачуну

Постоји неколико могућих начина да се дефинишу природни бројеви у ламбда рачуну, али у скоро већини случајева су Черчови бројеви, који се могу дефинисати као:

0 := λf.λx.x

1 := λf.λx.f x

2 := λf.λx.f (f x)

3 := λf.λx.f (f (f x))

и тако даље. Или користити алтернативну синтаксу:

0 := λfx.x

1 := λfx.f x

2 := λfx.f (f x)

3 := λfx.f (f (f x))

Черчова цифра је функција вишег реда—која узима једну функцију f, а враћа другу функцију. Черчов број n је функција која узима функцију f као аргумент и враћа n-ту композицију f, тј. функција f се позива сама n пута. Ово је означено са f⁽ⁿ⁾ у односу n-ти степен f (сматрати оператором); f⁽⁰⁾ је дефинисана да буде идентична функција. Такве поновљене композиције (једне функције f) поштују законе ескпоната, због којег ови бројеви могу бити коришћени у аритметици. (У Черчовом оригиналном ламбда рачуну, формални параметар ламбда израза је био морао да се појављује барем једном у телу функције, што чини ову дефиницију 0 немогућом)

Можемо дефинисати наслеђену функцију , која узима број n и враћа n + 1 додајући другу апликацију f, где '(mf)x' значи да је функција 'f' примењена 'm' пута на 'x':

SUCC := λn.λf.λx.f (n f x)

Због m-тог члана f упоређујући га са n-тим чланом f даје m+n-ти члан f, додавања се могу дефинисати на следећи начин:

PLUS := λm.λn.λf.λx.m f (n f x)

PLUS се може сматрати као функција која узима два природна броја као аргумента а враћа природан број; може се представити на следећи начин

PLUS 2 3

и

5

су β-еквивалентни ламбда изрази. Додавање m броју n се може постићи додавањем 1 m пута, еквивалентна дефиниција је:

PLUS := λm.λn.m SUCC n ^[17]

Слично томе, множење се дефинише као

MULT := λm.λn.λf.m (n f)^[18]

Алтернативно

MULT := λm.λn.m (PLUS n) 0

умножавање m и n је исто што и понављање додате n функције m пута и помножено 0. Експонат је чешће једоставан враћајући Черчове бројеве, именоване

POW := λb.λe.e b

Претходна функција дефинисана PRED n = n − 1 за позитивни цели број n и PRED 0 = 0  је знатно више компликованија. Формула

PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)

може бити доказана, показујући да ако је T означено (λg.λh.h (g f)), онда је T⁽ⁿ⁾(λu.x) = (λh.h(f⁽ⁿ⁻¹⁾(x)))за n > 0. Две постале дефиниције PRED су дате испод, једна користи услове а друга користећи парове. Са претходном функцијом, одузимање је једноставно. Дефинисање

SUB := λm.λn.n PRED m,

SUB m n позива m − n када је m > n и 0 другачије.

Логика и искази

Конвенцијом, следеће две дефиниције (позната и као Черчова истинитосна вредност) које се користе за одређивање истинитосне вредности TRUE(тачно) и FALSE(нетачно):

TRUE := λx.λy.x

FALSE := λx.λy.y

(Приметити да  FALSE еквивалентно Черчовом броју нула)

Затим, са ова два λ-израза, можемо дефинисати неке логичке операције (ово су само могуће формулације; остали изрази су еквивалентно тачнии):

AND := λp.λq.p q p

OR := λp.λq.p p q

NOT := λp.λa.λb.p b a

IFTHENELSE := λp.λa.λb.p a b

Сада можемо да изралунамо логичке функције, нпр. :

AND TRUE FALSE

≡ (λp.λq.p q p) TRUE FALSE →_β TRUE FALSE TRUE

≡ (λx.λy.x) FALSE TRUE →_β FALSE

видимо да је AND(и) TRUE(тачно) FALSE(нетачно) еквивалетно  FALSE(нетачном).

Предикат је функција која враћа истинитосну вредност. Најбитнији предикат је ISZERO(је нула), који враћа TRUE(тачно)ако је аргумент Черчов број 0, а FALSE(нетачно)ако је аргумент било који други Черчов број:

ISZERO := λn.n (λx.FALSE) TRUE

Следећи предикат тестира да ли је први аргумент мањи или једнак другом:

LEQ := λm.λn.ISZERO (SUB m n),

и док је m = n, ако LEQ m n и LEQ n m, онда је лако изградити предикат нумеричке једнакости.

Доступност предиката и дефиниције TRUE и FALSE чине га жељеним да се напишу "ако-онда-или" изрази у ламбда рачуну. На пример, претходник функције се може дефинисати као:

PRED := λn.n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) 0

што се може доказати покзујући индуктивно да је n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) додата n − 1 функција за n > 0.

Парови

Пар (2-заграде) се може дефинисати уз помоћ TRUE and FALSE, користећи Черчово дешифровање за парове. На пример, PAIR енкапсулира пар (x,y), FIRST враа први елемент тог пара, док SECOND враћа други.

PAIR := λx.λy.λf.f x y

FIRST := λp.p TRUE

SECOND := λp.p FALSE

NIL := λx.TRUE

NULL := λp.p (λx.λy.FALSE)

Линковане листе се могу дефинисати и као NIL за празну листу, или PAIR(пар) елемента и мале листе. Птерпоставимо да NULL тестира за вредност  NIL(нула). (Алтернативно, са NIL := FALSE, конструкција l (λh.λt.λz.deal_with_head_h_and_tail_t) (deal_with_nil) уклања потребу за експлицитним NULL тестом.

Као пример коришћења парова, функције промена и раста које мапирају (m, n) до (n, n + 1) се може дефинисати као

Φ := λx.PAIR (SECOND x) (SUCC (SECOND x))

Који нам омогућава да добијемо можда и најтранспарентнију верзију претходне функције

PRED := λn.FIRST (n Φ (PAIR 0 0)).

Рекурзија и фиксне тачке

Рекурзија је дефиница функције која позива себе; ламбда рачун не дозвољава ово (не можемо одредити вредности која тек треба да се дефинише, унутар ламбда израза дефинише се иста вредност, као све анонимне функције у ламбда рачуну). Међутим, овај утисак вара: у (λx.x x) y  обе x‍ ‍ вредности се односе на исти ламбда израз , y, па је самим тим могућа за ламбда израз –овде је y – направљен тако да позива сопствену вредност, кроз своју апликацију.

Рекурзивна инстанца функције факторијела F(n) је дефинисана као

F(n) = 1, if n = 0; else n × F(n − 1).

У ламбда изразу који је изабран да представља ту функцију, за параметар (углавном први) се претпоставља да прима свој ламбда израз, а то се назива-примати то као аргумент- што ће бити рекурзија. Овако се достиже рекурзија, намерно као свој референтни аргумент,  (који се овде назива r) и мора увек себе да позива у телу функције, тј. :

G := λr. λn.(1, if n = 0; else n × (r r (n−1)))

with  r r x = F x = G r x  to hold, so  r = G  and

F := G G = (λx.x x) G

Сопствена-апликација постиже репликацију овде, пролазећи функцију ламбда израза на следећи позив као вредносни аргумент, чинећи то могућим за реферисање и позив.

Ово решава то али подразумева поновно писање сваког рекурзивног позив као сопствена-апликација. Волели бисмо да имамо генеричко решење, без потребе поновног писања:

G := λr. λn.(1, if n = 0; else n × (r (n−1)))

with  r x = F x = G r x  to hold, so  r = G r =: FIX G  and

F := FIX G  where  FIX g := (r where r = g r) = g (FIX g)

so that  FIX G = G (FIX G) = (λn.(1, if n = 0; else n × ((FIX G) (n−1))))

Дати ламбда израз са првим аргументом представља рекурзивни позив ( означено са G),  комбинатор фиксне тачке FIX ће вратити сопствену репликацију ламбда израза представљајући рекурзивну функцију (овде је то F). Функција не мора проћи саму себе по сваку цену, за сопствену репликацију која је направљена у наставку, када се креира, да буде извршена сваки пут када се позове. Оригиналан ламбда израз (FIX G)је поново направљен у самом себи, постижући сопствену референцу

Постоји много различитих дефиниција за FIX оператор, најједноставнији је:

Y := λg.(λx.g (x x)) (λx.g (x x))

У ламбда рачуну , Y g  је фиксирана тачка g, као што је показано:

Y g

λh.((λx.h (x x)) (λx.h (x x))) g

(λx.g (x x)) (λx.g (x x))

g ((λx.g (x x)) (λx.g (x x)))

g (Y g)

Сада, да бисмо извели наш рекурзивни позив функције факторијела, једноставно ћемо позвати (Y G) n, где је n број чији факторијел израчунавамо. Доделимо нпр. вредност  n = 4, што даје:

(Y G) 4

G (Y G) 4

(λr.λn.(1, if n = 0; else n × (r (n−1)))) (Y G) 4

(λn.(1, if n = 0; else n × ((Y G) (n−1)))) 4

1, if 4 = 0; else 4 × ((Y G) (4−1))

4 × (G (Y G) (4−1))

4 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (4−1))

4 × (1, if 3 = 0; else 3 × ((Y G) (3−1)))

4 × (3 × (G (Y G) (3−1)))

4 × (3 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (3−1)))

4 × (3 × (1, if 2 = 0; else 2 × ((Y G) (2−1))))

4 × (3 × (2 × (G (Y G) (2−1))))

4 × (3 × (2 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (2−1))))

4 × (3 × (2 × (1, if 1 = 0; else 1 × ((Y G) (1−1)))))

4 × (3 × (2 × (1 × (G (Y G) (1−1)))))

4 × (3 × (2 × (1 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (1−1)))))

4 × (3 × (2 × (1 × (1, if 0 = 0; else 0 × ((Y G) (0−1))))))

4 × (3 × (2 × (1 × (1))))

24

Свака рекурзивно дефинисана функција може бити представљена као фиксирана тачка неке одговарајуће дефинисане функције затварајући рекурзивни позив са екстра аргументом Y, свака рекурзивно дефинисана функција се може изразити као ламбда израз. Практично, ми можемо јасно дефинисати одузимање, множење и поређење предиката природних бројева рекурзивно.

Стандардни изрази

Следећи изрази обично прихватају имена:

I := λx.x

K := λx.λy.x

S := λx.λy.λz.x z (y z)

B := λx.λy.λz.x (y z)

C := λx.λy.λz.x z y

W := λx.λy.x y y

U := λx.λy.y (x x y)

ω := λx.x x

Ω := ω ω

Y := λg.(λx.g (x x)) (λx.g (x x))

Типски ламбда рачун

Типски ламбда рачун је типски формализам који користи ламбда симбол (${\displaystyle \lambda }$) да означи непознату апстракцију функције. У овом контексту, типови су обично објекти синтетичке природе који су додељени ламбда изразима; егзактна природа типова зависи од израчунавања рачуна (видети врсте у наставку) . Са одређене тачке гледишта, типски ламбда рачун се може представити као усавршавање нетипског ламбда рачуна али са друге тачке гледишта, они они се такође могу сматрати више фундаменталном теоријом и нетипски ламбда рачун је специјални случај са само једним типом.

Типски ламбда рачун је оснивач програмских језика и он представља базу функционалних програмских језика као што су ML и Хаскел и, више индиректни, типски императивни програмски језици. Типски ламбда рачун има веома важну улогу у дизајну типских система за програмске језике; овде одређивање типа обично означава пожељне карактеристике програма, нпр. програм неће наштетити приступ меморији

Типски ламбда рачун је уско повезан са математичком логиком и отпорном теоријом са Кари-Хаурадовим изоморфизмом и они се могу сматрати као интерни програми сачињени од класа категорија, нпр. једноставан типски ламбда рачун је програм Декартове затворене категорије (Дзк).

Израчуниве функције и ламбда рачун

Функција F: N → N природних бројева је израчунива ако и сако ако постоји ламбда израз  f такав да за сваки пар x, y у N, F(x)=y и ако и само ако је f x =_β y, где су x и y Черчови одговарајући бројеви за x и y, односно и =_β представља еквиваленцију за бета редукцију. Ово је један од много начина да се дефинише израчуњивост; видети Черч-Тјурингова теза за дискусију о другим прорачунима и њиховим једнакостима.

Несигурност еквиваленције

Не постоји алгоритам који узима као улазне податке два ламбда израза и враћа TRUE or FALSE у зависности од тога да ли су та два израза еквивалентна или нису. Историјски гледано, ово је први проблем чија се несигурност могла доказати. Као и код доказане несигурности , доказ показује да ни једна рачунива функција не може да одређује еквиваленцију. Черч-Тјурингова теза је уведена да покаже да не постоји алгоритам који ово ради.

Черчов доказ је први упростио проблем одређивања где ламбда израз има нормалну форму. Нормална форма је еквивалентна иразу који се не може упростити испод правила који су условљени правилом. Он сумња да је овај исказ рачунив, и да се мође представити преко ламбда рачуна. Надограђујући се на посао који је одрадио Клин, конструктујући Геделово бројање за ламбда изразем, он је осмислио ламбда израз e који стриктно прати доказ Геделове теореме о непотпуности . Ако се e примењује на сопствени Геделов број, резултат је контрадикција. 

Ламбда рачун и програмски језици

Као што је одређено од стране Питера Ландина 1965. кореспонденција између Алгола 60 и Черчове Ламбда нотације, секвенцијално процедурални програми могу да разумеју изразе ламбда рачуна, који пружају основне механизме за процедуралну апстракцију и процедуру (потпрограм) апликације.

Ламбда рачун чини "функције" повезанијим и чини их објектима прве класе што утиче на пораст комплексности имплементације када буде извршена. 

Анонимна функција

На пример, у Lisp-у квадратна функције се може представити као ламбда рачун, као:

(lambda (x) (* x x))

Дати пример је израз који припада првој класи функција. Симбол lambda креира анонимну функцију, дате листе имена параметра, (x) — само један аргумент у овом случају, и израз који је представљен као тело функције , (* x x). Хаскелов пример је идентичан. Анонимне функције се понекад зову ламбда изразима

На пример, Паскал и много осталих императивних програма је дуго подржавало прелазак преко потпрограма, као аргументе за друге потпрограме кроз механизам извршилаца функције. Међутим, извршиоци програма нису довољан услов за функције да буду типови прве класе, зато што је функција тип података прве класе ако и само ако нова инстанца функције може бити креирана у брзом времену. У овом брзом времену креирање функција је подржано у Smalltalkу, Јаваскрипти, и чешће у Скали, Ајфелу ("агенти", C# ("делегација" и C++11, и многи други.

Стратегија упрошћавања

Без обзира на то да ли се израз нормализује или не, и колико му треба да се изрши у нормализацији тога, израз зависи у великој мери од коришћене стратегије упрошћавања. Разлика између редукционих стратегија зависи од разлике у функционалном програмском језику између пожељне процене и непожељне процене.

Потпуна бета редукција

Било каква редукција се може редуковати било кад. Ово значи да у суштини одсуство било које практичне редукционе стратегије-која је уско повезана са редукцијом , "пада у воду".

Апликативни ред

Сркоз лево, по дубини се прво извршава редукција. Интуитивно ово значи да се увек прво упрошћавају аргументи функције пре саме функције. Апликативни ред увек покушава да прихвати функцију у нормалном облику, чак и када то није могуће. Многи програмски језици (као што су Lisp, ML, и императивни језици као што су C и Јава)су описани као "стриктни", мислећи да су функције примљене од стране не нормализујућих аргумената, не нормализујуће. Ово је урађено користећи апликативни ред, а назива се вредносно упрошћавање, или чешће "жељена еволуција".

Нормални ред

Скроз лево, се прво редукује по крајевима. Кад год је могуће, аргументи се замењују у тело абрстракције пре него што су аргументи упрошћени.

Позив по имену

Као нормални ред, али без редукционих перформанси унутар апстракција. На пример, λx.(λx.x)x је нормална форма према овој стратегији, иако садржи редекс  (λx.x)x.

Позив по вредности

Само крајеви редекса се упрошћавај; редекс је упрошћен само ако је десна страна подложна редукцији (променљива или ламбда апстракција).

Позив по потреби

Као нормални ред, али апликације функција ће удвостручити изразе уместо имена аргумената, који су затим редукују само " када је то потребно". Названо у практичном смислу "лења процена". У имплементацијама ово "име" узима форму извршиоца, са редексом представљеним уз помоћ узвика.

Апликативни израз није нормализовано осмишљен. Чести противпример је: дефинисати Ω = ωω где је ω = λx.xx. Цео овај израз садржи само један редекс, који именује цели израз; редукује се поново Ω. Како је ово једина могућа редукција, Ω нема нормалну форму (испод сваке процене стратегије). Користећи апликативни ред, израз KIΩ = (λx.λy.x) (λx.x)Ω је редукован од стране прве редукције Ω до нормалне форме (док је редекс скроз десно ), али док Ω нема нормалну форму, апликативни ред не може да нађе нормалну форму за KIΩ.

У супротности, нормални ред се тако назива зато што увек нађе нормализујућу редукцију. У наведеном примеру, KIΩ се редкује из нормалног реда до I, нормалне форме. Недостатак се огледа у томе што редекси у аргументима могу бити коопирани, што доводи до дуплираног израчунавања (нпр. , (λx.xx) ((λx.x)y) се редукује дп ((λx.x)y) ((λx.x)y) користећи ову стратегију; сада постоје два редекса, па целокупна процена мора да има још два корака, али ако су аргументи прво редуковани, тада ће неће постојати ништа).

Позитивни договор коришћења апликативног израза се огледа у томе што не изазива непотребно рачунањ, ако су сви аргументи коришћени, због тоха што се никада не замењују аргументи који садрже редекс и због тога их не треба никада копирати (што може да дуплира посао). У горњем примеру, у апликационом изразу (λx.xx) ((λx.x)y) се редукује прво до(λx.xx)y а затим до нормалног израза yy, узимајући два корака уместо да узме три израза.

Већина чистих функционалних програмских језика (посебно Миранда и његови претходници, укључујући Хаскел), и доказаних програмских језика теореме провере, користе лењу процену пто је у суштини исто ка и позив по потреби. Ове је слично нормалној редукцији, али позив по потреби успева да избегне дуплиање посла инхерентно у нормалној редукцији користећи дељење . У горе наведеном примеру, (λx.xx) ((λx.x)y) се редукује до ((λx.x)y) ((λx.x)y), што садржи два редекса, али у позиву по потреби они су представљени тако да користе исти објекат чешће него копирани, па када је један редукован, самим тим је и други редукован.

Напомена о сложености

Док је идеја бета редукције изгледала довољно једноставно, она ипак није атомски корак, у смислу да мора да има компликовану структуру при процени рачунарске сложености.^[19] Прецизно, једна мора некако да пронађе локацију свих ограничених појава променљиве V  у изразу E, што доводи до трошења времена, или једна мора да води евиденцију локација V у изразу E, што такође доводи до трошења времена. Наивна претрага локације V у изразу E је О(n) у дужини n од E. Ово доводи до проучавања система који користе експлицитну замену. Синотов управљач стринговима ^{[тражи се извор]} нуди начин снимања локација слободних варијабли у изразима.

Паралелизам и слагање

Черч-Росерова особина у ламбда рачуну значи да процена (β-редукција) може бити избачена у било ком редоследу, чак и у паралели. Ово значи да је променљива недетерминистичка процена стратегија битна. Међутим, ламбда рачун не нуди било какву експлицитну конструкцију за паралелну обраду. Један може додати конструкцију као карактеристику за ламбда рачун. Други процес рачунања је разби

Семантика

Чињеница, да се изрази ламбда рачуна понашају као функције на остале ламбда изразе, па чак и на саме себе, довела је до питања о семантици ламбда рачуна . Да ли се могу разумна значења доделти изразима ламбда рачуна? Природа семантике је је да нађе скупове D изоморфне функционалном простору D → D, функције на саму себе. Међутим, компликовано постојање D, уз помоћ кардиналног ограничења зато што скуп свих функција из  D до D има већу кардиналност него D, осим ако је D самостално.

У 1970-им, Дејна Скот је показако да, ако се посматрају само непрекидне функције, скуп или домен D са потребним особинама се може наћи, правећи тако модел ламбда рачуна.

Ово је створило основу за семантику система закона програмских језика.

Референце

1. Turing, A. M. (December 1937).
2. Mitchell 2003, стр. 57.
3. Coquand, Thierry, "Type Theory"^{[мртва веза]}, The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.
4. Moortgat 1988
5. Bunt & Muskens 2008
6. A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
7. For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
8. A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2.
9. Church, A. "A Formulation of the Simple Theory of Types".
10. Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics Архивирано на сајту (23. август 2004), Studies in Logic and the Foundations of Mathematics 103 (Revised ed.
11. "Example for Rules of Associativity".
12. Selinger, Peter (2008), Lecture Notes on the Lambda Calculus (PDF) 0804 (class: cs.
13. "Example for Rule of Associativity".
14. Barendregt, Henk; Barendsen, Erik (March 2000), Introduction to Lambda Calculus^{[мртва веза]} (PDF)
15. De Queiroz, Ruy J. G. B. (1988). „A Proof-Theoretic Account of Programming and the Role of Reduction Rules”. Dialectica. 42 (4): 265—282. doi:10.1111/j.1746-8361.1988.tb00919.x.
16. Turbak & Gifford 2008, стр. 251
17. Felleisen, Matthias; Flatt, Matthew (2006), Programming Languages and Lambda Calculi (PDF). стр. 26.
18. Selinger, Peter (2008), Lecture Notes on the Lambda Calculus (PDF) 0804 (class: cs.
19. R. Statman, "The typed λ-calculus is not elementary recursive."

Литература

• Turbak, Franklyn; Gifford, David (2008). Design concepts in programming languages. MIT press. стр. 251. ISBN 978-0-262-20175-9.
• Bunt, Harry; Muskens, Reinhard (2008). Computing Meaning. Springer Science & Business Media. ISBN 978-1-4020-5957-5.
• Moortgat, Michael (1988). Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus. Walter de Gruyter. ISBN 978-90-6765-387-9.
• Mitchell, John C. (2003). Concepts in Programming Languages. Cambridge University Press. стр. 57. ISBN 978-0-521-78098-8.