Просто напечатанное лямбда-исчисление

исчисление Просто типизированное лямбда- ( $\lambda ^{\to }$), Форма , теории типов представляет собой типизированную интерпретацию лямбда -исчисления только с одним конструктором типа ( $\to$), который создает типы функций . Это канонический и простейший пример типизированного лямбда-исчисления. Просто типизированное лямбда-исчисление было первоначально введено Алонзо Чёрчем в 1940 году как попытка избежать парадоксального использования нетипизированного лямбда-исчисления .

Термин простой тип также используется для обозначения расширений просто типизированного лямбда -исчисления с такими конструкциями, как произведения , копродукции или натуральные числа ( Система T ) или даже полная рекурсия (например, PCF ). Напротив, системы, в которых вводятся полиморфные типы (например, System F ) или зависимые типы (например, Logical Framework ), не считаются просто типизированными . Простые типы, за исключением полной рекурсии, по-прежнему считаются простыми, поскольку кодирование Чёрча таких структур можно выполнить, используя только $\to$ и подходящие переменные типа, тогда как полиморфизм и зависимость не могут.

Синтаксис

В 1930-х годах Алонзо Чёрч стремился использовать логистический метод : его лямбда-исчисление , как формальный язык, основанный на символических выражениях, состояло из счетно бесконечного ряда аксиом и переменных, но также и конечный набор примитивных символов, обозначающие абстракцию и область действия, а также четыре константы: отрицание, дизъюнкция, количественная оценка всеобщности и выбор соответственно; а также конечный набор правил от I до VI. Этот конечный набор правил включал правило V modus ponens , а также правила IV и VI для замены и обобщения соответственно. Правила I–III известны как альфа-, бета- и эта-преобразования в лямбда-исчислении. Чёрч стремился использовать английский только как язык синтаксиса (то есть метаматематический язык) для описания символических выражений без каких-либо интерпретаций.

В 1940 году Чёрч остановился на индексной записи для обозначения типа в символическом выражении. В своей презентации Чёрч использовал только два базовых типа: $o$ для «типа предложений» и $\iota$для «типа людей». Тип $o$ не имеет термоконстант, тогда как $\iota$имеет одну константу. Часто исчисление имеет только один базовый тип, обычно $o$, Считается. Нижние индексы греческих букв $\alpha ,\beta$и т. д. обозначают переменные типа; индекс в скобках $(\alpha \beta )$ обозначает тип функции $\beta \to \alpha$. Черч 1940, стр. 58 использовал «стрелу или $\to$' для обозначения означает или является аббревиатурой для . К 1970-м годам стали использоваться отдельные обозначения стрелок; например, в этой статье символы без индекса $\sigma$ и $\tau$может варьироваться по типам. Тогда считалось, что бесконечное число аксиом является следствием применения к типам правил от I до VI (см. Аксиомы Пеано ). Неформально, тип функции $\sigma \to \tau$ относится к типу функций, которые, учитывая ввод типа $\sigma$, создайте вывод типа $\tau$. Условно, $\to$ партнеры справа: $\sigma \to \tau \to \rho$ читается как $\sigma \to (\tau \to \rho )$.

Чтобы определить типы, набор типов базовых , $B$, необходимо сначала определить. Их иногда называют атомарными типами или константами типов . Если это исправлено, синтаксис типов будет следующим:

$\tau ::=\tau \to \tau \mid T\quad \mathrm {where} \quad T\in B$.

Например, $B=\{a,b\}$, генерирует бесконечный набор типов, начиная с $a$, $b$, $a\to a$, $a\to b$, $b\to b$, $b\to a$, $a\to (a\to a)$, ..., $(b\to a)\to (a\to b)$, ...

набор терминальных констант Для базовых типов также фиксирован . Например, можно предположить, что одним из базовых типов является nat , а его терминальные константы могут быть натуральными числами.

