Ламбда эсептөөсү – математикалык логикада абстракцияга негизделген эсептөөлөрдү туюнтуу жана байланыштыруучу жана өзгөрмө алмаштырууну колдонуу менен функцияларды колдонуу үчүн формалдуу система. Бул ар кандай Тьюринг машинасынын дизайнына колдонула турган универсалдуу модель. Ламбда эсептөөсү биринчи жолу 1930-жылдары белгилүү математик Черч тарабынан киргизилген.
Тутум ламбда мүчөлөрүн куруудан жана аларда кыскартуу операцияларын аткаруудан турат.
Түшүндүрүү жана колдонмолор
Грекче lambda (λ) тамгасы лямбда туюнтмаларында жана ламбда терминдеринде функциядагы өзгөрмөнүн байланышын белгилөө үчүн колдонулат.
Ламбда эсебин терүүгө же терүүгө болот. Биринчи вариантта функциялар ушул типтеги маалыматтарды кабыл алууга жөндөмдүү болгондо гана колдонулушу мүмкүн. Терилген ламбда таштары алсызыраак, кичине маанини билдире алат. Бирок, экинчи жагынан, алар сизге көбүрөөк нерселерди далилдөөгө мүмкүндүк берет.
Мынчалык көп түрдүү типтердин болушунун бир себеби - илимпоздордун ламбда эсептөөлөрүнүн күчтүү теоремаларын далилдөө мүмкүнчүлүгүнөн баш тартпастан дагы көп нерсеге умтулуусу.
Тутум математиканын, философиянын, лингвистиканын жана информатиканын ар кандай тармактарында колдонмолорго ээ. Биринчиден, ламбда эсептөөсү программалоо тилдеринин теориясын өнүктүрүүдө маанилүү роль ойногон эсептөө болуп саналат. Бул системаларды ишке ашыруучу функционалдык түзүүнүн стилдери. Алар ошондой эле бул категориялардын теориясын изилдөөнүн актуалдуу темасы.
Муляждар үчүн
Лямбда эсептөөсү 1930-жылдары математик Алонзо чиркөөсү тарабынан илимдин негиздерин изилдөөнүн бир бөлүгү катары киргизилген. 1935-жылы Стивен Клин менен Дж. Б. Россер Клин-Россер парадоксун иштеп чыкканда, баштапкы система логикалык жактан дал келбей турганы көрсөтүлгөн.
Кийинчерээк, 1936-жылы, Черч эсептөөлөргө тиешелүү бөлүгүн гана бөлүп чыгарып, басып чыгарган, азыр типтештирилбеген ламбда эсептөөсү деп аталат. 1940-жылы ал алсызыраак, бирок логикалык жактан ырааттуураак теорияны киргизген, ал биринчи типтеги система деп аталган. Ал өз ишинде бүт теорияны жөнөкөй сөз менен түшүндүрөт, ошондуктан Черч муляждар үчүн ламбда эсептөөсүн чыгарган деп айтууга болот.
1960-жылдарга чейин, анын программалоо тилдерине болгон мамилеси айкын болуп калганда, λ жөн гана формализм болгон. Ричард Монтагунун жана башка лингвисттердин табигый тилдин семантикасындагы колдонмолорунун аркасында эсептөө лингвистикада да, информатикада да сыймыктанган орунду ээледи.
Символдун келип чыгышы
Ламбда бир сөздү же акронимди билдирбейт, ал Расселлдин Негизги Математикасындагы шилтемеден келип чыккан, андан кийин эки типографиялык өзгөртүү. Белгилердин мисалы: f (y)=2y + 1 болгон f функциясы үчүн 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.
- Тиркемелер ассоциативдик бойдон калат деп болжолдонууда: ((MN) P ордуна MNP жазса болот).
- Абстракциянын денеси андан ары оңго созулат: λx. MN λx дегенди билдирет. (MN), эмес (λx. M) N.
- Абстракциялардын ырааттуулугу кыскартылган: λx.λy.λz. N λxyz. N болушу мүмкүн.
Эркин жана чектелген өзгөрмөлөр
Оператор λ анын туруктуу эмесин абстракциянын денесинин кайсы жеринде болсо да бириктирет. Аймакка кирген өзгөрмөлөр байланышкан деп аталат. λ x туюнтмасында. M, λ х бөлүгү көбүнчө бириктиргич деп аталат. Өзгөрмөлөрдүн Мга X x кошулуусу менен топ болуп калганын кыйыткандай. Калган туруксуздардын баары эркин деп аталат.
Мисалы, λ y туюнтмасында. x x y, y - байланган туруктуу эмес, жана x - эркин. Ошондой эле өзгөрмө анын "жакынкы" абстракциясы боюнча топтолгондугун белгилей кетүү керек. Төмөнкү мисалда, ламбда эсептөө чечими экинчи мөөнөткө байланыштуу болгон x бир эле көрүнүшү менен берилген:
λ x. y (λ x. z x)
М эркин өзгөрмөлөрүнүн жыйындысы FV (M) катары белгиленет жана терминдердин структурасы боюнча рекурсия менен төмөнкүдөй аныкталат:
- FV (x)={x}, мында x өзгөрмө.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Бош өзгөрмөлөрдү камтыбаган формула жабык деп аталат. Жабык ламбда туюнтмалары комбинаторлор катары да белгилүү жана комбинатордук логикадагы терминдерге эквиваленттүү.
Кыскартуу
Лямбда туюнтмаларынын мааниси аларды кантип кыскартса болору менен аныкталат.
Кыскартуунун үч түрү бар:
- α-трансформация: чектелген өзгөрмөлөрдү өзгөртүү (альфа).
- β-кыскартуу: алардын аргументтерине функцияларды колдонуу (бета).
- η-трансформация: кеңейтүү түшүнүгүн камтыйт.
Мына дасөз натыйжадагы эквиваленттүүлүк жөнүндө болуп жатат: эки туюнтма β-эквиваленттүү, эгерде аларды бир эле компонентке β-трансформациялоо мүмкүн болсо, жана α / η-эквиваленттүүлүк окшош аныкталат.
Кыскартыла турган жүгүртүү үчүн кыскартылган redex термини эрежелердин бири менен кыскартыла турган субтемаларга тиешелүү. Муляждар үчүн ламбда эсептөөлөрү, мисалдар:
(λ x. M) N – Mдеги N менен х менен алмаштыруу туюнтмасындагы бета-кайра деккс. Редекс төмөндөтүүчү компонент анын кыскаруусу деп аталат. Кыскартуу (λ x. M) N - M [x:=N].
Эгер x Mде бош болбосо, λ x. M x ошондой эле em-REDEX жөнгө салуучу M.
α-трансформация
Альфа аталыштары чектелген өзгөрмөлөрдүн атын өзгөртүүгө мүмкүндүк берет. Мисалы, х. x λ у бере алат. ж. Альфа трансформациясында гана айырмаланган терминдер α-эквивалент деп аталат. Көбүнчө, ламбда эсептөөсүн колдонгондо, α-эквиваленттер өз ара эсептелинет.
Альфа конверсиясынын так эрежелери анча деле маанилүү эмес. Биринчиден, бул абстракция менен бир эле система менен байланышкан өзгөрмөлөр гана аталышы өзгөртүлөт. Мисалы, альфа трансформациясы λ x.λ x. x λ y.λ x алып келиши мүмкүн. x, бирок бул λy.λx.y алып келбеши мүмкүн, акыркысы түпнускадан башка мааниге ээ. Бул өзгөрмөлөрдү көмүскө программалоо концепциясына окшош.
Экинчиден, эгер ал туруктуу эмес башка абстракция тарабынан кармалып калышына алып келсе, альфа-трансформация мүмкүн эмес. Мисалы, эгер сиз λ x.λ y ичинде xти у менен алмаштырсаңыз. x, анда ала аласызλy.λy. u, бул такыр окшош эмес.
Статикалык масштабы бар программалоо тилдеринде альфа конверсиясы аталышты чечүүнү жөнөкөйлөтүү үчүн колдонулушу мүмкүн. Ошол эле учурда, өзгөрмө түшүнүгү камтылган аймакта белгилөөнү жаап-жашырбашы үчүн кам көрүү.
Де Брюйне индексинин нотасында каалаган эки альфа-эквиваленттүү терминдер синтаксистик жактан бирдей.
Алмаштыруу
E [V:=R] тарабынан жазылган өзгөртүүлөр E туюнтмасындагы V өзгөрмөсүнүн бардык эркин көрүнүштөрүн 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.
Бета редукциясын Карри-Ховард изоморфизми аркылуу табигый чегерүү учурундагы жергиликтүү кыскартуу концепциясы менен бирдей көрүүгө болот.
η-трансформация
Бул конверсия кеңейтүү идеясын билдирет, бул контекстте эки функция бардык аргументтер үчүн бирдей натыйжа бергенде бирдей болот. Бул конверсия λ x ортосунда алмашат. (F x) жана f f. ичинде x бош көрүнбөгөндө
Бул аракетти Карри-Ховард изоморфизми аркылуу табигый дедукциядагы локалдык толуктук концепциясы менен бирдей деп кароого болот.
Кадимки формалар жана синтез
Типделбеген ламбда эсептөөсү үчүн β-кыскартуу эрежеси көбүнчө күчтүү да, алсыз да нормалдаштыруу эмес.
Ошентсе да, α-трансформацияга чейин иштегенде β-кыскартуу бириге турганын көрсөтсө болот (б.а., эгер биринен экинчисине α-трансформация мүмкүн болсо, эки нормалдуу форма бирдей деп эсептелинет).
Ошондуктан, катуу нормалдаштыруучу терминдер да, начар тууралоочу терминдер да бир нормалдуу формага ээ. Биринчи шарттар үчүн, ар кандай кыскартуу стратегиясы типтүү конфигурацияга алып келет деп кепилдик берилет. Ал эми шарттарды нормалдаштыруу начар болсо, кээ бир кыскартуу стратегиялары аны таппай калышы мүмкүн.
Кошумча программалоо ыкмалары
Лямбда эсептөөсү үчүн жаратуу идиомалары көп. Алардын көбү адегенде системаларды программалоо тилинин семантикасынын негизи катары колдонуу контекстинде иштелип чыккан, аларды төмөнкү деңгээлдеги конструкция катары эффективдүү колдонуу. Кээ бир стилдер фрагмент катары ламбда эсептөөсүн (же абдан окшош нерсени) камтыгандыктан, бул ыкмалар практикалык жаратууда да колдонулат, бирок кийин бүдөмүк же чет элдик катары кабыл алынышы мүмкүн.
Аты аталган константалар
Лямбда эсептөөсүндө китепкана мурда аныкталган функциялардын жыйындысы формасын алат, мында терминдер жөн гана конкреттүү константалар. Таза эсептөөдө аталган өзгөрүлгүстөр түшүнүгү жок, анткени бардык атомдук ламбда терминдери өзгөрмөлөр. Бирок аларды константтын аталышы катары өзгөрүлүүчүнү алып, лямбда абстракциясын колдонуп, ошол туруксуз затты денеде байланыштырып, ошол абстракцияны белгиленген аныктамага колдонуу менен да окшоштурса болот. Демек, N тилинде Mди көрсөтүү үчүн f колдонсоңуз,деп айтсаңыз болот.
(λ f. N) M.
Авторлор көбүнчө нерселерди интуитивдик жол менен жазууга мүмкүндүк берүү сыяктуу синтаксистик түшүнүктү киргизишет.
f=M - N
Мындай аныктамаларды чынжырлап, программанын негизги бөлүгүн түзгөн аныктамаларды колдонуп, ламбда эсептөө "программасын" нөл же андан көп функция аныктамалары, андан кийин бир ламбда мүчөсү катары жазууга болот.
Мунун көрүнүктүү чектөөсү, f аталышынын Mде аныкталбаганы,анткени M ламбда абстракциясынын милдеттүү чөйрөсүнөн тышкары f. Бул рекурсивдүү функция атрибутун let менен M катары колдонууга болбойт дегенди билдирет. Бул стилде рекурсивдүү функциянын аныктамаларын жазууга мүмкүндүк берген өркүндөтүлгөн letrec синтаксиси анын ордуна кошумча туруктуу чекиттүү бириктиргичтерди колдонот.
Басып чыгарылган аналогдор
Бул тип анонимдүү функциянын абстракциясын көрсөтүү үчүн символду колдонгон терилген формализм. Бул контекстте типтер адатта ламбда терминдерине ыйгарылган синтаксистик мүнөздөгү объектилер болуп саналат. Так табияты каралып жаткан эсептөөлөрдөн көз каранды. Белгилүү бир көз караштан алганда, терилген ЛИ типтештирилбеген ЛИнин тактоолору катары каралышы мүмкүн. Бирок, экинчи жагынан, аларды дагы фундаменталдуу теория катары кароого болот жана типтештирилбеген ламбда эсептөөсү бир гана түрү бар өзгөчө учур.
Typed LI программалоо тилдеринин негизи жана ML жана Haskell сыяктуу функционалдык тилдердин негизи болуп саналат. Жана, кыйыр түрдө, түзүүнүн императивдик стилдери. Терилген ламбда эсептөөлөрү программалоо тилдери үчүн типтүү системаларды иштеп чыгууда маанилүү роль ойнойт. Бул жерде терүү мүмкүнчүлүгү адатта программанын керектүү касиеттерин камтыйт, мисалы, эстутумга кирүү мүмкүнчүлүгүн бузууга алып келбейт.
Типтелген ламбда эсептери Карри-Ховард изоморфизми аркылуу математикалык логика жана далилдөө теориясы менен тыгыз байланышта жана категория класстарынын ички тили катары кароого болот, мисалы,жөн гана декарттык жабуунун стили.
