Temas de Final (Paradigmas)

De Cuba-Wiki
Saltar a: navegación, buscar
Back.png Volver a la página de la materia

Funcional[editar]

La parte de funcional abarca dos grandes áreas: la parte más teórica vinculada al lambda cálculo tipado y la parte práctica utilizando Haskell.

La primera se centra en tipado, semántica operacional, inferencia de tipos, extensiones del lenguaje, agregado de referencias y recursión. La segunda se focaliza más en alto orden (como esquemas de recursión) o currificación.

Haskell[editar]

Alto Orden[editar]

Un ejercicio común es escribir esquemas de recursión para estructuras de datos nuevas que se indican en el momento, por ejemplo, árbol binario:

data BinTree a = Nil | Branch a (BinTree a) (BinTree a)

La aridad de un fold sobre una estructura esta dada por sus constructores. Así, por cada constructor recursivo se agrega una función que tome los tipos básicos del constructor y los resultados de las llamadas recursivas, y devuelva el resultado. Para los constructores básicos simplemente se toman los parámetros que reciba y se devuelve el resultado. Suponiendo que el resultado es de tipo b:

De Nil:                     b           
De Branch a (BT a) (BT a):  a -> b -> b -> b

El fold va a tomar estas funciones en algún orden (generalmente recursivos primero), una instancia de la estructura, y devolver el resultado:

foldBinTree :: (a -> b -> b -> b) -> b -> BinTree a -> b

Otro ejemplo más complejo es el de expresiones regulares:

data RE = Const Char | WildCard | Plus RE | Seq RE RE | Union RE RE

foldRE :: (a -> a) -> (a -> a -> a) -> (a -> a -> a) -> (Char -> a) -> a -> RE -> a
foldRE fplus fseq funion fconst fwild re = 
    case re of
        Plus r1 -> fplus (rec r1)
        Seq r1 r2 -> fseq (rec r1) (rec r2)
        Union r1 r2 -> funion (rec r1) (rec r2)
        Const c -> fconst c
        WildCard -> fwild
    where rec = foldRE fplus fseq funion fconst fwild

Tipado en Lambda Cálculo[editar]

El objetivo del sistema de tipos de lambda cálculo es asegurar que si un término es cerrado, está bien tipado y termina, entonces evalúa a un valor (a menos que se mantengan formas normales que no sean valores para representar errores).

La correctitud del sistema de tipos se basa en el progreso y la preservación. El progreso indica que si se tiene un término M cerrado y bien tipado, entonces es un valor, o existe un M' tal que el primero evalúa en el segundo. La preservación se refiere a que el progreso preserva tipos.

Agregado de Referencias[editar]

Al agregar referencias al lambda cálculo tipado se deben modificar las definiciones de progreso y preservación, agregando al store (mu) y su contexto de tipado (sigma). La expresión original de preservación era:

La versión revisada incluye, además del tipado de M, el tipado del store asociado y su inclusión en otro contexto de tipado de store que será el usado para el N. Es necesario que el Sigma usado para N sea distinto, pues puede incrementarse ante posibles alocaciones.

Respecto de progreso, es necesario cuantificarlo universalmente sobre los stores correctamente tipados respecto del término cerrado. Esto es, dado un M cerrado y bien tipado, , entonces M es un valor o bien para cualquier store , existen tales que .

Recordar que al agregar referencias se pierde terminación. Es decir, dado un término de lambda cálculo con referencias, este puede no terminar. Por ejemplo:

M = \r : Ref (Unit -> Unit).
     (r := \x : Unit.(!r)x);(!r)unit)

M(ref (\x : Unit.x))

Recursión en Lambda Cálculo[editar]

El operador más usado para la recursión en lambda cálculo es el de punto fijo, el operador fix. Se aplica sobre una función que toma un parámetro de un determinado tipo y devuelve un resultado del mismo tipo (la función puede luego tomar más parámetros).

El operador se encarga de reemplazar el parámetro dentro de la función por una nueva llamada a fix sobre la misma función. Es decir:

Notar que la sustitución que se realiza dentro del nuevo término es de alguna manera lazy, no se resuelve si no es necesaria. Esto permite desdoblar el control dentro de la función con un if para que en los casos base no se resuelva el fix anidado. Por ejemplo:

