type-theory – ¿Qué saldrá mal si un tipo de registro recursivo tiene una regla eta negativa?

Pregunta:

En el contexto de Agda como teoría de tipos dependientes:

Este breve artículo https://jesper.sikanda.be/files/vectors-are-records-too.pdf dice que algunos tipos inductivos pueden verse como registros, por ejemplo, el Vector de lista de longitud fija se puede ver como una familia definida inductivamente de tipos no recursivos .

Pero argumentan que, por ejemplo, el tipo de número natural no debería tener una regla eta porque es un tipo recursivo (el artículo original dice que N = Unit \/ N no es terminante).

Entonces, ¿qué saldrá mal si tenemos este tipo?

data out where
  cons : out => out

in : out => out
in (cons a) = a

y darle una regla eta negativa:

(a: out) luego a = cons (in a) juiciosamente

¿Puede probarse False ? ¿O simplemente es una mala idea …?


editar: ¿Parece que Agda tiene una regla eta para registros recursivos? pero no para el definido anteriormente, consulte este número https://github.com/agda/agda/issues/402 . pero el definido anteriormente está descartado creo que por cuestiones de implementación, no teóricas.

Respuesta:

Tener un tipo de registro recursivo con igualdad eta no destruiría la coherencia de la teoría, pero destruiría la decidibilidad de la verificación de tipos.

Por ejemplo, definamos su tipo de out como un tipo de registro en Agda:

record Out : Set where
  inductive
  constructor cons
  field
    in : Out

Agda no usa la igualdad eta para este tipo. Supongamos que lo hizo, entonces typechecker de Agda sería bucle siempre que trata de resolver una ecuación de la forma x = y : Out (donde x y y son dos variables o términos neutros): x = y si y sólo si in x = in y si y sólo si in (in x) = in (in y) sif in (in (in x)) = in (in (in y))

Leave a Comment

Your email address will not be published.

Scroll to Top

istanbul avukat

-

web tasarım