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

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

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

Синтаксис [ править ]

В этой статье мы используем и для выбора типов. Неформально тип функции относится к типу функций, которые при вводе типа производят вывод типа . По условию единомышленники справа: читаем как .${\ displaystyle \ sigma}$${\ Displaystyle \ тау}$ ${\ displaystyle \ sigma \ to \ tau}$${\ displaystyle \ sigma}$${\ Displaystyle \ тау}$${\ displaystyle \ to}$${\ Displaystyle \ сигма \ к \ тау \ к \ ро}$${\ Displaystyle \ сигма \ к (\ тау \ к \ ро)}$

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

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

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

Мы также фиксируем набор термических констант для базовых типов. Например, мы могли бы принять базовый тип nat , а термины константы могли быть натуральными числами. В первоначальной презентации Черч использовал только два базовых типа: для «типа предложений» и для «типа индивидов». Тип не имеет термических констант, но имеет одну термальную константу. Часто, как правило , рассматривается исчисление только с одним базовым типом .${\displaystyle o}$${\displaystyle \iota }$${\displaystyle o}$${\displaystyle \iota }$${\displaystyle o}$

Синтаксис просто типизированного лямбда-исчисления по сути совпадает с синтаксисом самого лямбда-исчисления. Мы пишем для обозначения того, что переменная имеет тип . Таким образом, синтаксис термина в BNF выглядит следующим образом:${\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 }$

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