M = \f : Nat -> Nat.
     \x : Nat.
      if x = 0 then 1 else x * f (pred(x))

let fact = fix M in fact 3

Asimismo, no es necesario realizar ningún desdoblamiento para tipar un término fix, el axioma simplemente indica que fix M es de un tipo sigma sii M es una función de sigma en sigma.

Otra posibilidad es usar letrec que es una manera más cómoda de utilizar el fix, pues no es necesario que la función a la que se aplica el letrec se reciba a sí misma como parámetro:

Extensiones de Lambda Cálculo[editar]

Otro tema recurrente es extender los algoritmos de inferencia de tipos, semántica o chequeo de tipos de lambda cálculo dada una extensión al lenguaje, como ser una nueva estructura de datos (árbol binario es el ejemplo típico) o una nueva estructura de control (excepciones, case of, switch).

Chequeo de Tipos[editar]

Los axiomas para el chequeo de tipos se basan en una serie de precondiciones (las cuales pueden hacer uso de predicados auxiliares en caso de ser necesario) que generalmente están relacionadas con el tipado de átomos del término a tipar.

Recordar que siempre hay un contexto de tipado (gamma) presente, el cual asigna tipos a las variables libres de la expresión. Esto hace que toda sentencia que ligue variables (como ser la abstracción) deba tener un cuidado especial en su axioma:

Otra construcción que liga variables es el case, en el caso de los parámetros de los constructores recursivos del tipo que se está observando:

Un ejemplo un tanto más elaborado es el de match, donde además es necesario pedir que el patrón no posea variables repetidas para que tipe. Notar que para que M2 tipe es necesario agregar al contexto el tipo de las variables libres que aparecen en el patrón, que serán ligadas en la evaluación.

Inferencia de Tipos[editar]

El algoritmo de inferencia de tipos se basa en dos partes: las llamadas a los subtérminos del término a analizar y la sustitución que se obtiene del most general unifier de todos los tipos necesarios.

El caso típico es el if-then-else, donde primero se obtienen los tres contextos de tipado y tipos para cada subtérmino, luego se unifica el primero a bool y los otros dos entre sí, y todas las variables del mismo nombre entre los términos. Notar que los términos retornados por el algoritmo de inferencia pueden no ser los mismos ya que están decorados.

Dado

Si





Entonces

El caso en que se ligan variables, como ser la abstracción, es un poco más complicado, pues implica sacar la información del tipo de las variables del contexto a retornar (recordar que el contexto sólo indica cómo tipar variables libres). Para estas variables es necesario asegurarse de usar la información que había de ellas en el contexto, o usar una variable fresca si no.

Nunca se deben devolver metavariables (sigma, rho, tau) del algoritmo, siempre deben ser variables de tipo. Las metavariables son meramente comunicativas para expresar la mecánica del algortimo.

Dado


si


si no, sea s variable fresca

Valores[editar]

No siempre que se extienda el lenguaje se aumenta el conjunto de valores, pero puede que sí aumenten las formas normales. Recordar que los valores del lenguaje son los resultados a los que puede evaluar un término bien tipado y cerrado. En cambio, las formas normales son términos que no pueden evaluarse más.

Si se tiene una forma normal cerrada que no es un valor, se tiene un término que representa un estado de indefinición o error; pues no es posible seguir evaluándolo, pero tampoco es un resultado válido de una computación.


Lógico[editar]

El paradigma lógico tiene el acento teórico puesto en las definiciones de lógica proposicional y de primer orden y los métodos de resoluccón. La parte práctica comprende ejercicios en Prolog.

Conversión a Forma Clausal[editar]

Para aplicar el método de resolución es necesario convertir la fórmula que se tiene a forma clausal. Esta forma no posee cuantificadores, y es una conjunción de disyunciones de literales, donde cada literal puede estar o no negado.

Eliminar implicaciones[editar]

El primer paso es sencillo: consiste en eliminar las implicaciones de la fórmula, escribiéndolas como la disyunción entre el consecuente y la negación del antecedente.

Forma Normal Negada[editar]

En forma normal negada todas las negaciones se llevan a nivel de las fórmulas atómicas. Es decir, las negaciones se aplican solamente a predicados, y no a términos más complejos.

Forma Normal Prenexa[editar]

