Лямбда-куб: измерения зависимостей в исчислении конструкций.
Lambda cube
Лямбда-куб: математическая логика, теория типов. Исследование обобщений лямбда-исчисления через зависимости типов и термов (зависимые типы, полиморфизм).
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
В математической логике и теории типов, λ-куб (также называемый кубом лямбда) — это фреймворк, предложенный Хенком Барендрегтом для исследования различных измерений, в которых исчисление конструкций является обобщением просто типизированного λ-исчисления. Каждое измерение куба соответствует новому виду зависимости между термами и типами. Здесь под "зависимостью" понимается способность терма или типа связывать терм или тип. Соответствующие измерения λ-куба следующие:
In mathematical logic and type theory, the λ cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ cube correspond to:
Ось x: типы, способные связывать термы, что соответствует зависимым типам. Ось y: термы, способные связывать типы, что соответствует полиморфизму. Ось z: типы, способные связывать типы, что соответствует (связывающим) операторам типов. Различные комбинации этих трех измерений дают 8 вершин куба, каждая из которых соответствует определенному типу системы. λ-куб может быть обобщен до концепции системы чистых типов.
x axis : types that can bind terms, corresponding to dependent types. y axis : terms that can bind types, corresponding to polymorphism. z axis : types that can bind types, corresponding to (binding) type operators. The different ways to combine these three dimensions yield the 8 vertices of the cube, each corresponding to a different kind of typed system. The λ cube can be generalized into the concept of a pure type system.
(λ→) Простой тип ламбда-расчета
Самая простая система, обнаруженная в λ-кубе, — это ламбда-исчисление с простой типизацией, также называемое λ→. В этой системе единственный способ построить абстракцию — это сделать один член зависимым от другого, с правилом типизации:
The simplest system found in the λ cube is the simply typed lambda calculus, also called λ→. In this system, the only way to construct an abstraction is by making a term depend on a term, with the typing rule:
(λω) Система Fω
В системе F введена конструкция для предоставления типов, зависящих от других типов. Это называется конструктором типа и обеспечивает способ построения "функции, принимающей тип в качестве значения". Примером такого конструктора типа является тип двоичных деревьев с листьями, помеченными данными заданного типа: , где "" неформально означает "является типом". Это функция, которая принимает параметр типа в качестве аргумента и возвращает тип значений типа . В конкретном программировании эта возможность соответствует способности определять конструкторы типов внутри языка, а не рассматривать их как примитивы. Предыдущий конструктор типа примерно соответствует следующему определению дерева с помеченными листьями в OCaml: type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree.
In System F a construction is introduced to supply types that depend on other types. This is called a type constructor and provides a way to build "a function with a type as a value". An example of such a type constructor is the type of binary trees with leaves labeled by data of a given type : , where "" informally means " is a type". This is a function that takes a type parameter as an argument and returns the type of s of values of type In concrete programming, this feature corresponds to the ability to define type constructors inside the language, rather than considering them as primitives. The previous type constructor roughly corresponds to the following definition of a tree with labeled leaves in OCaml:type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree
Этот конструктор типа может быть применен к другим типам для получения новых типов. Например, для получения типа деревьев целых чисел: type int tree = int tree.
This type constructor can be applied to other types to obtain new types. E. g., to obtain type of trees of integers:type int tree = int tree
Система F обычно не используется самостоятельно, но полезна для выделения независимой особенности – конструкторов типов.
System F is generally not used on its own, but is useful to isolate the independent feature of type constructors.
(λP) Ламбда-П
В системе λP, также называемой ΛΠ, и тесно связанной с логической структурой LF Logical Framework, существуют так называемые зависимые типы. Это типы, которым разрешено зависеть от термов. Ключевое правило введения в системе имеет вид
In the λP system, also named ΛΠ, and closely related to the LF Logical Framework, one has so called dependent types. These are types that are allowed to depend on terms. The crucial introduction rule of the system is
где обозначает допустимые типы. Новый конструктор типа соответствует, посредством изоморфизма Карри-Говарда, универсальному квантору, а система λP в целом соответствует логике первого порядка, где единственным связующим элементом является импликация. Примером таких зависимых типов в конкретном программировании является тип векторов заданной длины: длина является термом, от которого зависит тип.
where represents valid types. The new type constructor corresponds via the Curry Howard isomorphism to a universal quantifier, and the system λP as a whole corresponds to first order logic with implication as only connective. An example of these dependent types in concrete programming is the type of vectors on a certain length: the length is a term, on which the type depends.
(λω) Система Fω
Система Fω объединяет конструктор системы F и конструкторы типов из системы F. Таким образом, система Fω обеспечивает наличие как термов, зависящих от типов, так и типов, зависящих от типов.
System Fω combines both the constructor of System F and the type constructors from System F. Thus System Fω provides both terms that depend on types and types that depend on types.
λ2
В λ2 такие термы могут быть получены как с помощью. Если интерпретировать как универсальную квантификацию, то, благодаря изоморфизму Карри-Ховарда, это можно рассматривать как доказательство принципа взрыва. В общем случае, λ2 добавляет возможность иметь импредикативные типы, такие как , то есть термы, квантифицирующие по всем типам, включая сами себя. Полиморфизм также позволяет конструировать функции, которые не были построимы в λ→. Более точно, функции, определимые в λ2, – это те, которые доказуемо тотальны в арифметике Пеано второго порядка. В частности, все примитивно рекурсивные функции определимы.
In λ2, such terms can be obtained aswith If one reads as a universal quantification, via the Curry Howard isomorphism, this can be seen as a proof of the principle of explosion. In general, λ2 adds the possibility to have impredicative types such as , that is terms quantifying over all types including themselves. The polymorphism also allows the construction of functions that were not constructible in λ→. More precisely, the functions definable in λ2 are those provably total in second order Peano arithmetic. In particular, all primitive recursive functions are definable.
λP
В λP возможность задавать типы, зависящие от термов, позволяет выражать логические предикаты. Например, следующее является выводимым: что соответствует, посредством изоморфизма Карри-Говарда, доказательству. С вычислительной точки зрения, однако, наличие зависимых типов не увеличивает вычислительную мощность, а лишь возможность выражать более точные типовые свойства. Правило конверсии (или правило преобразования) крайне необходимо при работе с зависимыми типами, поскольку оно позволяет выполнять вычисления над термами внутри типа. Например, если у вас есть и , вам необходимо применить правило конверсии (или правило преобразования), чтобы получить и, таким образом, иметь возможность определить тип .
In λP, the ability to have types depending on terms means one can express logical predicates. For instance, the following is derivable:which corresponds, via the Curry Howard isomorphism, to a proof of From the computational point of view, however, having dependent types does not enhance computational power, only the possibility to express more precise type properties. The conversion rule is strongly needed when dealing with dependent types, because it allows to perform computation on the terms in the type. For instance, if you have and , you need to apply the conversion rule to obtain to be able to type .
λω
В λω определим следующий оператор, то есть, вывод можно получить уже в λ2, однако полиморфный оператор может быть определен только при наличии правила . С точки зрения вычислительных возможностей, λω чрезвычайно мощна и рассматривается как основа для языков программирования.
In λω, the following operatoris definable, that is The derivationcan be obtained already in λ2, however the polymorphic can only be defined if the rule is also present. From a computing point of view, λω is extremely strong, and has been considered as a basis for programming languages.