Синтаксис просто типизированного лямбда-исчисления по существу аналогичен синтаксису самого лямбда-исчисления. Термин $x{\mathbin {:}}\tau$ означает, что переменная $x$ имеет тип $\tau$. Синтаксис термина в форме Бэкуса-Наура представляет собой ссылку на переменную , абстракцию , приложение или константу :

$e::=x\mid \lambda x{\mathbin {:}}\tau .e\mid e\,e\mid c$

где $c$является термином-константой. Ссылка на переменную $x$ связан , если он находится внутри привязки абстракции $x$. Терм считается закрытым , если нет несвязанных переменных.

Для сравнения, синтаксис нетипизированного лямбда-исчисления не имеет такой типизации или терминальных констант:

$e::=x\mid \lambda x.e\mid e\,e$

Тогда как в типизированном лямбда-исчислении каждая абстракция (т.е. функция) должна указывать тип своего аргумента.

Правила набора текста

Чтобы определить набор правильно типизированных лямбда-терминов данного типа, необходимо определить отношение типизации между терминами и типами. Во-первых, мы знакомимся с контекстами ввода или средами ввода. $\Gamma ,\Delta ,\dots$, которые представляют собой наборы предположений о типизации. Предположение о типизации имеет вид $x{\mathbin {:}}\sigma$, что означает переменную $x$ имеет тип $\sigma$.

Отношение типизации $\Gamma \vdash e{\mathbin {:}}\sigma$ указывает на то, что $e$ это термин типа $\sigma$ в контексте $\Gamma$. В этом случае $e$ называется хорошо типизированным (имеющим тип $\sigma$). Экземпляры отношения типизации называются суждениями о типизации . Обоснованность суждения о типизации демонстрируется путем предоставления вывода о типизации , построенного с использованием правил типизации (при этом помещения над линией позволяют нам сделать вывод под линией). Просто типизированное лямбда-исчисление использует следующие правила:

${\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x{\mathbin {:}}\sigma }}$ (1)	${\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c{\mathbin {:}}T}}$ (2)
${\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau }{\Gamma \vdash (\lambda x{\mathbin {:}}\sigma .~e){\mathbin {:}}(\sigma \to \tau )}}$ (3)	${\frac {\Gamma \vdash e_{1}{\mathbin {:}}\sigma \to \tau \quad \Gamma \vdash e_{2}{\mathbin {:}}\sigma }{\Gamma \vdash e_{1}~e_{2}{\mathbin {:}}\tau }}$ (4)

В словах,

1. Если $x$ имеет тип $\sigma$ в контексте, тогда $x$ имеет тип $\sigma$.
2. Термические константы имеют соответствующие базовые типы.
3. Если в определенном контексте $x$ имеющий тип $\sigma$, $e$ имеет тип $\tau$, то в том же контексте без $x$, $\lambda x{\mathbin {:}}\sigma .~e$ имеет тип $\sigma \to \tau$.
4. Если в определенном контексте $e_{1}$ имеет тип $\sigma \to \tau$, и $e_{2}$ имеет тип $\sigma$, затем $e_{1}~e_{2}$ имеет тип $\tau$.

Примерами закрытых терминов, т.е. терминов, вводимых в пустом контексте, являются:

• Для каждого типа $\tau$, термин $\lambda x{\mathbin {:}}\tau .x{\mathbin {:}}\tau \to \tau$ ( функция тождества /И-комбинатор),
• Для типов $\sigma ,\tau$, термин $\lambda x{\mathbin {:}}\sigma .\lambda y{\mathbin {:}}\tau .x{\mathbin {:}}\sigma \to \tau \to \sigma$ (K-комбинатор) и
• Для типов $\tau ,\tau ',\tau ''$, термин $\lambda x{\mathbin {:}}\tau \to \tau '\to \tau ''.\lambda y{\mathbin {:}}\tau \to \tau '.\lambda z{\mathbin {:}}\tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''$ (S-комбинатор).

