Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка 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 и исчисление конструкций). Некоторые типизированные ламбда-исчисления вводят понятие подтипирования, то есть, если является подтипом , то все термы типа также имеют тип . Типизированные ламбда-исчисления с подтипированием – это просто типизированное ламбда-исчисление с конъюнктивными типами и Система F<:. Все системы, упомянутые до сих пор, за исключением нетипизированного ламбда-исчисления, сильно нормализуемы: все вычисления завершаются. Следовательно, они не могут описать все функции, вычислимые по Тьюрингу. Как следствие, они логически непротиворечивы, то есть существуют необитаемые типы. Однако существуют типизированные ламбда-исчисления, которые не являются сильно нормализуемыми. Например, зависимо типизированное ламбда-исчисление с типом всех типов (Type : Type) не нормализуется из-за парадокса Жирара. Эта система также является самой простой чистой системой типов, формализмом, обобщающим куб Ламбды. Системы с явными рекурсивными комбинаторами, такие как «язык программирования для вычислимых функций» (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.