Просто напечатанное лямбда-исчисление
Просто типизированное лямбда-исчисление ( ), форма , теории типов представляет собой типизированную интерпретацию лямбда -исчисления только с одним конструктором типа ( ), который создает типы функций . Это канонический и простейший пример типизированного лямбда-исчисления. Просто типизированное лямбда-исчисление было первоначально введено Алонзо Чёрчем в 1940 году как попытка избежать парадоксального использования нетипизированного лямбда-исчисления . [1]
Термин простой тип также используется для обозначения расширений просто типизированного лямбда -исчисления с такими конструкциями, как произведения , копродукции или натуральные числа ( Система T ) или даже полная рекурсия (например, PCF ). Напротив, системы, в которых вводятся полиморфные типы (например, System F ) или зависимые типы (например, Logical Framework ), не считаются просто типизированными . Простые типы, за исключением полной рекурсии, по-прежнему считаются простыми , поскольку кодирование Чёрча таких структур можно выполнить, используя только и подходящие переменные типа, тогда как полиморфизм и зависимость не могут.
Синтаксис [ править ]
В 1930-х годах Алонзо Чёрч стремился использовать логистический метод : [а] его лямбда-исчисление , как формальный язык, основанный на символических выражениях, состояло из счетно бесконечного ряда аксиом и переменных, [б] но также и конечный набор примитивных символов, [с] обозначающие абстракцию и область действия, а также четыре константы: отрицание, дизъюнкция, количественная оценка всеобщности и выбор соответственно; [д] [и] а также конечный набор правил от I до VI. Этот конечный набор правил включал правило V modus ponens , а также правила IV и VI для замены и обобщения соответственно. [д] Правила I–III известны как альфа-, бета- и эта-преобразования в лямбда-исчислении. Чёрч стремился использовать английский только как язык синтаксиса (то есть метаматематический язык) для описания символических выражений без каких-либо интерпретаций. [ф]
В 1940 году Чёрч остановился на индексной записи для обозначения типа в символическом выражении. [б] В своей презентации Чёрч использовал только два базовых типа: для «типа предложений» и для «типа людей». Тип не имеет термоконстант, тогда как имеет одну константу. Часто исчисление имеет только один базовый тип, обычно , считается. Нижние индексы греческих букв и т. д. обозначают переменные типа; индекс в скобках обозначает тип функции . Черч 1940, стр. 58 использовал «стрелу или ' для обозначения означает или является аббревиатурой для . [г] К 1970-м годам стали использоваться отдельные обозначения стрелок; например, в этой статье символы без индекса и может варьироваться по типам. Тогда считалось, что бесконечное число аксиом является следствием применения к типам правил от I до VI (см. Аксиомы Пеано ). Неформально, тип функции относится к типу функций, которые, учитывая ввод типа , создайте вывод типа .По соглашению, партнеры справа: читается как .
Чтобы определить типы, набор базовых типов , , необходимо сначала определить. Их иногда называют атомарными типами или константами типов . Если это исправлено, синтаксис типов будет следующим:
- .
Например, , генерирует бесконечный набор типов, начиная с , , , , , , , ..., , ...
набор терминальных констант Для базовых типов также фиксирован . Например, можно предположить, что одним из базовых типов является nat , а его терминальные константы могут быть натуральными числами.
Синтаксис просто типизированного лямбда-исчисления по существу аналогичен синтаксису самого лямбда-исчисления. Термин означает, что переменная имеет тип . Синтаксис термина в форме Бэкуса-Наура представляет собой ссылку на переменную , абстракцию , приложение или константу :
где является термином-константой. Ссылка на переменную связан , если он находится внутри привязки абстракции . Терм считается замкнутым , если нет несвязанных переменных.
Для сравнения, синтаксис нетипизированного лямбда-исчисления не имеет такой типизации или терминальных констант:
Тогда как в типизированном лямбда-исчислении каждая абстракция (т.е. функция) должна указывать тип своего аргумента.
Правила набора текста [ править ]
Чтобы определить набор правильно типизированных лямбда-терминов данного типа, необходимо определить отношение типизации между терминами и типами. Во-первых, мы знакомимся с контекстами ввода или средами ввода. , которые представляют собой наборы предположений о типизации. Предположение о типизации имеет вид , что означает переменную имеет тип .
Отношение типизации указывает на то, что это термин типа в контексте . В этом случае называется хорошо типизированным (имеющим тип ). Экземпляры отношения типизации называются суждениями о типизации . Обоснованность суждения о типизации демонстрируется путем предоставления вывода о типизации , построенного с использованием правил типизации (при этом помещения над линией позволяют нам сделать вывод под линией). Просто типизированное лямбда-исчисление использует следующие правила: [час]
(1) | (2) |
(3) | (4) |
Другими словами,
- Если имеет тип в контексте, тогда имеет тип .
- Термические константы имеют соответствующие базовые типы.
- Если в определенном контексте имеющий тип , имеет тип , то в том же контексте без , имеет тип .
- Если в определенном контексте имеет тип , и имеет тип , затем имеет тип .
Примерами закрытых терминов, т.е. терминов, вводимых в пустом контексте, являются:
- Для каждого типа , термин ( функция тождества /И-комбинатор),
- Для типов , термин (K-комбинатор) и
- Для типов , термин (S-комбинатор).
Это типизированные представления основных комбинаторов комбинаторной логики в лямбда-исчислении .
Каждый тип присваивается порядок, номер . Для базовых типов ; для типов функций, . То есть порядок типа измеряет глубину самой левой вложенной стрелки. Следовательно:
Семантика [ править ]
и внешние интерпретации Внутренние
Вообще говоря, существует два разных способа присвоения значения просто типизированному лямбда-исчислению, как и типизированным языкам в более общем смысле, которые по-разному называются внутренними и внешними, онтологическими и семантическими или в стиле Чёрча и в стиле Карри. [1] [7] [8] Внутренняя семантика присваивает значение только правильно типизированным терминам или, точнее, присваивает значение непосредственно типизированным выводам. Это приводит к тому, что терминам, различающимся только аннотациями типа, тем не менее, можно придавать разные значения. Например, термин идентичности о целых числах и тождественном термине логические значения могут означать разные вещи. (Классические предполагаемые интерпретацииявляются тождественной функцией для целых чисел и тождественной функцией для логических значений.)Напротив, внешняя семантика придает значение терминам независимо от типизации, поскольку они интерпретировались бы на нетипизированном языке. С этой точки зрения, и означают то же самое ( т. е. то же самое, что и ).
Различие между внутренней и внешней семантикой иногда связано с наличием или отсутствием аннотаций на лямбда-абстракциях, но, строго говоря, такое использование неточно. Можно определить внешнюю семантику аннотированных терминов, просто игнорируя типы ( т. е . посредством стирания типа ), как можно задать внутреннюю семантику неаннотированных терминов, когда типы можно вывести из контекста ( т. е . посредством вывода типа). ). Существенная разница между внутренним и внешним подходами заключается в том, рассматриваются ли правила типизации как определение языка или как формализм для проверки свойств более примитивного базового языка. Большинство различных семантических интерпретаций, обсуждаемых ниже, можно рассматривать как с внутренней, так и с внешней точки зрения.
теория Эквациональная
Просто типизированное лямбда-исчисление (STLC) имеет ту же эквациональную теорию βη-эквивалентности, что и нетипизированное лямбда-исчисление , но с учетом ограничений типа. Уравнение бета-редукции [я]
держится в контексте в любое время и , а уравнение для эта-редукции [Дж]
держится всякий раз, когда и не кажется бесплатным в .Преимущество типизированного лямбда-исчисления состоит в том, что STLC позволяет сократить потенциально незавершающие вычисления (то есть сократить их ). [9]
Операционная семантика [ править ]
Аналогично, операционную семантику просто типизированного лямбда-исчисления можно исправить, как и для нетипизированного лямбда-исчисления, используя вызов по имени , вызов по значению или другие стратегии оценки . Как и в любом типизированном языке, безопасность типов является фундаментальным свойством всех этих стратегий оценки. Кроме того, сильной нормализации, свойство описанное ниже, подразумевает, что любая стратегия оценки завершится на всех просто типизированных терминах. [10]
Категориальная семантика [ править ]
Простое типизированное лямбда-исчисление, обогащенное типами произведений, операторами спаривания и проекции (с -эквивалентность) — это внутренний язык декартовых замкнутых категорий (CCC), как впервые заметил Иоахим Ламбек . [11] Для любого CCC основными типами соответствующего лямбда-исчисления являются объекты , а терминами — морфизмы . И наоборот, просто типизированное лямбда-исчисление с типами продуктов и операторами спаривания над набором базовых типов и заданными терминами образует CCC, объектами которого являются типы, а морфизмы - классы эквивалентности терминов.
Существуют правила набора пар , проекции и единичного термина . Учитывая два термина и , термин имеет тип . Аналогично, если у кого-то есть термин , то есть условия и где соответствуют проекциям декартова произведения. Единичный термин типа 1, записанный как и произносится как «ноль», является конечным объектом . Эквациональная теория расширяется аналогичным образом, так что имеем
Последнее читается как « если t имеет тип 1, то оно сводится к нулю ».
Вышеупомянутое затем можно превратить в категорию, взяв типы в качестве объектов . Морфизмы являются классами эквивалентности пар где x — переменная (типа ) и t — терм (типа ), не имеющий в себе свободных переменных, за исключением (необязательно) x . Совокупность терминов в языке есть замыкание этого множества терминов под действием операций абстрагирования и применения .
Это соответствие можно расширить, включив в него «языковые гомоморфизмы» и функторы между категорией декартовых замкнутых категорий и категорией просто типизированных лямбда-теорий.
Часть этого соответствия может быть расширена до замкнутых симметричных моноидальных категорий с помощью системы линейного типа .
- доказательная Теоретико семантика
Просто типизированное лямбда-исчисление тесно связано с импликационным фрагментом пропозициональной интуиционистской логики , т. е. с импликационным исчислением высказываний , через изоморфизм Карри-Говарда : термины точно соответствуют доказательствам в естественной дедукции , а обитаемые типы являются в точности тавтологиями этой логики. .
Из его логистического метода Черч 1940 г. [1] на стр.58 изложена схема аксиом , [1] п. 60, который Хенкин заполнил в 1949 году. [3] чтобы показать домены этого типа (например, натуральные числа, действительные числа и т. д.). Хенкин 1996 с. 146 описал, как логистический метод Чёрча может служить основой математики (арифметика Пеано и реальный анализ), [4] через теорию моделей .
Альтернативные синтаксисы [ править ]
Приведенное выше представление — не единственный способ определения синтаксиса просто типизированного лямбда-исчисления. Одной из альтернатив является полное удаление аннотаций типов (чтобы синтаксис был идентичен нетипизированному лямбда-исчислению), гарантируя при этом правильность типизации терминов с помощью вывода типа Хиндли-Милнера . Алгоритм вывода является завершающим, надежным и полным: всякий раз, когда терм является типизированным, алгоритм вычисляет его тип. термина Точнее, он вычисляет основной тип , поскольку часто неаннотированный термин (например, ) может иметь более одного типа ( , и т. д., которые все являются экземплярами основного типа ).
Другое альтернативное представление просто типизированного лямбда-исчисления основано на двунаправленной проверке типов , которая требует большего количества аннотаций типов, чем вывод Хиндли-Милнера, но ее легче описать. Система типов разделена на два суждения, представляющие собой как проверку , так и синтез , записанные и соответственно. С функциональной точки зрения три компонента , , и все это входные данные для проверочного суждения , тогда как суждение о синтезе только занимает и в качестве входных данных, создавая тип в качестве вывода. Эти суждения выносятся по следующим правилам:
[1] | [2] |
[3] | [4] |
[5] | [6] |
Обратите внимание, что правила [1]–[4] почти идентичны правилам (1)–(4) выше , за исключением тщательного выбора проверочных или синтезирующих суждений. Этот выбор можно объяснить так:
- Если находится в контексте, мы можем синтезировать тип для .
- Типы термоконстант фиксированы и могут быть синтезированы.
- Чтобы проверить это имеет тип в некотором контексте мы расширяем контекст с помощью и проверь это имеет тип .
- Если синтезирует тип (в некотором контексте) и проверяет тип (в том же контексте), то синтезирует тип .
Обратите внимание, что правила синтеза читаются сверху вниз, тогда как правила проверки читаются снизу вверх. Обратите внимание, в частности, что нам не нужны какие-либо аннотации к лямбда-абстракции в правиле [3], поскольку тип связанной переменной можно вывести из типа, по которому мы проверяем функцию. Наконец, мы объясняем правила [5] и [6] следующим образом:
- Чтобы проверить это имеет тип , достаточно синтезировать тип .
- Если проверяет тип , то явно аннотированный термин синтезирует .
Из-за этих двух последних правил, ограничивающих синтез и проверку, легко увидеть, что любой правильно типизированный, но неаннотированный термин может быть проверен в двунаправленной системе, если мы вставим «достаточное» количество аннотаций типа. А на самом деле аннотации нужны только у β-редексов.
Общие наблюдения [ править ]
Учитывая стандартную семантику, просто типизированное лямбда-исчисление является строго нормализующим : каждая последовательность сокращений в конечном итоге завершается. [10] Это связано с тем, что рекурсия не разрешена правилами типизации: невозможно найти типы для комбинаторов с фиксированной точкой и термина цикла. . Рекурсию можно добавить в язык, используя специальный оператор типа или добавление общих рекурсивных типов , хотя оба исключают строгую нормализацию.
В отличие от нетипизированного лямбда-исчисления, просто типизированное лямбда-исчисление не является полным по Тьюрингу . Все программы в простом лямбда-исчислении останавливаются. Для нетипизированного лямбда-исчисления существуют программы, которые не останавливаются, и, более того, не существует общей процедуры принятия решения, которая могла бы определить, останавливается ли программа.
Важные результаты [ править ]
- Тейт показал в 1967 году, что -редукция сильно нормализует . [10] Как следствие -эквивалентность разрешима . Статман показал в 1979 году, что проблема нормализации не является элементарно-рекурсивной . [12] доказательство, которое позже было упрощено Майрсоном. [13] Известно, что проблема в наборе иерархии Гжегорчиков . [14] Чисто семантическое доказательство нормализации (см. нормализацию по оценке ) было дано Бергером и Швихтенбергом в 1991 году. [15]
- Проблема объединения для -эквивалентность неразрешима. В 1973 году Юэ показал, что объединение третьего порядка неразрешимо. [16] и это было улучшено Бакстером в 1978 году. [17] затем Гольдфарбом в 1981 году [18] показав, что объединение 2-го порядка уже неразрешимо. Доказательство разрешимости сопоставления более высокого порядка (объединение, при котором только один термин содержит экзистенциальные переменные) было объявлено Колином Стирлингом в 2006 году, а полное доказательство было опубликовано в 2009 году. [19]
- Мы можем кодировать натуральные числа с помощью терминов типа ( Церковные цифры ). Швихтенберг показал в 1975 году, что в именно расширенные полиномы представимы как функции над цифрами Чёрча; [20] это примерно полиномы, замкнутые под действием условного оператора.
- Полная модель задается путем интерпретации базовых типов как множеств и типов функций с помощью теоретико-множественного функционального пространства . Фридман показал в 1975 году, что эта интерпретация является полной для -эквивалентность, если базовые типы интерпретируются бесконечными множествами. [21] Статман показал в 1983 году, что -эквивалентность — это максимальная эквивалентность, которая обычно неоднозначна , т.е. замкнута относительно замен типов ( Теорема Статмана о типичной неоднозначности ). [22] Следствием этого является то, что сохраняется свойство конечной модели , т. е. конечных множеств достаточно, чтобы различать термины, которые не идентифицируются -эквивалентность.
- Плоткин ввел логические отношения в 1973 году, чтобы охарактеризовать элементы модели, которые можно определить с помощью лямбда-терминов. [23] В 1993 году Юнг и Тюрин показали, что общая форма логического отношения (логические отношения Крипке с переменной арностью) точно характеризует лямбда-определимость. [24] Плоткин и Статман предположили, что можно решить, можно ли определить данный элемент модели, созданной из конечных множеств, с помощью лямбда-члена ( гипотеза Плоткина-Стэтмана ). Лоудер доказал ложность этой гипотезы в 2001 году. [25]
Примечания [ править ]
- ^ Алонзо Чёрч (1956) Введение в математическую логику , стр. 47-68 [2]
- ^ Jump up to: Перейти обратно: а б Church 1940, стр. 57 обозначает переменные с индексами для их типа: [1]
- ^ Чёрч 1940, стр.57: перечисленные 2-й и 3-й примитивные символы ( ) обозначают область действия: [1]
- ^ Jump up to: Перейти обратно: а б Церковь 1940, стр.60: — это четыре константы, обозначающие отрицание, дизъюнкцию, количественную оценку универсальности и выбор соответственно. [1]
- ^ Церковь 1940, стр.59 [1] Хенкин 1949 с.160; [3] Хенкин 1996 г. стр.144 [4]
- ^ Церковь 1940, стр.57 [1]
- ^ Чёрч 1940, стр. 58, перечисляет 24 сокращенные формулы. [1]
- ^ представлены 4 печатных суждения В этой статье ниже прописью. это среда набора текста . [5]
- ^ ' ' обозначает процесс замены выражения u вместо x в форме t
- ^ ' ' обозначает процесс создания разложения формы t, примененного к x
- ^ Jump up to: Перейти обратно: а б с д и ж г час я дж Черч, Алонсо (июнь 1940 г.). «Формулировка простой теории типов» (PDF) . Журнал символической логики . 5 (2): 56–68. дои : 10.2307/2266170 . JSTOR 2266170 . S2CID 15889861 . Архивировано из оригинала (PDF) 12 января 2019 года.
- ^ Черч, Алонсо (1956) Введение в математическую логику
- ^ Jump up to: Перейти обратно: а б Леон Хенкин (сентябрь 1949 г.) Полнота функционального исчисления первого порядка стр.160
- ^ Jump up to: Перейти обратно: а б Леон Хенкин (июнь 1996 г.) Открытие моих доказательств полноты
- ^ Гедонистическое обучение: обучение ради удовольствия (последнее обновление: 25 ноября 2021 г., 14:00 UTC). Понимание суждений при наборе текста.
- ^ Пфеннинг, Франк, Черч и Карри: объединение внутренней и внешней типизации (PDF) , стр. 1 , получено 26 февраля 2022 г.
- ^ Карри, Хаскелл Б. (20 сентября 1934 г.). «Функциональность в комбинаторной логике» . Труды Национальной академии наук Соединенных Штатов Америки . 20 (11): 584–90. Бибкод : 1934PNAS...20..584C . дои : 10.1073/pnas.20.11.584 . ISSN 0027-8424 . ПМЦ 1076489 . ПМИД 16577644 . (представляет внешне типизированную комбинаторную логику, позже адаптированную другими для лямбда-исчисления) [6]
- ^ Рейнольдс, Джон (1998). Теории языков программирования . Кембридж, Англия: Издательство Кембриджского университета. стр. 327, 334. ISBN. 9780521594141 .
- ^ Норман Рэмси (весна 2019 г.) Стратегии сокращения лямбда-исчисления
- ^ Jump up to: Перейти обратно: а б с Тейт, WW (август 1967 г.). «Интенсиональные интерпретации функционалов конечного типа I» . Журнал символической логики . 32 (2): 198–212. дои : 10.2307/2271658 . ISSN 0022-4812 . JSTOR 2271658 . S2CID 9569863 .
- ^ Ламбек, Дж. (1986). «Декартовы замкнутые категории и типизированные λ-исчисления» . Комбинаторы и языки функционального программирования . Конспекты лекций по информатике. Том. 242. Спрингер. стр. 136–175. дои : 10.1007/3-540-17184-3_44 . ISBN 978-3-540-47253-7 .
- ^ Статман, Ричард (1 июля 1979 г.). «Типизированное λ-исчисление не является элементарно-рекурсивным» . Теоретическая информатика . 9 (1): 73–81. дои : 10.1016/0304-3975(79)90007-0 . hdl : 2027.42/23535 . ISSN 0304-3975 .
- ^ Майрсон, Гарри Г. (14 сентября 1992 г.). «Простое доказательство теоремы Статмана». Теоретическая информатика . 103 (2): 387–394. дои : 10.1016/0304-3975(92)90020-G . ISSN 0304-3975 .
- ^ Статман, Ричард (июль 1979 г.). «Типизированное λ-исчисление не является элементарно-рекурсивным» . Теоретическая информатика . 9 (1): 73–81. дои : 10.1016/0304-3975(79)90007-0 . hdl : 2027.42/23535 . ISSN 0304-3975 .
- ^ Бергер, У.; Швихтенберг, Х. (июль 1991 г.). «Обратный функционал оценки для типизированного лямбда-исчисления» . [1991] Материалы шестого ежегодного симпозиума IEEE по логике в информатике . стр. 203–211. дои : 10.1109/LICS.1991.151645 . ISBN 0-8186-2230-Х . S2CID 40441974 .
- ^ Юэ, Жерар П. (1 апреля 1973 г.). «Неразрешимость объединения в логике третьего порядка». Информация и контроль . 22 (3): 257–267. дои : 10.1016/S0019-9958(73)90301-X . ISSN 0019-9958 .
- ^ Бакстер, Льюис Д. (1 августа 1978 г.). «Неразрешимость проблемы диадического объединения третьего порядка» . Информация и контроль . 38 (2): 170–178. дои : 10.1016/S0019-9958(78)90172-9 . ISSN 0019-9958 .
- ^ Гольдфарб, Уоррен Д. (1 января 1981 г.). «Неразрешимость проблемы объединения второго порядка». Теоретическая информатика . 13 (2): 225–230. дои : 10.1016/0304-3975(81)90040-2 . ISSN 0304-3975 .
- ^ Стирлинг, Колин (22 июля 2009 г.). «Разрешимость сопоставления высшего порядка». Логические методы в информатике . 5 (3): 1–52. arXiv : 0907.3804 . дои : 10.2168/LMCS-5(3:2)2009 . S2CID 1478837 .
- ^ Швихтенберг, Гельмут (1 сентября 1975 г.). «Определимые функции в λ-исчислении с типами» . Архив математической логики и фундаментальных исследований (на немецком языке). 17 (3): 113–114. дои : 10.1007/BF02276799 . ISSN 1432-0665 . S2CID 11598130 .
- ^ Фридман, Харви (1975). «Равенство между функционалами» . Логический коллоквиум . Конспект лекций по математике. Том. 453. Спрингер. стр. 22–37. дои : 10.1007/BFb0064870 . ISBN 978-3-540-07155-6 .
- ^ Статман, Р. (1 декабря 1983 г.). " -определяемые функционалы и преобразование» . Архив математической логики и фундаментальных исследований . 23 (1): 21–26. doi : 10.1007/BF02023009 . ISSN 1432-0665 . S2CID 33920306 .
- ^ Плоткин, Г.Д. (1973). Лямбда-определимость и логические отношения (PDF) (Технический отчет). Эдинбургский университет . Проверено 30 сентября 2022 г.
- ^ Юнг, Ахим; Тюрин, Ежи (1993). «Новая характеристика определимости лямбды» . Типизированные лямбда-исчисления и приложения . Конспекты лекций по информатике. Том. 664. Спрингер. стр. 245–257. дои : 10.1007/BFb0037110 . ISBN 3-540-56517-5 .
- ^ Погрузчик, Ральф (2001). «Неразрешимость λ-определимости» . Логика, смысл и вычисления . Спрингер Нидерланды. стр. 331–342. дои : 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 г.). «Заметки о просто типизированном лямбда-исчислении» .
- «Теория типов Черча» Запись в Стэнфордской энциклопедии философии.