PDF de programación - El lenguaje Iswim

1 El lenguaje Iswim

Este lenguaje fue introducido por Peter Landing, y aunque nunca fue imple-
mentado, fue el primero en su tipo en ser presentado con una clara comprensión
de los principios que subyacen en su diseño.

El lenguaje Iswim propone incorporar una componente imperativa a un
lenguaje aplicativo eager mediante la adición de referencias como un tipo más
de valores, y que por lo tanto pueden ser devueltos por una función, o pasa-
dos como valor que recibe una función. Este principio es incorporado en los
lenguajes Algol 68, Basel, Gendaken y Standard ML.

El lenguaje Iswim extiende al lenguaje aplicativo eager mediante las sigu-

ientes construcciones:

(cid:104)exp(cid:105) ::= ref (cid:104)exp(cid:105) | val (cid:104)exp(cid:105) | (cid:104)exp(cid:105) := (cid:104)exp(cid:105)| (cid:104)exp(cid:105) =ref (cid:104)exp(cid:105)

La expresión ref e extiende el estado generando una referencia nueva que aloja
el valor producido por e. Note que no hay restricciones (al menos en la sintaxis)
para el valor que puede adquirir e. La expresión val e estará denida cuando
e produzca un valor de tipo referencia, y la expresión completa devolverá lo
alojado en esa referencia. La expresión e := e(cid:48) produce la modicación en el
estado producto de la asignación (e debe producir un valor de tipo referencia),
devolviendo el valor de la expresión e(cid:48).

Note que típicas construcciones del lenguaje imperativo como la secuen-
ciación, la iteración y la declaración de variables locales no se incorporan a la
sintaxis abstracta. En efecto, el orden de evaluación eager permite obtener-
las como azúcar sintáctico. Deniremos estas expresiones después de dar los
signicados denotacionales y operacionales del lenguaje.

Asumimos que Rf es un conjunto innito de referencias, no es necesario pre-
cisar con detalle qué son las referencias, aunque si quisiéramos podríamos asumir
que las mismas son, por ejemplo, números naturales. El conjunto de todos los
estados se sigue escribiendo Σ, pero ahora los estados son funciones parciales de
Rf en V . Los estados no mapean como antes identicadores en enteros, sino
referencias en valores de cualquier tipo. Esto signica que la memoria es capaz
de alojar cualquier tipo de valor (números, valores lógicos, funciones, tuplas,
referencias). Dijimos que los estados son funciones parciales: es más, si σ ∈ Σ,
entonces dom(σ) ⊂ Rf y dom(σ) es nito. Asumimos que existe una función
new que aplicada a un estado devuelve una referencia nueva: new(σ) ∈ Rf y
new(σ) (cid:54)∈ dom(σ). Para el lenguaje Iswim el conjunto de valores se extiende de
la siguiente manera:

V = Vint + Vbool + Vf un + Vtuple + Vref
D = (Σ × V + {error, typeerror})⊥
La función ιnorm aceptará ahora un par estado-valor: ιnorm <σ, z> ∈ D.

Como en el lenguaje aplicativo:

1

Env = (cid:104)var(cid:105) → V
Vint = Z

Vbool = B
Vf un = Σ × V → D
Vtuple = V ∗
Vref = Rf
ιint ∈ Vint → V
ιbool ∈ Vbool → V
ιf un ∈ Vf un → V
ιtuple ∈ Vtuple → V
ιref ∈ Vref → V

Las funciones ahora deben reejar la posibilidad de cambio del estado, es decir,
una función no sólo puede utilizar el valor de su argumento, sino que los cóm-
putos que realiza se efectúan en el estado resultante luego de evaluarse dicho
argumento.
Disponemos además de resultados err, tyerr,⊥ ∈ D que constituyen la deno-
tación de los errores y de la no-terminación.
funcionalidad: Si f ∈ Σ × V → D, entonces f∗ ∈ D → D se dene:

Las funciones que asisten la transferencia de control se adaptan a la nueva

f∗ ιnorm (cid:104)σ, z(cid:105) = f (cid:104)σ, z(cid:105)
f∗ err = err
f∗ tyerr = tyerr
f∗ ⊥ = ⊥

Por otro lado, si f ∈ Σ × Vint → D, entonces fint ∈ Σ × V → D se dene:

fint (cid:104)σ, ιinti(cid:105) = f (cid:104)σ, i(cid:105)
fint (cid:104)σ, ιθz(cid:105) = tyerr

(θ (cid:54)= int)

