Ver el código de «Práctica 3: Cuantificadores (Algoritmos I)»

===Ejercicio 1===
'''Determinar cuales de las variables que aparecen en las siguientes expresiones aparecen libres y cuales ligadas.'''

# (<math>\forall x \in [0..n)) x+y==z </math>
# (<math>\forall x \in [0..n), y \in [0..m)) x+y==z </math>
# (<math>\forall j \in [0..|s|)) s_j == 0 </math>
# (<math>\forall j \in [0..|s|)) s_j == x </math>
# (<math>\exists x \in r, x\ mod\ 2 == 0)(\forall j \in [0..|s|)) s_j == x </math>
# <math> ( |s|>5 \land a < b-1 \land (\forall j \in [a..b)) 2 * s_j == s_{j+1})</math>


'''Respuestas:'''
Recordemos que las variables ligadas son aquellas que son variables de selector y están al alcance del mismo.

# x.
# x e y.
# j
# j
# x y j
# j

===Ejercicio 2===
'''Escriba los siguientes predicados en lenguaje de especificación:'''

a) aux suc<math>(x: \mathbb{Z}): \mathbb{Z}</math>, que corresponde al sucesor de x.

b) aux suma<math>(x,y: \mathbb{R}): \mathbb{R}</math>, que corresponda a la suma entre x e y.

c) aux producto<math>(x, y: \mathbb{R}): \mathbb{R}</math>, que corresponde al producto entre x e y.

d) aux cuadrado<math>(x: \mathbb{Z})</math>: Bool, que sea verdadero sii x es un número cuadrado.

e) aux primo<math>(x: \mathbb{Z})</math>: Bool, que sea verdadero sii x es primo.

f) aux coprimos<math>(x,y: \mathbb{Z})</math>: Bool, que sea verdadero sii x e y son coprimos.

g) aux divisoresGrandes<math>(x, y : \mathbb{Z})</math>: Bool, que sea verdadero sii todos los divisores de x, sin contar el uno, son mayores que y.

h) aux mayorPrimo<math>(x: \mathbb{Z}): \mathbb{Z}</math>, que represente el mayor primo que divide a x.

i) aux mcm<math>(x,y: \mathbb{Z}): \mathbb{Z}</math>, que represente el mínimo común múltiplo entre x e y.

j) aux mcd<math>(x,y: \mathbb{Z}): \mathbb{Z}</math>, que represente el máximo común divisor entre x e y.


'''Respuestas:'''

a) aux suc <math>(x: \mathbb{Z}): \mathbb{Z}</math> = x + 1;

b) aux suma <math>(x,y: \mathbb{R}): \mathbb{R}</math> = x + y;

c) aux producto<math>(x, y: \mathbb{R}): \mathbb{R}</math> = x * y;

d) aux cuadrado<math>(x: \mathbb{Z})</math>: Bool = (x <math>\geq</math> 0 <math>\wedge</math>(<math>\exists</math> y <math>\leftarrow</math> [0..x]) y*y == x);

e)aux primo<math>(x: \mathbb{Z})</math>: Bool = |[ y | y <math>\leftarrow</math>[1..|x|], x mod y == 0]| == 2 (Recordemos que un número es primo si tiene exactamente dos divisores positivos: el 1 y su valor absoluto) 

f) aux coprimos<math>(x,y: \mathbb{Z})</math>: Bool == |[ z | z <math>\leftarrow</math> [1..x], x mod z==0, y mod z == 0]| == 1 (Dos números son coprimos si tienen un único divisor positivo en común: el uno)

g) aux divisoresGrandes<math>(x,y : \mathbb{Z})</math>: Bool = (<math>\forall</math> z <math>\leftarrow</math> [ t | t <math>\leftarrow</math> [2..|x|], x mod t == 0]) z > y

h) aux mayorPrimo<math>(x: \mathbb{Z}): \mathbb{Z}</math> = 
<math>[y | y \leftarrow [0..|x|], primo(y), x \ mod \ y == 0 ]_{|[ y | y \leftarrow [0..|x|], \ primo(y), x \ mod \ y == 0]|-1}</math>
otras formas: 
-utilizar un aux ultimo que sea algo asi como cabeza(invertir(l:[T]))

i) aux mcm<math>(x,y: \mathbb{Z}): \mathbb{Z}</math> = cab([ z | z <math>\leftarrow</math> [0..|x*y|], z \ mod \ x == 0, z \ mod \ y == 0])

j) aux mcd<math>(x,y: \mathbb{Z}): \mathbb{Z}</math> = <math>[ z | z \leftarrow [0..|x|], x \ mod \ z == 0, y \ mod \ z == 0 ]_{[ z | z \leftarrow [0..|x|], x \ mod \ z == 0, y \ mod \ z == 0 ] - 1}</math>

===Ejercicio 3===
'''Escriba las siguientes funciones auxiliares sobre secuencias de enteros, aclarando los tipos de los parámetros que recibe y devuelve:'''

1. ''capicua'', que determina si una secuencia es capicúa. (Por ejemplo, [0,2,1,2,0] es capicúa y [0,2,1,4,0] no).

''capicua''(x: [T]): Bool = (<math>\forall</math>i <math> \leftarrow</math> [0..|x|) ) <math>x_i==x_{|x|-i-1}</math>


2. ''esPrefijo'', que determina si una secuencia es prefijo de otra.

''esPrefijo''(x,y: [T]): Bool = (<math>\exists</math> i <math>\leftarrow</math> [0..|y|-1]) x==[<math>y_i</math>| j <math>\leftarrow</math> [0..i] ]

