Algoritmos y Estructuras de Datos 1
Expresiones Cuantificadas

Expresiones Cuantificadas

Para seguir con este tema, recomendamos repasar una sección de la anterior materia: Cálculo de Predicados (IAA)

Cuantificación

Es el uso de variables con un alcance delimitado. Estas pueden usarse para consturir expresiones dependientes de las mismas, pero solo en su rango.

Expresión Cuantificada

Es una notación que tiene en cuenta lo siguiente:

  • El operador de la cuantificación.
  • Las variables para crear expresiones.
  • El rango de especificación de variación de las variables.
  • El término (expresión dependiente) de las variables.

Ejemplo:

En base a la función parpar:

par:Num→Boolpar.x≐(x  mod  2=0)par : Num \to Bool \\ par.x \doteq (x\;mod\;2 = 0)

Definimos la siguiente expresión cuantificada:

⟨  ∃i:0≤i≤n:par.i  ⟩\bigl \langle \; \exists i : 0 \leq i \leq n : par.i \; \bigr \rangle ={ Idea intuitiva de ∃  }= \{\textnormal{ Idea intuitiva de } \exists\; \} par.0∨par.1∨...∨par.npar.0 \lor par.1 \lor ... \lor par.n

Analizando la expresión cuantificada por parte tenemos:

  • El cuantificador ∃\exists el cual está ligado al operador ∨\lor
  • La variable ligada ii o “dummy”.
  • El rango 0≤i≤n0 \leq i \leq n (de tipo BoolBool)
  • El término par.ipar.i (de tipo BoolBool)

Evaluar esta expresión nos devuelve un valor BoolBool.

Otro ejemplo puede ser la expresión:

⟨  ∑i:0≤i≤n:2∗i  ⟩\bigl \langle \; \sum i : 0 \leq i \leq n : 2 * i \; \bigr \rangle

Comparándola con su notación matemática:   ∑i=0n2∗i\;\displaystyle{\sum_{i=0}^{n}}2*i
la primera es más clara para programar.

Podemos establecer la siguiente expresión:

⟨⨁i:R:T  ⟩\bigl \langle \bigoplus i : R : T \; \bigr \rangle

Donde ⨁\bigoplus designa un operador asociativo y conmutativo ⊕\oplus (por ejemplo, +,∨,∧,Max,Min+, \lor, \land, Max, Min…)

Cuantificador de Conteo N

El cuantificador de conteo NN se define como:

⟨  N  i:R.i:T.i  ⟩\bigl \langle \; N \; i : R.i : T.i \; \bigr \rangle

Donde NN cuenta la cantidad de veces que el término T.iT.i es TrueTrue dentro del rango R.iR.i

En base a la definición, el cuantificador es igual a:

⟨  N  i:R.i:T.i  ⟩≐⟨  ∑i:R.i∧T.i:1 ⟩\bigl \langle \; N \; i : R.i : T.i \; \bigr \rangle \doteq \bigl \langle \; \sum i : R.i \land T.i : 1 \ \bigr \rangle
Introducción (AyED1)Especificaciones, Verificaciones y Derivaciones