Download lenguajes de programación - Departamento de Matematicas
Document related concepts
Transcript
Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Lenguajes de programación LÓGICA COMPUTACIONAL LENGUAJES DE PROGRAMACIÓN Con el fin de ilustrar algunas aplicaciones de la lógica a la computación, presentaremos tres tipos de lenguajes: Dos lenguajes imperativos: IMP y el lenguaje de comandos custodiados de Dijkstra. Francisco Hernández Quiroz Dos lenguajes funcionales. La sintaxis de los dos es igual y se distinguen únicamente por su semántica. Departamento de Matemáticas Facultad de Ciencias, UNAM E-mail: fhq@ciencias.unam.mx Página Web: www.matematicas.unam.mx/fhq Un lenguaje de descripción de procesos concurrentes: Calculus of Concurrent Systems, el cual es más abstracto que un lenguaje de programación en sentido estricto. Facultad de Ciencias Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 1 / 35 Programación imperativa Programación funcional Concurrencia Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 2 / 35 Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Sintaxis y semántica formales Lenguaje IMP La sintaxis del lenguaje IMP se describe a continuación en la notación de Backus-Naur. Empezaremos con las expresiones aritméticas EA: La notación de Backus-Naur (BNF) es ya un estándar para la presentación de la sintaxis de lenguajes de programación. A ::= n | X | (A + A0 ) | (A − A0 ) | (A × A0 ) Sin embargo, en el terreno de la semántica siguen predominando las explicaciones informales. donde n ∈ Z, X ∈ Loc y A, A0 ∈ EA. Tenemos ahora las expresiones booleanas EB: Aquí se usará una notación formal: la semántica operacional estructural. B ::= V | F | (A = A0 ) | (A ≤ A0 ) | ¬B | (B ∧ B 0 ) | (B ∨ B 0 ) Aunque no es el único formalismo para describir los lenguajes de programación (por ejemplo, la semántica denotacional es una opción matemáticamente más elegante) sí es el más cercano a las intuiciones del programador típico. donde A, A0 ∈ EA y B, B 0 ∈ EB. Finalmente, los comandos del lenguaje IMP se definen así: C ::= skip | X := A | (C ; C 0 ) | (if B then C else C 0 ) | (while B do C) donde A ∈ EA, B ∈ EB y C, C 0 ∈ IMP. Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 3 / 35 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 4 / 35 Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Semántica operacional estructural No determinismo Semántica operacional estructural I Semántica operacional estructural II La forma más común de definir el significado de las construcciones de un lenguaje es por medio de explicaciones en una lengua natural (inglés, generalmente). Las reglas de SOE son un tipo particular de reglas de inferencia en las que las premisas y la conclusión son transiciones. Sin embargo, el lenguaje natural se presta a las ambigüedades y éstas, a los errores o a las divergencias entre las diferentes implementaciones de un mismo lenguaje. Una transición tiene la forma α→β Para evitar estos problemas, aquí se usarán reglas de semántica operacional estructural o SOE, para abreviar. La forma concreta de las expresiones α y β, así como las transiciones aceptables, se definirán más adelante. Una regla de inferencia tiene la forma siguiente: p1 , . . . , pn q donde p1 , . . . , pn son las premisas y q es la conclusión. Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 5 / 35 Francisco Hernández Quiroz Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Semántica operacional estructural No determinismo ¿Qué es la programación imperativa? Lógica Computacional Lenguajes de Programación 6 / 35 Estados de la memoria Un estado de la memoria es una función σ : Loc → Z. La expresión σ(X) IMP es un lenguaje imperativo típico: el comando básico es la asignación de valor a las localidades de la memoria de la computadora. nos dice qué valor contiene la localidad X en el estado σ. La alteración del valor de una sola localidad de la memoria cuando se encuentra en el estado σ se representa con la función Para definir el significado de una asignación se parte de la existencia de una máquina virtual que posee una memoria con localidades con nombre: Loc = {X, Y , Z , X0 , . . . } σ[m/X ] , donde X es la localidad modificada y m es el nuevo valor. Formalmente: ( σ(Y ) si X 6= Y σ[m/X ] (Y ) = m en caso contrario. Las localidades pueden tomar valores de Z. El conjunto de estados es Σ. Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 7 / 35 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 8 / 35 Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Semántica operacional estructural No determinismo SOE para IMP. Expresiones aritméticas SOE En el caso de las expresiones aritméticas, las transiciones α → β tienen la forma ha, σi → n En las expresiones booleanas, una transición es hb, σi → T , con b ∈ EB, σ ∈ Σ y T ∈ {V , F }. Las reglas operacionales son: donde a ∈ EA, σ ∈ Σ y n ∈ Z. Diremos que “evaluar operacionalmente la expresión a en el estado σ da como resultado el valor n”. Dicha evaluación se realiza de acuerdo con las siguientes reglas: hn, σi → n hV , σi → V hX, σi → σ(X) ha0 , σi → n ha1 , σi → m h(a0 = a1 ), σi → F ha0 , σi → n ha1 , σi → m h(a0 ≤ a1 ), σi → V En esta regla op puede ser +, − o × y op, +Z , −Z o ×Z (ambos operadores deben coincidir). Lógica Computacional Lenguajes de Programación 9 / 35 Francisco Hernández Quiroz Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Semántica operacional estructural No determinismo para IMP. Expresiones booleanas II ha0 , σi → n ha1 , σi → m h(a0 ≤ a1 ), σi → F hb, σi → V h¬b, σi → F SOE sii n y m son iguales sii n y m no son iguales sii n es menor o igual a m Lógica Computacional Programación imperativa Programación funcional Concurrencia SOE hF , σi → F ha0 , σi → n ha1 , σi → m h(a0 = a1 ), σi → V ha0 , σi → n0 ha1 , σi → n1 n0 op n1 = n ha0 op a1 , σi → n Francisco Hernández Quiroz para IMP. Expresiones booleanas I Lenguajes de Programación 10 / 35 para IMP. Comandos I Las reglas de transición de los comandos son así: sii n no es menor o igual a m hc, σi → σ 0 , donde c ∈ IMP y σ, σ 0 ∈ Σ. El valor de σ 0 se infiere de este modo: hb, σi → F h¬b, σi → V hb0 , σi → T0 hb1 , σi → T1 h(b0 ∧ b1 ), σi → T con T = V si T0 , T1 = V y T = F en caso contrario hb0 , σi → T0 hb1 , σi → T1 h(b0 ∨ b1 ), σi → T con T = V si T0 = V o T1 = V y T = F en caso contrario Comandos atómicos hskip, σi → σ ha, σi → m hX := a, σi → σ[m/X] Composición secuencial hc0 , σi → σ 00 hc1 , σ 00 i → σ 0 h(c0 ; c1 ), σi → σ 0 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 11 / 35 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 12 / 35 Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Semántica operacional estructural No determinismo SOE para IMP. Comandos II Ejemplo Condicionales hb, σi → V hc0 , σi → σ 0 h(if b then c0 else c1 ), σi → σ 0 hb, σi → F hc1 , σi → σ 0 h(if b then c0 else c1 ), σi → σ 0 Dadas las reglas anteriores, no es difícil ver que el programa de IMP siguiente calcula el factorial del número n (si n ≥ 0) y lo guarda en la localidad Y : X := 1; Y := 1; while X ≤ n do (X := X + 1; Y := Y × X) Ciclos hb, σi → F h(while b do c), σi → σ hb, σi → V hc, σi → σ 00 h(while b do c), σ 00 i → σ 0 h(while b do c), σi → σ 0 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 13 / 35 Francisco Hernández Quiroz Lógica Computacional Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Semántica operacional estructural No determinismo No determinismo Lenguajes de Programación 14 / 35 Un lenguaje no determinista Ahora se presentará un lenguaje imperativo con no determinismo explícito. Para esto necesitaremos una categoría especial de comandos llamados comandos resguardados (guarded commands): Como primera aproximación a la computación, IMP es bastante bueno. No obstante, hay una serie de “fenómenos” computacionales que no pueden modelarse con IMP. G ::= (B → C) | (G G0 ) Uno de estos es el no determinismo: la posibilidad de que la ejecución de un programa dé resultados distintos en distintas ocasiones a pesar de que recibe los mismos datos de entrada siempre. donde G y G0 son comandos resguardados y B ∈ EB. Como los comandos resguardados son básicos en nuestro lenguaje, lo llamaremos GCL: guarded command language. He aquí la sintaxis de GCL: El no determinismo puede surgir en diversas situaciones. La más común es la concurrencia de procesos, pero también puede presentarse por una decisión en el diseño mismo de los lenguajes de programación. C ::= skip | abort | X := A | (C ; C 0 ) | if g fi | do g od donde abort es un nuevo programa primitivo, G es un comando resguardado y C, C 0 ∈ GCL. Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 15 / 35 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 16 / 35 Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Semántica operacional estructural No determinismo Semántica operacional I Semántica operacional I Ahora seguimos con las reglas para comandos generales: Comencemos con las reglas de comandos resguardados: ha, σi → m hX := a, σi → σ[m/X] hskip, σi → σ hb, σi → V hb → c, σi → hc, σi hg0 , σi → hc, σ 0 i h(g0 g1 ), σi → hc, σ 0 i hb, σi → F hb → c, σi → fail hc0 , σi → σ 00 hc1 , σ 00 i → σ 0 h(c0 ; c1 ), σi → σ 0 hg1 , σi → hc, σ 0 i h(g0 g1 ), σi → hc, σ 0 i hg, σi → hc, σ 0 i hif g fi, σi → hc, σ 0 i hg0 , σi → fail hg1 , σi → fail h(g0 g1 ), σi → fail hg, σi → fail hdo g od, σi → σ Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 17 / 35 Francisco Hernández Quiroz Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Semántica operacional estructural No determinismo Sintaxis Semánticas Ejemplos Ejemplo hg, σi → hc, σ 0 i hdo g od, σi → hc ; do g od, σ 0 i Lógica Computacional Lenguajes de Programación 18 / 35 Programación funcional El lector puede verificar, haciendo uso de las reglas anteriores y de su conocimiento del , que El siguiente programa implementa el viejo algoritmo de Euclides para calcular el máximo común divisor de los enteros positivos n y m. El resultado queda guardado en las localidades X y Y . Un estilo de programación radicalmente distinto al imperativo es el funcional. La idea básica es que en lugar de programas con instrucciones detalladas para la computadora, se deben usar definiciones de funciones. X := n; Y := m; do X > Y → X := X − Y Y > X → Y := Y − X od Nota: X > Y es una abreviatura, obviamente, de Y ≤ X ∧ ¬(X = Y ). Francisco Hernández Quiroz hc0 , σi → hc00 , σ 0 i h(c0 ; c1 ), σi → hc00 ; c1 , σ 0 i Lógica Computacional Lenguajes de Programación La ejecución de un programa consiste en la evaluación de una función definida anteriormente con argumentos concretos. 19 / 35 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 20 / 35 Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Sintaxis Semánticas Ejemplos Sintaxis Semánticas Ejemplos Sintaxis Declaraciones El estilo funcional de programación permite prescindir de la referencia a una máquina virtual y su memoria. Las funciones tomarán su significado a partir de declaraciones. Una declaración es un conjunto finito de ecuaciones. Del lado izquierdo aparece una función con variables como argumentos; del derecho, aparecen términos del lenguaje funcional. Nuevamente, usaremos la notación Backus-Naur: t ::= n | x | (t+t)0 | (t−t 0 ) | (t×t 0 ) | (if t then t 0 else t)00 | fi (t1 , . . . , tn ) t, t 0 y t 0 designan términos del lenguaje funcional. Obsérvese como en el condicional no se usan expresiones booleanas sino términos como condición. f1 (x1 , . . . , xn1 ) = d1 .. . El valor 0 tendrá el papel de verdadero y cualquier otro valor se considerará falso. fk (x1 , . . . , xnk ) = dk donde d1 , . . . , dk son términos del lenguaje funcional. No se permite más de una ecuación por cada función, pero sí se acepta la recursividad. Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 21 / 35 Francisco Hernández Quiroz Lógica Computacional Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Sintaxis Semánticas Ejemplos Sintaxis Semánticas Ejemplos Semántica operacional Lenguajes de Programación 22 / 35 Semántica con llamada por valor Números n →dv n Las transiciones ahora son de la forma Operadores t0 →dv n0 t1 →dv n1 (t0 op t1 ) →dv (n0 op n1 ) t →ds t 0 Condicional verdadero donde t y t 0 son términos del lenguaje, d es una declaración y s puede tomar el valor v (llamada por valor) o n (llamada por nombre). t0 →dv En el estilo de llamada por valor, los argumentos de las funciones son evaluados antes de evaluar la función misma. t1 →dv n1 ··· tmi →dv nmi di [n1 /x1 ,...,nm /xm ] →dv n i i fi (t1 , . . . , tmi ) →dv n La diferencia entre los dos estilos se manifiestan sólo en una regla de evaluación de términos. Lenguajes de Programación n0 t2 →dv n2 n0 6= 0 if t0 then t1 else t2 →dv n2 Funciones En el estilo de llamado por nombre, la evaluación se pospone hasta que se evalúa el cuerpo mismo de la función. Lógica Computacional t0 →dv 0 n1 if t0 then t1 else t2 →dv n1 Las transiciones dependen de declaraciones específicas. Francisco Hernández Quiroz Condicional falso t1 →dv Conviene prestar atención a la última regla, pues es la que varía con respecto a la llamada por nombre. 23 / 35 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 24 / 35 Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Sintaxis Semánticas Ejemplos Sintaxis Semánticas Ejemplos Llamada por nombre Ejemplos I Números n →dn n Operadores t0 →dn n0 t1 →dn n1 (t0 op t1 ) →dn (n0 op n1 ) Condicional verdadero t0 →dn Supóngase que se tiene la siguiente declaración: f1 (x) = if x then 1 else f1 (x − 1) × x f2 (x, y) = x f3 (x) = f3 (x + 1) Condicional falso t1 →dn t0 →dn t2 →dn n0 n2 n0 6= 0 if t0 then t1 else t2 →dn n2 0 n1 if t0 then t1 else t2 →dn n1 Entonces el programa f1 (n) calcula el factorial de n, en cualquiera de los dos estilos de programación. Funciones di [t1 /x1 ,...,tm /xm ] →dn n i i fi (t1 , . . . , tmi ) →dn n Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 25 / 35 Francisco Hernández Quiroz Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Sintaxis Semánticas Ejemplos Sintaxis Semánticas Ejemplos Ejemplos II Lógica Computacional Lenguajes de Programación 26 / 35 Ejemplos III En cambio, considérese el programa f2 (2, f3 (1)). De acuerdo con las reglas de llamado por nombre, para realizar la evaluación del programa debemos evaluar la expresión Nota Si se adopta el estilo de llamada por valor, el lenguaje funcional se asemeja a un subconjunto de ML. x[x/2,y/f3 (1)] = 2 Si se adopta llamada por nombre, será parecido a un subconjunto de Haskell. que, de acuerdo con la regla para números, nos da 2. En cambio, las reglas de llamada por valor nos piden que primero evaluemos los términos 2 y f3 (1) el segundo de los cuales nunca nos da un resultado, como se puede deducir de la tercera ecuación de la declaración. Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 27 / 35 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 28 / 35 Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Sintaxis Semántica Ejemplos Sintaxis Semántica Ejemplos Concurrencia Communicating Concurrent Systems La idea de que un sistema de cómputo se basa en la ejecución secuencial de una serie de instrucciones por parte de un ente aislado es obsoleta. Los sistemas actuales contienen subsistemas que actúan de manera simultánea y que intercambian información. Estos sistemas se llaman concurrentes. Hay dos modelos fundamentales de cómo se realiza el intercambio de información: 1 2 En los 80, Robin Milner propuso un lenguaje de especificación para procesos concurrentes: CCS (Communicating Concurrent Systems). Dicho lenguaje consta de: Un conjunto de valores (enteros, por ejemplo) que se envían o reciben a través de canales α, β, etc. Operadores para la composición secuencial o paralela de procesos. memoria compartida; envío de mensajes. Un operador de “elección” En el primero, hay un área de la memoria (variables, buffers, etc.) a la que varios sistemas concurrentes tienen acceso para guardar o leer datos. El envío de mensajes se realiza por un medio abierto (difusión) o por medio de canales específicos. Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación Operaciones para reetiquetar canales y restringir el acceso a éstos. 29 / 35 Francisco Hernández Quiroz Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Sintaxis Semántica Ejemplos Sintaxis Semántica Ejemplos Sintaxis I Lógica Computacional Lenguajes de Programación 30 / 35 Sintaxis II Para comenzar, las acciones básicas de comunicación entre procesos: P es la elección arbitraria de un proceso tomado del conjunto de procesos indexado por I; λ ::= τ | α!m | α?m k es la composición paralela de procesos (intuitivamente, ambos procesos pueden realizarse simultáneamente); τ es la acción nula, α!m es el envío de m por el puerto de salida del canal α y α?m es la recepción de m por el puerto de entrada del mismo canal. Los procesos de CCS se definen así: X p ::= nil | λ . p | pi | p k p0 | p\L | p[f ] | P L es un conjunto de canales (cuyo acceso se restringirá a otros procesos, como se verá más adelante); P designa a un proceso definido por medio de una expresión del tipo i∈I P ≡def p En términos informales, la sintaxis contiene los siguientes elementos: nil es un proceso que no realiza ninguna acción y se considera primitivo; que puede tener carácter recursivo. λ es una acción; Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 31 / 35 Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 32 / 35 Programación imperativa Programación funcional Concurrencia Programación imperativa Programación funcional Concurrencia Sintaxis Semántica Ejemplos Sintaxis Semántica Ejemplos Semántica I Semántica II En términos de reglas SOE: Restricción λ Procesos resguardados p −→ q λ . p −→ p Reetiquetamiento Sumas λ p −→ q λ pj −→ q P λ 6∈ L ∪ L̄ λ p\L −→ q\L λ j∈I λ f (λ) p[f ] −→ q[f ] i∈I pi −→ q Identificadores Composición λ λ p0 k p0 −→ p00 λ p1 −→ p00 λ λ k p1 p0 k Francisco Hernández Quiroz p1 −→ p10 λ p1 −→ p0 p0 −→ p00 k p10 Lógica Computacional p0 k p −→ q λ̄ p1 −→ p10 τ p1 −→ p00 k p10 Lenguajes de Programación λ P −→ q 33 / 35 Programación imperativa Programación funcional Concurrencia Sintaxis Semántica Ejemplos Ejemplos Veamos un ejemplo muy sencillo: un buffer de capacidad 1. Un buffer es un dispositivo de almacenamiento con capacidad finita en el que un proceso (el productor) puede guardar información a la espera de que otro proceso (el consumidor) lea esta información. La lectura destruye la información guardada. Es importante que la información se guarde y se consuma de acuerdo con los permisos de los procesos. El siguiente proceso de CCS se comporta de acuerdo con la descripción anterior: B ≡def ((α?m . β!m . nil) k (β?m . γ!m . B))\{β} Francisco Hernández Quiroz Lógica Computacional Lenguajes de Programación 35 / 35 Francisco Hernández Quiroz donde P ≡def p. Lógica Computacional Lenguajes de Programación 34 / 35