Buenas,
Este post es para preguntar si alguien conoce algo parecido a esto (dado que ya he buscado en varios lugares y preguntado y nadie me ha sabido responder que haya algo así... pero debería haberlo ¿no?)
La idea es, dado un sistema de tipos deterministico,
i.e. si me das un secuente y una regla de tipado, te doy la conclusión determinísticamente (Para ponerlo más claro, piensen en un sistema de tipos de segundo orden, donde hay un
y la regla
me dice que lo puedo eliminar reemplazando la
por algo, bueno, eso no sería determinístico ya que a la
la puedo reemplazar por diferentes cosas, algo determinístico en cambio sería si la regla
fuese una familia de reglas
(una por cada
posible)), bueno, entonces, dado un sistema de tipos determinístico, lo que quiero es algo parecido a una función que tome una lista de sequentes y devuelva un árbol de prueba completo. O sea, es como si la función tuviera un árbol de pruebas vacío, donde sólo están las reglas a aplicar y los sequentes que hay en los axiomas, y cuando toma la lista de secuentes, los acomoda en los espacios vacíos de las hojas del árbol (o sea, los toma como hipótesis).
¿Se entiende la idea? Definirlo formalmente no es muy difícil, de hecho ya lo tengo hecho, pero quería saber si alguien conocía que ya exista algo así (como para no redefinir lo que ya existe).
Ya he preguntado a varias personas y nadie me supo decir que haya algo así, pero bueno, si a alguien esta "función" le suena parecido a algo que conozcan, avisen.
0 comments:
Publicar un comentario