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

Просто типизированное лямбда-исчисление ( $\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 г.). «Заметки о просто типизированном лямбда-исчислении» .
• «Теория типов Черча» Запись в Стэнфордской энциклопедии философии.