En la forma normal prenexa se mueven todos los cuantificadores al principio de la expresión. En este paso aún se preserva equivalencia lógica, es decir, para cualquier fórmula puede encontrarse otra lógicamente equivalente (es decir, que A sii B es tautología) que esté en forma normal prenexa.

Forma Normal de Skolem[editar]

La skolemización es un proceso que permite la eliminación de cuantificadores existenciales. Para esto, por cada cuantificador existencial, se calculan cuáles son las variables libres de la expresión que este afecta, y se reemplaza toda aparición de la variable cuantificada por una función que toma dichas variables libres. De no haber, se introduce un símbolo de constante.

Notar que la skolemizacion preserva satisfactibilidad, pero no validez. Por ejemplo, la expresion es válida (pues siempre se puede tomar un valor de x igual a a) pero no lo es, ya que depende del valor en el modelo que la asignación le aplique a b.

De todas maneras, el método solamente requiere que se preserve insatisfactibilidad para poder probar la validez de la negación de la fórmula original. Por la forma en que se va construyendo el resutado se recomiendo Skolemnizar de afuera hacia adentro ya que la formula obtenida resulta más clara.

Forma Clausal[editar]

Para pasar de Skolem a forma clausal, se pasa la matriz (parte sin los cuantificadores) a forma conjuntiva (conjuncion de disyunciones), se distribuyen los cuantificadores sobre cada grupo de disyunciones y se los eliminan adoptando notación de conjuntos.

Resolución[editar]

La resolución consiste en una serie de aplicaciones de la regla de resolución sobre literales de pares de clausulas, hasta llegar a la clausula vacia, que es trivialmente insatisfacible. Puesto que hay una cantidad limitada de combinaciones, el algoritmo siempre termina, aunque puede que sea en un numero exponencial de pasos.

De esto se desprenden dos reglas: de búsqueda (qué dos cláusulas se toman) y de selección (que terminales dentro de las clausulas se eliminan).

Resolución Lineal[editar]

Consiste en partir de una cláusula inicial y realizar todas las aplicaciones de la regla de resolución a partir de la inicial o del resultado de la resolución anterior. Si bien reduce el espacio de búsqueda, aún no lo determina, y queda pendiente selección. Preserva completitud.

Resolución SLD[editar]

La resolución SLD es una variante de lineal que se aplica sobre cláusulas de Horn (que tienen a lo sumo un literal positivo). Se debe tener un único goal (clausula con todos negativos) y los demás reglas o hechos.

A cada paso se toma una cláusula de definición o hecho cuyo literal positivo unifique con alguno de los negativos de la goal actual, y se aplica resolución, avanzando un paso en la resolución lineal.

Si bien aún no se especifica cuál cláusula se elige a cada paso, el espacio de búsqueda es mucho más reducido. Esta resolución, aplicada sobre un conjunto de cláusulas de Horn, es completa y correcta.

Estrategia en Prolog[editar]

La estrategia es la suma de las reglas de búsqueda y selección. Prolog realiza SLD tomando las cláusulas de arriba a abajo, y selección de izquierda a derecha. La sustitución que se obtiene al final de cada rama exitosa del árbol SLD es la sustitución respuesta del cómputo.

Notar que esta estrategia hace que se pierda completitud (aunque se mantiene correctitud). Es posible que haya una resolución SLD para las cláusulas existentes y Prolog no la encuentre.

El siguiente es un ejemplo a partir de las cláusulas:

ArbolSLD.PNG

Implementación en Prolog[editar]

Las cláusulas de definición consisten en un literal positivo B con todos los demás A1, A2, An negados, lo que equivale a decir que la conjunción de los negados implica al positivo. En prolog, esto se escribe como B :- A1, A2, An. Los hechos son simplemente un terminal positivo, y se escriben directamente en prolog.

La resolución se implementa recorriendo el árbol de manera DFS utilizando una pila.

  • Se usa una pila para representar los atomos del goal.
  • Se hace un push del resolvente del atomo del tope de la pila con la clausula de definicion.
  • Se hace un pop cuando el atomo del tope de la pila no unifica con ninguna clausula de definicion mas (luego, el atomo que queda en el tope se unifica con la siguiente clausula de definicion)

ArbolProlog.PNG

Objetos[editar]

