Programación Declarativa Multi-paradigma

Lenguaje

Carácterística introducida

ALGOL

Bloques Gestión dinámica pila (arrays dinámicos)

LISP

Listas y recursión Orden superior Gestión dinámica heap (listas dinámicas), con garbage collection

Simula

Clases y herencia Concurrencia

Pascal

Gestión dinámica heap (punteros), sin garbage collection Código intermedio (P-code)

Prolog

Listas y recursión Variables Lógicas Código intermedio

Smalltalk

Jerarquía de clases Modelo de mensajes

ML

Inferencia de tipos Polimorfismo

Ada

Tipos Abstractos de Datos

Java

Código intermedio (de Prolog) Gestión dinámica heap, con Garbage collection (de LISP) ………… (de muchos otros)

Programación Declarativa vs. Programación Imperativa PROGRAMA

Transcripción de un algoritmo

INSTRUCCIONES MODELO DE COMPUTACIÓN VARIABLES

Órdenes a la máquina Máquina de estados Referencias a la memoria

Más compleja de lo que parece (así lo demuestra la complejidad de sus definiciones semánticas o la dificultad de las técnicas asociadas, e.g., de las técnicas de verificación formal de programas) Distrae la atención del programador sobre el aspecto funcional de la solución para centrarse en el control de la máquina Difícil de paralelizar

Programación Declarativa = Lógica como Lenguaje de programación

PROGRAMA

Especificacion de un problema

INSTRUCCIONES MODELO DE COMPUTACIÓN VARIABLES

Fórmulas lógicas Máquina de inferencias Variables lógicas

function length (L: list): nat B:bool; aux:list;

PROGRAMA IMPERATIVO

B:= is_empty(L); case B of true: return 0; false: aux:=tail(L); return 1+length(aux) end case end function; length(nil) = 0 length(E:L) = length(L)+1

PROGRAMA FUNCIONAL

length(nil,0) length(E.L,N) ! length(L,M) ^ N = M+1

PROGRAMA LÓGICO

RESTRICCION LOGICA CLAUSAL cláusulas de Horn

PARADIGMA RELACIONAL (Pr ol og)

A ! B1 ^ ... ^ Bn, n"0 (donde A no es una ecuación)

LOGICA ECUACIONAL

ecuaciones condicionales

FUNCIONAL (Haskell)

s=t ! s1=t1 ^ ... ^ sn=tn, n"0 (donde todo son ecuaciones)

IDEA 1: PROGRAMA ! ESPECIFICACION EJECUTABLE

Leng. de PROGRAMACION LOGICA ! Leng. de ESPECIFICACION (ejecutable) ! Leng. de PROGRAMACION (alto nivel)

ESPECIFICACION

P R O G R A M A C I O N

L O G I C A

PROGRAMACION

Especificación vs programación Especificación: fib(0)=suc(0) fib(suc(0))=suc(0) fib(suc(suc(X)))=fib(suc(X)) + fib(X) Programa:

fib(X)=fib_aux(suc(0),suc(0),X) fib_aux(A,B,0)=A fib_aux(A,B,suc(X))= fib_aux(B,A + B,X) fib(suc(0))

-> -> -> fib(suc(suc(0))) -> -> -> ->

