Следующий термин (используя 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, требуется гораздо меньше бета-шагов, но больше взаимодействий. Если оптимальные оценщики являются оптимальными, как они могут оценивать термины асимптотически медленнее, чем существующие оценщики?
Эта ссылка содержит объяснение о происхождении термина, а также реализацию той же функции, которая ведет себя противоположно, почти странным образом: она должна работать за экспоненциальное время - она работает за экспоненциальное время в большинстве оценщиков - но оптимально оценщики нормализуют его за линейное время!
Such a number must be, by definition, basically the same on a given term
так я и думал. Это удивило меня, поскольку во многих случаях, которые я тестировал, Optlam дает такое же количество бета, что и BOHM. В некоторых случаях это дает меньше, хотя, из-за его стратегии по требованию. Кто-то сказал мне, что сокращение без оракула на самом деле не оптимально, и теперь я больше не знаю. В общем, я глубоко запутался. Но нет, определенно нет никаких доказательств того, что Optlam работает правильно. Я думаю об остальной части вашего комментария - спасибо.