В том, что мы считаем "той же ценностью", есть немного свободы. Позвольте мне показать, что такого алгоритма не существует, если «одно и то же значение» означает «обсервационно эквивалентный». Я буду использовать фрагмент Исчисления конструкций, а именно Систему Геделя T (просто напечатанный исчисление, натуральные числа и примитивная рекурсия на них), поэтому аргумент уже применяется к гораздо более слабому исчислению.λ
Принимая во внимание число , пусть ¯ п соответствующая цифра , представляющая ее, то есть п применения с у с гр до 0 . Для данного тьюрингова махина M пусть ⌈ M ⌉ будет числовым кодированием M некоторым разумным образом.NN¯¯¯Nы у с гр0M⌈ М⌉M
Скажем , что две замкнутые условия будут эквивалентны , написаны т ≃ U , когда для всех п ∈ N , тt , u : n a t → n a tт ≃ Un ∈ N исTN¯¯¯ и нормализуют к однойтой же цифры (они нормализуют к цифрепотому что мы находимся в сильно нормализующее claculus).sN¯¯¯
Предположим, у нас был алгоритм, который для любого замкнутого члена типа вычисляет минимальный эквивалентный член. Тогда мы можем решить оракула Halting следующим образом.n a t → n a t
Существует термин такое , что для всех п ∈ N и все машины Тьюринга M ,
S ( ⌈ М ⌉ , ¯ п ) нормализует чтобы ¯ 1 , если Т останавливается в пределах п шагов и нормализует в ¯ 0 в противном случае. Это хорошо известно, поскольку моделирование машины Тьюринга для фиксированного числа шагов n является примитивно рекурсивным.S: n a t × n a t → n a tn ∈ NMS( ⌈ М⌉ , н¯¯¯)1¯¯¯TN0¯¯¯N
Существует конечное число замкнутых слагаемых которые являются минимальными слагаемыми, эквивалентными λ x : n a t .Z1, … , ZК . Наш алгоритм минимизации возвращает один из них, когда мы даем ему λ x : n a t .λ x : n a t .0 , и это может даже быть случай, когда λ x : n a t .λ x : n a t .0 на самом деле единственный такой минимальный термин. Все это не имеет значения, единственное, что имеет значение, - это то, что существует конечное число минимальных членов, эквивалентных λ x : n a t .λ x : n a t .0 .λ x : n a t .0
Теперь для любой машины рассмотрим член
u : = λ x : n a t .M
Если М пробегает навсегдато у ¯ п нормализует к ¯ 0 для каждого п и эквивалентно λ х : п т .
u : = λ x : n a t .S( ⌈ М⌉ , х )
Mты н¯¯¯0¯¯¯N . Чтобы решить, будет ли
M работать вечно, мывводим
u в наш алгоритм минимизации и проверяем, вернул ли алгоритм один из
Z 1 , … , Z k . Если это так, то
М работает вечно. Если это не так, то он останавливается. (Примечание: алгоритм не должен вычислять
Z 1 , … , Z k сам по себе, они могут быть жестко запрограммированы в алгоритме.)
λ x : n a t .0MUZ1, … , ZКMZ1, … , ZК
Было бы хорошо узнать аргумент, который работает с более слабым понятием эквивалентности, например, просто сводимость.β
Как сказал Андрей, проблема неразрешима, если вы разрешите заменять один термин другим, экстенсивно равным. Тем не менее, вы можете быть заинтересованы в оптимальном обмене выражений, в следующем смысле: с учетом сокращения , ясно , что вхождения термина у могут быть совместно в памяти , и каждое сокращение, примененное к одному, может быть применено к другому.
В этом смысле известно, как оптимальным образом сократить нетипизированные термины, максимально сокращая совместное использование. Это объясняется здесь: /programming//a/41737550/2059388, и соответствующая цитата Дж. Лампинга Алгоритм оптимального сокращения лямбда-исчисления . Нет сомнений, что теорема для нетипизированного исчисления может быть распространена на CIC.
Другим важным вопросом является количество информации о типах, которое может быть стерто при выполнении преобразования типов, или, действительно, как выполнить эффективное преобразование, которое является активной областью исследований, см., Например , тезис Мишры-Лингера .
источник
Позвольте мне настаивать на точке зрения, затронутой ответом Коди.
Насколько нам известно, вопрос о нахождении наименьшей термы, эквивалентной другой λ- терме, не очень интересен, даже если бы существовал алгоритм, вычисляющий его. Фактически, большинство программ, которые вы пишете в λ- калькуляторе (или в любом исчислении λ- куба), уже находятся в нормальной форме или, по крайней мере, имеют нормальную форму головы, поэтому они уже достигли своего «наименьшего» значения в том смысле, который вы описали. Кроме того, быть «маленьким» не значит быть более эффективным, как обсуждалось в этом вопросе .λ λ λ λ
Этот же синтаксис может использоваться для доказательства того, что, в отличие от наивной интуиции, ответ на поставленный выше вопрос - да, действительно: число крайних левых шагов к нормальной форме является разумной мерой стоимости, даже если размер увеличивается, потому что на самом деле существует другой способ представления того же вычисления (с использованием линейных явных подстановок), в котором:
Это все объясняется в статье Аккаттоли и Дала Лаго «Бета-сокращение действительно инвариантно» (LICS 2014, и тогда я думаю, что есть более свежая версия журнала).
источник