Дедуктивное лямбда-исчисление

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

История [ править ]

Алонзо Чёрч изобрел лямбда-исчисление в 1930-х годах, первоначально для того, чтобы обеспечить новую и более простую основу для математики. ^[1]^[2] Однако вскоре после его изобретения основные логические проблемы были выявлены с определением лямбда-абстракции: парадокс Клини – Россера - это реализация парадокса Ричарда в лямбда-исчислении. ^[3] Хаскелл Карри обнаружил, что ключевой шаг в этом парадоксе можно использовать для реализации более простого парадокса Карри . Существование этих парадоксов означало, что лямбда-исчисление не могло быть одновременно последовательным и полным как дедуктивная система . ^[4]

Хаскелл Карри изучал иллюзорную (дедуктивную) комбинаторную логику в 1941 году. ^[5] Комбинаторная логика тесно связана с лямбда-исчислением, и в каждом из них есть одни и те же парадоксы.

Позже лямбда-исчисление было возрождено как определение языка программирования.

Введение [ править ]

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

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

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

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

Для этого обсуждения лямбда-абстракция добавляется в качестве дополнительного оператора в математике. Будут доступны обычные домены, такие как Boolean и real . К этим областям будет применено математическое равенство. Цель состоит в том, чтобы увидеть, какие проблемы возникают из этого определения.

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

Следующая таблица резюмирует;

Имя	Обозначение
Лямбда-абстракция.	${\ displaystyle \ lambda vy}$
Применение функции f к x	${\ displaystyle f \ x}$
Умножение a на b	${\ displaystyle a \ cdot b}$
Пусть x in y	${\ displaystyle \ operatorname {let} x \ operatorname {in} y}$
Математическое равенство	${\ displaystyle m = n}$
Бета сводимое равенство	${\ Displaystyle м \ {\ underset {\ beta} {=}} \ п}$

Интерпретация лямбда-исчисления как математики [ править ]

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

{\ displaystyle \ operatorname {eta-reduct} [X] = X}

{\ displaystyle \ operatorname {beta-reduct} [X] = X}

Эта редукция как математика [ править ]

Эта-редукт определяется как,

x\not \in \operatorname {FV} (f)\to \operatorname {eta-reduct} [\lambda x.(f\ x)]=f

В математической интерпретации

\operatorname {eta-reduct} [X]=X

Тогда принимая f за переменную,

\lambda x.(f\ x)=f

или позволив $f\ x=y$

f\ x=y\iff f=\lambda x.y

Это определение определяет решение для f в уравнении $\lambda x.y$

f\ x=y

Бета-редукция как математика [ править ]

Бета-редукт - это,

\operatorname {beta-reduct} [(\lambda x.b)\ z]=b[x:=z]

и, как,

\operatorname {beta-reduct} [X]=X

тогда,

(\lambda x.b)\ z=b[x:=z]

Это правило вытекает из конкретизации из количественных переменных. Если,

\forall x:f\ x=y

тогда это выражение y с количественной переменной x, представленной как z. $f\ z$

f\ z=y[x:=z]

так,

(\lambda x.y)\ z=y[x:=z]

Поскольку бета-редукция подразумевается из эта-редукции, между двумя определениями нет противоречия.

Несоответствие Принципу Бивалентности [ править ]

Пусть z - логическое значение ; тогда мы можем составить уравнение без решений,

z=\neg z

Чтобы решить это уравнение рекурсией, мы вводим новую функцию $f,$ определяемую формулой

f\ n=\neg (n\ n)

где $n$ - вспомогательная переменная для хранения значения рекурсии. (Мы предполагаем, что он все еще возвращает логическое значение, даже если ему задан не-логический аргумент.) Посредством эта-редукции мы получаем, $\neg$

f=\lambda x.\neg (x\ x)

А потом,

{\begin{aligned}f\ f&=(\lambda x.\neg (x\ x))(\lambda x.\neg (x\ x))\\&=\neg ((\lambda x.\neg (x\ x))(\lambda x.\neg (x\ x)))\\&=\neg (f\ f)\end{aligned}}

Тогда $ff не$ является ни истинным, ни ложным, и поскольку $ff$ является логическим значением (для любого $x$ , $f$ возвращает логическое значение ), мы видим, что $ff не$ является ни истинным, ни ложным; это также демонстрирует, что отрицание имеет меньший смысл в применении к нелогическим значениям. $\neg (x\ x)$