${\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x{\mathbin {:}}\sigma }}}$ (1)	${\displaystyle {\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c{\mathbin {:}}T}}}$ (2)
${\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau }{\Gamma \vdash (\lambda x{\mathbin {:}}\sigma .~e){\mathbin {:}}(\sigma \to \tau )}}}$ (3)	${\displaystyle {\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. Если есть тип в контексте, мы знаем, что у него есть тип .${\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 }$
• Для типов терм (K-комбинатор) и${\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] Внутренняя семантика / семантика в стиле Чёрча присваивает значение только хорошо типизированным терминам, или, точнее, придает значение непосредственно типизированным производным. Это приводит к тому, что термины, различающиеся только аннотациями типов, тем не менее могут иметь разные значения. Например, термин идентичности для целых чисел и термин идентичности${\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}$

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

Теория уравнений [ править ]

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

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

выполняется в контексте всякий раз , когда и , в то время как уравнение для сведения eta${\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}$

держится всякий раз и не кажется свободным внутри .${\displaystyle \Gamma \vdash t\!:\sigma \to \tau }$${\displaystyle x}$${\displaystyle t}$

Операционная семантика [ править ]

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

Категориальная семантика [ править ]

Просто напечатал лямбда - исчисление (с -эквивалентностью) является внутренний язык в декартово замкнутых категорий (ООД), как это было впервые обнаружено Ламбека . Для любого конкретного 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, то он сводится к нулю ».

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

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

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

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

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

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

Представленное выше представление - не единственный способ определения синтаксиса просто типизированного лямбда-исчисления. Одна из альтернатив - полностью удалить аннотации типов (так, чтобы синтаксис был идентичен нетипизированному лямбда-исчислению), обеспечивая при этом правильную типизацию терминов с помощью вывода типа Хиндли-Милнера . Алгоритм вывода является завершающим, надежным и завершенным: всякий раз, когда термин является типизированным, алгоритм вычисляет его тип. Точнее, он вычисляет основной тип термина , поскольку часто неаннотированный термин (например, ) может иметь более одного типа ( , и т. Д., Которые все являются экземплярами основного типа ).${\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 }$

${\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x\Rightarrow \sigma }}}$ [1]	${\displaystyle {\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c\Rightarrow T}}}$ [2]
${\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e\Leftarrow \tau }{\Gamma \vdash \lambda x.~e\Leftarrow \sigma \to \tau }}}$ [3]	${\displaystyle {\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]
${\displaystyle {\frac {\Gamma \vdash e\Rightarrow \tau }{\Gamma \vdash e\Leftarrow \tau }}}$ [5]	${\displaystyle {\frac {\Gamma \vdash e\Leftarrow \tau }{\Gamma \vdash (e{\mathbin {:}}\tau )\Rightarrow \tau }}}$ [6]

Обратите внимание, что правила [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 }$

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

Общие наблюдения [ править ]

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

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

Важные результаты [ править ]

• В 1967 году Тейт показал, что восстановление сильно нормализует . Как следствие, -эквивалентность разрешима . Статман показал в 1977 году, что проблема нормализации не является элементарно рекурсивной , доказательство, которое позже было упрощено Майерсоном (1992). Чисто семантическое доказательство нормализации (см. Нормализация по оценке ) было дано Бергером и Швихтенбергом в 1991 году.${\displaystyle \beta }$${\displaystyle \beta \eta }$
• Унификация проблема -эквивалентностью неразрешима. В 1973 году Хуэ показал, что объединение третьего порядка неразрешимо, и это было улучшено Бакстером в 1978 году, а затем Гольдфарбом в 1981 году, показав, что объединение второго порядка уже неразрешимо. Доказательство того, что сопоставление более высокого порядка (объединение, где только один член содержит экзистенциальные переменные) разрешимо, было объявлено Колином Стирлингом в 2006 году, а полное доказательство было опубликовано в 2009 году ^[2].${\displaystyle \beta \eta }$
• Мы можем кодировать натуральные числа терминами типа (числа Чёрча ). Швихтенберг показал в 1976 году, что в точности расширенные многочлены могут быть представлены как функции над числами Чёрча; это примерно полиномы, замкнутые под условным оператором.${\displaystyle (o\to o)\to (o\to o)}$${\displaystyle \lambda ^{\to }}$
• Полная модель из дается путем интерпретации базовых типов , как наборы и типы функций по теоретико-множественной функции пространства . Фридман показал в 1975 году, что эта интерпретация является полной для -эквивалентности, если базовые типы интерпретируются бесконечными множествами. Статман показал в 1983 году, что -эквивалентность - это максимальная эквивалентность, которая обычно неоднозначна , т. Е. Закрыта относительно подстановок типов ( Типичная теорема Статмана о неоднозначности ). Следствием этого является то, что свойство конечной модели выполняется, т. Е. Конечных наборов достаточно, чтобы различать термины, которые не идентифицируются с помощью -эквивалентности.${\displaystyle \lambda ^{\to }}$${\displaystyle \beta \eta }$${\displaystyle \beta \eta }$${\displaystyle \beta \eta }$
• Плоткин ввел логические отношения в 1973 году для характеристики элементов модели, определяемых лямбда-терминами. В 1993 году Юнг и Тюрин показали, что общая форма логического отношения (логические отношения Крипке с разной степенью достоверности) точно характеризует лямбда-определимость. Плоткин и Статман предположили, что разрешимо ли определимость данного элемента модели, порожденной из конечных множеств, с помощью лямбда-члена ( гипотеза Плоткина – Статмана ). В 1993 году Лоадер показал, что это предположение неверно.

Заметки [ править ]

Ссылки [ править ]

• А. Чёрч: формулировка простой теории типов , JSL 5, 1940
• WWTait : Интенсивные интерпретации функционалов конечного типа I, JSL 32 (2), 1967
• Г. Д. Плоткин: Лямбда-определимость и логические отношения, Технический отчет, 1973.
• Г. П. Хуэ: Неразрешимость объединения в логической информации и управлении третьего порядка 22 (3): 257-267 (1973)
• Х. Фридман: Равенство функционалов . LogicColl. '73, страницы 22-37, LNM 453, 1975.
• Х. Швихтенберг: Функции, определяемые в простом типизированном лямбда-исчислении, Arch. Математическая логика 17 (1976) 113-114.
• Р. Статман: Типизированное лямбда-исчисление не является элементарным рекурсивным методом FOCS 1977: 90-94
• WD Goldfarb: Неразрешимость проблемы объединения 2-го порядка, TCS (1981), no. 13, 225–230.
• Р. Статман. -определяемые функционалы и преобразование. Arch. Математика. Логик, 23: 21–26, 1983.${\displaystyle \lambda }$${\displaystyle \beta \eta }$
• Дж. Ламбек : Декартовы замкнутые категории и типизированные лямбда-исчисления . Комбинаторы и языки функционального программирования 1985: 136-175
• У. Бергер, Х. Швихтенберг: обратная функция оценочного функционала для типизированного лямбда-исчисления LICS 1991: 203-211
• Х. Майерсон: простое доказательство теоремы Статмана , TCS 103 (2): 387-394, 1992.
• Юнг, А., Тюрин, Дж .: Новая характеристика определяемости лямбда , TLCA 1993
• Р. Лоадер: Неразрешимость λ-определимости , опубликовано в Church Festschrift, 2001.
• Х. Барендрегт, Лямбда-исчисления с типами , Справочник по логике в компьютерных науках, том II, Oxford University Press, 1993. ISBN 0-19-853761-1 . 
• Л. Бакстер: Неразрешимость проблемы диадического объединения третьего порядка , Информация и управление, 38 (2), 170-178 (1978)

Внешние ссылки [ править ]

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