PDF de programación - Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Lenguajes y Compiladores

2015

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Estructura de la materia a grandes rasgos:

Primera Parte: Lenguaje imperativo

Segunda Parte: Lenguaje aplicativo puro, y lenguaje
aplicativo con referencias y asignación

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Ejes de contenidos de la primer parte

1

Introducción a la sintaxis y la semántica de lenguajes

2 El problema de dar significado a la recursión e iteración

3 Un Lenguaje Imperativo Simple

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Un Lenguaje Imperativo Simple

LIS
(cid:104)comm(cid:105)

::= skip

(cid:104)var(cid:105) := (cid:104)intexp(cid:105)
(cid:104)comm(cid:105) ; (cid:104)comm(cid:105)
if (cid:104)boolexp(cid:105) then (cid:104)comm(cid:105) else (cid:104)comm(cid:105)
newvar (cid:104)var(cid:105) := (cid:104)intexp(cid:105) in (cid:104)comm(cid:105)
while (cid:104)boolexp(cid:105) do (cid:104)comm(cid:105)

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

(cid:104)intexp(cid:105)

::= (cid:104)natconst(cid:105)
(cid:104)var(cid:105)
(cid:104)intexp(cid:105) + (cid:104)intexp(cid:105)
(cid:104)intexp(cid:105) ∗ (cid:104)intexp(cid:105)
(cid:104)intexp(cid:105) − (cid:104)intexp(cid:105)
(cid:104)intexp(cid:105) /(cid:104)intexp(cid:105)
(cid:104)intexp(cid:105) %(cid:104)intexp(cid:105)
−(cid:104)intexp(cid:105)

(cid:104)natconst(cid:105)
(cid:104)boolconst(cid:105)

::= 0 | 1 | 2 |....
::= true | false

(cid:104)boolexp(cid:105)

::= (cid:104)boolconst(cid:105)
(cid:104)intexp(cid:105) = (cid:104)intexp(cid:105)
(cid:104)intexp(cid:105) < (cid:104)intexp(cid:105)
(cid:104)intexp(cid:105) ≤ (cid:104)intexp(cid:105)
(cid:104)intexp(cid:105) > (cid:104)intexp(cid:105)
(cid:104)intexp(cid:105) ≥ (cid:104)intexp(cid:105)
¬(cid:104)boolexp(cid:105)
(cid:104)boolexp(cid:105) ∨ (cid:104)boolexp(cid:105)
(cid:104)boolexp(cid:105) ∧ (cid:104)boolexp(cid:105)

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Características de LIS

Hay sólo dos tipos de expresiones: enteras y booleanas

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Características de LIS

Hay sólo dos tipos de expresiones: enteras y booleanas
Las expresiones enteras siempre se pueden evaluar, y su
resultado es un entero.Todas las funciones primitivas
(incluida la división) son funciones totales.

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Características de LIS

Hay sólo dos tipos de expresiones: enteras y booleanas
Las expresiones enteras siempre se pueden evaluar, y su
resultado es un entero.Todas las funciones primitivas
(incluida la división) son funciones totales.
Sólo posee variables que adoptan valores enteros. Luego
la noción de estado se refleja en la siguiente definición:

Conjunto de estados:

Σ = (cid:104)var(cid:105) → Z

(la memoria posee infinitos lugares que siempre alojan un
número entero).

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Significado de los comandos de LIS (sin iteración)

Todos los comandos terminan su ejecución (no necesitamos
⊥Σ), y el único resultado posible es un estado.

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Significado de los comandos de LIS (sin iteración)

Todos los comandos terminan su ejecución (no necesitamos
⊥Σ), y el único resultado posible es un estado.

Funciones semánticas:
[[_]]intexp ∈ (cid:104)intexp(cid:105) → Σ → Z
[[_]]boolexp ∈ (cid:104)boolexp(cid:105) → Σ → {V , F}
[[_]]comm ∈ (cid:104)comm(cid:105) → Σ → Σ

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Primeras ecuaciones semánticas

[[skip]]σ = σ

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Primeras ecuaciones semánticas

[[skip]]σ
[[v := e]]σ = [σ|v : [[e]]σ]

= σ

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Primeras ecuaciones semánticas

= σ

[[skip]]σ
[[v := e]]σ = [σ|v : [[e]]σ]
[[c0; c1]]σ = [[c1]]([[c0]]σ)

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Primeras ecuaciones semánticas

