Исчисление конструкций: сжать выражение до его наименьшей формы

11

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

Но в некоторых случаях нормализация может уменьшить маленькое выражение до огромного (с точки зрения размера).

Есть ли наименьшая форма выражений? Форма, которая вычисляет то же значение с наименьшим размером.

Другими словами, вместо эффективной по времени нормальной формы, эффективной по пространству.

user47376
источник

Ответы:

8

В том, что мы считаем "той же ценностью", есть немного свободы. Позвольте мне показать, что такого алгоритма не существует, если «одно и то же значение» означает «обсервационно эквивалентный». Я буду использовать фрагмент Исчисления конструкций, а именно Систему Геделя T (просто напечатанный исчисление, натуральные числа и примитивная рекурсия на них), поэтому аргумент уже применяется к гораздо более слабому исчислению.λ

Принимая во внимание число , пусть ¯ п соответствующая цифра , представляющая ее, то есть п применения с у с гр до 0 . Для данного тьюрингова махина M пусть M будет числовым кодированием M некоторым разумным образом.NN¯NsUсс0MMM

Скажем , что две замкнутые условия будут эквивалентны , написаны т U , когда для всех п N , тT,U:NaTNaTTUNN исTN¯ и нормализуют к однойтой же цифры (они нормализуют к цифрепотому что мы находимся в сильно нормализующее claculus).sN¯

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

Существует термин такое , что для всех п N и все машины Тьюринга M , S ( М , ¯ п ) нормализует чтобы ¯ 1 , если Т останавливается в пределах п шагов и нормализует в ¯ 0 в противном случае. Это хорошо известно, поскольку моделирование машины Тьюринга для фиксированного числа шагов n является примитивно рекурсивным.S:NaT×NaTNaTNNMS(M,N¯)1¯TN0¯N

Существует конечное число замкнутых слагаемых которые являются минимальными слагаемыми, эквивалентными λ x : n a t .Z1,...,ZК . Наш алгоритм минимизации возвращает один из них, когда мы даем ему λ x : n a t .λИкс:NaT,0 , и это может даже быть случай, когда λ x : n a t .λИкс:NaT,0 на самом деле единственный такой минимальный термин. Все это не имеет значения, единственное, что имеет значение, - это то, что существует конечное число минимальных членов, эквивалентных λ x : n a t .λИкс:NaT,0 .λИкс:NaT,0

Теперь для любой машины рассмотрим член u : = λ x : n a t .M Если М пробегает навсегдато у ¯ п нормализует к ¯ 0 для каждого п и эквивалентно λ х : п т .

U:знак равноλИкс:NaT,S(M,Икс)
MUN¯0¯N . Чтобы решить, будет ли M работать вечно, мывводим u в наш алгоритм минимизации и проверяем, вернул ли алгоритм один из Z 1 , , Z k . Если это так, то М работает вечно. Если это не так, то он останавливается. (Примечание: алгоритм не должен вычислять Z 1 , , Z k сам по себе, они могут быть жестко запрограммированы в алгоритме.)λИкс:NaT,0MUZ1,...,ZКMZ1,...,ZК

Было бы хорошо узнать аргумент, который работает с более слабым понятием эквивалентности, например, просто сводимость.β

Андрей Бауэр
источник
Как вы рассчитываете Z1, .. Zk?
user47376
Вам не нужно. То есть алгоритм, который я описываю, существует, и мы не знаем точно, что это, но это не имеет значения. На самом деле я не пытаюсь запустить алгоритм, мне просто нужно его существование, чтобы показать, что ваш алгоритм не существует.
Андрей Бауэр
Да, но ваш аргумент говорит, что если мой алгоритм существует, мы можем решить проблему остановки. Чтобы определить, останавливает ли машина Тьюринга M ваш алгоритм, нормализует u и проверяет, является ли он одним из Z1, .. Zk. Поэтому он должен быть в состоянии перечислить их, иначе он может не остановиться.
user47376
являются зашитыми в алгоритме, алгоритм не нужно перечислить их в вычислительном смысле. Если вы предпочитаете, исходный код алгоритма будет начинаться с объявления целого числа k (например, директивы #define в C) и массива Z длины k , а затем код может свободно использовать Z [ i ] , независимо от того, что они являются. Нам не нужно явно их знать, нам просто нужно знать, что они существуют. Z1,...,ZККZКZ[i]
Дамиано
7

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

(λx:T.C x x) uβC u u
u

В этом смысле известно, как оптимальным образом сократить нетипизированные термины, максимально сокращая совместное использование. Это объясняется здесь: /programming//a/41737550/2059388, и соответствующая цитата Дж. Лампинга Алгоритм оптимального сокращения лямбда-исчисления . Нет сомнений, что теорема для нетипизированного исчисления может быть распространена на CIC.

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

Коди
источник
6

Позвольте мне настаивать на точке зрения, затронутой ответом Коди.

Насколько нам известно, вопрос о нахождении наименьшей термы, эквивалентной другой λ- терме, не очень интересен, даже если бы существовал алгоритм, вычисляющий его. Фактически, большинство программ, которые вы пишете в λ- калькуляторе (или в любом исчислении λ- куба), уже находятся в нормальной форме или, по крайней мере, имеют нормальную форму головы, поэтому они уже достигли своего «наименьшего» значения в том смысле, который вы описали. Кроме того, быть «маленьким» не значит быть более эффективным, как обсуждалось в этом вопросе .λλλλ

Mе

MИкс¯L(|Икс|)е(Икс)¯
L(|Икс|)L(N)знак равноО(NК)Ке

λΘ(N)Θ(2N)λλ

λλ

λ

Этот же синтаксис может использоваться для доказательства того, что, в отличие от наивной интуиции, ответ на поставленный выше вопрос - да, действительно: число крайних левых шагов к нормальной форме является разумной мерой стоимости, даже если размер увеличивается, потому что на самом деле существует другой способ представления того же вычисления (с использованием линейных явных подстановок), в котором:

  1. размер не взрывается;
  2. λ

Это все объясняется в статье Аккаттоли и Дала Лаго «Бета-сокращение действительно инвариантно» (LICS 2014, и тогда я думаю, что есть более свежая версия журнала).

λ

Дамиано Мазза
источник
Я имел в виду, например, термин, который разворачивает миллион шагов, чтобы создать список из миллиона элементов. Это нормализуется к фактическому списку, который является наиболее эффективным представлением этого значения (это фактический конечный результат, никаких дальнейших шагов не требуется). Но сам раскрывающийся термин может быть очень маленьким.
user47376
β
Да, это невозможно, как сказал Андрей. Это ответило на мой вопрос.
user47376