De manera similar se denen fbool, ff un, ftuple, fref .

La función semántica será de tipo:

[[_]] ∈ (cid:104)exp(cid:105) → Env → Σ → D

(cid:26) ιnorm (cid:104)σ(cid:48), σ(cid:48)r(cid:105)

La semántica de los construcciones típicamente imperativas es la siguiente:

[[val e]]ησ = (λ(cid:104)σ(cid:48), r(cid:105) ∈ Σ×Vref .
[[ref e]]ησ = (λ(cid:104)σ(cid:48), z(cid:105) ∈ Σ × V. ιnorm (cid:104)[σ(cid:48)|r : z], ιref r(cid:105))∗([[e]]ησ)
donde r = new(σ(cid:48))

err

r ∈ dom(σ(cid:48))
c.c.

)ref∗([[e]]ησ)

2

[[e := e(cid:48)]]ησ = (λ(cid:104)σ(cid:48), r(cid:105) ∈ Σ × Vref . (λ(cid:104)σ(cid:48)(cid:48), z(cid:105) ∈ Σ × V. ιnorm (cid:104)[σ(cid:48)(cid:48)|r : z], z(cid:105))∗

[[e =ref e(cid:48)]]ησ = (λ(cid:104)σ(cid:48), r(cid:105) ∈ Σ×Vref . (λ(cid:104)σ(cid:48)(cid:48), z(cid:105) ∈ Σ×Vref . ιnorm (cid:104)σ(cid:48)(cid:48), ιboolr = r(cid:48)(cid:105))ref∗

([[e(cid:48)]]ησ(cid:48)))ref∗([[e]]ησ)

([[e(cid:48)]]ησ(cid:48)))ref∗([[e]]ησ)

La semántica de las construcciones aplicativas requiere solamente adaptar la
funcionalidad. La semántica de 0 o true, es trivial, salvo que hay que promover
el resultado para que sea un elemento de D, y el estado por supuesto no se
modica:

[[0]]ησ = ιnorm (cid:104)σ, ιint0(cid:105)
[[true]]ησ = ιnorm (cid:104)σ, ιboolT(cid:105)

Para evaluar −e se evalúa e y se chequea que dé entero (en caso contrario, el
subíndice int se encargará de disparar un error de tipos) y que no se haya pro-
ducido ya algún error (en cuyo caso, el subíndice * se encargará de propagarlo).
Si todo anda bien se devuelve el entero correspondiente promoviendolo para que
sea un D.

[[−e]]ησ = (λ(cid:104)σ(cid:48), i(cid:105) ∈ Σ × Vint. ιnorm (cid:104)σ(cid:48), ιint − i(cid:105))int∗([[e]]ησ)

Lo mismo ocurre con la negación lógica:

[[¬e]]ησ = (λ(cid:104)σ(cid:48), b(cid:105) ∈ Σ × Vbool. ιnorm (cid:104)σ(cid:48), ιbool¬b(cid:105))bool∗([[e]]ησ)

Un recurso similar sirve para los operadores binarios (salvo división y módulo):

[[e+e(cid:48)]]ησ = (λ(cid:104)σ(cid:48), i(cid:105) ∈ Σ×Vint.(λ(cid:104)σ(cid:48)(cid:48), j(cid:105) ∈ Σ×Vint. ιnorm (cid:104)σ(cid:48)(cid:48), ιinti + j(cid:105))int∗([[e(cid:48)]]ησ(cid:48)))int∗([[e]]ησ)

Los operadores típicos del cálculo lambda se adaptan como sigue:

[[ee(cid:48)]]ησ = (λ(cid:104)σ(cid:48), f(cid:105) ∈ Σ × Vf un. f∗([[e(cid:48)]]ησ(cid:48)))f un∗([[e]]ησ)
[[λv. e(cid:48)]]ησ = ιnorm (cid:104)σ, ιf un(λ(cid:104)σ(cid:48), z(cid:105) . [[e]][η|v : z]σ(cid:48))(cid:105)

Finalmente, la semántica del letrec se dene como sigue:

[[letrec w = λv. e in e(cid:48)]]ησ = [[e(cid:48)]][η|w : ιf unf ]σ

donde

f = YVf un F
F f (cid:104)σ(cid:48), z(cid:105) = [[e]][η|w : ιf unf|v : z]σ(cid:48)

3

1.1 Semántica operacional de Iswim

Para dar la semántica denotacional sumamos como formas canónicas a las ref-
erencias:

(cid:104)cnf(cid:105) ::= Rf