fib_aux(suc(0),suc(0),suc(0)) fib_aux(suc(0),suc(suc((0)),0) suc(0) fib_aux(suc(0),suc(0),suc(suc(0))) fib_aux(suc(0),suc(suc((0)),suc(0)) fib_aux(suc(suc(0)),suc(suc(suc(0))),0) suc(suc(0))

IDEA 2: PROGRAMA ∫ LOGICA + CONTROL (Kowalski) LOGICA: se relaciona con el establecimiento del QUE CONTROL: e relaciona con elestablecimiento del CÓMO

VENTAJA: el programador aspectos lógicos de la aspectos de control al sistema.

se centra solución y

en deja

Carácterísticas de la Programación Declarativa Nivel más alto de programación:   

   

semántica más sencilla control automático más fácil de paralelizar mayor potencia expresiva menor tamaño del código mayor productividad mejor mantenimiento

Eficiencia ≈ lenguajes imperativos

Descripción formal de un LP Sintaxis: qué secuencia de caracteres constituyen un programa “legal”  

elementos sintácticos del lenguaje modelos de ejecución

Semántica: qué significa (qué calcula) un programa legal dado 

Además de ayudar al programador a “razonar” sobre el programa, es necesaria para implementar correctamente el lenguaje, y sirve para desarrollar técnicas y herramientas de:    

Análisis y Optimización Depuración Verificación Transformación

Semántica (3) Estilos de definición semántica   

Operacional Axiomática Declarativa  Algebraica  Teoría de Modelos  Punto fijo  Denotacional

Semántica operacional (i) es el enfoque más antiguo (con este estilo se definió la semántica de ALGOL’60) primero se define una máquina abstracta M, y el significado de cada construcción se expresa en términos de las acciones a realizar por la máquina la forma má simple de definirla es proporcionar un intérprete para el lenguaje L sobre la máquina M cuyas componentes se describen de modo matemático la definición semántica operacional de un lenguaje lo hace ejecutable proporciona un modelo para la implementación

Semántica operacional (ii) Ejemplo: Structural Operacional Semantics (SOS) (o sistemas de transición de Plotkin) se de finen reglas de transición que especifican los pasos de computación para una construcción compuesta A op B en términos de la semántica de las componentes las reglas se suelen escribir en el estilo de los sistemas de deducción natural _ premisa _ conclusión

Semántica operacional (iii) Dado que las construcciones en general modifican una cierta noción de estado, las reglas de transición se suelen definir sobre configuraciones del tipo las reglas

de transición tienen entonces la forma: ____premisa____ →

indicando que una configuración en otra, cuando se satisface cierta premisa

el conjunto de estas reglas define una relación de transición (que llamaremos →) sobre el conjunto de las configuraciones (un grafo de transiciones)

Semántica operacional (iv) Formalmente, un ST es una 4-tupla (C,I,F,→), donde o

o o o

C es el conjunto de las configuraciones c, que son pares de la forma I ⊆ C es el conjunto de las configuraciones iniciales F ⊆ C es el conjunto de las configuraciones finales → ⊆ C x C es la relación de transición (escribiremos c → c’ para indicar que el par (c,c’) ∈ →

Una secuencia de ejecución es una secuencia de configuraciones c1 c2 ... cn tal que   

c1 ∈ I cn ∈ F ci → ci+1, para cada i en [0..n[

Un ST se llama determinista si para cada c ∈ C existe como mucho un c’ tal que c → c’

Semántica operacional (v) La relación de transición → se define recursivamente como la mínima relación que satisface que: Si c1 → c’1, …. cn → c’n entonces op(c1,…, cn) → op(c’1,…, c’n)

Ejemplo: SOS de un minilenguaje imperativo Expresiones aritméticas, booleanas e instrucciones NOTA: estas reglas son semánticas, no están en BNF!

Arit-expr: a ::= n | X |a0+a1 | a0-a1 | a0*a1 Bool-expr: b ::= true | false | a0=a1 | a0≤a1 | ¬b | b0 ∨ b1 Command: i ::= skip | X:=a | i0;i1 | if b then i0 else i1 |while b do i

ejemplo Semántica de las expresiones aritméticas: Evaluación de constantes → n Evaluación de variables → e(X) asumir que el estado está representado como una función e= {X1→n1…Xk → nk} que asigna a cada variable X su valor n en dicho estado (o error si X no está inicializada)

Evaluación de sumas → n0

→ n1

< a0 + a1, e> → n0 + n1 Evaluación de restas y productos.... similar

ejemplo Semántica de las expresiones booleanas: Evaluación de las constantes < true, e> → true < false, e> → false Evaluación de la igualdad → n0 → n1 < a0 = a1, e> → true → n0

→ n1

< a0 = a1, e> → false

si n0 y n1 son iguales

si n0 y n1 son distintos

ejemplo Semántica de las expresiones booleanas: Evaluación de la comparación → n0 → n1 < a0 ≤ a1, e> → true

n0 es menor o igual que n1

→ n0 → n1 < a0 ≤ a1, e> → false

n0 no es menor o igual que n1

Evaluación de la negación → true < ¬ b,e> → false

ejercicio: disyunción

→ false < ¬ b,e> → true

ejemplo Semántica de las instrucciones: Evaluación de las instrucciones simples < skip, e> → e → n < X:=a , e> → e ° {Xn} Evaluación del condicional → true < i0,e> → e’ < if b then i0 else i1 , e> → e’ →false

< i1,e> → e’

< if b then i0 else i1 , e> → e’

ejemplo Semántica de las instrucciones: Evaluación de la iteración → false < while b do i, e> → e →true

< i,e> → e’’ < while b do i, e’’> → e’ < while b do i, e> → e’

Evaluación de la secuencia < i0,e> → e’’ < i1,e’’> → e’ < i0; i1, e> → e’

Ejercicio Calcular la semántica de: {X:=4; while X≤2 do X:=X-1 } Sem(P)=e if →* e (el lenguaje del ejemplo es determinista) → < while X≤2 do X:=X-1,{X→4}> → {X→4}

Semántica axiomática (i) enfoque típico de los trabajos sobre verificación fomal de programas (con este estilo se definió la semántica de Pascal) el significado de cada construcción i del lenguaje se expresa en términos de una transformación que establece qué se puede afirmar sobre el estado de la máquina tras la ejecución de i en términos de lo que era cierto antes o viceversa, qué debe cumplirse antes para llegar al estado que se quiere obtener tras la ejecución

Semántica axiomática (ii) En general se define representando los estados mediante predicados (en vez de como funciones) y asociando a cada instrucción i del lenguaje un transformador de predicados (o transformador de estados) que funciona en “sentido inverso” al programa es decir, a partir del estado “de llegada”, representado por el predicado p, y dada una instrucción i del lenguaje considerado, el transformador de predicados

pmd: Instrucciones x LógicaPred. -> LógicaPred proporciona el “predicado más debil” pmd(i, p) que expresa lo que debe cumplirse en el estado anterior a la ejecución de i para que, después de dicha ejecución, se haya alcanzado el estado p

Semántica axiomática (iii) Por ejemplo, si i es una instruccion de asignación del tipo ”X:=e“ definimos:

pcm(”X:=e“,p) = p[e → X] donde p[e→ X] es el predicado que resulta de “deshacer el efecto” de haber sustituido X por e en p, es decir, donde está e poner X otra vez

pcm(“X:=a“, Y=[a,b,Z]) ≡ Y=[X,b,Z]

Semántica declarativa (i) el significado de cada construcción se define en términos de elementos y estructuras de un dominio matemático conocido. este enfoque ha dado lugar a diferentes aproximaciones: TEORÍA MATEMÁTICA

1. 2. 3. 4.

Tª Tª Tª Tª

Modelos Lógica Categorías Funciones Recursivas Dominios

ESTILO SEMÁNTICO

-> -> -> ->

Tª DE MODELOS ALGEBRAICA PUNTO FIJO DENOTACIONAL

Semántica declarativa (ii) 1. Semántica por TEORÍA DE MODELOS

STM

Con este estilo se ha definido la semántica de los lenguajes lógicos como Prolog 





Intuitivamente, un programa lógico P es un conjunto de fórmulas lógicas que definen relaciones ejemplo

P= par(0).

par(s(s(X)) ← par(X).

el significado del programa lógico P dado por una semántica STM es el conjunto de átomos (sin variables) que son consecuencia lógica de P: STM(P) = {par(0),par(s(s(0))),par(s(s(s(s(0))))),….}

Semántica declarativa (iii) 2.

Semántica ALGEBRAICA SALG Con este estilo se ha definido la semántica de algunos lenguajes funcionales como OBJ 



Intuitivamente, un programa funcional R es un conjunto de ecuaciones que definen funciones ejemplo R =

par(0)=true par(s(0))=false par(s(s(X)) = par(X) el significado SALG(R) del programa funcional R es el Tipo Abstracto de Datos asociado, definido formamente como la menor congruencia inducida en el dominio del programa (el conjunto de datos que éste manipula) por las ecuaciones del mismo (álgebra inicial)

Semántica declarativa (iv) SALG(R) =

true par(0) par(s(s(0))) par(s(s(s(s(0))))) … false par(s(0)) par(s(s(s(0)))) …

Semántica declarativa (v) 3. Semántica de PUNTO FIJO SPF Se usa para todo tipo de lenguajes (imperativo, lógico, funcional, etc) Se utiliza como enlace para demostrar la equivalencia entre diferentes caracterizaciones de un mismo lenguaje. 



Intuitivamente, se asocia al programa P una transformación (generalmente una función continua) TP definida sobre conjuntos de átomos el significado del programa se define como el menor punto fijo (least fixpoint lfp) de dicha transformación lfp(TP)

Semántica declarativa (vi) 





dado un conjunto C de átomos, definimos la transformación TP (C) así: TP (C) = { A | hay una regla H ← B ∈ P tal que en C hay una instancia del átomo B que está en la premisa de la regla y A se calcula como la correspondiente instancia de la conclusión H} el menor punto fijo de una función T es el menor valor C de su argumento t.q. T(C)=C y se obtiene aplicándolo infinitas veces empezando desde el conjunto vacío ejemplo P= par(0). par(s(s(X)) ← par(X). SPF(P) = lfp(TP)= {par(0),par(s(s(0))),par(s(s(s(s(0))))),….}

Semántica declarativa (vii) 4. Semántica DENOTACIONAL SDEN Con este estilo se ha la semántica de lenguajes funcionales e imperativos, como ML y ADA 



Técnicamente, es la más compleja, pero también muy rica; permite dar cuenta de computaciones que no terminan, orden superior … Se requiere definir:  los dominios sintácticos (construcciones sintác. correctas)  los dominios semánticos (valores asociados a cada const. sintác. correcta)

 las funciones de evaluación semántica (de los dominios sintácticos a los semánticos)  las ecuaciones semánticas 

Operadores estándar sobre dominios + (∪), ×, →

ejemplo: SDEN de un minilenguaje imperativo

::= PROGRAM READ ; BEGIN END; WRITE END ::=

:= | ; | WHILE DO END

::= | | () | ::= …… ::= …….. ::= ……..

ejemplo 

dominios sintácticos: (conjuntos)  Id (identificadores) - predefinido  Cte (Constantes) - idem  Op (Operadores) - idem  Exp (Expresiones) - definido como:

Exp= Id + Cte + (Exp x Op x Exp)

 Inst (Instrucciones) - definido como:

Inst= (Id x Exp) + (Inst x Inst) + (Exp x Inst)

 Prog (Programas)

Prog = Id x Inst x Exp

ejemplo 

dominios semánticos: (funciones)      

E V Sop Sexp Sinst Sprog

(Estados) (Valores) - predefinido (Dominio semántico asociado (Dominio semántico asociado (Dominio semántico asociado (Dominio semántico asociado

a los a las a las a los

operadores) expresiones) instrucciones) Programas)

con las siguientes definiciones: (como funciones!) E = Id → V (estado como función de Id a V) Sop = V x V → V (opera con valores y da valor) Sexp = E → V (evalua una expresion a su valor) Sinst = E → E (transforma estado en estado) Sprog = V → V (lee valor y entrega valor)

ejemplo 

valuaciones

: (de los dominios sintácticos a los dominios semánticos)

 Vconst: Const → V  Vop: Op → Sop

- predefinida - predefinida

 Vexp: Exp → Sexp  Vins: Inst → Sinst  Vprog: Prog → Sprog 

ecuaciones semánticas ejemplo: Vinst[i1;i2](e) = Vinst[i2] (Vinst[i1] (e))

Semántica declarativa (viii) La elección de la semántica depende de: * el uso que se dará a la definición semántica ayuda a la implementación del lenguaje (e.g. OPERACIONAL) ayuda al programador diseño del lenguaje (e.g. PUNTO FIJO) … * el tipo de lenguaje LOGICO FUNCIONAL IMPERATIVO … * la riqueza pretendida para las descripciones

Equivalencia de programas. Corrección y Completitud. La semántica de un lenguaje nos permite razonar sobre la equivalencia de programas  P ≡OB P’ si y solo si SOB (P)=SOB(P’)  P es completo respecto a P’ si SOB (P) ⊇ SOB (P’)  P es correcto respecto a P’ si SOB(P) ⊆ SOB(P’) donde OB= cualquiera de las semánticas que hemos visto

EJEMPLO: SOP(while false do Q) = SOP(skip) En particular, si P’ es una especificación formal (presentada también como un programa, probablemente escrito en otro lenguaje, que resuelve el mismo problema que P de manera más simple aunque menos eficiente). la semántica ayuda a verificar si P es una implementación correcta y completa de la especificación P’: es decir, si computa todo lo que debe y sólo eso. EJEMPLO:

P’=programa funcional “par” P={par(0)=true, par(s(s(X)))=true}

SALG(P) ≠ SALG(P’) de hecho, P no sería una implementación correcta ni completa de P’