La parte práctica de objetos está dada en Smalltalk, aunque también pueda estudiarse sobre otros lenguajes orientados a objetos, posiblemente tipados, como ser Java. La parte teórica se centra en los fundamentos, el subtipado visto sobre lambda cálculo, la representación del paradigma usando lambda cálculo y la construcción de un intérprete funcional.

Subtipado[editar]

Conteo[editar]

Dado un lenguaje con tipos básicos (como ser Bool, Nat, Int y Float), registros y funciones, un problema frecuente es el conteo de supertipos y subtipos de un cierto tipo.



Las fórmulas anteriores sirven para contar subtipos y supertipos no estrictos (es decir, incluyendo al tipo original como subtipo/supertipo de sí mismo). Para contar subtipos o supertipos estrictos, aplicar la misma fórmula y restar 1 al resultado final (es decir, eliminar el tipo original).

Tipado Algorítmico[editar]

El tipado algorítmico busca el tipo mínimo al que tipe una determinada expresión. Para esto usa el algoritmo de subtipado, el cual dados dos tipos S y T, devuelve true sii S <: T, y se nota |-> S <: T.

Los axiomas del tipado algorítmico son exactamente los mismos que los axiomas coomunes de tipado, exceptuando TA-Sub y TA-App. El primero es un axioma no dirigido por sintaxis que permite cambiar el tipo de un término a uno más general. La idea es posponer lo más posible su uso, pues se está buscando el tipo mínimo.

El axioma de aplicación se modifica permitiendo que el parámetro que recibe la abstracción sea de un tipo inferior al que espera; es decir, si espera T y se le pasa S con S <: T.

Este algoritmo es correcto, es decir, si determina que un término M tiene tipo T, entonces es posible chequear que M tiene tipo T.

El algoritmo también verifica sub completitud, es decir, que si es posible chequear que un término M tiene tipo T, el algoritmo devuelve algun tipo S menor o igual a T.

Esto, sumado a correctitud, indica que el algoritmo siempre devuelve el tipo mínimo.

Join y Meet[editar]

Dados dos tipos S y T, se define el Join de ambos como la disyunción (unión) de ambos tipos, es decir, el mínimo tipo tal que S y T heredan de él.

Análogamente, el meet de S y T es la conjunción, el máximo tipo tal que hereda tanto de S como de T. El meet puede no existir.

De esta forma, teniendo un término del tipo if M then N else O, donde N:T1 y O:T2, el tipo resultante del if es el join entre T1 y T2. Esto permite que un if tipe sin necesidad que ambas ramas retornen exactamente el mismo tipo.

Codificación en Lambda Cálculo[editar]

Un ejercicio posible es tener que escribir una estructura de clases en lambda cálculo de acuerdo a la codificación vista en clase, y hacer algunas operaciones elementales sobre ellas.

Para este apunte los ejemplos a usar serán la clase Punto (con valores x e y, getters y setters) de la que hereda PuntoColor (que agrega un entero que representa el color).

Lo fundamental es saber que las clases se codifican como funciones que toman la representación de un objeto y devuelven un objeto en sí, donde la representación del objeto es un registro con los fields. El objeto, por su parte, es un registro con las funciones que expone. Por ejemplo:

PuntoRep = {x:Ref Nat, y:Ref Nat}
Punto = {getx:Unit->Nat, gety:Unit->Nat,
        setx:Nat->Unit, sety:Nat->Unit,
        moveUp:Unit->Unit}

Hay dos codificaciones que pueden utilizarse: la primera utiliza fix para generar la referencia a self, y la segunda (más eficiente) utiliza un source (referencia de sólo lectura).

Utilizando Fix[editar]

En una primera versión de la codificación con fix, las clases son de tipo ClaseRep -> Objeto -> Objeto. Esto hace que dada una representación, luego pueda usarse fix para inyectar referencias a sí misma donde sean necesarias.

Pero esto lleva a una recursión infinita, por lo que es necesario usar thunks. La idea es envolver a un tipo con una abstracción, para demorar su evaluación hasta que sea necesario y no generar un desdoble infinito. Así, toda referencia a un término se reemplaza por un . Cuando se desea utilizarlo, se lo evalúa retornando su valor: N unit.

