Segundo Parcial 2do Cuat 2009 (Paradigmas)
Ejercicio 2 - Resolución Lógica[editar]
Las siguientes formulas definen qué es una expresión regular y qué no lo es.
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle regex( \lambda ) \,}
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \forall x (simbolo(x) \Rightarrow regex(x))}
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \forall r (regex(r) \Rightarrow regex(r^*))}
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \forall r (regex(r) \Rightarrow regex(r^+))}
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \forall r_1 \forall r_2 (regex(r_1) \land regex(r_2) \Rightarrow regex(r_1.r_2)}
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \forall r_1 \forall r_2 (regex(r_1) \land regex(r_2) \Rightarrow regex(r_1 || r_2)}
{ !, a, b, . . . , z } son constantes, { Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle ^*} , Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle ^+} } son símbolos de función unarios y { ||, . } símbolos de función binarios. Asumir que el predicado simbolo vale para cada letra: simbolo(a), simbolo(b), . . . simbolo(z). Interesa verificar que “plp forever” es una expresión regular, para lo cual se pide probar que Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle regex((p . l . p)^+) }
a) (5 puntos) ¿Es posible dar una demostracion por resolucion sld de este hecho? ¿Por que sı/no?
RESPUESTA
Es posible dar una demostracion SLD pues todas las clausulas son de Horn, y tenemos una clausula goal para arrancar. Esto no dice nada sobre el resultado de la demostración (ie: si se llega o no a una refutación).
b) (10 puntos) Dar una demostración por resolución de este hecho que no sea sld. Justificar.
RESPUESTA
Primero llevamos las formulas del enunciado a su forma clausal:
1) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle regex (\lambda \,)}
}
2) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(r_2), regex(r_2 ^+)}
}
3) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg simbolo(x_3), regex(x_3)}
}
4) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(r_3), \neg regex(r_4), regex(r_3.r_4)}
}
5) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(r_5), \neg regex(r_6), regex(r_5||r_6)}
}
6) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(r_7), regex(r_7^*)}
}
7) goal {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex((p.l.p)^+)}
}
Ahora la demostracion por resolución no lineal
De 7 y 2: Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( r_2 \leftarrow p.l.p)}
8) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(p.l.p)\,}
} (asocia a derecha : p.(l.p))
De 8 y 4: Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( r_3 \leftarrow p, r_4 \leftarrow l.p)}
9) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(p), \neg regex(l.p)}
}
De 9 y 3: Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( x_3 \leftarrow p )}
10) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg simbolo(p), \neg regex(l.p)}
}
De 10 y Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle P_p \equiv simbolo(p)}
: Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( )}
11) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(l.p) \,}
}
De 11 y 4: Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( r_3 \leftarrow l, r_4 \leftarrow p)}
12) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(l), \neg regex(p)}
}
De 12 y 3: Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( x_3 \leftarrow p )}
13) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg regex(l),\neg simbolo(p)}
}
De 13 y 3: Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( x_3 \leftarrow l)}
14) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg simbolo(l), \neg simbolo(p)}
}
De 13 y Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle P_p}
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( )}
15) {Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \neg simbolo(l)}
}
De 15 y Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle P_l \equiv simbolo(l)}
: Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma = ( )}
16) Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \Box}
La demostracion NO ES SLD porque no es cierto que en cada paso el resolvente del paso anterior es utilizado, por ejemplo en 15 se utiliza 13 y Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle P_p}
Ejercicio 4 - Smalltalk (17 puntos)[editar]
La clase Region y sus subclases modelan ciertos subconjuntos de N2 que se definen en terminos de su geometria.
| class Circulo super Region |
class Rectangulo super Region |
class Interseccion super Region |
class Union super Region |
|---|---|---|---|
| #centro: unPunto radio: unNumero “Constructor con centro y radio” #centro “Devuelve el punto del centro” |
#infIzq: unPunto supDer: otroPunto “Constructor con dos vertices” #infIzq “Devuelve el punto inferior izquierdo” #supDer “Devuelve el punto superior derecho” |
#de: unaRegion con: otraRegion “Constructor con dos regiones” #region1
|
#de: unaRegion y: otraRegion “Constructor con dos regiones” #region1
|
Implementar los metodos de modo que todas las instancias sean capaces de responder apropiadamente los
mensajes relevantes.
Definirlos en las clases que correspondan, de modo tal de compartir el comportamiento siempre que sea
posible. Pueden agregarse nuevos meetodos de clase o instancia a Point de ser necesario.
Justificar las decisiones tomadas.
a) (5 puntos) contiene: unPunto, que indica si el punto esta dentro de la region receptora.
b) (2 puntos) cotaDer, que devuelve algun numero x0 que acota “por derecha” la region receptora, cuyos puntos quedan a la izquierda de la recta vertical que pasa por x0.
c) (2 puntos) cotaSup, que devuelve algun numero y0 que acota “por arriba” la region receptora, cuyos puntos quedan por debajo de la recta horizontal que pasa por y0.
d) (8 puntos) puntos, que devuelve un conjunto con todos los puntos contenidos en la regi´on receptora.
Sugerencia: cada region esta totalmente incluida en una region mas grande, determinada por las cotas.
Respuesta
a) Implementando todos como metodos de instancia.
@Interseccion: ^(self region1 contiene: unPunto) & (self region2 contiene: unPunto).
@Union: ^(self region1 contiene: unPunto) | (self region2 contiene: unPunto).
@Circulo: ^(unPunto dist: (self centro)) < (self radio).
@Rectangulo: "Algunos parentesis pueden omitirse se ponen por claridad" ^(((unPunto x > (self infIzq) x ) & (unPunto y > (self infIzq) y )) & (unPunto x < (self supDer) x )) & (unPunto y < (self supDer) y ).
b) Todos como metodos de instancia nuevamente
@Interseccion y @Union |c1 c2| c1 := self region1 cotaDer. c2 := self region2 cotaDer. (c1 > c2) ifTrue:[^c1] ifFalse:[^c2].
@Rectangulo ^self supDer x + 1.
@Circulo ^(self centro x + self radio x) + 1.
c) Todos como metodos de instancia
@Interseccion y @Union |c1 c2| c1 := self region1 cotaSup. c2 := self region2 cotaSup. (c1 > c2) ifTrue:[^c1] ifFalse:[^c2].
@Circulo ^(self centro y + self radio y) + 1.
@Rectangulo ^self supDer y + 1.
d) La definimos en la clase Region, heredada como metodo de instancia al resto.
@Region
|rv ix iy|
rv := Set new.
ix := self cotaDer.
iy := self cotaSup.
[iy >= 0] whileTrue: [ [ix >= 0] whileTrue: [|p| p:=Point x:ix y:iy.
(self contiene:p) ifTrue:[rv add:p].
ix := ix - 1.].
ix := self cotaDer.
iy := iy - 1].
^rv.
Ejercicio 5 - Subtipado (19 puntos)[editar]
Trabajaremos con los tipos Bool <: Nat <: Int <: Float, funciones y registros. Además asumiremos que Float tiene la operación +, que Int tiene además las operaciones pred y suc, y que Bool cuenta también con la operación if, con las reglas de tipado habituales.
a) (6 puntos)
Considerar esta regla de subtipado:
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle { \, \over \sigma <: \{l_i : \sigma\}_{i=1,..,n}} \quad (SRec)}
En términos del principio de sustitutividad: “siempre que se espere un registro con campos (todos) de tipo Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma} podría usarse en su lugar un término M : Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma} , que se interpretaría como registro cuyos campos tienen (todos) valor M”.
Incorporando dicha regla, ¿es tipable el siguiente termino?
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \lambda n:\{l:Nat\}.suc(n.l)) \quad 4}
Exhibir una derivacion que lo pruebe o lo refute. Puede asumirse como axioma que Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \Gamma \vartriangleright 4 : Nat}
RESPUESTA
Es tipable, segun vemos a continuacion.
El objetivo se encuentra en demostrar que la expresion tipa usando las reglas de tipado vistas. Mostraremos que tiene tipo Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \sigma} que luego unificara con el tipo Nat.
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \dfrac { \dfrac { \dfrac { \dfrac { \dfrac {\,}{\Gamma \vartriangleright n:\{l:Nat\} } TVar } { \Gamma \vartriangleright n.l \, : \, Nat } TReg^{(*)} } { \Gamma = \{\{n:Nat\}\} \vartriangleright suc(n.l):Nat } TSuc } { \lambda n:\{l:Nat\} \, . \, suc(n.l) \, : \, \{l:Nat\} \rightarrow \sigma } TAbs \qquad \quad \dfrac { \dfrac {\,}{\emptyset \vartriangleright 4:Nat} \ AXIOMA \quad \quad \dfrac {\,}{Nat <: \{l:Nat\} } \ SRec } { \emptyset \vartriangleright 4:\{l:Nat\} } TSub } { \emptyset \vartriangleright \lambda n:\{l:Nat\}.suc(n.l) \quad 4 \quad : \sigma } TApp }
(*) No es exacto este paso, pero esta simplificado. La idea es que se proyecta el valor dentro del registro si el registro tiene el valor de el mismo tipo.
b) (13 puntos) Suponer que ahora se decidiera agregar al lenguaje un nuevo termino M[l = N], que representa al registro M en el que l pasa a valer N, con la siguiente regla de tipado:
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \dfrac { \Gamma \vartriangleright M:\{l_i:\sigma _i\}_{i=1..n} \qquad \Gamma \vartriangleright N : \sigma _k \qquad (1 <= k <= n) } {\Gamma \vartriangleright M[l_k = N]:\{l_i : \sigma _i\}_{i=1..n} } \quad TASS }
Mostrar que SRec no es buena idea en este contexto:
- Dar una expresion M del lambda calculo (apropiada para lo que sigue).
- Explicar brevemente por que no tiene sentido evaluar M.
- Dar una derivacion que pruebe que, sin embargo, M tiene tipo.
RESPUESTA
Por SREC en lugar de un registro de Nats todos iguales puedo utilizar un Nat n que representa a todos los elementos del registro. Si yo puedo asignar un valor a un elemento del registro, el valor n que represente ese registro no tiene sentido pues no puedo acceder a los elementos del registro para asignar, y semanticamente el registro podria tener valores diferentes por lo que su representacion n dejaria de ser correcta.
Consideremos por ejemplo la expresion
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle (\lambda r:\{l_1:Nat,l_2:Nat\} \, . \, r[l_2=40]) \quad 3}
Esto esta permitido por SREC, y tipa bien, pero cuando tengo que evaluar Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle 3 \, [l_2 = 40]} no puedo y no tiene sentido.
Finalmente demostramos que la expresion tipa correctamente.
Error al representar (SVG o PNG como alternativa (MathML puede ser habilitado mediante plugin de navegador): respuesta no válida («Math extension cannot connect to Restbase.») del servidor «https://en.wikipedia.org/api/rest_v1/»:): {\displaystyle \dfrac { \dfrac { \dfrac { \dfrac { \, } {\Gamma \vartriangleright r: \{ l_1:Nat,l_2:Nat \} } \, TVAR \qquad \dfrac { \, } {\Gamma \vartriangleright 40 : Nat } \, ^{TSUC}_{TZERO} \qquad 1 <= 2 <= 2 } { \Gamma = \{ r: \{ l_1:Nat, l_2:Nat \} \} \vartriangleright r [l_2=40] : \{ l_1:Nat,l_2:Nat \} \, \doteq \, \sigma } \, TASS } { \emptyset \vartriangleright \lambda r:\{ l_1:Nat,l_2:Nat \} \, . \, r[l_2=40]:\{ l_1:Nat,l_2:Nat \} \rightarrow \sigma } \, TABS \qquad \dfrac { \dfrac { \, } { \emptyset \vartriangleright 3 : Nat } \, ^{TSUC}_{TZERO} \quad \dfrac { \, } { Nat <: \{l_1 : Nat, l_2 : Nat\} } \, SREC } { \emptyset \vartriangleright 3 : \{l_1 : Nat,l_2 : Nat\} } \, TSUB } { \emptyset \vartriangleright (\lambda r:\{l_1 : Nat,l_2 : Nat \} \, . \, r[l_2 = 40]) \quad 3 \quad : \sigma } \, TAPP }
