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

Формальная система в математической логике

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

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

Синтаксис

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

В 1940 году Чёрч остановился на индексной нотации для обозначения типа в символическом выражении. ^[b] В своей презентации Чёрч использовал только два базовых типа: для «типа предложений» и для «типа индивидуумов». Тип не имеет констант-терминов, тогда как имеет одну константу-терминов. Часто рассматривается исчисление только с одним базовым типом, обычно . Греческие буквенные индексы и т. д. обозначают переменные типа; заключенный в скобки нижний индекс обозначает тип функции . Чёрч 1940 с. 58 использовал «стрелку » для обозначения означает , или является сокращением для . ^[g] К 1970-м годам использовалась автономная стрелочная нотация; например, в этой статье символы без индексов и могут охватывать типы. Бесконечное число аксиом тогда рассматривалось как следствие применения правил I–VI к типам (см. аксиомы Пеано ). Неформально, тип функции относится к типу функций, которые, при заданном вводе типа , производят вывод типа . По соглашению, ассоциации справа: читаются как . ${\displaystyle o}$ ${\displaystyle \iota }$ ${\displaystyle o}$ ${\displaystyle \iota }$ ${\displaystyle o}$ ${\displaystyle \alpha ,\beta }$ ${\displaystyle (\alpha \beta )}$ ${\displaystyle \beta \to \alpha }$ ${\displaystyle \to }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$ ${\displaystyle \to }$ ${\displaystyle \sigma \to \tau \to \rho }$ ${\displaystyle \sigma \to (\tau \to \rho )}$

Чтобы определить типы, сначала необходимо определить набор базовых типов , ,. Иногда их называют атомарными типами или константами типов . С этим фиксированным синтаксисом типов будет: ${\displaystyle B}$

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

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

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

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

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

где — константа терма. Ссылка на переменную связана, если она находится внутри связывания абстракции . Терм закрыт , если нет несвязанных переменных. ${\displaystyle c}$ ${\displaystyle x}$ ${\displaystyle x}$

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

${\displaystyle e::=x\mid \lambda x.e\mid e\,e}$

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

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

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

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

На словах,

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

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

