O seguinte termo-λ, aqui na forma normal:
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))
Implementa um algoritmo de classificação para listas codificadas por igrejas. Ou seja, o resultado de:
sort (λ c n . (c 3 (c 1 (c 2 n)))) β→ (λ c n . (c 1 (c 2 (c 3 n))))
Similarmente,
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))))
Também implementa a classificação para as mesmas listas acima, exceto que você deve fornecer um argumento adicional com um limite para os números que serão considerados:
sort_below 4 [5,1,3,2,4] → [1,2,3]
Estou tentando determinar se esses termos são tipificáveis na lógica afetiva elementar. Como não conheço nenhum verificador de tipos EAL disponível publicamente, isso está se tornando uma tarefa mais difícil do que eu esperava. Existe um tipo para sort
na lógica afetiva elementar?
lo.logic
lambda-calculus
type-systems
MaiaVictor
fonte
fonte
Respostas:
Eu acho que
sort
, como apresentado lá, não pode ser digitado no EAL. Não posso provar isso, mas não funciona no algoritmo abstrato de Lamping sem o oráculo. Além disso, embora o termo seja um pouco inteligente e breve, ele usa estratégias muito malucas que não são compatíveis com a EAL.Mas por trás dessa pergunta, há uma mais interessante: "uma função de classificação nat pode ser implementada no EAL" ? Essa era uma pergunta muito difícil na época, mas agora parece bastante trivial. Sim, claro. Existem muitas maneiras mais simples de fazer isso. Por exemplo, pode-se preencher apenas um codificado em Scott
NatSet
comNat
s codificados pela Igreja e depois convertê-lo em uma lista. Aqui está uma demonstração completa:Aqui está a forma normal indexada por bruijn de uma versão ligeiramente alterada da
sort
acima, que deve receber(x -> (x x))
como o primeiro argumento para funcionar (caso contrário, ela não tem uma forma normal):Muito simples em retrospecto.
fonte