[[skip]]σ
[[v := e]]σ
[[c0; c1]]σ
[[if e then c else c(cid:48)]]σ = if [[e]]σ then [[c]]σ else [[c(cid:48)]]σ

= σ
= [σ|v : [[e]]σ]
= [[c1]]([[c0]]σ)

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Primeras ecuaciones semánticas

[[skip]]σ
[[v := e]]σ
[[c0; c1]]σ
[[if e then c else c(cid:48)]]σ = if [[e]]σ then [[c]]σ else [[c(cid:48)]]σ
Ejemplo:

= σ
= [σ|v : [[e]]σ]
= [[c1]]([[c0]]σ)

[[x := x − 1]]σ = [σ|x : [[x − 1]]σ]

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Primeras ecuaciones semánticas

[[skip]]σ
[[v := e]]σ
[[c0; c1]]σ
[[if e then c else c(cid:48)]]σ = if [[e]]σ then [[c]]σ else [[c(cid:48)]]σ
Ejemplo:

= σ
= [σ|v : [[e]]σ]
= [[c1]]([[c0]]σ)

[[x := x − 1]]σ = [σ|x : [[x − 1]]σ]

= [σ|x : [[x]]σ − [[1]]σ]

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Primeras ecuaciones semánticas

[[skip]]σ
[[v := e]]σ
[[c0; c1]]σ
[[if e then c else c(cid:48)]]σ = if [[e]]σ then [[c]]σ else [[c(cid:48)]]σ
Ejemplo:

= σ
= [σ|v : [[e]]σ]
= [[c1]]([[c0]]σ)

[[x := x − 1]]σ = [σ|x : [[x − 1]]σ]
= [σ|x : [[x]]σ − [[1]]σ]
= [σ|x : σ x − 1]

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Semántica de newvar

Función “restauración de v según σ”:

fv ,σσ(cid:48) = [σ(cid:48)|v : σv ]

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Semántica de newvar

Función “restauración de v según σ”:

fv ,σσ(cid:48) = [σ(cid:48)|v : σv ]

[[newvar v := e in c]]σ = fv ,σ([[c]][σ|v : [[e]]σ])

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Semántica de newvar

Función “restauración de v según σ”:

fv ,σσ(cid:48) = [σ(cid:48)|v : σv ]

[[newvar v := e in c]]σ = fv ,σ([[c]][σ|v : [[e]]σ])

Notación lambda para la función restauración:
fv ,σ = λσ(cid:48) ∈ Σ. [σ(cid:48)|v : σv ]

[[newvar v := e in c]]σ = (λσ(cid:48) ∈ Σ. [σ(cid:48)|v : σv ]) ([[c]][σ|v : [[e]]σ])

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

¿Qué función en Z → Z⊥ computa haskell?

g :: Int -> Int
g n = if n == 0 then 0

else if n == 1 then 1

else g (n-2)

Es la menor solución en Z → Z⊥ de la ecuación recursiva:

si n = 0
si n = 1
caso contrario (c.c.)

(ER)

 0

f n =

1
f (n − 2)

La ecuación ER define una familia de funciones.

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Una función es solución de ER si y sólo si es punto fijo de:

 0

si n = 0
si n = 1
si n (cid:54)∈ {0, 1}

F f n =

1
f (n − 2)

El menor punto fijo es:

({F i ⊥Z→Z⊥|i ≥ 0})

sup
Z→Z⊥

donde ⊥Z→Z⊥ es el elemento mínimo de Z → Z⊥, es decir, la
función que devuelve siempre ⊥.

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Dificultades para dar significado a la iteración

El comando

while b do c

debe satisfacer la propiedad:

[[while b do c]]σ = if [[b]]σ then [[c; while b do c]]σ else [[skip]]σ

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

Dificultades para dar significado a la iteración

El comando

while b do c

debe satisfacer la propiedad:

[[while b do c]]σ = if [[b]]σ then [[c; while b do c]]σ else [[skip]]σ

=

σ

(cid:40) [[while b do c]]([[c]]σ) si [[b]]σ

si ¬[[b]]σ

Lenguajes y Compiladores

Introducción a la sintaxis y la semántica de lenguajes
El problema de dar significado a la recursión e iteración
Un Lenguaje Imperativo Simple

¿Define esta propiedad una función en Σ → Σ⊥?

el domin