Интенсиональное и экстенсиональное равенство [ править ]

Еще одна трудность для интерпретации лямбда-исчисления как дедуктивной системы - это представление значений в виде лямбда-членов, которые представляют функции. Нетипизированное лямбда-исчисление реализуется путем редукции лямбда-члена до тех пор, пока терм не будет в нормальной форме. Интенсиональная интерпретация ^[6]^[7] равенство является то , что сокращение срока лямбды к нормальной форме является значением термина лямбды.

Эта интерпретация рассматривает лямбда-выражение как его структуру. Два лямбда-члена равны, если они альфа-конвертируемы.

Экстенсиональное определение функции равенства является то , что две функции равны , если они выполняют то же отображение;

f=g\iff (\forall xf\ x=g\ x)

Один из способов описать это состоит в том, что экстенсиональное равенство описывает равенство функций, тогда как интенсиональное равенство описывает равенство реализаций функций.

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

Пример [ править ]

В арифметике это подразумевает закон распределения . Используя кодировку цифр Чёрча, левая и правая части могут быть представлены в виде лямбда-членов. $2*(r+s)=2*r+2*s$

Итак, закон распределения гласит, что две функции,

\lambda r.\lambda s.2*(r+s)=\lambda r.\lambda s.2*r+2*s

равны, как функции на числах Чёрча. (Здесь мы сталкиваемся с технической слабостью нетипизированного лямбда-исчисления: нет способа ограничить область определения функции числами Чёрча. В следующем аргументе мы проигнорируем эту трудность, притворившись, что «все» лямбда-выражения являются числами Чёрча. .) Закон о распределении должен применяться, если числа Чёрча обеспечивают удовлетворительную реализацию чисел.

{\begin{aligned}\lambda r.\lambda s.\operatorname {mult} \ 2\ (\operatorname {plus} \ r\ s)&=\lambda r.\lambda s.\operatorname {plus} \ (\operatorname {mult} \ 2\ r)\ (\operatorname {mult} \ 2\ s)\\{\scriptstyle \lambda r.\lambda s.(\lambda m.\lambda n.\lambda f.m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ ((\lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x))\ r\ s)}&={\scriptstyle \lambda r.\lambda s.(\lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x))\ ((\lambda m.\lambda n.\lambda f.m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ r)\ ((\lambda m.\lambda n.\lambda f.m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ s)}\\\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (s\ f\ (r\ f\ (s\ f\ x)))&=\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (r\ f\ (s\ f\ (s\ f\ x)))\end{aligned}}

Два термина бета сводятся к похожим выражениям. Тем не менее, они не являются альфа-конвертируемыми и даже не конвертируемыми в эту (последнее следует, потому что оба термина уже имеют длинную форму эта). Итак, согласно интенсиональному определению равенства, выражения не равны. Но если две функции применяются к одним и тем же числам Чёрча, они дают одинаковый результат в соответствии с законом распределения; таким образом, они экстенсивно равны.

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

Если для всех лямбда-выражений $t$ мы имеем , то . $f\ t\ {\underset {\beta }{=}}\ g\ t$ $f\ {\underset {\beta }{=}}\ g$

В нашей ситуации «все лямбда-выражения» означают «все числительные Чёрча», так что это также омега-правило в стандартном смысле. Обратите внимание, что правило омега подразумевает правило эта, поскольку с помощью бета-редукции с правой стороны. $f\ t\ {\underset {\beta }{=}}\ (\lambda x.f\ x)\ t$

Теоретическая область множеств [ править ]

Лямбда-абстракции - это функции функций. Естественным шагом является определение домена для лямбда-абстракции как набора всех функций.

Набор всех функций из области D в диапазон R задается K в,

f\in K\iff (\forall x:x\in D\implies f\ x\in R)

Тогда (мнимое) определение множества всех функций функций дается F в,

f\in F\iff (\forall x:x\in F\implies f\ x\in F)

Это определение нельзя сформулировать в аксиоматической теории множеств; и это наивное уравнение, даже если его можно записать в рамках теории множеств, не имеет решений.

Теперь лямбда-исчисление определяется бета-редукцией и эта-редукцией. Интерпретация сокращения как определения равенства дает неявную область лямбда-исчисления. Правила таковы,

Каждая лямбда-абстракция имеет одно значение.
Бета-сокращение лямбда-члена имеет такое же значение.
Такое же значение имеет сокращение эта лямбда-члена.
Альфа-конвертируемые лямбда-члены равны.
[Если присутствует омега-правило] «омега-эквивалентные» лямбда-члены равны.
Если два лямбда-члена не могут быть показаны как равные по приведенным выше правилам, они не равны.

Если два лямбда-члена могут быть приведены к нормальной форме, то можно использовать теорему Черча – Россера, чтобы показать, что они равны, если их нормальные формы альфа-конвертируемы.

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

Пример: нет решений → одно решение [ править ]

Например, уравнение можно закодировать с помощью кодирования Черча и использования комбинатора Y Карри как, $x=\neg x$

\operatorname {not} _{1}=\lambda p.\lambda a.\lambda b.p\ b\ a

(\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)))(\lambda p.\lambda a.\lambda b.p\ b\ a)