Это типизированные представления лямбда-исчисления основных комбинаторов комбинаторной логики .

Каждый тип $\tau$ присваивается порядок, номер $o(\tau )$. Для базовых типов $o(T)=0$; для типов функций, $o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))$. То есть порядок типа измеряет глубину самой левой вложенной стрелки. Следовательно:

$o(\iota \to \iota \to \iota )=1$

$o((\iota \to \iota )\to \iota )=2$

Семантика

Внутренние

Вообще говоря, существует два разных способа присвоения значения просто типизированному лямбда-исчислению, как и типизированным языкам в более общем смысле, которые по-разному называются внутренними и внешними, онтологическими и семантическими или в стиле Черча и в стиле Карри. Внутренняя семантика присваивает значение только правильно типизированным терминам или, точнее, присваивает значение непосредственно типизированным выводам. Это приводит к тому, что терминам, различающимся только аннотациями типов, тем не менее, можно придавать разные значения. Например, термин идентичности $\lambda x{\mathbin {:}}{\mathtt {int}}.~x$ о целых числах и тождественном члене $\lambda x{\mathbin {:}}{\mathtt {bool}}.~x$логические значения могут означать разные вещи. (Классические предполагаемые интерпретации являются тождественной функцией для целых чисел и тождественной функцией для логических значений.) Напротив, внешняя семантика придает значение терминам независимо от типизации, поскольку они интерпретировались бы на нетипизированном языке. С этой точки зрения, $\lambda x{\mathbin {:}}{\mathtt {int}}.~x$ и $\lambda x{\mathbin {:}}{\mathtt {bool}}.~x$ означают то же самое ( т. е . то же самое, что и $\lambda x.~x$).

Различие между внутренней и внешней семантикой иногда связано с наличием или отсутствием аннотаций на лямбда-абстракциях, но, строго говоря, такое использование неточно. Можно определить внешнюю семантику аннотированных терминов, просто игнорируя типы ( т. е . посредством стирания типа ), как можно задать внутреннюю семантику неаннотированных терминов, когда типы могут быть выведены из контекста ( т. е . посредством вывода типа). ). Существенная разница между внутренним и внешним подходами заключается в том, рассматриваются ли правила типизации как определение языка или как формализм для проверки свойств более примитивного базового языка. Большинство различных семантических интерпретаций, обсуждаемых ниже, можно рассматривать как с внутренней, так и с внешней точки зрения.

Эквациональная

Просто типизированное лямбда-исчисление (STLC) имеет ту же эквациональную теорию βη-эквивалентности, что и нетипизированное лямбда-исчисление , но с учетом ограничений типа. Уравнение бета-редукции

$(\lambda x{\mathbin {:}}\sigma .~t)\,u=_{\beta }t[x:=u]$

держится в контексте $\Gamma$ в любое время $\Gamma ,x{\mathbin {:}}\sigma \vdash t{\mathbin {:}}\tau$ и $\Gamma \vdash u{\mathbin {:}}\sigma$, а уравнение для эта-редукции

$\lambda x{\mathbin {:}}\sigma .~t\,x=_{\eta }t$

держится всякий раз, когда $\Gamma \vdash t\!:\sigma \to \tau$ и $x$ не кажется бесплатным в $t$. Преимущество типизированного лямбда-исчисления состоит в том, что STLC позволяет сократить потенциально незавершающие вычисления (то есть сократить их ).

Операционная семантика

Аналогично, операционную семантику просто типизированного лямбда-исчисления можно исправить, как и для нетипизированного лямбда-исчисления, используя вызов по имени , вызов по значению или другие стратегии оценки . Как и в любом типизированном языке, безопасность типов является фундаментальным свойством всех этих стратегий оценки. Кроме того, сильной нормализации свойство , описанное ниже, означает, что любая стратегия оценки завершится на всех просто типизированных терминах.

Категориальная семантика

