Secuencias (definición)

Varios elementos del mismo tipo $T$, posiblemente repetidos, ubicados en cierto orden.

$\text{seq } T$ es el tipo de las secuencias cuyos elementos son de tipo $T$.

Notación

$$ \langle ... \rangle \in \text{seq } T $$

Secuencias bien formadas

Una secuencia está bien formada si todos los elementos son del mismo tipo.

Recuerdo que indefinido no es un tipo.

Funciones sobre secuencias

• Longitud: $\text{length } (a : \text{seq } \langle T \rangle) : \Z$

• Indexación: $\text{seq } \langle T \rangle [i : \Z] : T$

• Igualdad: $a = b$ si y sólo si

• Head: $\text{head }(a : \text{seq } \langle T \rangle ) : T$

• Cambiar una posición: $\text{setAt } (a : \text{seq } \langle T \rangle, i : \Z, val : T) : \text{seq } \langle T \rangle$

• Tail: $\text{tail }(a : \text{seq } \langle T \rangle ) : \text{seq } \langle T \rangle$

• Agregar cabeza: $\text{addFirst } (t : T, a : \text{seq } \langle T \rangle) : \text{seq } \langle T \rangle$

• Concatenar: $\text{concat } (a : \text{seq } \langle T \rangle, b : \text{seq } \langle T \rangle) : \text{seq } \langle T \rangle$

• Subsecuencia: $\text{subseq } (a : \text{seq } \langle T \rangle, d : \Z, h : \Z) : \text{seq } \langle T \rangle$

Lemas sobre secuencias

Sea $s_0, s_1$ secuencias de tipo $T$ y $e$ un elemento de tipo $T$.

1. |addFirst(e, s0)| = 1 + |s0|
2. |concat(s0, s1)| = |s0| + |s1|
3. s0 = tail(addFirst(e,s0))
4. s0 = subseq(s0, 0, |s0|)
5. s0 = subseq(concat(s0, s1), 0, |s0|)
6. e = head(addFirst(e, s0))
7. e = addFirst(e, s0)[0]
8. addFirst(e, s0)[0] = head(addFirst(e, s0))