Ламбда изчисление: описание на теоремата, характеристики, примери

Ламбда-калкулусът е формална система в математическата логика за изразяване на числа, основана на абстракция и прилагане на функции чрез свързване и заместване на променливи. Това е универсален модел, който може да се прилага за проектиране на всяка машина на Тюринг. Въведен за първи път от Чърч, известен математик, през 30-те години на ХХ век.

Системата се състои от конструиране на ламбда членове и извършване на редукционни операции върху тях.

Обяснения и приложения

Гръцката буква ламбда (λ) се използва в ламбда изрази и ламбда термини за обозначаване на свързването на променлива във функция.

Ламбда изчисленията могат да бъдат без типизация или с типизация. В първия вариант функциите могат да се прилагат само ако могат да приемат данни от този тип. Типизираното ламбда изчисление е по-слабо, може да изразява по-малко. Но от друга страна, те позволяват да се докажат повече неща.

Една от причините за съществуването на много различни видове е желанието на учените да правят повече, без да се отказват от възможността да доказват силни теореми от ламбда смятането.

Системата има приложения в много различни области на математиката, философията, лингвистиката и компютърните науки. Преди всичко ламбда-изчислението е изчисление, което е изиграло важна роля в развитието на теорията на езиците за програмиране. Това са функционалните стилове за създаване, които прилагат системите. Те са и актуална тема за изследване в теорията на тези категории.

За глупаци

Ламбда-изчислението е въведено от математика Алонзо Чърч през 30-те години на миналия век като част от изследване на основите на науката. Първоначалната система е показана като логически непоследователна през 1935 г., когато Стивън Клайн, Джей Джей Клин и Джей Ар Клин пишат за теорията на ламбда-изчислението. Б. Росър разработва парадокса на Клайн-Росър.

По-късно, през 1936 г., Чърч отделя и публикува само частта, която е от значение за изчисленията, това, което сега се нарича неизброено ламбда-изчисление. През 1940 г. той представя и по-слаба, но логически последователна теория, известна като проста система от типове. В работата си той обяснява цялата теория на прост език, така че може да се каже, че Чърч е публикувал ламбда-изчислението за манекени.

До 60-те години на миналия век, когато става ясна връзката му с езиците за програмиране, λ е само формализъм. Благодарение на приложенията на Ричард Монтегю и други лингвисти към семантиката на естествения език, калкулът заема почетно място както в лингвистиката, така и в компютърните науки.

Произход на символа

Ламбда не означава дума или съкращение, а произлиза от препратка в "Принцип на математиката" на Ръсел, последвана от две типографски промени. Примерен запис: за функцията f с f (y) = 2y + 1 е 2ŷ + 1. А тук се използва символ за карета ("шапка") над y, за да се маркира входната променлива.

Първоначално църквата е възнамерявала да използва подобни символи, но печатарите не са могли да поставят символа "шапка" върху буквите. Вместо това те са го написали първоначално като "/y.2y+1". В следващия епизод на редактиране съставителите заместват "/ " с визуално подобен символ.

Въведение в ламбда смятането

Системата се състои от език от термини, които се избират чрез определен формален синтаксис, и набор от правила за трансформация, които позволяват тяхното манипулиране. Последната точка може да се разглежда като теория на уравнението или като оперативно определение.

Всички функции в ламбда смятането са анонимни, т.е. без имена. Те приемат само една входна променлива, а за реализиране на графи с няколко непроменливи се използва currying.

Ламбда термини

Синтаксисът на изчисленията определя някои изрази като валидни, а други - като невалидни. Точно както различни символни низове са валидни за програми на C, а някои не са. Валиден израз на ламбда-крайник се нарича ""ламбда-крайник"".

Следващите три правила предоставят индуктивна дефиниция, която може да се приложи за конструиране на всички синтактично валидни термини:

Самата променлива x е валиден ламбда термин:

• ако T е LT и x е непостоянен, тогава (lambda xt) се нарича абстракция.
• ако T и s са понятия, то (TS) се нарича приложение.

Нищо друго не е ламбда термин. Следователно едно понятие е валидно само и единствено, ако може да бъде изведено чрез повторното прилагане на тези три правила. ` Въпреки това някои скоби могат да бъдат пропуснати в съответствие с други критерии.

Определение

Ламбда изразите се състоят от:

• променливи v 1, v 2,..., в н,...
• символите на абстракцията ""λ"" и точката "".`
• скоби ().

Множеството Λ, може да се дефинира индуктивно:

• Ако x е променлива, то x ∈ Λ