Простое типизированное лямбда-исчисление, обогащенное типами произведений, операторами спаривания и проекции (с $\beta \eta$-эквивалентность) — это внутренний язык декартовых замкнутых категорий (CCC), как впервые заметил Иоахим Ламбек . Для любого CCC основными типами соответствующего лямбда-исчисления являются объекты , а терминами — морфизмы . И наоборот, просто типизированное лямбда-исчисление с типами продуктов и операторами спаривания над набором базовых типов и заданными терминами образует CCC, объектами которого являются типы, а морфизмы - классы эквивалентности терминов.

Существуют правила набора пар , проекции и единичного термина . Учитывая два термина $s{\mathbin {:}}\sigma$ и $t{\mathbin {:}}\tau$, термин $(s,t)$ имеет тип $\sigma \times \tau$. Аналогично, если у кого-то есть термин $u{\mathbin {:}}\tau _{1}\times \tau _{2}$, то есть условия $\pi _{1}(u){\mathbin {:}}\tau _{1}$ и $\pi _{2}(u){\mathbin {:}}\tau _{2}$ где $\pi _{i}$соответствуют проекциям декартова произведения. Единичный термин типа 1, записанный как $()$и произносится как «ноль», является конечным объектом . Эквациональная теория расширяется аналогичным образом, так что имеем

$\pi _{1}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=s{\mathbin {:}}\sigma$

$\pi _{2}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=t{\mathbin {:}}\tau$

$(\pi _{1}(u{\mathbin {:}}\sigma \times \tau ),\pi _{2}(u{\mathbin {:}}\sigma \times \tau ))=u{\mathbin {:}}\sigma \times \tau$

$t{\mathbin {:}}1=()$

Последнее читается как « если t имеет тип 1, то оно сводится к нулю ».

Вышеупомянутое затем можно превратить в категорию, взяв типы в качестве объектов . Морфизмы ​ $\sigma \to \tau$ являются классами эквивалентности пар $(x{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )$ где x — переменная (типа $\sigma$) и t — терм (типа $\tau$), не имеющий в себе свободных переменных, за исключением (необязательно) x . Совокупность терминов в языке есть замыкание этого множества терминов под действием операций абстрагирования и применения .

Это соответствие можно расширить, включив в него «языковые гомоморфизмы» и функторы между категорией декартовых замкнутых категорий и категорией просто типизированных лямбда-теорий.

Часть этого соответствия может быть расширена до замкнутых симметричных моноидальных категорий с помощью системы линейного типа .

доказательная

Просто типизированное лямбда-исчисление тесно связано с импликативным фрагментом пропозициональной интуиционистской логики , т. е. с импликационным исчислением высказываний , через изоморфизм Карри-Говарда : термины точно соответствуют доказательствам в естественной дедукции , а обитаемые типы являются в точности тавтологиями этой логики. .

Из его логистического метода Черч 1940 г. на стр.58 изложена схема аксиом , п. 60, который Хенкин заполнил в 1949 году. чтобы показать домены этого типа (например, натуральные числа, действительные числа и т. д.). Хенкин 1996 с. 146 описал, как логистический метод Чёрча может служить основой математики (арифметика Пеано и реальный анализ), через теорию моделей .

Альтернативные синтаксисы

Приведенное выше представление — не единственный способ определения синтаксиса просто типизированного лямбда-исчисления. Одной из альтернатив является полное удаление аннотаций типов (чтобы синтаксис был идентичен нетипизированному лямбда-исчислению), при этом гарантируя, что термины правильно типизированы с помощью вывода типа Хиндли-Милнера . Алгоритм вывода является завершающим, надежным и полным: всякий раз, когда терм является типизированным, алгоритм вычисляет его тип. термина Точнее, он вычисляет основной тип , поскольку часто неаннотированный термин (например, $\lambda x.~x$) может иметь более одного типа ( ${\mathtt {int}}\to {\mathtt {int}}$, ${\mathtt {bool}}\to {\mathtt {bool}}$и т. д., которые все являются экземплярами основного типа $\alpha \to \alpha$).

Другое альтернативное представление просто типизированного лямбда-исчисления основано на двунаправленной проверке типов , которая требует большего количества аннотаций типов, чем вывод Хиндли-Милнера, но ее легче описать. Система типов разделена на два суждения, представляющие собой как проверку , так и синтез , записанные $\Gamma \vdash e\Leftarrow \tau$ и $\Gamma \vdash e\Rightarrow \tau$соответственно. С функциональной точки зрения три компонента $\Gamma$, $e$, и $\tau$ все это входные данные для проверочного суждения $\Gamma \vdash e\Leftarrow \tau$, тогда как суждение о синтезе $\Gamma \vdash e\Rightarrow \tau$ только занимает $\Gamma$ и $e$ в качестве входных данных, создавая тип $\tau$в качестве вывода. Эти суждения выносятся по следующим правилам:

${\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x\Rightarrow \sigma }}$ [1]	${\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c\Rightarrow T}}$ [2]
${\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e\Leftarrow \tau }{\Gamma \vdash \lambda x.~e\Leftarrow \sigma \to \tau }}$ [3]	${\frac {\Gamma \vdash e_{1}\Rightarrow \sigma \to \tau \quad \Gamma \vdash e_{2}\Leftarrow \sigma }{\Gamma \vdash e_{1}~e_{2}\Rightarrow \tau }}$ [4]
${\frac {\Gamma \vdash e\Rightarrow \tau }{\Gamma \vdash e\Leftarrow \tau }}$ [5]	${\frac {\Gamma \vdash e\Leftarrow \tau }{\Gamma \vdash (e{\mathbin {:}}\tau )\Rightarrow \tau }}$ [6]

