Тайпталған лямбда-есептеуі – типтермен жұмыс істейтін формализм. Функционалдық бағдарламалау тілдерінің (ML, Haskell) негізі, қауіпсіздікті қамтамасыз етеді.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Типтелген ламбда-калькуль – анонимді функциялық абстракцияны белгілеу үшін ламбда символын пайдаланатын типтелген формализм. Бұл контексте типтер әдетте синтаксистік табиғаттағы объектілер болып табылады, олар ламбда термдеріне тағайындалады; типтің нақты табиғаты қарастырылып отырған калькульге байланысты (төмендегі түрлерді қараңыз). Бір тұрғыдан алғанда, типтелген ламбда калькульдерін типтелмеген ламбда калькульдің жетілдірілген түрі деп қарастыруға болады, бірақ екінші тұрғыдан алғанда, оларды негізгі теория деп санауға болады, ал типтелмеген ламбда калькуль – тек бір типті қамтитын ерекше жағдай. Типтелген ламбда калькульдері – негізгі бағдарламалау тілдері және ML және Haskell сияқты типтелген функционалдық бағдарламалау тілдерінің негізі болып табылады, сондай-ақ, жанама түрде типтелген императивті бағдарламалау тілдерінің дамуына әсер етеді. Типтелген ламбда калькульдері бағдарламалау тілдері үшін типтік жүйелерді жобалауда маңызды рөл атқарады; мұнда типтеу бағдарламаның қажетті қасиеттерін қамтиды (мысалы, бағдарлама жадқа рұқсатсыз қол жеткізуге себеп болмайды). Типтелген ламбда калькульдері Кьюри-Ховард изоморфизмі арқылы математикалық логика мен дәлелдеу теориясымен тығыз байланысты және оларды кейбір категориялар кластарының ішкі тілі деп қарастыруға болады. Мысалы, қарапайым типтелген ламбда калькуль Картезиандық жабық категориялардың (CCC) тілі болып табылады.
A typed lambda calculus is a typed formalism that uses the lambda symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see kinds below). From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus, but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type. Typed lambda calculi are foundational programming languages and are the base of typed functional programming languages such as ML and Haskell and, more indirectly, typed imperative programming languages. Typed lambda calculi play an important role in the design of type systems for programming languages; here, typability usually captures desirable properties of the program (e. g., the program will not cause a memory access violation). Typed lambda calculi are closely related to mathematical logic and proof theory via the Curry–Howard isomorphism and they can be considered as the internal language of certain classes of categories. For example, the simply typed lambda calculus is the language of Cartesian closed categories (CCCs)
Типі бар ламбда калькулі түрлері
Түрлі типтелген ламбда калькульдері зерттелді. Қарапайым типтелген ламбдалық есептеуде тек бір типтік конструктор бар, яғни жебе, және оның типтері негізгі типтер мен функция типтері ғана. T жүйесі қарапайым типтелген ламбдалық есептеуді табиғи сандар және жоғары ретті примитивті рекурсиямен кеңейтеді; бұл жүйеде Пеано арифметикасында дәлелдеме арқылы рекурсивті болатын барлық функция анықталады. F жүйесі полиморфизмге барлық типтер бойынша әмбебап квантификацияны пайдалану арқылы мүмкіндік береді; логикалық тұрғыдан алғанда, ол екінші реттік логикада толық дәлелденген барлық функцияларды сипаттай алады. Тәуелді типтері бар ламбда калькульдері интуиционистік типтер теориясының, конструкциялар калькулының және логикалық базаның (LF) негізі болып табылады – бұл тәуелді типтері бар таза ламбда калькулы. Берардидің таза типтік жүйелердегі жұмысына сүйене отырып, Хенк Барендрегт таза типтелген ламбда калькульдерінің (оның ішінде қарапайым типтелген ламбда калькулі, F жүйесі, LF және конструкциялар калькулы) қатынастарын жүйелеу үшін Ламбда кубін ұсынды. Бұрын аталған жүйелердің барлығы, типтелмеген ламбда калькулінен басқа, күшті нормалдануға ие: барлық есептеулер аяқталады. Сондықтан олар барлық Тьюринг есептелетін функцияларын сипаттауға қабілетсіз. Сонымен қатар, олар логикалық тұрғыдан дұрыс, яғни, мәні жоқ типтер бар. Дегенмен, күшті нормалдануға ие емес типтелген ламбда калькульдері де бар. Мысалы, барлық типтердің типі бар тәуелді типтелген ламбдалық есептеу (Тип: Тип) Жирард парадоксының салдарынан нормалдана алмайды. Бұл жүйе сонымен қатар ең қарапайым таза типтік жүйе болып табылады, ол Ламбда кубін жалпылайтын формализм. Эксплицитті рекурсиялық комбинаторлары бар жүйелер, мысалы, Плоткиннің "Компьютерлік функциялар үшін бағдарламалау тілі" (PCF), нормалдана алмайды, бірақ олар логика ретінде интерпретациялануға арналмаған. Шындығында, PCF – прототиптік типтелген функционалдық бағдарламалау тілі, онда типтер бағдарламалардың дұрыс жұмыс істеуін қамтамасыз ету үшін қолданылады, бірақ міндетті түрде олардың аяқталуын емес.
Various typed lambda calculi have been studied. The simply typed lambda calculus has only one type constructor, the arrow , and its only types are basic types and function types System T extends the simply typed lambda calculus with a type of natural numbers and higher order primitive recursion; in this system all functions provably recursive in Peano arithmetic are definable. System F allows polymorphism by using universal quantification over all types; from a logical perspective it can describe all functions that are provably total in second order logic. Lambda calculi with dependent types are the base of intuitionistic type theory, the calculus of constructions and the logical framework (LF), a pure lambda calculus with dependent types. Based on work by Berardi on pure type systems, Henk Barendregt proposed the Lambda cube to systematize the relations of pure typed lambda calculi (including simply typed lambda calculus, System F, LF and the calculus of constructions). Some typed lambda calculi introduce a notion of subtyping, i. e. if is a subtype of , then all terms of type also have type Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and System F<:. All the systems mentioned so far, with the exception of the untyped lambda calculus, are strongly normalizing: all computations terminate. Therefore, they cannot describe all Turing computable functions. As another consequence they are consistent as a logic, i. e. there are uninhabited types. There exist, however, typed lambda calculi that are not strongly normalizing. For example the dependently typed lambda calculus with a type of all types (Type : Type) is not normalizing due to Girard's paradox. This system is also the simplest pure type system, a formalism which generalizes the Lambda cube. Systems with explicit recursion combinators, such as Plotkin's "Programming language for Computable Functions" (PCF), are not normalizing, but they are not intended to be interpreted as a logic. Indeed, PCF is a prototypical, typed functional programming language, where types are used to ensure that programs are well behaved but not necessarily that they are terminating.
Бағдарламалау тілдеріне қолдану
Компьютерлік бағдарламалауда, күшті типтелген бағдарламалау тілдерінің процедуралары (функциялары, процедуралары, методтары) типтелген лямбда-өрімдерге тікелей сәйкес келеді.
In computer programming, the routines (functions, procedures, methods) of strongly typed programming languages closely correspond to typed lambda expressions.