otra forma:
(|b| > |a| <math>\wedge</math> (<math>\forall i \leftarrow</math> [0..|a|) ) <math>a_i==b_i</math>);


3. ''estaOrdenada'', que determina si la secuencia está ordenada de menor a mayor.

''estaOrdenada''(x: [Int]): Bool = (<math>\forall</math> i,j <math>\leftarrow</math> [0..|x|-1], i<j) <math>x_i < x_j</math>


4. ''todosPrimos'', que determina si todos los elementos de la secuencia son números primos.

''todosPrimos''(x: [<math>\mathbb{Z}</math>]): Bool = (<math>\forall</math> t <math>\leftarrow</math> x) primo(t)


(primos la definimos en el ejercicio 2.5)


5. ''todosIguales'', que determina si todos los elementos de la secuencia son iguales.

''todosIguales''(x: [T]): Bool = (<math>\forall</math> a, b <math>\leftarrow</math> x) a==b


6. ''hayUnoParQueDivideAlResto'', que determina si hay un elemento par en la secuencia que divide al resto.


''hayUnoParQueDivideAlResto''(x: [<math>\mathbb{Z}</math>]): Bool = (<math>\exists</math> a <math>\leftarrow</math> x, a mod 2 == 0) (<math>\forall</math> b <math>\leftarrow</math> x) b mod a == 0



7. ''hayUnoEnPosicionParQueDivideAlResto'', que determina si hay un elemento en una posición par de la secuencia que divide al resto.

''hayUnoEnPosicionParQueDivideAlResto''(x: [<math>\mathbb{Z}</math>]): Bool =<br>
(<math>\exists</math> i <math>\leftarrow</math> [0..|x|-1], i mod 2 == 0)(<math>\forall</math> a <math>\leftarrow</math> x) <math> a mod x_i == 0</math>


8. ''sinRepetidos'', que determina si la secuencia no tiene repetidos.

''sinRepetidos''(x: [T]): Bool = (<math>\forall</math> i,j <math>\leftarrow</math> [0..|x|-1], i <math>\neq</math>j) <math>x_i \neq x_j </math>
otra forma: 
(<math>\forall</math> i <math>\leftarrow</math> [0..|x|-1]), <math>x_i \not\in x_{[0..i)}) </math>
otra más:
(<math>\forall</math> e <math>\leftarrow</math> x, cuenta(e, x) == 1)


9. ''sinMasDeNApariciones'', que determina si en la secuencia, ningún elemento aparece más de n veces.

''sinMasDeNApariciones''(x: [T]): Bool = (<math>\forall</math> a <math>\leftarrow</math> x) | [ b | b <math>\leftarrow</math> x, b==a ] | <math>\leq</math> n


10. otroMayorADerecha, que determina si todo elemento de la secuencia, salvo el último, tiene otro mayor a su derecha.

''otroMayorADerecha''(x: [<math>\mathbb{Z}</math>]): Bool = (<math>\forall</math> i <math>\leftarrow</math> [0..|x|-2]) <math> x_i < x_{i+1} </math>


11. ''todoEsMultiplo'', que determina si todo elemento de la secuencia es múltiplo de alg¶un otro.

''todoEsMultiplo''(x: [<math>\mathbb{Z}</math>]): Bool = (<math>\exists</math> a <math>\leftarrow</math> x)(<math>\forall</math> b <math>\leftarrow</math> x) b mod a == 0


12. ''enTresPartes'', que determina si en la secuencia aparecen (de izquierda a derecha) primero 0s, después 1s y por último 2s. Por ejemplo [0; 0; 1; 1; 1; 1; 2] cumple con enTresPartes, pero [0; 1; 3; 0] o [0; 0; 0; 1; 1] no.
¿Cómo modificaría la expresión para que se admitan cero apariciones de 0s, 1s y 2s (es decir, para que por ejemplo [0; 0; 0; 1; 1] o [ ] sí cumplan nTresPartes?


''enTresPartes''(x: [<math>\mathbb{Z}]</math>): Bool = ( estaOrdenada(x) <math> \land x_0== 0 \ \land \ x_{|x|-1}==2 \ \land \ 1 \in x </math> )

Pero si queremos que no sea estrictamente necesaria la pertenencia de al menos un 0, un 1 y un 2, podemos modificarlo de la siguiente manera:


''enTresPartesPrima''(x: [<math>\mathbb{Z}]</math>): Bool = ( estaOrdenada(x) <math> \land (\forall</math> a <math>\leftarrow</math> x) <math> (0 \geq a  \ \land \ a \leq 2 </math> ) )

===Ejercicio 4===

1- "Todos los naturales menores a 10 que cumplen P, cumplen Q":

aux a: Bool (<math>\forall x \in</math> [0..10)) (<math>P(x) \wedge Q(x)</math>)

Esta mal porque no queremos que para todos, todos cumplan P y Q, sino que cuando P sea verdadero, Q tambien lo sea:

aux a: Bool (<math>\forall x \in</math> [0..10))(<math>P(x) \Rightarrow Q(x)</math>)

2- "No hay ningún natural menor a 10 que cumpla P y Q":

aux c: Bool = <math>(\neg ( \exists x \in [0..10) P(x)  \wedge \neg ( \exists x \in [0..10) Q(x))</math>

Pero esto diría que ninguno en s cumple P y ninguno en s cumple Q.
En su lugar deberíamos poner:

aux c: Bool = <math>\neg ( \exists x \in [0..10) ) P(x) \wedge Q(x)</math>;