Алгоритм определения равенства функций по простому типу лямбда-исчисления?

Мы знаем, что бета-равенство просто типизированных лямбда-терминов разрешимо. Учитывая M, N: σ → τ, разрешимо ли для всех X: σ, MX NX? $≃_β$

ds.algorithms pl.programming-languages type-theory functional-programming MaiaVictor
источник

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

vzn

@Marzio: На самом деле, я думаю, что проблема здесь в том, как вопрос сформулирован, что довольно неточно. После правильной формулировки это вопрос исследовательского уровня. Лучшая формулировка была бы такова: мы знаем, что бета-равенство просто типизированных лямбда-терминов разрешимо. Учитывая , разрешимо ли для всех , ? В общем, ответ отрицательный (поэтому не существует алгоритма, подобного тому, который искал Viclib). Хотя, возможно, и ожидаемо, это не очевидно априори и является следствием нескольких работ 90-х годов.

M, N : σ \to τ

$M,N:\sigma\rightarrow\tau$

X : σ

$X:\sigma$

M X ≃_{β} N X

$MX\simeq_\beta NX$

Дамиано Мазза

@DamianoMazza: хорошо, действительно, я не голосовал, чтобы закрыть его ... Я удалю свой комментарий, оставлю ваш и дождусь комментария / редактирования ОП.

Марцио де Биаси

@DamianoMazza и Marzio, я не знаю достаточно, чтобы сделать такой официальный вопрос. Хотя я бы хотел, но я не учусь в школе. На самом деле, даже поиск в Google «бета-равенства», который я действительно пробовал, прежде чем задавать вопрос, дает мне так мало результатов, что почти как этот термин вообще не существует. Так что я даже не представляю, где вы узнаете и читаете обо всем этом. Ребята, не могли бы вы указать мне правильное место, чтобы начать самостоятельное изучение темы? Вопрос обновлен.

MaiaVictor

@Viclib: бета-эквивалентность - это техническое понятие, я избегал упоминать его в своем ответе. Грубо говоря, два термина бета-эквивалентны, когда они дают одинаковый результат. Так, говоря, что для всех означает, что и вычисляют одну и ту же функцию. Что касается указателей для изучения (типизированного или нетипизированного) лямбда-исчисления, я думаю, что заметки Питера Селинджера, а также конспекты лекций Сёренсена и Уржичина по Карри-Говарду являются отличными отправными точками .

M X ≃_{β} N X

$MX\simeq_\beta NX$

X

$X$

M

$M$

N

$N$

Дамиано Мазза

Как я уже сказал в своем комментарии, ответ в целом - нет.

Важный момент для понимания (я говорю это для Viclib, который, кажется, узнает об этих вещах), состоит в том, что наличие языка программирования / набора машин, на котором все программы / вычисления не заканчиваются, ни в коем случае не подразумевает равенство функций (т.е. программы / машины вычисляют одну и ту же функцию) разрешима. Простой пример: возьмем набор машин Тьюринга с полиномиальной синхронизацией. По определению все такие машины заканчиваются на всех входах. Теперь для любой машины Тьюринга, какой бы ни была , существует машина Тьюринга которая при вводе строки моделируетшаги вычисления на фиксированном входе (скажем, пустой строке) и принимает, если заканчивается не более $M$ $M_0$ $x$ $|x|$ $M$ $M$ $|x|$ шаги или отклоняет иначе. Если - машина Тьюринга, которая всегда сразу отклоняет, и оба (очевидно) синхронизируются полиномиально, и все же, если бы мы могли решить, ли и и ту же функцию (или, в этом случае, выбрать один и тот же язык), мы могли бы решить, заканчивается ли (который, помните, является произвольной машиной Тьюринга) пустой строкой. $N$ $M_0$ $N$ $M_0$ $N$ $M$

В случае простого типа -calculus (STLC) работает аналогичный аргумент, за исключением того, что измерение выразительной мощности STLC не так тривиально, как в приведенном выше случае. Когда я писал свой комментарий, я имел в виду пару работ Хиллебранда, Канеллакиса и Майерсона начала 90-х годов, которые показывают, что при использовании более сложных типов, чем обычный тип церковных целых чисел, можно кодировать в STLC достаточно сложный вычисления для приведенного выше аргумента для работы. На самом деле, теперь я вижу, что необходимый материал уже находится в упрощенном доказательстве теоремы Статмана: $\lambda$

Гарри Дж. Марсон, Простое доказательство теоремы Статмана. Теоретическая информатика, 103 (2): 387-394, 1992. (Доступно онлайн здесь ).

В этой работе, Mairson показывает, что для любой машины Тьюринга , существует простой тип и -term , кодирующей функции переходов . (Это не очевидно априори, если иметь в виду чрезвычайно слабую выразительную силу STLC на целочисленных значениях Церкви. Действительно, кодирование Mairson не является непосредственным). Из этого нетрудно построить термин $M$ $\sigma$ $\lambda$ $\delta_M:\sigma\rightarrow\sigma$ $M$

$t_M:\mathtt{nat}[\sigma]\rightarrow\mathtt{bool}$

(где - это экземпляр в типа целых чисел Чёрча), такой что сводится к если заканчивается не более чем на шагов, когда передал пустую строку или в противном случае сводится к . Как и выше, если бы мы могли решить, что функция, представленная как является константы , мы бы решили завершение в пустой строке. $\mathtt{nat}[\sigma]$ $\sigma$ $t_M\,\underline{n}$ $\underline{1}$ $M$ $n$ $\underline{0}$ $t_M$ $\underline{0}$ $M$

Дамиано Мазза
источник

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

Коди

Таким образом, STLC не является полным по Тьюрингу, но достаточно мощным для кодирования функции перехода машины Тьюринга !? Таким образом, машину Тьюринга можно определить как ленту плюс работающая на ней программа STLC?

MaiaVictor

@Viclib: Подумайте об этом: моделирование одного шага произвольной машины Тьюринга не требует больших вычислительных мощностей. По сути, вам нужны только конечные типы данных (с if-then-else), списки (с основными операциями: cons, tail и т. Д.) И упорядоченные пары. (Фактически, расширенный тезис Черча-Тьюринга утверждает, что такая низкая сложность характерна для любой разумной модели машины). Чего не хватает в STLC, так это способности запускать переходы TM «ad libitum» независимо от входных данных: он может выполнять их итерацию только несколько раз, равный башне экспонент по входному размеру (см. Статью Mairson).

Дамиано Мазза

@cody: Спасибо, я не знал эту газету. Думаю ты прав.

Дамиано Мазза

Алгоритм определения равенства функций по простому типу лямбда-исчисления?

Ответы: