Оптимальные оценщики на самом деле оптимальны?

10

Следующий термин (используя bruijn-индексы):

BADTERM = λ((0 λλλλ((((3 λλ(((0 3) 4) (1 λλ0))) λλ(((0 4) 3) (1 0))) λ1) λλ1)) λλλ(2 (2 (2 (2 (2 (2 (2 (2 0)))))))))

Применительно к церковному номеру Nбыстро оценивается нормальная форма в нескольких существующих оценщиках, включая наивных . Тем не менее, если вы закодируете этот термин в сети взаимодействия и оцените его с помощью абстрактного алгоритма Лэмпинга, для него потребуется экспоненциальное число бета-сокращений по отношению к N. На Optlam, а именно:

N   interactions(betas)     (BADTERM N)
1   129(72)                 λλλ(1 (2 (2 (2 (2 (2 (2 (2 0))))))))
2   437(205)                λλλ(2 (1 (2 (2 (2 (2 (2 (2 0))))))))
3   976(510)                λλλ(1 (1 (2 (2 (2 (2 (2 (2 0))))))))
4   1836(1080)              λλλ(2 (2 (1 (2 (2 (2 (2 (2 0))))))))
5   3448(2241)              λλλ(1 (2 (1 (2 (2 (2 (2 (2 0))))))))
6   6355(4537)              λλλ(2 (1 (1 (2 (2 (2 (2 (2 0))))))))
7   11888(9181)             λλλ(1 (1 (1 (2 (2 (2 (2 (2 0))))))))
8   22590(18388)            λλλ(2 (2 (2 (1 (2 (2 (2 (2 0))))))))
9   43833(36830)            λλλ(1 (2 (2 (1 (2 (2 (2 (2 0))))))))
10  85799(73666)            λλλ(2 (1 (2 (1 (2 (2 (2 (2 0))))))))
11  169287(147420)          λλλ(1 (1 (2 (1 (2 (2 (2 (2 0))))))))
12  335692(294885)          λλλ(2 (2 (1 (1 (2 (2 (2 (2 0))))))))
13  668091(589821)          λλλ(1 (2 (1 (1 (2 (2 (2 (2 0))))))))
14  1332241(1179619)        λλλ(2 (1 (1 (1 (2 (2 (2 (2 0))))))))
15  2659977(2359329)        λλλ(1 (1 (1 (1 (2 (2 (2 (2 0))))))))

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

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

MaiaVictor
источник

Ответы:

5

Эффективность оптлама

Я не изучал ни детали BADTERM, ни реализацию оценщика optlam, но я нахожу довольно странным, что optlam выполняет ряд β-взаимодействий, существенно отличающихся от другого оптимального оценщика, такого как BOHM. Такое число должно быть по определению в основном одинаковым для данного термина. Вы уверены в правильности ядра optlam?

Эффективность оптимальных оценщиков

Напомним, что понятие оптимальности этих оценщиков более правильно известно как Леви-оптимальность, и оно не является наивным, поскольку стратегия сокращения, выполняющая минимальное число бета-шагов, не вычислима. Таким образом, минимизируется количество параллельных шагов β-редукции, выполненных для целого семейства переопределений, то есть приблизительно набор, полученный симметричным и транзитивным замыканием отношения, которое связывает два переопределения, когда один копируется из другого. В целом не должно удивлять наличие расхождений между числом бета-шагов и остальными шагами дублирования, поскольку мы знаем, что большая часть нормализационной нагрузки может быть перенесена с первого на второе, как показали Асперти, Коппола и Мартини [1].

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

С другой стороны, теоретические результаты об эффективности оптимального сокращения (что является вашим большим вопросом) все еще немногочисленны и еще не являются общими, поскольку они ограничены сетями доказательства типа EAL (что в основном является тем же ограничением оптической оценки). оценщик, если я правильно понимаю), но все они слегка позитивны, так как в худшем случае сложность сокращения общего доступа ограничена обычным постоянным фактором [2,3].

Ссылки

  1. А. Асперти, П. Коппола и С. Мартини, (Оптимально) Дублирование не элементарно рекурсивно , Информация и вычисления, том. 193, 2004.
  2. П. Бейло, П. Коппола и У. Дал Лаго. Легкая логика и оптимальное редукция: полнота и сложность. Информация и вычисления. 209, нет. 2, с. 118–142, 2011.
  3. С. Геррини, Т. Левентис и М. Сольери. Глубоко в оптимальность - сложность и правильность совместного использования реализации ограниченной логики , DICE 2012, Таллин, Эстония, 2012.
Марко Сольери
источник
Such a number must be, by definition, basically the same on a given termтак я и думал. Это удивило меня, поскольку во многих случаях, которые я тестировал, Optlam дает такое же количество бета, что и BOHM. В некоторых случаях это дает меньше, хотя, из-за его стратегии по требованию. Кто-то сказал мне, что сокращение без оракула на самом деле не оптимально, и теперь я больше не знаю. В общем, я глубоко запутался. Но нет, определенно нет никаких доказательств того, что Optlam работает правильно. Я думаю об остальной части вашего комментария - спасибо.
MaiaVictor
Более того, я нашел много разных терминов, которые ведут себя так же, как Бадтерм. Я изучаю проблему дальше, чтобы найти более простые термины, которые ее повторяют.
MaiaVictor
Разновидность параллельной стратегии по требованию является стандартной для оптимальных оценщиков, включая BOHM, поскольку она необходима для самой оптимальности Леви. Оракул не является строго необходимым для оптимального сокращения любых λ-терминов: стратифицированные термины, такие как EAL-типа, не нуждаются в этом.
Марко Сольери
О, тогда плохо. В любом случае, просто чтобы убедиться, что я понимаю это, когда вы учитываете дублирование (а не только бета), могут быть термины, которые асимптотически медленнее сокращать на оптимальных оценщиках, даже в случае типа EAL? В этом случае я бы удивился, почему имеет смысл считать только бета-шаги и есть ли какая-то польза от использования сетей взаимодействия с целью уменьшения λ-исчисления ...
MaiaVictor
1
Ага! Значит, есть не типичные для EAL термины, которые можно уменьшить без оракула? Я предположил, что если Optlam уменьшит его, это будет EAL-typeable (так как у меня нет Inferr типа EAL). Если это не так, то теперь все имеет смысл. Поскольку подмножество термов с типом EAL обладает достаточной мощностью для выражения любого многовременного алгоритма, такого как сортировка, я думаю, что было бы целесообразно специально попытаться разработать термы с типом EAL. Интересно, как это можно сделать на практике? Огромное спасибо.
MaiaVictor