Ламбда рачун (ознака λ-рачун) је формални систем у математичкој логици за представљање рачунања базираног на апстракцији функција и апликација користећи везивање и супституцију променљиве. Увео га је Алонзо Черч да формулише концепт ефективног рачунања, ламбда рачун је наишо на прве успехе на пољу теорије рачунања, као што је негативан одговор на Хилбертов проблем одлуке. Ламбда рачун је концептуално једноставан универзални модел рачунања (Тјуринг је показао 1937. године да Тјурингова машина једнака ламбда рачуну у експресивности). Име потиче од грчког слова ламбда (λ) коришћеног да означи везивање променљивих у функцији. Слово је само по себи произвољно и нема никакво специјално значење. Ламбда рачун се учи и користи у рачунарству због своје корисности у приказивању функционалног размишљања и итеративне редукције.
Због важности појма везивања променљиве и субституције, не постоји само један систем ламбда рачуна, и у пракси постоје "типске" и "нетипске" варијанте. Историјски гледано, најважнији систем је био нетипски ламбда рачун, у којем функција апликације нема рестрикција (појам домена функције није уграђен у систем. У Черч-Тјуринговој тези, нетипски ламбда рачун је подешен да буде могуће израчунати све ефективно израчуниве функције. Типски ламбда рачун је варијација која има рестрикције за функцију апликације, тако да се функција може применити само ако се прихвати улазни тип података.
Данас, ламбда рачун има улогу у много различитих свера, као нпр. у математици, филозофији,Coquand, Thierry, "Type Theory", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed. лингвистици, и рачунарству. Још увек се користи у области теорије рачунања, као и Тјурингова машина која је врло важан модел за рачунање. Ламбда рачун је одиграо веома важну улоу у развоју теорије програмских језика. Делови бројача, у ламбда рачуну у рачунарству, су функционални програми, који имплементирају ламбда рачун (повећати неке константе и типове података). Поред програмских језика, лабмда рачун игра улогу у теорији доказа. Главни пример тога је Кари-Хауардова кореспонденција, која даје кореспонденцију између различитих система типова ламбда рачуна и система формалне логике.
Историја ламбда рачуна у математици Ламбда рачун је увео Алонзо Черч у 1930—им годинама као део истраге о основама математике.A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006). Оригинални систем је показан као логички противречан 1935. године када су Стивен Клин и Ј. Б. Росер развили Клин-Росеров парадокс.
Након тога, у 1936. години, Черч је изоловао и објавио само део битан за рачунање, који се данас зове нетипски ламбда рачун.A. Church, . У 1940. години, он је такође увео рачунски слабији, али логички доследнији систем, знан као једноставни типски ламбда рачун.Church, A. "A Formulation of the Simple Theory of Types".
Мотивација Рачунске функције представљају круцијалан концепт у рачунарству и математици. Ламбда рачун даје једноставу семантику за израчунавање, омогућавајући особине израчунавања да буду формално учене. Ламбда рачун укључује два упрошћавања која чине семантику једноставном. Прво поједностављење је то да Ламбда рачун третира функцију "анонимно", без давања експлицитних имена. На пример, функција
може се поново написати у анонимној форми као
(чита се као "пар x и y је мапиран у "). Слично,
се може написати у анонимној форми , где је улаз једноставно мапиран у самог себе
Друго поједностављење је то да ламбда рачун користи само функције једног улаза. Обична функција која захтева два улаза , за инстанцу (збир квадрата) функције, може се написати као једна еквивалентна функција која прима један улаз, а да излаз враћа другу функцију, која заузврат прима један улаз. На пример,
се може написати као
Ова метода, позната и као кариинг, трансформише функцију која узима више аргумената у ланац функција, где свака има један аргумент.
Функционално окружење функције са аргументима (5, 2), добијено одједном
, док процена каријеве верзије захтева још један корак
добија се исти резултат.
Ламбда рачун Ламбда рачун се састоји од програма ламбда услова, који су дефинисани одређеном формалном синтаксом, и сетом трансформацијских правила, који допуштају манипулацију ламбда услова. Ова трансформацијска правила се могу представити као еквивалентна теорија или као операционализам.
Као што је већ описано, све функције у ламбда рачуну су у ствари анонимне функције, тј. немају име. Дозвољавају само једну улазну променљиву, са каријевом верзијом да се убаце функције са неколико променљивих.
Ламбда правила Синтакса ламбда рачуна дефинише неке изразе као дозвољене изразе ламбда рачуна и неке неважеће, као што су на пример стрингови који се састоје од карактера валидних C програма а неки ипак нису. Дозвољени израз ламбда рачуна се назива ламбда израз.
Следећа три правила дају индуктивну дефиницију која се могу искористити за прављење синтатички исправних ламбда изрази: променљива, , је сам по себи валидан ламбда израз ако је ламбда израз, а је променљива, онда је ламбда израз (назива се и ламбда апстракцијом); ако су и ламбда изрази, онда је и ламбда израз (апликација). Ништа друго није ламбда услов. Ламбда услов је валидан ако и само ако се може добити применом ова три правила. Међутим, неке заграде могу бити изостављене у складу са неким правилима. На пример, спољашње заграде се обично не пишу.
Ламбда апстракција је дефиниција анонимне функције која може да узме један улаз и замени га у израз . На тај начин се дефинишу анонимне функције које узимају x а враћају t. На пример, је ламбда апстракција функције користећи израз за . Дефиниција функције са ламбда абрстракцијом само "поставља" функцију али је не уводи. Абрстракција везује променљиву у израз .
Апликација представља примену функције на улаз , који представља чин позива функције у односу на улаз да би се добио .
Не постоји концепт променљивих декларација у ламбда рачуну. У дефиницији као што је (i.e. ), ламбда рачун третира променљиву која још увек није дефинисана. Ламбда абрстракција је синтатички исправна, и представља функцију која додаје своје уносе за још увек непознату .
Заграде се могу користити тј. могу бити потребне неким изразима. На пример, and означава резиличите изразе (иако се случајно сређивањем добија исти резултат). Ево првог примера дефинисања функције која дефинише функцију и враћа резултат узимајући х из дечије-функције (примени функцију а затим врати), док други пример дефинише функцију која враћа функцију за било који улаз враћа његову вредност узете х (враћа функцију а онда је примени).
Функције које оперишу (врше неку радњу) на друге функције У ламбда рачуну, функције су узете да буду вредности прве класе, па тако функције могу бити коришћене као улази, или бити враћене као излази из других функција.
На пример, представља идентичну функцију, , а представља идентичну функцију примењену на . Дакле, представља константну функцију , функцију која увек враћа , без обзира на улаз. У ламбда рачуну, апликација функције се сматра лево-асоцијативном, што значи да значи .
Потоји неколико појмова "еквиваленције" и "редукције" која дозвољава ламбда изразима да буду "поједностављени" својим "еквивалентним" ламбда изразима.
Алфа еквиваленција Основна форма еквиваленције, дефинисана на основу ламбда услова . Она нам казује да партикулатан избор ограничене променљиве није битан. Инстанце, и су алфа-еквивалентни изрази, и представљају исте функције (идентичне функције). Изрази и нису алфа-еквивалентни, зато што нису ограничене ламбда апстракцијом. У доста случајева, обично се прво индетификују алфа-еквивалентни изрази.
Ове дефиниције су неопходне у одредђивању бета редукције.
Слободне променљиве Слободне променљиве су оне променљиве које нису ограничене лабда апстракцијом. Низ израза, који је сачињен од слободних променљивих, је дефинисан индуктивно: Слободне променљиве су само Скуп слободних променљивих је скуп од слободних променљивих , али са брисањем Скуп слободних променљивих је унија свих скупова слободних променљивих и скупова слободних променљивих . На пример, ламбда израз представљен идентитетом нема слободне променљиве , али функција има једну слободну променљиву, .
Избегавање-утврђених измена Претпоставимо да су , и ламбда изрази а и да су променљиве. Ознака означава замену за у у маниру ухватити-избегнуто. Ово је дефинисано као: ; if ;
ако је , није у слободној променљивој . За променљиву се каже да је свежа за r. На пример, , и .
Услов свежине (захтева да није у слободној променљивој ) је круцијалан у смислу да осигурава да замена не мења значење функција. На пример, замена је направљена тако да игнорише услов свежине: . Ова замена претвара константну функцију у идентитет уз помоћ измене.
Генерално, неуспех у успостављању услова свежине се може исправити уз помоћ алфа-преименовања са одговорајућом свежом променљивом. На пример, враћајући се назад на нашу тачну нотацију замене, у ламбда апстракција се може преименовати уз помоћ нове променљиве , да се добије , и значење функције је заштићено заменом.
Бета редукција Правило бета редукције каже да се редукује на израз . Ознака се користи да означи да се бета редукује до . На пример, за свако , . Ово значи да је стварно идентитет. Слично, , што показује да је константна функција.
Ламбда рачун се може представити као идеализовани функционални програм, као што је Хаскел или Стандард ML. Према томе, бета редукција одговара математичком кораку. Овај корак може бити поновљен у одговарајућој бета конверзији све док се не истроше све апликације. У нетипском ламбда рачуну, као што је овде показано, ова редукција се можда не би извршила. На пример, посматрати израз . Here . Израз се упрошћава у једној бета редукцији, а самим тим се процес редукције никада неће извршити.
Други аспект нетипског ламбда рачуна је та да не прави разлику између различитих дипова података. На пример, може се тражити да се напише функција која врши одређену операцију само на бројеве. Међутим, у нетипском ламбда рачуну, не постоји начин да се сачува функција од примењивања истинитосних вредонсти, стрингова или других објеката који нису бројеви.
Дефиниција Ламбда изрази се састоје од променљивих v1, v2, ..., vn, ... апстрактних симбола лабда 'λ' и тачке '.' заграда ( ) Скуп ламбда израза, Λ, могу бити индуктивно дефинисани: Ако је x променљива, онда x ∈ Λ Ако је х променљива и М ∈ Λ, онда (λx.M) ∈ Λ Ако M, N ∈ Λ, онда (M N) ∈ Λ Инстанце правила 2 су познате као абрстракција а инстанце правила 3 су познате као апликацијеBarendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics , Studies in Logic and the Foundations of Mathematics 103 (Revised ed.
Ознака Да би се задржала ознака ламбда израза, обично се примењују следеће конвенције. Крајње заграде се одбацују: M N уместо (M N) Претпостављено је ду су апликације асоцијативне: M N P се може написати као ((M N) P)"Example for Rules of Associativity". Тело абрстракције се проширује колико год је могуће: λx.M N значи λx.(M N) а не значи (λx.M) N Низ апстракција је повезано: λx.λy.λz.N је скраћено као λxyz.NSelinger, Peter (2008), Lecture Notes on the Lambda Calculus (PDF) 0804 (class: cs."Example for Rule of Associativity".
Слободне и ограничене променљиве За апстракциони оператор, λ, се каже да везује своје променљиве кад год се појаве у телу апстракције. Променљиве које спадају у апстракцију су ограничене . Све остале су слободне. На пример, у пратећим изразима y је ограничена променљива а x слободна: λy.x x y. Такође се примећује да је променљива ограничена "најближом апстракцијом". У следећим примерима једно појављивање x у изразима је ограничено другим ламбда: λx.y (λx.z x)