Обратите внимание, что правила [1]–[4] почти идентичны правилам (1)–(4) выше , за исключением тщательного выбора проверочных или синтезирующих суждений. Этот выбор можно объяснить так:

1. Если $x{\mathbin {:}}\sigma$ находится в контексте, мы можем синтезировать тип $\sigma$ для $x$.
2. Типы термоконстант фиксированы и могут быть синтезированы.
3. Чтобы проверить это $\lambda x.~e$ имеет тип $\sigma \to \tau$ в некотором контексте мы расширяем контекст с помощью $x{\mathbin {:}}\sigma$ и проверь это $e$ имеет тип $\tau$.
4. Если $e_{1}$ синтезирует тип $\sigma \to \tau$ (в некотором контексте) и $e_{2}$ проверяет тип $\sigma$ (в том же контексте), то $e_{1}~e_{2}$ синтезирует тип $\tau$.

Обратите внимание, что правила синтеза читаются сверху вниз, тогда как правила проверки читаются снизу вверх. Обратите внимание, в частности, что нам не нужны какие-либо аннотации к лямбда-абстракции в правиле [3], поскольку тип связанной переменной можно вывести из типа, по которому мы проверяем функцию. Наконец, мы объясняем правила [5] и [6] следующим образом:

5. Чтобы проверить это $e$ имеет тип $\tau$, достаточно синтезировать тип $\tau$.
6. Если $e$ проверяет тип $\tau$, то явно аннотированный термин $(e{\mathbin {:}}\tau )$ синтезирует $\tau$.

Из-за этих двух последних правил, ограничивающих синтез и проверку, легко увидеть, что любой правильно типизированный, но неаннотированный термин может быть проверен в двунаправленной системе, если мы вставим «достаточное» количество аннотаций типа. А на самом деле аннотации нужны только у β-редексов.

Общие наблюдения

