Лямбда-ларар

Ля́мбда-лара (λ-ларар) — америкин математико Чёрч Алонзос, ларадаларан кхетамна формализаци а, анализ а ярхьама, кхоьллина формалан система.

ЦӀена λ-ларар

ЦӀена λ-ларар, термаш, цунах кхин а олу объекташ («обаш»), я λ-термаш, хиттийна еккъа хийцалуш йолчу аппликаци а, абстракци а лелош. Юьхьанца цхьан констант а хилар дуьцуш а дац.

Аппликаци а, абстракци а

λ-лараран бухе йиллина шиъ фундаментан операци:

• Кеп:ЯкорьАппликаци (Кеп:Lang-lat — тӀедилла, тӀехоттар) деллачу терхьийна хьалха функци лелор я кхайкхар бохург ду. Иза билгалдоккху $fa$, $f$ — функци ю, ткъа $a$ — аргумент ю. Иза догӀу массара а математикехь тӀеэцнадолчу яздарца $f(a)$, иза а наггахь лелош ду, амма λ-ларарна коьрта ду, $f$ алгоритм маьӀнехь ларар, лоруш долу жамӀ деллачу чудогӀучу терахьца. Оцу маьӀнехь аппликаци $f$ тӀиера $a$ тӀе ган тарло шалха: цхьаъ — жамӀ лелор $f$ тӀиера $a$ тӀе, шиъ — $fa$ лараран процесс санна. ТӀаьххьара аппликацин интерпретаци йоьзна ю β-редукци кхетамах.

• Кеп:ЯкорьАбстракцино я λ-абстракцино (Кеп:Lang-lat — тергояйар, дӀакъастар) шен агӀора функцеш хиттайо деллачу терхьашца. Мадарра, нагахь $t\equiv t[x]$ — терахь делахь, паргӀата $x$ юкъахь долуш, тӀаккха $\lambda x.t[x]$ яздаран маьӀна ду: $\lambda$ функци $x$ аргументах, цуьнан ю $t[x]$ кеп, цуо гойту $x\mapsto t[x]$ функци. Иштта, абстракцин гӀоьнца мега керла функцеш кхолла. Оьшург, $x$ паргӀата юкъадахар $t$, доккха хьесап долуш дац — тоьуш ду дагахь хилар, $\lambda x.t\equiv t$, нагахь иза иштта дацахь.