Ламбда изчислението е формална система в математическата логика за изразяване на базирани на абстракция изчисления и прилагане на функции с помощта на свързване и заместване на променливи. Това е универсален модел, който може да се приложи към дизайна на всяка машина на Тюринг. Ламбда изчислението е въведено за първи път от Чърч, известен математик, през 30-те години на миналия век.
Системата се състои от изграждане на ламбда членове и извършване на операции за намаляване на тях.
Обяснения и приложения
Гръцката буква ламбда (λ) се използва в ламбда изрази и ламбда термини за обозначаване на свързването на променлива във функция.
Ламбда изчислението може да не бъде въведено или въведено. В първия вариант функциите могат да се използват само ако са в състояние да получават данни от този тип. Въведените ламбда изчисления са по-слаби, могат да изразяват по-малка стойност. Но, от друга страна, те ви позволяват да докажете повече неща.
Една от причините за толкова много различни видове е желанието на учените да направят повече, без да се отказват от възможността да докажат силни теореми за ламбда изчисление.
Системата има приложения в много различни области на математиката, философията, лингвистиката и компютърните науки. На първо място, ламбда изчислението е изчисление, което е изиграло важна роля в развитието на теорията на езиците за програмиране. Системите прилагат стиловете на функционално създаване. Те също са гореща тема за изследвания в теорията на тези категории.
За манекени
Изчислението на ламбда е въведено от математика Алонзо Чърч през 30-те години на миналия век като част от неговото изследване на основите на науката. Показано е, че първоначалната система е логически непоследователна през 1935 г., когато Стивън Клин и Дж. Б. Росър разработиха парадокса на Клийн-Росер.
По-късно, през 1936 г., Чърч отделя и публикува само частта, която е от значение за изчисленията, което сега се нарича нетипизирано ламбда изчисление. През 1940 г. той също така въвежда по-слаба, но логически последователна теория, известна като система от първичен тип. В работата си той обяснява цялата теория с прости думи, така че може да се каже, че Чърч публикува ламбда-изчислението за манекени.
До 60-те години на миналия век, когато връзката му с езиците за програмиране стана ясна, λ беше просто формализъм. Благодарение на приложенията на Ричард Монтагю и други лингвисти в семантиката на естествения език, смятането зае гордо място както в лингвистиката, така и в компютърните науки.
Произход на символа
Lambda не означава дума или акроним, идва от препратка в Основната математика на Ръсел, последвана от две типографски промени. Пример за нотация: за функция f с f (y)=2y + 1 е 2ŷ + 1. И тук използваме карета („шапка“) над y за етикетиране на входната променлива.
Църквата първоначално е възнамерявала да използва подобни символи, но наборчиците не успяха да поставят символа "шапка" над буквите. Вместо това те го отпечатаха първоначално като "/\y.2y+1". В следващия епизод на редактиране машинописците замениха "/ \" с визуално подобен знак.
Въведение в ламбда смятането
Системата се състои от език на термините, които са избрани от определен формален синтаксис, и набор от правила за трансформация, които позволяват да бъдат манипулирани. Последната точка може да се разглежда като теория на уравненията или като оперативна дефиниция.
Всички функции в ламбда изчислението са анонимни, което означава, че нямат имена. Те приемат само една входна променлива, а кърирането се използва за изпълнение на графики с множество променливи.
Ламбда термини
Синтаксисът на изчислението дефинира някои изрази като валидни, а други като невалидни. Точно както различните низове от знаци са валидни C програми, а някои не са. Действителният израз на ламбда изчислението се нарича "ламбда термин".
Следните три правила предоставят индуктивна дефиниция, която може да бъдесе прилага за изграждането на всички синтактично валидни понятия:
Самата променлива x е валиден ламбда термин:
- ако T е LT и x е непостоянен, тогава (lambda xt) се нарича абстракция.
- ако T, както и s са понятия, тогава (TS) се нарича приложение.
Нищо друго не е ламбда термин. По този начин една концепция е валидна, ако и само ако може да бъде получена чрез многократно прилагане на тези три правила. Въпреки това някои скоби могат да бъдат пропуснати според други критерии.
Определение
Ламбда изразите се състоят от:
- променливи v 1, v 2, …, v n, …
- символи на абстракция 'λ' и точка '.'
- скоби ().
Наборът Λ може да бъде дефиниран индуктивно:
- Ако x е променлива, тогава x ∈ Λ;
- x не е константа и M ∈ Λ, тогава (λx. M) ∈ Λ;
- M, N ∈ Λ, след това (MN) ∈ Λ.
Обозначение
За да запазите нотацията на ламбда изразите без претрупване, обикновено се използват следните конвенции:
- Външните скоби са пропуснати: MN вместо (MN).
- Приложенията се приемат да останат асоциативни: може да се пише MNP вместо ((MN) P).
- Тялото на абстракцията се простира още надясно: λx. MN означава λx. (MN), не (λx. M) N.
- Последователността от абстракции е намалена: λx.λy.λz. N може да бъде λxyz. N.
Свободни и обвързани променливи
Операторът λ свързва своята неконстанта, където и да е в тялото на абстракцията. Променливите, които попадат в обхвата, се наричат обвързани. В израза λ x. М, частта λ x често се нарича свързващо вещество. Сякаш намеква, че променливите стават група с добавяне на X x към M. Всички останали нестабилни се наричат свободни.
Например, в израза λ y. x x y, y - обвързан непостоянен, и x - свободен. И също така си струва да се отбележи, че променливата е групирана по своята "най-близка" абстракция. В следващия пример решението на ламбда изчислението е представено с еднократно появяване на x, което е свързано с втория член:
λ x. y (λ x. z x)
Наборът от свободни променливи M се обозначава като FV (M) и се дефинира чрез рекурсия върху структурата на термините, както следва:
- FV (x)={x}, където x е променлива.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Формула, която не съдържа свободни променливи, се нарича затворена. Затворените ламбда изрази са известни също като комбинатори и са еквивалентни на термини в комбинаторната логика.
Съкращение
Значението на ламбда изразите се определя от това как те могат да бъдат съкратени.
Има три вида разфасовки:
- α-трансформация: промяна на свързаните променливи (алфа).
- β-редукция: прилагане на функции към техните аргументи (бета).
- η-трансформация: обхваща понятието екстенсионалност.
Ето същоговорим за получените еквивалентности: два израза са β-еквивалентни, ако могат да бъдат β-преобразувани в един и същи компонент, а α / η-еквивалентността се дефинира по подобен начин.
Терминът redex, съкратено от намален оборот, се отнася до подтеми, които могат да бъдат намалени с някое от правилата. Ламбда изчисление за манекени, примери:
(λ x. M) N е бета редекс в израза за заместване на N с x в M. Компонентът, до който редексът намалява, се нарича негов редукция. Намалението (λ x. M) N е M [x:=N].
Ако x не е свободно в M, λ x. M x също em-REDEX с регулатор M.
α-трансформация
Алфа преименуванията ви позволяват да променяте имената на свързаните променливи. Например, x. x може да даде λ y. г. Термините, които се различават само по алфа трансформация, се казва, че са α-еквивалентни. Често, когато се използва ламбда изчислението, α-еквивалентите се считат за реципрочни.
Точните правила за алфа преобразуване не са съвсем тривиални. Първо, с тази абстракция се преименуват само онези променливи, които са свързани със същата система. Например алфа трансформацията λ x.λ x. x може да доведе до λ y.λ x. x, но това може да не доведе до λy.λx.y Последното има различно значение от оригинала. Това е аналогично на концепцията за програмиране на променливо сенки.
На второ място, алфа трансформацията не е възможна, ако би довела до улавяне от непостоянна друга абстракция. Например, ако замените x с y в λ x.λ y. x, тогава можете да получитеλy.λy. u, което изобщо не е същото.
В езиците за програмиране със статичен обхват, алфа преобразуването може да се използва за опростяване на разделянето на имена. В същото време, като се внимава концепцията за променлива да не маскира обозначението в съдържащата област.
В индексната нотация на De Bruyne всеки два алфа-еквивалентни термина са синтактично идентични.
Замяна
Промените, записани от E [V:=R], са процесът на заместване на всички свободни срещания на променливата V в израза E с оборота R. Заместването по отношение на λ се дефинира от ламбдата на рекурсията изчисляване на структурата на концепцията, както следва (забележка: x и y - само променливи и M и N - всеки λ-израз).
x [x:=N] ≡ N
y [x:=N] ≡ y, ако x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) ако x ≠ y, при условие че y ∉ FV (N).
За заместване в ламбда абстракция, понякога е необходимо α-трансформиране на израз. Например, не е вярно, че (λ x. Y) [y:=x] води до (λ x. X), тъй като заместеното x е трябвало да бъде свободно, но в крайна сметка е свързано. Правилното заместване в този случай е (λ z. X) до α-еквивалентност. Имайте предвид, че заместването е уникално дефинирано до ламбда.
β-намаляване
бета намаляването отразява идеята за прилагане на функция. Бета-редуктивното се дефинира в терминизаместване: ((X V. E) E ') е E [V:=E'].
Например, ако приемем някакво кодиране 2, 7, ×, има следното β-редукция: ((λ n. N × 2) 7) → 7 × 2.
Редукцията на бета може да се разглежда като същата като концепцията за локална редуцируемост при естествена дедукция чрез изоморфизма на Къри-Хауърд.
η-transform
Това преобразуване изразява идеята за екстенсионалност, която в този контекст е, че две функции са равни, когато дават един и същ резултат за всички аргументи. Това преобразуване се обменя между λ x. (F x) и f всеки път, когато x не изглежда свободен в f.
Това действие може да се разглежда като същото като концепцията за локална пълнота в естествената дедукция чрез изоморфизма на Къри-Хауърд.
Нормални форми и сливане
За нетипизирано ламбда изчисление, правилото за β-редукция обикновено не е нито силно, нито слабо нормализиращо.
Въпреки това може да се покаже, че β-редукцията се слива, когато се изпълнява преди α-трансформацията (т.е. две нормални форми могат да се считат за равни, ако е възможна α-трансформация от едната към другата).
Следователно, както силно нормализиращите термини, така и слабо коригиращите термини имат една нормална форма. За първите срокове всяка стратегия за намаляване гарантирано ще доведе до типична конфигурация. Докато при слабо нормализиращи се условия някои стратегии за намаляване може да не го намерят.
Допълнителни методи за програмиране
Има много идиоми за създаване за ламбда смятането. Много от тях първоначално са разработени в контекста на използване на системи като основа за семантиката на език за програмиране, като ефективно ги прилагат като конструкция от ниско ниво. Тъй като някои стилове включват ламбда изчисление (или нещо много подобно) като фрагмент, тези техники намират приложение и в практическото създаване, но след това могат да се възприемат като неясни или чужди..
Именувани константи
В ламбда изчислението библиотеката приема формата на набор от предварително дефинирани функции, където термините са просто конкретни константи. Чистото смятане няма концепция за именувани неизменни, тъй като всички атомни ламбда термини са променливи. Но те също могат да бъдат имитирани, като се вземе променливото като име на константата, като се използва ламбда абстракция, за да се свърже това летливо в тялото, и се прилага тази абстракция към предвидената дефиниция. Така че, ако използвате f за представяне на M в N, можете да кажете
(λ f. N) M.
Авторите често въвеждат синтактична концепция, като например позволяване на нещата да бъдат написани по по-интуитивен начин.
f=M до N
Чрез свързване на такива дефиниции, човек може да напише "програма" за ламбда изчисление като нула или повече дефиниции на функции, последвани от един ламбда член, използвайки тези дефиниции, които съставляват по-голямата част от програмата.
Забележимо ограничение на това поле е, че името f не е дефинирано в M,тъй като M е извън обхвата на свързване на ламбда абстракцията f. Това означава, че атрибут на рекурсивна функция не може да се използва като M с let. По-усъвършенстваният синтаксис на letrec, който ви позволява да пишете дефиниции на рекурсивни функции в този стил, освен това използва комбинатори с фиксирана точка.
Печатни аналози
Този тип е типизиран формализъм, който използва символ за представяне на абстракция на анонимна функция. В този контекст типовете обикновено са обекти от синтактичен характер, които се приписват на ламбда термини. Точният характер зависи от въпросното смятане. От определена гледна точка, типизираният LI може да се разглежда като усъвършенстване на нетипизиран LI. Но от друга страна, те също могат да се считат за по-фундаментална теория, а нетипизираното ламбда изчисление е специален случай само с един тип.
Typed LI са основата на езиците за програмиране и гръбнакът на функционалните езици като ML и Haskell. И по-непряко, императивни стилове на създаване. Типизираните ламбда изчисления играят важна роля в разработването на типови системи за езици за програмиране. Тук възможността за писане обикновено улавя желаните свойства на програмата, например няма да причини нарушение на достъпа до паметта.
Въведените ламбда изчисления са тясно свързани с математическата логика и теорията на доказателствата чрез изоморфизма на Къри-Хауърд и могат да се разглеждат като вътрешен език на категорийните класове, например, койтопросто е стилът на декартовото затваряне.
