Segundo Parcial 2do Cuat 2009 (Paradigmas)

Ejercicio 2 - Resolución Lógica

Las siguientes formulas definen qué es una expresión regular y qué no lo es.

$regex(\lambda )\,$

$\forall x(simbolo(x)\Rightarrow regex(x))$

$\forall r(regex(r)\Rightarrow regex(r^{*}))$

$\forall r(regex(r)\Rightarrow regex(r^{+}))$

$\forall r_{1}\forall r_{2}(regex(r_{1})\land regex(r_{2})\Rightarrow regex(r_{1}.r_{2})$

$\forall r_{1}\forall r_{2}(regex(r_{1})\land regex(r_{2})\Rightarrow regex(r_{1}||r_{2})$

{ !, a, b, . . . , z } son constantes, { $^{*}$, $^{+}$ } 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 $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) {$regex(\lambda \,)$}
2) {$\neg regex(r_{2}),regex(r_{2}^{+})$}
3) {$\neg simbolo(x_{3}),regex(x_{3})$}
4) {$\neg regex(r_{3}),\neg regex(r_{4}),regex(r_{3}.r_{4})$}
5) {$\neg regex(r_{5}),\neg regex(r_{6}),regex(r_{5}||r_{6})$}
6) {$\neg regex(r_{7}),regex(r_{7}^{*})$}
7) goal {$\neg regex((p.l.p)^{+})$}

Ahora la demostracion por resolución no lineal

De 7 y 2: $\sigma =(r_{2}\leftarrow p.l.p)$
8) {$\neg regex(p.l.p)\,$}  (asocia a derecha : p.(l.p))

De 8 y 4: $\sigma =(r_{3}\leftarrow p,r_{4}\leftarrow l.p)$
9) {$\neg regex(p),\neg regex(l.p)$}

De 9 y 3: $\sigma =(x_{3}\leftarrow p)$
10) {$\neg simbolo(p),\neg regex(l.p)$}

De 10 y $P_{p}\equiv simbolo(p)$: $\sigma =()$
11) {$\neg regex(l.p)\,$}

De 11 y 4: $\sigma =(r_{3}\leftarrow l,r_{4}\leftarrow p)$
12) {$\neg regex(l),\neg regex(p)$}

De 12 y 3: $\sigma =(x_{3}\leftarrow p)$
13) {$\neg regex(l),\neg simbolo(p)$}

De 13 y 3: $\sigma =(x_{3}\leftarrow l)$
14) {$\neg simbolo(l),\neg simbolo(p)$}

De 13 y $P_{p}$ $\sigma =()$
15) {$\neg simbolo(l)$}

De 15 y $P_{l}\equiv simbolo(l)$: $\sigma =()$
16) $\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 $P_{p}$

Ejercicio 4 - Smalltalk (17 puntos)

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” #radio “Devuelve el radio”	#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 “Devuelve una region” #region2 “Devuelve la otra region”	#de: unaRegion y: otraRegion “Constructor con dos regiones” #region1 “Devuelve una region” #region2 “Devuelve la otra region”

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)

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:

${\, \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 $\sigma$ podría usarse en su lugar un término M : $\sigma$, que se interpretaría como registro cuyos campos tienen (todos) valor M”.

Incorporando dicha regla, ¿es tipable el siguiente termino?

$\lambda n:\{l:Nat\}.suc(n.l))\quad 4$

Exhibir una derivacion que lo pruebe o lo refute. Puede asumirse como axioma que $\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 $\sigma$ que luego unificara con el tipo Nat.

${\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:

${\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

$(\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 $3\,[l_{2}=40]$ no puedo y no tiene sentido.

Finalmente demostramos que la expresion tipa correctamente.

${\dfrac {{\dfrac {{\dfrac {{\dfrac {\,}{\Gamma \vartriangleright r:\{l_{1}:Nat,l_{2}:Nat\}}}\,TVAR\qquad {\dfrac {\,}{\Gamma \vartriangleright 40:Nat}}\,_{TZERO}^{TSUC}\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}}\,_{TZERO}^{TSUC}\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$