И рекурсия,

(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))

(\lambda p.\lambda a.\lambda b.p\ b\ a)\ ((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))

\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a

...

\lambda a.\lambda b.(\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a)\ b\ a

... (бета, а затем уменьшение эта)

(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))

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

Пример: несколько решений → одно решение [ править ]

Используя числа с делением и числа со знаком, комбинатор Y может использоваться для определения выражения, представляющего квадратный корень целого числа. Кодирование Чёрча также может быть расширено до рациональных и действительных чисел, так что можно определить действительный квадратный корень. Тезис Черча-Тьюринга означает , что любая вычислимая оператор (и его операнды) можно представить в лямбда - исчислении.

Используя такую кодировку,

x^{2}=n\Rightarrow x={\frac {n}{x}}\Rightarrow f\ x={\frac {n}{x}}\land Y\ f=x

Тогда, используя реализацию div ,

Y(\operatorname {divide} n)

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

См. Также [ править ]

Лямбда-исчисление
Пусть выражение
Церковная кодировка

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

Перейти ↑ Church, A. (1932). «Набор постулатов в основу логики». Анналы математики . Series 2. 33 (2): 346–366. DOI : 10.2307 / 1968337 . JSTOR 1968337 .
^ Для полной истории см. Кардоне и Хиндли « История лямбда-исчисления и комбинаторной логики » (2006).
Перейти ↑ Kleene, SC & Rosser, JB (1935). «Несостоятельность некоторых формальных логик». Анналы математики . 36 (3): 630–636. DOI : 10.2307 / 1968646 . JSTOR 1968646 .
^ Карри, Хаскелл Б. (1942). «Несогласованность определенной формальной логики». Журнал символической логики . 7 (3): 115–117. DOI : 10.2307 / 2269292 . JSTOR 2269292 .
^ Карри, Хаскелл Б. (1941). «Парадокс Клини и Россера» . Труды Американского математического общества . 50 : 454–516. DOI : 10.1090 / S0002-9947-1941-0005275-6 . JSTOR 1990124 . Руководство по ремонту 0005275 . Проверено 24 января 2013 года .
^ Селинджер, Питер. «Конспект лекций по лямбда-исчислению (PDF)» (PDF) . п. 6.
^ «Лямбда-исчисление - интенсиональность» . Стэнфорд. п. 1.2 Интенциональность.

[1] Перейти ↑ Church, A. (1932). «Набор постулатов в основу логики». Анналы математики . Series 2. 33 (2): 346–366. DOI : 10.2307 / 1968337 . JSTOR 1968337 .

[2] Для полной истории см. Кардоне и Хиндли « История лямбда-исчисления и комбинаторной логики » (2006).

[3] Перейти ↑ Kleene, SC & Rosser, JB (1935). «Несостоятельность некоторых формальных логик». Анналы математики . 36 (3): 630–636. DOI : 10.2307 / 1968646 . JSTOR 1968646 .

[4] Карри, Хаскелл Б. (1942). «Несогласованность определенной формальной логики». Журнал символической логики . 7 (3): 115–117. DOI : 10.2307 / 2269292 . JSTOR 2269292 .

[5] Карри, Хаскелл Б. (1941). «Парадокс Клини и Россера» . Труды Американского математического общества . 50 : 454–516. DOI : 10.1090 / S0002-9947-1941-0005275-6 . JSTOR 1990124 . Руководство по ремонту 0005275 . Проверено 24 января 2013 года .

[6] Селинджер, Питер. «Конспект лекций по лямбда-исчислению (PDF)» (PDF) . п. 6.

[7] «Лямбда-исчисление - интенсиональность» . Стэнфорд. п. 1.2 Интенциональность.

[1]