Лямбда есептеуі – абстракцияға негізделген есептеулерді өрнектеуге және байланыстыру және айнымалыларды ауыстыру арқылы функцияларды қолдануға арналған математикалық логикадағы ресми жүйе. Бұл кез келген Тьюринг машинасының дизайнына қолдануға болатын әмбебап модель. Ламбда есебін алғаш рет 1930 жылдары әйгілі математик Черч енгізген.
Жүйе ламбда мүшелерін құрудан және оларда азайту операцияларын орындаудан тұрады.
Түсіндірмелер мен қолданбалар
Грек әрпі lambda (λ) лямбда өрнектерінде және лямбда терминдерінде функциядағы айнымалының байланысуын белгілеу үшін қолданылады.
Лямбда есебін теруге немесе теруге болады. Бірінші нұсқада функциялар осы түрдегі деректерді қабылдау мүмкіндігіне ие болған жағдайда ғана пайдаланылуы мүмкін. Терілген ламбда тастары әлсіз, кішірек мәнді көрсете алады. Бірақ, керісінше, олар сізге көп нәрсені дәлелдеуге мүмкіндік береді.
Түрлі түрлердің көп болуының бір себебі – ғалымдардың ламбда есептеулерінің күшті теоремаларын дәлелдеу мүмкіндігінен бас тартпай, көп нәрсені істеуге ұмтылысы.
Жүйенің математика, философия, лингвистика және информатиканың көптеген әртүрлі салаларында қолданбалары бар. Ең алдымен, ламбда есептеулері программалау тілдерінің теориясын дамытуда маңызды рөл атқарған есептеулер болып табылады. Бұл жүйелер жүзеге асыратын функционалдық құру стильдері. Олар сондай-ақ осы категориялар теориясы бойынша зерттеудің өзекті тақырыбы болып табылады.
Манекелер үшін
Лямбда есебін 1930 жылдары математик Алонзо шіркеуі ғылым негіздерін зерттеудің бір бөлігі ретінде енгізген. 1935 жылы Стивен Клин мен Дж. Б. Россер Клин-Россер парадоксын жасағанда, бастапқы жүйе логикалық тұрғыдан сәйкес келмейтіні көрсетілді.
Кейінірек, 1936 жылы Черч тек есептеулерге қатысы бар бөлігін бөліп алып, жариялады, қазір оны типтелмеген ламбда есебі деп атайды. 1940 жылы ол сондай-ақ қарапайым типті жүйе деп аталатын әлсіз, бірақ логикалық тұрғыдан дәйекті теорияны енгізді. Ол өз жұмысында барлық теорияны қарапайым тілмен түсіндіреді, сондықтан Черч манекендерге арналған ламбда есептеулерін жариялады деп айтуға болады.
1960 жылдарға дейін, оның бағдарламалау тілдерімен байланысы анық болған кезде, λ жай ғана формализм болды. Ричард Монтагу және басқа лингвисттердің табиғи тілдің семантикасындағы қолданбаларының арқасында есептеулер лингвистикада да, информатикада да мақтаныш болды.
Символның шығу тегі
Ламбда сөзді немесе аббревиатураны білдірмейді, ол Расселлдің негізгі математикасындағы екі типографиялық өзгерістен кейін алынған анықтамадан шыққан. Белгілеу мысалы: f (y)=2y + 1 функциясы бар f функциясы үшін 2ŷ + 1 болады. Мұнда кіріс айнымалысын белгілеу үшін у үстінен карет («қалпақ») қолданылады.
Шіркеу бастапқыда ұқсас белгілерді қолдануды көздеді, бірақ терушілер «қалпақ» таңбасын әріптердің үстіне қоя алмады. Сондықтан олар оны бастапқыда "/\y.2y+1" ретінде басып шығарды. Өңдеудің келесі эпизодында терушілер "/ \" таңбасын көрнекі ұқсас таңбамен ауыстырды.
Лямбда есептеулеріне кіріспе
Жүйе белгілі бір формальды синтаксиспен таңдалған терминдер тілінен және оларды өңдеуге мүмкіндік беретін түрлендіру ережелерінің жиынтығынан тұрады. Соңғы нүктені теңдеу теориясы немесе операциялық анықтама ретінде қарастыруға болады.
Лямбда есептеуіндегі барлық функциялар анонимді, яғни олардың атаулары жоқ. Олар тек бір кіріс айнымалысын қабылдайды және карриинг бірнеше айнымалысы бар сызбаларды жүзеге асыру үшін пайдаланылады.
Ламбда шарттары
Есеп синтаксисі кейбір өрнектерді жарамды, ал басқаларын жарамсыз деп анықтайды. Әр түрлі таңбалар қатары жарамды C бағдарламалары сияқты, ал кейбіреулері жарамсыз. Ламбда есебінің нақты өрнегі "лямбда термині" деп аталады.
Келесі үш ереже болуы мүмкін индуктивті анықтаманы бередібарлық синтаксистік жарамды ұғымдардың құрылысына қолданылады:
X айнымалысының өзі жарамды лямбда термині:
- егер T LT және x тұрақты емес болса, онда (лямбда 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 x қосу арқылы топқа айналатынын меңзегендей. Қалған тұрақсыздардың барлығы бос деп аталады.
Мысалы, λ y өрнегінде. x x y, y - байланысқан тұрақты емес, ал х - бос. Сондай-ақ, айнымалы оның «ең жақын» абстракциясы бойынша топтастырылғанын атап өткен жөн. Келесі мысалда ламбда есебінің шешімі екінші мүшеге қатысты 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-ке ауыстыруға арналған өрнектегі бета-редекс. Тотықсыздандырғыш төмендететін компонент оның азаюы деп аталады. Қысқарту (λ x. M) N - M [x:=N].
Егер x M тілінде бос болмаса, λ x. M x сонымен қатар M реттегіші бар em-REDEX.
α-трансформация
Альфа атаулары шектелген айнымалылардың атауларын өзгертуге мүмкіндік береді. Мысалы, x. 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-де М-ні көрсету үшін f қолдансаңыз,деп айтуға болады.
(λ f. N) M.
Авторлар синтаксистік тұжырымдаманы жиі енгізеді, мысалы, нәрселерді интуитивті түрде жазуға мүмкіндік береді.
f=M-N
Осындай анықтамаларды тізбектей отырып, бағдарламаның негізгі бөлігін құрайтын анықтамаларды пайдалана отырып, ламбда есебінің "бағдарламасын" нөл немесе одан да көп функция анықтамалары, одан кейін бір ламбда мүшесі ретінде жазуға болады.
Мұның маңызды шектеуі f атауының M тілінде анықталмағандығы,өйткені M ламбда абстракциясының байланыстыру аймағынан тыс f. Бұл рекурсивті функция төлсипатын let-мен бірге M ретінде пайдалануға болмайтынын білдіреді. Осы стильде рекурсивті функция анықтамаларын жазуға мүмкіндік беретін кеңейтілген letrec синтаксисі оның орнына қосымша бекітілген нүктелі біріктіргіштерді пайдаланады.
Басып шығарылған аналогтар
Бұл тип анонимді функция абстракциясын көрсету үшін таңбаны пайдаланатын терілген формализм. Бұл контексте типтер әдетте ламбда терминдеріне тағайындалған синтаксистік сипаттағы нысандар болып табылады. Нақты табиғат қарастырылып отырған есептеуге байланысты. Белгілі бір тұрғыдан алғанда, терілген ЛИ типтелмеген LI нақтылаулары ретінде қарастырылуы мүмкін. Бірақ екінші жағынан, оларды анағұрлым іргелі теория деп санауға болады, ал типтелмеген ламбда есебі тек бір түрі бар ерекше жағдай болып табылады.
Typed LI - бағдарламалау тілдерінің негізі және ML және Haskell сияқты функционалды тілдердің негізі. Және, жанама түрде, жасаудың императивті стильдері. Типтелген ламбда есептеулері программалау тілдерінің типтік жүйелерін жасауда маңызды рөл атқарады. Мұнда теру мүмкіндігі әдетте бағдарламаның қажетті қасиеттерін түсіреді, мысалы, ол жадқа кіру рұқсатын бұзбайды.
Типтелген лямбда есептеулері Карри-Ховард изоморфизмі арқылы математикалық логикамен және дәлелдеу теориясымен тығыз байланысты және оларды категория кластарының ішкі тілі ретінде қарастыруға болады, мысалы,жай ғана декарттық жабу стилі.