Por lo tanto, una clase es una función ClaseRep -> (Unit->Objeto) -> (Unit->Objeto).

objetoClass =
 \r : ClaseRep.
  \self : Unit -> Objeto.
   \_ : Unit.
    let super = padreClass r self unit in ...

En el ejemplo de Punto y PuntoColor, se tiene lo siguiente. Notar que para utilizar self es necesario resolverlo con unit primero, no así con super.

puntoClass =
 \r:PuntoRep.
  \self:Unit -> Punto.
   \_:Unit.
    {getx = \_:Unit.!(r.x),
     gety = \_:Unit.!(r.y),
     setx = \i:Nat.(r.x):=i,
     sety = \i:Nat.(r.y):=i,
     moveUp = \_:Unit.(r.x):=suc((self unit).getx unit)
    }

puntoColorClass =
 \r:PuntoColorRep.
  \self:Unit -> PuntoColor.
   \_:Unit.
    let super = puntoClass r self unit in
     {getx = super.getx,
      gety = super.gett,
      setx = super.setx,
      sety = super.sety,
      getc = \_:Unit.!(r.c),
      setc = \i:Nat.(r.c):=i,
      moveUp = \_:Unit.super.moveUp;(r.c):=suc((self unit).getc unit)
     }

El constructor es una función que toma Unit (aunque podría tomar argumentos para la inicialización) y dada una representación inicial construye el objeto usando fix.

newPunto = 
 \_:Unit. let r = {x=ref 0, y=ref 0} in 
  fix (puntoClass r) unit

newPuntoColor = 
 \_:Unit. let r = {x=ref 0, y=ref 0, c=ref 0} in
  fix (puntoColorClass r) unit

Utilizando Source[editar]

Si bien un primer enfoque usa Ref, no sirve pues si T <: S, no vale que Ref T <: Ref S, y la herencia es necesaria para que se mantenga el type check en la jerarquía. Como self es una referencia de sólo lectura en la clase, es posible usar Source en su lugar.

La aridad de las clases es ahora ClaseRep -> (Source Objeto) -> Objeto, pues además de recibir la representación interna como parámetro, recibe una referencia a sí misma.

objetoClass =
 \r : ClaseRep.
  \self : Source Objeto.
   let super = padreClass r self in ...

En el ejemplo resultaría lo siguiente. Notar que ahora, en lugar de usar self unit para referirse a sí mismo, se utiliza !self, o sea, se desreferencia la referencia a this.

puntoClass =
 \r:PuntoRep.
  \self:Source Punto.
    {getx = \_:Unit.!(r.x),
     gety = \_:Unit.!(r.y),
     setx = \i:Nat.(r.x):=i,
     sety = \i:Nat.(r.y):=i,
     moveUp = \_:Unit.(r.x):=suc((!self).getx unit)
    }

puntoColorClass =
 \r:PuntoColorRep.
  \self:Unit -> PuntoColor.
   \_:Unit.
    let super = puntoClass r self unit in
     {getx = super.getx,
      gety = super.gett,
      setx = super.setx,
      sety = super.sety,
      getc = \_:Unit.!(r.c),
      setc = \i:Nat.(r.c):=i,
      moveUp = \_:Unit.super.moveUp;(r.c):=suc((!self).getc unit)
     }

Si bien la codificación de clases es más simple, se complica en el constructor, pues es necesario tener una referencia a this (cuando this aún no existe) para poder llamar a la función de clase. Esto se resuelve teniendo un objeto dummy que se pasa en la inicialización. El dummy no hace absolutamente nada, pero sus funciones deben respetar la aridad del objeto.

dummyPuntoColor : PuntoColor =
    {getx = \_:Unit. 0,
     gety = \_:Unit. 0,
     getc = \_:Unit. 0,
     setx = \i:Nat.unit,
     sety = \i:Nat.unit,
     setc = \i:Nat.unit,
     moveUp = \_:Unit.unit)

El constructor entonces le pasa una referencia fresca al objeto dummy a la función de clase, pisa el dummy de la referencia con el resultado y lo devuelve.

newPuntoColor : Unit -> PuntoColor =
 \_:Unit.
  let r = {x=ref 0, y=ref 0, c=ref 0} in
   let c = ref dummyPuntoColor in
    (c := puntoColor r c; !c)