El predicado de evaluación tendrá la siguiente forma, que reeja no sólo el
cómputo de un valor sino además la modicación del estado:

σ, e ⇒ z, σ(cid:48)

con la salvedad de que ahora los estados son funciones parciales de referencias
en formas canónicas (y no en elementos de V ). Todas las reglas aplicativas del
lenguaje eager se incorporan con la indicación explícita de cómo se transforma
el estado. Por ejemplo la regla
e ⇒ λv. e0

(e0/v → z(cid:48)) ⇒ z

e(cid:48) ⇒ z(cid:48)

ee(cid:48) ⇒ z

se transforma en:

σ, e ⇒ λv. e0, σ(cid:48) σ(cid:48), e(cid:48) ⇒ z(cid:48), σ(cid:48)(cid:48) σ(cid:48)(cid:48), (e0/v → z(cid:48)) ⇒ z, σ(cid:48)(cid:48)(cid:48)

ee(cid:48), s ⇒ z, σ(cid:48)(cid:48)(cid:48)

De manera similar se transforman las demás reglas del lenguaje aplicativo ea-
ger. Las nuevas reglas que describen el comportamiento de las construcciones
típicamente imperativas son las siguientes:

σ, e ⇒ r, σ(cid:48) σ(cid:48), e(cid:48) ⇒ z, σ(cid:48)(cid:48)
σ, e := e(cid:48) ⇒ z, [σ(cid:48)(cid:48)|r : z]

σ, e ⇒ z, σ(cid:48)

σ, ref e ⇒ r, [σ(cid:48)|r : z]

(r = new(σ(cid:48)))

σ, e ⇒ r, σ(cid:48)

σ, val e ⇒ σ(cid:48)r, σ(cid:48)
σ, e ⇒ r, σ(cid:48) σ(cid:48), e(cid:48) ⇒ r(cid:48), σ(cid:48)(cid:48)
σ, e =ref e(cid:48) ⇒ (cid:98)r = r(cid:48)(cid:99), σ(cid:48)(cid:48)

(r ∈ dom(σ(cid:48)))

1.2 Algunas propiedades del fragmento imperativo
Dado que una frase de tipo (cid:104)exp(cid:105) tiene el potencial de simultaneamente producir
un efecto en el estado y a su vez un valor, podemos modelar la secuencia de
comandos a través de un let en el cual el valor producido por la expresión se
descarte:

e; e(cid:48) =def let v = e in e(cid:48)

(v /∈ F V e(cid:48))

4

La semántica operacional nos permite vericar el signicado esperado:

σ, e ⇒ z, σ(cid:48) σ(cid:48), e(cid:48) ⇒ z(cid:48), σ(cid:48)(cid:48)

σ, e; e(cid:48) ⇒ z(cid:48), σ(cid:48)(cid:48)

Note que la regla pone en evidencia que el valor z producido al evaluar e es
descartado.

Por supuesto que esta regla debe ser deducida de las reglas dadas, en tanto
e; e es introducido como una abreviatura. Expresándonos con precisión, es nece-
sario probar una propiedad que exprese la regla de la siguiente manera:
Propiedad Si σ, e ⇒ z, σ(cid:48) y σ(cid:48), e(cid:48) ⇒ z(cid:48), σ(cid:48)(cid:48), entonces

σ, e; e(cid:48) ⇒ z(cid:48), σ(cid:48)(cid:48)

Es un buen ejercicio vericar esta propiedad usando la regla de la aplicación,

y el hecho de que let v = e in e(cid:48) es una abreviatura de (λv. e(cid:48))e.

También podemos deducir inmediatamente una ecuación semántica para el

punto y coma:

[[e; e(cid:48)]]ησ = (λ(cid:104)σ(cid:48), z(cid:105) . [[e(cid:48)]]ησ(cid:48))∗([[e]]ησ)

Nuevamente la ecuación reeja el hecho de que el valor z producido por la
evaluación de e es descartado. En efecto, estamos usando la propiedad [[e(cid:48)]]η =
[[e(cid:48)]][η|v : z], garantizada por el teorema de coincidencia y por la condición
v /∈ F V e(cid:48). Note que aquí es fundamental el orden de evaluación eager para que
la secuencia de ejecución de los comandos involucrados se respete.

Ampliar el ambiente con una nueva variable que denote una referencia tam-

bién puede ser expresado mediante un let:

newvar v = e in e(cid:48) =def let v = ref e in e(cid:48)

La regla resultante de esta denición es la siguiente (que deb