coq - qué - indicadores e indices metodologia
¿Diferencia entre los parámetros de tipo y los índices? (2)
Soy nuevo en los tipos dependientes y estoy confundido acerca de la diferencia entre los dos. Parece que la gente suele decir que un tipo está parametrizado por otro tipo e indexado por algún valor . ¿Pero no hay distinción entre tipos y términos en un lenguaje tipificado de manera dependiente? ¿Es fundamental la distinción entre parámetros e índices? ¿Me puede mostrar ejemplos que muestren diferencias en sus significados tanto en la programación como en la prueba de teoremas?
Aquí hay un ejemplo de un tipo paramerizado por algún valor:
open import Data.Nat
infixr 4 _∷_
data ≤List (n : ℕ) : Set where
[] : ≤List n
_∷_ : {m : ℕ} -> m ≤ n -> ≤List n -> ≤List n
1≤3 : 1 ≤ 3
1≤3 = s≤s z≤n
3≤3 : 3 ≤ 3
3≤3 = s≤s (s≤s (s≤s z≤n))
example : ≤List 3
example = 3≤3 ∷ 1≤3 ∷ []
Es un tipo de listas con cada elemento menor o igual n . La intuición general es: si alguna propiedad se mantiene para cada habitante de un tipo, entonces puede abstraerla en un parámetro. También hay una regla mecánica: "El primer índice se puede convertir en un nuevo parámetro si cada constructor tiene la misma variable en la primera posición del índice (en el tipo de resultado)". Esta cita es de *, deberías leerla.
Cuando vea una familia de tipos, puede preguntarse si cada uno de los argumentos que tiene son parámetros o índices .
Los parámetros son meramente indicativos de que el tipo es un tanto genérico y se comporta de forma paramétrica con respecto al argumento proporcionado.
Lo que esto significa, por ejemplo, es que el tipo List T tendrá las mismas formas independientemente de la T que considere: nil , cons t0 nil , cons t1 (cons t2 nil) , etc. La elección de T solo afecta a qué valores pueden ser enchufado para t0 , t1 , t2 .
Por otro lado, los índices pueden afectar a qué habitantes puede encontrar en el tipo. Es por eso que decimos que indexan una familia de tipos, es decir, cada índice le dice a cuál de los tipos (dentro de la familia de tipos) está viendo (en ese sentido, un parámetro es un caso degenerado donde todos los índices apuntan al mismo conjunto de "formas").
Por ejemplo, la familia de tipos Fin n o conjuntos finitos de tamaño n contienen estructuras muy diferentes dependiendo de su elección de n .
El índice 0 indiza un conjunto vacío. El índice 1 indiza un conjunto con un elemento.
¡En ese sentido, el conocimiento del valor del índice puede llevar información importante! Por lo general, puede saber qué constructores pueden o no haber sido utilizados al observar un índice. Así es como la combinación de patrones en lenguajes dependientes puede eliminar patrones no factibles y extraer información de la activación de un patrón.
Esta es la razón por la que, cuando define familias inductivas, generalmente puede definir los parámetros para todo el tipo, pero debe especificar los índices para cada constructor (ya que se le permite especificar, para cada constructor, en qué índices vive).
Por ejemplo puedo definir:
F (T : Type) : ℕ → Type
C1 : F T 0
C2 : F T 1
C3 : F T 0
Aquí, T es un parámetro, mientras que 0 y 1 son índices. Cuando reciba alguna x del tipo FT n , mirar qué T es no revelará nada acerca de x . Pero mirando a n te dirá:
- que
xdebe serC1oC3cuandones0 - que
xdebe serC2cuandones1 - ese
xdebe haber sido forjado a partir de una contradicción de lo contrario
De manera similar, si recibe una y de tipo FT 0 , sabe que solo necesita una coincidencia de patrón contra C1 y C3 .