Учитывая стандартную семантику, просто типизированное лямбда-исчисление является строго нормализующим : каждая последовательность сокращений в конечном итоге завершается. Это связано с тем, что рекурсия не разрешена правилами типизации: невозможно найти типы для комбинаторов с фиксированной точкой и термина цикла. $\Omega =(\lambda x.~x~x)(\lambda x.~x~x)$. Рекурсию можно добавить в язык, используя специальный оператор ${\mathtt {fix}}_{\alpha }$типа $(\alpha \to \alpha )\to \alpha$ или добавление общих рекурсивных типов , хотя оба исключают строгую нормализацию.

В отличие от нетипизированного лямбда-исчисления, просто типизированное лямбда-исчисление не является полным по Тьюрингу . Все программы в простом лямбда-исчислении останавливаются. Для нетипизированного лямбда-исчисления существуют программы, которые не останавливаются, и, более того, не существует общей процедуры принятия решения, которая могла бы определить, останавливается ли программа.

Важные результаты

• Тейт показал в 1967 году, что $\beta$-редукция сильно нормализует . Как следствие $\beta \eta$-эквивалентность разрешима . Статман показал в 1979 году, что проблема нормализации не является элементарно-рекурсивной . доказательство, которое позже было упрощено Майрсоном. Известно, что проблема в наборе ${\mathcal {E}}^{4}$ Гжегорчиков иерархии . Чисто семантическое доказательство нормализации (см. нормализацию по оценке ) было дано Бергером и Швихтенбергом в 1991 году.
• объединения для Проблема $\beta \eta$-эквивалентность неразрешима. В 1973 году Юэ показал, что объединение третьего порядка неразрешимо. и это было улучшено Бакстером в 1978 году. затем Гольдфарбом в 1981 году показав, что объединение 2-го порядка уже неразрешимо. Доказательство разрешимости сопоставления более высокого порядка (объединение, при котором только один термин содержит экзистенциальные переменные) было объявлено Колином Стирлингом в 2006 году, а полное доказательство было опубликовано в 2009 году.
• Мы можем кодировать натуральные числа с помощью терминов типа $(o\to o)\to (o\to o)$( Церковные цифры ). Швихтенберг показал в 1975 году, что в $\lambda ^{\to }$ именно расширенные полиномы представимы как функции над цифрами Чёрча; это примерно полиномы, замкнутые под действием условного оператора.
• Полная модель ​ $\lambda ^{\to }$задается путем интерпретации базовых типов как множеств и типов функций с помощью теоретико-множественного функционального пространства . Фридман показал в 1975 году, что эта интерпретация является полной для $\beta \eta$-эквивалентность, если базовые типы интерпретируются бесконечными множествами. Статман показал в 1983 году, что $\beta \eta$-эквивалентность — это максимальная эквивалентность, которая обычно неоднозначна , т.е. замкнута относительно замен типов ( Теорема Статмана о типичной неоднозначности ). Следствием этого является то, что сохраняется свойство конечной модели , т. е. конечных множеств достаточно, чтобы различать термины, которые не идентифицируются $\beta \eta$-эквивалентность.
• Плоткин ввел логические отношения в 1973 году, чтобы охарактеризовать элементы модели, которые можно определить с помощью лямбда-терминов. В 1993 году Юнг и Тюрин показали, что общая форма логического отношения (логические отношения Крипке с переменной арностью) точно характеризует лямбда-определимость. Плоткин и Статман предположили, что можно решить, можно ли определить данный элемент модели, созданной из конечных множеств, с помощью лямбда-члена ( гипотеза Плоткина-Стэтмана ). Лоудер доказал ложность этой гипотезы в 2001 году.

Ссылки

• Х. Барендрегт , Лямбда-исчисления с типами , Справочник по логике в информатике, Том II, Oxford University Press, 1993. ISBN   0-19-853761-1 .

Внешние ссылки

• Погрузчик, Ральф (февраль 1998 г.). «Заметки о просто типизированном лямбда-исчислении» .
• Запись «Теория типов Черча» в Стэнфордской энциклопедии философии.