Следующий λ-член здесь в нормальной форме:
sort = (λabc.(a(λdefg.(f(d(λhij.(j(λkl.(k(λmn.(mhi))l))
(h(λkl.l)i)))(λhi.(i(λjk.(bd(jhk)))(bd(h(λjk.(j
(λlm.m)k))c)))))e))(λde.e)(λde.(d(λfg.g)e))c))
Реализует алгоритм сортировки для церковно-закодированных списков. То есть результат:
sort (λ c n . (c 3 (c 1 (c 2 n)))) β→ (λ c n . (c 1 (c 2 (c 3 n))))
По аналогии,
sort_below = λabcd.a(λef.f(λghi.g(λj.h(λkl.kj(ikl)))(hi))e(λgh.h))
(λe.d)(λe.b(λf.e(f(λghi.hg)(λgh.cfh))))
Также реализует сортировку для тех же списков, что и выше, за исключением того, что вы должны предоставить дополнительный аргумент с пределом для чисел, которые он будет учитывать:
sort_below 4 [5,1,3,2,4] → [1,2,3]
Я пытаюсь определить, поддаются ли эти термины элементарной аффинной логике. Поскольку я не знаю общедоступных средств проверки типов EAL, это оказалось сложнее, чем я ожидал. Есть ли тип для sort
элементарной аффинной логики?
lo.logic
lambda-calculus
type-systems
MaiaVictor
источник
источник
Ответы:
Я думаю
sort
, как представлено там, не может быть напечатано на EAL. Я не могу доказать это, но он не работает на абстрактном алгоритме Лампинга без оракула. Более того, хотя этот термин несколько умный и краткий, он использует очень дурацкие стратегии, которые не подходят для EAL.Но за этим вопросом стоит более интересный: «можно ли реализовать функцию сортировки nat в EAL» ? Тогда это был очень сложный вопрос, но теперь он выглядит довольно тривиально. Ну конечно; естественно. Есть много простых способов сделать это. Например, можно просто заполнить кодировкой Скотта s -кодированными
NatSet
ЦерковьюNat
, а затем преобразовать ее в список. Вот полная демонстрация:Вот индекс bruijn с нормальной формой слегка измененной версии
sort
вышеупомянутого, который должен получить(x -> (x x))
в качестве первого аргумента для работы (в противном случае он не имеет нормальной формы):Довольно просто в ретроспективе.
источник