• Для каждого типа определен термин ( функция тождества /I-комбинатор), ${\displaystyle \tau }$ ${\displaystyle \lambda x{\mathbin {:}}\tau .x{\mathbin {:}}\tau \to \tau }$
• Для типов , терм (К-комбинатор) и ${\displaystyle \sigma ,\tau }$ ${\displaystyle \lambda x{\mathbin {:}}\sigma .\lambda y{\mathbin {:}}\tau .x{\mathbin {:}}\sigma \to \tau \to \sigma }$
• Для типов — термин (S-комбинатор). ${\displaystyle \tau ,\tau ',\tau ''}$ ${\displaystyle \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 ''}$

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

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

${\displaystyle o(\iota \to \iota \to \iota )=1}$

${\displaystyle o((\iota \to \iota )\to \iota )=2}$

Семантика

Внутренние и внешние интерпретации

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

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

Эквациональная теория

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

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

выполняется в контексте всякий раз , когда и , в то время как уравнение для эта-редукции ^[j] ${\displaystyle \Gamma }$ ${\displaystyle \Gamma ,x{\mathbin {:}}\sigma \vdash t{\mathbin {:}}\tau }$ ${\displaystyle \Gamma \vdash u{\mathbin {:}}\sigma }$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Теоретико-доказательная семантика

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

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

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

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

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

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

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

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

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

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

Общие замечания

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

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

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

• В 1967 году Тейт показал, что -редукция является строго нормализующей . ^[10] Как следствие, -эквивалентность разрешима . В 1979 году Статман показал, что проблема нормализации не является элементарно рекурсивной , ^[12] доказательство, которое позже было упрощено Мэрсоном. ^[13] Известно, что проблема находится в множестве иерархии Гжегорчика . ^[14] Чисто семантическое доказательство нормализации (см. нормализация с помощью оценки ) было дано Бергером и Швихтенбергом в 1991 году. ^[15] ${\displaystyle \beta }$ ${\displaystyle \beta \eta }$ ${\displaystyle {\mathcal {E}}^{4}}$
• Проблема объединения для -эквивалентности неразрешима. Хьюэт показал в 1973 году, что объединение 3-го порядка неразрешимо ^[16] , и это было улучшено Бакстером в 1978 году ^[17], а затем Голдфарбом в 1981 году ^[18], показав, что объединение 2-го порядка уже неразрешимо. Доказательство того, что сопоставление более высокого порядка (объединение, где только один член содержит экзистенциальные переменные) разрешимо, было объявлено Колином Стирлингом в 2006 году, а полное доказательство было опубликовано в 2009 году. ^[19] ${\displaystyle \beta \eta }$
• Мы можем кодировать натуральные числа с помощью терминов типа ( чисел Чёрча ). Швихтенберг показал в 1975 году, что в точности расширенные многочлены представимы как функции над числами Чёрча; ^[20] это примерно многочлены, замкнутые относительно условного оператора. ${\displaystyle (o\to o)\to (o\to o)}$ ${\displaystyle \lambda ^{\to }}$
• Полная модель дается путем интерпретации базовых типов как множеств , а типов функций с помощью теоретико-множественного функционального пространства . Фридман показал в 1975 году, что эта интерпретация является полной для -эквивалентности, если базовые типы интерпретируются бесконечными множествами. ^[21] Статман показал в 1983 году, что -эквивалентность является максимальной эквивалентностью, которая обычно неоднозначна , т. е. замкнута относительно подстановок типов ( Типичная теорема Статмана о неоднозначности ). ^[22] Следствием этого является то, что свойство конечной модели сохраняется, т. е. конечных множеств достаточно для различения терминов, которые не идентифицируются с помощью -эквивалентности. ${\displaystyle \lambda ^{\to }}$ ${\displaystyle \beta \eta }$ ${\displaystyle \beta \eta }$ ${\displaystyle \beta \eta }$
• Плоткин ввел логические отношения в 1973 году для характеристики элементов модели, которые определяются лямбда-термами. ^[23] В 1993 году Юнг и Тьюрин показали, что общая форма логического отношения (логические отношения Крипке с переменной арностью) точно характеризует лямбда-определимость. ^[24] Плоткин и Статман предположили, что разрешимо, определяется ли заданный элемент модели, сгенерированной из конечных множеств, лямбда-термом ( гипотеза Плоткина–Статмана ). Лоадер показал, что эта гипотеза ложна в 2001 году. ^[25]

Примечания

1. Алонзо Чёрч (1956) Введение в математическую логику стр.47-68 ^[2]
2. Church 1940, p.57 обозначает переменные с помощью нижних индексов для их типа: ^[1] ${\displaystyle a_{\alpha },b_{\alpha },...z_{\alpha },...{\bar {a}}_{\alpha },{\bar {b}}_{\alpha },...{\bar {z}}_{\alpha },...}$
3. Чёрч 1940, стр. 57: 2-й и 3-й примитивные символы, перечисленные ( ), обозначают область действия: ^[1] ${\displaystyle \lambda ,(,),N_{oo},A_{ooo},\Pi _{o(o\alpha )},\iota _{\alpha (o\alpha )}}$
4. Church 1940, стр. 60: четыре константы, обозначающие отрицание, дизъюнкцию, всеобщую квантификацию и выбор соответственно. ^[1] ${\displaystyle N_{oo},A_{ooo},\Pi _{o(o\alpha )},\iota _{\alpha (o\alpha )}}$
5. Черч 1940, стр.59 ^[1] Хенкин 1949 стр.160; ^[3] Хенкин, 1996 г., стр. 144 ^[4]
6. Чёрч 1940, стр.57 ^[1]
7. Чёрч 1940 стр. 58 перечисляет 24 сокращённые формулы. ^[1]
8. В этой статье ниже приведены 4 суждения о печати, в словах. — это среда печати . ^​​[5] ${\displaystyle \Gamma }$
9. ' ' обозначает процесс создания замены выражения u на x в форме t ${\displaystyle =_{\beta }}$
10. ' ' обозначает процесс создания расширения формы t, примененной к x ${\displaystyle =_{\eta }}$

1. Church, Alonzo (июнь 1940 г.). «Формулировка простой теории типов» (PDF) . Journal of Symbolic Logic . 5 (2): 56–68. doi :10.2307/2266170. JSTOR  2266170. S2CID  15889861. Архивировано из оригинала (PDF) 12 января 2019 г.
2. Чёрч, Алонзо (1956) Введение в математическую логику
3. Леон Хенкин (сентябрь 1949) Полнота функционального исчисления первого порядка, стр. 160
4. Леон Хенкин (июнь 1996 г.) Открытие моих доказательств полноты
5. Гедонистическое обучение: обучение ради удовольствия (последнее обновление 25 ноября 2021 г. 14:00 UTC) Понимание суждений о типировании
6. Пфеннинг, Фрэнк, Чёрч и Карри: Сочетание внутренней и внешней типизации (PDF) , стр. 1 , получено 26 февраля 2022 г.
7. Карри, Хаскелл Б. (1934-09-20). «Функциональность в комбинаторной логике». Труды Национальной академии наук Соединенных Штатов Америки . 20 (11): 584–90. Bibcode :1934PNAS...20..584C. doi : 10.1073/pnas.20.11.584 . ISSN  0027-8424. PMC 1076489 . PMID  16577644. (представляет внешне типизированную комбинаторную логику, позднее адаптированную другими к лямбда-исчислению) ^[6]
8. Рейнольдс, Джон (1998). Теории языков программирования . Кембридж, Англия: Cambridge University Press. С. 327, 334. ISBN 9780521594141.
9. Норман Рэмси (весна 2019 г.) Стратегии сокращения для лямбда-исчисления
10. Tait, WW (август 1967). «Интенсиональные интерпретации функционалов конечного типа I». The Journal of Symbolic Logic . 32 (2): 198–212. doi :10.2307/2271658. ISSN  0022-4812. JSTOR  2271658. S2CID  9569863.
11. Lambek, J. (1986). "Декартовы замкнутые категории и типизированные λ-исчисления". Комбинаторы и функциональные языки программирования . Конспект лекций по информатике. Том 242. Springer. С. 136–175. doi :10.1007/3-540-17184-3_44. ISBN 978-3-540-47253-7.
12. Статман, Ричард (1 июля 1979 г.). «Типизированное λ-исчисление не является элементарно рекурсивным». Теоретическая информатика . 9 (1): 73–81. doi : 10.1016/0304-3975(79)90007-0 . hdl : 2027.42/23535 . ISSN  0304-3975.
13. Mairson, Harry G. (14 сентября 1992 г.). «Простое доказательство теоремы Статмана». Теоретическая информатика . 103 (2): 387–394. doi :10.1016/0304-3975(92)90020-G. ISSN  0304-3975.
14. Статман, Ричард (июль 1979). «Типизированное λ-исчисление не является элементарно рекурсивным». Теоретическая информатика . 9 (1): 73–81. doi : 10.1016/0304-3975(79)90007-0 . hdl : 2027.42/23535 . ISSN  0304-3975.
15. Бергер, У.; Швихтенберг, Х. (июль 1991 г.). «Обратный функционал оценки для типизированного лямбда-исчисления». [1991] Труды шестого ежегодного симпозиума IEEE по логике в информатике. стр. 203–211. doi :10.1109/LICS.1991.151645. ISBN 0-8186-2230-X. S2CID  40441974.
16. Huet, Gérard P. (1 апреля 1973 г.). «Неразрешимость объединения в логике третьего порядка». Information and Control . 22 (3): 257–267. doi :10.1016/S0019-9958(73)90301-X. ISSN  0019-9958.
17. Бакстер, Льюис Д. (1 августа 1978 г.). «Неразрешимость проблемы диадической унификации третьего порядка». Информация и управление . 38 (2): 170–178. doi : 10.1016/S0019-9958(78)90172-9 . ISSN  0019-9958.
18. Голдфарб, Уоррен Д. (1 января 1981 г.). «Неразрешимость проблемы объединения второго порядка». Теоретическая информатика . 13 (2): 225–230. doi :10.1016/0304-3975(81)90040-2. ISSN  0304-3975.
19. Стирлинг, Колин (22 июля 2009 г.). «Разрешимость сопоставления высшего порядка». Логические методы в информатике . 5 (3): 1–52. arXiv : 0907.3804 . doi :10.2168/LMCS-5(3:2)2009. S2CID  1478837.
20. Швихтенберг, Гельмут (1 сентября 1975 г.). «Definierbare Funktionen imλ-Kalkül mit Typen». Archiv für mathematische Logik und Grundlagenforschung (на немецком языке). 17 (3): 113–114. дои : 10.1007/BF02276799. ISSN  1432-0665. S2CID  11598130.
21. Фридман, Харви (1975). «Равенство между функционалами». Logic Colloquium . Lecture Notes in Mathematics. Vol. 453. Springer. pp. 22–37. doi :10.1007/BFb0064870. ISBN 978-3-540-07155-6.
22. Статман, Р. (1 декабря 1983 г.). « λ {\displaystyle \lambda } -определимые функционалы и преобразование β η {\displaystyle \beta \eta }». Archiv für mathematische Logik und Grundlagenforschung . 23 (1): 21–26. дои : 10.1007/BF02023009. ISSN  1432-0665. S2CID  33920306.
23. Плоткин, ГД (1973). Лямбда-определимость и логические отношения (PDF) (Технический отчет). Эдинбургский университет . Получено 30 сентября 2022 г.
24. Юнг, Ахим; Тюрин, Ежи (1993). "Новая характеристика лямбда-определимости". Типизированные лямбда-исчисления и приложения . Конспект лекций по информатике. Том 664. Springer. С. 245–257. doi :10.1007/BFb0037110. ISBN 3-540-56517-5.
25. Loader, Ralph (2001). «Неразрешимость λ-определимости». Логика, значение и вычисления . Springer Netherlands. стр. 331–342. doi :10.1007/978-94-010-0526-5_15. ISBN 978-94-010-3891-1.

Ссылки

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

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

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