El siguiente término λ, aquí en 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 un algoritmo de clasificación para listas codificadas por la iglesia. Es decir, el resultado de:
sort (λ c n . (c 3 (c 1 (c 2 n)))) β→ (λ c n . (c 1 (c 2 (c 3 n))))
Similar,
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))))
También implementa la clasificación para las mismas listas que anteriormente, excepto que debe proporcionar un argumento adicional con un límite para los números que considerará:
sort_below 4 [5,1,3,2,4] → [1,2,3]
Estoy tratando de determinar si esos términos se pueden escribir en lógica afín elemental. Como no conozco ningún verificador de tipo EAL disponible públicamente, esto está resultando una tarea más difícil de lo que esperaba. ¿Hay un tipo para sort
en lógica afín elemental?
lo.logic
lambda-calculus
type-systems
MaiaVictor
fuente
fuente
Respuestas:
Creo que
sort
, como se presenta allí, no se puede escribir en EAL. No puedo probar eso, pero no funciona en el algoritmo abstracto de Lamping sin el oráculo. Además, aunque el término es algo inteligente y breve, utiliza estrategias muy extrañas que no son compatibles con EAL.Pero detrás de esta pregunta hay una más interesante: "¿se puede implementar una función de clasificación nat en EAL" ? Esa era una pregunta muy difícil en aquel entonces, pero ahora parece bastante trivial. Sí, por supuesto. Hay muchas formas más simples de hacerlo. Por ejemplo, uno puede llenar un s codificado por Scott con s codificado
NatSet
por ChurchNat
, y luego convertirlo en una lista. Aquí hay una demostración completa:Aquí está la forma normal indexada por bruijn de una versión ligeramente alterada de lo
sort
anterior, que debe recibir(x -> (x x))
como primer argumento para funcionar (de lo contrario, no tiene una forma normal):Bastante simple en retrospectiva.
fuente